---

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

---

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.  Refl(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
11.  Trans(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)
12.  \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))
13.  \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))
14.  (\muparrow{}x  \mleq{}\mleq{}\msubb{}  y)  {}\mRightarrow{}  False  {}\mRightarrow{}  (x  =  y)
15.  \muparrow{}x  \mleq{}\mleq{}\msubb{}  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  skip\{(D  (-2)  THEN  RWO  "assert\_of\_eq\_list"  (-1)  THEN  Auto)\})\mcdot{}

---

Home Index