---

Step * of Lemma fun-connected-tree

∀[T:Type]
  ∀f:T ⟶ T
    ∀x,y:T.  (x is f*(y) ⇒ (∀z:T. (x is f*(z) ⇒ (z is f*(y) ∨ y is f*(z))))) 
    supposing ∀a,b:T.  (((f a) = (f b) ∈ T) ⇒ (¬((f a) = a ∈ T)) ⇒ (¬((f b) = b ∈ T)) ⇒ (a = b ∈ T))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN BLemma `fun-connected-induction` THEN Auto) }

1
1. [T] : Type
2. f : T ⟶ T
3. ∀a,b:T.  (((f a) = (f b) ∈ T) ⇒ (¬((f a) = a ∈ T)) ⇒ (¬((f b) = b ∈ T)) ⇒ (a = b ∈ T))
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. y is f*(z)
10. ∀z@0:T. (y is f*(z@0) ⇒ (z@0 is f*(z) ∨ z is f*(z@0)))
11. z@0 : T
12. x is f*(z@0)
⊢ z@0 is f*(z) ∨ z is f*(z@0)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  T
        \mforall{}x,y:T.    (x  is  f*(y)  {}\mRightarrow{}  (\mforall{}z:T.  (x  is  f*(z)  {}\mRightarrow{}  (z  is  f*(y)  \mvee{}  y  is  f*(z))))) 
        supposing  \mforall{}a,b:T.    (((f  a)  =  (f  b))  {}\mRightarrow{}  (\mneg{}((f  a)  =  a))  {}\mRightarrow{}  (\mneg{}((f  b)  =  b))  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  BLemma  `fun-connected-induction`  THEN  Auto)

---

Home Index