---

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


∀Info,A1,B1,A2,B2,C:Type. ∀X1:EClass(A1). ∀X2:EClass(A2). ∀b1:B1. ∀b2:B2. ∀acc1:B1 ─→ A1 ─→ B1. ∀acc2:B2 ─→ A2 ─→ B2.
∀F1:B1 ─→ C. ∀F2:B2 ─→ C.
  ((∀es:EO+(Info). ∀e:E.  (↑e ∈b X1 ⇐⇒ ↑e ∈b X2))
  ⇒ (F1[b1] = F2[b2] ∈ C)
  ⇒ (∀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)))))
  ⇒ ((F1[x] where x from es-interface-accum(acc1;b1;X1))
     = (F2[x] where x from es-interface-accum(acc2;b2;X2))
     ∈ EClass(C)))
BY
{ (Auto
   THEN BLemma `map-class_functionality`
   THEN Try (Complete (Auto))
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert es-interface-accum(acc1;b1;X1) ∈ EClass(B1) BY
               Auto)
   THEN (Assert es-interface-accum(acc2;b2;X2) ∈ EClass(B2) BY
               Auto)
   THEN Auto
   THEN (RWW "es-interface-accum-val is-interface-accum" 0
         THEN Auto
         THEN RWW "is-interface-accum" (-1)
         THEN Auto
         THEN Subst' ≤(X1)(e) = ≤(X2)(e) ∈ (E(X1) List) 0
         THEN Auto)⋅) }

1
.....equality..... 
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
⊢ ≤(X1)(e) = ≤(X2)(e) ∈ (E(X1) List)

2
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

---

Latex:

---

Latex:

\mforall{}Info,A1,B1,A2,B2,C:Type.  \mforall{}X1:EClass(A1).  \mforall{}X2:EClass(A2).  \mforall{}b1:B1.  \mforall{}b2:B2.  \mforall{}acc1:B1  {}\mrightarrow{}  A1  {}\mrightarrow{}  B1.
\mforall{}acc2:B2  {}\mrightarrow{}  A2  {}\mrightarrow{}  B2.  \mforall{}F1:B1  {}\mrightarrow{}  C.  \mforall{}F2:B2  {}\mrightarrow{}  C.
    ((\mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  X1  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  X2))
    {}\mRightarrow{}  (F1[b1]  =  F2[b2])
    {}\mRightarrow{}  (\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)])))))
    {}\mRightarrow{}  ((F1[x]  where  x  from  es-interface-accum(acc1;b1;X1))
          =  (F2[x]  where  x  from  es-interface-accum(acc2;b2;X2))))


By

---

Latex:
(Auto
  THEN  BLemma  `map-class\_functionality`
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (Assert  es-interface-accum(acc1;b1;X1)  \mmember{}  EClass(B1)  BY
                          Auto)
  THEN  (Assert  es-interface-accum(acc2;b2;X2)  \mmember{}  EClass(B2)  BY
                          Auto)
  THEN  Auto
  THEN  (RWW  "es-interface-accum-val  is-interface-accum"  0
              THEN  Auto
              THEN  RWW  "is-interface-accum"  (-1)
              THEN  Auto
              THEN  Subst'  \mleq{}(X1)(e)  =  \mleq{}(X2)(e)  0
              THEN  Auto)\mcdot{})

---

Home Index