-- I) Base case

open INV
  red inv100(init) .
close

-- II) Inductive ceses

--> 1) send(s)
-- 1.1) c-send(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-send(s) = true .
  eq flag(s) = false .
-- successor state
  eq s' = send(s) .
-- check if the predicate is true.
  red istep100 .
close
--
-- 1.2) not c-send(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-send(s) = false .
-- successor state
  eq s' = send(s) .
-- check if the predicate is true.
  red istep100 .
close

--> 2) receive(s)
-- 2.1) c-receive(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-receive(s) = false .
  eq flag(s) = false .
  eq empty?(cell(s)) = false .
--
  eq (mk(next(s)) = (next(s) list(s))) = false .
-- successor state
  eq s' = receive(s) .
-- check if the predicate is true.
  red istep100 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-receive(s) = false .
  eq flag(s) = false .
  eq empty?(cell(s)) = false .
--
  eq mk(next(s)) = (next(s) list(s)) .
-- successor state
  eq s' = receive(s) .
-- check if the predicate is true.
  red inv110(s) implies istep100 .
close
--
-- 2.2) not c-receive(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-receive(s) = false .
-- successor state
  eq s' = receive(s) .
-- check if the predicate is true.
  red istep100 .
close

--> 3) steal(s)
-- 3.1) c-steal(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-steal(s) = true .
  eq empty?(cell(s)) = false .
-- successor state
  eq s' = steal(s) .
-- check if the predicate is true.
  red istep100 .
close
--
-- 3.2) not c-steal(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-steal(s) = false .
-- successor state
  eq s' = steal(s) .
-- check if the predicate is true.
  red istep100 .
close

--> 4) update(s)
-- 4.1) c-update(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-update(s) = true .
  eq flag(s) = true .
-- successor state
  eq s' = update(s) .
-- check if the predicate is true.
  red istep100 .
close
--
-- 4.2) not c-update(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-update(s) = false .
-- successor state
  eq s' = update(s) .
-- check if the predicate is true.
  red istep100 .
close

--> Q.E.D.