# Introduction to mathematical rules

There are 3 kinds of rules:

- Backforward: a predicate is transformed into zero, one or more (simpler) predicates
- Forward: 1 or more new hypotheses are generated
- Rewriting: a predicate or expression is rewritten

*Rules are generic*. Wildcards (1-letter identifiers) are used to denote any identifier.

For example, the predicate aa+bb+cc <= dd + ee matches with the following formulas:

*x <= y*where*x = aa+bb+cc*and*y = dd+ee**x+y <= z*where*x = aa+bb*,*y=cc*and*z=dd+ee*

*Rules container is THEORY*

Their general form is

- either A => B (the => symbol is a separator between sequents, not the logical implication)
- or B

B is the predicate that should match with the goal.

A (optional) is a list of conditions C (guards) and sub-goals G.

The proof of B is then replaced by the proof of G if C is true, namely C & G => B

Examples:

The rule is applied without condition:

The rule is applied if the guards hold (binhyp(H)is successful if H is an hypothesis):

Their general form is A & B => C

A is an hypothesis that has been generated

B is made of guards (D) and sub-goals (G)

C is a (list of) hypothesis to generate

If D is true and G proved then C is added to hypotheses

Their general form is C & G => A == B

A is the predicate or expression to rewrite in B

C are conditions

G are sub-goals

If C is true and G proved the A is rewritten in B

Last modified 9mo ago