Nuprl Lemma : TC-min

[Dom:Type]. ∀[R,Q:Dom ─→ Dom ─→ ℙ].
  ((∀x,y,z:Dom.  ((Q y)  (Q z)  (Q z)))
   (∀x,y:Dom.  ((R y)  (Q y)))
   (∀x,y:Dom.  (TC(λa,b.R b)(x,y)  (Q y))))


Proof




Definitions occuring in Statement :  TC: TC(λx,y.F[x; y])(a,b) uall: [x:A]. B[x] prop: all: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x] universe: Type
Lemmas :  TC_wf all_wf transitive-closure-minimal rel_implies_wf
\mforall{}[Dom:Type].  \mforall{}[R,Q:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y,z:Dom.    ((Q  x  y)  {}\mRightarrow{}  (Q  y  z)  {}\mRightarrow{}  (Q  x  z)))
    {}\mRightarrow{}  (\mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (Q  x  y)))
    {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  (Q  x  y))))



Date html generated: 2015_07_17-AM-07_52_34
Last ObjectModification: 2015_01_30-AM-01_13_28

Home Index