---

Step * of Lemma rel-immediate-rel-plus

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (SWellFounded(R x y) ⇒ (∀x,y:T.  Dec(∃z:T. ((R x z) ∧ (R z y)))) ⇒ R+ => R!+)
BY
{ xxx(Auto
      THEN D -2
      THEN RepUR ``rel_implies rel_plus infix_ap`` 0
      THEN Assert ⌜∀n:ℕ. (0 < n ⇒ (∀x,y:T.  ((R^n x y) ⇒ (∃n:ℕ+. (R!^n x y)))))⌝⋅
      THEN Try ((Auto THEN ExRepD THEN Using [`n',⌜n⌝] (BackThruSomeHyp)⋅ THEN Complete (Auto'))))xxx }

1
.....assertion..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. f : T ⟶ ℕ
4. ∀x,y:T.  ((R x y) ⇒ f x < f y)
5. ∀x,y:T.  Dec(∃z:T. ((R x z) ∧ (R z y)))
⊢ ∀n:ℕ. (0 < n ⇒ (∀x,y:T.  ((R^n x y) ⇒ (∃n:ℕ+. (R!^n x y)))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (SWellFounded(R  x  y)  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(\mexists{}z:T.  ((R  x  z)  \mwedge{}  (R  z  y))))  {}\mRightarrow{}  R\msupplus{}  =>  R!\msupplus{})


By

---

Latex:
xxx(Auto
        THEN  D  -2
        THEN  RepUR  ``rel\_implies  rel\_plus  infix\_ap``  0
        THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}
                                      (0  <  n  {}\mRightarrow{}  (\mforall{}x,y:T.    ((R\^{}n  x  y)  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}\msupplus{}.  (R!\^{}n  x  y)))))\mkleeneclose{}\mcdot{}
        THEN  Try  ((Auto  THEN  ExRepD  THEN  Using  [`n',\mkleeneopen{}n\mkleeneclose{}]  (BackThruSomeHyp)\mcdot{}  THEN  Complete  (Auto'))))xxx

---

Home Index