---

{ f,es,X,Y,e:Top.
    ((f)(X,(Y)',self')(e) ~ outl(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)',  eclass-val: X(e),  outl: outl(x),  top: Top,  all: x:A. B[x],  apply: f a,  sqequal: s ~ t
Definitions :  es-prior-val: (X)',  lambda: x.A[x],  es-rec-combined-interface: f(Y;(Z)';self'),  do-apply: do-apply(f;x),  es-rec-combined-interface1-1: (f)(X,(Y)',self'),  eclass-val: X(e),  equal: s = t,  member: t  T,  function: x:A  B[x],  all: x:A. B[x],  top: Top,  sqequal: s ~ t,  Auto: Error :Auto,  CollapseTHEN: Error :CollapseTHEN,  CollapseTHENA: Error :CollapseTHENA
Lemmas :  top_wf

---

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


Date html generated: 2010_08_27-PM-02_40_57
Last ObjectModification: 2010_03_24-PM-12_41_37

Home Index