theory Szymanski_at_defs

use import bool.Bool
use import int.Int

type location = L0 | L1 | L2 | L3 | L4 | L5 | L6 | L7

function a int : location
function b int : bool
function s int : bool
function w int : bool
function a' int : location
function b' int : bool
function s' int : bool
function w' int : bool

end


theory Szymanski_at_invpreds

use import bool.Bool
use import int.Int
use import Szymanski_at_defs

predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L7 /\
(a z2) = L7)

predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L7 /\
(a' z2) = L7)

predicate invariantX159 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L6 /\
(a z2) = L4)

predicate invariantX159' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L6 /\
(a' z2) = L4)

predicate invariant129 =
not (exists z1:int. (a z1) = L6 /\
(b z1) = True)

predicate invariant129' =
not (exists z1:int. (a' z1) = L6 /\
(b' z1) = True)

predicate invariant258 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L7 /\
(a z2) = L2)

predicate invariant258' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L7 /\
(a' z2) = L2)

predicate invariant418 =
not (exists z1:int. (a z1) = L6 /\
(w z1) = True)

predicate invariant418' =
not (exists z1:int. (a' z1) = L6 /\
(w' z1) = True)

predicate invariant162 =
not (exists z1:int. (a z1) = L2 /\
(b z1) = True)

predicate invariant162' =
not (exists z1:int. (a' z1) = L2 /\
(b' z1) = True)

predicate invariant68 =
not (exists z1:int. (a z1) = L5 /\
(s z1) = False)

predicate invariant68' =
not (exists z1:int. (a' z1) = L5 /\
(s' z1) = False)

predicate invariant389 =
not (exists z1:int. (a z1) = L0 /\
(w z1) = True)

predicate invariant389' =
not (exists z1:int. (a' z1) = L0 /\
(w' z1) = True)

predicate invariant38 =
not (exists z1 z2:int. z1 <> z2 /\ z2 <= z1 /\
(a z1) = L7 /\
(a z2) = L5 /\
(w z1) = False)

predicate invariant38' =
not (exists z1 z2:int. z1 <> z2 /\ z2 <= z1 /\
(a' z1) = L7 /\
(a' z2) = L5 /\
(w' z1) = False)

predicate invariant455 =
not (exists z1:int. (a z1) = L0 /\
(s z1) = True)

predicate invariant455' =
not (exists z1:int. (a' z1) = L0 /\
(s' z1) = True)

predicate invariantX182 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L7 /\
(a z2) = L3)

predicate invariantX182' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L7 /\
(a' z2) = L3)

predicate invariantX212 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L6 /\
(a z2) = L3)

predicate invariantX212' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L6 /\
(a' z2) = L3)

predicate invariant429 =
not (exists z1:int. (a z1) = L5 /\
(w z1) = True)

predicate invariant429' =
not (exists z1:int. (a' z1) = L5 /\
(w' z1) = True)

predicate invariant141 =
not (exists z1:int. (a z1) = L5 /\
(b z1) = True)

predicate invariant141' =
not (exists z1:int. (a' z1) = L5 /\
(b' z1) = True)

predicate invariantX307 =
not (exists z1:int. (a z1) = L2 /\
(s z1) = True)

predicate invariantX307' =
not (exists z1:int. (a' z1) = L2 /\
(s' z1) = True)

predicate invariant302 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L6 /\
(a z2) = L2)

predicate invariant302' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L6 /\
(a' z2) = L2)

predicate invariant78 =
not (exists z1:int. (a z1) = L3 /\
(s z1) = False)

predicate invariant78' =
not (exists z1:int. (a' z1) = L3 /\
(s' z1) = False)

predicate invariantX18 =
not (exists z1:int. (a z1) = L7 /\
(s z1) = False)

predicate invariantX18' =
not (exists z1:int. (a' z1) = L7 /\
(s' z1) = False)

predicate invariantX241 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L5 /\
(a z2) = L2)

predicate invariantX241' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L5 /\
(a' z2) = L2)

predicate invariant16 =
not (exists z1 z2:int. z1 <> z2 /\ z2 <= z1 /\
(a z1) = L7 /\
(a z2) = L6)

