---

Step * of Lemma sqequal-list_accum-list_ind

∀[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[b1;rec-case(as) of
                       [] => b2
                       h::t =>
                        r.J[h;r]] 
        supposing ∀x:Base. (F[x] ~ G[x;b2]) 
      supposing ∀a,b,c:Base.  (G[H[b;a];c] ~ G[b;J[a;c]]) 
    supposing ∀z:Base. strict1(λx.G[z;x]) 
  supposing strict1(λx.F[x])
BY
{ ((UnivCD THENA Auto)
   THEN SqequalSqle
   THEN Try ((InstLemma `sqle-list_accum-list_ind` [⌜F⌝;⌜G⌝;⌜H⌝;⌜J⌝;⌜as⌝;⌜b1⌝;⌜b2⌝]⋅
              THEN Try (Trivial)
              THEN RWO "-1 -5" 0
              THEN Auto))
   THEN InstLemma `sqle-list_ind-list_accum` [⌜F⌝;⌜G⌝;⌜H⌝;⌜J⌝;⌜as⌝;⌜b1⌝;⌜b2⌝]⋅
   THEN Try (Trivial)
   THEN RWO "-1 -5" 0
   THEN Auto) }

---

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[b1;rec-case(as)  of
                                              []  =>  b2
                                              h::t  =>
                                                r.J[h;r]] 
                supposing  \mforall{}x:Base.  (F[x]  \msim{}  G[x;b2]) 
            supposing  \mforall{}a,b,c:Base.    (G[H[b;a];c]  \msim{}  G[b;J[a;c]]) 
        supposing  \mforall{}z:Base.  strict1(\mlambda{}x.G[z;x]) 
    supposing  strict1(\mlambda{}x.F[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqequalSqle
  THEN  Try  ((InstLemma  `sqle-list\_accum-list\_ind`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}
                        THEN  Try  (Trivial)
                        THEN  RWO  "-1  -5"  0
                        THEN  Auto))
  THEN  InstLemma  `sqle-list\_ind-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  Try  (Trivial)
  THEN  RWO  "-1  -5"  0
  THEN  Auto)

---

Home Index