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

At: Tarski 1 1 1 2 1 1 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. Tr(SUBX(tr; S)) Tr(SUBX(tr; S))
False
By: FwdThru Thm* (P P) False [7]
Generated subgoals:

None

About:
applyfunctionequalpropimpliesfalse

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