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

At: Tarski 1 1 1 2 1
1. Tr: TermProp
2. tr: Term
3. L: TermProp
4. RespectsNot(Tr; L)
5. ReflectsProp(Tr; tr; Tr)
6. S: Term
7. S = s(NOT(tr))
8. S = NOT(SUBX(tr; S))
9. L(SUBX(tr; S))
False
By:
Unfold `ReflectsProp` 5
THEN
InstHyp [NOT(SUBX(tr; S));S] 5
THEN
Thin 5
Generated subgoal:

15. S: Term
6. S = s(NOT(tr))
7. S = NOT(SUBX(tr; S))
8. L(SUBX(tr; S))
9. Tr(SUBX(tr; S)) Tr(NOT(SUBX(tr; S)))
False		4 steps

About:
applyfunctionequalpropfalse

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