Nuprl Lemma : rec-combined-loc-class-opt-3-classrel

[B,F,init,X,Y,Z,es,e,v:Top].
  (v ∈ rec-combined-loc-class-opt-3(F;init;X;Y;Z)(e) 
  v ∈ simple-loc-comb-4(F;X;Y;Z;Prior(rec-combined-loc-class-opt-3(F;init;X;Y;Z))?init)(e))


Proof




Definitions occuring in Statement :  simple-loc-comb-4: simple-loc-comb-4(F;W;X;Y;Z) rec-combined-loc-class-opt-3: rec-combined-loc-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: t
Lemmas :  top_wf

Latex:
\mforall{}[B,F,init,X,Y,Z,es,e,v:Top].
    (v  \mmember{}  rec-combined-loc-class-opt-3(F;init;X;Y;Z)(e) 
    \msim{}  v  \mmember{}  simple-loc-comb-4(F;X;Y;Z;Prior(rec-combined-loc-class-opt-3(F;init;X;Y;Z))?init)(e))



Date html generated: 2015_07_22-PM-00_15_15
Last ObjectModification: 2015_01_28-AM-10_44_01

Home Index