---

Step * of Lemma select-shorten-tuple

∀[n,m:ℕ]. ∀[L:Type List].  ∀[x:tuple-type(L)]. (shorten-tuple(x;n).m ~ x.n + m) supposing n + m < ||L||
BY
{ TACTIC:TACTIC:(InductionOnNat
                 THEN (RecUnfold `shorten-tuple` 0 THEN RecUnfold `select-tuple` 0)⋅
                 THEN Reduce 0
                 THEN (UnivCD THENA Auto)
                 THEN (((EqCD THENL [Complete (Auto); Id; Id]) THEN Auto)
                 ORELSE (Repeat (((SplitOnConclITE THENA Auto) THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))))
                         THEN DVar `L'
                         THEN All Reduce
                         THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
                         THEN (Subst' null(v) ~ ff 8 THENA (DVar `v' THEN All Reduce THEN Auto'))
                         THEN All Reduce
                         THEN DVar `x'
                         THEN All Reduce
                         THEN ((InstHyp [⌜m⌝;⌜v⌝;⌜x2⌝] 3⋅ THENA Auto')⋅
                               THEN NthHypSq (-1)
                               THEN EqCD
                               THEN Try ((EqCD THEN Complete (Auto')))
                               THEN RW (AddrC [2] (RecUnfoldC `select-tuple`)) 0
                               THEN RepeatFor 2 ((SplitOnConclITE THEN Auto)))⋅)
                 )) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[L:Type  List].
    \mforall{}[x:tuple-type(L)].  (shorten-tuple(x;n).m  \msim{}  x.n  +  m)  supposing  n  +  m  <  ||L||


By

---

Latex:
TACTIC:TACTIC:(InductionOnNat
                              THEN  (RecUnfold  `shorten-tuple`  0  THEN  RecUnfold  `select-tuple`  0)\mcdot{}
                              THEN  Reduce  0
                              THEN  (UnivCD  THENA  Auto)
                              THEN  (((EqCD  THENL  [Complete  (Auto);  Id;  Id])  THEN  Auto)
                              ORELSE  (Repeat  (((SplitOnConclITE  THENA  Auto)
                                                                THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
                                                                ))
                                              THEN  DVar  `L'
                                              THEN  All  Reduce
                                              THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
                                              THEN  (Subst'  null(v)  \msim{}  ff  8  THENA  (DVar  `v'  THEN  All  Reduce  THEN  Auto'))
                                              THEN  All  Reduce
                                              THEN  DVar  `x'
                                              THEN  All  Reduce
                                              THEN  ((InstHyp  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]  3\mcdot{}  THENA  Auto')\mcdot{}
                                                          THEN  NthHypSq  (-1)
                                                          THEN  EqCD
                                                          THEN  Try  ((EqCD  THEN  Complete  (Auto')))
                                                          THEN  RW  (AddrC  [2]  (RecUnfoldC  `select-tuple`))  0
                                                          THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto)))\mcdot{})
                              ))

---

Home Index