yav/tc-solver — Issue #2: Backward reasoning for <=
Author: yav
Created: 2011-11-11 06:56:26+00:00
State: open

We need backward rules of the form:

(x <= 5) => (x <= 7)

They are derived by specializing transitivity of <= on the axioms. It is easy to generate the correct rules
(they got removed accidentally) but first I'll have to update the generator so that it can deal with brule with parameters.

I never updated that part when adding proof objects because I though (incorrectly) that all BRules will be simple.