---

Step * 1 2 of Lemma taba_wf


1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
6. ∀xs,ys:A List.
     ((||xs|| ≤ ||ys||)
     ⇒ (rec-case(xs) of
         [] => <init, ys>
         x::xs' =>
          p.let a,ys = p 
            in let h,t = ys 
               in <F[x;h;a], t> ∈ {p:B × (A List)| (||xs|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
⊢ fst(rec-case(xs) of
      [] => <init, xs>
      x::xs' =>
       p.let a,ys = p 
         in let h,t = ys 
            in <F[x;h;a], t>) ∈ B
BY
{ (InstHyp [⌜xs⌝;⌜xs⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  init  :  B
4.  F  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  xs  :  A  List
6.  \mforall{}xs,ys:A  List.
          ((||xs||  \mleq{}  ||ys||)
          {}\mRightarrow{}  (rec-case(xs)  of
                  []  =>  <init,  ys>
                  x::xs'  =>
                    p.let  a,ys  =  p 
                        in  let  h,t  =  ys 
                              in  <F[x;h;a],  t>  \mmember{}  \{p:B  \mtimes{}  (A  List)|  (||xs||  +  ||snd(p)||)  =  ||ys||\}  ))
\mvdash{}  fst(rec-case(xs)  of
            []  =>  <init,  xs>
            x::xs'  =>
              p.let  a,ys  =  p 
                  in  let  h,t  =  ys 
                        in  <F[x;h;a],  t>)  \mmember{}  B


By

---

Latex:
(InstHyp  [\mkleeneopen{}xs\mkleeneclose{};\mkleeneopen{}xs\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index