theory German_pfs_defs

use import bool.Bool
use import int.Int

type state = Invalid | Shared | Exclusive
type msg1 = Empty1 | Reqs | Reqe
type msg2 = Empty2 | Inv | Gnts | Gnte
type msg3 = Empty3 | Invack

function exgntd : bool
function curcmd : msg1
function flag : bool
function exgntd' : bool
function curcmd' : msg1
function flag' : bool
function cache int : state
function chan1 int : msg1
function chan2 int : msg2
function chan3 int : msg3
function curptr int : bool
function shrset int : bool
function invset int : bool
function cache' int : state
function chan1' int : msg1
function chan2' int : msg2
function chan3' int : msg3
function curptr' int : bool
function shrset' int : bool
function invset' int : bool

end


theory German_pfs_invdecls

use import bool.Bool
use import int.Int
use import German_pfs_defs

predicate invariantX1361
predicate invariantX1361'
predicate invariantX74
predicate invariantX74'
predicate invariantX110
predicate invariantX110'
predicate invariantX129
predicate invariantX129'
predicate invariantX142
predicate invariantX142'
predicate invariantX172
predicate invariantX172'
predicate invariantX196
predicate invariantX196'
predicate invariantX221
predicate invariantX221'
predicate invariantX246
predicate invariantX246'
predicate invariantX274
predicate invariantX274'
predicate invariantX282
predicate invariantX282'
predicate invariantX298
predicate invariantX298'
predicate invariantX308
predicate invariantX308'
predicate invariantX323
predicate invariantX323'
predicate invariantX341
predicate invariantX341'
predicate invariantX668
predicate invariantX668'
predicate invariantX716
predicate invariantX716'
predicate invariantX762
predicate invariantX762'
predicate invariantX795
predicate invariantX795'
predicate invariantX820
predicate invariantX820'
predicate invariantX839
predicate invariantX839'
predicate invariantX850
predicate invariantX850'
predicate invariantX358
predicate invariantX358'
predicate invariantX395
predicate invariantX395'
predicate invariantX11
predicate invariantX11'
predicate invariantX22
predicate invariantX22'
predicate invariantX35
predicate invariantX35'
predicate invariantX46
predicate invariantX46'
predicate invariantX57
predicate invariantX57'
predicate invariantX431
predicate invariantX431'
predicate invariantX444
predicate invariantX444'
predicate invariantX500
predicate invariantX500'
predicate invariantX516
predicate invariantX516'
predicate invariantX539
predicate invariantX539'
predicate invariantX563
predicate invariantX563'
predicate invariantX576
predicate invariantX576'
predicate invariantX587
predicate invariantX587'
predicate invariant1
predicate invariant1'
predicate invariant506
predicate invariant506'
predicate invariant526
predicate invariant526'
predicate invariant648
predicate invariant648'
predicate invariant638
predicate invariant638'
predicate invariant873
predicate invariant873'
predicate invariant1073
predicate invariant1073'
predicate invariant1132
predicate invariant1132'
predicate invariant1104
predicate invariant1104'
predicate invariant1108
predicate invariant1108'
predicate invariant1086
predicate invariant1086'
predicate invariant1114
predicate invariant1114'
predicate invariant1106
predicate invariant1106'
predicate invariant1160
predicate invariant1160'

end


theory German_pfs_invdefs

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls

axiom invariantX576_def:
invariantX576 <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(invset z2) = True)

axiom invariantX576'_def:
invariantX576' <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(invset' z2) = True)

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

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

axiom invariantX444_def:
invariantX444 <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan3 z2) = Invack)

axiom invariantX444'_def:
invariantX444' <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan3' z2) = Invack)

axiom invariantX762_def:
invariantX762 <-> not (exists z1:int. (chan2 z1) = Gnte /\
(shrset z1) = False)

axiom invariantX762'_def:
invariantX762' <-> not (exists z1:int. (chan2' z1) = Gnte /\
(shrset' z1) = False)

axiom invariantX57_def:
invariantX57 <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Gnte)

axiom invariantX57'_def:
invariantX57' <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Gnte)

axiom invariant1160_def:
invariant1160 <-> not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty1 /\
flag = False /\
(cache z3) = Invalid /\
(chan1 z3) = Empty1 /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(shrset z1) = True /\
(shrset z2) = True)

axiom invariant1160'_def:
invariant1160' <-> not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty1 /\
flag' = False /\
(cache' z3) = Invalid /\
(chan1' z3) = Empty1 /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(shrset' z1) = True /\
(shrset' z2) = True)

axiom invariant648_def:
invariant648 <-> not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
flag = False /\
(chan2 z1) = Inv /\
(chan2 z2) = Inv /\
(chan3 z2) = Empty3)

axiom invariant648'_def:
invariant648' <-> not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
flag' = False /\
(chan2' z1) = Inv /\
(chan2' z2) = Inv /\
(chan3' z2) = Empty3)

axiom invariantX246_def:
invariantX246 <-> not (exists z1:int. (shrset z1) = False /\
(invset z1) = True)

axiom invariantX246'_def:
invariantX246' <-> not (exists z1:int. (shrset' z1) = False /\
(invset' z1) = True)

axiom invariantX500_def:
invariantX500 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(chan2 z2) = Inv)

axiom invariantX500'_def:
invariantX500' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(chan2' z2) = Inv)

axiom invariantX820_def:
invariantX820 <-> not (exists z1:int. (chan2 z1) = Gnts /\
(shrset z1) = False)

