Thm* t:Term. s(t) = SUBX(t; s(t)) | [s_reps] |
Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); f(t))) | [s2] |
Thm* t,r,t',r':Term. t = t' & r = r'  SUBX(t; r) = SUBX(t'; r') | [qsubx_repst] |
Thm* t:Term. UP( t) = t | [qup_up_repst] |
Thm* t:Term. t = t | [up_repst] |
Def RepsTruth(L; Tr; tr) == ( S:Term. ( t:Term. S = t)  L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr) | [RepsTruth] |
Def ReflectsProp(P; qP; Tr) == t,qt:Term. qt = t  {Tr(SUBX(qP; qt))  Tr(t)} | [ReflectsProp] |