-- I) Base case

open INV
  red inv110(init) .
close

-- II) Inductive ceses

--> 1) inc(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq x(s) >= 0 = true .
-- successor state
  eq s' = inc(s) .
-- check if the predicate is true.
  red istep110 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  eq x(s) >= 0 = false .
-- successor state
  eq s' = inc(s) .
-- check if the predicate is true.
  red inv100(s) implies istep110 .
close

--> 2) dec(s)
-- 2.1) c-dec(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dec(s) = treue .
  eq flag(s) = true .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red istep110 .
close
--
-- 2.1) not c-dec(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-dec(s) = false .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red istep110 .
close

--> Q.E.D.