---

Step * of Lemma sqle-list_accum

∀[F:Base]
  ∀[G:Base]
    ∀[H,J:Base].
      ∀as,b1,b2:Base.
        F[accumulate (with value v and list item a):
           H[v;a]
          over list:
            as
          with starting value:
           b1)] ≤ G[accumulate (with value v and list item a):
                     J[v;a]
                    over list:
                      as
                    with starting value:
                     b2)] 
        supposing F[b1] ≤ G[b2] 
      supposing ∀a,r1,r2:Base.  ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]])) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])
BY
{ ((UnivCD THENA Auto)
   THEN Assert ⌜∀j:ℕ. ∀as,b1,b2:Base.
                  ((F[b1] ≤ G[b2])
                  ⇒ (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 
                        ⊥ 
                        b1 
                        as] ≤ G[λlist_accum,y,L. eval v = L in
                                                 if v is a pair then let h,t = v 
                                                                     in list_accum J[y;h] t
                                                 otherwise if v = Ax then y otherwise ⊥^j 
                                ⊥ 
                                b2 
                                as]))⌝⋅
   ) }

1
.....assertion..... 
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. strict1(λx.G[x])
5. H : Base
6. J : Base
7. ∀a,r1,r2:Base.  ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]]))
8. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. F[b1] ≤ G[b2]
⊢ ∀j:ℕ. ∀as,b1,b2:Base.
    ((F[b1] ≤ G[b2])
    ⇒ (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 
          ⊥ 
          b1 
          as] ≤ G[λlist_accum,y,L. eval v = L in
                                   if v is a pair then let h,t = v 
                                                       in list_accum J[y;h] t otherwise if v = Ax then y otherwise ⊥^j 
                  ⊥ 
                  b2 
                  as]))

2
1. F : Base
2. strict1(λx.F[x])
3. G : Base
4. strict1(λx.G[x])
5. H : Base
6. J : Base
7. ∀a,r1,r2:Base.  ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]]))
8. as : Base@i
9. b1 : Base@i
10. b2 : Base@i
11. F[b1] ≤ G[b2]
12. ∀j:ℕ. ∀as,b1,b2:Base.
      ((F[b1] ≤ G[b2])
      ⇒ (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 
            ⊥ 
            b1 
            as] ≤ G[λlist_accum,y,L. eval v = L in
                                     if v is a pair then let h,t = v 
                                                         in list_accum J[y;h] t otherwise if v = Ax then y otherwise ⊥^j\000C 
                    ⊥ 
                    b2 
                    as]))
⊢ F[accumulate (with value v and list item a):
     H[v;a]
    over list:
      as
    with starting value:
     b1)] ≤ G[accumulate (with value v and list item a):
               J[v;a]
              over list:
                as
              with starting value:
               b2)]

---

Latex:

---

Latex:
\mforall{}[F:Base]
    \mforall{}[G:Base]
        \mforall{}[H,J:Base].
            \mforall{}as,b1,b2:Base.
                F[accumulate  (with  value  v  and  list  item  a):
                      H[v;a]
                    over  list:
                        as
                    with  starting  value:
                      b1)]  \mleq{}  G[accumulate  (with  value  v  and  list  item  a):
                                          J[v;a]
                                        over  list:
                                            as
                                        with  starting  value:
                                          b2)] 
                supposing  F[b1]  \mleq{}  G[b2] 
            supposing  \mforall{}a,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[r1;a]]  \mleq{}  G[J[r2;a]])) 
        supposing  strict1(\mlambda{}x.G[x]) 
    supposing  strict1(\mlambda{}x.F[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}.  \mforall{}as,b1,b2:Base.
                                ((F[b1]  \mleq{}  G[b2])
                                {}\mRightarrow{}  (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;\000Ch]  t
                                                                            otherwise  if  v  =  Ax  then  y  otherwise  \mbot{}\^{}j 
                                            \mbot{} 
                                            b1 
                                            as]  \mleq{}  G[\mlambda{}list$_{accum}$,y,L.  eval  v  =  L  in
                                                                                            if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                                    in  list$_{accum}\mbackslash{}f\000Cf24  J[y;h]  t
                                                                                            otherwise  if  v  =  Ax  then  y  otherwise  \mbot{}\^{}j 
                                                            \mbot{} 
                                                            b2 
                                                            as]))\mkleeneclose{}\mcdot{}
  )

---

Home Index