-- I) Base case
open QLOCK .
-- fresh constants
   op i : -> Pid .
-- |-  
   red inv7(init,i) .
close
-- II) Induction cases
-- 1) want(s,k)
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv3(s,I:Pid) = true .
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = rs .
  eq i = k .
  eq k \in queue(s) = true .
-- |-
   red inv3(s,k) and inv7(s,i) implies inv7(want(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = rs .
  eq i = k .
  eq k \in queue(s) = false .
-- |-
   red inv7(s,i) implies inv7(want(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = rs .
  eq (i = k) = false .
-- |-
   red inv7(s,i) implies inv7(want(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
   op q : -> Queue .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq (pc(s,k) = rs) = false .
-- |-
   red inv7(s,i) implies inv7(want(s,k),i) .
close
--> 2) try(s,k)
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = ws .
  eq top(queue(s)) = k .
-- |-
   red inv7(s,i) implies inv7(try(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = ws .
  eq (top(queue(s)) = k) = false .
-- |-
   red inv7(s,i) implies inv7(try(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
   op q : -> Queue .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq (pc(s,k) = ws) = false .
-- |-
   red inv7(s,i) implies inv7(try(s,k),i) .
close
-- 3) exit(s,k)
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = cs .
  eq queue(s) = empty .
-- |-
   red inv7(s,i) implies inv7(exit(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k j : -> Pid .
   op q : -> Queue .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = cs .
  eq queue(s) = j q .
  eq i = j .
  eq j = k .
  eq k \in q = true .
-- |-
   red inv7(s,i) implies inv7(exit(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k j : -> Pid .
   op q : -> Queue .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = cs .
  eq queue(s) = j q .
  eq i = j .
  eq j = k .
  eq k \in q = false .
-- |-
   red inv7(s,i) implies inv7(exit(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k j : -> Pid .
   op q : -> Queue .
-- IH
  eq [:nonexec] : inv2(s,I:Pid) = true .
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = cs .
  eq queue(s) = j q .
  eq i = j .
  eq (j = k) = false .
-- |-
   red inv2(s,k) and inv7(s,i) implies inv7(exit(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k j : -> Pid .
   op q : -> Queue .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq pc(s,k) = cs .
  eq queue(s) = j q .
  eq (i = j) = false .
-- |-
   red inv7(s,i) implies inv7(exit(s,k),i) .
close
open QLOCK .
-- fresh constants
   op s : -> Sys .
   ops i k : -> Pid .
-- IH
  eq [:nonexec] : inv7(s,I:Pid) = true .
-- assumptions
  eq (pc(s,k) = cs) = false .
-- |-
   red inv7(s,i) implies inv7(exit(s,k),i) .
close
--> Q.E.D