-- I) Base case

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

-- II) Inductive ceses

--> 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 p = p10 .
  eq q = p10 .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
--
  eq p = p10 .
  eq (q = p10) = false .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
--
  eq (p = p10) = false .
  eq q = p10 .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-begin(s,p10) = true .
  eq pc(s,p10) = l1 .
--
  eq (p = p10) = false .
  eq (q = p10) = false .
-- successor state
  eq s' = begin(s,p10) .
-- check if the predicate is true.
  red istep110(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 istep110(p,q) .
close

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

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

--> 4) exit(s,p10)
-- 4.1) c-exit(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = true .
  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 istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = true .
  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 istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = true .
  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 istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-exit(s,p10) = true .
  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 istep110(p,q) .
close
--
-- 4.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 istep110(p,q) .
close

--> 5) end(s,p10)
-- 5.1) c-end(s,p10)
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = true .
  eq pc(s,p10) = l4 .
--
  eq p = p10 .
  eq q = p10 .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = true .
  eq pc(s,p10) = l4 .
--
  eq p = p10 .
  eq (q = p10) = false .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = true .
  eq pc(s,p10) = l4 .
--
  eq (p = p10) = false .
  eq q = p10 .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Process .
-- assumptions
  -- eq c-end(s,p10) = true .
  eq pc(s,p10) = l4 .
--
  eq (p = p10) = false .
  eq (q = p10) = false .
-- successor state
  eq s' = end(s,p10) .
-- check if the predicate is true.
  red istep110(p,q) .
close
--
-- 5.2) not c-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 istep110(p,q) .
close

--> Q.E.D.