---

Step * 1 of Lemma int_add_grp_wf2


<ℤ+> ∈ OCMon
BY
{ MemTypeCD THENW Auto }

1
<ℤ+> ∈ AbMon

2
.....set predicate..... 
(UniformLinorder(|<ℤ+>|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|<ℤ+>| ⟶ |<ℤ+>| ⟶ 𝔹)))
∧ Cancel(|<ℤ+>|;|<ℤ+>|;*)
∧ (∀[z:|<ℤ+>|]. monot(|<ℤ+>|;x,y.↑(x ≤b y);λw.(z * w)))

---

Latex:

---

Latex:

<\mBbbZ{}+>  \mmember{}  OCMon


By

---

Latex:
MemTypeCD  THENW  Auto

---

Home Index