sassertion

sassertion:=
assertions | axiom sdeclname sfun_arg : sexpr ;

An axiom using a general predicate to specify semantics.

assertions | axiom sdeclname sfun_arg : sexpr = sexpr ;

An axiom using equality to specify semantics.

assertions | lemma sdeclname sfun_arg : sexpr ;
assertions | lemma sdeclname sfun_arg : sexpr = sexpr ;

A lemma is a proposition which can be derived from axioms by an automatic theorem prover.

assertions | reduce sdeclname sreduce_args : sexpr => sexpr ;

A reduction is an axiom or lemma specified as a rewriting rule. Rewriting rules are applied exhaustively to eliminate left hand side terms globally.