---

Step * 3 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. IsGroup(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).zero;omral_alg(g;r).minus)
⊢ Comm(omral_alg(g;r).car;omral_alg(g;r).plus)
BY
{ % Need finer grading of strengths to avoid the 
  ugliness of the first 3 steps here %  
   
((ARepD ["basic"] 
THENM RWH AbRedexC 0 
THENM Force `2` (Reduce 0) 
THENM BLemma `omral_plus_comm`) THENA Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  IsGroup(omral\_alg(g;r).car;omral\_alg(g;r).plus;omral\_alg(g;r).zero;omral\_alg(g;r).minus)
\mvdash{}  Comm(omral\_alg(g;r).car;omral\_alg(g;r).plus)


By

---

Latex:
\%  Need  finer  grading  of  strengths  to  avoid  the 
    ugliness  of  the  first  3  steps  here  \%   
     
((ARepD  ["basic"] 
THENM  RWH  AbRedexC  0 
THENM  Force  `2`  (Reduce  0) 
THENM  BLemma  `omral\_plus\_comm`)  THENA  Auto)

---

Home Index