--> Base case
open INV
  red inv4(init,i,j) .
close

--> Inductive cases
--> 1 try(s,k)
-- 1.1 c-try(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-try(s,k) = true .
  eq loc(s,k) = a .
  --
  eq i = k .
-- successor state
  eq s' = try(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-try(s,k) = true .
  eq loc(s,k) = a .
  --
  eq (i = k) = false .
  eq j = k .
-- successor state
  eq s' = try(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-try(s,k) = true .
  eq loc(s,k) = a .
  --
  eq (i = k) = false .
  eq (j = k) = false .
-- successor state
  eq s' = try(s,k) .
-- check 
  red istep4(i,j) .
close
--
-- 1.2 not c-try(s,k) 
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-try(s,k) = false .
-- successor state
  eq s' = try(s,k) .
-- check 
  red istep4(i,j) .
close

--> 2 test(s,k)
-- 2.1 c-test(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-test(s,k) = true .
  eq loc(s,k) = b .
  eq turn(s) = nop .
  --
  eq i = k .
-- successor state
  eq s' = test(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-test(s,k) = true .
  eq loc(s,k) = b .
  eq turn(s) = nop .
  --
  eq (i = k) = false .
-- successor state
  eq s' = test(s,k) .
-- check 
  red istep4(i,j) .
close
--
-- 2.2 not c-test(s,k) 
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-test(s,k) = false .
-- successor state
  eq s' = test(s,k) .
-- check 
  red istep4(i,j) .
close

--> 3 set(s,k)
-- 3.1 c-set(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-set(s,k) = true .
  eq loc(s,k) = c .
  --
  eq i = k .
-- successor state
  eq s' = set(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-set(s,k) = true .
  eq loc(s,k) = c .
  --
  eq (i = k) = false .
  eq j = k .
-- successor state
  eq s' = set(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-set(s,k) = true .
  eq loc(s,k) = c .
  --
  eq (i = k) = false .
  eq (j = k) = false .
-- successor state
  eq s' = set(s,k) .
-- check 
  red inv4(s,i,k) implies istep4(i,j) .
close
--
-- 3.2 not c-set(s,k) 
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-set(s,k) = false .
-- successor state
  eq s' = set(s,k) .
-- check 
  red istep4(i,j) .
close

--> 4 check(s,k)
-- 4.1 c-check(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq i = k .
  eq j = k .
  eq turn(s) = k .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq i = k .
  eq j = k .
  eq (turn(s) = k) = false .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq i = k .
  eq (j = k) = false .
  eq turn(s) = k .
  eq now(s) <= u(s,j) = true .
-- facts
  ceq (X:Real+) <= (Y:Timeval) = true if X <= now(s) and now(s) <= Y .
-- successor state
  eq s' = check(s,k) .
-- check 
  red inv2(s,i,j) implies istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq i = k .
  eq (j = k) = false .
  eq turn(s) = k .
  eq now(s) <= u(s,j) = false .
-- successor state
  eq s' = check(s,k) .
-- check 
  red inv5(s,j) implies istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq i = k .
  eq (j = k) = false .
  eq (turn(s) = k) = false .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq (i = k) = false .
  eq j = k .
  eq turn(s) = k .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq (i = k) = false .
  eq j = k .
  eq (turn(s) = k) = false .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-check(s,k) = true .
  eq loc(s,k) = d .
  eq l(s,k) <= now(s) = true .
  --
  eq (i = k) = false .
  eq (j = k) = false .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close
--
-- 4.2 not c-check(s,k) 
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-check(s,k) = false .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep4(i,j) .
close

--> 5 exit(s,k)
-- 5.1 c-exit(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq loc(s,k) = cs .
  --
  eq i = k .
  eq j = k .
-- successor state
  eq s' = exit(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq loc(s,k) = cs .
  --
  eq i = k .
  eq (j = k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq loc(s,k) = cs .
  --
  eq (i = k) = false .
  eq j = k .
-- successor state
  eq s' = exit(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-exit(s,k) = true .
  eq loc(s,k) = cs .
  --
  eq (i = k) = false .
  eq (j = k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check 
  red istep4(i,j) .
close
--
-- 5.2 not c-exit(s,k) 
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-exit(s,k) = false .
-- successor state
  eq s' = exit(s,k) .
-- check 
  red istep4(i,j) .
close

--> 6 reset(s,k)
-- 6.1 c-reset(s,k)
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-reset(s,k) = true .
  eq loc(s,k) = e .
  --
  eq i = k .
-- successor state
  eq s' = reset(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-reset(s,k) = true .
  eq loc(s,k) = e .
  --
  eq (i = k) = false .
  eq turn(s) = k .
-- successor state
  eq s' = reset(s,k) .
-- check 
  red istep4(i,j) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-reset(s,k) = true .
  eq loc(s,k) = e .
  --
  eq (i = k) = false .
  eq (turn(s) = k) = false .
-- successor state
  eq s' = reset(s,k) .
-- check 
  red inv4(s,k,i) implies istep4(i,j) .
close
--
-- 6.2 not c-reset(s,k) 
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  eq c-reset(s,k) = false .
-- successor state
  eq s' = reset(s,k) .
-- check 
  red istep4(i,j) .
close

--> 7 tick(s,d)
-- 7.1 c-tick(s,d)
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
  op k : -> Pid .
-- assumptions
  eq c-tick(s,d) = true .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep4(i,j) .
close
--
-- 7.2 not c-tick(s,d) 
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq c-tick(s,d) = false .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep4(i,j) .
close

--> Q.E.D.