• 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