in citp
in cloud



fth GOAL is 
 inc CLOUD .
 ceq tmp(S:Sys,I:Client) = valc(S:Sys) if statusp(S:Sys,I:Client) = gotval [metadata "inv6"].
 ceq true = false if statusp(S:Sys,J:Client)= updated /\ statusp(S:Sys,I:Client)= gotval[metadata "inv3" nonexec].
endfth

select #CITP# .
loop init .

(goal GOAL |- ceq valp(S:Sys,I:Client)= valc(S:Sys) if statusp(S:Sys,I:Client)= updated ;)

(ind on S:Sys red)

(tc red ca red ca red ca red imp red)

(init inv3 by S:Sys <- x#1 ; J:Client <- I#3 ; I:Client <- z#2)