Step
*
1
2
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)))
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|
BY
{ (BHyp 9 THEN Auto{1,3}-1) }
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|) ∨ (↑(u ∈b as))
13. ∀v:|s|. ((↑b[v]) ⇒ (↑((a (=b) v) ∨b(v ∈b as))) ⇒ (v = u ∈ |s|))
14. ¬↑b[a]
⊢ ↑(u ∈b as)
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]
15. v : |s|
16. ↑b[v]
17. ↑(v ∈b as)
⊢ v = u ∈ |s|
3
.....wf.....
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]
15. v : |s|
16. ↑b[v]
⊢ istype(↑(v ∈b as))
4
.....wf.....
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]
15. v : |s|
⊢ istype(↑b[v])
5
.....wf.....
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]
⊢ istype(|s|)
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)))
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. \mneg{}\muparrow{}b[a]
\mvdash{} (For\{g\} x \mmember{} as. (when b[x]. f[x])) = f[u]
By
Latex:
(BHyp 9 THEN Auto\{1,3\}-1)
Home
Index