in citp
in cloud

fth INV6 is 
 inc CLOUD .
 vars I J : Client . var S : Sys .
 ceq true = false if (I ~ J) = false /\ statusp(S,J)= gotval /\ statusp(S,I)= gotval[nonexec metadata "inv4"].
endfth

select #CITP# .
loop init .

*** 1 ***
(goal INV6 |-
ceq tmp(S:Sys,I:Client)= valc(S:Sys)if statusp(S:Sys,I:Client)= gotval ;)
(ind on S:Sys red)
*** 3 ***
(tc red ca red ca red imp red)
*** 4 ***
(init inv4 by S:Sys <- x#1 ; I:Client <- I#3 ; J:Client <- z#2 ;)