---

Step * 2 3 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. 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
BY
{ ((D (-3) THEN Auto')⋅
   THEN CaseNat 0 `i'
   THEN (Reduce 0 THEN Auto)
   THEN RWO "select_cons_tl" (0)
   THEN Auto'
   THEN InstHyp [⌜i - 1⌝] (-2)⋅
   THEN Auto')⋅ }

---

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


By

---

Latex:
((D  (-3)  THEN  Auto')\mcdot{}
  THEN  CaseNat  0  `i'
  THEN  (Reduce  0  THEN  Auto)
  THEN  RWO  "select\_cons\_tl"  (0)
  THEN  Auto'
  THEN  InstHyp  [\mkleeneopen{}i  -  1\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto')\mcdot{}

---

Home Index