---

Step * of Lemma select-update-tuple

∀[m,n:ℕ]. ∀[L:Type List].
  (∀[x:tuple-type(L)]. ∀[y:Top].  (update-tuple(||L||;x;n;y).m ~ if (n =z m) then y else x.m fi )) supposing 
     (m < ||L|| and 
     n < ||L||)
BY
{ (InductionOnNat
   THEN (RecUnfold `select-tuple` 0 THEN RecUnfold `update-tuple` 0)
   THEN Reduce 0
   THEN ((UnivCD THENA Auto)
         THEN RepeatFor 2 (OldAutoSplit)
         THEN Try (Complete (RepeatFor 2 (OldAutoSplit)))
         THEN DVar `L'
         THEN All Reduce
         THEN Try (Complete (Auto))
         THEN Subst' (||v|| + 1) - 1 ~ ||v|| 0
         THEN Auto
         THEN RWO "3" 0
         THEN Auto)⋅) }

1
.....wf..... 
1. m : ℤ
2. 0 < m
3. ∀[n:ℕ]. ∀[L:Type List].
     (∀[x:tuple-type(L)]. ∀[y:Top].
        (update-tuple(||L||;x;n;y).m - 1 ~ if (n =z m - 1) then y else x.m - 1 fi )) supposing 
        (m - 1 < ||L|| and 
        n < ||L||)
4. n : ℕ
5. u : Type
6. v : Type List
7. n < ||v|| + 1
8. m < ||v|| + 1
9. x : if null(v) then u else u × tuple-type(v) fi 
10. y : Top
11. ¬(m = 0 ∈ ℤ)
12. ¬(n = 0 ∈ ℤ)
⊢ snd(x) ∈ tuple-type(v)

---

Latex:

---

Latex:
\mforall{}[m,n:\mBbbN{}].  \mforall{}[L:Type  List].
    (\mforall{}[x:tuple-type(L)].  \mforall{}[y:Top].
          (update-tuple(||L||;x;n;y).m  \msim{}  if  (n  =\msubz{}  m)  then  y  else  x.m  fi  ))  supposing 
          (m  <  ||L||  and 
          n  <  ||L||)


By

---

Latex:
(InductionOnNat
  THEN  (RecUnfold  `select-tuple`  0  THEN  RecUnfold  `update-tuple`  0)
  THEN  Reduce  0
  THEN  ((UnivCD  THENA  Auto)
              THEN  RepeatFor  2  (OldAutoSplit)
              THEN  Try  (Complete  (RepeatFor  2  (OldAutoSplit)))
              THEN  DVar  `L'
              THEN  All  Reduce
              THEN  Try  (Complete  (Auto))
              THEN  Subst'  (||v||  +  1)  -  1  \msim{}  ||v||  0
              THEN  Auto
              THEN  RWO  "3"  0
              THEN  Auto)\mcdot{})

---

Home Index