---

Step * 5 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)
4. Comm(omral_alg(g;r).car;omral_alg(g;r).plus)
5. IsAction(|r|;*;1;omral_alg(g;r).car;omral_alg(g;r).act)
⊢ IsBilinear(|r|;omral_alg(g;r).car;omral_alg(g;r).car;+r;omral_alg(g;r).plus;omral_alg(g;r).plus;omral_alg(g;r).act)
BY
{ Unfolds ``bilinear_p`` 0  
THEN RWH AbRedexC 0 THEN Force `5` (Reduce 0) 
THEN ((Backchain ``omral_action_plus_l omral_action_plus_r``) 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)
4.  Comm(omral\_alg(g;r).car;omral\_alg(g;r).plus)
5.  IsAction(|r|;*;1;omral\_alg(g;r).car;omral\_alg(g;r).act)
\mvdash{}  IsBilinear(|r|;omral\_alg(g;r).car;omral\_alg(g;r).car;+r;omral\_alg(g;r).plus;....plus;....act)


By

---

Latex:
Unfolds  ``bilinear\_p``  0   
THEN  RWH  AbRedexC  0  THEN  Force  `5`  (Reduce  0) 
THEN  ((Backchain  ``omral\_action\_plus\_l  omral\_action\_plus\_r``)  THENA  Auto)

---

Home Index