---

Step * 1 1 of Lemma es-interface-set-subtype


1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
7. eo : EO+(Info)
8. e : E
9. #(X eo e) ≤ 1
⊢ X eo e ∈ bag({a:A| P[a]} )
BY
{ (All (Fold `eclass`)
   THEN (Decide ⌈↑e ∈b X⌉⋅ THENA Auto)
   THEN Try (((InstHyp [⌈eo⌉;⌈e⌉] (-5)⋅ THENA Complete (Auto)) THEN MoveToConcl (-1)))⋅
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (RepUR ``eclass-val in-eclass`` 0
         THEN All (Unfold `eclass`)
         THEN (GenConcl ⌈(X eo e) = z ∈ bag(A)⌉⋅ THEN Auto)⋅)⋅)⋅ }

1
1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
7. eo : EO+(Info)
8. e : E
9. z : bag(A)@i
10. (X eo e) = z ∈ bag(A)@i
11. #(z) ≤ 1@i
12. ↑(#(z) =z 1)@i
13. P[only(z)]@i
⊢ z ∈ bag({a:A| P[a]} )

2
1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
7. eo : EO+(Info)
8. e : E
9. z : bag(A)@i
10. (X eo e) = z ∈ bag(A)@i
11. #(z) ≤ 1@i
12. ↑(#(z) =z 1)@i
⊢ single-valued-bag(z;A)

3
1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
7. eo : EO+(Info)
8. e : E
9. z : bag(A)@i
10. (X eo e) = z ∈ bag(A)@i
11. #(z) ≤ 1@i
12. ↑(#(z) =z 1)@i
13. single-valued-bag(z;A)
⊢ 0 < #(z)

4
1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
7. eo : EO+(Info)
8. e : E
9. z : bag(A)@i
10. (X eo e) = z ∈ bag(A)@i
11. #(z) ≤ 1@i
12. ¬↑(#(z) =z 1)@i
⊢ z ∈ bag({a:A| P[a]} )

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  P  :  A  {}\mrightarrow{}  \mBbbP{}
4.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
5.  Singlevalued(X)
6.  \mforall{}es:EO+(Info).  \mforall{}e:E(X).    P[X(e)]
7.  eo  :  EO+(Info)
8.  e  :  E
9.  \#(X  eo  e)  \mleq{}  1
\mvdash{}  X  eo  e  \mmember{}  bag(\{a:A|  P[a]\}  )


By

(All  (Fold  `eclass`)
  THEN  (Decide  \mkleeneopen{}\muparrow{}e  \mmember{}\msubb{}  X\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((InstHyp  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-5)\mcdot{}  THENA  Complete  (Auto))  THEN  MoveToConcl  (-1)))\mcdot{}
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (RepUR  ``eclass-val  in-eclass``  0
              THEN  All  (Unfold  `eclass`)
              THEN  (GenConcl  \mkleeneopen{}(X  eo  e)  =  z\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{})\mcdot{})\mcdot{}

---

Home Index