monoid-cancellation-laws
comb_kk-values
compute-card
covers-direct-image-to-inverse-image-conversion-macete
indicator-conversions
iota-abstraction-macete
eliminate-iota-macete
eliminate-forsome-macete
direct-image-to-inverse-image-conversion-macete
indicator-facts-macete
rewrite-rules-for-pairs
drop-cons-and-simplify
in_seq-macete
sequence-length
le-contains-point
simplify-set-translations
simplify-actions
group-cancellation-laws
lct-macete
simplify-normal-subgroup-expressions
simplify-right-coset-expressions
subgroup-membership
abstraction
composite-continuity-macete
real-fn-abstraction
polynomial-continuity-macete
simplify-subnet-disjointness-assertion
simplify-address-set-disjointness-assertion
simplify-address-expression
ns-fractional-expression-manipulation
fractional-expression-manipulation
integer-induction
definedness-manipulations
factorial-reduction
abstraction-for-sequences
solve-product-equation-or-inequality
solve-quadratic-equation-or-inequality
crude-primality-test