---

{ [Info:Type]. [es:EO+(Info)]. [A,B:Type]. [Ia1,Ia2:EClass(A)].
  [Ib1,Ib2:EClass(B)]. [g1:E(Ib1)  E(Ia1)]. [g2:E(Ib2)  E(Ia2)].
    ([{Ib1}? g1 : g2]  E([Ib1?Ib2])  E([Ia1?Ia2])) }

{ Proof }

---

Definitions occuring in Statement :  es-E-interface: E(X),  es-interface-predicate: {I},  cond-class: [X?Y],  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  conditional: [P? f : g],  uall: [x:A]. B[x],  member: t  T,  lambda: x.A[x],  function: x:A  B[x],  universe: Type,  bool-decider: bool-decider(b)
Definitions :  uall: [x:A]. B[x],  member: t  T,  conditional: [P? f : g],  prop: ,  so_lambda: x.t[x],  so_lambda: x y.t[x; y],  es-interface-predicate: {I},  es-E-interface: E(X),  assert: b,  or: P  Q,  all: x:A. B[x],  implies: P  Q,  guard: {T},  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  so_apply: x[s],  so_apply: x[s1;s2],  not: A,  iff: P  Q,  and: P  Q,  false: False,  rev_implies: P  Q,  sq_type: SQType(T),  uimplies: b supposing a,  subtype: S  T
Lemmas :  branch_wf2,  es-interface-predicate_wf,  es-E-interface_wf,  cond-class_wf,  top_wf,  not_wf,  es-interface-top,  eclass_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  bool-decider_wf,  in-eclass_wf,  assert_wf,  es-E-interface-conditional-subtype1,  is-cond-class,  es-E-interface-subtype_rel,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_elim

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[Ia1,Ia2:EClass(A)].  \mforall{}[Ib1,Ib2:EClass(B)].
\mforall{}[g1:E(Ib1)  {}\mrightarrow{}  E(Ia1)].  \mforall{}[g2:E(Ib2)  {}\mrightarrow{}  E(Ia2)].
    ([\{Ib1\}?  g1  :  g2]  \mmember{}  E([Ib1?Ib2])  {}\mrightarrow{}  E([Ia1?Ia2]))


Date html generated: 2011_08_16-PM-05_56_54
Last ObjectModification: 2011_06_20-AM-01_39_42

Home Index