---

Step * 2 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
⊢ ∀x,y,a,b:T.  a before b ∈ [u / v] ⇒ a is f*(b) supposing x=f*(y) via [u / v]
BY
{ xxx(Auto THEN ((RWO "fun-path-cons" (-2)) THENM (RWO "cons_before" (-1))) THEN Auto)xxx }

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) ∧ (b ∈ v)) ∨ 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
\mvdash{}  \mforall{}x,y,a,b:T.    a  before  b  \mmember{}  [u  /  v]  {}\mRightarrow{}  a  is  f*(b)  supposing  x=f*(y)  via  [u  /  v]


By

---

Latex:
xxx(Auto  THEN  ((RWO  "fun-path-cons"  (-2))  THENM  (RWO  "cons\_before"  (-1)))  THEN  Auto)xxx

---

Home Index