---

Step * 1 of Lemma es-interface-extensionality


1. Info : Type
2. A : Type
3. X : es:EO+(Info) ─→ e:E ─→ bag(A)
4. Y : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(Y)
6. Singlevalued(X)
7. ∀es:EO+(Info). ∀e:E.  (↑e ∈b X ⇐⇒ ↑e ∈b Y)
8. ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X) ⇒ (↑e ∈b Y) ⇒ (X(e) = Y(e) ∈ A))
9. es : EO+(Info)
10. e : E
⊢ (X es e) = (Y es e) ∈ bag(A)
BY
{ ((Assert #(X es e) ≤ 1 BY Auto) THEN (Assert #(Y es e) ≤ 1 BY Auto)) }

1
1. Info : Type
2. A : Type
3. X : es:EO+(Info) ─→ e:E ─→ bag(A)
4. Y : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(Y)
6. Singlevalued(X)
7. ∀es:EO+(Info). ∀e:E.  (↑e ∈b X ⇐⇒ ↑e ∈b Y)
8. ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X) ⇒ (↑e ∈b Y) ⇒ (X(e) = Y(e) ∈ A))
9. es : EO+(Info)
10. e : E
11. #(X es e) ≤ 1
12. #(Y es e) ≤ 1
⊢ (X es e) = (Y es e) ∈ bag(A)

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
4.  Y  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
5.  Singlevalued(Y)
6.  Singlevalued(X)
7.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  Y)
8.  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((\muparrow{}e  \mmember{}\msubb{}  X)  {}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  Y)  {}\mRightarrow{}  (X(e)  =  Y(e)))
9.  es  :  EO+(Info)
10.  e  :  E
\mvdash{}  (X  es  e)  =  (Y  es  e)


By

((Assert  \#(X  es  e)  \mleq{}  1  BY  Auto)  THEN  (Assert  \#(Y  es  e)  \mleq{}  1  BY  Auto))

---

Home Index