Artur, 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
