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