-- I) Base case

open INV
  red inv100(init,p,q) .
close

-- II) Inductive ceses

--
-- In each inductive case where we prove that any transition rule
-- corresponding to an action 'act' preserves a property P, namely
-- P(s) implies P(act(s)) for any s, we usually have to split the
-- state space into multiple ones to make progress on the proof.
-- For each sub-space, a proof score that looks as follows is written:
--
--   open ISTEP
--   -- arbitrary objects
--     Declare constants denoting arbitrary objects.
--   -- assumption
--     Declare equations characterizing this sub-space.
--   -- successor state
--     eq s' = act(s) .
--   -- check if the predicate is true
--     red P(s) implies P(s') .
--   close
--
-- In a proof score, we use constants to denote arbitrary objects.
--
-- Invariants and actions usually have arguments other than one
-- denoting states such as p, q, and p10 of inv100(s,p,q) and begin(s,p10). 
-- We have to show invariants for not only any state but also any such
-- arguments. Constants are usually used to denote arbitrary objects
-- such as states and processes. 
--
-- Constants, such as s, denoting arbitaray states are declared in
-- module ISTEP. 
-- Constans, such as p and q, denoting arbitrary arguments except for
-- states of invariants are declared in module INV.
-- Constants, such as p10, denoting argutrary arguments except for
-- states of actions are declared in each proof score.
--
-- We sometimes need more constnats, which are declared in each proof
-- score.
--
--> 1) begin(s,p10)
-- 1.1) c-begin(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
  eq locked(s) = false .
--
  eq p = p10 .
  eq q = p10 .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
  eq locked(s) = false .
--
  eq (q = p10) = false .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red inv110(s,q) implies istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
  eq locked(s) = false .
--
  eq (p = p10) = false .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red inv110(s,p) implies istep100(p,q) .
close
--
-- 1.2) not c-begin(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  eq c-begin(s,p10) = false .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close

--> 2) exit(s,p10)
-- 2.1) c-exit(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = false .
  eq pc(s,p10) = cs .
--
  eq p = p10 .
  eq q = p10 .
-- successor state
  eq s' = exit(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = false .
  eq pc(s,p10) = cs .
--
  eq p = p10 .
  eq (q = p10) = false .
-- successor state
  eq s' = exit(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = false .
  eq pc(s,p10) = cs .
--
  eq (p = p10) = false .
  eq q = p10 .
-- successor state
  eq s' = exit(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = false .
  eq pc(s,p10) = cs .
--
  eq (p = p10) = false .
  eq (q = p10) = false .
-- successor state
  eq s' = exit(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
-- 2.2) not c-exit(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  eq c-exit(s,p10) = false .
-- successor state
  eq s' = exit(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close

--> 3) end(s,p10)
-- 3.1) end(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = false .
  eq pc(s,p10) = l2 .
--
  eq p = p10 .
  eq q = p10 .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = false .
  eq pc(s,p10) = l2 .
--
  eq p = p10 .
  eq (q = p10) = false .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = false .
  eq pc(s,p10) = l2 .
--
  eq (p = p10) = false .
  eq q = p10 .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = false .
  eq pc(s,p10) = l2 .
--
  eq (p = p10) = false .
  eq (q = p10) = false .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close
--
-- 3.2) not end(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  eq c-end(s,p10) = false .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep100(p,q) .
close

--> Q.E.D.