---

Step * 1 1 1 of Lemma es-interface-map-val


1. Info : Type
2. A : Type
3. es : EO+(Info)
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. f : A ─→ E(X) ─→ bag(Top)
6. e : E
7. #(X es e) = 1 ∈ ℤ
8. X es e ~ {only(X es e)}
9. x : A@i
10. ↑e ∈b X
⊢ Ax ∈ only(f x e) ~ only(f x e) supposing ↑(#(f x e) =z 1)
BY
{ (All (Fold `eclass`) THEN GenConcl ⌈(f x e) = B ∈ bag(Top)⌉⋅) }

1
.....wf..... 
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. X : EClass(A)
5. f : A ─→ E(X) ─→ bag(Top)
6. e : E
7. #(X es e) = 1 ∈ ℤ
8. X es e ~ {only(X es e)}
9. x : A@i
10. ↑e ∈b X
⊢ f x e ∈ bag(Top)

2
.....wf..... 
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. X : EClass(A)
5. f : A ─→ E(X) ─→ bag(Top)
6. e : E
7. #(X es e) = 1 ∈ ℤ
8. X es e ~ {only(X es e)}
9. x : A@i
10. ↑e ∈b X
⊢ bag(Top) ∈ Type

3
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. X : EClass(A)
5. f : A ─→ E(X) ─→ bag(Top)
6. e : E
7. #(X es e) = 1 ∈ ℤ
8. X es e ~ {only(X es e)}
9. x : A@i
10. ↑e ∈b X
11. B : bag(Top)@i
12. (f x e) = B ∈ bag(Top)@i
⊢ Ax ∈ only(B) ~ only(B) supposing ↑(#(B) =z 1)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  es  :  EO+(Info)
4.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
5.  f  :  A  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  bag(Top)
6.  e  :  E
7.  \#(X  es  e)  =  1
8.  X  es  e  \msim{}  \{only(X  es  e)\}
9.  x  :  A@i
10.  \muparrow{}e  \mmember{}\msubb{}  X
\mvdash{}  Ax  \mmember{}  only(f  x  e)  \msim{}  only(f  x  e)  supposing  \muparrow{}(\#(f  x  e)  =\msubz{}  1)


By

---

Latex:
(All  (Fold  `eclass`)  THEN  GenConcl  \mkleeneopen{}(f  x  e)  =  B\mkleeneclose{}\mcdot{})

---

Home Index