(13steps total) PrintForm Definitions Lemmas ElisTarskiPf A Sections NuprlLIB Doc

At: Tarski 1 1 1 2 1 1 1
1. Tr: TermProp
2. tr: Term
3. L: TermProp
4. S: Term
5. S = s(NOT(tr))
6. S = NOT(SUBX(tr; S))
7. L(SUBX(tr; S))
8. Tr(SUBX(tr; S)) Tr(NOT(SUBX(tr; S)))
9. Tr(NOT(SUBX(tr; S))) L(SUBX(tr; S)) & Tr(SUBX(tr; S))
False
By:
Assert (Tr(NOT(SUBX(tr; S))) Tr(SUBX(tr; S))) THENA Using [`B',(L(SUBX(tr; S)))] (BackThru Thm* B (A B & C) (A C))
THEN
OnHyps [9;7] Thin
Generated subgoal:

17. Tr(SUBX(tr; S)) Tr(NOT(SUBX(tr; S)))
8. Tr(NOT(SUBX(tr; S))) Tr(SUBX(tr; S))
False		2 steps

About:
applyfunctionequalpropimpliesandfalse

(13steps total) PrintForm Definitions Lemmas ElisTarskiPf A Sections NuprlLIB Doc