predicate invariant16' =
not (exists z1 z2:int. z1 <> z2 /\ z2 <= z1 /\
(a' z1) = L7 /\
(a' z2) = L6)

predicate invariantX109 =
not (exists z1:int. (a z1) = L4 /\
(b z1) = True)

predicate invariantX109' =
not (exists z1:int. (a' z1) = L4 /\
(b' z1) = True)

predicate invariantX171 =
not (exists z1:int. (a z1) = L4 /\
(w z1) = False)

predicate invariantX171' =
not (exists z1:int. (a' z1) = L4 /\
(w' z1) = False)

predicate invariant150 =
not (exists z1:int. (a z1) = L3 /\
(b z1) = True)

predicate invariant150' =
not (exists z1:int. (a' z1) = L3 /\
(b' z1) = True)

predicate invariant56 =
not (exists z1:int. (a z1) = L6 /\
(s z1) = False)

predicate invariant56' =
not (exists z1:int. (a' z1) = L6 /\
(s' z1) = False)

predicate invariant409 =
not (exists z1:int. (a z1) = L7 /\
(w z1) = True)

predicate invariant409' =
not (exists z1:int. (a' z1) = L7 /\
(w' z1) = True)

predicate invariantX262 =
not (exists z1:int. (a z1) = L2 /\
(w z1) = True)

predicate invariantX262' =
not (exists z1:int. (a' z1) = L2 /\
(w' z1) = True)

predicate invariantX230 =
not (exists z1:int. (a z1) = L3 /\
(w z1) = False)

predicate invariantX230' =
not (exists z1:int. (a' z1) = L3 /\
(w' z1) = False)

predicate invariant379 =
not (exists z1:int. (a z1) = L1 /\
(w z1) = True)

predicate invariant379' =
not (exists z1:int. (a' z1) = L1 /\
(w' z1) = True)

predicate invariant444 =
not (exists z1:int. (a z1) = L1 /\
(s z1) = True)

predicate invariant444' =
not (exists z1:int. (a' z1) = L1 /\
(s' z1) = True)

predicate invariantX66 =
not (exists z1:int. (a z1) = L7 /\
(b z1) = True)

predicate invariantX66' =
not (exists z1:int. (a' z1) = L7 /\
(b' z1) = True)

predicate invariantX129 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L7 /\
(a z2) = L4)

predicate invariantX129' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L7 /\
(a' z2) = L4)


end


theory Szymanski_at_trdefs

use import bool.Bool
use import int.Int
use import Szymanski_at_defs

