---

Step * 4 of Lemma oal_mon_wf


1. a : LOSet@i'
2. b : AbDMon@i'
⊢ Comm(|oal(a;b)|;λx,y. (x ++ y))
BY
{ % AbReduceIf needed to prevent oalist getting opened up.  
  Probably should fix projection computation funs to not 
  open oalist % 
 
Unfold `comm` 0  
THEN AbReduceIf (\e t.not is_term `set_car` t) 0 
THEN ((RepD THENM BLemma `oal_merge_comm`) THENA Auto) 
⋅ }

---

Latex:

---

Latex:

1.  a  :  LOSet@i'
2.  b  :  AbDMon@i'
\mvdash{}  Comm(|oal(a;b)|;\mlambda{}x,y.  (x  ++  y))


By

---

Latex:
\%  AbReduceIf  needed  to  prevent  oalist  getting  opened  up.   
    Probably  should  fix  projection  computation  funs  to  not 
    open  oalist  \% 
 
Unfold  `comm`  0   
THEN  AbReduceIf  (\mbackslash{}e  t.not  is\_term  `set\_car`  t)  0 
THEN  ((RepD  THENM  BLemma  `oal\_merge\_comm`)  THENA  Auto) 
\mcdot{}

---

Home Index