(COMMENT

Sequent calculus modulo, by Éric Deplagne 
   (based on ESSLLI student session 2000)

)

(VAR b  a  g  f  u  t  s  y  x)

(THEORY (AC * virg))

(RULES

substt(ef(x),y) -> ef(substt(x,y)) 
substf(Pe(x),y) -> Pe(substt(x,y)) 
substf(neg(f),s) -> neg(substf(f,s)) 
substf(and(f,g),s) -> and(substf(f,s),substf(g,s)) 
substf(or(f,g),s) -> or(substf(f,s),substf(g,s)) 
substf(imp(f,g),s) -> imp(substf(f,s),substf(g,s)) 
substf(forall(f),s) -> forall(substf(f,.(1,ron(s,shift)))) 
substf(exists(f),s) -> exists(substf(f,.(1,ron(s,shift)))) 
substt(x,id) -> x 
substf(f,id) -> f 
substt(substt(x,s),t) -> substt(x,ron(s,t)) 
substf(substf(f,s),t) -> substf(f,ron(s,t)) 
substt(1,.(x,s)) -> x 
ron(id,s) -> s 
ron(shift,.(x,s)) -> s 
ron(ron(s,t),u) -> ron(s,ron(t,u)) 
ron(.(x,s),t) -> .(substt(x,t),ron(s,t)) 
ron(s,id) -> s 
.(1,shift) -> id 
.(substt(1,s),ron(shift,s)) -> s 
virg(emptyfset,a) -> a 
virg(a,a) -> a 
*(emptysset,a) -> a 
*(a,a) -> a 
neg(neg(f)) -> f 
and(f,f) -> f 
or(f,f) -> f 
imp(f,g) -> or(neg(f),g) 
exists(f) -> neg(forall(neg(f))) 
sequent(virg(convf(neg(f)),a),b) -> sequent(a,virg(convf(f),b)) 
sequent(convf(neg(f)),b) -> sequent(emptyfset,virg(convf(f),b)) 
sequent(a,virg(convf(neg(f)),b)) -> sequent(virg(convf(f),a),b) 
sequent(a,convf(neg(f))) -> sequent(virg(convf(f),a),emptyfset) 
sequent(virg(convf(and(f,g)),a),b) -> 
sequent(virg(convf(g),virg(convf(f),a)),b) 
sequent(convf(and(f,g)),b) -> sequent(virg(convf(f),convf(g)),b) 
sequent(a,virg(convf(or(f,g)),b)) -> 
sequent(a,virg(virg(convf(f),convf(g)),b)) 
sequent(a,convf(or(f,g))) -> sequent(a,virg(convf(f),convf(g))) 
convs(sequent(a,virg(convf(and(f,g)),b))) -> 
*(convs(sequent(a,virg(convf(f),b))),convs(sequent(a,virg(convf(g),b)))) 
convs(sequent(a,convf(and(f,g)))) ->
*(convs(sequent(a,convf(f))),convs(sequent(a,convf(g)))) 
convs(sequent(virg(convf(or(f,g)),a),b)) ->
*(convs(sequent(virg(convf(f),a),b)),convs(sequent(virg(convf(g),a),b))) 
convs(sequent(convf(or(f,g)),b)) -> 
*(convs(sequent(convf(f),b)),convs(sequent(convf(g),b))) 
convs(sequent(virg(convf(f),a),virg(convf(f),b))) -> emptysset 
convs(sequent(virg(convf(f),a),convf(f))) -> emptysset 
convs(sequent(convf(f),virg(convf(f),b))) -> emptysset 
convs(sequent(convf(f),convf(f))) -> emptysset 
*(convs(sequent(virg(f,a),virg(g,b))),convs(sequent(a,b))) -> 
convs(sequent(a,b)) 
*(convs(sequent(virg(f,a),b)),convs(sequent(a,b))) -> convs(sequent(a,b)) 
*(convs(sequent(a,virg(f,b))),convs(sequent(a,b))) -> convs(sequent(a,b)) 
*(convs(sequent(virg(f,a),b)),convs(sequent(a,emptyfset))) -> 
convs(sequent(a,emptyfset)) 
*(convs(sequent(emptyfset,b)),convs(sequent(a,virg(f,b)))) -> 
convs(sequent(emptyfset,b)) 
*(convs(sequent(emptyfset,b)),convs(sequent(a,b))) -> 
convs(sequent(emptyfset,b)) 
*(convs(sequent(a,emptyfset)),convs(sequent(a,b))) -> 
convs(sequent(a,emptyfset)) 
*(convs(sequent(emptyfset,emptyfset)),convs(sequent(a,b))) -> 
convs(sequent(emptyfset,emptyfset)) 

)