---

Step * 1 1 2 1 of Lemma taba_wf


1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
6. u : A
7. v : A List
8. ∀ys:A List
     ((||v|| ≤ ||ys||)
     ⇒ (rec-case(v) 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)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
9. ys : A List
10. (||v|| + 1) ≤ ||ys||
11. rec-case(v) 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)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} 
12. v1 : {p:B × (A List)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} 
⊢ let a,ys = v1 
  in let h,t = ys 
     in <F[u;h;a], t> ∈ {p:B × (A List)| ((||v|| + 1) + ||snd(p)||) = ||ys|| ∈ ℤ} 
BY
{ (D (-1) THEN RepeatFor 2 (D -2) THEN All Reduce THEN skip{MaAuto}) }

1
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
6. u : A
7. v : A List
8. ∀ys:A List
     ((||v|| ≤ ||ys||)
     ⇒ (rec-case(v) 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)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
9. ys : A List
10. (||v|| + 1) ≤ ||ys||
11. rec-case(v) 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)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} 
12. v2 : B
13. (||v|| + 0) = ||ys|| ∈ ℤ
⊢ let h,t = [] 
  in <F[u;h;v2], t> ∈ {p:B × (A List)| ((||v|| + 1) + ||snd(p)||) = ||ys|| ∈ ℤ} 

2
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
6. u : A
7. v : A List
8. ∀ys:A List
     ((||v|| ≤ ||ys||)
     ⇒ (rec-case(v) 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)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} ))
9. ys : A List
10. (||v|| + 1) ≤ ||ys||
11. rec-case(v) 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)| (||v|| + ||snd(p)||) = ||ys|| ∈ ℤ} 
12. v2 : B
13. u1 : A
14. v4 : A List
15. (||v|| + ||v4|| + 1) = ||ys|| ∈ ℤ
⊢ <F[u;u1;v2], v4> ∈ {p:B × (A List)| ((||v|| + 1) + ||snd(p)||) = ||ys|| ∈ ℤ} 

---

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.  u  :  A
7.  v  :  A  List
8.  \mforall{}ys:A  List
          ((||v||  \mleq{}  ||ys||)
          {}\mRightarrow{}  (rec-case(v)  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)|  (||v||  +  ||snd(p)||)  =  ||ys||\}  ))
9.  ys  :  A  List
10.  (||v||  +  1)  \mleq{}  ||ys||
11.  rec-case(v)  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)|  (||v||  +  ||snd(p)||)  =  ||ys||\} 
12.  v1  :  \{p:B  \mtimes{}  (A  List)|  (||v||  +  ||snd(p)||)  =  ||ys||\} 
\mvdash{}  let  a,ys  =  v1 
    in  let  h,t  =  ys 
          in  <F[u;h;a],  t>  \mmember{}  \{p:B  \mtimes{}  (A  List)|  ((||v||  +  1)  +  ||snd(p)||)  =  ||ys||\} 


By

---

Latex:
(D  (-1)  THEN  RepeatFor  2  (D  -2)  THEN  All  Reduce  THEN  skip\{MaAuto\})

---

Home Index