---

Step * 1 2 of Lemma fun-connected-tree


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=f*(z@0) via [u / v]
⊢ z@0 is f*(z) ∨ z is f*(z@0)
BY
{ xxx(((RWO "fun-path-cons" (-1)) THENM D -1 THENM Decide 0 < ||v||) THEN Auto THEN ThinTrivial THEN Auto)xxx }

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. u : T
13. v : T List
14. x = u ∈ T
15. z@0 = u ∈ T supposing ¬0 < ||v||
16. 0 < ||v||
17. u = (f hd(v)) ∈ T
18. ¬(u = hd(v) ∈ T)
19. hd(v)=f*(z@0) via v
⊢ z@0 is f*(z) ∨ z is f*(z@0)

2
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
⊢ z@0 is f*(z) ∨ z is f*(z@0)

---

Latex:

---

Latex:

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=f*(z@0)  via  [u  /  v]
\mvdash{}  z@0  is  f*(z)  \mvee{}  z  is  f*(z@0)


By

---

Latex:
xxx(((RWO  "fun-path-cons"  (-1))  THENM  D  -1  THENM  Decide  0  <  ||v||)
        THEN  Auto
        THEN  ThinTrivial
        THEN  Auto)xxx

---

Home Index