---

{ [T:Type]. [R,Q:T  T  ]. [P:T  ].
    (Trans(T;x,y.Q x y)
     R => Q
        (x,y:T.  (((P x)  (P y))  (((R x y)  (x = y))  (R y x))))
        (x,y:T.  (((P x)  (P y))  (R x y  Q x y))) 
       supposing x,y:T.  ((Q x y)  ((Q y x)))) }

{ Proof }

---

Definitions occuring in Statement :  trans: Trans(T;x,y.E[x; y]),  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  iff: P  Q,  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t,  rel_implies: R1 => R2
Definitions :  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  uimplies: b supposing a,  all: x:A. B[x],  not: A,  and: P  Q,  or: P  Q,  iff: P  Q,  member: t  T,  false: False,  rev_implies: P  Q,  so_lambda: x y.t[x; y],  infix_ap: x f y,  so_apply: x[s1;s2],  rel_implies: R1 => R2
Lemmas :  rel_implies_wf,  not_wf,  trans_wf

---

\mforall{}[T:Type].  \mforall{}[R,Q:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T;x,y.Q  x  y)
    {}\mRightarrow{}  R  =>  Q
          {}\mRightarrow{}  (\mforall{}x,y:T.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (((R  x  y)  \mvee{}  (x  =  y))  \mvee{}  (R  y  x))))
          {}\mRightarrow{}  (\mforall{}x,y:T.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (R  x  y  \mLeftarrow{}{}\mRightarrow{}  Q  x  y))) 
          supposing  \mforall{}x,y:T.    ((Q  x  y)  {}\mRightarrow{}  (\mneg{}(Q  y  x))))


Date html generated: 2011_08_16-AM-11_18_15
Last ObjectModification: 2011_06_20-AM-00_23_22

Home Index