theory Szymanski_na_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 cpt int int : bool
function a' int : location
function b' int : bool
function s' int : bool
function w' int : bool
function cpt' int int : bool

end


theory Szymanski_na_invpreds

use import bool.Bool
use import int.Int
use import Szymanski_na_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 invariantX62 =
not (exists z1:int. (a z1) = L7 /\
(s z1) = False)

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

predicate invariant67 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = L7 /\
(a z2) = L5 /\
(cpt z2 z1) = True)

predicate invariant67' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = L7 /\
(a' z2) = L5 /\
(cpt' z2 z1) = True)

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

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

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

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

predicate invariant73 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = L6 /\
(a z2) = L6 /\
(cpt z1 z2) = True)

predicate invariant73' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = L6 /\
(a' z2) = L6 /\
(cpt' z1 z2) = True)

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

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

predicate invariant330 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = L6 /\
(a z2) = L5 /\
(w z1) = False /\
(cpt z1 z2) = True /\
(cpt z2 z1) = False)

predicate invariant330' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = L6 /\
(a' z2) = L5 /\
(w' z1) = False /\
(cpt' z1 z2) = True /\
(cpt' z2 z1) = False)

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

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

predicate invariantX245 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L1 /\
(cpt z1 z2) = True)

predicate invariantX245' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L1 /\
(cpt' z1 z2) = True)

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

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

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

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

predicate invariant592 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L3 /\
(a z2) = L2 /\
(cpt z1 z2) = True)

predicate invariant592' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L3 /\
(a' z2) = L2 /\
(cpt' z1 z2) = True)

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

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

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

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

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

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

predicate invariant723 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L0 /\
(cpt z1 z2) = True)

predicate invariant723' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L0 /\
(cpt' z1 z2) = True)

predicate invariant1237 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L5 /\
(a z2) = L4 /\
(cpt z1 z2) = True)

predicate invariant1237' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L5 /\
(a' z2) = L4 /\
(cpt' z1 z2) = True)

predicate invariant150 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = L6 /\
(a z2) = L5 /\
(cpt z1 z2) = True /\
(cpt z2 z1) = True)

predicate invariant150' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = L6 /\
(a' z2) = L5 /\
(cpt' z1 z2) = True /\
(cpt' z2 z1) = True)

predicate invariantX233 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L2 /\
(cpt z1 z2) = True)

predicate invariantX233' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L2 /\
(cpt' z1 z2) = True)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

predicate invariant486 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L5 /\
(a z2) = L3 /\
(cpt z1 z2) = True)

