---

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

.....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)
BY
{ EAuto 1 }

---

Latex:

---

Latex:
.....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  {}\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{}  \mleq{}(X1)(e)  =  \mleq{}(X2)(e)


By

---

Latex:
EAuto  1

---

Home Index