---

Step * 1 1 1 of Lemma oal_grp_wf1

.....subterm..... T:t
1:n
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
6. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
7. x : {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 
8. y : {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 
⊢ x =b y = x ≤≤b y ∧b y ≤≤b x
BY
{ (InstLemma `oal_le_is_order` [⌜s⌝;⌜g⌝]⋅ THEN Auto THEN D -1 THEN Auto)⋅ }

1
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
6. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
7. x : {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 
8. y : {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 
9. Refl(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
10. Trans(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
11. AntiSym(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
⊢ x =b y = x ≤≤b y ∧b y ≤≤b x

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  s  :  LOSet
2.  g  :  OGrp
3.  g  \mmember{}  AbDGrp
4.  g  \mmember{}  AbDMon
5.  UniformLinorder(|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
6.  UniformLinorder(|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  x  :  \{ps:(|s|  \mtimes{}  |g|)  List|  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))  \mwedge{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))\} 
8.  y  :  \{ps:(|s|  \mtimes{}  |g|)  List|  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))  \mwedge{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))\} 
\mvdash{}  x  =\msubb{}  y  =  x  \mleq{}\mleq{}\msubb{}  y  \mwedge{}\msubb{}  y  \mleq{}\mleq{}\msubb{}  x


By

---

Latex:
(InstLemma  `oal\_le\_is\_order`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  D  -1  THEN  Auto)\mcdot{}

---

Home Index