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