---

Step * of Lemma fst-recode-tuple

∀[T:Type]. ∀[f:T ⟶ (T List × Top × Top)]. ∀[L:T List].
  ((fst((recode-tuple(f) L))) = reduce(λT,X. ((fst((f T))) @ X);[];L) ∈ (T List))
BY
{ (Unfold `recode-tuple` 0
   THEN InductionOnList
   THEN All Reduce
   THEN Try (Complete (Auto))
   THEN (GenConcl ⌜(f u) = p ∈ (T List × Top × Top)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN (GenConclAtAddrType ⌜T List × Top × Top⌝ [2;1;1]⋅
         THENA (Auto THEN GenConclAtAddr [2;1] THEN RepeatFor 2 ((D -2 THEN Reduce 0)) THEN Auto)
         )
   THEN (RepeatFor 2 (D -2) THEN Reduce 0 THEN AutoSplit THEN DVar `v' THEN Reduce 0 THEN RWW "append-nil" 0 THEN Auto)
   ⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  (T  List  \mtimes{}  Top  \mtimes{}  Top)].  \mforall{}[L:T  List].
    ((fst((recode-tuple(f)  L)))  =  reduce(\mlambda{}T,X.  ((fst((f  T)))  @  X);[];L))


By

---

Latex:
(Unfold  `recode-tuple`  0
  THEN  InductionOnList
  THEN  All  Reduce
  THEN  Try  (Complete  (Auto))
  THEN  (GenConcl  \mkleeneopen{}(f  u)  =  p\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  (GenConclAtAddrType  \mkleeneopen{}T  List  \mtimes{}  Top  \mtimes{}  Top\mkleeneclose{}  [2;1;1]\mcdot{}
              THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  RepeatFor  2  ((D  -2  THEN  Reduce  0))  THEN  Auto)
              )
  THEN  (RepeatFor  2  (D  -2)
              THEN  Reduce  0
              THEN  AutoSplit
              THEN  DVar  `v'
              THEN  Reduce  0
              THEN  RWW  "append-nil"  0
              THEN  Auto)\mcdot{})

---

Home Index