---

Step * 1 1 of Lemma cnv-taba-property


1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.
    ((||xs|| ≤ ||ys||)
    ⇒ ((fst(rec-case(xs) of
             [] => <[], ys>
             x::xs' =>
              p.let a,ys = p 
                in let h,t = ys 
                   in <[<x, h> / a], t>))
       = zip(xs;rev(firstn(||xs||;ys)))
       ∈ ((A × B) List)))
BY
{ Assert ⌜∀xs:A List. ∀ys:B List.
            ((||xs|| ≤ ||ys||)
            ⇒ (rec-case(xs) of
                [] => <[], ys>
                x::xs' =>
                 p.let a,ys = p 
                   in let h,t = ys 
                      in <[<x, h> / a], t>
               = <zip(xs;rev(firstn(||xs||;ys))), nth_tl(||xs||;ys)>
               ∈ ((A × B) List × (B List))))⌝⋅ }

1
.....assertion..... 
1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.
    ((||xs|| ≤ ||ys||)
    ⇒ (rec-case(xs) of
        [] => <[], ys>
        x::xs' =>
         p.let a,ys = p 
           in let h,t = ys 
              in <[<x, h> / a], t>
       = <zip(xs;rev(firstn(||xs||;ys))), nth_tl(||xs||;ys)>
       ∈ ((A × B) List × (B List))))

2
1. A : Type
2. B : Type
3. ∀xs:A List. ∀ys:B List.
     ((||xs|| ≤ ||ys||)
     ⇒ (rec-case(xs) of
         [] => <[], ys>
         x::xs' =>
          p.let a,ys = p 
            in let h,t = ys 
               in <[<x, h> / a], t>
        = <zip(xs;rev(firstn(||xs||;ys))), nth_tl(||xs||;ys)>
        ∈ ((A × B) List × (B List))))
⊢ ∀xs:A List. ∀ys:B List.
    ((||xs|| ≤ ||ys||)
    ⇒ ((fst(rec-case(xs) of
             [] => <[], ys>
             x::xs' =>
              p.let a,ys = p 
                in let h,t = ys 
                   in <[<x, h> / a], t>))
       = zip(xs;rev(firstn(||xs||;ys)))
       ∈ ((A × B) List)))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}xs:A  List.  \mforall{}ys:B  List.
        ((||xs||  \mleq{}  ||ys||)
        {}\mRightarrow{}  ((fst(rec-case(xs)  of
                          []  =>  <[],  ys>
                          x::xs'  =>
                            p.let  a,ys  =  p 
                                in  let  h,t  =  ys 
                                      in  <[<x,  h>  /  a],  t>))
              =  zip(xs;rev(firstn(||xs||;ys)))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}xs:A  List.  \mforall{}ys:B  List.
                    ((||xs||  \mleq{}  ||ys||)
                    {}\mRightarrow{}  (rec-case(xs)  of
                            []  =>  <[],  ys>
                            x::xs'  =>
                              p.let  a,ys  =  p 
                                  in  let  h,t  =  ys 
                                        in  <[<x,  h>  /  a],  t>
                          =  <zip(xs;rev(firstn(||xs||;ys))),  nth\_tl(||xs||;ys)>))\mkleeneclose{}\mcdot{}

---

Home Index