Step
*
2
1
1
2
of Lemma
oal_lt_trichot
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. ps : |oal(s;g)|
6. qs : |oal(s;g)|
7. ↑pos(--(qs ++ (--ps)))
⊢ ↑pos(ps ++ (--qs))
BY
{ (Subst' (--(qs ++ (--ps))) = (ps ++ (--qs)) ∈ |oal(s;g)| -1 THEN Try (Trivial)) }
1
.....equality.....
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. ps : |oal(s;g)|
6. qs : |oal(s;g)|
7. ↑pos(--(qs ++ (--ps)))
⊢ (--(qs ++ (--ps))) = (ps ++ (--qs)) ∈ |oal(s;g)|
2
.....wf.....
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. ps : |oal(s;g)|
6. qs : |oal(s;g)|
7. ↑pos(--(qs ++ (--ps)))
8. z : |oal(s;g)|
⊢ ↑pos(z) ∈ ℙ
Latex:
Latex:
1. s : LOSet
2. g : OGrp
3. g \mmember{} AbDGrp
4. g \mmember{} AbDMon
5. ps : |oal(s;g)|
6. qs : |oal(s;g)|
7. \muparrow{}pos(--(qs ++ (--ps)))
\mvdash{} \muparrow{}pos(ps ++ (--qs))
By
Latex:
(Subst' (--(qs ++ (--ps))) = (ps ++ (--qs)) -1 THEN Try (Trivial))
Home
Index