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,
> %BV% NewState %def% [OldState : State]
> In a new operation, the predicate presented before is not accepted in
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
Hard to say how to fix the problem without knowing more about
what you are truing to do.
Proofpower mailing list