---

Step * of Lemma recode-tuple_wf

∀[f:TypeRecoding]. (recode-tuple(f) ∈ TupleRecoding)
BY
{ (RepUR ``type-recoding tuple-recoding recode-tuple`` 0
   THEN (D 0 THENA Auto)
   THEN (MemCD THENA Auto)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN ((GenConclAtAddr [2;1]
          THEN (Thin (-1) THEN Thin (-2))
          THEN RepeatFor 3 (D -1)
          THEN Reduce 0
          THEN (GenConclAtAddr [2;1] THEN Thin (-1) THEN RepeatFor 3 (D -1) THEN Reduce 0 THEN OldAutoSplit)⋅)
   ORELSE Auto
   )) }

1
1. f : T:Type ⟶ (L:Type List × h:T ⟶ tuple-type(L) × {j:tuple-type(L) ⟶ T| ∀s:T. ((j (h s)) = s ∈ T)} )
2. u : Type
3. v : Type List
4. L' : Type List
5. h : tuple-type(v) ⟶ tuple-type(L')
6. v3 : tuple-type(L') ⟶ tuple-type(v)
7. ∀s:tuple-type(v). ((v3 (h s)) = s ∈ tuple-type(v))
8. L : Type List
9. h1 : u ⟶ tuple-type(L)
10. v6 : tuple-type(L) ⟶ u
11. ∀s:u. ((v6 (h1 s)) = s ∈ u)
12. null(v) = ff
⊢ <L @ L'
  , λx.let a,b = x 
       in append-tuple(||L||;||L'||;h1 a;h b)
  , if null(L') then λx.<v6 x, v3 ⋅> else λx.let a,b = split-tuple(x;||L||) in <v6 a, v3 b> fi > ∈ L':Type List
  × h:(u × tuple-type(v)) ⟶ tuple-type(L')
  × {j:tuple-type(L') ⟶ (u × tuple-type(v))| ∀s:u × tuple-type(v). ((j (h s)) = s ∈ (u × tuple-type(v)))} 

---

Latex:

---

Latex:
\mforall{}[f:TypeRecoding].  (recode-tuple(f)  \mmember{}  TupleRecoding)


By

---

Latex:
(RepUR  ``type-recoding  tuple-recoding  recode-tuple``  0
  THEN  (D  0  THENA  Auto)
  THEN  (MemCD  THENA  Auto)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  ((GenConclAtAddr  [2;1]
                THEN  (Thin  (-1)  THEN  Thin  (-2))
                THEN  RepeatFor  3  (D  -1)
                THEN  Reduce  0
                THEN  (GenConclAtAddr  [2;1]
                            THEN  Thin  (-1)
                            THEN  RepeatFor  3  (D  -1)
                            THEN  Reduce  0
                            THEN  OldAutoSplit)\mcdot{})
  ORELSE  Auto
  ))

---

Home Index