---

Step * 1 of Lemma ocmon_properties


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)))
BY
{ ((RepUnfolds ``ulinorder uorder`` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  AbMon
2.  [\%1]  :  (UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))  \mwedge{}  (=\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x)))))
\mwedge{}  Cancel(|g|;|g|;*)
\mwedge{}  (\mforall{}[z:|g|].  monot(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w)))
\mvdash{}  SqStable(UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y)))


By

---

Latex:
((RepUnfolds  ``ulinorder  uorder``  0)  THEN  Auto)

---

Home Index