The frame rule allows to put execute a command in a wider frame:
A number of support functions have to be implemented to support this rule.
Given our command r, its pre and post formulas p and q, and the outer formula q * t, we want to derive t in order to then derive p * t. This can be first done by brutally searching for the exact formula q inside of the formula q * t, but of course other smarter solution will be later needed.
Other functions to extract modified and free variables.
The frame rule allows to put execute a command in a wider frame:
A number of support functions have to be implemented to support this rule.
r, its pre and post formulaspandq, and the outer formulaq * t, we want to derivetin order to then derivep * t. This can be first done by brutally searching for the exact formulaqinside of the formulaq * t, but of course other smarter solution will be later needed.