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 <->
(exists x:int.
(
flag = False /\
(cache x) <> Exclusive /\
(chan1 x) = Empty1) /\
(
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 <->
(exists x:int.
(
flag = True /\
(invset x) = (shrset x)
/\ (forall j:int.x = j \/
((invset j) = (shrset j)))
) /\
(
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 <->
(exists x:int.
(
exgntd = True /\
curcmd = Reqs /\
flag = False /\
(chan2 x) = Empty2 /\
(invset x) = True) /\
(
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 <->
(exists x:int.
(
flag = False /\
(cache x) = Invalid /\
(chan1 x) = Empty1) /\
(
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 <->
(exists x:int.
(
curcmd = Empty1 /\
flag = False /\
(chan1 x) = Reqs) /\
(
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 <->
(exists x:int.
(
curcmd <> Empty1 /\
flag = False /\
(chan3 x) = Invack) /\
(
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 <->
(exists x:int.
(
curcmd = Reqe /\
flag = False /\
(chan2 x) = Empty2 /\
(invset x) = True) /\
(
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 <->
(exists x:int.
(
flag = False /\
(chan2 x) = Gnte) /\
(
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 <->
(exists x:int.
(
flag = True /\
(shrset x) = False) /\
(
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 <->
(exists x:int.
(
curcmd = Empty1 /\
flag = False /\
(chan1 x) = Reqe) /\
(
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 <->
(exists x:int.
(
curcmd = Reqe /\
flag = False /\
(chan2 x) = Empty2 /\
(curptr x) = True /\
(shrset x) = False
/\ (forall j:int.x = j \/
((shrset j) = False))
) /\
(
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 <->
(exists x:int.
(
flag = False /\
(chan2 x) = Inv /\
(chan3 x) = Empty3) /\
(
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 <->
(exists x:int.
(
exgntd = False /\
curcmd = Reqs /\
flag = False /\
(chan2 x) = Empty2 /\
(curptr x) = True) /\
(
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 <->
(exists x:int.
(
flag = False /\
(chan2 x) = Gnts) /\
(
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 <->
(exists x:int.
(
flag = True /\
(shrset x) = True) /\
(
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