---

Step * 1 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
11. #(X es e) ≤ 1
12. #(Y es e) ≤ 1
⊢ (X es e) = (Y es e) ∈ bag(A)
BY
{ (AllHyps (\h. SimpleInstHyp ⌈es⌉ h THENA Auto THEN Thin h )⋅
   THEN AllHyps (\h. SimpleInstHyp ⌈e⌉ h THENA Auto THEN Thin h THEN MoveToConcl (-1))⋅
   THEN RepUR ``in-eclass eclass-val`` 0
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclAtAddr [1;1;1]
   THEN GenConclAtAddr [2;1;1;1]
   THEN All Thin) }

1
1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
⊢ (#(v) ≤ 1)
⇒ (#(v1) ≤ 1)
⇒ ((↑(#(v) =z 1)) ⇒ (↑(#(v1) =z 1)) ⇒ (only(v) = only(v1) ∈ A))
⇒ (↑(#(v) =z 1) ⇐⇒ ↑(#(v1) =z 1))
⇒ (v = v1 ∈ 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
11.  \#(X  es  e)  \mleq{}  1
12.  \#(Y  es  e)  \mleq{}  1
\mvdash{}  (X  es  e)  =  (Y  es  e)


By

(AllHyps  (\mbackslash{}h.  SimpleInstHyp  \mkleeneopen{}es\mkleeneclose{}  h  THENA  Auto  THEN  Thin  h  )\mcdot{}
  THEN  AllHyps  (\mbackslash{}h.  SimpleInstHyp  \mkleeneopen{}e\mkleeneclose{}  h  THENA  Auto  THEN  Thin  h  THEN  MoveToConcl  (-1))\mcdot{}
  THEN  RepUR  ``in-eclass  eclass-val``  0
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;1;1]
  THEN  GenConclAtAddr  [2;1;1;1]
  THEN  All  Thin)

---

Home Index