Nuprl Lemma : rec-combined-class-opt-3-classrel
∀[B,F,init,X,Y,Z,es,e,v:Top].
(v ∈ rec-combined-class-opt-3(F;init;X;Y;Z)(e)
~ v ∈ simple-comb-4(F;X;Y;Z;Prior(rec-combined-class-opt-3(F;init;X;Y;Z))?init)(e))
Proof
Definitions occuring in Statement :
simple-comb-4: simple-comb-4(F;W;X;Y;Z),
rec-combined-class-opt-3: rec-combined-class-opt-3(F;init;X;Y;Z),
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,Z,es,e,v:Top].
(v \mmember{} rec-combined-class-opt-3(F;init;X;Y;Z)(e)
\msim{} v \mmember{} simple-comb-4(F;X;Y;Z;Prior(rec-combined-class-opt-3(F;init;X;Y;Z))?init)(e))
Date html generated:
2015_07_22-PM-00_15_17
Last ObjectModification:
2015_01_28-AM-10_44_04
Home
Index