```theory Bakery_defs

use import int.Int

type t = Idle | Wait | Crit | Crash

function a int : t
function a' int : t

end

theory Bakery_invpreds

use import int.Int
use import Bakery_defs

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

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

predicate invariant3 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = Crit /\
(a z2) = Wait)

predicate invariant3' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = Crit /\
(a' z2) = Wait)

end

theory Bakery_trdefs

use import int.Int
use import Bakery_defs

predicate transition__tr3 =
(* transition tr3 *)
(exists z:int.
( (* requires *)
(a z) = Crit) /\
( (* actions *)
(forall j:int.
if j = z then
a' j = Idle
else a' j = (a j))))

predicate transition__tr2 =
(* transition tr2 *)
(exists z:int.
( (* requires *)
(a z) = Wait) /\
( (* actions *)
(forall j:int.
if j = z then
a' j = Crit
else if z < j then
a' j = (a j)
else if j < z /\
(a j) = Idle then
a' j = Idle
else a' j = Crash)))

predicate transition__tr1 =
(* transition tr1 *)
(exists z:int.
( (* requires *)
(a z) = Idle) /\
( (* actions *)
(forall j:int.
if j = z then
a' j = Wait
else if j < z then
a' j = (a j)
else if z < j /\
(a j) = Idle then
a' j = (a j)
else a' j = Crash)))

predicate tau =
(transition__tr1 \/ transition__tr2 \/ transition__tr3)

end

theory Bakery_initialisation

use import int.Int
use import Bakery_defs
use import Bakery_invpreds

predicate init =
forall z:int. ((a z) = Idle)

goal initialisation:
init -> (invariant3 /\ invariant1)

end

theory Bakery_property

use import int.Int
use import Bakery_defs
use import Bakery_invpreds

goal property:
(invariant3 /\ invariant1) -> (not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit))

end

theory Bakery_hint_1

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs

lemma hint_1:
(invariant1 /\ invariant3 /\ tau)
-> invariant1'

end

theory Bakery_hint_2

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs

lemma hint_2:
(invariant3 /\ tau)
-> invariant3'

end

theory Bakery_preservation

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs
use import Bakery_hint_2
use import Bakery_hint_1

goal preservation:
(invariant3 /\ invariant1 /\ tau)
->
(invariant3' /\ invariant1')

end

```