---

Step * 1 2 of Lemma map-interface-accum-equal


1. Info : Type@i'
2. A1 : Type@i'
3. B1 : Type@i'
4. A2 : Type@i'
5. B2 : Type@i'
6. C : Type@i'
7. X1 : EClass(A1)@i'
8. X2 : EClass(A2)@i'
9. b1 : B1@i
10. b2 : B2@i
11. acc1 : B1 ─→ A1 ─→ B1@i
12. acc2 : B2 ─→ A2 ─→ B2@i
13. F1 : B1 ─→ C@i
14. F2 : B2 ─→ C@i
15. ∀es:EO+(Info). ∀e:E.  (↑e ∈b X1 ⇐⇒ ↑e ∈b X2)@i'
16. F1[b1] = F2[b2] ∈ C@i
17. ∀a:B1. ∀b:B2.
      (((F1 a) = (F2 b) ∈ C)
      ⇒ (∀es:EO+(Info). ∀e:E.  ((↑e ∈b X1) ⇒ (↑e ∈b X1) ⇒ (F1[acc1 a X1(e)] = F2[acc2 b X2(e)] ∈ C))))@i'
18. es : EO+(Info)@i'
19. e : E@i
20. es-interface-accum(acc1;b1;X1) ∈ EClass(B1)
21. es-interface-accum(acc2;b2;X2) ∈ EClass(B2)
22. ↑e ∈b es-interface-accum(acc1;b1;X1)@i
23. ↑e ∈b X2@i
⊢ F1[accumulate (with value b and list item e):
      acc1 b X1(e)
     over list:
       ≤(X2)(e)
     with starting value:
      b1)]
= F2[accumulate (with value b and list item e):
      acc2 b X2(e)
     over list:
       ≤(X2)(e)
     with starting value:
      b2)]
∈ C
BY
{ (InstLemma `list_accum_equality` [⌈E(X1)⌉;⌈B1⌉;⌈B2⌉;⌈C⌉;⌈λ2b e.acc1 b X1(e)⌉;⌈λ2b e.acc2 b X2(e)⌉;⌈F1⌉;⌈F2⌉;⌈≤(X2)(e)⌉
   ;⌈b1⌉;⌈b2⌉]⋅
   THEN Auto
   THEN Try ((D (-1) THEN MemTypeCD THEN Auto)))⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type@i'
2.  A1  :  Type@i'
3.  B1  :  Type@i'
4.  A2  :  Type@i'
5.  B2  :  Type@i'
6.  C  :  Type@i'
7.  X1  :  EClass(A1)@i'
8.  X2  :  EClass(A2)@i'
9.  b1  :  B1@i
10.  b2  :  B2@i
11.  acc1  :  B1  {}\mrightarrow{}  A1  {}\mrightarrow{}  B1@i
12.  acc2  :  B2  {}\mrightarrow{}  A2  {}\mrightarrow{}  B2@i
13.  F1  :  B1  {}\mrightarrow{}  C@i
14.  F2  :  B2  {}\mrightarrow{}  C@i
15.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  X1  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  X2)@i'
16.  F1[b1]  =  F2[b2]@i
17.  \mforall{}a:B1.  \mforall{}b:B2.
            (((F1  a)  =  (F2  b))
            {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}e:E.
                        ((\muparrow{}e  \mmember{}\msubb{}  X1)  {}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  X1)  {}\mRightarrow{}  (F1[acc1  a  X1(e)]  =  F2[acc2  b  X2(e)]))))@i'
18.  es  :  EO+(Info)@i'
19.  e  :  E@i
20.  es-interface-accum(acc1;b1;X1)  \mmember{}  EClass(B1)
21.  es-interface-accum(acc2;b2;X2)  \mmember{}  EClass(B2)
22.  \muparrow{}e  \mmember{}\msubb{}  es-interface-accum(acc1;b1;X1)@i
23.  \muparrow{}e  \mmember{}\msubb{}  X2@i
\mvdash{}  F1[accumulate  (with  value  b  and  list  item  e):
            acc1  b  X1(e)
          over  list:
              \mleq{}(X2)(e)
          with  starting  value:
            b1)]
=  F2[accumulate  (with  value  b  and  list  item  e):
            acc2  b  X2(e)
          over  list:
              \mleq{}(X2)(e)
          with  starting  value:
            b2)]


By

---

Latex:
(InstLemma  `list\_accum\_equality`  [\mkleeneopen{}E(X1)\mkleeneclose{};\mkleeneopen{}B1\mkleeneclose{};\mkleeneopen{}B2\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}b  e.acc1  b  X1(e)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}b  e.acc2  b  X2(e)\mkleeneclose{};
  \mkleeneopen{}F1\mkleeneclose{};\mkleeneopen{}F2\mkleeneclose{};\mkleeneopen{}\mleq{}(X2)(e)\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((D  (-1)  THEN  MemTypeCD  THEN  Auto)))\mcdot{}

---

Home Index