Step
*
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)))} )
⊢ x =b y = x ≤≤b y ∧b y ≤≤b x
BY
{ (AutoBoolCase ⌜x ≤≤b y⌝⋅ THEN AutoBoolCase ⌜y ≤≤b x⌝⋅) }
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)))} )
14. ↑x ≤≤b y
15. ↑y ≤≤b x
⊢ x =b y = tt
2
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
3
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. ¬↑x ≤≤b y
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. False
⇒ (↑y ≤≤b x)
⇒ (x = y ∈ {ps:(|s| × |g|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} )
15. ↑y ≤≤b x
⊢ x =b y = ff
4
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
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)
\mvdash{} x =\msubb{} y = x \mleq{}\mleq{}\msubb{} y \mwedge{}\msubb{} y \mleq{}\mleq{}\msubb{} x
By
Latex:
(AutoBoolCase \mkleeneopen{}x \mleq{}\mleq{}\msubb{} y\mkleeneclose{}\mcdot{} THEN AutoBoolCase \mkleeneopen{}y \mleq{}\mleq{}\msubb{} x\mkleeneclose{}\mcdot{})
Home
Index