---

Step * 1 of Lemma mon_for_when_unique


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))) ∧b distinct{s}(as))
11. ↑((a (=b) u) ∨b(u ∈b as))
12. ∀v:|s|. ((↑b[v]) ⇒ (↑((a (=b) v) ∨b(v ∈b as))) ⇒ (v = u ∈ |s|))
⊢ ((when b[a]. f[a]) * (For{g} x ∈ as. (when b[x]. f[x]))) = f[u] ∈ |g|
BY
{ (((((OnMHyps [10; 11] (RW bool_to_propC) THENM D 10) THENM RWN 1 (UnfoldTopC `mon_when`) 0) THENM SplitOnConclITE)
   THENM RW MonNormC 0
   )
   THENA Auto
   ) }

1
.....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|

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. (a = u ∈ |s|) ∨ (↑(u ∈b as))
13. ∀v:|s|. ((↑b[v]) ⇒ (↑((a (=b) v) ∨b(v ∈b as))) ⇒ (v = u ∈ |s|))
14. ¬↑b[a]
⊢ (For{g} x ∈ as. (when b[x]. f[x])) = f[u] ∈ |g|

---

Latex:

---

Latex:

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)))  \mwedge{}\msubb{}  distinct\{s\}(as))
11.  \muparrow{}((a  (=\msubb{})  u)  \mvee{}\msubb{}(u  \mmember{}\msubb{}  as))
12.  \mforall{}v:|s|.  ((\muparrow{}b[v])  {}\mRightarrow{}  (\muparrow{}((a  (=\msubb{})  v)  \mvee{}\msubb{}(v  \mmember{}\msubb{}  as)))  {}\mRightarrow{}  (v  =  u))
\mvdash{}  ((when  b[a].  f[a])  *  (For\{g\}  x  \mmember{}  as.  (when  b[x].  f[x])))  =  f[u]


By

---

Latex:
(((((OnMHyps  [10;  11]  (RW  bool\_to\_propC)  THENM  D  10)  THENM  RWN  1  (UnfoldTopC  `mon\_when`)  0)
    THENM  SplitOnConclITE
    )
  THENM  RW  MonNormC  0
  )
  THENA  Auto
  )

---

Home Index