--> a line starting with **> indicates a added/changed proof passage
--> a line ending with * indicates a non-effective proof passage
--
**> [mx]*
**> Q.E.D

--> [mx]*
open INV1 
-- for reachable states from init
   op s : -> Sys . 
   ops i j : -> Pid .
-- |=
   red inv1(s,i,j) .  
close 
--> Q.E.D