---

Step * 2 of Lemma fun-path-cons


1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. x : T
6. y : T
7. z : T
⊢ uiff(z=f*(x) via [y; [u / v]];{(z = y ∈ T)
∧ ((y = (f hd([u / v])) ∈ T) ∧ (¬(y = hd([u / v]) ∈ T))) ∧ hd([u / v])=f*(x) via [u / v] supposing 0 < ||[u / v]||
∧ x = y ∈ T supposing ¬0 < ||[u / v]||})
BY
{ (RepUR ``guard fun-path last`` 0
   THEN Auto'
   THEN Try (((InstHyp [⌜0⌝] (-2)⋅ THENA Complete (Auto')) THEN All Reduce THEN Auto))) }

1
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. x : T
6. y : T
7. z : T
8. 0 < (||v|| + 1) + 1
9. z = y ∈ T
10. x = [y; [u / v]][((||v|| + 1) + 1) - 1] ∈ T
11. ∀i:ℕ((||v|| + 1) + 1) - 1
      (([y; [u / v]][i] = (f [y; [u / v]][i + 1]) ∈ T) ∧ (¬([y; [u / v]][i] = [y; [u / v]][i + 1] ∈ T)))
12. 0 < ||v|| + 1
13. i : ℕ(||v|| + 1) - 1
⊢ [u / v][i] = (f [u / v][i + 1]) ∈ T

2
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. x : T
6. y : T
7. z : T
8. 0 < (||v|| + 1) + 1
9. z = y ∈ T
10. x = [y; [u / v]][((||v|| + 1) + 1) - 1] ∈ T
11. ∀i:ℕ((||v|| + 1) + 1) - 1
      (([y; [u / v]][i] = (f [y; [u / v]][i + 1]) ∈ T) ∧ (¬([y; [u / v]][i] = [y; [u / v]][i + 1] ∈ T)))
12. 0 < ||v|| + 1
13. i : ℕ(||v|| + 1) - 1
⊢ ¬([u / v][i] = [u / v][i + 1] ∈ T)

3
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. x : T
6. y : T
7. z : T
8. z = y ∈ T
9. ((y = (f u) ∈ T) ∧ (¬(y = u ∈ T)))
   ∧ 0 < ||v|| + 1
   ∧ (u = u ∈ T)
   ∧ (x = [u / v][(||v|| + 1) - 1] ∈ T)
   ∧ (∀i:ℕ(||v|| + 1) - 1. (([u / v][i] = (f [u / v][i + 1]) ∈ T) ∧ (¬([u / v][i] = [u / v][i + 1] ∈ T)))) 
   supposing 0 < ||v|| + 1
10. x = y ∈ T supposing ¬0 < ||v|| + 1
11. i : ℕ((||v|| + 1) + 1) - 1
⊢ [y; [u / v]][i] = (f [y; [u / v]][i + 1]) ∈ T

4
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. x : T
6. y : T
7. z : T
8. z = y ∈ T
9. ((y = (f u) ∈ T) ∧ (¬(y = u ∈ T)))
   ∧ 0 < ||v|| + 1
   ∧ (u = u ∈ T)
   ∧ (x = [u / v][(||v|| + 1) - 1] ∈ T)
   ∧ (∀i:ℕ(||v|| + 1) - 1. (([u / v][i] = (f [u / v][i + 1]) ∈ T) ∧ (¬([u / v][i] = [u / v][i + 1] ∈ T)))) 
   supposing 0 < ||v|| + 1
10. x = y ∈ T supposing ¬0 < ||v|| + 1
11. i : ℕ((||v|| + 1) + 1) - 1
⊢ ¬([y; [u / v]][i] = [y; [u / v]][i + 1] ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  v  :  T  List
5.  x  :  T
6.  y  :  T
7.  z  :  T
\mvdash{}  uiff(z=f*(x)  via  [y;  [u  /  v]];\{(z  =  y)
\mwedge{}  ((y  =  (f  hd([u  /  v])))  \mwedge{}  (\mneg{}(y  =  hd([u  /  v]))))  \mwedge{}  hd([u  /  v])=f*(x)  via  [u  /  v] 
    supposing  0  <  ||[u  /  v]||
\mwedge{}  x  =  y  supposing  \mneg{}0  <  ||[u  /  v]||\})


By

---

Latex:
(RepUR  ``guard  fun-path  last``  0
  THEN  Auto'
  THEN  Try  (((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Complete  (Auto'))  THEN  All  Reduce  THEN  Auto)))

---

Home Index