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 =
(exists x:int.
(
(a x) = L1
/\ (forall y:int.x = y \/
((s y) = False))
) /\
(
(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 =
(exists x:int.
(
(a x) = L6
/\ (forall j:int.x = j \/
(x <= j) \/
((s j) = False))
) /\
(
(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 =
(exists x y:int. x <> y /\
(
(a x) = L3 /\
(b y) = False /\
(w y) = False) /\
(
(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 =
(exists x:int.
(
(a x) = L7) /\
(
(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 =
(exists x:int.
(
(a x) = L5
/\ (forall y:int.x = y \/
((w y) = False))
) /\
(
(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 =
(exists x:int.
(
(a x) = L0) /\
(
(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 =
(exists x y:int. x <> y /\
(
(a x) = L4 /\
(s y) = True /\
(w y) = False) /\
(
(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 =
(exists x:int.
(
(a x) = L2) /\
(
(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 =
(exists x:int.
(
(a x) = L3
/\ (forall y:int.x = y \/
((b y) = True) \/
((w y) = True))
) /\
(
(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