---

Step * of Lemma update-tuple_wf

∀[L:Type List]. ∀[n:ℕ]. ∀[x:tuple-type(L)].  ∀[y:L[n]]. (update-tuple(||L||;x;n;y) ∈ tuple-type(L)) supposing n < ||L||
BY
{ (InductionOnList THEN Reduce 0 THEN RecUnfold `update-tuple` 0 THEN All Reduce) }

1
∀[n:ℕ]. ∀[x:Unit].
  ∀[y:⊥]. (if (n =z 0) then <y, snd(x)> else <fst(x), update-tuple(-1;snd(x);n - 1;y)> fi  ∈ Unit) supposing n < 0

2
1. u : Type
2. v : Type List
3. ∀[n:ℕ]. ∀[x:tuple-type(v)].  ∀[y:v[n]]. (update-tuple(||v||;x;n;y) ∈ tuple-type(v)) supposing n < ||v||
⊢ ∀[n:ℕ]. ∀[x:if null(v) then u else u × tuple-type(v) fi ].
    ∀[y:[u / v][n]]
      (if (n =z 0)
       then if (||v|| + 1 =z 1) then y else <y, snd(x)> fi 
       else <fst(x), update-tuple((||v|| + 1) - 1;snd(x);n - 1;y)>
       fi  ∈ if null(v) then u else u × tuple-type(v) fi ) 
    supposing n < ||v|| + 1

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[n:\mBbbN{}].  \mforall{}[x:tuple-type(L)].
    \mforall{}[y:L[n]].  (update-tuple(||L||;x;n;y)  \mmember{}  tuple-type(L))  supposing  n  <  ||L||


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  RecUnfold  `update-tuple`  0  THEN  All  Reduce)

---

Home Index