At: zero rank valid or falsifiable 1 1 1 1 1 1 2 1 2 1 1 1 1 2 1 1 1 1
1. L: Sequent List
2. eqS: {Sequent=
}
3. eqF: {Formula=}
4. 
s
L.(
(s) = 0)
5. 
sL.disjoint(eqF;s.H;s.C)
6. hyp: Formula List
7. concl: Formula List
8. < hyp,concl > (eqS) L
9. disjoint(eqF;hyp;concl)
10. (
v.if 
v
(eqF) hyp
3 ;v(eqF) concl3
else 3
fi) Assignment
11. z: Formula
12. z(eqF) hyp
13. v: Var
14. z = v
15. v(eqF) hyp = true
if true3 ;v(eqF) concl3 else 3 fi = 3
By: Reduce 0
Generated subgoals:None
About:
