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 =
(* transition sendGnts *)
(exists i:int. 
( (* requires *)
exgntd = False /\
curcmd = Reqs /\
curClient = i /\
(chan2Cmd i) = Empty) /\
( (* actions *)
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 =
(* transition recvGnte *)
(exists i:int. 
( (* requires *)
(chan2Cmd i) = Gnte) /\
( (* actions *)
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 =
(* transition recvInvack *)
(exists i:int. 
( (* requires *)
curcmd <> Empty /\
(chan3Cmd i) = Invack) /\
( (* actions *)
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 =
(* transition sendInv *)
(exists i:int. 
( (* requires *)
curcmd = Reqe /\
(chan2Cmd i) = Empty /\
(invset i) = True) /\
( (* actions *)
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 =
(* transition recvReqe *)
(exists i:int. 
( (* requires *)
curcmd = Empty /\
(chan1Cmd i) = Reqe) /\
( (* actions *)
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 =
(* transition recvReqs *)
(exists i:int. 
( (* requires *)
curcmd = Empty /\
(chan1Cmd i) = Reqs) /\
( (* actions *)
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 =
(* transition sendGnte *)
(exists i:int. 
( (* requires *)
exgntd = False /\
curcmd = Reqe /\
curClient = i /\
(chan2Cmd i) = Empty /\
(shrset i) = False
/\ (forall j:int.i = j \/ 
((shrset j) = False))
) /\
( (* actions *)
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 =
(* transition sendReqe *)
(exists i:int. 
( (* requires *)
(chan1Cmd i) = Empty /\
(cacheState i) <> Exclusive) /\
( (* actions *)
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 =
(* transition sendReqs *)
(exists i:int. 
( (* requires *)
(chan1Cmd i) = Empty /\
(cacheState i) = Invalid) /\
( (* actions *)
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_ =
(* transition sendInv *)
(exists i:int. 
( (* requires *)
exgntd = True /\
curcmd = Reqs /\
(chan2Cmd i) = Empty /\
(invset i) = True) /\
( (* actions *)
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 =
(* transition store *)
(exists n:int. 
( (* requires *)
(cacheState n) = Exclusive) /\
( (* actions *)
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 =
(* transition recvGnts *)
(exists i:int. 
( (* requires *)
(chan2Cmd i) = Gnts) /\
( (* actions *)
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 =
(* transition sendInvack *)
(exists i:int. 
( (* requires *)
(chan2Cmd i) = Inv /\
(chan3Cmd i) = Empty) /\
( (* actions *)
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