---

Step * of Lemma fun-connected-induction2

∀[T:Type]
  ∀f:T ⟶ T
    ∀[R:T ⟶ T ⟶ ℙ]
      ((∀x:T. R[x;x])
      ⇒ (∀x,y:T.  x is f*(f y) ⇒ R[x;f y] ⇒ R[x;y] supposing ¬((f y) = y ∈ T))
      ⇒ {∀x,y:T.  (x is f*(y) ⇒ R[x;y])})
BY
{ xxxAutoxxx }

1
1. [T] : Type
2. f : T ⟶ T
3. [R] : T ⟶ T ⟶ ℙ
4. ∀x:T. R[x;x]
5. ∀x,y:T.  x is f*(f y) ⇒ R[x;f y] ⇒ R[x;y] supposing ¬((f y) = y ∈ T)
⊢ {∀x,y:T.  (x is f*(y) ⇒ R[x;y])}

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  T
        \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}x:T.  R[x;x])
            {}\mRightarrow{}  (\mforall{}x,y:T.    x  is  f*(f  y)  {}\mRightarrow{}  R[x;f  y]  {}\mRightarrow{}  R[x;y]  supposing  \mneg{}((f  y)  =  y))
            {}\mRightarrow{}  \{\mforall{}x,y:T.    (x  is  f*(y)  {}\mRightarrow{}  R[x;y])\})


By

---

Latex:
xxxAutoxxx

---

Home Index