---

Step * of Lemma strict-fun-connected-induction

∀[T:Type]
  ∀f:T ⟶ T
    ∀[R:T ⟶ T ⟶ ℙ]
      ((∀x,y,z:T.  (y is f*(z) ⇒ (R[y;z] ∨ (y = z ∈ T)) ⇒ R[x;z]) supposing ((¬(x = y ∈ T)) and (x = (f y) ∈ T)))
      ⇒ {∀x,y:T.  (x = f+(y) ⇒ R[x;y])})
BY
{ xxx(Unfold `guard` 0
      THEN RepeatFor 4 ((D 0 THENA Auto))
      THEN (Assert ∀x,y:T.  (x is f*(y) ⇒ (R[x;y] ∨ (x = y ∈ T))) BY
                  (BLemma `fun-connected-induction` THEN Auto)))xxx }

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

---

Latex:

---

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


By

---

Latex:
xxx(Unfold  `guard`  0
        THEN  RepeatFor  4  ((D  0  THENA  Auto))
        THEN  (Assert  \mforall{}x,y:T.    (x  is  f*(y)  {}\mRightarrow{}  (R[x;y]  \mvee{}  (x  =  y)))  BY
                                (BLemma  `fun-connected-induction`  THEN  Auto)))xxx

---

Home Index