---

Step * 1 of Lemma hgrp_of_ocgrp_wf2


1. g : OGrp
⊢ ∃h:OCMon
   ∃f:|(g↓hgrp)| ⟶ |h|
    (IsMonHomInj(g↓hgrp;h;f)
    ∧ RelsIso(|(g↓hgrp)|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
    ∧ RelsIso(|(g↓hgrp)|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))
BY
{ ((Reduce 0 
THENM InstConcl [g;λx.x] 
THENM GenRepD) THENA Auto) }

1
1. g : OGrp
⊢ IsMonHomInj(g↓hgrp;g;λx.x)

2
1. g : OGrp
⊢ RelsIso(|g|+;|g|;x,y.↑(x =b y);x,y.↑(x =b y);λx.x)

3
1. g : OGrp
⊢ RelsIso(|g|+;|g|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);λx.x)

---

Latex:

---

Latex:

1.  g  :  OGrp
\mvdash{}  \mexists{}h:OCMon
      \mexists{}f:|(g\mdownarrow{}hgrp)|  {}\mrightarrow{}  |h|
        (IsMonHomInj(g\mdownarrow{}hgrp;h;f)
        \mwedge{}  RelsIso(|(g\mdownarrow{}hgrp)|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
        \mwedge{}  RelsIso(|(g\mdownarrow{}hgrp)|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f))


By

---

Latex:
((Reduce  0 
THENM  InstConcl  [g;\mlambda{}x.x] 
THENM  GenRepD)  THENA  Auto)

---

Home Index