---

Step * 1 1 1 2 of Lemma cnv-taba_wf


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> ∈ {p:(A × B) List × (B List)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
⊢ ∀ys:B List
    (((||v|| + 1) ≤ ||ys||)
    ⇒ (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> ∈ {p:(A × B) List × (B List)| ((||v|| + 1) + ||snd(p)||) = ||ys|| ∈ ℤ} ))
BY
{ xxx((RepeatFor 2 (ParallelLast) THENA Auto') THEN GenConclAtAddr [2;1] THEN Thin (-1))xxx }

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> ∈ {p:(A × B) List × (B List)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
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> ∈ {p:(A × B) List × (B List)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} 
9. v1 : {p:(A × B) List × (B List)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} 
⊢ let a,ys = v1 
  in let h,t = ys 
     in <[<u, h> / a], t> ∈ {p:(A × B) List × (B List)| ((||v|| + 1) + ||snd(p)||) = ||ys|| ∈ ℤ} 

---

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>  \mmember{}  \{p:(A  \mtimes{}  B)  List  \mtimes{}  (B  List)|  (||v||  +  ||snd(p)||)  =  ||ys||\}  ))
\mvdash{}  \mforall{}ys:B  List
        (((||v||  +  1)  \mleq{}  ||ys||)
        {}\mRightarrow{}  (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>  \mmember{}  \{p:(A  \mtimes{}  B)  List  \mtimes{}  (B  List)|  ((||v||  +  1)  +  ||snd(p)||)  =  ||ys||\}  )\000C)


By

---

Latex:
xxx((RepeatFor  2  (ParallelLast)  THENA  Auto')  THEN  GenConclAtAddr  [2;1]  THEN  Thin  (-1))xxx

---

Home Index