---

Step * 1 of Lemma cnv-taba-property


1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.  ((||xs|| ≤ ||ys||) ⇒ (cnv-taba(xs;ys) = zip(xs;rev(firstn(||xs||;ys))) ∈ ((A × B) List)))
BY
{ TACTIC:Unfold `cnv-taba` 0 }

1
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)))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}xs:A  List.  \mforall{}ys:B  List.    ((||xs||  \mleq{}  ||ys||)  {}\mRightarrow{}  (cnv-taba(xs;ys)  =  zip(xs;rev(firstn(||xs||;ys)))))


By

---

Latex:
TACTIC:Unfold  `cnv-taba`  0

---

Home Index