Step * 1 1 2 of Lemma bag-summation-linear-right


1. Type
2. Type
3. add R ⟶ R ⟶ R
4. mul R ⟶ R ⟶ R
5. zero R
6. T ⟶ R
7. T ⟶ R
8. minus R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. BiLinear(R;add;mul)
12. R
13. T
14. List
15. ∀x,y,z:R.
      ((z mul[add[x;y];a] ∈ R)
       (accumulate (with value and list item x):
           add mul[add[f[x];g[x]];a] c
          over list:
            v
          with starting value:
           z)
         mul[add[accumulate (with value and list item x):
                    add f[x] c
                   over list:
                     v
                   with starting value:
                    x);accumulate (with value and list item x):
                        add g[x] c
                       over list:
                         v
                       with starting value:
                        y)];a]
         ∈ R))
⊢ ∀x,y,z:R.
    ((z mul[add[x;y];a] ∈ R)
     (accumulate (with value and list item x):
         add mul[add[f[x];g[x]];a] c
        over list:
          v
        with starting value:
         add mul[add[f[u];g[u]];a] z)
       mul[add[accumulate (with value and list item x):
                  add f[x] c
                 over list:
                   v
                 with starting value:
                  add f[u] x);accumulate (with value and list item x):
                               add g[x] c
                              over list:
                                v
                              with starting value:
                               add g[u] y)];a]
       ∈ R))
BY
(Auto THEN BackThruSomeHyp) }

1
1. Type
2. Type
3. add R ⟶ R ⟶ R
4. mul R ⟶ R ⟶ R
5. zero R
6. T ⟶ R
7. T ⟶ R
8. minus R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. BiLinear(R;add;mul)
12. R
13. T
14. List
15. ∀x,y,z:R.
      ((z mul[add[x;y];a] ∈ R)
       (accumulate (with value and list item x):
           add mul[add[f[x];g[x]];a] c
          over list:
            v
          with starting value:
           z)
         mul[add[accumulate (with value and list item x):
                    add f[x] c
                   over list:
                     v
                   with starting value:
                    x);accumulate (with value and list item x):
                        add g[x] c
                       over list:
                         v
                       with starting value:
                        y)];a]
         ∈ R))
16. R
17. R
18. R
19. mul[add[x;y];a] ∈ R
⊢ (add mul[add[f[u];g[u]];a] z) mul[add[add f[u] x;add g[u] y];a] ∈ R


Latex:


Latex:

1.  T  :  Type
2.  R  :  Type
3.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
4.  mul  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
5.  zero  :  R
6.  f  :  T  {}\mrightarrow{}  R
7.  g  :  T  {}\mrightarrow{}  R
8.  minus  :  R  {}\mrightarrow{}  R
9.  IsGroup(R;add;zero;minus)
10.  Comm(R;add)
11.  BiLinear(R;add;mul)
12.  a  :  R
13.  u  :  T
14.  v  :  T  List
15.  \mforall{}x,y,z:R.
            ((z  =  mul[add[x;y];a])
            {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                      add  mul[add[f[x];g[x]];a]  c
                    over  list:
                        v
                    with  starting  value:
                      z)
                  =  mul[add[accumulate  (with  value  c  and  list  item  x):
                                        add  f[x]  c
                                      over  list:
                                          v
                                      with  starting  value:
                                        x);accumulate  (with  value  c  and  list  item  x):
                                                add  g[x]  c
                                              over  list:
                                                  v
                                              with  starting  value:
                                                y)];a]))
\mvdash{}  \mforall{}x,y,z:R.
        ((z  =  mul[add[x;y];a])
        {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                  add  mul[add[f[x];g[x]];a]  c
                over  list:
                    v
                with  starting  value:
                  add  mul[add[f[u];g[u]];a]  z)
              =  mul[add[accumulate  (with  value  c  and  list  item  x):
                                    add  f[x]  c
                                  over  list:
                                      v
                                  with  starting  value:
                                    add  f[u]  x);accumulate  (with  value  c  and  list  item  x):
                                                              add  g[x]  c
                                                            over  list:
                                                                v
                                                            with  starting  value:
                                                              add  g[u]  y)];a]))


By


Latex:
(Auto  THEN  BackThruSomeHyp)




Home Index