support for inequations and deductions

[lzace817]

when we do basic algebra, we want to use rules of equivalence:

• = in math;
• if and only if in logic;
• equivalence relation in abstract algebra.

and this is what we have in noq.

but sometimes we need thing that have some sort of order:

• < in math;
• imply in logic;
• partial order in abstract algebra.

the killer application for this, is the ability to make logical deductions.

you can deduce Q from P and Q. but you can not deduce P and Q from Q.

so we would have rules like: A ^ B -> A that allow us to replace the lhs by rhs. And also rules like: A^B == B^A that works both ways.

I suppose the way shaping would work in 2 possible ways:

• manual mode where a shaping operation can be selected to be either equivalece of deductive (noob)
• auto mode where shaping would be internally deductive, but if all steps are equivalence, the result must be equal. (pro)

[rexim]

I have no idea what all of these means, but it sounds way beyond the scope of a simple expression transformer.