standard simplifier
| rlsimpl(formula: Formula, assume = {}: List(Atom), depth = - 1: Integer, ...) |
| Formula |
| formula | first-order input formula |
| assume | atomic input assumptions |
| depth | maximal recursion depth |
| sichk | check for equal nonatomic sibling formulas |
| sid | smart simplification of derivatives (domain 'padic' only) |
| sisocx | sort non-atomic subformulas |
| sipd | degree parity decompositon |
| siplugtheo | plug in values obtained from implicit theory |
| siexpla | always split atoms f*g=0 and f*g<>0 |
| siexpl | split f*g=0 and f*g<>0 in disjunctions and conjunctions, respectively |
| sifaco | factorize left hand sides of order relations |
| sifac | factorize left hand sides of non-order relations |
| sipw | prefer <=, >= over <, > |
| sipo | prefer <, <=, >, >= over =, <> |