PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

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

3 = 3
By: Using [`T',Formula;`eq',eqF;`P',(x. x(eqF) concl);`L',hyp;`z',v] (FwdThru Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [-10])
Generated subgoal:

119. v(eqF) concl
3 = 3

About:
equalassertlistintapplynatural_number
pairmemberlambdaifthenelseboolbtrue