Nuprl - Proof: Tarski 1 1 1 2 1 1 1

(13steps total) PrintForm Definitions Lemmas ElisTarskiPf B 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 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

By: Assert (Tr(NOT(tr/S)) Tr(tr/S)) THENA Using [`B',(L(tr/S))] (BackThru Thm* B (A B & C) (A C)) THEN OnHyps [9;7] Thin

Generated subgoal:

1 7. Tr(tr/S) Tr(NOT(tr/S))
8. Tr(NOT(tr/S)) Tr(tr/S)
False 2 steps

About:

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