---

{ [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(...)?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
Lemmas :  top_wf

---

\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: 2011_08_17-PM-06_25_01
Last ObjectModification: 2011_07_24-PM-11_48_52

Home Index