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