--> I) Base case
open INV
  red inv2(init) .
close

--> II) Inductive case
--> 1 send(s)
-- 1.1 l(s) <= now(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq l(s) <= now(s) = true .
-- successor state
  eq s' = send(s) .
-- check 
  red istep2 .
close
--
-- 1.2 not(l(s) <= now(s)) 
open ISTEP
-- arbitrary objects
-- assumptions
  eq l(s) <= now(s) = false .
-- successor state
  eq s' = send(s) .
-- check 
  red istep2 .
close

--> 2 rec(s)
-- 2.1 not empty(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq empty(s) = false .
-- successor state
  eq s' = rec(s) .
-- check 
  red istep2 .
close
--
-- 2.2 empty(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq empty(s) = true .
-- successor state
  eq s' = rec(s) .
-- check 
  red istep2 .
close

--> 3 tick(s,d)
-- 3.1 now(s) + d <= u(s)
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq now(s) + d <= u(s) = true .
  --
  eq empty(s) = true .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep2 .
close
--
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq now(s) + d <= u(s) = true .
  --
  eq empty(s) = false .
  eq u(s) < l(s) = true .
-- facts
  ceq (X:Timeval) < (Y:Timeval) = true if X <= u(s) and u(s) < Y .
  ceq (X:Timeval) < (Y:Timeval) = true if X + d < Y .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep2 .
close
--
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq now(s) + d <= u(s) = true .
  --
  eq empty(s) = false .
  eq u(s) < l(s) = false .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red inv5(s) implies istep2 .
close
--
-- 3.2 not(now(s) + d <= u(s))
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq now(s) + d <= u(s) = false .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep2 .
close

--> Q.E.D.