Simultaneous Induction Scheme for QLOCK:

{ [1-init], [1-2-want]*, [1-2-try]*, [1-2-exit]*,
  [2-init], [2-2-want]*, [2-2-try]*, [2-2-exit]* }
   implies { [mx]*, [inv2]* } 

=def=

{ [1-init], [1-2-want]*, [1-2-try]*, [1-2-exit]*,
  [2-init], [2-2-want]*, [2-2-try]*, [2-2-exit]* }
   implies [mx]*
and
{ [1-init], [1-2-want]*, [1-2-try]*, [1-2-exit]*,
  [2-init], [2-2-want]*, [2-2-try]*, [2-2-exit]* }
   implies [inv2]*


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

-- [inv2]*
open INV2
-- for reachable states from init
   op s : -> Sys . 
   op i : -> Pid .
-- |=
   red inv2(s,i) .  
close

--> [1-init]
open INV1
   ops i j : -> Pid .
-- |=  
   red inv1(init,i,j) .
close

-- [1-2-want]*
open INV2
   ops i j k : -> Pid .
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
   eq s' = want(s,k) .
-- |=
   red istep1(i,j) .
close
-- [1-2-try]*
open INV2
   ops i j k : -> Pid .
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
   eq s' = try(s,k) .
-- |=
   red istep1(i,j) .
close
-- [1-2-exit]*
open INV2
   ops i j k : -> Pid .
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
   eq s' = exit(s,k) .
-- |=
   red istep1(i,j) .
close
-- [2-init]
open INV2
   ops i : -> Pid .
-- |=  
   red inv2(init,i) .
close
-- [2-2-want]*
open ISTEP2
   ops i k : -> Pid .
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
   eq s' = want(s,k) .
-- |=
   red istep2(i) .
close
-- [2-2-try]*
open ISTEP2
   ops i k : -> Pid .
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
   eq s' = try(s,k) .
-- |=
   red istep2(i) .
close
-- [2-2-exit]*
open ISTEP2
   ops i k : -> Pid .
   -- eq inv1(s,I:Pid,J:Pid) = true .
   -- eq inv2(s,I:Pid) = true .
   eq s' = exit(s,k) .
-- |=
   red istep2(i) .
close