Go backward to Actions Go up to Top Go forward to Validity and Provability

Predicates as Actions

• s[[P]] is boolean for any s.
• View P as action without primed variables.
  • s[[P]]t = s[[P]] for any s,t.
  • s,t is a P step iff s satisfies P.
• Replacement of unprimed variables:
  • State function or predicate F.
  • F' := F(forall 'v': v'/v).
  • s[[P']]t = t[[P]]