in citp
in qlock

select #CITP# .
loop init .

*** 1 ***
(goal QLOCK |-
ceq top(sq(S:Sys))= I:X$Pid if pc(S:Sys,I:X$Pid)= cs[nonexec];)
*** 2 ***
(ind on S:Sys red tc red)
*** 3 ***
(select 3)
*** 4 ***
(. imp)
*** 5 ***
(init ceq top(sq(S:Sys))= I:X$Pid if pc(S:Sys,I:X$Pid)= cs ; by I:X$Pid <- I#3
*** 6 ***
ca red imp red)
*** 7 ***
(init 1 by I:X$Pid <- z#2)
*** 8 ***
(cp-l 4 >< 6)