Step
*
1
of Lemma
oal_le_is_order
1. s : LOSet@i'
2. g : OGrp@i'
⊢ Order(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
BY
{ (% Switch to treating relations-as-1st-class-objects %
((RWH ab_binrelC 0
THENM RWW "xxorder_eq_order<" 0) THENA Auto)
THEN Try ((BLemma `omon_inc` THEN Complete (Auto)))
THEN Try ((BLemma `ocgrp_abdgrp` THEN Complete (Auto)))) }
1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ order(|oal(s;g)|;x,y:|oal(s;g)|. x ≤{s,g} y)
Latex:
Latex:
1. s : LOSet@i'
2. g : OGrp@i'
\mvdash{} Order(|oal(s;g)|;ps,qs.ps \mleq{}\{s,g\} qs)
By
Latex:
(\% Switch to treating relations-as-1st-class-objects \%
((RWH ab\_binrelC 0
THENM RWW "xxorder\_eq\_order<" 0) THENA Auto)
THEN Try ((BLemma `omon\_inc` THEN Complete (Auto)))
THEN Try ((BLemma `ocgrp\_abdgrp` THEN Complete (Auto))))
Home
Index