Edit formulas edit
to simplify formulas.
Edit supports special functions: use
abbrv
to abbreviate terms
expand
to expand functions abs/min/max
How to abbreviate:
- Click Edit, enclose a term with
abbrv(...)
for anonymous abbreviation or type
abbrv(..., x)
to introduce abbreviation x
.
- Click hint Abbrv and enter an abbreviation name and a term that should be abbreviated.
How to expand:
- Click Edit, enclose a function symbol abs(t), min(s,t), or max(s,t) with
expand(...)
to expand the function symbol
See also
- Tools → Smart Arithmetic for quantifier elimination that attempts automated hiding.
- Tools → Counterexample to get potentially faster feedback whether the sequent might be true or false.
- Tools → Find assumptions to get hints on how to strengthen the assumptions to make the sequent provable.
Learning resources