---

Step * 1 1 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. ∀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)))} )
14. ↑x ≤≤b y
15. ↑y ≤≤b x
⊢ x =b y = tt
BY
{ RepeatFor 2 (ThinTrivial)⋅ }

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
14. ↑y ≤≤b x
15. x = y ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 
⊢ x =b y = tt

---

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.  \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))
12.  \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))
13.  (\muparrow{}x  \mleq{}\mleq{}\msubb{}  y)  {}\mRightarrow{}  (\muparrow{}y  \mleq{}\mleq{}\msubb{}  x)  {}\mRightarrow{}  (x  =  y)
14.  \muparrow{}x  \mleq{}\mleq{}\msubb{}  y
15.  \muparrow{}y  \mleq{}\mleq{}\msubb{}  x
\mvdash{}  x  =\msubb{}  y  =  tt


By

---

Latex:
RepeatFor  2  (ThinTrivial)\mcdot{}

---

Home Index