theory German_baukus_defs

use import bool.Bool
use import int.Int

type state = Invalid | Shared | Exclusive
type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte

function exgntd : bool
function curcmd : msg
function curClient : int
function exgntd' : bool
function curcmd' : msg
function curClient' : int
function chan1 int : msg
function chan2 int : msg
function chan3 int : msg
function cache int : state
function invset int : bool
function shrset int : bool
function chan1' int : msg
function chan2' int : msg
function chan3' int : msg
function cache' int : state
function invset' int : bool
function shrset' int : bool

end


theory German_baukus_invpreds

use import bool.Bool
use import int.Int
use import German_baukus_defs

predicate invariantX512 =
not (exists z1:int. (cache z1) <> Invalid /\
(shrset z1) = False)

predicate invariantX512' =
not (exists z1:int. (cache' z1) <> Invalid /\
(shrset' z1) = False)

predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(cache z2) <> Invalid)

predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(cache' z2) <> Invalid)

predicate invariantX186 =
not (exists z1:int. curcmd = Empty /\
(chan2 z1) = Inv)

predicate invariantX186' =
not (exists z1:int. curcmd' = Empty /\
(chan2' z1) = Inv)

predicate invariant456 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan3 z2) = Invack)

predicate invariant456' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan3' z2) = Invack)

predicate invariantX117 =
not (exists z1:int. (chan2 z1) = Inv /\
(chan3 z1) = Invack)

predicate invariantX117' =
not (exists z1:int. (chan2' z1) = Inv /\
(chan3' z1) = Invack)

predicate invariantX307 =
not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(invset z2) = True)

predicate invariantX307' =
not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(invset' z2) = True)

predicate invariant974 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z1) = Empty /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(cache z1) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)

predicate invariant974' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z1) = Empty /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(cache' z1) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)

predicate invariant910 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(invset z1) = True /\
(invset z2) = True)

predicate invariant910' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(invset' z1) = True /\
(invset' z2) = True)

predicate invariant528 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Empty /\
(chan3 z2) = Invack /\
(invset z1) = True)

predicate invariant528' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Empty /\
(chan3' z2) = Invack /\
(invset' z1) = True)

predicate invariant530 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan2 z1) = Inv /\
(chan2 z2) = Inv /\
(chan3 z2) = Empty)

predicate invariant530' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan2' z1) = Inv /\
(chan2' z2) = Inv /\
(chan3' z2) = Empty)

predicate invariantX238 =
not (exists z1 z2:int. z1 <> z2 /\ (chan3 z2) = Invack /\
(cache z1) = Exclusive)

predicate invariantX238' =
not (exists z1 z2:int. z1 <> z2 /\ (chan3' z2) = Invack /\
(cache' z1) = Exclusive)

predicate invariantX494 =
not (exists z1:int. (chan2 z1) = Gnts /\
(chan3 z1) = Invack)

predicate invariantX494' =
not (exists z1:int. (chan2' z1) = Gnts /\
(chan3' z1) = Invack)

predicate invariantX428 =
not (exists z1:int. (cache z1) = Exclusive /\
(shrset z1) = False)

predicate invariantX428' =
not (exists z1:int. (cache' z1) = Exclusive /\
(shrset' z1) = False)

predicate invariantX172 =
not (exists z1:int. curcmd = Empty /\
(chan3 z1) = Invack)

predicate invariantX172' =
not (exists z1:int. curcmd' = Empty /\
(chan3' z1) = Invack)

predicate invariant407 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan3 z1) = Invack /\
(chan3 z2) = Invack)

predicate invariant407' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan3' z1) = Invack /\
(chan3' z2) = Invack)

predicate invariant87 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Gnte)

predicate invariant87' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Gnte)

predicate invariantX40 =
not (exists z1:int. exgntd = False /\
(cache z1) = Exclusive)

predicate invariantX40' =
not (exists z1:int. exgntd' = False /\
(cache' z1) = Exclusive)

predicate invariant731 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Inv /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(invset z2) = True)

predicate invariant731' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Inv /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(invset' z2) = True)

predicate invariantX101 =
not (exists z1:int. (chan2 z1) = Inv /\
(shrset z1) = False)

