---

Step * of Lemma unique-minimal-wellfounded-implies

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (decidable-non-minimal(T;x,y.R[x;y])
  ⇒ WellFnd{i}(T;x,y.R[x;y])
  ⇒ (∀m:T. (unique-minimal(T;x,y.R[x;y];m) ⇒ (∀y:T. (↓m ((λx,y. R[x;y])^*) y)))))
BY
{ (Auto THEN ((MoveToConcl (-1) THEN BackThruHyp' 4) THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. decidable-non-minimal(T;x,y.R[x;y])@i
4. ∀[P:T ⟶ ℙ]. ((∀j:T. ((∀k:T. (R[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T. P[n]})@i'
5. m : T@i
6. unique-minimal(T;x,y.R[x;y];m)@i
7. j : T@i
8. ∀k:T. (R[k;j] ⇒ (↓m ((λx,y. R[x;y])^*) k))@i
⊢ ↓m ((λx,y. R[x;y])^*) j

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (decidable-non-minimal(T;x,y.R[x;y])
    {}\mRightarrow{}  WellFnd\{i\}(T;x,y.R[x;y])
    {}\mRightarrow{}  (\mforall{}m:T.  (unique-minimal(T;x,y.R[x;y];m)  {}\mRightarrow{}  (\mforall{}y:T.  (\mdownarrow{}m  rel\_star(T;  \mlambda{}x,y.  R[x;y])  y)))))


By

---

Latex:
(Auto  THEN  ((MoveToConcl  (-1)  THEN  BackThruHyp'  4)  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index