---

Step * 1 1 2 2 1 of Lemma inj_into_ocmon


1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
19. x : |g|
20. x1 : |g|
⊢ ↑(x =b x1) ⇐⇒ ↑((x ≤b x1) ∧b (x1 ≤b x))
BY
{ (Thin (-3)
   THEN (Unfold `rels_iso` -4 THEN (RWO "-4" 0 THENA Auto))
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (Unfold `rels_iso` -3 THEN (RWO "-3" 0 THENA Auto))⋅) }

1
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. ∀x,y:|g|.  (↑(x =b y) ⇐⇒ ↑((f x) =b (f y)))
17. ∀x,y:|g|.  (↑(x ≤b y) ⇐⇒ ↑((f x) ≤b (f y)))
18. x : |g|
19. x1 : |g|
⊢ (f x) = (f x1) ∈ |h| ⇐⇒ (↑((f x) ≤b (f x1))) ∧ (↑((f x1) ≤b (f x)))

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  OCMon
3.  Assoc(|h|;*)
4.  Ident(|h|;*;e)
5.  Comm(|h|;*)
6.  UniformlyRefl(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  UniformlyTrans(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
8.  UniformlyAntiSym(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
9.  Connex(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
10.  Cancel(|h|;|h|;*)
11.  \mforall{}[z:|h|].  monot(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))
12.  f  :  |g|  {}\mrightarrow{}  |h|
13.  FunThru2op(|g|;|h|;*;*;f)
14.  (f  e)  =  e
15.  Inj(|g|;|h|;f)
16.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
17.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)
18.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
19.  x  :  |g|
20.  x1  :  |g|
\mvdash{}  \muparrow{}(x  =\msubb{}  x1)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}((x  \mleq{}\msubb{}  x1)  \mwedge{}\msubb{}  (x1  \mleq{}\msubb{}  x))


By

---

Latex:
(Thin  (-3)
  THEN  (Unfold  `rels\_iso`  -4  THEN  (RWO  "-4"  0  THENA  Auto))
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (Unfold  `rels\_iso`  -3  THEN  (RWO  "-3"  0  THENA  Auto))\mcdot{})

---

Home Index