---

Step * 1 1 of Lemma filter-image-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 ─→ 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)
BY
{ (BLemma `filter-image_functionality`⋅ THENA 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'
⊢ ∀es:EO+(Info). ∀e:E.
    ((↑e ∈b es-interface-accum(acc1;b1;X1) ⇐⇒ ↑e ∈b es-interface-accum(acc2;b2;X2))
    ∧ ((↑e ∈b es-interface-accum(acc1;b1;X1))
      ⇒ (↑e ∈b es-interface-accum(acc2;b2;X2))
      ⇒ ((F1 es-interface-accum(acc1;b1;X1)(e)) = (F2 es-interface-accum(acc2;b2;X2)(e)) ∈ bag(C))))

---

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{}  bag(C)@i
14.  F2  :  B2  {}\mrightarrow{}  bag(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'
\mvdash{}  F1[es-interface-accum(acc1;b1;X1)]  =  F2[es-interface-accum(acc2;b2;X2)]


By

---

Latex:
(BLemma  `filter-image\_functionality`\mcdot{}  THENA  Auto)

---

Home Index