---

Step * 1 1 1 2 1 1 of Lemma cnv-taba-property


1. A : Type
2. B : Type
3. u : A
4. v : A List
5. ∀ys:B List
     ((||v|| ≤ ||ys||)
     ⇒ (rec-case(v) of
         [] => <[], ys>
         x::xs' =>
          p.let a,ys = p 
            in let h,t = ys 
               in <[<x, h> / a], t>
        = <zip(v;rev(firstn(||v||;ys))), nth_tl(||v||;ys)>
        ∈ ((A × B) List × (B List))))
6. ys : B List
7. (||v|| + 1) ≤ ||ys||
8. rec-case(v) of
   [] => <[], ys>
   x::xs' =>
    p.let a,ys = p 
      in let h,t = ys 
         in <[<x, h> / a], t>
= <zip(v;rev(firstn(||v||;ys))), nth_tl(||v||;ys)>
∈ ((A × B) List × (B List))
9. 0 < ||v|| + 1
⊢ let a,ys = rec-case(v) of
             [] => <[], ys>
             h@0::t =>
              r.let a,ys = r 
                in let h,t = ys 
                   in <[<h@0, h> / a], t> 
  in let h,t = ys 
     in <[<u, h> / a], t>
= <zip([u / v];rev(firstn(||v|| + 1;ys))), nth_tl((||v|| + 1) - 1;tl(ys))>
∈ ((A × B) List × (B List))
BY
{ (RecUnfold `firstn` 0 THEN OldAutoSplit THEN Auto')⋅ }

1
1. A : Type
2. B : Type
3. u : A
4. v : A List
5. ∀ys:B List
     ((||v|| ≤ ||ys||)
     ⇒ (rec-case(v) of
         [] => <[], ys>
         x::xs' =>
          p.let a,ys = p 
            in let h,t = ys 
               in <[<x, h> / a], t>
        = <zip(v;rev(firstn(||v||;ys))), nth_tl(||v||;ys)>
        ∈ ((A × B) List × (B List))))
6. ys : B List
7. (||v|| + 1) ≤ ||ys||
8. rec-case(v) of
   [] => <[], ys>
   x::xs' =>
    p.let a,ys = p 
      in let h,t = ys 
         in <[<x, h> / a], t>
= <zip(v;rev(firstn(||v||;ys))), nth_tl(||v||;ys)>
∈ ((A × B) List × (B List))
9. 0 < ||v|| + 1
10. 0 < ||v|| + 1
⊢ let a,ys = rec-case(v) of
             [] => <[], ys>
             h@0::t =>
              r.let a,ys = r 
                in let h,t = ys 
                   in <[<h@0, h> / a], t> 
  in let h,t = ys 
     in <[<u, h> / a], t>
= <zip([u / v];rev(case ys of [] => [] | a::as' => [a / firstn((||v|| + 1) - 1;as')] esac))
  , nth_tl((||v|| + 1) - 1;tl(ys))
  >
∈ ((A × B) List × (B List))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  u  :  A
4.  v  :  A  List
5.  \mforall{}ys:B  List
          ((||v||  \mleq{}  ||ys||)
          {}\mRightarrow{}  (rec-case(v)  of
                  []  =>  <[],  ys>
                  x::xs'  =>
                    p.let  a,ys  =  p 
                        in  let  h,t  =  ys 
                              in  <[<x,  h>  /  a],  t>
                =  <zip(v;rev(firstn(||v||;ys))),  nth\_tl(||v||;ys)>))
6.  ys  :  B  List
7.  (||v||  +  1)  \mleq{}  ||ys||
8.  rec-case(v)  of
      []  =>  <[],  ys>
      x::xs'  =>
        p.let  a,ys  =  p 
            in  let  h,t  =  ys 
                  in  <[<x,  h>  /  a],  t>
=  <zip(v;rev(firstn(||v||;ys))),  nth\_tl(||v||;ys)>
9.  0  <  ||v||  +  1
\mvdash{}  let  a,ys  =  rec-case(v)  of
                          []  =>  <[],  ys>
                          h@0::t  =>
                            r.let  a,ys  =  r 
                                in  let  h,t  =  ys 
                                      in  <[<h@0,  h>  /  a],  t> 
    in  let  h,t  =  ys 
          in  <[<u,  h>  /  a],  t>
=  <zip([u  /  v];rev(firstn(||v||  +  1;ys))),  nth\_tl((||v||  +  1)  -  1;tl(ys))>


By

---

Latex:
(RecUnfold  `firstn`  0  THEN  OldAutoSplit  THEN  Auto')\mcdot{}

---

Home Index