Rather than ensuring sub-expressions are identical in order to cancel them (in a sum or product/division), we can do this based upon canonical forms. This has been implemented for Add (in the QPE_finale_witzel branch) but not yet for Mult and Divide. Cancelation theorems need to be changed for this to work flexibly. For example,
rather than just having "a - a = 0". The same needs to be done for multiplicative cancelations.
Rather than ensuring sub-expressions are identical in order to cancel them (in a sum or product/division), we can do this based upon canonical forms. This has been implemented for Add (in the QPE_finale_witzel branch) but not yet for Mult and Divide. Cancelation theorems need to be changed for this to work flexibly. For example,
rather than just having "a - a = 0". The same needs to be done for multiplicative cancelations.