---

{ f,es,X,Y,e:Top.
    (e  (f)(X,(Y)',self') ~ isl(f (X es e) ((Y)' es e) 
                                  (((f)(X,(Y)',self'))' es e))) }

{ Proof }

---

Definitions occuring in Statement :  es-rec-combined-interface1-1: (f)(X,(Y)',self'),  es-prior-val: (X)',  in-eclass: e  X,  isl: isl(x),  top: Top,  all: x:A. B[x],  apply: f a,  sqequal: s ~ t
Definitions :  es-prior-val: (X)',  lambda: x.A[x],  can-apply: can-apply(f;x),  in-eclass: e  X,  es-rec-combined-interface1-1: (f)(X,(Y)',self'),  equal: s = t,  member: t  T,  function: x:A  B[x],  all: x:A. B[x],  top: Top,  sqequal: s ~ t,  Auto: Error :Auto,  RepUR: Error :RepUR,  CollapseTHEN: Error :CollapseTHEN,  Unfold: Error :Unfold,  CollapseTHENA: Error :CollapseTHENA
Lemmas :  top_wf

---

\mforall{}f,es,X,Y,e:Top.    (e  \mmember{}\msubb{}  (f)(X,(Y)',self')  \msim{}  isl(f  (X  es  e)  ((Y)'  es  e)  (((f)(X,(Y)',self'))'  es  e)))


Date html generated: 2010_08_27-PM-02_40_54
Last ObjectModification: 2010_03_24-PM-12_39_37

Home Index