---

Step * of Lemma ocmon_properties

∀g:OCMon
  (UniformLinorder(|g|;x,y.↑(x ≤b y))
  ∧ Cancel(|g|;|g|;*)
  ∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w)))
  ∧ IsEqFun(|g|;=b))
BY
{ ProvePropertiesLemma }

1
1. g : AbMon
2. [%1] : (UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)))
∧ Cancel(|g|;|g|;*)
∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w)))
⊢ SqStable(UniformLinorder(|g|;x,y.↑(x ≤b y)))

---

Latex:

---

Latex:
\mforall{}g:OCMon
    (UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
    \mwedge{}  Cancel(|g|;|g|;*)
    \mwedge{}  (\mforall{}[z:|g|].  monot(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w)))
    \mwedge{}  IsEqFun(|g|;=\msubb{}))


By

---

Latex:
ProvePropertiesLemma

---

Home Index