---

Step * 1 1 1 1 1 4 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. ¬↑y ≤≤b x
10. ¬↑x ≤≤b y
11. Refl(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
12. Trans(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
13. ∀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)))} ))
14. ∀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)))} ))
15. False
⇒ False
⇒ (x = y ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
⊢ x =b y = ff
BY
{ ((Assert g ∈ DMon BY
          (BLemma `omon_inc` THEN Auto))
   THEN AutoBoolCase ⌜x =b y⌝⋅
   THEN Auto
   THEN Assert ⌜↑x ≤≤b y⌝⋅
   THEN Auto)⋅ }

1
.....assertion..... 
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. ¬↑y ≤≤b x
10. ¬↑x ≤≤b y
11. Refl(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
12. Trans(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
13. ∀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)))} ))
14. ∀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)))} ))
15. False
⇒ False
⇒ (x = y ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
16. g ∈ DMon
17. ↑(x =b y)
⊢ ↑x ≤≤b y

---

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.  \mneg{}\muparrow{}y  \mleq{}\mleq{}\msubb{}  x
10.  \mneg{}\muparrow{}x  \mleq{}\mleq{}\msubb{}  y
11.  Refl(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
12.  Trans(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
13.  \mforall{}ps,qs:\{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)))\}  .
            ((\muparrow{}ps  \mleq{}\mleq{}\msubb{}  qs)  {}\mRightarrow{}  (\muparrow{}qs  \mleq{}\mleq{}\msubb{}  ps)  {}\mRightarrow{}  (ps  =  qs))
14.  \mforall{}qs:\{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)))\} 
            ((\muparrow{}x  \mleq{}\mleq{}\msubb{}  qs)  {}\mRightarrow{}  (\muparrow{}qs  \mleq{}\mleq{}\msubb{}  x)  {}\mRightarrow{}  (x  =  qs))
15.  False  {}\mRightarrow{}  False  {}\mRightarrow{}  (x  =  y)
\mvdash{}  x  =\msubb{}  y  =  ff


By

---

Latex:
((Assert  g  \mmember{}  DMon  BY
                (BLemma  `omon\_inc`  THEN  Auto))
  THEN  AutoBoolCase  \mkleeneopen{}x  =\msubb{}  y\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\muparrow{}x  \mleq{}\mleq{}\msubb{}  y\mkleeneclose{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index