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 ∈ (Loc,X, Prior(F|Loc, X, Prior(self)?init|)?init)(e))


Proof




Definitions occuring in Statement :  simple-loc-comb-2: (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: t
Definitions unfolded in proof :  rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init| simple-loc-comb-2: (Loc,X, Y) classrel: v ∈ X(e) simple-loc-comb: F|Loc; Xs| select: L[n] cons: [a b] subtract: m rec-comb: rec-comb(X;f;init) member: t ∈ T uall: [x:A]. B[x]

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: 2016_05_17-AM-09_27_51
Last ObjectModification: 2015_12_29-PM-04_02_53

Theory : classrel!lemmas


Home Index