On Monday 09 February 2009 14:58:17 Artur Oliveira Gomes wrote:

> To represent that everything except "a" is unchanged in State, we use:
> %BV%  %theta%(State \%down%s (a))' =
> %BV%      %theta%(State \%down%s (a))
> But, using this,
> %SFT%Z
> %BV% NewState %def% [OldState : State]
> %EFT%
> In a new operation, the predicate presented before is not accepted in
> ProofPower.

For a similar predicate to work you would need the signature
of NewState to be the same as for State.
But NewState has a single component called OldState, a completely
different signature.

Hard to say how to fix the problem without knowing more about
what you are truing to do.

Roger Jones

Proofpower mailing list

Reply via email to