---

Step * of Lemma simple-dependent-choice

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀x:T. ∃y:T. R[x;y]) ⇒ (∀x0:T. ∃f:ℕ ⟶ T. (((f 0) = x0 ∈ T) ∧ (∀i:ℕ. R[f i;f (i + 1)]))))
BY
{ (Auto THEN (Skolemize  (-2) `F' THENA Auto) THEN D 0 With ⌜λn.(F^n x0)⌝  THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x:T. ∃y:T. R[x;y]
4. x0 : T
5. F : x:T ⟶ T
6. ∀x:T. R[x;F x]
7. (F^0 x0) = x0 ∈ T
8. i : ℕ
⊢ R[F^i x0;F^i + 1 x0]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:T.  \mexists{}y:T.  R[x;y])  {}\mRightarrow{}  (\mforall{}x0:T.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  (((f  0)  =  x0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  R[f  i;f  (i  +  1)]))))


By

---

Latex:
(Auto  THEN  (Skolemize    (-2)  `F'  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}\mlambda{}n.(F\^{}n  x0)\mkleeneclose{}    THEN  Reduce  0  THEN  Auto)

---

Home Index