---

Step * 1 1 of Lemma mon_for_when_unique

.....truecase..... 
1. s : DSet
2. g : IMonoid
3. f : |s| ⟶ |g|
4. b : |s| ⟶ 𝔹
5. u : |s|
6. ↑b[u]
7. a : |s|
8. as : |s| List
9. (↑distinct{s}(as))
⇒ (↑(u ∈b as))
⇒ (∀v:|s|. ((↑b[v]) ⇒ (↑(v ∈b as)) ⇒ (v = u ∈ |s|)))
⇒ ((For{g} x ∈ as. (when b[x]. f[x])) = f[u] ∈ |g|)
10. ↑(∀br(:|s|) ∈ as
         (¬b(r (=b) a)))
11. ↑distinct{s}(as)
12. (a = u ∈ |s|) ∨ (↑(u ∈b as))
13. ∀v:|s|. ((↑b[v]) ⇒ (↑((a (=b) v) ∨b(v ∈b as))) ⇒ (v = u ∈ |s|))
14. ↑b[a]
⊢ (f[a] * (For{g} x ∈ as. (when b[x]. f[x]))) = f[u] ∈ |g|
BY
{ D 12 }

1
1. s : DSet
2. g : IMonoid
3. f : |s| ⟶ |g|
4. b : |s| ⟶ 𝔹
5. u : |s|
6. ↑b[u]
7. a : |s|
8. as : |s| List
9. (↑distinct{s}(as))
⇒ (↑(u ∈b as))
⇒ (∀v:|s|. ((↑b[v]) ⇒ (↑(v ∈b as)) ⇒ (v = u ∈ |s|)))
⇒ ((For{g} x ∈ as. (when b[x]. f[x])) = f[u] ∈ |g|)
10. ↑(∀br(:|s|) ∈ as
         (¬b(r (=b) a)))
11. ↑distinct{s}(as)
12. a = u ∈ |s|
13. ∀v:|s|. ((↑b[v]) ⇒ (↑((a (=b) v) ∨b(v ∈b as))) ⇒ (v = u ∈ |s|))
14. ↑b[a]
⊢ (f[a] * (For{g} x ∈ as. (when b[x]. f[x]))) = f[u] ∈ |g|

2
1. s : DSet
2. g : IMonoid
3. f : |s| ⟶ |g|
4. b : |s| ⟶ 𝔹
5. u : |s|
6. ↑b[u]
7. a : |s|
8. as : |s| List
9. (↑distinct{s}(as))
⇒ (↑(u ∈b as))
⇒ (∀v:|s|. ((↑b[v]) ⇒ (↑(v ∈b as)) ⇒ (v = u ∈ |s|)))
⇒ ((For{g} x ∈ as. (when b[x]. f[x])) = f[u] ∈ |g|)
10. ↑(∀br(:|s|) ∈ as
         (¬b(r (=b) a)))
11. ↑distinct{s}(as)
12. ↑(u ∈b as)
13. ∀v:|s|. ((↑b[v]) ⇒ (↑((a (=b) v) ∨b(v ∈b as))) ⇒ (v = u ∈ |s|))
14. ↑b[a]
⊢ (f[a] * (For{g} x ∈ as. (when b[x]. f[x]))) = f[u] ∈ |g|

---

Latex:

---

Latex:
.....truecase..... 
1.  s  :  DSet
2.  g  :  IMonoid
3.  f  :  |s|  {}\mrightarrow{}  |g|
4.  b  :  |s|  {}\mrightarrow{}  \mBbbB{}
5.  u  :  |s|
6.  \muparrow{}b[u]
7.  a  :  |s|
8.  as  :  |s|  List
9.  (\muparrow{}distinct\{s\}(as))
{}\mRightarrow{}  (\muparrow{}(u  \mmember{}\msubb{}  as))
{}\mRightarrow{}  (\mforall{}v:|s|.  ((\muparrow{}b[v])  {}\mRightarrow{}  (\muparrow{}(v  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (v  =  u)))
{}\mRightarrow{}  ((For\{g\}  x  \mmember{}  as.  (when  b[x].  f[x]))  =  f[u])
10.  \muparrow{}(\mforall{}\msubb{}r(:|s|)  \mmember{}  as
                  (\mneg{}\msubb{}(r  (=\msubb{})  a)))
11.  \muparrow{}distinct\{s\}(as)
12.  (a  =  u)  \mvee{}  (\muparrow{}(u  \mmember{}\msubb{}  as))
13.  \mforall{}v:|s|.  ((\muparrow{}b[v])  {}\mRightarrow{}  (\muparrow{}((a  (=\msubb{})  v)  \mvee{}\msubb{}(v  \mmember{}\msubb{}  as)))  {}\mRightarrow{}  (v  =  u))
14.  \muparrow{}b[a]
\mvdash{}  (f[a]  *  (For\{g\}  x  \mmember{}  as.  (when  b[x].  f[x])))  =  f[u]


By

---

Latex:
D  12

---

Home Index