Nuprl - Proof: Tarski 1 1 1 1 1

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

At: Tarski 1 1 1 1 1

1. Tr: TermProp
2. tr: Term
3. L: TermProp
4. S:Term. (t:Term. S = t) L(SUBX(tr; S))
5. RespectsNot(Tr; L)
6. ReflectsProp(Tr; tr; Tr)
7. S: Term
8. S = s(NOT(tr))

s(NOT(tr)) = NOT(SUBX(tr; s(NOT(tr))))

By: Rewrite Thm* t,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e)) 0

Generated subgoal:

1 s(NOT(tr)) = SUBX(NOT(tr); s(NOT(tr))) 1 step

About:

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