[PVS-Help] Substitution matter

["Brian J. Cardiff" <bcardiff@xxxxxxxxx>]

Hi, I need a bit of help with the substitution rule.

In some moment of a proof I have equations of the form:

f(a) = g(f(a))
...
|---
... f(a) ...

If the prover subst f(a) with g(f(a)) (once and again) the proof would
never finish.
Actually i am not interested in the proof conclude in a Q.E.D. just
the subgoals.

I can't just change the substitution order (LR or RL) because it's not
fixed the way this equations appear.

I think it would be necessary to have another substitution rule that
check the appearance of the LHS in the RHS. Also y would need this to
apply for example in a grind strategy.

Could anybody introduce me on how this could be accomplished.

Thanks.
Brian J. Cardiff