---

{ [T:Type]
    ((x,y:T.  Dec(x = y))
     ([R:T  T  ]
          (SWellFounded(x R y)
           rel_finite(T;R)
           (x,y:T.  Dec(x R y))
           (x,y:T.  Dec(x (R^*) y))))) }

{ Proof }

---

Definitions occuring in Statement :  decidable: Dec(P),  uall: [x:A]. B[x],  prop: ,  infix_ap: x f y,  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  universe: Type,  equal: s = t,  rel_star: R^*,  rel_finite: rel_finite(T;R),  strongwellfounded: SWellFounded(R[x; y])
Definitions :  uall: [x:A]. B[x],  implies: P  Q,  all: x:A. B[x],  prop: ,  infix_ap: x f y,  member: t  T,  or: P  Q,  so_lambda: x y.t[x; y],  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  so_apply: x[s1;s2]
Lemmas :  decidable__rel_plus,  decidable_functionality,  rel_star_wf,  rel_plus_wf,  rel-star-iff-rel-plus-or,  decidable__or,  decidable_wf,  rel_finite_wf,  strongwellfounded_wf

---

\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
                (SWellFounded(x  R  y)
                {}\mRightarrow{}  rel\_finite(T;R)
                {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  R  y))
                {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  rel\_star(T;  R)  y)))))


Date html generated: 2011_08_16-AM-10_18_51
Last ObjectModification: 2011_06_18-AM-09_07_43

Home Index