predicate invariant486' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = L5 /\
(a' z2) = L3 /\
(cpt' z1 z2) = True)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


end


theory Szymanski_na_trdefs

use import bool.Bool
use import int.Int
use import Szymanski_na_defs

predicate transition__t4_exit_for =
(* transition t4_exit_for *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L4 /\
(s y) = True /\
(w y) = False /\
(cpt x y) = False) /\
( (* actions *)
(forall _j20:int.
(if _j20 = x then
 (a' _j20) = L5
else (a' _j20) = (a _j20))) /\
(forall _j21:int.
(if _j21 = x then
 (s' _j21) = True
else (s' _j21) = (s _j21))) /\
(forall _j22:int.
(if _j22 = x then
 (w' _j22) = False
else (w' _j22) = (w _j22))) /\
(forall i j:int.
(if i = x then
 (cpt' i j) = False
else (cpt' i j) = (cpt i j))) /\
(forall z1:int. b' z1 = b z1) ))


predicate transition__t3_abort_for =
(* transition t3_abort_for *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L3 /\
(b y) = False /\
(w y) = False /\
(cpt x 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 i j:int.
(if i = x then
 (cpt' i j) = False
else (cpt' i j) = (cpt i j))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t4_restart_for =
(* transition t4_restart_for *)
(exists x:int. 
( (* requires *)
(a x) = L4
/\ (forall y:int.x = y \/ 
((cpt x y) = True))
) /\
( (* actions *)
(forall i j:int.
(if i = x then
 (cpt' i j) = False
else (cpt' i j) = (cpt i j))) /\
(forall z1:int. a' z1 = a z1) /\
(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) /\
(forall z1 z2:int. cpt' z1 z2 = cpt z1 z2) ))


predicate transition__t5_enter_for =
(* transition t5_enter_for *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L5 /\
(w y) = False /\
(cpt x y) = False) /\
( (* actions *)
(forall _j23 _j24:int.
(if _j23 = x /\
_j24 = y then
 (cpt' _j23 _j24) = True
else (cpt' _j23 _j24) = (cpt _j23 _j24))) /\
(forall z1:int. a' z1 = a z1) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


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) /\
(forall z1 z2:int. cpt' z1 z2 = cpt z1 z2) ))


predicate transition__t6_exit_for =
(* transition t6_exit_for *)
(exists x:int. 
( (* requires *)
(a x) = L6
/\ (forall y:int.x = y \/ 
(x < y) \/
((cpt x y) = True))
) /\
( (* actions *)
(forall _j28:int.
(if _j28 = x then
 (a' _j28) = L7
else (a' _j28) = (a _j28))) /\
(forall i j:int.
(if i = x then
 (cpt' i j) = False
else (cpt' i j) = (cpt i j))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t4_incr_for2 =
(* transition t4_incr_for2 *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L4 /\
(w y) = True /\
(cpt x y) = False) /\
( (* actions *)
(forall _j18 _j19:int.
(if _j18 = x /\
_j19 = y then
 (cpt' _j18 _j19) = True
else (cpt' _j18 _j19) = (cpt _j18 _j19))) /\
(forall z1:int. a' z1 = a z1) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t4_incr_for1 =
(* transition t4_incr_for1 *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L4 /\
(s y) = False /\
(cpt x y) = False) /\
( (* actions *)
(forall _j16 _j17:int.
(if _j16 = x /\
_j17 = y then
 (cpt' _j16 _j17) = True
else (cpt' _j16 _j17) = (cpt _j16 _j17))) /\
(forall z1:int. a' z1 = a z1) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t3_incr_for1 =
(* transition t3_incr_for1 *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L3 /\
(b y) = True /\
(cpt x y) = False) /\
( (* actions *)
(forall _j10 _j11:int.
(if _j10 = x /\
_j11 = y then
 (cpt' _j10 _j11) = True
else (cpt' _j10 _j11) = (cpt _j10 _j11))) /\
(forall z1:int. a' z1 = a z1) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t6_enter_for =
(* transition t6_enter_for *)
(exists x y:int. x <> y /\ 
( (* requires *)
y < x /\
(a x) = L6 /\
(s y) = False /\
(cpt x y) = False) /\
( (* actions *)
(forall _j26 _j27:int.
(if _j26 = x /\
_j27 = y then
 (cpt' _j26 _j27) = True
else (cpt' _j26 _j27) = (cpt _j26 _j27))) /\
(forall z1:int. a' z1 = a z1) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t3_incr_for2 =
(* transition t3_incr_for2 *)
(exists x y:int. x <> y /\ 
( (* requires *)
(a x) = L3 /\
(w y) = True /\
(cpt x y) = False) /\
( (* actions *)
(forall _j12 _j13:int.
(if _j12 = x /\
_j13 = y then
 (cpt' _j12 _j13) = True
else (cpt' _j12 _j13) = (cpt _j12 _j13))) /\
(forall z1:int. a' z1 = a z1) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w z1) ))


predicate transition__t3_exit_for =
(* transition t3_exit_for *)
(exists x:int. 
( (* requires *)
(a x) = L3
/\ (forall y:int.x = y \/ 
((cpt x y) = True))
) /\
( (* actions *)
(forall _j14:int.
(if _j14 = x then
 (a' _j14) = L5
else (a' _j14) = (a _j14))) /\
(forall _j15:int.
(if _j15 = x then
 (w' _j15) = False
else (w' _j15) = (w _j15))) /\
(forall i j:int.
(if i = x then
 (cpt' i j) = False
else (cpt' i j) = (cpt i j))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) ))


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


predicate transition__t5_exit_for =
(* transition t5_exit_for *)
(exists x:int. 
( (* requires *)
(a x) = L5
/\ (forall y:int.x = y \/ 
((cpt x y) = True))
) /\
( (* actions *)
(forall _j25:int.
(if _j25 = x then
 (a' _j25) = L6
else (a' _j25) = (a _j25))) /\
(forall i j:int.
(if i = x then
 (cpt' i j) = False
else (cpt' i j) = (cpt i j))) /\
(forall z1:int. b' z1 = b z1) /\
(forall z1:int. s' z1 = s z1) /\
(forall z1:int. w' z1 = w 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) /\
(forall z1 z2:int. cpt' z1 z2 = cpt z1 z2) ))


predicate tau =
(transition__t2 \/ transition__t5_exit_for \/ transition__t7 \/ transition__t3_exit_for \/ transition__t3_incr_for2 \/ transition__t6_enter_for \/ transition__t3_incr_for1 \/ transition__t4_incr_for1 \/ transition__t4_incr_for2 \/ transition__t6_exit_for \/ transition__t1 \/ transition__t5_enter_for \/ transition__t0 \/ transition__t4_restart_for \/ transition__t3_abort_for \/ transition__t4_exit_for)


end


theory Szymanski_na_initialisation

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds

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

goal initialisation:
    init -> (invariant255 /\ invariant1020 /\ invariant954 /\ invariant377 /\ invariantX393 /\ invariantX204 /\ invariantX463 /\ invariantX143 /\ invariant238 /\ invariantX276 /\ invariant486 /\ invariant1061 /\ invariant33 /\ invariant32 /\ invariant1115 /\ invariantX294 /\ invariant216 /\ invariantX361 /\ invariantX233 /\ invariant150 /\ invariant1237 /\ invariant723 /\ invariant1041 /\ invariantX175 /\ invariant976 /\ invariant592 /\ invariantX434 /\ invariant141 /\ invariantX245 /\ invariant842 /\ invariant330 /\ invariant457 /\ invariant73 /\ invariantX312 /\ invariant1093 /\ invariant67 /\ invariantX62 /\ invariant1)


end


theory Szymanski_na_property

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds

goal property:
    (invariant255 /\ invariant1020 /\ invariant954 /\ invariant377 /\ invariantX393 /\ invariantX204 /\ invariantX463 /\ invariantX143 /\ invariant238 /\ invariantX276 /\ invariant486 /\ invariant1061 /\ invariant33 /\ invariant32 /\ invariant1115 /\ invariantX294 /\ invariant216 /\ invariantX361 /\ invariantX233 /\ invariant150 /\ invariant1237 /\ invariant723 /\ invariant1041 /\ invariantX175 /\ invariant976 /\ invariant592 /\ invariantX434 /\ invariant141 /\ invariantX245 /\ invariant842 /\ invariant330 /\ invariant457 /\ invariant73 /\ invariantX312 /\ invariant1093 /\ invariant67 /\ invariantX62 /\ invariant1) -> (not (exists z1 z2:int. z1 <> z2 /\ (a z1) = L7 /\
(a z2) = L7))


end


theory Szymanski_na_hint_1

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_1:
    (invariantX463 /\ invariantX276 /\  tau)
    -> invariantX463'



end


theory Szymanski_na_hint_2

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_2:
    (invariantX434 /\ invariantX175 /\ invariant216 /\ invariant1041 /\ invariant1237 /\  tau)
    -> invariantX434'



end


theory Szymanski_na_hint_3

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_3:
    (invariantX434 /\ invariantX393 /\ invariantX143 /\ invariantX62 /\ invariant1020 /\  tau)
    -> invariantX393'



end


theory Szymanski_na_hint_4

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_4:
    (invariantX361 /\ invariantX312 /\ invariantX294 /\ invariant1093 /\  tau)
    -> invariantX361'



end


theory Szymanski_na_hint_5

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_5:
    (invariantX312 /\ invariantX294 /\ invariant954 /\  tau)
    -> invariantX312'



end


theory Szymanski_na_hint_6

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_6:
    (invariantX294 /\  tau)
    -> invariantX294'



end


theory Szymanski_na_hint_7

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_7:
    (invariantX276 /\  tau)
    -> invariantX276'



end


theory Szymanski_na_hint_8

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_8:
    (invariantX245 /\ invariant723 /\ invariant954 /\ invariant1093 /\  tau)
    -> invariantX245'



end


theory Szymanski_na_hint_9

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_9:
    (invariantX361 /\ invariantX312 /\ invariantX294 /\ invariantX245 /\ invariantX233 /\  tau)
    -> invariantX233'



end


theory Szymanski_na_hint_10

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_10:
    (invariantX463 /\ invariantX434 /\ invariantX393 /\ invariantX361 /\ invariantX276 /\ invariantX204 /\ invariant238 /\ invariant592 /\ invariant1061 /\ invariant1093 /\ invariant1115 /\  tau)
    -> invariantX204'



end


theory Szymanski_na_hint_11

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_11:
    (invariantX175 /\ invariant216 /\ invariant457 /\ invariant486 /\ invariant1041 /\  tau)
    -> invariantX175'



end


theory Szymanski_na_hint_12

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_12:
    (invariantX175 /\ invariantX143 /\ invariantX62 /\ invariant377 /\ invariant1020 /\  tau)
    -> invariantX143'



end


theory Szymanski_na_hint_13

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_13:
    (invariantX62 /\ invariant216 /\  tau)
    -> invariantX62'



end


theory Szymanski_na_hint_14

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_14:
    (invariantX62 /\ invariant1 /\ invariant32 /\ invariant33 /\ invariant1020 /\  tau)
    -> invariant1'



end


theory Szymanski_na_hint_15

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_15:
    (invariantX62 /\ invariant32 /\ invariant67 /\ invariant73 /\ invariant1020 /\  tau)
    -> invariant32'



end


theory Szymanski_na_hint_16

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_16:
    (invariantX62 /\ invariant33 /\ invariant73 /\ invariant1020 /\  tau)
    -> invariant33'



end


theory Szymanski_na_hint_17

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_17:
    (invariantX62 /\ invariant67 /\ invariant141 /\ invariant150 /\ invariant1020 /\  tau)
    -> invariant67'



end


theory Szymanski_na_hint_18

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_18:
    (invariant73 /\ invariant150 /\ invariant216 /\ invariant1041 /\  tau)
    -> invariant73'



end


theory Szymanski_na_hint_19

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_19:
    (invariantX393 /\ invariantX143 /\ invariantX62 /\ invariant141 /\ invariant330 /\  tau)
    -> invariant141'



end


theory Szymanski_na_hint_20

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_20:
    (invariant150 /\ invariant216 /\ invariant238 /\ invariant330 /\ invariant1041 /\  tau)
    -> invariant150'



end


theory Szymanski_na_hint_21

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_21:
    (invariant216 /\ invariant238 /\  tau)
    -> invariant216'



end


theory Szymanski_na_hint_22

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_22:
    (invariant238 /\ invariant255 /\  tau)
    -> invariant238'



end


theory Szymanski_na_hint_23

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_23:
    (invariantX276 /\ invariant255 /\  tau)
    -> invariant255'



end


theory Szymanski_na_hint_24

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_24:
    (invariantX434 /\ invariantX175 /\ invariant216 /\ invariant238 /\ invariant330 /\  tau)
    -> invariant330'



end


theory Szymanski_na_hint_25

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_25:
    (invariantX62 /\ invariant377 /\ invariant457 /\ invariant1020 /\  tau)
    -> invariant377'



end


theory Szymanski_na_hint_26

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_26:
    (invariantX204 /\ invariant216 /\ invariant457 /\ invariant1041 /\  tau)
    -> invariant457'



end


theory Szymanski_na_hint_27

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_27:
    (invariantX276 /\ invariantX204 /\ invariant238 /\ invariant486 /\ invariant1061 /\  tau)
    -> invariant486'



end


theory Szymanski_na_hint_28

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_28:
    (invariantX312 /\ invariantX294 /\ invariantX276 /\ invariantX233 /\ invariant255 /\ invariant592 /\  tau)
    -> invariant592'



end


theory Szymanski_na_hint_29

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_29:
    (invariant723 /\ invariant842 /\ invariant976 /\ invariant1115 /\  tau)
    -> invariant723'



end


theory Szymanski_na_hint_30

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_30:
    (invariantX393 /\ invariantX143 /\ invariantX62 /\ invariant1 /\ invariant377 /\ invariant842 /\ invariant1020 /\  tau)
    -> invariant842'



end


theory Szymanski_na_hint_31

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_31:
    (invariant954 /\ invariant976 /\  tau)
    -> invariant954'



end


theory Szymanski_na_hint_32

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_32:
    (invariant976 /\ invariant1020 /\  tau)
    -> invariant976'



end


theory Szymanski_na_hint_33

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_33:
    (invariantX62 /\ invariant1020 /\ invariant1041 /\  tau)
    -> invariant1020'



end


theory Szymanski_na_hint_34

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_34:
    (invariant216 /\ invariant1041 /\ invariant1061 /\  tau)
    -> invariant1041'



end


theory Szymanski_na_hint_35

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_35:
    (invariant238 /\ invariant1061 /\  tau)
    -> invariant1061'



end


theory Szymanski_na_hint_36

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_36:
    (invariant954 /\ invariant1093 /\ invariant1115 /\  tau)
    -> invariant1093'



end


theory Szymanski_na_hint_37

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_37:
    (invariant976 /\ invariant1115 /\  tau)
    -> invariant1115'



end


theory Szymanski_na_hint_38

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs

lemma hint_38:
    (invariantX463 /\ invariant238 /\ invariant486 /\ invariant1061 /\ invariant1237 /\  tau)
    -> invariant1237'



end


theory Szymanski_na_preservation

use import bool.Bool
use import int.Int
use import Szymanski_na_defs
use import Szymanski_na_invpreds
use import Szymanski_na_trdefs
use import Szymanski_na_hint_38
use import Szymanski_na_hint_37
use import Szymanski_na_hint_36
use import Szymanski_na_hint_35
use import Szymanski_na_hint_34
use import Szymanski_na_hint_33
use import Szymanski_na_hint_32
use import Szymanski_na_hint_31
use import Szymanski_na_hint_30
use import Szymanski_na_hint_29
use import Szymanski_na_hint_28
use import Szymanski_na_hint_27
use import Szymanski_na_hint_26
use import Szymanski_na_hint_25
use import Szymanski_na_hint_24
use import Szymanski_na_hint_23
use import Szymanski_na_hint_22
use import Szymanski_na_hint_21
use import Szymanski_na_hint_20
use import Szymanski_na_hint_19
use import Szymanski_na_hint_18
use import Szymanski_na_hint_17
use import Szymanski_na_hint_16
use import Szymanski_na_hint_15
use import Szymanski_na_hint_14
use import Szymanski_na_hint_13
use import Szymanski_na_hint_12
use import Szymanski_na_hint_11
use import Szymanski_na_hint_10
use import Szymanski_na_hint_9
use import Szymanski_na_hint_8
use import Szymanski_na_hint_7
use import Szymanski_na_hint_6
use import Szymanski_na_hint_5
use import Szymanski_na_hint_4
use import Szymanski_na_hint_3
use import Szymanski_na_hint_2
use import Szymanski_na_hint_1

goal preservation:
    (invariant255 /\ invariant1020 /\ invariant954 /\ invariant377 /\ invariantX393 /\ invariantX204 /\ invariantX463 /\ invariantX143 /\ invariant238 /\ invariantX276 /\ invariant486 /\ invariant1061 /\ invariant33 /\ invariant32 /\ invariant1115 /\ invariantX294 /\ invariant216 /\ invariantX361 /\ invariantX233 /\ invariant150 /\ invariant1237 /\ invariant723 /\ invariant1041 /\ invariantX175 /\ invariant976 /\ invariant592 /\ invariantX434 /\ invariant141 /\ invariantX245 /\ invariant842 /\ invariant330 /\ invariant457 /\ invariant73 /\ invariantX312 /\ invariant1093 /\ invariant67 /\ invariantX62 /\ invariant1 /\ tau)
    ->
    (invariant255' /\ invariant1020' /\ invariant954' /\ invariant377' /\ invariantX393' /\ invariantX204' /\ invariantX463' /\ invariantX143' /\ invariant238' /\ invariantX276' /\ invariant486' /\ invariant1061' /\ invariant33' /\ invariant32' /\ invariant1115' /\ invariantX294' /\ invariant216' /\ invariantX361' /\ invariantX233' /\ invariant150' /\ invariant1237' /\ invariant723' /\ invariant1041' /\ invariantX175' /\ invariant976' /\ invariant592' /\ invariantX434' /\ invariant141' /\ invariantX245' /\ invariant842' /\ invariant330' /\ invariant457' /\ invariant73' /\ invariantX312' /\ invariant1093' /\ invariant67' /\ invariantX62' /\ invariant1')


end