---

Step * of Lemma sqequal-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]])))
      ∧ (∀a,r1,r2:Base.  ((G[r1] ≤ F[r2]) ⇒ (G[J[r1;a]] ≤ F[H[r2;a]]))) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])
BY
{ ((UnivCD THENA Auto)
   THEN SqequalSqle
   THEN SplitAndHyps
   THEN ((InstLemma `sqle-list_accum` [⌜F⌝;⌜G⌝;⌜H⌝;⌜J⌝;⌜as⌝;⌜b1⌝;⌜b2⌝]⋅
          THEN (Trivial ORELSE (HypSubst'  (-1) 0 THEN Complete (SqLeCD)))
          )
   ORELSE (InstLemma `sqle-list_accum` [⌜G⌝;⌜F⌝;⌜J⌝;⌜H⌝;⌜as⌝;⌜b2⌝;⌜b1⌝]⋅
           THEN (Trivial ORELSE (HypSubst'  (-1) 0 THEN Complete (SqLeCD)))
           )
   )) }

---

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)]  \msim{}  G[accumulate  (with  value  v  and  list  item  a):
                                          J[v;a]
                                        over  list:
                                            as
                                        with  starting  value:
                                          b2)] 
                supposing  F[b1]  \msim{}  G[b2] 
            supposing  (\mforall{}a,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[r1;a]]  \mleq{}  G[J[r2;a]])))
            \mwedge{}  (\mforall{}a,r1,r2:Base.    ((G[r1]  \mleq{}  F[r2])  {}\mRightarrow{}  (G[J[r1;a]]  \mleq{}  F[H[r2;a]]))) 
        supposing  strict1(\mlambda{}x.G[x]) 
    supposing  strict1(\mlambda{}x.F[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqequalSqle
  THEN  SplitAndHyps
  THEN  ((InstLemma  `sqle-list\_accum`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}
                THEN  (Trivial  ORELSE  (HypSubst'    (-1)  0  THEN  Complete  (SqLeCD)))
                )
  ORELSE  (InstLemma  `sqle-list\_accum`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}
                  THEN  (Trivial  ORELSE  (HypSubst'    (-1)  0  THEN  Complete  (SqLeCD)))
                  )
  ))

---

Home Index