axiom invariantX820'_def:
invariantX820' <-> not (exists z1:int. (chan2' z1) = Gnts /\
(shrset' z1) = False)

axiom invariantX308_def:
invariantX308 <-> not (exists z1:int. flag = True /\
(chan2 z1) = Inv)

axiom invariantX308'_def:
invariantX308' <-> not (exists z1:int. flag' = True /\
(chan2' z1) = Inv)

axiom invariantX563_def:
invariantX563 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(shrset z2) = True)

axiom invariantX563'_def:
invariantX563' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(shrset' z2) = True)

axiom invariant526_def:
invariant526 <-> not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
flag = False /\
(chan2 z1) = Inv /\
(chan3 z2) = Invack)

axiom invariant526'_def:
invariant526' <-> not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
flag' = False /\
(chan2' z1) = Inv /\
(chan3' z2) = Invack)

axiom invariant1104_def:
invariant1104 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty1 /\
flag = False /\
(chan1 z2) = Reqs /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(shrset z1) = True /\
(shrset z2) = True)

axiom invariant1104'_def:
invariant1104' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty1 /\
flag' = False /\
(chan1' z2) = Reqs /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(shrset' z1) = True /\
(shrset' z2) = True)

axiom invariantX431_def:
invariantX431 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(chan3 z2) = Invack)

axiom invariantX431'_def:
invariantX431' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(chan3' z2) = Invack)

axiom invariant1106_def:
invariant1106 <-> not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty1 /\
flag = False /\
(chan1 z3) = Reqs /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(shrset z1) = True /\
(shrset z2) = True)

axiom invariant1106'_def:
invariant1106' <-> not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty1 /\
flag' = False /\
(chan1' z3) = Reqs /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(shrset' z1) = True /\
(shrset' z2) = True)

axiom invariantX46_def:
invariantX46 <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Gnts)

axiom invariantX46'_def:
invariantX46' <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Gnts)

axiom invariantX110_def:
invariantX110 <-> not (exists z1:int. exgntd = False /\
(chan2 z1) = Gnte)

axiom invariantX110'_def:
invariantX110' <-> not (exists z1:int. exgntd' = False /\
(chan2' z1) = Gnte)

axiom invariant1108_def:
invariant1108 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
flag = True /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(shrset z2) = True /\
(invset z1) = True /\
(invset z1) = (shrset z1))

axiom invariant1108'_def:
invariant1108' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
flag' = True /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(shrset' z2) = True /\
(invset' z1) = True /\
(invset' z1) = (shrset' z1))

axiom invariantX172_def:
invariantX172 <-> not (exists z1:int. (chan3 z1) = Invack /\
(shrset z1) = False)

axiom invariantX172'_def:
invariantX172' <-> not (exists z1:int. (chan3' z1) = Invack /\
(shrset' z1) = False)

axiom invariantX298_def:
invariantX298 <-> not (exists z1:int. (chan2 z1) = Inv /\
(invset z1) = True)

axiom invariantX298'_def:
invariantX298' <-> not (exists z1:int. (chan2' z1) = Inv /\
(invset' z1) = True)

axiom invariant1114_def:
invariant1114 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty1 /\
flag = False /\
(cache z2) = Invalid /\
(chan1 z2) = Empty1 /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(shrset z1) = True /\
(shrset z2) = True)

axiom invariant1114'_def:
invariant1114' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty1 /\
flag' = False /\
(cache' z2) = Invalid /\
(chan1' z2) = Empty1 /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(shrset' z1) = True /\
(shrset' z2) = True)

axiom invariantX358_def:
invariantX358 <-> not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan3 z1) = Invack)

axiom invariantX358'_def:
invariantX358' <-> not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan3' z1) = Invack)

axiom invariantX35_def:
invariantX35 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z2) <> Invalid /\
(chan2 z1) = Gnte)

axiom invariantX35'_def:
invariantX35' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z2) <> Invalid /\
(chan2' z1) = Gnte)

axiom invariantX221_def:
invariantX221 <-> not (exists z1:int. (chan2 z1) = Inv /\
(chan3 z1) = Invack)

axiom invariantX221'_def:
invariantX221' <-> not (exists z1:int. (chan2' z1) = Inv /\
(chan3' z1) = Invack)

axiom invariantX668_def:
invariantX668 <-> not (exists z1:int. exgntd = True /\
(chan2 z1) = Gnts)

axiom invariantX668'_def:
invariantX668' <-> not (exists z1:int. exgntd' = True /\
(chan2' z1) = Gnts)

axiom invariantX539_def:
invariantX539 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(invset z2) = True)

axiom invariantX539'_def:
invariantX539' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(invset' z2) = True)

axiom invariantX795_def:
invariantX795 <-> not (exists z1:int. (cache z1) <> Invalid /\
(shrset z1) = False)

axiom invariantX795'_def:
invariantX795' <-> not (exists z1:int. (cache' z1) <> Invalid /\
(shrset' z1) = False)

axiom invariantX282_def:
invariantX282 <-> not (exists z1:int. flag = True /\
(chan3 z1) = Invack)

axiom invariantX282'_def:
invariantX282' <-> not (exists z1:int. flag' = True /\
(chan3' z1) = Invack)

axiom invariant873_def:
invariant873 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
flag = False /\
(chan2 z1) = Inv /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(invset z2) = True)

axiom invariant873'_def:
invariant873' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
flag' = False /\
(chan2' z1) = Inv /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(invset' z2) = True)

axiom invariantX22_def:
invariantX22 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(chan2 z2) = Gnte)

axiom invariantX22'_def:
invariantX22' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(chan2' z2) = Gnte)

axiom invariantX341_def:
invariantX341 <-> not (exists z1:int. curcmd = Empty1 /\
(chan2 z1) = Inv)