predicate invariantX101' =
not (exists z1:int. (chan2' z1) = Inv /\
(shrset' z1) = False)

predicate invariant732 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Inv /\
(chan3 z2) = Empty /\
(invset z1) = True)

predicate invariant732' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Inv /\
(chan3' z2) = Empty /\
(invset' z1) = True)

predicate invariant28 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z2) = Gnts /\
(cache z1) = Exclusive)

predicate invariant28' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z2) = Gnts /\
(cache' z1) = Exclusive)

predicate invariant796 =
not (exists z1:int. (chan2 z1) = Gnte /\
(shrset z1) = False)

predicate invariant796' =
not (exists z1:int. (chan2' z1) = Gnte /\
(shrset' z1) = False)

predicate invariant30 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z2) = Gnte /\
(cache z1) = Exclusive)

predicate invariant30' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z2) = Gnte /\
(cache' z1) = Exclusive)

predicate invariant31 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(cache z2) <> Invalid)

predicate invariant31' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(cache' z2) <> Invalid)

predicate invariantX160 =
not (exists z1:int. (chan2 z1) = Inv /\
(invset z1) = True)

predicate invariantX160' =
not (exists z1:int. (chan2' z1) = Inv /\
(invset' z1) = True)

predicate invariant225 =
not (exists z1:int. (chan2 z1) = Gnte /\
(chan3 z1) = Invack)

predicate invariant225' =
not (exists z1:int. (chan2' z1) = Gnte /\
(chan3' z1) = Invack)

predicate invariantX285 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z2) = Inv /\
(cache z1) = Exclusive)

predicate invariantX285' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z2) = Inv /\
(cache' z1) = Exclusive)

predicate invariant422 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan2 z1) = Inv /\
(chan3 z2) = Invack)

predicate invariant422' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan2' z1) = Inv /\
(chan3' z2) = Invack)

predicate invariantX217 =
not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan2 z1) = Inv)

predicate invariantX217' =
not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan2' z1) = Inv)

predicate invariantX88 =
not (exists z1:int. (chan3 z1) = Invack /\
(shrset z1) = False)

predicate invariantX88' =
not (exists z1:int. (chan3' z1) = Invack /\
(shrset' z1) = False)

predicate invariantX151 =
not (exists z1:int. (chan3 z1) = Invack /\
(invset z1) = True)

predicate invariantX151' =
not (exists z1:int. (chan3' z1) = Invack /\
(invset' z1) = True)

predicate invariant687 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(shrset z2) = True)

predicate invariant687' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(shrset' z2) = True)

predicate invariantX529 =
not (exists z1:int. (chan3 z1) = Invack /\
(cache z1) <> Invalid)

predicate invariantX529' =
not (exists z1:int. (chan3' z1) = Invack /\
(cache' z1) <> Invalid)

predicate invariantX465 =
not (exists z1:int. (chan2 z1) = Gnts /\
(shrset z1) = False)

predicate invariantX465' =
not (exists z1:int. (chan2' z1) = Gnts /\
(shrset' z1) = False)

predicate invariantX336 =
not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(shrset z2) = True)

predicate invariantX336' =
not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(shrset' z2) = True)

predicate invariant625 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(invset z2) = True)

predicate invariant625' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(invset' z2) = True)

predicate invariantX399 =
not (exists z1:int. exgntd = True /\
(chan2 z1) = Gnts)

predicate invariantX399' =
not (exists z1:int. exgntd' = True /\
(chan2' z1) = Gnts)

predicate invariant946 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z2) = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)

predicate invariant946' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z2) = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)

predicate invariant947 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z1) = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)

predicate invariant947' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z1) = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)

predicate invariant1012 =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z3) = Empty /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(cache z3) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)

predicate invariant1012' =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z3) = Empty /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(cache' z3) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)

predicate invariant948 =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z3) = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)

predicate invariant948' =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z3) = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)

predicate invariant565 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Inv)

predicate invariant565' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Inv)

predicate invariantX199 =
not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan3 z1) = Invack)

predicate invariantX199' =
not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan3' z1) = Invack)

predicate invariantX134 =
not (exists z1:int. (invset z1) = True /\
(shrset z1) = False)

