in invariants-0.mod

mod ISTEP1 {
  inc(INV1)
-- s stands for current state and 
-- s' stans for next state
  ops s s' : -> Sys
-- declare predicates to prove in inductive step
  pred istep1 : Pid Pid
-- CafeOBJ variables
  vars I J : Pid
-- for defining predicates to prove in inductive step
  eq istep1(I,J) = inv1(s,I,J) implies inv1(s',I,J) .
}