(13steps total) PrintForm Definitions Lemmas ElisTarskiPf B 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 reps t) L(tr/S)
5. RespectsNot(Tr; L)
6. ReflectsProp(Tr; tr; Tr)
7. S: Term
8. S = s(NOT(tr))
s(NOT(tr)) reps NOT(tr/s(NOT(tr)))
By: Rewrite Thm* t,e:Term. NOT(t)/e = NOT(t/e) 0
Generated subgoal:

1 s(NOT(tr)) reps NOT(tr)/s(NOT(tr))1 step

About:
applyfunctionequalpropimpliesallexists

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