---

{ [A:Type]. [B,C:A  Type].
    eq:EqDecider(A). f:a:A fp-> B[a]. g:a:A fp-> C[a]. x:A.
      [P:a:A  B[a]  ]. [Q:a:A  C[a]  ].
        ((x:A
            ((C[x] r B[x]) c (P[x;g(x)]  Q[x;g(x)])) supposing 
               ((x  dom(f)) and 
               (x  dom(g))))
         {z != f(x) ==> P[y;z]  z != g(x) ==> Q[y;z] supposing g  f}) }

{ Proof }

---

Definitions occuring in Statement :  fpf-sub: f  g,  fpf-val: z != f(x) ==> P[a; z],  fpf-ap: f(x),  fpf-dom: x  dom(f),  fpf: a:A fp-> B[a],  subtype_rel: A r B,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  cand: A c B,  prop: ,  guard: {T},  so_apply: x[s1;s2],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  universe: Type,  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  so_apply: x[s],  prop: ,  implies: P  Q,  uimplies: b supposing a,  cand: A c B,  so_apply: x[s1;s2],  guard: {T},  fpf-sub: f  g,  fpf-val: z != f(x) ==> P[a; z],  member: t  T,  so_lambda: x.t[x]
Lemmas :  pair_wf,  assert_wf,  fpf-dom_wf,  fpf-trivial-subtype-top,  assert_witness,  fpf-ap_wf,  fpf_wf,  deq_wf

---

\mforall{}[A:Type].  \mforall{}[B,C:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f:a:A  fp->  B[a].  \mforall{}g:a:A  fp->  C[a].  \mforall{}x:A.
        \mforall{}[P:a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:a:A  {}\mrightarrow{}  C[a]  {}\mrightarrow{}  \mBbbP{}].
            ((\mforall{}x:A
                    ((C[x]  \msubseteq{}r  B[x])  c\mwedge{}  (P[x;g(x)]  {}\mRightarrow{}  Q[x;g(x)]))  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  (\muparrow{}x  \mmember{}  dom(g))))
            {}\mRightarrow{}  \{z  !=  f(x)  ==>  P[y;z]  {}\mRightarrow{}  z  !=  g(x)  ==>  Q[y;z]  supposing  g  \msubseteq{}  f\})


Date html generated: 2011_08_10-AM-08_02_23
Last ObjectModification: 2011_06_18-AM-08_20_25

Home Index