--> Base case
open INV
  red inv5(init,i) .
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 .
-- successor state
  eq s' = try(s,k) .
-- check 
  red istep5(i) .
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 istep5(i) .
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 istep5(i) .
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 istep5(i) .
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 istep5(i) .
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 istep5(i) .
close
--
open ISTEP
-- arbitrary objects
  op k : -> Pid .
-- assumptions
  -- eq c-set(s,k) = true .
  eq loc(s,k) = c .
  --
  eq (i = k) = false .
-- successor state
  eq s' = set(s,k) .
-- check 
  red istep5(i) .
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 istep5(i) .
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 .
-- successor state
  eq s' = check(s,k) .
-- check 
  red istep5(i) .
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 istep5(i) .
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 .
-- successor state
  eq s' = exit(s,k) .
-- check 
  red istep5(i) .
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 istep5(i) .
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 .
-- successor state
  eq s' = reset(s,k) .
-- check 
  red istep5(i) .
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 istep5(i) .
close

--> 7 tick(s,d)
-- 7.1 c-tick(s,d)
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq c-tick(s,d) = true .
  eq now(s) + d <= u(s,i) = true .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep5(i) .
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 istep5(i) .
close

--> Q.E.D.