---

Step * 2 1 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
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
BY
{ xxx((((InstHyp [⌜i + 1⌝] (-3))⋅ THENM (RWO "select_cons_tl" (-1))) THENA Auto')
      THEN Auto
      THEN (NthHypEq (-2))
      THEN EqCD
      THEN Auto')xxx }

---

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
8.  0  <  (||v||  +  1)  +  1
9.  z  =  y
10.  x  =  [y;  [u  /  v]][((||v||  +  1)  +  1)  -  1]
11.  \mforall{}i:\mBbbN{}((||v||  +  1)  +  1)  -  1
            (([y;  [u  /  v]][i]  =  (f  [y;  [u  /  v]][i  +  1]))  \mwedge{}  (\mneg{}([y;  [u  /  v]][i]  =  [y;  [u  /  v]][i  +  1])))
12.  0  <  ||v||  +  1
13.  i  :  \mBbbN{}(||v||  +  1)  -  1
\mvdash{}  [u  /  v][i]  =  (f  [u  /  v][i  +  1])


By

---

Latex:
xxx((((InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-3))\mcdot{}  THENM  (RWO  "select\_cons\_tl"  (-1)))  THENA  Auto')
        THEN  Auto
        THEN  (NthHypEq  (-2))
        THEN  EqCD
        THEN  Auto')xxx

---

Home Index