predicate transition__t1 =
(* transition t1 *)
(exists x:int. 
( (* requires *)
(a x) = L1
/\ (forall y:int.x = y \/ 
((s y) = False))
) /\
( (* actions *)
(forall _j3:int.
(if _j3 = x then
 (a' _j3) = L2
else (a' _j3) = (a _j3))) /\
(forall _j4:int.
(if _j4 = x then
 (b' _j4) = False
else (b' _j4) = (b _j4))) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t6 =
(* transition t6 *)
(exists x:int. 
( (* requires *)
(a x) = L6
/\ (forall j:int.x = j \/ 
(x <= j) \/
((s j) = False))
) /\
( (* actions *)
(forall _j16:int.
(if _j16 = x then
 (a' _j16) = L7
else (a' _j16) = (a _j16))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t3_then =
(* transition t3_then *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L3 /\
(b y) = False /\
(w y) = False) /\
( (* actions *)
(forall _j8:int.
(if _j8 = x then
 (a' _j8) = L4
else (a' _j8) = (a _j8))) /\
(forall _j9:int.
(if _j9 = x then
 (s' _j9) = False
else (s' _j9) = (s _j9))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t7 =
(* transition t7 *)
(exists x:int. 
( (* requires *)
(a x) = L7) /\
( (* actions *)
(forall _j17:int.
(if _j17 = x then
 (a' _j17) = L0
else (a' _j17) = (a _j17))) /\
(forall _j18:int.
(if _j18 = x then
 (s' _j18) = False
else (s' _j18) = (s _j18))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t5 =
(* transition t5 *)
(exists x:int. 
( (* requires *)
(a x) = L5
/\ (forall y:int.x = y \/ 
((w y) = False))
) /\
( (* actions *)
(forall _j15:int.
(if _j15 = x then
 (a' _j15) = L6
else (a' _j15) = (a _j15))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t0 =
(* transition t0 *)
(exists x:int. 
( (* requires *)
(a x) = L0) /\
( (* actions *)
(forall _j1:int.
(if _j1 = x then
 (a' _j1) = L1
else (a' _j1) = (a _j1))) /\
(forall _j2:int.
(if _j2 = x then
 (b' _j2) = True
else (b' _j2) = (b _j2))) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t4 =
(* transition t4 *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L4 /\
(s y) = True /\
(w y) = False) /\
( (* actions *)
(forall _j12:int.
(if _j12 = x then
 (a' _j12) = L5
else (a' _j12) = (a _j12))) /\
(forall _j13:int.
(if _j13 = x then
 (s' _j13) = True
else (s' _j13) = (s _j13))) /\
(forall _j14:int.
(if _j14 = x then
 (w' _j14) = False
else (w' _j14) = (w _j14))) /\
(forall z1:int. b' z1 = b z1) ))


predicate transition__t2 =
(* transition t2 *)
(exists x:int. 
( (* requires *)
(a x) = L2) /\
( (* actions *)
(forall _j5:int.
(if _j5 = x then
 (a' _j5) = L3
else (a' _j5) = (a _j5))) /\
(forall _j6:int.
(if _j6 = x then
 (s' _j6) = True
else (s' _j6) = (s _j6))) /\
(forall _j7:int.
(if _j7 = x then
 (w' _j7) = True
else (w' _j7) = (w _j7))) /\
(forall z1:int. b' z1 = b z1) ))


predicate transition__t3_else =
(* transition t3_else *)
(exists x:int. 
( (* requires *)
(a x) = L3
/\ (forall y:int.x = y \/ 
((b y) = True) \/
((w y) = True))
) /\
( (* actions *)
(forall _j10:int.
(if _j10 = x then
 (a' _j10) = L5
else (a' _j10) = (a _j10))) /\
(forall _j11:int.
(if _j11 = x then
 (w' _j11) = False
else (w' _j11) = (w _j11))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) ))


predicate tau =
(transition__t3_else \/ transition__t2 \/ transition__t4 \/ transition__t0 \/ transition__t5 \/ transition__t7 \/ transition__t3_then \/ transition__t6 \/ transition__t1)


end


theory Szymanski_at_initialisation

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds

predicate init =
    forall x:int. ((a x) = L0 /\
(b x) = False /\
(s x) = False /\
(w x) = False)

goal initialisation:
    init -> (invariantX129 /\ invariantX66 /\ invariant444 /\ invariant379 /\ invariantX230 /\ invariantX262 /\ invariant409 /\ invariant56 /\ invariant150 /\ invariantX171 /\ invariantX109 /\ invariant16 /\ invariantX241 /\ invariantX18 /\ invariant78 /\ invariant302 /\ invariantX307 /\ invariant141 /\ invariant429 /\ invariantX212 /\ invariantX182 /\ invariant455 /\ invariant38 /\ invariant389 /\ invariant68 /\ invariant162 /\ invariant418 /\ invariant258 /\ invariant129 /\ invariantX159 /\ invariant1)


end


theory Szymanski_at_property

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds

goal property:
    (invariantX129 /\ invariantX66 /\ invariant444 /\ invariant379 /\ invariantX230 /\ invariantX262 /\ invariant409 /\ invariant56 /\ invariant150 /\ invariantX171 /\ invariantX109 /\ invariant16 /\ invariantX241 /\ invariantX18 /\ invariant78 /\ invariant302 /\ invariantX307 /\ invariant141 /\ invariant429 /\ invariantX212 /\ invariantX182 /\ invariant455 /\ invariant38 /\ invariant389 /\ invariant68 /\ invariant162 /\ invariant418 /\ invariant258 /\ invariant129 /\ invariantX159 /\ invariant1) -> (not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L7 /\
(a z2) = L7))


end


theory Szymanski_at_hint_1

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_1:
    (invariantX307 /\ invariantX262 /\ invariant444 /\  tau)
    -> invariantX307'



end


theory Szymanski_at_hint_2

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_2:
    (invariantX262 /\ invariant379 /\  tau)
    -> invariantX262'



end


theory Szymanski_at_hint_3

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_3:
    (invariantX307 /\ invariantX262 /\ invariantX241 /\ invariantX230 /\ invariantX171 /\ invariantX159 /\ invariantX129 /\ invariant68 /\ invariant141 /\ invariant162 /\ invariant429 /\ invariant444 /\ invariant455 /\  tau)
    -> invariantX241'



end


theory Szymanski_at_hint_4

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_4:
    (invariantX230 /\  tau)
    -> invariantX230'



end


theory Szymanski_at_hint_5

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_5:
    (invariantX230 /\ invariantX212 /\ invariant56 /\ invariant129 /\ invariant302 /\ invariant418 /\  tau)
    -> invariantX212'



end


theory Szymanski_at_hint_6

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_6:
    (invariantX212 /\ invariantX182 /\ invariantX66 /\ invariantX18 /\ invariant258 /\ invariant409 /\  tau)
    -> invariantX182'



end


theory Szymanski_at_hint_7

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_7:
    (invariantX230 /\ invariantX171 /\ invariantX109 /\  tau)
    -> invariantX171'



end


theory Szymanski_at_hint_8

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_8:
    (invariantX212 /\ invariantX171 /\ invariantX159 /\ invariant56 /\ invariant129 /\ invariant418 /\  tau)
    -> invariantX159'



end


theory Szymanski_at_hint_9

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_9:
    (invariantX182 /\ invariantX159 /\ invariantX129 /\ invariantX66 /\ invariantX18 /\ invariant409 /\  tau)
    -> invariantX129'



end


theory Szymanski_at_hint_10

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_10:
    (invariantX109 /\ invariant150 /\  tau)
    -> invariantX109'



end


theory Szymanski_at_hint_11

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_11:
    (invariantX66 /\ invariantX18 /\ invariant129 /\  tau)
    -> invariantX66'



end


theory Szymanski_at_hint_12

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_12:
    (invariantX18 /\ invariant56 /\  tau)
    -> invariantX18'



end


theory Szymanski_at_hint_13

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_13:
    (invariantX66 /\ invariantX18 /\ invariant1 /\ invariant16 /\ invariant409 /\  tau)
    -> invariant1'



end


theory Szymanski_at_hint_14

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_14:
    (invariantX66 /\ invariantX18 /\ invariant16 /\ invariant38 /\ invariant56 /\ invariant409 /\  tau)
    -> invariant16'



end


theory Szymanski_at_hint_15

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_15:
    (invariantX129 /\ invariantX66 /\ invariantX18 /\ invariant38 /\ invariant68 /\  tau)
    -> invariant38'



end


theory Szymanski_at_hint_16

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_16:
    (invariant56 /\ invariant68 /\  tau)
    -> invariant56'



end


theory Szymanski_at_hint_17

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_17:
    (invariant68 /\ invariant78 /\  tau)
    -> invariant68'



end


theory Szymanski_at_hint_18

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_18:
    (invariantX230 /\ invariant78 /\  tau)
    -> invariant78'



end


theory Szymanski_at_hint_19

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_19:
    (invariant56 /\ invariant129 /\ invariant141 /\  tau)
    -> invariant129'



end


theory Szymanski_at_hint_20

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_20:
    (invariantX109 /\ invariant68 /\ invariant141 /\ invariant150 /\  tau)
    -> invariant141'



end


theory Szymanski_at_hint_21

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_21:
    (invariantX230 /\ invariant78 /\ invariant150 /\ invariant162 /\  tau)
    -> invariant150'



end


theory Szymanski_at_hint_22

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_22:
    (invariantX307 /\ invariantX262 /\ invariant162 /\  tau)
    -> invariant162'



end


theory Szymanski_at_hint_23

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_23:
    (invariantX66 /\ invariantX18 /\ invariant258 /\ invariant302 /\ invariant409 /\  tau)
    -> invariant258'



end


theory Szymanski_at_hint_24

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_24:
    (invariantX241 /\ invariant56 /\ invariant129 /\ invariant302 /\ invariant418 /\  tau)
    -> invariant302'



end


theory Szymanski_at_hint_25

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_25:
    (invariant379 /\ invariant389 /\  tau)
    -> invariant379'



end


theory Szymanski_at_hint_26

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_26:
    (invariant389 /\ invariant409 /\  tau)
    -> invariant389'



end


theory Szymanski_at_hint_27

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_27:
    (invariantX66 /\ invariantX18 /\ invariant409 /\ invariant418 /\  tau)
    -> invariant409'



end


theory Szymanski_at_hint_28

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_28:
    (invariant56 /\ invariant129 /\ invariant418 /\ invariant429 /\  tau)
    -> invariant418'



end


theory Szymanski_at_hint_29

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_29:
    (invariant68 /\ invariant141 /\ invariant429 /\  tau)
    -> invariant429'



end


theory Szymanski_at_hint_30

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_30:
    (invariant379 /\ invariant444 /\ invariant455 /\  tau)
    -> invariant444'



end


theory Szymanski_at_hint_31

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs

lemma hint_31:
    (invariant389 /\ invariant455 /\  tau)
    -> invariant455'



end


theory Szymanski_at_preservation

use import bool.Bool
use import int.Int
use import Szymanski_at_defs
use import Szymanski_at_invpreds
use import Szymanski_at_trdefs
use import Szymanski_at_hint_31
use import Szymanski_at_hint_30
use import Szymanski_at_hint_29
use import Szymanski_at_hint_28
use import Szymanski_at_hint_27
use import Szymanski_at_hint_26
use import Szymanski_at_hint_25
use import Szymanski_at_hint_24
use import Szymanski_at_hint_23
use import Szymanski_at_hint_22
use import Szymanski_at_hint_21
use import Szymanski_at_hint_20
use import Szymanski_at_hint_19
use import Szymanski_at_hint_18
use import Szymanski_at_hint_17
use import Szymanski_at_hint_16
use import Szymanski_at_hint_15
use import Szymanski_at_hint_14
use import Szymanski_at_hint_13
use import Szymanski_at_hint_12
use import Szymanski_at_hint_11
use import Szymanski_at_hint_10
use import Szymanski_at_hint_9
use import Szymanski_at_hint_8
use import Szymanski_at_hint_7
use import Szymanski_at_hint_6
use import Szymanski_at_hint_5
use import Szymanski_at_hint_4
use import Szymanski_at_hint_3
use import Szymanski_at_hint_2
use import Szymanski_at_hint_1

goal preservation:
    (invariantX129 /\ invariantX66 /\ invariant444 /\ invariant379 /\ invariantX230 /\ invariantX262 /\ invariant409 /\ invariant56 /\ invariant150 /\ invariantX171 /\ invariantX109 /\ invariant16 /\ invariantX241 /\ invariantX18 /\ invariant78 /\ invariant302 /\ invariantX307 /\ invariant141 /\ invariant429 /\ invariantX212 /\ invariantX182 /\ invariant455 /\ invariant38 /\ invariant389 /\ invariant68 /\ invariant162 /\ invariant418 /\ invariant258 /\ invariant129 /\ invariantX159 /\ invariant1 /\ tau)
    ->
    (invariantX129' /\ invariantX66' /\ invariant444' /\ invariant379' /\ invariantX230' /\ invariantX262' /\ invariant409' /\ invariant56' /\ invariant150' /\ invariantX171' /\ invariantX109' /\ invariant16' /\ invariantX241' /\ invariantX18' /\ invariant78' /\ invariant302' /\ invariantX307' /\ invariant141' /\ invariant429' /\ invariantX212' /\ invariantX182' /\ invariant455' /\ invariant38' /\ invariant389' /\ invariant68' /\ invariant162' /\ invariant418' /\ invariant258' /\ invariant129' /\ invariantX159' /\ invariant1')


end