---

Step * 1 of Lemma recode-tuple_wf


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)))} 
BY
{ xxx(Decide 0 < ||L'|| THENA Auto)xxx }

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
13. 0 < ||L'||
⊢ <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)))} 

2
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
13. ¬0 < ||L'||
⊢ <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:

1.  f  :  T:Type  {}\mrightarrow{}  (L:Type  List
                                  \mtimes{}  h:T  {}\mrightarrow{}  tuple-type(L)
                                  \mtimes{}  \{j:tuple-type(L)  {}\mrightarrow{}  T|  \mforall{}s:T.  ((j  (h  s))  =  s)\}  )
2.  u  :  Type
3.  v  :  Type  List
4.  L'  :  Type  List
5.  h  :  tuple-type(v)  {}\mrightarrow{}  tuple-type(L')
6.  v3  :  tuple-type(L')  {}\mrightarrow{}  tuple-type(v)
7.  \mforall{}s:tuple-type(v).  ((v3  (h  s))  =  s)
8.  L  :  Type  List
9.  h1  :  u  {}\mrightarrow{}  tuple-type(L)
10.  v6  :  tuple-type(L)  {}\mrightarrow{}  u
11.  \mforall{}s:u.  ((v6  (h1  s))  =  s)
12.  null(v)  =  ff
\mvdash{}  <L  @  L'
    ,  \mlambda{}x.let  a,b  =  x 
              in  append-tuple(||L||;||L'||;h1  a;h  b)
    ,  if  null(L')  then  \mlambda{}x.<v6  x,  v3  \mcdot{}>  else  \mlambda{}x.let  a,b  =  split-tuple(x;||L||)  in  <v6  a,  v3  b>  fi  >
    \mmember{}  L':Type  List
    \mtimes{}  h:(u  \mtimes{}  tuple-type(v))  {}\mrightarrow{}  tuple-type(L')
    \mtimes{}  \{j:tuple-type(L')  {}\mrightarrow{}  (u  \mtimes{}  tuple-type(v))|  \mforall{}s:u  \mtimes{}  tuple-type(v).  ((j  (h  s))  =  s)\} 


By

---

Latex:
xxx(Decide  0  <  ||L'||  THENA  Auto)xxx

---

Home Index