---

Step * 1 1 1 1 of Lemma oal_grp_wf1


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
BY
{ (UnfoldTopAb (-1)⋅
   THEN RepUR ``oal_le`` (-1)⋅
   THEN (SimpleInstHyp ⌜x⌝ (-1)⋅ THENA Auto)
   THEN (SimpleInstHyp ⌜y⌝ (-1)⋅ THENA 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. ∀ps,qs:{ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} .
      ((↑ps ≤≤b qs)
      ⇒ (↑qs ≤≤b ps)
      ⇒ (ps = qs ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} ))
12. ∀qs:{ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 
      ((↑x ≤≤b qs)
      ⇒ (↑qs ≤≤b x)
      ⇒ (x = qs ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} ))
13. (↑x ≤≤b y)
⇒ (↑y ≤≤b x)
⇒ (x = 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

---

Latex:

---

Latex:

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)))\} 
9.  Refl(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
10.  Trans(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
11.  AntiSym(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
\mvdash{}  x  =\msubb{}  y  =  x  \mleq{}\mleq{}\msubb{}  y  \mwedge{}\msubb{}  y  \mleq{}\mleq{}\msubb{}  x


By

---

Latex:
(UnfoldTopAb  (-1)\mcdot{}
  THEN  RepUR  ``oal\_le``  (-1)\mcdot{}
  THEN  (SimpleInstHyp  \mkleeneopen{}x\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (SimpleInstHyp  \mkleeneopen{}y\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index