Question: Assumptions - calculations

restart;
a:='a';
                               a
assume(a>0);
H:=a;
                               a
subs(a=b, H);
                               b
a:='a';
                               a
assume(a>0);
subs(a=b, H);
                               a
It's clear that last operator return a, not b, because originally H points to "1st assumed a", which is became invalid. How to recalculate ALL "calculated-after-assumptions" expressions to become those pointers valid?

Please Wait...