*** I. Base case

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

*** II. Induction case

*** 1. get(s,k)
*** c-get(s,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 j = k .
  *** successor state
  eq s' = get(s,k) .
endfm
*** check
red istep3 .

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

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

*** ~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 istep3 .

*** 2. try(s,k)
*** c-try(s,k), ~(j = 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 (j = k) = false .
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red istep3 .

*** c-try(s,k), j = k, turn(s) < vm(s)
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 j = k .
  eq turn(s) < vm(s) = true .
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red istep3 .

*** c-try(s,k), j = k, ~(turn(s) < vm(s))
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 j = k .
  eq turn(s) < vm(s) = false .
  *** successor state
  eq s' = try(s,k) .
endfm
*** check
red inv5(s,j) implies istep3 .

*** ~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 istep3 .

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

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

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

*** ~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 istep3 .

*** Q.E.D.