At: zero rank valid or falsifiable 1 1 2 1 1 1 1 1 1 1 1 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. z: Sequent
7. x: Formula
8. x(eqF) z.H
9. x(eqF) z.C
10. a: Assignment
11. Fz.H.a |= F
12. Fz.C.a |
F
13. a |= x
a |= z
By: Using [`T',Formula;`eq',eqF;`P',(
F. a | F);`L',z.C;`z',x]
(FwdThru
Thm* eq:{T=}, P:(T
Prop), L:T List.
xL.P(x) 
(z:T. z(eq) L 
P(z))
[12])
Generated subgoal:| 1 | 14. a | x
a |= z |
About:
