---

Step * 1 1 1 2 of Lemma oal_grp_wf2

.....set predicate..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ AbMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))
⊢ (UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
  ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹)))
∧ Cancel(|oal_grp(s;g)|;|oal_grp(s;g)|;*)
∧ (∀[z:|oal_grp(s;g)|]. monot(|oal_grp(s;g)|;x,y.↑(x ≤b y);λw.(z * w)))
BY
{ TACTIC:D 0 }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ AbMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))
⊢ UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))

2
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ AbMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))
⊢ Cancel(|oal_grp(s;g)|;|oal_grp(s;g)|;*) ∧ (∀[z:|oal_grp(s;g)|]. monot(|oal_grp(s;g)|;x,y.↑(x ≤b y);λw.(z * w)))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  oal\_grp(s;g)  \mmember{}  AbGrp
4.  oal\_grp(s;g)  \mmember{}  AbMon
5.  UniformLinorder(|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))  \mwedge{}  (=\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x))))
\mvdash{}  (UniformLinorder(|oal\_grp(s;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(|oal\_grp(s;g)|;|oal\_grp(s;g)|;*)
\mwedge{}  (\mforall{}[z:|oal\_grp(s;g)|].  monot(|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w)))


By

---

Latex:
TACTIC:D  0

---

Home Index