---

Step * 1 1 2 of Lemma cnv-taba_wf


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> ∈ {p:(A × B) List × (B List)| (||xs|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
⊢ ∀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>) ∈ (A × B) List))
BY
{ (RepeatFor 3 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  \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>  \mmember{}  \{p:(A  \mtimes{}  B)  List  \mtimes{}  (B  List)|  (||xs||  +  ||snd(p)||)  =  ||ys||\}  ))
\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>)  \mmember{}  (A  \mtimes{}  B)  List))


By

---

Latex:
(RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index