[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Substitution matter
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
Actually i am not interested in the proof conclude in a Q.E.D. just
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.
Brian J. Cardiff