--> I) Base case
open INV
  red inv1(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 .
  eq empty(s) = true .
-- successor state
  eq s' = send(s) .
-- check 
  red inv2(s) implies istep1 .
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 istep1 .
close

--> 2 rec(s)
-- 2.1 not empty(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq empty(s) = false .
--
  eq list(s) = (0 .. dec(dec(data(s)))) .
  eq data(s) = 0 .
-- successor state
  eq s' = rec(s) .
-- check 
  red inv3(s) implies istep1 .
close
--
open ISTEP
-- arbitrary objects
  op n : -> Nat .
-- assumptions
  eq empty(s) = false .
--
  eq list(s) = (0 .. dec(dec(data(s)))) .
  eq data(s) = s(n) .
  eq content(s) = n .
-- successor state
  eq s' = rec(s) .
-- check 
  red istep1 .
close
--
open ISTEP
-- arbitrary objects
  op n : -> Nat .
-- assumptions
  eq empty(s) = false .
--
  eq list(s) = (0 .. dec(dec(data(s)))) .
  eq data(s) = s(n) .
  eq (content(s) = n) = false .
-- successor state
  eq s' = rec(s) .
-- check 
  red inv4(s) implies istep1 .
close
--
open ISTEP
-- arbitrary objects
  op n : -> Nat .
-- assumptions
  eq empty(s) = false .
--
  eq (list(s) = (0 .. dec(dec(data(s))))) = false .
-- successor state
  eq s' = rec(s) .
-- check 
  red istep1 .
close
--
-- 2.2 empty(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq empty(s) = true .
-- successor state
  eq s' = rec(s) .
-- check 
  red istep1 .
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 istep1 .
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 istep1 .
close

--> Q.E.D.