axiom invariantX341'_def:
invariantX341' <-> not (exists z1:int. curcmd' = Empty1 /\
(chan2' z1) = Inv)

axiom invariant1132_def:
invariant1132 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
flag = True /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(shrset z1) = True /\
(shrset z2) = True)

axiom invariant1132'_def:
invariant1132' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
flag' = True /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(shrset' z1) = True /\
(shrset' z2) = True)

axiom invariantX850_def:
invariantX850 <-> not (exists z1:int. (chan2 z1) = Gnts /\
(chan3 z1) = Invack)

axiom invariantX850'_def:
invariantX850' <-> not (exists z1:int. (chan2' z1) = Gnts /\
(chan3' z1) = Invack)

axiom invariantX274_def:
invariantX274 <-> not (exists z1:int. (chan3 z1) = Invack /\
(invset z1) = True)

axiom invariantX274'_def:
invariantX274' <-> not (exists z1:int. (chan3' z1) = Invack /\
(invset' z1) = True)

axiom invariantX1361_def:
invariantX1361 <-> not (curcmd = Empty1 /\
flag = True)

axiom invariantX1361'_def:
invariantX1361' <-> not (curcmd' = Empty1 /\
flag' = True)

axiom invariant1073_def:
invariant1073 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
flag = False /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(invset z1) = True /\
(invset z2) = True)

axiom invariant1073'_def:
invariant1073' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
flag' = False /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(invset' z1) = True /\
(invset' z2) = True)

axiom invariantX142_def:
invariantX142 <-> not (exists z1:int. (chan2 z1) = Gnte /\
(chan3 z1) = Invack)

axiom invariantX142'_def:
invariantX142' <-> not (exists z1:int. (chan2' z1) = Gnte /\
(chan3' z1) = Invack)

axiom invariantX716_def:
invariantX716 <-> not (exists z1:int. (cache z1) = Exclusive /\
(shrset z1) = False)

axiom invariantX716'_def:
invariantX716' <-> not (exists z1:int. (cache' z1) = Exclusive /\
(shrset' z1) = False)

axiom invariantX587_def:
invariantX587 <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(shrset z2) = True)

axiom invariantX587'_def:
invariantX587' <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(shrset' z2) = True)

axiom invariantX11_def:
invariantX11 <-> not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(chan2 z2) = Gnts)

axiom invariantX11'_def:
invariantX11' <-> not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(chan2' z2) = Gnts)

axiom invariantX395_def:
invariantX395 <-> not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan2 z1) = Inv)

axiom invariantX395'_def:
invariantX395' <-> not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan2' z1) = Inv)

axiom invariantX74_def:
invariantX74 <-> not (exists z1:int. exgntd = False /\
(cache z1) = Exclusive)

axiom invariantX74'_def:
invariantX74' <-> not (exists z1:int. exgntd' = False /\
(cache' z1) = Exclusive)

axiom invariantX839_def:
invariantX839 <-> not (exists z1:int. (cache z1) <> Invalid /\
(chan3 z1) = Invack)

axiom invariantX839'_def:
invariantX839' <-> not (exists z1:int. (cache' z1) <> Invalid /\
(chan3' z1) = Invack)

axiom invariant506_def:
invariant506 <-> not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
flag = False /\
(chan3 z1) = Invack /\
(chan3 z2) = Invack)

axiom invariant506'_def:
invariant506' <-> not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
flag' = False /\
(chan3' z1) = Invack /\
(chan3' z2) = Invack)

axiom invariantX516_def:
invariantX516 <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Inv)

axiom invariantX516'_def:
invariantX516' <-> not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Inv)

axiom invariantX196_def:
invariantX196 <-> not (exists z1:int. (chan2 z1) = Inv /\
(shrset z1) = False)

axiom invariantX196'_def:
invariantX196' <-> not (exists z1:int. (chan2' z1) = Inv /\
(shrset' z1) = False)

axiom invariantX323_def:
invariantX323 <-> not (exists z1:int. curcmd = Empty1 /\
(chan3 z1) = Invack)

axiom invariantX323'_def:
invariantX323' <-> not (exists z1:int. curcmd' = Empty1 /\
(chan3' z1) = Invack)

axiom invariant1086_def:
invariant1086 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
flag = True /\
(chan2 z1) = Empty2 /\
(chan2 z2) = Empty2 /\
(chan3 z2) = Empty3 /\
(invset z1) = True /\
(invset z1) = (shrset z1) /\
(invset z2) = True /\
(invset z2) = (shrset z2))

axiom invariant1086'_def:
invariant1086' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
flag' = True /\
(chan2' z1) = Empty2 /\
(chan2' z2) = Empty2 /\
(chan3' z2) = Empty3 /\
(invset' z1) = True /\
(invset' z1) = (shrset' z1) /\
(invset' z2) = True /\
(invset' z2) = (shrset' z2))

axiom invariant638_def:
invariant638 <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
flag = False /\
(chan2 z1) = Empty2 /\
(chan3 z2) = Invack /\
(invset z1) = True)

axiom invariant638'_def:
invariant638' <-> not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
flag' = False /\
(chan2' z1) = Empty2 /\
(chan3' z2) = Invack /\
(invset' z1) = True)

axiom invariantX129_def:
invariantX129 <-> not (exists z1:int. (cache z1) = Exclusive /\
(chan3 z1) = Invack)

