---

Step * 1 of Lemma filter-image-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 ─→ bag(C). ∀F2:B2 ─→ bag(C).
  ((∀es:EO+(Info). ∀e:E.  (↑e ∈b X1 ⇐⇒ ↑e ∈b X2))
  ⇒ (F1[b1] = F2[b2] ∈ bag(C))
  ⇒ (∀a:B1. ∀b:B2.
        (((F1 a) = (F2 b) ∈ bag(C))
        ⇒ (∀es:EO+(Info). ∀e:E.  ((↑e ∈b X1) ⇒ (↑e ∈b X1) ⇒ (F1[acc1 a X1(e)] = F2[acc2 b X2(e)] ∈ bag(C))))))
  ⇒ (F1[es-interface-accum(acc1;b1;X1)] = F2[es-interface-accum(acc2;b2;X2)] ∈ EClass(C)))
BY
{ Auto }

1
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 ─→ bag(C)@i
14. F2 : B2 ─→ bag(C)@i
15. ∀es:EO+(Info). ∀e:E.  (↑e ∈b X1 ⇐⇒ ↑e ∈b X2)@i'
16. F1[b1] = F2[b2] ∈ bag(C)@i
17. ∀a:B1. ∀b:B2.
      (((F1 a) = (F2 b) ∈ bag(C))
      ⇒ (∀es:EO+(Info). ∀e:E.  ((↑e ∈b X1) ⇒ (↑e ∈b X1) ⇒ (F1[acc1 a X1(e)] = F2[acc2 b X2(e)] ∈ bag(C)))))@i'
⊢ F1[es-interface-accum(acc1;b1;X1)] = F2[es-interface-accum(acc2;b2;X2)] ∈ EClass(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{}  bag(C).  \mforall{}F2:B2  {}\mrightarrow{}  bag(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[es-interface-accum(acc1;b1;X1)]  =  F2[es-interface-accum(acc2;b2;X2)]))


By

---

Latex:
Auto

---

Home Index