# Re: problem with prover

```I have enclosed chunnel.pvs. The problem arises when i try to prove the
lemma "loopy". I initially tried to (expand "index") but it comes back
with 'no change'. Why? I also tried to (expand "train1") but again 'no
change'. This makes no sense to me??
--
_________________________________________________________________________
Richard Botting                         tel: +44 141 339 8855 ext. 8335
Computing Science                      fax: +44 141 330 4913
University of Glasgow                email: rmb@dcs.gla.ac.uk
Glasgow G12 8QQ
SCOTLAND
__________________________________________________________________________
```
```
defs: THEORY
BEGIN

person_name: NONEMPTY_TYPE

current_indication_values: NONEMPTY_TYPE

mode_values: NONEMPTY_TYPE

train_name: NONEMPTY_TYPE

track_no: NONEMPTY_TYPE

collision_values: TYPE = {collision, no_collision}

condition_status_values: TYPE = {condition_defect, condition_ok}

direction_values: TYPE = {low_to_high, high_to_low}

cp_state: TYPE = {cp_open, cp_closed}

END defs

points: THEORY
BEGIN

ASSUMING

IMPORTING finite_sequences

point_values: TYPE = finseq[real]

points_ax: AXIOM
FORALL (mpv: point_values):
length(mpv) >= 2
AND (FORALL (i: nat): member(i, {n: nat | n <= length(mpv) - 2}) IMPLIES seq(mpv)(i) > seq(mpv)(i + 1))

ENDASSUMING

END points

Position: THEORY
BEGIN

ASSUMING

IMPORTING points

block: TYPE = [real, real]

blocks: TYPE = finseq[block]

blocks_ax: AXIOM
FORALL (b: blocks): (length(b) /= 0 AND (FORALL (i: nat):
member(i, {n: nat | n <= length(b) - 2}) IMPLIES PROJ_2(seq(b)(i)) = PROJ_1(seq(b)(i + 1))))

ENDASSUMING

END Position

Train: THEORY
BEGIN

IMPORTING Position, defs

train:
TYPE =
[# name: train_name,
position: blocks,
max_length: posnat,
collision_status: collision_values,
speed: nat,
direction: direction_values,
mode: mode_values,
condition_status: condition_status_values #]

come_to_stop((t1: train)): train = t1 WITH [speed := 0]

in_collision((t1: train)): train = t1 WITH [collision_status := collision]

change_action((t1: train), (action?: mode_values)): train = t1 WITH [mode := action?]

END Train

my_sequence_ops[T: TYPE]: THEORY    % remember: finite sequences are defined as records.
BEGIN

IMPORTING finite_sequences[T]

finseq1: TYPE = { fs: finseq[T] | length(fs) /= 0 }

sub_seq((fs1: finseq[T]), (fs2: finseq[T])): bool =
length(fs1) <= length(fs2)
AND EXISTS (j: nat):
(j <= length(fs2) - length(fs1) AND (FORALL (i: nat): i < length(fs1) IMPLIES seq(fs1)(i) = seq(fs2)(j + i)))

in_seq((t: T), (fs: finseq[T])): bool = EXISTS (i: below(length(fs))): t = seq(fs)(i)

last((fs: finseq1)): T =  seq(fs)(length(fs) - 1)

tail((fs: finseq[T])): finseq[T] = IF length(fs) = 0 THEN fs
ELSE ^( fs, (1, length(fs) - 1))
ENDIF

front((fs: finseq[T])): finseq[T] = IF length(fs) = 0 THEN fs
ELSIF length(fs) = 1 THEN empty_seq
ELSE ^( fs, (0, length(fs) - 2))
ENDIF

END my_sequence_ops

Track: THEORY
BEGIN

ASSUMING

IMPORTING Position, defs, Train, my_sequence_ops

track:
TYPE =
[# track_name: track_no,
points: point_values,
blocks: blocks,
trains: setof[train],
obstruction_position: setof[blocks] #]

track_ax1: AXIOM FORALL (tk: track): length(blocks(tk)) = length(points(tk)) - 1

track_ax2: AXIOM
FORALL (tk: track), (i: nat):
member(i, {n: nat | n <= length(points(tk)) - 2})
IMPLIES
(PROJ_1(finseq_appl(blocks(tk))(i)) = finseq_appl(points(tk))(i)
AND PROJ_2(finseq_appl(blocks(tk))(i)) = finseq_appl(points(tk))(i + 1))

track_ax3: AXIOM FORALL (tk: track), (b: blocks): member(b, obstruction_position(tk)) IMPLIES sub_seq(b, blocks(tk))

track_ax4: AXIOM FORALL (tk: track), (t: train): member(t, trains(tk)) IMPLIES sub_seq(position(t), blocks(tk))

ENDASSUMING

i: VAR nat

add_a_train((tk: track), (t?: train)): track = IF member(t?, trains(tk)) THEN tk ELSE tk WITH [trains := add(t?, trains(tk))] ENDIF

% index works because the block in blocks are unique, so there is a unique index.

index((tk: track), (b: block | EXISTS (i: below(length(blocks(tk)))): b = finseq_appl(blocks(tk))(i))):
RECURSIVE nat = (IF b = finseq_appl(blocks(tk))(0) THEN 0 ELSE index(tk WITH [blocks := tail(blocks(tk))], b) + 1 ENDIF)
MEASURE
(LAMBDA (tk: track), (b: block | EXISTS (i: below(length(blocks(tk)))): b = finseq_appl(blocks(tk))(i)): length(blocks(tk)))

next_position((tk: track), (t?: train)): blocks =
IF NOT member(t?, trains(tk)) THEN position(t?)
ELSE IF direction(t?) = high_to_low AND last(position(t?)) = last(blocks(tk)) THEN position(t?)
ELSE IF direction(t?) = high_to_low THEN IF length(position(t?)) = max_length(t?) + 1 THEN tail(position(t?))
ELSE IF length(position(t?)) = max_length(t?)
THEN o(position(t?), ^(blocks(tk), (index(tk, last(position(t?))) + 1, index(tk, last(position(t?))) + 1)))
ELSE position(t?)
ENDIF
ENDIF
ELSE IF direction(t?) = low_to_high THEN IF length(position(t?)) = max_length(t?) + 1 THEN front(position(t?))
ELSE IF length(position(t?)) = max_length(t?)
ELSE position(t?)
ENDIF
ENDIF
ELSE position(t?)
ENDIF
ENDIF
ENDIF
ENDIF
ENDIF

move1((tk: track), (t?: train | member(t?,trains(tk)) AND speed(t?) /= 0)): [track,train] =
LET updated_t?: train = t? WITH [position := next_position(tk,t?)] in
(tk WITH
[trains := union({t: train | member(t,trains(tk)) AND t /= t?},
{t: train | t = updated_t?}) ],
updated_t?)

collision_situation((tk: track), (p1?,p2?: blocks)): bool =
EXISTS (b: block | in_seq(b,blocks(tk))): in_seq(b,p1?) AND in_seq(b,p2?)

obstruction_in_way?((tk: track), (t?: train | member(t?,trains(tk)))): bool =
EXISTS (obs_pos: blocks | member(obs_pos,obstruction_position(tk))):
collision_situation(tk, obs_pos, next_position(tk, t?))

train_in_way?((tk: track), (t?: train | member(t?,trains(tk)))): bool =
EXISTS (t2: train | member(t2,trains(tk)) AND t2 /= t?):
collision_situation(tk, next_position(tk, t?), position(t2))

trains_in_way((tk: track), (t?: train | member(t?,trains(tk)))): setof[train] =
{t: train | member(t,trains(tk)) AND t /= t? AND collision_situation(tk, next_position(tk, t?), position(t)) }

% move: the train moves a step forward, if there is an obstruction or train in the way
% there is a collision.

move((tk: track), (t?: train | member(t?,trains(tk)) AND speed(t?) /= 0)): [track,train] =
IF NOT train_in_way?(tk,t?) AND NOT obstruction_in_way?(tk,t?) THEN move1(tk,t?)
ELSE let updated_t?: train = PROJ_2(move1(tk,t?)) WITH [collision_status := collision] in
IF train_in_way?(tk,t?) THEN
(PROJ_1(move1(tk,t?)) WITH
[trains := union(union(
{t: train | member(t,trains(tk)) AND t /= t? AND NOT member(t,trains_in_way(tk,t?))},
{t: train | t = updated_t?}),
{t: train | FORALL (tt: train):
member(tt,trains_in_way(tk,t?)) AND t = tt WITH [collision_status := collision]})],
updated_t?)
ELSE  % obstruction in the way.
(PROJ_1(move1(tk,t?)) WITH
[ trains := union(
{t: train | member(t,trains(tk)) AND t /= t?},
{t: train | t = updated_t?})],
updated_t?)
ENDIF
ENDIF

END Track

General_Train_System: THEORY
BEGIN

ASSUMING

IMPORTING Train, Track, finite_sets@finite_sets[train]

system: TYPE = [# trains: setof[train], tracks: setof[track] #]

system_ax1: AXIOM  % a train is either not on any track or is associated with a unique track.
FORALL (s: system), (t: train | member(t, trains(s))):
EXISTS (tk: track | member(tk, tracks(s))): member(t, trains(tk)) IMPLIES
NOT EXISTS (tk2: track | member(tk2, tracks(s)) AND tk2 /= tk ): member(t, trains(tk2))

system_ax2: AXIOM  % if a train is associated with a track then its position is on that track.
FORALL (s: system), (t: train | member(t, trains(s))):
EXISTS (tk: track | member(tk, tracks(s))): member(t, trains(tk)) IMPLIES
sub_seq(position(t),blocks(tk))

ENDASSUMING

s: VAR system

s_tracks(s): TYPE = {tk: track | member(tk,tracks(s))}
s_trains(s): TYPE = {t: train | member(t,trains(s))}

find_train((trains: setof[train] | nonempty?(trains)), (tn: train_name | EXISTS (t: train): name(t) = tn)):
RECURSIVE train =
LET t = choose(trains) in
IF name(t) = tn THEN t
ELSE find_train(remove(t,trains),tn)
ENDIF
MEASURE (LAMBDA (trains: setof[train] | nonempty?(trains)), (tn: train_name | EXISTS (t: train): name(t) = tn):
Card(trains) )

add_train_to_system( s, (t?: train | NOT member(t?,trains(s)))): system =

remove_train_from_system( s, (t?: s_trains(s))): system =
IF EXISTS (tk1: s_tracks(s)): member(t?, trains(tk1)) THEN s
ELSE s WITH [trains := remove(t?,trains(s))]
ENDIF

add_train_to_track( s, (tk?: s_tracks(s)), (t?: s_trains(s))): system =
IF EXISTS (tk1: s_tracks(s)): member(t?, trains(tk1)) THEN s
ELSE s WITH [tracks := union(
{tk: s_tracks(s) | tk /= tk?},
{tk: s_tracks(s) | tk = tk? WITH [trains := add(t?,trains(tk?))]})]
ENDIF

remove_train_from_track( s, (tk?: s_tracks(s)), (t?: s_trains(s))): system =
IF NOT member(t?,trains(tk?)) THEN s
ELSE s WITH [tracks := union(
{tk: s_tracks(s) | tk /= tk?},
{tk: s_tracks(s) | tk = tk? WITH [trains := remove(t?,trains(tk?))]})]
ENDIF

change_track( s, (tk1?,tk2?: s_tracks(s)), (t?: s_trains(s))): system =
IF NOT member(t?, trains(tk1?)) THEN s
ELSE s WITH [tracks := union(union(
{tk: s_tracks(s) | tk /= tk1? AND tk /= tk2?},
{tk: s_tracks(s) | tk = tk1? WITH [trains := remove(t?,trains(tk1?))]}),
{tk: s_tracks(s) | tk = tk2? WITH [trains := add(t?,trains(tk1?))]})]
ENDIF

END General_Train_System

Thedford_scenario: THEORY

BEGIN

ASSUMING
IMPORTING General_Train_System
ENDASSUMING

t1,t2: train_name
tk1: track_no

mp: point_values = (# length:= 5,
seq:= (LAMBDA (n: below(5)):
COND n=0 -> 256 + 1/10,
n=1 -> 254 + 2/10,
n=2 -> 252 + 4/10,
n=3 -> 250 + 8/10,
n=4 -> 249 + 1/10
ENDCOND) #)

tk1_blocks: blocks = (# length:= 4,
seq:= (LAMBDA (n: below(4)):
COND n=0 -> (mp(0),mp(1)),
n=1 -> (mp(1),mp(2)),
n=2 -> (mp(2),mp(3)),
n=3 -> (mp(3),mp(4))
ENDCOND) #)

mode1: mode_values

train1: train = (#
name:= t1,
position:= (# length:= 1,
seq:= (LAMBDA (n: below(1)):
COND n=0 -> (mp(0),mp(1))
ENDCOND) #),
max_length:= 1,
collision_status:= no_collision,
speed:= 100,
direction:= high_to_low,
mode:= mode1,
condition_status:= condition_ok #)

train2: train = (#
name:= t2,
position:= (# length:= 1,
seq:= (LAMBDA (n: below(1)):
COND n=0 -> (mp(2),mp(3))
ENDCOND) #),
max_length:= 1,
collision_status:= no_collision,
speed:= 0,
direction:= high_to_low,
mode:= mode1,
condition_status:= condition_ok #)

track1: track = (#
track_name:= tk1,
points:= mp,
blocks:= tk1_blocks,
trains:= {t:train | t=train1 OR t=train2},
obstruction_position:= emptyset #)

speed_lemma: LEMMA
FORALL (tk: track):
FORALL (t: train | member(t, trains(tk))):
speed(t) /= 0 AND NOT train_in_way?(tk,t) AND NOT obstruction_in_way?(tk,t)
IMPLIES speed(PROJ_2(move(tk, t))) /= 0

member_lemma: LEMMA FORALL (tk: track):
FORALL (t: train | member(t, trains(tk))):
speed(t) /= 0 IMPLIES member(PROJ_2(move(tk,t)),trains(PROJ_1(move(tk,t))))

move1_lemma: LEMMA PROJ_2(move(track1,train1)) = train1 WITH [position:= (# length:= 2,
seq:= (LAMBDA (n: below(2)):
COND n=0 -> (mp(0),mp(1)),
n=1 -> (mp(1),mp(2))
ENDCOND) #)]

crash_scenario: THEOREM LET tk1m1: track = PROJ_1(move(track1,train1)),
t1m1: train = PROJ_2(move(track1,train1)),
tk1m2: track = PROJ_1(move(tk1m1,t1m1)),
t1m2: train = PROJ_2(move(tk1m1,t1m1)),
tk1m3: track = PROJ_1(move(tk1m2,t1m2)),
t1m3: train = PROJ_2(move(tk1m2,t1m2))
in
collision_status(t1m3) = collision AND
collision_status(find_train(trains(tk1m3),t2)) = collision

loopy: LEMMA

((LAMBDA (n:
below[1
+
length(((# length := 4,
seq :=
(LAMBDA (n: below(4)):
COND
n = 0 -> (256 + 1 / 10, 254 + 2 / 10),
n = 1 -> (254 + 2 / 10, 252 + 4 / 10),
n = 2 -> (252 + 4 / 10, 250 + 8 / 10),
ELSE -> (250 + 8 / 10, 249 + 1 / 10)
ENDCOND)
#)
^
((1
+
index((# track_name := tk1,
points :=
(# length := 5,
seq :=
(LAMBDA (n: below(5)):
COND
n = 0 ->
256 + 1 / 10,
n = 1 ->
254 + 2 / 10,
n = 2 ->
252 + 4 / 10,
n = 3 ->
250 + 8 / 10,
ELSE ->
249 + 1 / 10
ENDCOND)
#),
blocks :=
(# length := 4,
seq :=
(LAMBDA (n: below(4)):
COND
n = 0 ->
(256 + 1 / 10,
254 + 2 / 10),
n = 1 ->
(254 + 2 / 10,
252 + 4 / 10),
n = 2 ->
(252 + 4 / 10,
250 + 8 / 10),
ELSE ->
(250 + 8 / 10,
249 + 1 / 10)
ENDCOND)
#),
trains := {t: train | t = train1 OR t = train2},
obstruction_position := emptyset #),
(256 + 1 / 10, 254 + 2 / 10))),
(1
+
index((# track_name := tk1,
points :=
(# length := 5,
seq :=
(LAMBDA (n: below(5)):
COND
n = 0 ->
256 + 1 / 10,
n = 1 ->
254 + 2 / 10,
n = 2 ->
252 + 4 / 10,
n = 3 ->
250 + 8 / 10,
ELSE ->
249 + 1 / 10
ENDCOND)
#),
blocks :=
(# length := 4,
seq :=
(LAMBDA (n: below(4)):
COND
n = 0 ->
(256 + 1 / 10,
254 + 2 / 10),
n = 1 ->
(254 + 2 / 10,
252 + 4 / 10),
n = 2 ->
(252 + 4 / 10,
250 + 8 / 10),
ELSE ->
(250 + 8 / 10,
249 + 1 / 10)
ENDCOND)
#),
trains := {t: train | t = train1 OR t = train2},
obstruction_position := emptyset #),
(256 + 1 / 10, 254 + 2 / 10))))))]):
IF n < 1 THEN (256 + 1 / 10, 254 + 2 / 10)
ELSE COND
((n - 1) = 0) -> (254 + 2 / 10, 252 + 4 / 10),
(n = 2) -> (252 + 4 / 10, 250 + 8 / 10),
ELSE -> (250 + 8 / 10, 249 + 1 / 10)
ENDCOND
ENDIF)
=
(LAMBDA (n: below(2)): COND n = 0 -> (256 + 1 / 10, 254 + 2 / 10), ELSE -> (254 + 2 / 10, 252 + 4 / 10) ENDCOND))

END Thedford_scenario

```