---

Step * of Lemma rel-immediate-exists

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (SWellFounded(R x y) ⇒ (∀x,y:T.  Dec(∃z:T. ((R x z) ∧ (R z y)))) ⇒ (∀y:T. ((∃x:T. (R x y)) ⇒ (∃x:T. (R! x y)))))
BY
{ (Auto THEN ((InstLemma `rel-immediate-rel-plus` [⌜T⌝; ⌜R⌝])⋅ THENA Auto)) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. SWellFounded(R x y)@i
4. ∀x,y:T.  Dec(∃z:T. ((R x z) ∧ (R z y)))@i
5. y : T@i
6. ∃x:T. (R x y)@i
7. R+ => R!+
⊢ ∃x:T. (R! 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{}  (\mforall{}y:T.  ((\mexists{}x:T.  (R  x  y))  {}\mRightarrow{}  (\mexists{}x:T.  (R!  x  y)))))


By

---

Latex:
(Auto  THEN  ((InstLemma  `rel-immediate-rel-plus`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}R\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index