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: s ~ t
Definitions unfolded in proof : 
rec-combined-loc-class-opt-3: rec-combined-loc-class-opt-3(F;init;X;Y;Z)
, 
simple-loc-comb-4: simple-loc-comb-4(F;W;X;Y;Z)
, 
classrel: v ∈ X(e)
, 
simple-loc-comb: F|Loc; Xs|
, 
select: L[n]
, 
cons: [a / b]
, 
subtract: n - m
, 
rec-comb: rec-comb(X;f;init)
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
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:
2016_05_17-AM-09_28_07
Last ObjectModification:
2015_12_29-PM-04_02_26
Theory : classrel!lemmas
Home
Index