---

Step * 1 1 of Lemma inj_into_ocmon


1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
⊢ g ∈ OCMon
BY
{ MemTypeCD }

1
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
⊢ g ∈ AbMon

2
.....set predicate..... 
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
⊢ (UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)))
∧ Cancel(|g|;|g|;*)
∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w)))

3
.....wf..... 
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
18. g1 : AbMon
⊢ istype((UniformLinorder(|g1|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g1| ⟶ |g1| ⟶ 𝔹)))
∧ Cancel(|g1|;|g1|;*)
∧ (∀[z:|g1|]. monot(|g1|;x,y.↑(x ≤b y);λw.(z * w))))

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  OCMon
3.  Assoc(|h|;*)
4.  Ident(|h|;*;e)
5.  Comm(|h|;*)
6.  UniformlyRefl(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  UniformlyTrans(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
8.  UniformlyAntiSym(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
9.  Connex(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
10.  Cancel(|h|;|h|;*)
11.  \mforall{}[z:|h|].  monot(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))
12.  f  :  |g|  {}\mrightarrow{}  |h|
13.  FunThru2op(|g|;|h|;*;*;f)
14.  (f  e)  =  e
15.  Inj(|g|;|h|;f)
16.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
17.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)
\mvdash{}  g  \mmember{}  OCMon


By

---

Latex:
MemTypeCD

---

Home Index