---

Step * 1 2 2 1 1 of Lemma fun-connected-tree

.....assertion..... 
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. u : T
13. v : T List
14. x = u ∈ T
15. ¬0 < ||v||
16. z@0 = u ∈ T
⊢ x = f+(y)
BY
{ (HypSubst 7 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  \mforall{}a,b:T.    (((f  a)  =  (f  b))  {}\mRightarrow{}  (\mneg{}((f  a)  =  a))  {}\mRightarrow{}  (\mneg{}((f  b)  =  b))  {}\mRightarrow{}  (a  =  b))
4.  x  :  T
5.  y  :  T
6.  z  :  T
7.  x  =  (f  y)
8.  \mneg{}(x  =  y)
9.  y  is  f*(z)
10.  \mforall{}z@0:T.  (y  is  f*(z@0)  {}\mRightarrow{}  (z@0  is  f*(z)  \mvee{}  z  is  f*(z@0)))
11.  z@0  :  T
12.  u  :  T
13.  v  :  T  List
14.  x  =  u
15.  \mneg{}0  <  ||v||
16.  z@0  =  u
\mvdash{}  x  =  f+(y)


By

---

Latex:
(HypSubst  7  0  THEN  Auto)

---

Home Index