predicate invariantX134' =
not (exists z1:int. (invset' z1) = True /\
(shrset' z1) = False)

predicate invariant59 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Gnts)

predicate invariant59' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Gnts)

predicate invariant188 =
not (exists z1:int. exgntd = False /\
(chan2 z1) = Gnte)

predicate invariant188' =
not (exists z1:int. exgntd' = False /\
(chan2' z1) = Gnte)

predicate invariant958 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z2) = Empty /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(cache z2) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)

predicate invariant958' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z2) = Empty /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(cache' z2) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)

predicate invariantX65 =
not (exists z1:int. (chan3 z1) = Invack /\
(cache z1) = Exclusive)

predicate invariantX65' =
not (exists z1:int. (chan3' z1) = Invack /\
(cache' z1) = Exclusive)


end


theory German_baukus_trdefs

use import bool.Bool
use import int.Int
use import German_baukus_defs

predicate transition__send_invack =
(* transition send_invack *)
(exists n:int. 
( (* requires *)
(chan2 n) = Inv /\
(chan3 n) = Empty) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan2' j = Empty
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
 chan3' j = Invack
else chan3' j = (chan3 j)) /\
(forall j:int.
if j = n then
 cache' j = Invalid
else cache' j = (cache j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__send_req_shared =
(* transition send_req_shared *)
(exists n:int. 
( (* requires *)
(chan1 n) = Empty /\
(cache n) = Invalid) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan1' j = Reqs
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__recv_gnt_exclusive =
(* transition recv_gnt_exclusive *)
(exists n:int. 
( (* requires *)
(chan2 n) = Gnte) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 cache' j = Exclusive
else cache' j = (cache j)) /\
(forall j:int.
if j = n then
 chan2' j = Empty
else chan2' j = (chan2 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__send_gnt_exclusive =
(* transition send_gnt_exclusive *)
(exists n:int. 
( (* requires *)
curcmd = Reqe /\
curClient = n /\
(chan2 n) = Empty /\
(shrset n) = False
/\ (forall j:int.n = j \/ 
((shrset j) = False))
) /\
( (* actions *)
curcmd' = Empty /\
exgntd' = True /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan2' j = Gnte
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
 shrset' j = True
else shrset' j = (shrset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) ))


predicate transition__send_req_exclusive_2 =
(* transition send_req_exclusive_2 *)
(exists n:int. 
( (* requires *)
(chan1 n) = Empty /\
(cache n) = Shared) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan1' j = Reqe
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__recv_req_exclusive =
(* transition recv_req_exclusive *)
(exists n:int. 
( (* requires *)
curcmd = Empty /\
(chan1 n) = Reqe) /\
( (* actions *)
curcmd' = Reqe /\
curClient' = n /\
exgntd' = exgntd /\
(forall j:int.
invset' j = (shrset j)) /\
(forall j:int.
if j = n then
 chan1' j = Empty
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__recv_gnt_shared =
(* transition recv_gnt_shared *)
(exists n:int. 
( (* requires *)
(chan2 n) = Gnts) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 cache' j = Shared
else cache' j = (cache j)) /\
(forall j:int.
if j = n then
 chan2' j = Empty
else chan2' j = (chan2 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__send_gnt_shared =
(* transition send_gnt_shared *)
(exists n:int. 
( (* requires *)
exgntd = False /\
curcmd = Reqs /\
curClient = n /\
(chan2 n) = Empty) /\
( (* actions *)
curcmd' = Empty /\
exgntd' = exgntd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan2' j = Gnts
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
 shrset' j = True
else shrset' j = (shrset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) ))


predicate transition__recv_req_shared =
(* transition recv_req_shared *)
(exists n:int. 
( (* requires *)
curcmd = Empty /\
(chan1 n) = Reqs) /\
( (* actions *)
curcmd' = Reqs /\
curClient' = n /\
exgntd' = exgntd /\
(forall j:int.
invset' j = (shrset j)) /\
(forall j:int.
if j = n then
 chan1' j = Empty
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__recv_invack =
(* transition recv_invack *)
(exists n:int. 
( (* requires *)
curcmd <> Empty /\
(chan3 n) = Invack) /\
( (* actions *)
exgntd' = False /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan3' j = Empty
else chan3' j = (chan3 j)) /\
(forall j:int.
if j = n then
 shrset' j = False
else shrset' j = (shrset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) ))


predicate transition__send_inv_2 =
(* transition send_inv_2 *)
(exists n:int. 
( (* requires *)
exgntd = True /\
curcmd = Reqs /\
(chan2 n) = Empty /\
(invset n) = True) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan2' j = Inv
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
 invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__send_inv_1 =
(* transition send_inv_1 *)
(exists n:int. 
( (* requires *)
curcmd = Reqe /\
(chan2 n) = Empty /\
(invset n) = True) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan2' j = Inv
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
 invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate transition__send_req_exclusive_1 =
(* transition send_req_exclusive_1 *)
(exists n:int. 
( (* requires *)
(chan1 n) = Empty /\
(cache n) = Invalid) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
 chan1' j = Reqe
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


predicate tau =
(transition__send_req_exclusive_1 \/ transition__send_inv_1 \/ transition__send_inv_2 \/ transition__recv_invack \/ transition__recv_req_shared \/ transition__send_gnt_shared \/ transition__recv_gnt_shared \/ transition__recv_req_exclusive \/ transition__send_req_exclusive_2 \/ transition__send_gnt_exclusive \/ transition__recv_gnt_exclusive \/ transition__send_req_shared \/ transition__send_invack)


end


theory German_baukus_initialisation

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds

predicate init =
    forall z:int. (exgntd = False /\
curcmd = Empty /\
(chan1 z) = Empty /\
(chan2 z) = Empty /\
(chan3 z) = Empty /\
(cache z) = Invalid /\
(invset z) = False /\
(shrset z) = False)

goal initialisation:
    init -> (invariantX65 /\ invariant958 /\ invariant188 /\ invariant59 /\ invariantX134 /\ invariantX199 /\ invariant565 /\ invariant948 /\ invariant1012 /\ invariant947 /\ invariant946 /\ invariantX399 /\ invariant625 /\ invariantX336 /\ invariantX465 /\ invariantX529 /\ invariant687 /\ invariantX151 /\ invariantX88 /\ invariantX217 /\ invariant422 /\ invariantX285 /\ invariant225 /\ invariantX160 /\ invariant31 /\ invariant30 /\ invariant796 /\ invariant28 /\ invariant732 /\ invariantX101 /\ invariant731 /\ invariantX40 /\ invariant87 /\ invariant407 /\ invariantX172 /\ invariantX428 /\ invariantX494 /\ invariantX238 /\ invariant530 /\ invariant528 /\ invariant910 /\ invariant974 /\ invariantX307 /\ invariantX117 /\ invariant456 /\ invariantX186 /\ invariant1 /\ invariantX512)


end


theory German_baukus_property

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds

goal property:
    (invariantX65 /\ invariant958 /\ invariant188 /\ invariant59 /\ invariantX134 /\ invariantX199 /\ invariant565 /\ invariant948 /\ invariant1012 /\ invariant947 /\ invariant946 /\ invariantX399 /\ invariant625 /\ invariantX336 /\ invariantX465 /\ invariantX529 /\ invariant687 /\ invariantX151 /\ invariantX88 /\ invariantX217 /\ invariant422 /\ invariantX285 /\ invariant225 /\ invariantX160 /\ invariant31 /\ invariant30 /\ invariant796 /\ invariant28 /\ invariant732 /\ invariantX101 /\ invariant731 /\ invariantX40 /\ invariant87 /\ invariant407 /\ invariantX172 /\ invariantX428 /\ invariantX494 /\ invariantX238 /\ invariant530 /\ invariant528 /\ invariant910 /\ invariant974 /\ invariantX307 /\ invariantX117 /\ invariant456 /\ invariantX186 /\ invariant1 /\ invariantX512) -> (not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(cache z2) <> Invalid))


end


theory German_baukus_hint_1

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_1:
    (invariantX529 /\ invariantX494 /\ invariantX172 /\ invariantX151 /\ invariantX88 /\ invariant225 /\ tau)
    -> invariantX529'



end


theory German_baukus_hint_2

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_2:
    (invariantX529 /\ invariantX512 /\ invariantX465 /\ invariantX134 /\ invariant796 /\ tau)
    -> invariantX512'



end


theory German_baukus_hint_3

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_3:
    (invariantX494 /\ invariantX399 /\ invariantX199 /\ invariantX172 /\ invariantX88 /\ tau)
    -> invariantX494'



end


theory German_baukus_hint_4

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_4:
    (invariantX494 /\ invariantX465 /\ invariantX399 /\ tau)
    -> invariantX465'



end


theory German_baukus_hint_5

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_5:
    (invariantX428 /\ invariantX134 /\ invariantX65 /\ invariantX40 /\ invariant796 /\ tau)
    -> invariantX428'



end


theory German_baukus_hint_6

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_6:
    (invariantX465 /\ invariantX399 /\ tau)
    -> invariantX399'



end


theory German_baukus_hint_7

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_7:
    (invariantX428 /\ invariantX336 /\ invariantX307 /\ invariantX285 /\ invariantX65 /\ invariantX40 /\ invariant687 /\ tau)
    -> invariantX336'



end


theory German_baukus_hint_8

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_8:
    (invariantX428 /\ invariantX336 /\ invariantX307 /\ invariantX285 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant625 /\ tau)
    -> invariantX307'



end


theory German_baukus_hint_9

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_9:
    (invariantX428 /\ invariantX307 /\ invariantX285 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant565 /\ tau)
    -> invariantX285'



end


theory German_baukus_hint_10

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_10:
    (invariantX428 /\ invariantX285 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant456 /\ tau)
    -> invariantX238'



end


theory German_baukus_hint_11

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_11:
    (invariantX217 /\ invariantX186 /\ invariantX117 /\ invariant422 /\ tau)
    -> invariantX217'



end


theory German_baukus_hint_12

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_12:
    (invariantX529 /\ invariantX494 /\ invariantX217 /\ invariantX199 /\ invariantX172 /\ invariant188 /\ invariant407 /\ tau)
    -> invariantX199'



end


theory German_baukus_hint_13

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_13:
    (invariantX217 /\ invariantX186 /\ invariantX101 /\ tau)
    -> invariantX186'



end


theory German_baukus_hint_14

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_14:
    (invariantX199 /\ invariantX186 /\ invariantX172 /\ invariantX88 /\ tau)
    -> invariantX172'



end


theory German_baukus_hint_15

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_15:
    (invariantX186 /\ invariantX160 /\ invariantX117 /\ invariantX101 /\ tau)
    -> invariantX160'



end


theory German_baukus_hint_16

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_16:
    (invariantX172 /\ invariantX160 /\ invariantX151 /\ invariantX88 /\ tau)
    -> invariantX151'



end


theory German_baukus_hint_17

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_17:
    (invariantX151 /\ invariantX134 /\ invariantX101 /\ tau)
    -> invariantX134'



end


theory German_baukus_hint_18

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_18:
    (invariantX151 /\ invariantX117 /\ invariantX88 /\ tau)
    -> invariantX117'



end


theory German_baukus_hint_19

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_19:
    (invariantX134 /\ invariantX117 /\ invariantX101 /\ tau)
    -> invariantX101'



end


theory German_baukus_hint_20

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_20:
    (invariantX101 /\ invariantX88 /\ tau)
    -> invariantX88'



end


theory German_baukus_hint_21

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_21:
    (invariantX65 /\ invariantX40 /\ invariant225 /\ tau)
    -> invariantX65'



end


theory German_baukus_hint_22

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_22:
    (invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant188 /\ tau)
    -> invariantX40'



end


theory German_baukus_hint_23

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_23:
    (invariantX428 /\ invariantX307 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant1 /\ invariant28 /\ invariant30 /\ invariant31 /\ tau)
    -> invariant1'



end


theory German_baukus_hint_24

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_24:
    (invariantX428 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant1 /\ invariant28 /\ invariant59 /\ tau)
    -> invariant28'



end


theory German_baukus_hint_25

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_25:
    (invariantX428 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant1 /\ invariant30 /\ invariant87 /\ tau)
    -> invariant30'



end


theory German_baukus_hint_26

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_26:
    (invariantX512 /\ invariant31 /\ invariant59 /\ invariant87 /\ invariant188 /\ invariant225 /\ invariant796 /\ tau)
    -> invariant31'



end


theory German_baukus_hint_27

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_27:
    (invariantX465 /\ invariant31 /\ invariant59 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant796 /\ tau)
    -> invariant59'



end


theory German_baukus_hint_28

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_28:
    (invariant31 /\ invariant87 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant796 /\ tau)
    -> invariant87'



end


theory German_baukus_hint_29

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_29:
    (invariant188 /\ invariant225 /\ invariant456 /\ tau)
    -> invariant188'



end


theory German_baukus_hint_30

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_30:
    (invariantX529 /\ invariantX172 /\ invariantX88 /\ invariant188 /\ invariant225 /\ tau)
    -> invariant225'



end


theory German_baukus_hint_31

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_31:
    (invariantX529 /\ invariantX494 /\ invariantX172 /\ invariantX151 /\ invariant225 /\ invariant407 /\ invariant422 /\ tau)
    -> invariant407'



end


theory German_baukus_hint_32

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_32:
    (invariantX186 /\ invariantX117 /\ invariant422 /\ invariant528 /\ invariant530 /\ tau)
    -> invariant422'



end


theory German_baukus_hint_33

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_33:
    (invariantX88 /\ invariant31 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant565 /\ invariant796 /\ tau)
    -> invariant456'



end


theory German_baukus_hint_34

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_34:
    (invariantX399 /\ invariantX172 /\ invariantX160 /\ invariant456 /\ invariant528 /\ invariant732 /\ tau)
    -> invariant528'



end


theory German_baukus_hint_35

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_35:
    (invariantX186 /\ invariantX117 /\ invariant422 /\ invariant530 /\ invariant731 /\ invariant732 /\ tau)
    -> invariant530'



end


theory German_baukus_hint_36

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_36:
    (invariantX101 /\ invariant31 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant565 /\ invariant625 /\ invariant796 /\ tau)
    -> invariant565'



end


theory German_baukus_hint_37

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_37:
    (invariantX134 /\ invariant31 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant565 /\ invariant625 /\ invariant687 /\ invariant796 /\ tau)
    -> invariant625'



end


theory German_baukus_hint_38

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_38:
    (invariant31 /\ invariant188 /\ invariant225 /\ invariant565 /\ invariant625 /\ invariant687 /\ invariant796 /\ tau)
    -> invariant687'



end


theory German_baukus_hint_39

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_39:
    (invariantX399 /\ invariantX186 /\ invariant565 /\ invariant731 /\ invariant910 /\ tau)
    -> invariant731'



end


theory German_baukus_hint_40

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_40:
    (invariantX399 /\ invariantX186 /\ invariantX160 /\ invariant565 /\ invariant732 /\ invariant910 /\ tau)
    -> invariant732'



end


theory German_baukus_hint_41

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_41:
    (invariantX512 /\ invariant188 /\ invariant225 /\ invariant796 /\ tau)
    -> invariant796'



end


theory German_baukus_hint_42

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_42:
    (invariantX399 /\ invariantX160 /\ invariant625 /\ invariant910 /\ invariant946 /\ invariant947 /\ invariant948 /\ tau)
    -> invariant910'



end


theory German_baukus_hint_43

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_43:
    (invariantX399 /\ invariantX186 /\ invariant687 /\ invariant946 /\ invariant958 /\ tau)
    -> invariant946'



end


theory German_baukus_hint_44

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_44:
    (invariantX399 /\ invariantX186 /\ invariant687 /\ invariant947 /\ invariant974 /\ tau)
    -> invariant947'



end


theory German_baukus_hint_45

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_45:
    (invariantX399 /\ invariantX186 /\ invariant687 /\ invariant948 /\ invariant958 /\ invariant974 /\ invariant1012 /\ tau)
    -> invariant948'



end


theory German_baukus_hint_46

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_46:
    (invariantX399 /\ invariantX186 /\ invariant687 /\ invariant958 /\ tau)
    -> invariant958'



end


theory German_baukus_hint_47

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_47:
    (invariantX399 /\ invariantX186 /\ invariant687 /\ invariant958 /\ invariant974 /\ tau)
    -> invariant974'



end


theory German_baukus_hint_48

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs

lemma hint_48:
    (invariantX399 /\ invariantX186 /\ invariant687 /\ invariant958 /\ invariant974 /\ invariant1012 /\ tau)
    -> invariant1012'



end


theory German_baukus_preservation

use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
use import German_baukus_hint_48
use import German_baukus_hint_47
use import German_baukus_hint_46
use import German_baukus_hint_45
use import German_baukus_hint_44
use import German_baukus_hint_43
use import German_baukus_hint_42
use import German_baukus_hint_41
use import German_baukus_hint_40
use import German_baukus_hint_39
use import German_baukus_hint_38
use import German_baukus_hint_37
use import German_baukus_hint_36
use import German_baukus_hint_35
use import German_baukus_hint_34
use import German_baukus_hint_33
use import German_baukus_hint_32
use import German_baukus_hint_31
use import German_baukus_hint_30
use import German_baukus_hint_29
use import German_baukus_hint_28
use import German_baukus_hint_27
use import German_baukus_hint_26
use import German_baukus_hint_25
use import German_baukus_hint_24
use import German_baukus_hint_23
use import German_baukus_hint_22
use import German_baukus_hint_21
use import German_baukus_hint_20
use import German_baukus_hint_19
use import German_baukus_hint_18
use import German_baukus_hint_17
use import German_baukus_hint_16
use import German_baukus_hint_15
use import German_baukus_hint_14
use import German_baukus_hint_13
use import German_baukus_hint_12
use import German_baukus_hint_11
use import German_baukus_hint_10
use import German_baukus_hint_9
use import German_baukus_hint_8
use import German_baukus_hint_7
use import German_baukus_hint_6
use import German_baukus_hint_5
use import German_baukus_hint_4
use import German_baukus_hint_3
use import German_baukus_hint_2
use import German_baukus_hint_1

goal preservation:
    (invariantX65 /\ invariant958 /\ invariant188 /\ invariant59 /\ invariantX134 /\ invariantX199 /\ invariant565 /\ invariant948 /\ invariant1012 /\ invariant947 /\ invariant946 /\ invariantX399 /\ invariant625 /\ invariantX336 /\ invariantX465 /\ invariantX529 /\ invariant687 /\ invariantX151 /\ invariantX88 /\ invariantX217 /\ invariant422 /\ invariantX285 /\ invariant225 /\ invariantX160 /\ invariant31 /\ invariant30 /\ invariant796 /\ invariant28 /\ invariant732 /\ invariantX101 /\ invariant731 /\ invariantX40 /\ invariant87 /\ invariant407 /\ invariantX172 /\ invariantX428 /\ invariantX494 /\ invariantX238 /\ invariant530 /\ invariant528 /\ invariant910 /\ invariant974 /\ invariantX307 /\ invariantX117 /\ invariant456 /\ invariantX186 /\ invariant1 /\ invariantX512 /\ tau)
    ->
    (invariantX65' /\ invariant958' /\ invariant188' /\ invariant59' /\ invariantX134' /\ invariantX199' /\ invariant565' /\ invariant948' /\ invariant1012' /\ invariant947' /\ invariant946' /\ invariantX399' /\ invariant625' /\ invariantX336' /\ invariantX465' /\ invariantX529' /\ invariant687' /\ invariantX151' /\ invariantX88' /\ invariantX217' /\ invariant422' /\ invariantX285' /\ invariant225' /\ invariantX160' /\ invariant31' /\ invariant30' /\ invariant796' /\ invariant28' /\ invariant732' /\ invariantX101' /\ invariant731' /\ invariantX40' /\ invariant87' /\ invariant407' /\ invariantX172' /\ invariantX428' /\ invariantX494' /\ invariantX238' /\ invariant530' /\ invariant528' /\ invariant910' /\ invariant974' /\ invariantX307' /\ invariantX117' /\ invariant456' /\ invariantX186' /\ invariant1' /\ invariantX512')


end