theory German_ctc_defs
use import bool.Bool
use import int.Int
type state = Invalid | Shared | Exclusive
type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte
type data
function exgntd : bool
function curcmd : msg
function curClient : int
function memData : data
function auxData : data
function store_data : data
function exgntd' : bool
function curcmd' : msg
function curClient' : int
function memData' : data
function auxData' : data
function store_data' : data
function chan1Cmd int : msg
function chan1Data int : data
function chan2Cmd int : msg
function chan2Data int : data
function chan3Cmd int : msg
function chan3Data int : data
function cacheState int : state
function cacheData int : data
function invset int : bool
function shrset int : bool
function chan1Cmd' int : msg
function chan1Data' int : data
function chan2Cmd' int : msg
function chan2Data' int : data
function chan3Cmd' int : msg
function chan3Data' int : data
function cacheState' int : state
function cacheData' int : data
function invset' int : bool
function shrset' int : bool
end
theory German_ctc_invpreds
use import bool.Bool
use import int.Int
use import German_ctc_defs
predicate invariant129 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(chan2Cmd z2) = Gnte)
predicate invariant129' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(chan2Cmd' z2) = Gnte)
predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (cacheState z1) = Exclusive /\
(cacheState z2) <> Invalid)
predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (cacheState' z1) = Exclusive /\
(cacheState' z2) <> Invalid)
predicate invariant897 =
not (exists z1:int. exgntd = True /\
curcmd = Reqs /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheData z1) <> auxData /\
(invset z1) = True)
predicate invariant897' =
not (exists z1:int. exgntd' = True /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheData' z1) <> auxData' /\
(invset' z1) = True)
predicate invariant2 =
not (exgntd = False /\
memData <> auxData)
predicate invariant2' =
not (exgntd' = False /\
memData' <> auxData')
predicate invariant3 =
not (exists z1:int. (cacheState z1) <> Invalid /\
(cacheData z1) <> auxData)
predicate invariant3' =
not (exists z1:int. (cacheState' z1) <> Invalid /\
(cacheData' z1) <> auxData')
predicate invariantX123 =
not (exists z1:int. (chan3Cmd z1) = Invack /\
(cacheState z1) = Exclusive)
predicate invariantX123' =
not (exists z1:int. (chan3Cmd' z1) = Invack /\
(cacheState' z1) = Exclusive)
predicate invariantX505 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z2) = Inv /\
(cacheState z1) = Exclusive)
predicate invariantX505' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z2) = Inv /\
(cacheState' z1) = Exclusive)
predicate invariant776 =
not (exists z1:int. exgntd = True /\
curcmd <> Empty /\
(chan2Cmd z1) = Inv /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheData z1) <> auxData)
predicate invariant776' =
not (exists z1:int. exgntd' = True /\
curcmd' <> Empty /\
(chan2Cmd' z1) = Inv /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheData' z1) <> auxData')
predicate invariant777 =
not (exists z1:int. exgntd = True /\
curcmd <> Empty /\
(chan2Cmd z1) = Inv /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive)
predicate invariant777' =
not (exists z1:int. exgntd' = True /\
curcmd' <> Empty /\
(chan2Cmd' z1) = Inv /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive)
predicate invariantX247 =
not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan3Cmd z1) = Invack)
predicate invariantX247' =
not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan3Cmd' z1) = Invack)
predicate invariantX371 =
not (exists z1:int. (chan2Cmd z1) = Inv /\
(invset z1) = True)
predicate invariantX371' =
not (exists z1:int. (chan2Cmd' z1) = Inv /\
(invset' z1) = True)
predicate invariant911 =
not (exists z1:int. exgntd = True /\
curcmd = Reqe /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(invset z1) = True)
predicate invariant911' =
not (exists z1:int. exgntd' = True /\
curcmd' = Reqe /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(invset' z1) = True)
predicate invariant913 =
not (exists z1:int. exgntd = True /\
curcmd = Reqs /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(invset z1) = True)
predicate invariant913' =
not (exists z1:int. exgntd' = True /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(invset' z1) = True)
predicate invariantX111 =
not (exists z1:int. (chan2Cmd z1) = Gnte /\
(cacheState z1) = Exclusive)
predicate invariantX111' =
not (exists z1:int. (chan2Cmd' z1) = Gnte /\
(cacheState' z1) = Exclusive)
predicate invariant1298 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z2) = Empty /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(cacheState z2) = Invalid /\
(shrset z1) = True)
predicate invariant1298' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z2) = Empty /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(cacheState' z2) = Invalid /\
(shrset' z1) = True)
predicate invariant1042 =
not (exists z1:int. exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Reqe /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheData z1) <> auxData /\
(shrset z1) = True)
predicate invariant1042' =
not (exists z1:int. exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Reqe /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheData' z1) <> auxData' /\
(shrset' z1) = True)
predicate invariant661 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z2) = Invack /\
(invset z1) = True)
predicate invariant661' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z2) = Invack /\
(invset' z1) = True)
predicate invariantX490 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(chan2Cmd z2) = Inv)
predicate invariantX490' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(chan2Cmd' z2) = Inv)
predicate invariantX362 =
not (exists z1:int. (chan3Cmd z1) = Invack /\
(invset z1) = True)
predicate invariantX362' =
not (exists z1:int. (chan3Cmd' z1) = Invack /\
(invset' z1) = True)
predicate invariant663 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan2Cmd z1) = Inv /\
(chan2Cmd z2) = Inv /\
(chan3Cmd z2) = Empty)
predicate invariant663' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan2Cmd' z1) = Inv /\
(chan2Cmd' z2) = Inv /\
(chan3Cmd' z2) = Empty)
predicate invariantX871 =
not (exists z1 z2:int. z1 <> z2 /\ (cacheState z1) = Exclusive /\
(shrset z2) = True)
predicate invariantX871' =
not (exists z1 z2:int. z1 <> z2 /\ (cacheState' z1) = Exclusive /\
(shrset' z2) = True)
predicate invariantX231 =
not (exists z1:int. (chan3Cmd z1) = Invack /\
(shrset z1) = False)
predicate invariantX231' =
not (exists z1:int. (chan3Cmd' z1) = Invack /\
(shrset' z1) = False)
predicate invariantX102 =
not (exists z1:int. (chan2Cmd z1) = Gnts /\
(cacheState z1) = Exclusive)
predicate invariantX102' =
not (exists z1:int. (chan2Cmd' z1) = Gnts /\
(cacheState' z1) = Exclusive)
predicate invariant798 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Inv /\
(chan3Cmd z2) = Empty /\
(invset z1) = True)
predicate invariant798' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Inv /\
(chan3Cmd' z2) = Empty /\
(invset' z1) = True)
predicate invariant1055 =
not (exists z1:int. exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Reqs /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheData z1) <> auxData /\
(shrset z1) = True)
predicate invariant1055' =
not (exists z1:int. exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheData' z1) <> auxData' /\
(shrset' z1) = True)
predicate invariant32 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z2) = Gnts /\
(cacheState z1) = Exclusive)
predicate invariant32' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z2) = Gnts /\
(cacheState' z1) = Exclusive)
predicate invariant1314 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z2) = Empty /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(cacheState z2) <> Exclusive /\
(shrset z1) = True)
predicate invariant1314' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z2) = Empty /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(cacheState' z2) <> Exclusive /\
(shrset' z1) = True)
predicate invariant930 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(invset z1) = True /\
(invset z2) = True)
predicate invariant930' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(invset' z1) = True /\
(invset' z2) = True)
predicate invariant34 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z2) = Gnte /\
(cacheState z1) = Exclusive)
predicate invariant34' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z2) = Gnte /\
(cacheState' z1) = Exclusive)
predicate invariant35 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(cacheState z2) <> Invalid)
predicate invariant35' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(cacheState' z2) <> Invalid)
predicate invariantX348 =
not (exists z1:int. curcmd = Empty /\
(chan2Cmd z1) = Inv)
predicate invariantX348' =
not (exists z1:int. curcmd' = Empty /\
(chan2Cmd' z1) = Inv)
predicate invariant1190 =
not (exists z1:int. exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Empty /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(shrset z1) = True)
predicate invariant1190' =
not (exists z1:int. exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Empty /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(shrset' z1) = True)
predicate invariant294 =
not (exists z1:int. (chan2Cmd z1) = Gnte /\
(shrset z1) = False)
predicate invariant294' =
not (exists z1:int. (chan2Cmd' z1) = Gnte /\
(shrset' z1) = False)
predicate invariantX601 =
not (exists z1:int. exgntd = True /\
(chan2Cmd z1) = Gnts)
predicate invariantX601' =
not (exists z1:int. exgntd' = True /\
(chan2Cmd' z1) = Gnts)
predicate invariantX88 =
not (exists z1:int. (cacheState z1) <> Invalid /\
(shrset z1) = False)
predicate invariantX88' =
not (exists z1:int. (cacheState' z1) <> Invalid /\
(shrset' z1) = False)
predicate invariant554 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan2Cmd z1) = Inv /\
(chan3Cmd z2) = Invack)
predicate invariant554' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan2Cmd' z1) = Inv /\
(chan3Cmd' z2) = Invack)
predicate invariantX854 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(shrset z2) = True)
predicate invariantX854' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(shrset' z2) = True)
predicate invariant1068 =
not (exists z1:int. exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Reqe /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(shrset z1) = True)
predicate invariant1068' =
not (exists z1:int. exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Reqe /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(shrset' z1) = True)
predicate invariant1069 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z2) = Reqe /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(shrset z1) = True)
predicate invariant1069' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z2) = Reqe /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(shrset' z1) = True)
predicate invariant46 =
not (exists z1:int. exgntd = True /\
curcmd <> Empty /\
(chan3Cmd z1) = Invack /\
(chan3Data z1) <> auxData)
predicate invariant46' =
not (exists z1:int. exgntd' = True /\
curcmd' <> Empty /\
(chan3Cmd' z1) = Invack /\
(chan3Data' z1) <> auxData')
predicate invariantX338 =
not (exists z1:int. (chan2Cmd z1) = Inv /\
(chan3Cmd z1) = Invack)
predicate invariantX338' =
not (exists z1:int. (chan2Cmd' z1) = Inv /\
(chan3Cmd' z1) = Invack)
predicate invariantX208 =
not (exists z1:int. (chan2Cmd z1) = Gnts /\
(chan3Cmd z1) = Invack)
predicate invariantX208' =
not (exists z1:int. (chan2Cmd' z1) = Gnts /\
(chan3Cmd' z1) = Invack)
predicate invariant819 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2Cmd z1) = Inv /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(invset z2) = True)
predicate invariant819' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Inv /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(invset' z2) = True)
predicate invariant1207 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z2) = Empty /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(cacheState z2) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1207' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z2) = Empty /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(cacheState' z2) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant1080 =
not (exists z1:int. exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Reqs /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(shrset z1) = True)
predicate invariant1080' =
not (exists z1:int. exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(shrset' z1) = True)
predicate invariant1081 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z2) = Reqs /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheState z1) <> Exclusive /\
(shrset z1) = True)
predicate invariant1081' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z2) = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheState' z1) <> Exclusive /\
(shrset' z1) = True)
predicate invariantX321 =
not (exists z1:int. (invset z1) = True /\
(shrset z1) = False)
predicate invariantX321' =
not (exists z1:int. (invset' z1) = True /\
(shrset' z1) = False)
predicate invariant69 =
not (exists z1:int. (chan2Cmd z1) = Gnts /\
(chan2Data z1) <> auxData)
predicate invariant69' =
not (exists z1:int. (chan2Cmd' z1) = Gnts /\
(chan2Data' z1) <> auxData')
predicate invariant71 =
not (exists z1:int. (chan2Cmd z1) = Gnte /\
(chan2Data z1) <> auxData)
predicate invariant71' =
not (exists z1:int. (chan2Cmd' z1) = Gnte /\
(chan2Data' z1) <> auxData')
predicate invariantX185 =
not (exists z1:int. (chan3Cmd z1) = Invack /\
(cacheState z1) <> Invalid)
predicate invariantX185' =
not (exists z1:int. (chan3Cmd' z1) = Invack /\
(cacheState' z1) <> Invalid)
predicate invariant1224 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Empty /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(cacheState z1) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1224' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Empty /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(cacheState' z1) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant1096 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z2) = Reqs /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1096' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z2) = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant1097 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z1) = Reqs /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1097' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z1) = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant1098 =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z3) = Reqs /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1098' =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z3) = Reqs /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariantX684 =
not (exists z1 z2:int. z1 <> z2 /\ (cacheState z1) = Exclusive /\
(invset z2) = True)
predicate invariantX684' =
not (exists z1 z2:int. z1 <> z2 /\ (cacheState' z1) = Exclusive /\
(invset' z2) = True)
predicate invariantX428 =
not (exists z1 z2:int. z1 <> z2 /\ (chan3Cmd z2) = Invack /\
(cacheState z1) = Exclusive)
predicate invariantX428' =
not (exists z1 z2:int. z1 <> z2 /\ (chan3Cmd' z2) = Invack /\
(cacheState' z1) = Exclusive)
predicate invariantX41 =
not (exists z1:int. exgntd = False /\
(cacheState z1) = Exclusive)
predicate invariantX41' =
not (exists z1:int. exgntd' = False /\
(cacheState' z1) = Exclusive)
predicate invariantX296 =
not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan2Cmd z1) = Inv)
predicate invariantX296' =
not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan2Cmd' z1) = Inv)
predicate invariant218 =
not (exists z1:int. exgntd = False /\
(chan2Cmd z1) = Gnte)
predicate invariant218' =
not (exists z1:int. exgntd' = False /\
(chan2Cmd' z1) = Gnte)
predicate invariant351 =
not (exists z1:int. (chan2Cmd z1) = Gnte /\
(chan3Cmd z1) = Invack)
predicate invariant351' =
not (exists z1:int. (chan2Cmd' z1) = Gnte /\
(chan3Cmd' z1) = Invack)
predicate invariantX415 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(chan3Cmd z2) = Invack)
predicate invariantX415' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(chan3Cmd' z2) = Invack)
predicate invariantX158 =
not (exists z1:int. (chan2Cmd z1) = Gnts /\
(shrset z1) = False)
predicate invariantX158' =
not (exists z1:int. (chan2Cmd' z1) = Gnts /\
(shrset' z1) = False)
predicate invariantX285 =
not (exists z1:int. curcmd = Empty /\
(chan3Cmd z1) = Invack)
predicate invariantX285' =
not (exists z1:int. curcmd' = Empty /\
(chan3Cmd' z1) = Invack)
predicate invariant100 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(chan2Cmd z2) = Gnts)
predicate invariant100' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(chan2Cmd' z2) = Gnts)
predicate invariantX659 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd z1) = Gnte /\
(invset z2) = True)
predicate invariantX659' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2Cmd' z1) = Gnte /\
(invset' z2) = True)
predicate invariant502 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan3Cmd z1) = Invack /\
(chan3Cmd z2) = Invack)
predicate invariant502' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan3Cmd' z1) = Invack /\
(chan3Cmd' z2) = Invack)
predicate invariantX265 =
not (exists z1:int. (chan2Cmd z1) = Inv /\
(shrset z1) = False)
predicate invariantX265' =
not (exists z1:int. (chan2Cmd' z1) = Inv /\
(shrset' z1) = False)
predicate invariant1278 =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1Cmd z3) = Empty /\
(chan2Cmd z1) = Empty /\
(chan2Cmd z2) = Empty /\
(chan3Cmd z2) = Empty /\
(cacheState z3) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1278' =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1Cmd' z3) = Empty /\
(chan2Cmd' z1) = Empty /\
(chan2Cmd' z2) = Empty /\
(chan3Cmd' z2) = Empty /\
(cacheState' z3) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant895 =
not (exists z1:int. exgntd = True /\
curcmd = Reqe /\
(chan2Cmd z1) = Empty /\
(chan3Cmd z1) = Empty /\
(chan3Data z1) <> auxData /\
(cacheData z1) <> auxData /\
(invset z1) = True)
predicate invariant895' =
not (exists z1:int. exgntd' = True /\
curcmd' = Reqe /\
(chan2Cmd' z1) = Empty /\
(chan3Cmd' z1) = Empty /\
(chan3Data' z1) <> auxData' /\
(cacheData' z1) <> auxData' /\
(invset' z1) = True)
end
theory German_ctc_trdefs
use import bool.Bool
use import int.Int
use import German_ctc_defs
predicate transition__sendGnts =
(exists i:int.
(
exgntd = False /\
curcmd = Reqs /\
curClient = i /\
(chan2Cmd i) = Empty) /\
(
curcmd' = Empty /\
exgntd' = exgntd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j12:int.
(if _j12 = i then
(chan2Cmd' _j12) = Gnts
else (chan2Cmd' _j12) = (chan2Cmd _j12))) /\
(forall _j13:int.
(if _j13 = i then
(chan2Data' _j13) = memData
else (chan2Data' _j13) = (chan2Data _j13))) /\
(forall _j14:int.
(if _j14 = i then
(shrset' _j14) = True
else (shrset' _j14) = (shrset _j14))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. invset' z1 = invset z1) ))
predicate transition__recvGnte =
(exists i:int.
(
(chan2Cmd i) = Gnte) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j21:int.
(if _j21 = i then
(cacheState' _j21) = Exclusive
else (cacheState' _j21) = (cacheState _j21))) /\
(forall _j22:int.
(if _j22 = i then
(cacheData' _j22) = (chan2Data i)
else (cacheData' _j22) = (cacheData _j22))) /\
(forall _j23:int.
(if _j23 = i then
(chan2Cmd' _j23) = Empty
else (chan2Cmd' _j23) = (chan2Cmd _j23))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recvInvack =
(exists i:int.
(
curcmd <> Empty /\
(chan3Cmd i) = Invack) /\
(
exgntd' = False /\
(if exgntd = True then
memData' = (chan3Data i)
else memData' = memData) /\
curcmd' = curcmd /\
curClient' = curClient /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j10:int.
(if _j10 = i then
(chan3Cmd' _j10) = Empty
else (chan3Cmd' _j10) = (chan3Cmd _j10))) /\
(forall _j11:int.
(if _j11 = i then
(shrset' _j11) = False
else (shrset' _j11) = (shrset _j11))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Cmd' z1 = chan2Cmd z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. invset' z1 = invset z1) ))
predicate transition__sendInv =
(exists i:int.
(
curcmd = Reqe /\
(chan2Cmd i) = Empty /\
(invset i) = True) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j5:int.
(if _j5 = i then
(chan2Cmd' _j5) = Inv
else (chan2Cmd' _j5) = (chan2Cmd _j5))) /\
(forall _j6:int.
(if _j6 = i then
(invset' _j6) = False
else (invset' _j6) = (invset _j6))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recvReqe =
(exists i:int.
(
curcmd = Empty /\
(chan1Cmd i) = Reqe) /\
(
curcmd' = Reqe /\
curClient' = i /\
exgntd' = exgntd /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j4:int.
(if _j4 = i then
(chan1Cmd' _j4) = Empty
else (chan1Cmd' _j4) = (chan1Cmd _j4))) /\
(forall j:int.
(invset' j) = (shrset j)) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Cmd' z1 = chan2Cmd z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recvReqs =
(exists i:int.
(
curcmd = Empty /\
(chan1Cmd i) = Reqs) /\
(
curcmd' = Reqs /\
curClient' = i /\
exgntd' = exgntd /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j3:int.
(if _j3 = i then
(chan1Cmd' _j3) = Empty
else (chan1Cmd' _j3) = (chan1Cmd _j3))) /\
(forall j:int.
(invset' j) = (shrset j)) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Cmd' z1 = chan2Cmd z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__sendGnte =
(exists i:int.
(
exgntd = False /\
curcmd = Reqe /\
curClient = i /\
(chan2Cmd i) = Empty /\
(shrset i) = False
/\ (forall j:int.i = j \/
((shrset j) = False))
) /\
(
curcmd' = Empty /\
exgntd' = True /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j15:int.
(if _j15 = i then
(chan2Cmd' _j15) = Gnte
else (chan2Cmd' _j15) = (chan2Cmd _j15))) /\
(forall _j16:int.
(if _j16 = i then
(chan2Data' _j16) = memData
else (chan2Data' _j16) = (chan2Data _j16))) /\
(forall _j17:int.
(if _j17 = i then
(shrset' _j17) = True
else (shrset' _j17) = (shrset _j17))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. invset' z1 = invset z1) ))
predicate transition__sendReqe =
(exists i:int.
(
(chan1Cmd i) = Empty /\
(cacheState i) <> Exclusive) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j2:int.
(if _j2 = i then
(chan1Cmd' _j2) = Reqe
else (chan1Cmd' _j2) = (chan1Cmd _j2))) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Cmd' z1 = chan2Cmd z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__sendReqs =
(exists i:int.
(
(chan1Cmd i) = Empty /\
(cacheState i) = Invalid) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j1:int.
(if _j1 = i then
(chan1Cmd' _j1) = Reqs
else (chan1Cmd' _j1) = (chan1Cmd _j1))) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Cmd' z1 = chan2Cmd z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__sendInv_ =
(exists i:int.
(
exgntd = True /\
curcmd = Reqs /\
(chan2Cmd i) = Empty /\
(invset i) = True) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j5:int.
(if _j5 = i then
(chan2Cmd' _j5) = Inv
else (chan2Cmd' _j5) = (chan2Cmd _j5))) /\
(forall _j6:int.
(if _j6 = i then
(invset' _j6) = False
else (invset' _j6) = (invset _j6))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__store =
(exists n:int.
(
(cacheState n) = Exclusive) /\
(
auxData' = store_data /\
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
store_data' = store_data /\
(forall j:int.
(if j = n then
(cacheData' j) = store_data
else (cacheData' j) = (cacheData j))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Cmd' z1 = chan2Cmd z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. cacheState' z1 = cacheState z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recvGnts =
(exists i:int.
(
(chan2Cmd i) = Gnts) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j18:int.
(if _j18 = i then
(cacheState' _j18) = Shared
else (cacheState' _j18) = (cacheState _j18))) /\
(forall _j19:int.
(if _j19 = i then
(cacheData' _j19) = (chan2Data i)
else (cacheData' _j19) = (cacheData _j19))) /\
(forall _j20:int.
(if _j20 = i then
(chan2Cmd' _j20) = Empty
else (chan2Cmd' _j20) = (chan2Cmd _j20))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. chan3Cmd' z1 = chan3Cmd z1) /\
(forall z1:int. chan3Data' z1 = chan3Data z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__sendInvack =
(exists i:int.
(
(chan2Cmd i) = Inv /\
(chan3Cmd i) = Empty) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
memData' = memData /\
auxData' = auxData /\
store_data' = store_data /\
(forall _j7:int.
(if _j7 = i then
(chan2Cmd' _j7) = Empty
else (chan2Cmd' _j7) = (chan2Cmd _j7))) /\
(forall _j8:int.
(if _j8 = i then
(chan3Cmd' _j8) = Invack
else (chan3Cmd' _j8) = (chan3Cmd _j8))) /\
(forall j:int.
(if j = i /\
(cacheState i) = Exclusive then
(chan3Data' j) = (cacheData i)
else (chan3Data' j) = (chan3Data j))) /\
(forall _j9:int.
(if _j9 = i then
(cacheState' _j9) = Invalid
else (cacheState' _j9) = (cacheState _j9))) /\
(forall z1:int. chan1Cmd' z1 = chan1Cmd z1) /\
(forall z1:int. chan1Data' z1 = chan1Data z1) /\
(forall z1:int. chan2Data' z1 = chan2Data z1) /\
(forall z1:int. cacheData' z1 = cacheData z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate tau =
(transition__sendInvack \/ transition__recvGnts \/ transition__store \/ transition__sendInv_ \/ transition__sendReqs \/ transition__sendReqe \/ transition__sendGnte \/ transition__recvReqs \/ transition__recvReqe \/ transition__sendInv \/ transition__recvInvack \/ transition__recvGnte \/ transition__sendGnts)
end
theory German_ctc_initialisation
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
predicate init =
forall z:int. (exgntd = False /\
curcmd = Empty /\
memData = auxData /\
(chan1Cmd z) = Empty /\
(chan2Cmd z) = Empty /\
(chan3Cmd z) = Empty /\
(cacheState z) = Invalid /\
(invset z) = False /\
(shrset z) = False)
goal initialisation:
init -> (invariant895 /\ invariant1278 /\ invariantX265 /\ invariant502 /\ invariantX659 /\ invariant100 /\ invariantX285 /\ invariantX158 /\ invariantX415 /\ invariant351 /\ invariant218 /\ invariantX296 /\ invariantX41 /\ invariantX428 /\ invariantX684 /\ invariant1098 /\ invariant1097 /\ invariant1096 /\ invariant1224 /\ invariantX185 /\ invariant71 /\ invariant69 /\ invariantX321 /\ invariant1081 /\ invariant1080 /\ invariant1207 /\ invariant819 /\ invariantX208 /\ invariantX338 /\ invariant46 /\ invariant1069 /\ invariant1068 /\ invariantX854 /\ invariant554 /\ invariantX88 /\ invariantX601 /\ invariant294 /\ invariant1190 /\ invariantX348 /\ invariant35 /\ invariant34 /\ invariant930 /\ invariant1314 /\ invariant32 /\ invariant1055 /\ invariant798 /\ invariantX102 /\ invariantX231 /\ invariantX871 /\ invariant663 /\ invariantX362 /\ invariantX490 /\ invariant661 /\ invariant1042 /\ invariant1298 /\ invariantX111 /\ invariant913 /\ invariant911 /\ invariantX371 /\ invariantX247 /\ invariant777 /\ invariant776 /\ invariantX505 /\ invariantX123 /\ invariant3 /\ invariant2 /\ invariant897 /\ invariant1 /\ invariant129)
end
theory German_ctc_property
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
goal property:
(invariant895 /\ invariant1278 /\ invariantX265 /\ invariant502 /\ invariantX659 /\ invariant100 /\ invariantX285 /\ invariantX158 /\ invariantX415 /\ invariant351 /\ invariant218 /\ invariantX296 /\ invariantX41 /\ invariantX428 /\ invariantX684 /\ invariant1098 /\ invariant1097 /\ invariant1096 /\ invariant1224 /\ invariantX185 /\ invariant71 /\ invariant69 /\ invariantX321 /\ invariant1081 /\ invariant1080 /\ invariant1207 /\ invariant819 /\ invariantX208 /\ invariantX338 /\ invariant46 /\ invariant1069 /\ invariant1068 /\ invariantX854 /\ invariant554 /\ invariantX88 /\ invariantX601 /\ invariant294 /\ invariant1190 /\ invariantX348 /\ invariant35 /\ invariant34 /\ invariant930 /\ invariant1314 /\ invariant32 /\ invariant1055 /\ invariant798 /\ invariantX102 /\ invariantX231 /\ invariantX871 /\ invariant663 /\ invariantX362 /\ invariantX490 /\ invariant661 /\ invariant1042 /\ invariant1298 /\ invariantX111 /\ invariant913 /\ invariant911 /\ invariantX371 /\ invariantX247 /\ invariant777 /\ invariant776 /\ invariantX505 /\ invariantX123 /\ invariant3 /\ invariant2 /\ invariant897 /\ invariant1 /\ invariant129) -> (not (exists z1 z2:int. z1 <> z2 /\ (cacheState z1) = Exclusive /\
(cacheState z2) <> Invalid) /\
not (exgntd = False /\
memData <> auxData) /\
not (exists z1:int. (cacheState z1) <> Invalid /\
(cacheData z1) <> auxData))
end
theory German_ctc_hint_1
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_1:
(invariantX871 /\ invariantX854 /\ invariantX684 /\ invariantX505 /\ invariantX123 /\ invariantX41 /\ tau)
-> invariantX871'
end
theory German_ctc_hint_2
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_2:
(invariantX854 /\ invariantX659 /\ invariantX490 /\ invariantX111 /\ invariant218 /\ invariant351 /\ tau)
-> invariantX854'
end
theory German_ctc_hint_3
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_3:
(invariantX871 /\ invariantX684 /\ invariantX659 /\ invariantX505 /\ invariantX428 /\ invariantX123 /\ invariantX41 /\ tau)
-> invariantX684'
end
theory German_ctc_hint_4
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_4:
(invariantX854 /\ invariantX659 /\ invariantX490 /\ invariantX415 /\ invariantX321 /\ invariantX111 /\ invariant218 /\ invariant351 /\ tau)
-> invariantX659'
end
theory German_ctc_hint_5
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_5:
(invariantX601 /\ invariantX158 /\ invariantX102 /\ tau)
-> invariantX601'
end
theory German_ctc_hint_6
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_6:
(invariantX684 /\ invariantX505 /\ invariantX490 /\ invariantX428 /\ invariantX123 /\ invariantX41 /\ tau)
-> invariantX505'
end
theory German_ctc_hint_7
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_7:
(invariantX659 /\ invariantX490 /\ invariantX415 /\ invariantX265 /\ invariantX111 /\ invariant218 /\ invariant351 /\ tau)
-> invariantX490'
end
theory German_ctc_hint_8
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_8:
(invariantX505 /\ invariantX428 /\ invariantX415 /\ invariantX123 /\ invariantX41 /\ tau)
-> invariantX428'
end
theory German_ctc_hint_9
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_9:
(invariantX490 /\ invariantX415 /\ invariantX231 /\ invariantX111 /\ invariant218 /\ invariant351 /\ tau)
-> invariantX415'
end
theory German_ctc_hint_10
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_10:
(invariantX371 /\ invariantX348 /\ invariantX338 /\ invariantX265 /\ tau)
-> invariantX371'
end
theory German_ctc_hint_11
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_11:
(invariantX371 /\ invariantX362 /\ invariantX285 /\ invariantX231 /\ invariantX208 /\ invariantX123 /\ tau)
-> invariantX362'
end
theory German_ctc_hint_12
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_12:
(invariantX348 /\ invariantX296 /\ invariantX265 /\ tau)
-> invariantX348'
end
theory German_ctc_hint_13
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_13:
(invariantX362 /\ invariantX338 /\ invariantX285 /\ invariantX231 /\ invariantX123 /\ tau)
-> invariantX338'
end
theory German_ctc_hint_14
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_14:
(invariantX362 /\ invariantX321 /\ invariantX265 /\ invariantX158 /\ invariantX88 /\ tau)
-> invariantX321'
end
theory German_ctc_hint_15
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_15:
(invariantX348 /\ invariantX338 /\ invariantX296 /\ invariantX41 /\ invariant554 /\ tau)
-> invariantX296'
end
theory German_ctc_hint_16
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_16:
(invariantX348 /\ invariantX285 /\ invariantX247 /\ invariantX231 /\ invariantX208 /\ invariantX123 /\ tau)
-> invariantX285'
end
theory German_ctc_hint_17
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_17:
(invariantX338 /\ invariantX321 /\ invariantX265 /\ invariantX88 /\ tau)
-> invariantX265'
end
theory German_ctc_hint_18
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_18:
(invariantX296 /\ invariantX285 /\ invariantX247 /\ invariantX208 /\ invariantX41 /\ invariant218 /\ invariant502 /\ tau)
-> invariantX247'
end
theory German_ctc_hint_19
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_19:
(invariantX265 /\ invariantX231 /\ invariantX158 /\ invariantX88 /\ tau)
-> invariantX231'
end
theory German_ctc_hint_20
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_20:
(invariantX247 /\ invariantX208 /\ invariantX158 /\ invariantX102 /\ tau)
-> invariantX208'
end
theory German_ctc_hint_21
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_21:
(invariantX208 /\ invariantX185 /\ invariantX123 /\ invariantX88 /\ invariant351 /\ tau)
-> invariantX185'
end
theory German_ctc_hint_22
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_22:
(invariantX208 /\ invariantX158 /\ invariantX88 /\ tau)
-> invariantX158'
end
theory German_ctc_hint_23
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_23:
(invariantX123 /\ invariantX41 /\ invariant351 /\ tau)
-> invariantX123'
end
theory German_ctc_hint_24
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_24:
(invariantX111 /\ invariantX41 /\ tau)
-> invariantX111'
end
theory German_ctc_hint_25
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_25:
(invariantX102 /\ invariantX41 /\ tau)
-> invariantX102'
end
theory German_ctc_hint_26
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_26:
(invariantX185 /\ invariantX158 /\ invariantX88 /\ invariant294 /\ tau)
-> invariantX88'
end
theory German_ctc_hint_27
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_27:
(invariantX428 /\ invariantX123 /\ invariantX41 /\ invariant218 /\ tau)
-> invariantX41'
end
theory German_ctc_hint_28
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_28:
(invariantX684 /\ invariantX428 /\ invariantX123 /\ invariantX41 /\ invariant1 /\ invariant32 /\ invariant34 /\ invariant35 /\ tau)
-> invariant1'
end
theory German_ctc_hint_29
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_29:
(invariantX41 /\ invariant2 /\ invariant46 /\ invariant218 /\ tau)
-> invariant2'
end
theory German_ctc_hint_30
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_30:
(invariantX871 /\ invariantX185 /\ invariantX88 /\ invariant3 /\ invariant69 /\ invariant71 /\ tau)
-> invariant3'
end
theory German_ctc_hint_31
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_31:
(invariantX428 /\ invariantX123 /\ invariantX41 /\ invariant1 /\ invariant32 /\ invariant100 /\ tau)
-> invariant32'
end
theory German_ctc_hint_32
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_32:
(invariantX428 /\ invariantX123 /\ invariantX41 /\ invariant1 /\ invariant34 /\ invariant129 /\ tau)
-> invariant34'
end
theory German_ctc_hint_33
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_33:
(invariantX659 /\ invariantX415 /\ invariantX111 /\ invariantX88 /\ invariant35 /\ invariant100 /\ invariant129 /\ invariant218 /\ invariant351 /\ tau)
-> invariant35'
end
theory German_ctc_hint_34
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_34:
(invariantX428 /\ invariantX362 /\ invariantX285 /\ invariantX208 /\ invariantX123 /\ invariant3 /\ invariant46 /\ invariant351 /\ invariant776 /\ invariant777 /\ tau)
-> invariant46'
end
theory German_ctc_hint_35
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_35:
(invariantX601 /\ invariantX208 /\ invariantX158 /\ invariantX102 /\ invariantX41 /\ invariant2 /\ invariant69 /\ tau)
-> invariant69'
end
theory German_ctc_hint_36
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_36:
(invariantX111 /\ invariant2 /\ invariant35 /\ invariant71 /\ tau)
-> invariant71'
end
theory German_ctc_hint_37
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_37:
(invariantX415 /\ invariantX158 /\ invariantX111 /\ invariant35 /\ invariant100 /\ invariant218 /\ invariant351 /\ tau)
-> invariant100'
end
theory German_ctc_hint_38
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_38:
(invariantX415 /\ invariantX111 /\ invariant35 /\ invariant129 /\ invariant218 /\ invariant351 /\ tau)
-> invariant129'
end
theory German_ctc_hint_39
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_39:
(invariantX415 /\ invariantX41 /\ invariant218 /\ invariant351 /\ tau)
-> invariant218'
end
theory German_ctc_hint_40
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_40:
(invariantX88 /\ invariant218 /\ invariant294 /\ invariant351 /\ tau)
-> invariant294'
end
theory German_ctc_hint_41
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_41:
(invariantX285 /\ invariantX231 /\ invariantX111 /\ invariant218 /\ invariant351 /\ tau)
-> invariant351'
end
theory German_ctc_hint_42
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_42:
(invariantX362 /\ invariantX285 /\ invariantX208 /\ invariantX123 /\ invariant351 /\ invariant502 /\ invariant554 /\ tau)
-> invariant502'
end
theory German_ctc_hint_43
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_43:
(invariantX428 /\ invariantX348 /\ invariantX338 /\ invariant554 /\ invariant661 /\ invariant663 /\ tau)
-> invariant554'
end
theory German_ctc_hint_44
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_44:
(invariantX601 /\ invariantX428 /\ invariantX415 /\ invariantX371 /\ invariantX285 /\ invariant661 /\ invariant798 /\ tau)
-> invariant661'
end
theory German_ctc_hint_45
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_45:
(invariantX505 /\ invariantX348 /\ invariantX338 /\ invariant554 /\ invariant663 /\ invariant798 /\ invariant819 /\ tau)
-> invariant663'
end
theory German_ctc_hint_46
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_46:
(invariantX505 /\ invariantX348 /\ invariant776 /\ invariant895 /\ invariant897 /\ tau)
-> invariant776'
end
theory German_ctc_hint_47
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_47:
(invariantX505 /\ invariantX348 /\ invariant777 /\ invariant911 /\ invariant913 /\ tau)
-> invariant777'
end
theory German_ctc_hint_48
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_48:
(invariantX601 /\ invariantX505 /\ invariantX490 /\ invariantX371 /\ invariantX348 /\ invariant798 /\ invariant930 /\ tau)
-> invariant798'
end
theory German_ctc_hint_49
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_49:
(invariantX684 /\ invariantX601 /\ invariantX490 /\ invariantX348 /\ invariant819 /\ invariant930 /\ tau)
-> invariant819'
end
theory German_ctc_hint_50
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_50:
(invariantX684 /\ invariantX601 /\ invariant3 /\ invariant71 /\ invariant895 /\ invariant1042 /\ invariant1069 /\ tau)
-> invariant895'
end
theory German_ctc_hint_51
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_51:
(invariantX684 /\ invariantX601 /\ invariant3 /\ invariant71 /\ invariant897 /\ invariant1055 /\ invariant1081 /\ tau)
-> invariant897'
end
theory German_ctc_hint_52
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_52:
(invariantX684 /\ invariantX601 /\ invariant911 /\ invariant1068 /\ invariant1069 /\ tau)
-> invariant911'
end
theory German_ctc_hint_53
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_53:
(invariantX684 /\ invariantX601 /\ invariant913 /\ invariant1080 /\ invariant1081 /\ tau)
-> invariant913'
end
theory German_ctc_hint_54
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_54:
(invariantX684 /\ invariantX659 /\ invariantX601 /\ invariantX371 /\ invariant930 /\ invariant1096 /\ invariant1097 /\ invariant1098 /\ tau)
-> invariant930'
end
theory German_ctc_hint_55
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_55:
(invariantX871 /\ invariantX601 /\ invariant71 /\ invariant1042 /\ invariant1190 /\ tau)
-> invariant1042'
end
theory German_ctc_hint_56
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_56:
(invariantX871 /\ invariantX601 /\ invariant71 /\ invariant1055 /\ invariant1190 /\ tau)
-> invariant1055'
end
theory German_ctc_hint_57
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_57:
(invariantX871 /\ invariantX601 /\ invariant1068 /\ invariant1190 /\ tau)
-> invariant1068'
end
theory German_ctc_hint_58
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_58:
(invariantX871 /\ invariantX601 /\ invariant1069 /\ invariant1190 /\ invariant1314 /\ tau)
-> invariant1069'
end
theory German_ctc_hint_59
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_59:
(invariantX871 /\ invariantX601 /\ invariant1080 /\ invariant1190 /\ tau)
-> invariant1080'
end
theory German_ctc_hint_60
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_60:
(invariantX871 /\ invariantX601 /\ invariant1081 /\ invariant1190 /\ invariant1298 /\ tau)
-> invariant1081'
end
theory German_ctc_hint_61
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_61:
(invariantX871 /\ invariantX854 /\ invariantX601 /\ invariantX348 /\ invariant1096 /\ invariant1207 /\ tau)
-> invariant1096'
end
theory German_ctc_hint_62
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_62:
(invariantX871 /\ invariantX854 /\ invariantX601 /\ invariantX348 /\ invariant1097 /\ invariant1224 /\ tau)
-> invariant1097'
end
theory German_ctc_hint_63
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_63:
(invariantX871 /\ invariantX854 /\ invariantX601 /\ invariantX348 /\ invariant1098 /\ invariant1207 /\ invariant1224 /\ invariant1278 /\ tau)
-> invariant1098'
end
theory German_ctc_hint_64
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_64:
(invariantX871 /\ invariantX601 /\ invariant1190 /\ tau)
-> invariant1190'
end
theory German_ctc_hint_65
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_65:
(invariantX871 /\ invariantX854 /\ invariantX601 /\ invariantX348 /\ invariant1207 /\ tau)
-> invariant1207'
end
theory German_ctc_hint_66
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_66:
(invariantX854 /\ invariantX601 /\ invariantX348 /\ invariant1207 /\ invariant1224 /\ tau)
-> invariant1224'
end
theory German_ctc_hint_67
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_67:
(invariantX871 /\ invariantX854 /\ invariantX601 /\ invariantX348 /\ invariant1207 /\ invariant1224 /\ invariant1278 /\ tau)
-> invariant1278'
end
theory German_ctc_hint_68
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_68:
(invariantX871 /\ invariantX601 /\ invariantX348 /\ invariant1190 /\ invariant1298 /\ tau)
-> invariant1298'
end
theory German_ctc_hint_69
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
lemma hint_69:
(invariantX871 /\ invariantX601 /\ invariantX348 /\ invariant1190 /\ invariant1314 /\ tau)
-> invariant1314'
end
theory German_ctc_preservation
use import bool.Bool
use import int.Int
use import German_ctc_defs
use import German_ctc_invpreds
use import German_ctc_trdefs
use import German_ctc_hint_69
use import German_ctc_hint_68
use import German_ctc_hint_67
use import German_ctc_hint_66
use import German_ctc_hint_65
use import German_ctc_hint_64
use import German_ctc_hint_63
use import German_ctc_hint_62
use import German_ctc_hint_61
use import German_ctc_hint_60
use import German_ctc_hint_59
use import German_ctc_hint_58
use import German_ctc_hint_57
use import German_ctc_hint_56
use import German_ctc_hint_55
use import German_ctc_hint_54
use import German_ctc_hint_53
use import German_ctc_hint_52
use import German_ctc_hint_51
use import German_ctc_hint_50
use import German_ctc_hint_49
use import German_ctc_hint_48
use import German_ctc_hint_47
use import German_ctc_hint_46
use import German_ctc_hint_45
use import German_ctc_hint_44
use import German_ctc_hint_43
use import German_ctc_hint_42
use import German_ctc_hint_41
use import German_ctc_hint_40
use import German_ctc_hint_39
use import German_ctc_hint_38
use import German_ctc_hint_37
use import German_ctc_hint_36
use import German_ctc_hint_35
use import German_ctc_hint_34
use import German_ctc_hint_33
use import German_ctc_hint_32
use import German_ctc_hint_31
use import German_ctc_hint_30
use import German_ctc_hint_29
use import German_ctc_hint_28
use import German_ctc_hint_27
use import German_ctc_hint_26
use import German_ctc_hint_25
use import German_ctc_hint_24
use import German_ctc_hint_23
use import German_ctc_hint_22
use import German_ctc_hint_21
use import German_ctc_hint_20
use import German_ctc_hint_19
use import German_ctc_hint_18
use import German_ctc_hint_17
use import German_ctc_hint_16
use import German_ctc_hint_15
use import German_ctc_hint_14
use import German_ctc_hint_13
use import German_ctc_hint_12
use import German_ctc_hint_11
use import German_ctc_hint_10
use import German_ctc_hint_9
use import German_ctc_hint_8
use import German_ctc_hint_7
use import German_ctc_hint_6
use import German_ctc_hint_5
use import German_ctc_hint_4
use import German_ctc_hint_3
use import German_ctc_hint_2
use import German_ctc_hint_1
goal preservation:
(invariant895 /\ invariant1278 /\ invariantX265 /\ invariant502 /\ invariantX659 /\ invariant100 /\ invariantX285 /\ invariantX158 /\ invariantX415 /\ invariant351 /\ invariant218 /\ invariantX296 /\ invariantX41 /\ invariantX428 /\ invariantX684 /\ invariant1098 /\ invariant1097 /\ invariant1096 /\ invariant1224 /\ invariantX185 /\ invariant71 /\ invariant69 /\ invariantX321 /\ invariant1081 /\ invariant1080 /\ invariant1207 /\ invariant819 /\ invariantX208 /\ invariantX338 /\ invariant46 /\ invariant1069 /\ invariant1068 /\ invariantX854 /\ invariant554 /\ invariantX88 /\ invariantX601 /\ invariant294 /\ invariant1190 /\ invariantX348 /\ invariant35 /\ invariant34 /\ invariant930 /\ invariant1314 /\ invariant32 /\ invariant1055 /\ invariant798 /\ invariantX102 /\ invariantX231 /\ invariantX871 /\ invariant663 /\ invariantX362 /\ invariantX490 /\ invariant661 /\ invariant1042 /\ invariant1298 /\ invariantX111 /\ invariant913 /\ invariant911 /\ invariantX371 /\ invariantX247 /\ invariant777 /\ invariant776 /\ invariantX505 /\ invariantX123 /\ invariant3 /\ invariant2 /\ invariant897 /\ invariant1 /\ invariant129 /\ tau)
->
(invariant895' /\ invariant1278' /\ invariantX265' /\ invariant502' /\ invariantX659' /\ invariant100' /\ invariantX285' /\ invariantX158' /\ invariantX415' /\ invariant351' /\ invariant218' /\ invariantX296' /\ invariantX41' /\ invariantX428' /\ invariantX684' /\ invariant1098' /\ invariant1097' /\ invariant1096' /\ invariant1224' /\ invariantX185' /\ invariant71' /\ invariant69' /\ invariantX321' /\ invariant1081' /\ invariant1080' /\ invariant1207' /\ invariant819' /\ invariantX208' /\ invariantX338' /\ invariant46' /\ invariant1069' /\ invariant1068' /\ invariantX854' /\ invariant554' /\ invariantX88' /\ invariantX601' /\ invariant294' /\ invariant1190' /\ invariantX348' /\ invariant35' /\ invariant34' /\ invariant930' /\ invariant1314' /\ invariant32' /\ invariant1055' /\ invariant798' /\ invariantX102' /\ invariantX231' /\ invariantX871' /\ invariant663' /\ invariantX362' /\ invariantX490' /\ invariant661' /\ invariant1042' /\ invariant1298' /\ invariantX111' /\ invariant913' /\ invariant911' /\ invariantX371' /\ invariantX247' /\ invariant777' /\ invariant776' /\ invariantX505' /\ invariantX123' /\ invariant3' /\ invariant2' /\ invariant897' /\ invariant1' /\ invariant129')
end