Nuprl Lemma : rec-combined-class-opt-2-classrel
∀[B,F,init,X,Y,es,e,v:Top]. (v ∈ F|X, Y, Prior(self)?init|(e) ~ v ∈ F|X, Y, Y|(e))
Proof
Definitions occuring in Statement :
simple-comb-3: F|X, Y, Y|,
rec-combined-class-opt-2: F|X, Y, Prior(self)?init|,
primed-class-opt: Prior(X)?b,
classrel: v ∈ X(e),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
top_wf
Latex:
\mforall{}[B,F,init,X,Y,es,e,v:Top]. (v \mmember{} F|X, Y, Prior(self)?init|(e) \msim{} v \mmember{} F|X, Y, Y|(e))
Date html generated:
2015_07_22-PM-00_15_13
Last ObjectModification:
2015_01_28-AM-10_44_07
Home
Index