--> I) Base case
open INV
  red inv5(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 istep5 .
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 istep5 .
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 istep5 .
close
--
-- 2.2 empty(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq empty(s) = true .
-- successor state
  eq s' = rec(s) .
-- check 
  red istep5 .
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 .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep5 .
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 istep5 .
close

--> Q.E.D.