*** I. Base case

fmod BASE is
  pr INV .
endfm
red inv2(init,i,j) .

*** II. Induction case

*** 1. get(s,k)
*** c-get(s,k), i = k, j = k
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-get(s,k) = true .
  eq pc(s,k) = rs .
  ---
  eq i = k .
  eq j = k .
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
red istep2 .

*** c-get(s,k), i = k, ~(j = k), ~(vm(s) = turn(s) and cs = pc(s,j))
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-get(s,k) = true .
  eq pc(s,k) = rs .
  ---
  eq i = k .
  eq (j = k) = false .
  eq (vm(s) = turn(s) and cs = pc(s,j)) = false .
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
red istep2 .

*** c-get(s,k), i = k, ~(j = k), vm(s) = turn(s) and cs = pc(s,j)
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-get(s,k) = true .
  eq pc(s,k) = rs .
  ---
  eq i = k .
  eq (j = k) = false .
  --- eq (vm(s) = turn(s) and cs = pc(s,j)) = true .
  eq turn(s) = vm(s) .
  eq pc(s,j) = cs .
  ---
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
--- red inv3(s,i,j) implies istep2 .
red inv3(s,j) implies istep2 .

*** c-get(s,k), ~(i = k), j = k
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-get(s,k) = true .
  eq pc(s,k) = rs .
  ---
  eq (i = k) = false .
  eq j = k .
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
red istep2 .

*** c-get(s,k), ~(i = k), j = k
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-get(s,k) = true .
  eq pc(s,k) = rs .
  ---
  eq (i = k) = false .
  eq (j = k) = false .
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
red istep2 .

*** ~c-get(s,k)
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  eq c-get(s,k) = false .
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
red istep2 .

*** 2. try(s,k)
*** c-try(s,k), i = k
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-try(s,k) = true .
  eq pc(s,k) = ws .
  eq ticket(s,k) = turn(s) .
  ---
  eq i = k .
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red istep2 .

*** c-try(s,k), ~(i = k), ~(turn(s) = ticket(s,i) and ws = pc(s,i))
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-try(s,k) = true .
  eq pc(s,k) = ws .
  eq ticket(s,k) = turn(s) .
  ---
  eq (i = k) = false .
  eq j = k .
  eq (turn(s) = ticket(s,i) and ws = pc(s,i)) = false .
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red istep2 .

*** c-try(s,k), ~(i = k), turn(s) = ticket(s,i) and ws = pc(s,i)
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-try(s,k) = true .
  eq pc(s,k) = ws .
  eq ticket(s,k) = turn(s) .
  ---
  eq (i = k) = false .
  eq j = k .
  --- eq (turn(s) = ticket(s,i) and ws = pc(s,i)) = true .
  eq ticket(s,i) = turn(s) .
  eq pc(s,i) = ws .
  ---
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red inv4(s,i,j) implies istep2 .

*** ~c-try(s,k)
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  eq c-try(s,k) = false .
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red istep2 .

*** 3. exit(s,k)
*** c-exit(s,k), i = k
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  ---
  eq i = k .
  *** successor state
  eq s' = exit(s,k) .
endfm
*** check
red istep2 .

*** c-exit(s,k), ~(i = k)
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  --- eq c-exit(s,k) = true .
  eq pc(s,k) = cs .
  ---
  eq (i = k) = false .
  eq j = k .
  *** successor state
  eq s' = exit(s,k) .
endfm
*** check
red istep2 .

*** ~c-exit(s,k)
fmod STEP is
  pr ISTEP .
  **** arbitrary values
  op k : -> Pid .
  *** assumptions
  eq c-exit(s,k) = false .
  *** successor state
  eq s' = exit(s,k) .
endfm
*** check
red istep2 .

*** Q.E.D.