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
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. disjoint(eqF;hyp;concl)
10. (v.if v(eqF) hyp3 ;v(eqF) concl3 else 3 fi) Assignment
11. z: Formula
12. z(eqF) concl

(v.if v(eqF) hyp3 ;v(eqF) concl3 else 3 fi) | z
By: Using [`L',L;`eqS',eqS;`eqF',eqF;`hyp',hyp;`concl',concl;`z',z] (FwdThru Thm* L:Sequent List, eqS:{Sequent=}, eqF:{Formula=}. sL.((s) = 0) (hyp,concl:Formula List. < hyp,concl > (eqS) L (z:Formula. z(eqF) hyp z(eqF) concl (v:Var. z = v))) [-5])
Generated subgoals:

1 z(eqF) hyp z(eqF) concl
213. v:Var. z = v
(v.if v(eqF) hyp3 ;v(eqF) concl3 else 3 fi) | z

About:
lambdaifthenelselistequalintapply
natural_numberassertpairmemberor