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

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

14. S: Term
5. S = s(NOT(tr))
6. S reps NOT(tr/S)
7. L(tr/S)
8. Tr(tr/S) Tr(NOT(tr/S))
9. Tr(NOT(tr/S)) L(tr/S) & Tr(tr/S)
False		3 steps

About:
applyfunctionequalpropfalse

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