---

Step * 2 1 1 1 1 1 2 1 of Lemma fun-path-before


1. [T] : Type
2. f : T ⟶ T
3. u : T
4. u1 : T
5. v : T List
6. ∀x,y,a,b:T.  a before b ∈ [u1 / v] ⇒ a is f*(b) supposing x=f*(y) via [u1 / v]
7. x : T
8. y : T
9. a : T
10. b : T
11. f u1 is f*(u1)
12. x = u ∈ T
13. y = u ∈ T supposing ¬0 < ||v|| + 1
14. a = u ∈ T
15. (b ∈ [u1 / v])
16. 0 < ||v|| + 1
17. u = (f u1) ∈ T
18. ¬(u = u1 ∈ T)
19. u1=f*(y) via [u1 / v]
⊢ a is f*(b)
BY
{ xxx(((RWO "cons_member" (-5)) THENM D -5) THEN Auto)xxx }

1
1. [T] : Type
2. f : T ⟶ T
3. u : T
4. u1 : T
5. v : T List
6. ∀x,y,a,b:T.  a before b ∈ [u1 / v] ⇒ a is f*(b) supposing x=f*(y) via [u1 / v]
7. x : T
8. y : T
9. a : T
10. b : T
11. f u1 is f*(u1)
12. x = u ∈ T
13. y = u ∈ T supposing ¬0 < ||v|| + 1
14. a = u ∈ T
15. (b ∈ v)
16. 0 < ||v|| + 1
17. u = (f u1) ∈ T
18. ¬(u = u1 ∈ T)
19. u1=f*(y) via [u1 / v]
⊢ a is f*(b)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  u1  :  T
5.  v  :  T  List
6.  \mforall{}x,y,a,b:T.    a  before  b  \mmember{}  [u1  /  v]  {}\mRightarrow{}  a  is  f*(b)  supposing  x=f*(y)  via  [u1  /  v]
7.  x  :  T
8.  y  :  T
9.  a  :  T
10.  b  :  T
11.  f  u1  is  f*(u1)
12.  x  =  u
13.  y  =  u  supposing  \mneg{}0  <  ||v||  +  1
14.  a  =  u
15.  (b  \mmember{}  [u1  /  v])
16.  0  <  ||v||  +  1
17.  u  =  (f  u1)
18.  \mneg{}(u  =  u1)
19.  u1=f*(y)  via  [u1  /  v]
\mvdash{}  a  is  f*(b)


By

---

Latex:
xxx(((RWO  "cons\_member"  (-5))  THENM  D  -5)  THEN  Auto)xxx

---

Home Index