---

{ [B,F,init,X,es,e,v:Top].
    (v  F|Loc, X, Prior(self)?init|(e) 
    ~ v  F|Loc,X, Prior(F|Loc, X, Prior(self)?init|)?init|(e)) }

{ Proof }

---

Definitions occuring in Statement :  simple-loc-comb-2: F|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

---

\mforall{}[B,F,init,X,es,e,v:Top].
    (v  \mmember{}  F|Loc,  X,  Prior(self)?init|(e)  \msim{}  v  \mmember{}  F|Loc,X,  Prior(F|Loc,  X,  Prior(self)?init|)?init|(e))


Date html generated: 2011_08_17-PM-06_24_30
Last ObjectModification: 2011_07_23-AM-10_45_50

Home Index