---

Step * 2 1 of Lemma fun-path-before


1. [T] : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. ∀x,y,a,b:T.  a before b ∈ v ⇒ a is f*(b) supposing x=f*(y) via v
6. x : T
7. y : T
8. a : T
9. b : T
10. {(x = u ∈ T)
∧ ((u = (f hd(v)) ∈ T) ∧ (¬(u = hd(v) ∈ T))) ∧ hd(v)=f*(y) via v supposing 0 < ||v||
∧ y = u ∈ T supposing ¬0 < ||v||}
11. ((a = u ∈ T) ∧ (b ∈ v)) ∨ a before b ∈ v
⊢ a is f*(b)
BY
{ (D (-1) THEN Auto) }

1
1. [T] : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. ∀x,y,a,b:T.  a before b ∈ v ⇒ a is f*(b) supposing x=f*(y) via v
6. x : T
7. y : T
8. a : T
9. b : T
10. {(x = u ∈ T)
∧ ((u = (f hd(v)) ∈ T) ∧ (¬(u = hd(v) ∈ T))) ∧ hd(v)=f*(y) via v supposing 0 < ||v||
∧ y = u ∈ T supposing ¬0 < ||v||}
11. a = u ∈ T
12. (b ∈ v)
⊢ a is f*(b)

2
1. [T] : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. ∀x,y,a,b:T.  a before b ∈ v ⇒ a is f*(b) supposing x=f*(y) via v
6. x : T
7. y : T
8. a : T
9. b : T
10. {(x = u ∈ T)
∧ ((u = (f hd(v)) ∈ T) ∧ (¬(u = hd(v) ∈ T))) ∧ hd(v)=f*(y) via v supposing 0 < ||v||
∧ y = u ∈ T supposing ¬0 < ||v||}
11. a before b ∈ v
⊢ a is f*(b)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}x,y,a,b:T.    a  before  b  \mmember{}  v  {}\mRightarrow{}  a  is  f*(b)  supposing  x=f*(y)  via  v
6.  x  :  T
7.  y  :  T
8.  a  :  T
9.  b  :  T
10.  \{(x  =  u)
\mwedge{}  ((u  =  (f  hd(v)))  \mwedge{}  (\mneg{}(u  =  hd(v))))  \mwedge{}  hd(v)=f*(y)  via  v  supposing  0  <  ||v||
\mwedge{}  y  =  u  supposing  \mneg{}0  <  ||v||\}
11.  ((a  =  u)  \mwedge{}  (b  \mmember{}  v))  \mvee{}  a  before  b  \mmember{}  v
\mvdash{}  a  is  f*(b)


By

---

Latex:
(D  (-1)  THEN  Auto)

---

Home Index