---

{ [A,C:Type]. [B1,B2:A  Type].
    (eq:EqDecider(A). f,g:x:A fp-> B1[x] List. R:C List  C  .
       (fpf-union-compatible(A;C;x.B1[x];eq;R;f;g)
        fpf-union-compatible(A;C;x.B2[x];eq;R;f;g))) supposing 
       ((x:A. (B1[x] r B2[x])) and 
       (a:A. (B2[a] r C))) }

{ Proof }

---

Definitions occuring in Statement :  fpf-union-compatible: fpf-union-compatible(A;C;x.B[x];eq;R;f;g),  fpf: a:A fp-> B[a],  subtype_rel: A r B,  bool: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  list: type List,  universe: Type,  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  so_apply: x[s],  implies: P  Q,  fpf-union-compatible: fpf-union-compatible(A;C;x.B[x];eq;R;f;g),  member: t  T,  and: P  Q,  exists: x:A. B[x],  prop: ,  so_lambda: x.t[x],  rev_implies: P  Q,  rev_uimplies: rev_uimplies(P;Q),  rev_subtype_rel: A r B,  cand: A c B,  subtype: S  T,  or: P  Q,  guard: {T}
Lemmas :  assert_wf,  fpf-dom_wf,  fpf-trivial-subtype-top,  fpf-union-compatible_wf,  implies_weakening_uimplies,  subtype_rel_wf,  subtype_rel_functionality_wrt_implies,  subtype_rel_weakening,  ext-eq_inversion,  ext-eq_weakening,  bool_wf,  fpf_wf,  deq_wf,  l_member_subtype,  fpf-ap_wf,  l_member_wf,  not_wf

---

\mforall{}[A,C:Type].  \mforall{}[B1,B2:A  {}\mrightarrow{}  Type].
    (\mforall{}eq:EqDecider(A).  \mforall{}f,g:x:A  fp->  B1[x]  List.  \mforall{}R:C  List  {}\mrightarrow{}  C  {}\mrightarrow{}  \mBbbB{}.
          (fpf-union-compatible(A;C;x.B1[x];eq;R;f;g)
          {}\mRightarrow{}  fpf-union-compatible(A;C;x.B2[x];eq;R;f;g)))  supposing 
          ((\mforall{}x:A.  (B1[x]  \msubseteq{}r  B2[x]))  and 
          (\mforall{}a:A.  (B2[a]  \msubseteq{}r  C)))


Date html generated: 2011_08_10-AM-07_56_19
Last ObjectModification: 2011_06_18-AM-08_17_10

Home Index