axiom invariantX129'_def:
invariantX129' <-> not (exists z1:int. (cache' z1) = Exclusive /\
(chan3' z1) = Invack)


end


theory German_pfs_trdecl

use import bool.Bool
use import int.Int
use import German_pfs_defs

predicate transition__t1
predicate transition__t2
predicate transition__t3
predicate transition__t3bis
predicate transition__t4
predicate transition__t5
predicate transition__t6
predicate transition__t7
predicate transition__t8
predicate transition__t9
predicate transition__t10
predicate transition__t11
predicate transition__t12
predicate transition__t13
predicate transition__t14

predicate tau

end


theory German_pfs_trdefs

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_trdecl

axiom transition__t11_def:
transition__t11 <-> (* transition t11 *)
(exists x:int. 
( (* requires *)
flag = False /\
(cache x) <> Exclusive /\
(chan1 x) = Empty1) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 chan1' j = Reqe
else chan1' j = (chan1 j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t6_def:
transition__t6 <-> (* transition t6 *)
(exists x:int. 
( (* requires *)
flag = True /\
(invset x) = (shrset x)
/\ (forall j:int.x = j \/ 
((invset j) = (shrset j)))
) /\
( (* actions *)
flag' = False /\
exgntd' = exgntd /\
curcmd' = curcmd /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t7_def:
transition__t7 <-> (* transition t7 *)
(exists x:int. 
( (* requires *)
exgntd = True /\
curcmd = Reqs /\
flag = False /\
(chan2 x) = Empty2 /\
(invset x) = True) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 chan2' j = Inv
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = x then
 invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


axiom transition__t10_def:
transition__t10 <-> (* transition t10 *)
(exists x:int. 
( (* requires *)
flag = False /\
(cache x) = Invalid /\
(chan1 x) = Empty1) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 cache' j = Invalid
else cache' j = (cache j)) /\
(forall j:int.
if j = x then
 chan1' j = Reqs
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t3_def:
transition__t3 <-> (* transition t3 *)
(exists x:int. 
( (* requires *)
curcmd = Empty1 /\
flag = False /\
(chan1 x) = Reqs) /\
( (* actions *)
flag' = True /\
curcmd' = Reqs /\
exgntd' = exgntd /\
(forall j:int.
invset' j = (shrset j)) /\
(forall j:int.
if j = x then
 chan1' j = Empty1
else chan1' j = (chan1 j)) /\
(forall j:int.
if j = x then
 curptr' j = True
else curptr' j = False) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


axiom transition__t9_def:
transition__t9 <-> (* transition t9 *)
(exists x:int. 
( (* requires *)
curcmd <> Empty1 /\
flag = False /\
(chan3 x) = Invack) /\
( (* actions *)
exgntd' = False /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 chan3' j = Empty3
else chan3' j = (chan3 j)) /\
(forall j:int.
if j = x then
 shrset' j = False
else shrset' j = (shrset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t8_def:
transition__t8 <-> (* transition t8 *)
(exists x:int. 
( (* requires *)
curcmd = Reqe /\
flag = False /\
(chan2 x) = Empty2 /\
(invset x) = True) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 chan2' j = Inv
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = x then
 invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


axiom transition__t14_def:
transition__t14 <-> (* transition t14 *)
(exists x:int. 
( (* requires *)
flag = False /\
(chan2 x) = Gnte) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 cache' j = Exclusive
else cache' j = (cache j)) /\
(forall j:int.
if j = x then
 chan2' j = Empty2
else chan2' j = (chan2 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t4_def:
transition__t4 <-> (* transition t4 *)
(exists x:int. 
( (* requires *)
flag = True /\
(shrset x) = False) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


axiom transition__t3bis_def:
transition__t3bis <-> (* transition t3bis *)
(exists x:int. 
( (* requires *)
curcmd = Empty1 /\
flag = False /\
(chan1 x) = Reqe) /\
( (* actions *)
flag' = True /\
curcmd' = Reqe /\
exgntd' = exgntd /\
(forall j:int.
invset' j = (shrset j)) /\
(forall j:int.
if j = x then
 chan1' j = Empty1
else chan1' j = (chan1 j)) /\
(forall j:int.
if j = x then
 curptr' j = True
else curptr' j = False) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


axiom transition__t2_def:
transition__t2 <-> (* transition t2 *)
(exists x:int. 
( (* requires *)
curcmd = Reqe /\
flag = False /\
(chan2 x) = Empty2 /\
(curptr x) = True /\
(shrset x) = False
/\ (forall j:int.x = j \/ 
((shrset j) = False))
) /\
( (* actions *)
curcmd' = Empty1 /\
exgntd' = True /\
flag' = flag /\
(forall j:int.
if j = x then
 chan2' j = Gnte
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = x then
 shrset' j = True
else shrset' j = (shrset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t12_def:
transition__t12 <-> (* transition t12 *)
(exists x:int. 
( (* requires *)
flag = False /\
(chan2 x) = Inv /\
(chan3 x) = Empty3) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 cache' j = Invalid
else cache' j = (cache j)) /\
(forall j:int.
if j = x then
 chan2' j = Empty2
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = x then
 chan3' j = Invack
else chan3' j = (chan3 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t1_def:
transition__t1 <-> (* transition t1 *)
(exists x:int. 
( (* requires *)
exgntd = False /\
curcmd = Reqs /\
flag = False /\
(chan2 x) = Empty2 /\
(curptr x) = True) /\
( (* actions *)
curcmd' = Empty1 /\
exgntd' = exgntd /\
flag' = flag /\
(forall j:int.
if j = x then
 chan2' j = Gnts
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = x then
 shrset' j = True
else shrset' j = (shrset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t13_def:
transition__t13 <-> (* transition t13 *)
(exists x:int. 
( (* requires *)
flag = False /\
(chan2 x) = Gnts) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 cache' j = Shared
else cache' j = (cache j)) /\
(forall j:int.
if j = x then
 chan2' j = Empty2
else chan2' j = (chan2 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) /\
(forall z1:int. invset' z1 = invset z1) ))


axiom transition__t5_def:
transition__t5 <-> (* transition t5 *)
(exists x:int. 
( (* requires *)
flag = True /\
(shrset x) = True) /\
( (* actions *)
exgntd' = exgntd /\
curcmd' = curcmd /\
flag' = flag /\
(forall j:int.
if j = x then
 invset' j = True
else invset' j = (invset j)) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. curptr' z1 = curptr z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))


axiom tau_def:
tau <-> (transition__t5 \/ transition__t13 \/ transition__t1 \/ transition__t12 \/ transition__t2 \/ transition__t3bis \/ transition__t4 \/ transition__t14 \/ transition__t8 \/ transition__t9 \/ transition__t3 \/ transition__t10 \/ transition__t7 \/ transition__t6 \/ transition__t11)


end


theory German_pfs_initialisation

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs

predicate init =
    forall z:int. (exgntd = False /\
curcmd = Empty1 /\
flag = False /\
(cache z) = Invalid /\
(chan1 z) = Empty1 /\
(chan2 z) = Empty2 /\
(chan3 z) = Empty3 /\
(curptr z) = False /\
(shrset z) = False /\
(invset z) = False)

goal initialisation:
    init -> (invariantX129 /\ invariant638 /\ invariant1086 /\ invariantX323 /\ invariantX196 /\ invariantX516 /\ invariant506 /\ invariantX839 /\ invariantX74 /\ invariantX395 /\ invariantX11 /\ invariantX587 /\ invariantX716 /\ invariantX142 /\ invariant1073 /\ invariantX1361 /\ invariantX274 /\ invariantX850 /\ invariant1132 /\ invariantX341 /\ invariantX22 /\ invariant873 /\ invariantX282 /\ invariantX795 /\ invariantX539 /\ invariantX668 /\ invariantX221 /\ invariantX35 /\ invariantX358 /\ invariant1114 /\ invariantX298 /\ invariantX172 /\ invariant1108 /\ invariantX110 /\ invariantX46 /\ invariant1106 /\ invariantX431 /\ invariant1104 /\ invariant526 /\ invariantX563 /\ invariantX308 /\ invariantX820 /\ invariantX500 /\ invariantX246 /\ invariant648 /\ invariant1160 /\ invariantX57 /\ invariantX762 /\ invariantX444 /\ invariant1 /\ invariantX576)


end


theory German_pfs_property

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs

goal property:
    (invariantX129 /\ invariant638 /\ invariant1086 /\ invariantX323 /\ invariantX196 /\ invariantX516 /\ invariant506 /\ invariantX839 /\ invariantX74 /\ invariantX395 /\ invariantX11 /\ invariantX587 /\ invariantX716 /\ invariantX142 /\ invariant1073 /\ invariantX1361 /\ invariantX274 /\ invariantX850 /\ invariant1132 /\ invariantX341 /\ invariantX22 /\ invariant873 /\ invariantX282 /\ invariantX795 /\ invariantX539 /\ invariantX668 /\ invariantX221 /\ invariantX35 /\ invariantX358 /\ invariant1114 /\ invariantX298 /\ invariantX172 /\ invariant1108 /\ invariantX110 /\ invariantX46 /\ invariant1106 /\ invariantX431 /\ invariant1104 /\ invariant526 /\ invariantX563 /\ invariantX308 /\ invariantX820 /\ invariantX500 /\ invariantX246 /\ invariant648 /\ invariant1160 /\ invariantX57 /\ invariantX762 /\ invariantX444 /\ invariant1 /\ invariantX576) -> (not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(cache z2) <> Invalid))


end


theory German_pfs_hint_1

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_1:
    (invariantX1361 /\ tau)
    -> invariantX1361'



end


theory German_pfs_hint_2

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_2:
    (invariantX850 /\ invariantX668 /\ invariantX358 /\ invariantX323 /\ invariantX282 /\ invariantX172 /\ tau)
    -> invariantX850'



end


theory German_pfs_hint_3

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_3:
    (invariantX850 /\ invariantX839 /\ invariantX323 /\ invariantX282 /\ invariantX274 /\ invariantX172 /\ invariantX142 /\ tau)
    -> invariantX839'



end


theory German_pfs_hint_4

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_4:
    (invariantX850 /\ invariantX820 /\ invariantX668 /\ tau)
    -> invariantX820'



end


theory German_pfs_hint_5

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_5:
    (invariantX839 /\ invariantX820 /\ invariantX795 /\ invariantX762 /\ invariantX246 /\ tau)
    -> invariantX795'



end


theory German_pfs_hint_6

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_6:
    (invariantX762 /\ invariantX142 /\ invariantX110 /\ tau)
    -> invariantX762'



end


theory German_pfs_hint_7

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_7:
    (invariantX762 /\ invariantX716 /\ invariantX246 /\ invariantX129 /\ invariantX74 /\ tau)
    -> invariantX716'



end


theory German_pfs_hint_8

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_8:
    (invariantX820 /\ invariantX668 /\ tau)
    -> invariantX668'



end


theory German_pfs_hint_9

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_9:
    (invariantX762 /\ invariantX587 /\ invariantX576 /\ invariantX516 /\ invariantX142 /\ invariantX110 /\ invariantX57 /\ invariantX46 /\ tau)
    -> invariantX587'



end


theory German_pfs_hint_10

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_10:
    (invariantX762 /\ invariantX587 /\ invariantX576 /\ invariantX516 /\ invariantX444 /\ invariantX246 /\ invariantX142 /\ invariantX110 /\ invariantX57 /\ invariantX46 /\ tau)
    -> invariantX576'



end


theory German_pfs_hint_11

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_11:
    (invariantX716 /\ invariantX587 /\ invariantX563 /\ invariantX539 /\ invariantX500 /\ invariantX129 /\ invariantX74 /\ invariantX22 /\ invariantX11 /\ tau)
    -> invariantX563'



end


theory German_pfs_hint_12

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_12:
    (invariantX716 /\ invariantX576 /\ invariantX563 /\ invariantX539 /\ invariantX500 /\ invariantX431 /\ invariantX129 /\ invariantX74 /\ invariantX22 /\ invariantX11 /\ tau)
    -> invariantX539'



end


theory German_pfs_hint_13

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_13:
    (invariantX762 /\ invariantX576 /\ invariantX516 /\ invariantX444 /\ invariantX196 /\ invariantX142 /\ invariantX110 /\ tau)
    -> invariantX516'



end


theory German_pfs_hint_14

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_14:
    (invariantX716 /\ invariantX539 /\ invariantX516 /\ invariantX500 /\ invariantX431 /\ invariantX129 /\ invariantX74 /\ tau)
    -> invariantX500'



end


theory German_pfs_hint_15

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_15:
    (invariantX762 /\ invariantX516 /\ invariantX444 /\ invariantX172 /\ invariantX142 /\ invariantX110 /\ invariantX57 /\ invariantX46 /\ tau)
    -> invariantX444'



end


theory German_pfs_hint_16

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_16:
    (invariantX716 /\ invariantX500 /\ invariantX444 /\ invariantX431 /\ invariantX129 /\ invariantX74 /\ invariantX22 /\ invariantX11 /\ tau)
    -> invariantX431'



end


theory German_pfs_hint_17

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_17:
    (invariantX395 /\ invariantX341 /\ invariantX308 /\ invariantX221 /\ invariantX196 /\ invariant526 /\ tau)
    -> invariantX395'



end


theory German_pfs_hint_18

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_18:
    (invariantX850 /\ invariantX395 /\ invariantX358 /\ invariantX323 /\ invariantX282 /\ invariantX172 /\ invariantX110 /\ invariant506 /\ tau)
    -> invariantX358'



end


theory German_pfs_hint_19

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_19:
    (invariantX1361 /\ invariantX395 /\ invariantX341 /\ invariantX196 /\ tau)
    -> invariantX341'



end


theory German_pfs_hint_20

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_20:
    (invariantX1361 /\ invariantX358 /\ invariantX341 /\ invariantX323 /\ invariantX172 /\ invariantX142 /\ tau)
    -> invariantX323'



end


theory German_pfs_hint_21

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_21:
    (invariantX341 /\ invariantX308 /\ invariantX196 /\ tau)
    -> invariantX308'



end


theory German_pfs_hint_22

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_22:
    (invariantX341 /\ invariantX308 /\ invariantX298 /\ invariantX221 /\ invariantX196 /\ tau)
    -> invariantX298'



end


theory German_pfs_hint_23

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_23:
    (invariantX323 /\ invariantX282 /\ invariantX172 /\ tau)
    -> invariantX282'



end


theory German_pfs_hint_24

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_24:
    (invariantX323 /\ invariantX298 /\ invariantX282 /\ invariantX274 /\ invariantX172 /\ invariantX142 /\ tau)
    -> invariantX274'



end


theory German_pfs_hint_25

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_25:
    (invariantX274 /\ invariantX246 /\ invariantX196 /\ tau)
    -> invariantX246'



end


theory German_pfs_hint_26

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_26:
    (invariantX274 /\ invariantX221 /\ invariantX172 /\ tau)
    -> invariantX221'



end


theory German_pfs_hint_27

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_27:
    (invariantX246 /\ invariantX221 /\ invariantX196 /\ tau)
    -> invariantX196'



end


theory German_pfs_hint_28

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_28:
    (invariantX196 /\ invariantX172 /\ invariantX142 /\ tau)
    -> invariantX172'



end


theory German_pfs_hint_29

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_29:
    (invariantX172 /\ invariantX142 /\ invariantX110 /\ tau)
    -> invariantX142'



end


theory German_pfs_hint_30

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def

lemma hint_30:
    (invariantX142 /\ invariantX129 /\ invariantX74 /\ tau)
    -> invariantX129'



end


theory German_pfs_hint_31

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_31:
    (invariantX444 /\ invariantX142 /\ invariantX110 /\ tau)
    -> invariantX110'



end


theory German_pfs_hint_32

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_32:
    (invariantX431 /\ invariantX129 /\ invariantX110 /\ invariantX74 /\ tau)
    -> invariantX74'



end


theory German_pfs_hint_33

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_33:
    (invariantX762 /\ invariantX142 /\ invariantX110 /\ invariantX57 /\ tau)
    -> invariantX57'



end


theory German_pfs_hint_34

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_34:
    (invariantX820 /\ invariantX762 /\ invariantX142 /\ invariantX110 /\ invariantX46 /\ tau)
    -> invariantX46'



end


theory German_pfs_hint_35

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_35:
    (invariantX795 /\ invariantX762 /\ invariantX142 /\ invariantX110 /\ invariantX57 /\ invariantX46 /\ invariantX35 /\ tau)
    -> invariantX35'



end


theory German_pfs_hint_36

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_36:
    (invariantX716 /\ invariantX129 /\ invariantX74 /\ invariantX57 /\ invariantX22 /\ tau)
    -> invariantX22'



end


theory German_pfs_hint_37

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_37:
    (invariantX716 /\ invariantX129 /\ invariantX74 /\ invariantX46 /\ invariantX11 /\ tau)
    -> invariantX11'



end


theory German_pfs_hint_38

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129'_def

lemma hint_38:
    (invariantX716 /\ invariantX563 /\ invariantX539 /\ invariantX431 /\ invariantX129 /\ invariantX74 /\ invariantX35 /\ invariantX22 /\ invariantX11 /\ invariant1 /\ tau)
    -> invariant1'



end


theory German_pfs_hint_39

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_39:
    (invariantX850 /\ invariantX282 /\ invariantX274 /\ invariantX142 /\ invariant506 /\ invariant526 /\ tau)
    -> invariant506'



end


theory German_pfs_hint_40

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_40:
    (invariantX308 /\ invariantX221 /\ invariant526 /\ invariant638 /\ invariant648 /\ tau)
    -> invariant526'



end


theory German_pfs_hint_41

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_41:
    (invariantX668 /\ invariantX444 /\ invariantX298 /\ invariantX274 /\ invariantX172 /\ invariant638 /\ invariant873 /\ tau)
    -> invariant638'



end


theory German_pfs_hint_42

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_42:
    (invariantX308 /\ invariantX274 /\ invariantX221 /\ invariant526 /\ invariant648 /\ invariant873 /\ tau)
    -> invariant648'



end


theory German_pfs_hint_43

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_43:
    (invariantX668 /\ invariantX516 /\ invariantX308 /\ invariant873 /\ invariant1073 /\ tau)
    -> invariant873'



end


theory German_pfs_hint_44

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_44:
    (invariantX668 /\ invariantX576 /\ invariantX298 /\ invariant1073 /\ invariant1086 /\ tau)
    -> invariant1073'



end


theory German_pfs_hint_45

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_45:
    (invariantX323 /\ invariantX246 /\ invariant1086 /\ invariant1104 /\ invariant1106 /\ invariant1108 /\ invariant1132 /\ tau)
    -> invariant1086'



end


theory German_pfs_hint_46

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_46:
    (invariantX1361 /\ invariantX668 /\ invariantX587 /\ invariantX341 /\ invariant1104 /\ invariant1114 /\ tau)
    -> invariant1104'



end


theory German_pfs_hint_47

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_47:
    (invariantX1361 /\ invariantX668 /\ invariantX587 /\ invariantX341 /\ invariant1106 /\ invariant1114 /\ invariant1160 /\ tau)
    -> invariant1106'



end


theory German_pfs_hint_48

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_48:
    (invariantX323 /\ invariant1104 /\ invariant1106 /\ invariant1108 /\ invariant1132 /\ tau)
    -> invariant1108'



end


theory German_pfs_hint_49

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_49:
    (invariantX1361 /\ invariantX668 /\ invariantX587 /\ invariantX341 /\ invariant1114 /\ tau)
    -> invariant1114'



end


theory German_pfs_hint_50

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant1160_def
meta remove_prop prop invariant1160'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_50:
    (invariantX323 /\ invariant1104 /\ invariant1106 /\ invariant1132 /\ tau)
    -> invariant1132'



end


theory German_pfs_hint_51

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_invdefs
use import German_pfs_trdecl
use import German_pfs_trdefs

meta remove_prop prop invariantX576_def
meta remove_prop prop invariantX576'_def
meta remove_prop prop invariant1_def
meta remove_prop prop invariant1'_def
meta remove_prop prop invariantX444_def
meta remove_prop prop invariantX444'_def
meta remove_prop prop invariantX762_def
meta remove_prop prop invariantX762'_def
meta remove_prop prop invariantX57_def
meta remove_prop prop invariantX57'_def
meta remove_prop prop invariant648_def
meta remove_prop prop invariant648'_def
meta remove_prop prop invariantX246_def
meta remove_prop prop invariantX246'_def
meta remove_prop prop invariantX500_def
meta remove_prop prop invariantX500'_def
meta remove_prop prop invariantX820_def
meta remove_prop prop invariantX820'_def
meta remove_prop prop invariantX308_def
meta remove_prop prop invariantX308'_def
meta remove_prop prop invariantX563_def
meta remove_prop prop invariantX563'_def
meta remove_prop prop invariant526_def
meta remove_prop prop invariant526'_def
meta remove_prop prop invariant1104_def
meta remove_prop prop invariant1104'_def
meta remove_prop prop invariantX431_def
meta remove_prop prop invariantX431'_def
meta remove_prop prop invariant1106_def
meta remove_prop prop invariant1106'_def
meta remove_prop prop invariantX46_def
meta remove_prop prop invariantX46'_def
meta remove_prop prop invariantX110_def
meta remove_prop prop invariantX110'_def
meta remove_prop prop invariant1108_def
meta remove_prop prop invariant1108'_def
meta remove_prop prop invariantX172_def
meta remove_prop prop invariantX172'_def
meta remove_prop prop invariantX298_def
meta remove_prop prop invariantX298'_def
meta remove_prop prop invariant1114'_def
meta remove_prop prop invariantX358_def
meta remove_prop prop invariantX358'_def
meta remove_prop prop invariantX35_def
meta remove_prop prop invariantX35'_def
meta remove_prop prop invariantX221_def
meta remove_prop prop invariantX221'_def
meta remove_prop prop invariantX668'_def
meta remove_prop prop invariantX539_def
meta remove_prop prop invariantX539'_def
meta remove_prop prop invariantX795_def
meta remove_prop prop invariantX795'_def
meta remove_prop prop invariantX282_def
meta remove_prop prop invariantX282'_def
meta remove_prop prop invariant873_def
meta remove_prop prop invariant873'_def
meta remove_prop prop invariantX22_def
meta remove_prop prop invariantX22'_def
meta remove_prop prop invariantX341'_def
meta remove_prop prop invariant1132_def
meta remove_prop prop invariant1132'_def
meta remove_prop prop invariantX850_def
meta remove_prop prop invariantX850'_def
meta remove_prop prop invariantX274_def
meta remove_prop prop invariantX274'_def
meta remove_prop prop invariantX1361'_def
meta remove_prop prop invariant1073_def
meta remove_prop prop invariant1073'_def
meta remove_prop prop invariantX142_def
meta remove_prop prop invariantX142'_def
meta remove_prop prop invariantX716_def
meta remove_prop prop invariantX716'_def
meta remove_prop prop invariantX587'_def
meta remove_prop prop invariantX11_def
meta remove_prop prop invariantX11'_def
meta remove_prop prop invariantX395_def
meta remove_prop prop invariantX395'_def
meta remove_prop prop invariantX74_def
meta remove_prop prop invariantX74'_def
meta remove_prop prop invariantX839_def
meta remove_prop prop invariantX839'_def
meta remove_prop prop invariant506_def
meta remove_prop prop invariant506'_def
meta remove_prop prop invariantX516_def
meta remove_prop prop invariantX516'_def
meta remove_prop prop invariantX196_def
meta remove_prop prop invariantX196'_def
meta remove_prop prop invariantX323_def
meta remove_prop prop invariantX323'_def
meta remove_prop prop invariant1086_def
meta remove_prop prop invariant1086'_def
meta remove_prop prop invariant638_def
meta remove_prop prop invariant638'_def
meta remove_prop prop invariantX129_def
meta remove_prop prop invariantX129'_def

lemma hint_51:
    (invariantX1361 /\ invariantX668 /\ invariantX587 /\ invariantX341 /\ invariant1114 /\ invariant1160 /\ tau)
    -> invariant1160'



end


theory German_pfs_preservation

use import bool.Bool
use import int.Int
use import German_pfs_defs
use import German_pfs_invdecls
use import German_pfs_trdecl
use import German_pfs_hint_51
use import German_pfs_hint_50
use import German_pfs_hint_49
use import German_pfs_hint_48
use import German_pfs_hint_47
use import German_pfs_hint_46
use import German_pfs_hint_45
use import German_pfs_hint_44
use import German_pfs_hint_43
use import German_pfs_hint_42
use import German_pfs_hint_41
use import German_pfs_hint_40
use import German_pfs_hint_39
use import German_pfs_hint_38
use import German_pfs_hint_37
use import German_pfs_hint_36
use import German_pfs_hint_35
use import German_pfs_hint_34
use import German_pfs_hint_33
use import German_pfs_hint_32
use import German_pfs_hint_31
use import German_pfs_hint_30
use import German_pfs_hint_29
use import German_pfs_hint_28
use import German_pfs_hint_27
use import German_pfs_hint_26
use import German_pfs_hint_25
use import German_pfs_hint_24
use import German_pfs_hint_23
use import German_pfs_hint_22
use import German_pfs_hint_21
use import German_pfs_hint_20
use import German_pfs_hint_19
use import German_pfs_hint_18
use import German_pfs_hint_17
use import German_pfs_hint_16
use import German_pfs_hint_15
use import German_pfs_hint_14
use import German_pfs_hint_13
use import German_pfs_hint_12
use import German_pfs_hint_11
use import German_pfs_hint_10
use import German_pfs_hint_9
use import German_pfs_hint_8
use import German_pfs_hint_7
use import German_pfs_hint_6
use import German_pfs_hint_5
use import German_pfs_hint_4
use import German_pfs_hint_3
use import German_pfs_hint_2
use import German_pfs_hint_1

goal preservation:
    (invariantX129 /\ invariant638 /\ invariant1086 /\ invariantX323 /\ invariantX196 /\ invariantX516 /\ invariant506 /\ invariantX839 /\ invariantX74 /\ invariantX395 /\ invariantX11 /\ invariantX587 /\ invariantX716 /\ invariantX142 /\ invariant1073 /\ invariantX1361 /\ invariantX274 /\ invariantX850 /\ invariant1132 /\ invariantX341 /\ invariantX22 /\ invariant873 /\ invariantX282 /\ invariantX795 /\ invariantX539 /\ invariantX668 /\ invariantX221 /\ invariantX35 /\ invariantX358 /\ invariant1114 /\ invariantX298 /\ invariantX172 /\ invariant1108 /\ invariantX110 /\ invariantX46 /\ invariant1106 /\ invariantX431 /\ invariant1104 /\ invariant526 /\ invariantX563 /\ invariantX308 /\ invariantX820 /\ invariantX500 /\ invariantX246 /\ invariant648 /\ invariant1160 /\ invariantX57 /\ invariantX762 /\ invariantX444 /\ invariant1 /\ invariantX576 /\ tau)
    ->
    (invariantX129' /\ invariant638' /\ invariant1086' /\ invariantX323' /\ invariantX196' /\ invariantX516' /\ invariant506' /\ invariantX839' /\ invariantX74' /\ invariantX395' /\ invariantX11' /\ invariantX587' /\ invariantX716' /\ invariantX142' /\ invariant1073' /\ invariantX1361' /\ invariantX274' /\ invariantX850' /\ invariant1132' /\ invariantX341' /\ invariantX22' /\ invariant873' /\ invariantX282' /\ invariantX795' /\ invariantX539' /\ invariantX668' /\ invariantX221' /\ invariantX35' /\ invariantX358' /\ invariant1114' /\ invariantX298' /\ invariantX172' /\ invariant1108' /\ invariantX110' /\ invariantX46' /\ invariant1106' /\ invariantX431' /\ invariant1104' /\ invariant526' /\ invariantX563' /\ invariantX308' /\ invariantX820' /\ invariantX500' /\ invariantX246' /\ invariant648' /\ invariant1160' /\ invariantX57' /\ invariantX762' /\ invariantX444' /\ invariant1' /\ invariantX576')


end