---

{ [T:Type]. [R:T  T  ].
    (rel_finite(T;R)
     (x,y:T.  Dec(x R y))
     ([P:T  ]
          y:T
            ((x:T. ((x R y)  Dec(P[x])))  Dec(x:T. ((x R y)  P[x]))))) }

{ Proof }

---

Definitions occuring in Statement :  decidable: Dec(P),  uall: [x:A]. B[x],  prop: ,  infix_ap: x f y,  so_apply: x[s],  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  and: P  Q,  function: x:A  B[x],  universe: Type,  rel_finite: rel_finite(T;R)
Definitions :  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  all: x:A. B[x],  decidable: Dec(P),  infix_ap: x f y,  so_apply: x[s],  exists: x:A. B[x],  and: P  Q,  member: t  T,  or: P  Q,  not: A,  guard: {T},  so_lambda: x.t[x],  cand: A c B,  rel_finite: rel_finite(T;R),  false: False,  l_exists: (xL. P[x])
Lemmas :  not_wf,  decidable__l_exists_better-extract,  l_member_wf,  decidable_wf,  rel_finite_wf

---

\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (rel\_finite(T;R)
    {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  R  y))
    {}\mRightarrow{}  (\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}y:T.  ((\mforall{}x:T.  ((x  R  y)  {}\mRightarrow{}  Dec(P[x])))  {}\mRightarrow{}  Dec(\mexists{}x:T.  ((x  R  y)  \mwedge{}  P[x])))))


Date html generated: 2011_08_16-AM-10_18_56
Last ObjectModification: 2011_06_18-AM-09_07_51

Home Index