---

Step * 2 of Lemma sqle-list_ind-list_accum


1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. ∀z:Base. strict1(λx.G[z;x])
5. H : Base
6. J : Base
7. ∀a,b,c:Base.  (G[b;J[a;c]] ≤ G[H[b;a];c])
8. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. ∀x:Base. (G[x;b2] ≤ F[x])
12. ∀j:ℕ. ∀as,x:Base.
      (G[x;λlist_ind,L. eval v = L in
                        if v is a pair then let h,t = v 
                                            in J[h;list_ind t] otherwise if v = Ax then b2 otherwise ⊥^j 
           ⊥ 
           as] ≤ F[λlist_accum,y,L. eval v = L in
                                    if v is a pair then let h,t = v 
                                                        in list_accum H[y;h] t otherwise if v = Ax then y otherwise ⊥^j 
                   ⊥ 
                   x 
                   as])
⊢ G[b1;rec-case(as) of
       [] => b2
       h::t =>
        r.J[h;r]] ≤ F[accumulate (with value v and list item a):
                       H[v;a]
                      over list:
                        as
                      with starting value:
                       b1)]
BY
{ (RW (AddrC [1;3] UnfoldTopAbC) 0
   THEN OneFixpointLeast⋅
   THEN (InstHyp [⌜j⌝;⌜as⌝;⌜b1⌝] (-2)⋅ THENA Auto)
   THEN SqLeTrans (-1)
   THEN Try (Trivial)
   THEN SqLeCD
   THEN Try (SqLeCD)
   THEN All Thin
   THEN Unfold `list_accum` 0
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Base
2.  strict1(\mlambda{}x.F[x])
3.  G  :  Base
4.  \mforall{}z:Base.  strict1(\mlambda{}x.G[z;x])
5.  H  :  Base
6.  J  :  Base
7.  \mforall{}a,b,c:Base.    (G[b;J[a;c]]  \mleq{}  G[H[b;a];c])
8.  as  :  Base@i
9.  b1  :  Base@i
10.  b2  :  Base@i
11.  \mforall{}x:Base.  (G[x;b2]  \mleq{}  F[x])
12.  \mforall{}j:\mBbbN{}.  \mforall{}as,x:Base.
            (G[x;\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                              if  v  is  a  pair  then  let  h,t  =  v 
                                                                                      in  J[h;list$_{ind}$  t]  otherwise  if  v\000C  =  Ax  then  b2  otherwise  \mbot{}\^{}j 
                      \mbot{} 
                      as]  \mleq{}  F[\mlambda{}list$_{accum}$,y,L.  eval  v  =  L  in
                                                                      if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                              in  list$_{accum}$  H[y;h]  \000Ct
                                                                      otherwise  if  v  =  Ax  then  y  otherwise  \mbot{}\^{}j 
                                      \mbot{} 
                                      x 
                                      as])
\mvdash{}  G[b1;rec-case(as)  of
              []  =>  b2
              h::t  =>
                r.J[h;r]]  \mleq{}  F[accumulate  (with  value  v  and  list  item  a):
                                              H[v;a]
                                            over  list:
                                                as
                                            with  starting  value:
                                              b1)]


By

---

Latex:
(RW  (AddrC  [1;3]  UnfoldTopAbC)  0
  THEN  OneFixpointLeast\mcdot{}
  THEN  (InstHyp  [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  SqLeTrans  (-1)
  THEN  Try  (Trivial)
  THEN  SqLeCD
  THEN  Try  (SqLeCD)
  THEN  All  Thin
  THEN  Unfold  `list\_accum`  0
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  Auto)

---

Home Index