---

Step * of Lemma omral_plus_wf

∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.  (ps ++ qs ∈ (|g| × |r|) List)
BY
{ (((Unfold `omral_plus` 0 THEN RepD) THENA Auto) THEN Assert ⌜r↓+gp ∈ AbDMon⌝⋅) }

1
.....assertion..... 
1. g : OCMon
2. r : CDRng
3. ps : (|g| × |r|) List
4. qs : (|g| × |r|) List
⊢ r↓+gp ∈ AbDMon

2
1. g : OCMon
2. r : CDRng
3. ps : (|g| × |r|) List
4. qs : (|g| × |r|) List
5. r↓+gp ∈ AbDMon
⊢ ps ++ qs ∈ (|g| × |r|) List

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:(|g|  \mtimes{}  |r|)  List.    (ps  ++  qs  \mmember{}  (|g|  \mtimes{}  |r|)  List)


By

---

Latex:
(((Unfold  `omral\_plus`  0  THEN  RepD)  THENA  Auto)  THEN  Assert  \mkleeneopen{}r\mdownarrow{}+gp  \mmember{}  AbDMon\mkleeneclose{}\mcdot{})

---

Home Index