:: by JingChao Chen

::

:: Received June 14, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

set A = NAT ;

set D = SCM-Data-Loc ;

::$CT

theorem Th2: :: SCMPDS_8:3

for t being State of SCMPDS

for i being Instruction of SCMPDS st InsCode i in {0,4,5,6,14} holds

Initialize t = Initialize (Exec (i,t))

for i being Instruction of SCMPDS st InsCode i in {0,4,5,6,14} holds

Initialize t = Initialize (Exec (i,t))

proof end;

::$CT

theorem Th3: :: SCMPDS_8:5

for a being Int_position ex f being Function of (product (the_Values_of SCMPDS)),NAT st

for s being State of SCMPDS holds

( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )

for s being State of SCMPDS holds

( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )

proof end;

:: while (a,i)<0 do I

definition

let a be Int_position;

let i be Integer;

let I be Program of SCMPDS;

(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is Program of SCMPDS ;

end;
let i be Integer;

let I be Program of SCMPDS;

func while<0 (a,i,I) -> Program of SCMPDS equals :: SCMPDS_8:def 2

(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

coherence (((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is Program of SCMPDS ;

:: deftheorem defines while<0 SCMPDS_8:def 2 :

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds while<0 (a,i,I) = (((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds while<0 (a,i,I) = (((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

registration

let I be shiftable Program of SCMPDS;

let a be Int_position;

let i be Integer;

correctness

coherence

while<0 (a,i,I) is shiftable ;

end;
let a be Int_position;

let i be Integer;

correctness

coherence

while<0 (a,i,I) is shiftable ;

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let i be Integer;

correctness

coherence

while<0 (a,i,I) is halt-free ;

;

end;
let a be Int_position;

let i be Integer;

correctness

coherence

while<0 (a,i,I) is halt-free ;

;

theorem Th4: :: SCMPDS_8:6

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds card (while<0 (a,i,I)) = (card I) + 2

for i being Integer

for I being Program of SCMPDS holds card (while<0 (a,i,I)) = (card I) + 2

proof end;

Lm1: for a being Int_position

for i being Integer

for I being Program of SCMPDS holds card (stop (while<0 (a,i,I))) = (card I) + 3

proof end;

theorem Th5: :: SCMPDS_8:7

for a being Int_position

for i being Integer

for m being Nat

for I being Program of SCMPDS holds

( m < (card I) + 2 iff m in dom (while<0 (a,i,I)) )

for i being Integer

for m being Nat

for I being Program of SCMPDS holds

( m < (card I) + 2 iff m in dom (while<0 (a,i,I)) )

proof end;

theorem Th6: :: SCMPDS_8:8

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds

( (while<0 (a,i,I)) . 0 = (a,i) >=0_goto ((card I) + 2) & (while<0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )

for i being Integer

for I being Program of SCMPDS holds

( (while<0 (a,i,I)) . 0 = (a,i) >=0_goto ((card I) + 2) & (while<0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )

proof end;

theorem Th7: :: SCMPDS_8:9

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

proof end;

theorem Th8: :: SCMPDS_8:10

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, c being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

IExec ((while<0 (a,i,I)),P,s) = s +* (Start-At (((card I) + 2),SCMPDS))

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, c being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

IExec ((while<0 (a,i,I)),P,s) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem :: SCMPDS_8:11

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

IC (IExec ((while<0 (a,i,I)),P,s)) = (card I) + 2

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

IC (IExec ((while<0 (a,i,I)),P,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_8:12

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

(IExec ((while<0 (a,i,I)),P,s)) . b = s . b

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds

(IExec ((while<0 (a,i,I)),P,s)) . b = s . b

proof end;

Lm2: for I being Program of SCMPDS

for a being Int_position

for i being Integer holds Shift (I,1) c= while<0 (a,i,I)

proof end;

scheme :: SCMPDS_8:sch 1

WhileLHalt{ F_{1}( State of SCMPDS) -> Nat, F_{2}() -> 0 -started State of SCMPDS, F_{3}() -> Instruction-Sequence of SCMPDS, F_{4}() -> halt-free shiftable Program of SCMPDS, F_{5}() -> Int_position, F_{6}() -> Integer, P_{1}[ State of SCMPDS] } :

WhileLHalt{ F

( while<0 (F_{5}(),F_{6}(),F_{4}()) is_closed_on F_{2}(),F_{3}() & while<0 (F_{5}(),F_{6}(),F_{4}()) is_halting_on F_{2}(),F_{3}() )

provided
A1:
for t being 0 -started State of SCMPDS st P_{1}[t] & F_{1}(t) = 0 holds

t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) >= 0
and

A2: P_{1}[F_{2}()]
and

A3: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P_{1}[t] & t . F_{5}() = F_{2}() . F_{5}() & t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) < 0 holds

( (IExec (F_{4}(),Q,t)) . F_{5}() = t . F_{5}() & F_{4}() is_closed_on t,Q & F_{4}() is_halting_on t,Q & F_{1}((Initialize (IExec (F_{4}(),Q,t)))) < F_{1}(t) & P_{1}[ Initialize (IExec (F_{4}(),Q,t))] )

t . (DataLoc ((F

A2: P

A3: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P

( (IExec (F

proof end;

scheme :: SCMPDS_8:sch 2

WhileLExec{ F_{1}( State of SCMPDS) -> Nat, F_{2}() -> 0 -started State of SCMPDS, F_{3}() -> Instruction-Sequence of SCMPDS, F_{4}() -> halt-free shiftable Program of SCMPDS, F_{5}() -> Int_position, F_{6}() -> Integer, P_{1}[ State of SCMPDS] } :

WhileLExec{ F

IExec ((while<0 (F_{5}(),F_{6}(),F_{4}())),F_{3}(),F_{2}()) = IExec ((while<0 (F_{5}(),F_{6}(),F_{4}())),F_{3}(),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))

provided
A1:
F_{2}() . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) < 0
and

A2: for t being 0 -started State of SCMPDS st P_{1}[t] & F_{1}(t) = 0 holds

t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) >= 0
and

A3: P_{1}[F_{2}()]
and

A4: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P_{1}[t] & t . F_{5}() = F_{2}() . F_{5}() & t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) < 0 holds

( (IExec (F_{4}(),Q,t)) . F_{5}() = t . F_{5}() & F_{4}() is_closed_on t,Q & F_{4}() is_halting_on t,Q & F_{1}((Initialize (IExec (F_{4}(),Q,t)))) < F_{1}(t) & P_{1}[ Initialize (IExec (F_{4}(),Q,t))] )

A2: for t being 0 -started State of SCMPDS st P

t . (DataLoc ((F

A3: P

A4: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P

( (IExec (F

proof end;

theorem :: SCMPDS_8:13

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & f . (Initialize (IExec (I,Q,t))) < f . t & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & f . (Initialize (IExec (I,Q,t))) < f . t & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

proof end;

theorem :: SCMPDS_8:14

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

proof end;

theorem Th13: :: SCMPDS_8:15

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set st ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set st ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

proof end;

theorem :: SCMPDS_8:16

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set st s . (DataLoc ((s . a),i)) < 0 & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds

( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

proof end;

:: while (a,i)>0 do I

definition

let a be Int_position;

let i be Integer;

let I be Program of SCMPDS;

(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is Program of SCMPDS ;

end;
let i be Integer;

let I be Program of SCMPDS;

func while>0 (a,i,I) -> Program of SCMPDS equals :: SCMPDS_8:def 3

(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

coherence (((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is Program of SCMPDS ;

:: deftheorem defines while>0 SCMPDS_8:def 3 :

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds while>0 (a,i,I) = (((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds while>0 (a,i,I) = (((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

registration

let I be shiftable Program of SCMPDS;

let a be Int_position;

let i be Integer;

correctness

coherence

while>0 (a,i,I) is shiftable ;

end;
let a be Int_position;

let i be Integer;

correctness

coherence

while>0 (a,i,I) is shiftable ;

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let i be Integer;

correctness

coherence

while>0 (a,i,I) is halt-free ;

;

end;
let a be Int_position;

let i be Integer;

correctness

coherence

while>0 (a,i,I) is halt-free ;

;

theorem Th15: :: SCMPDS_8:17

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds card (while>0 (a,i,I)) = (card I) + 2

for i being Integer

for I being Program of SCMPDS holds card (while>0 (a,i,I)) = (card I) + 2

proof end;

Lm3: for a being Int_position

for i being Integer

for I being Program of SCMPDS holds card (stop (while>0 (a,i,I))) = (card I) + 3

proof end;

theorem Th16: :: SCMPDS_8:18

for a being Int_position

for i being Integer

for m being Nat

for I being Program of SCMPDS holds

( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )

for i being Integer

for m being Nat

for I being Program of SCMPDS holds

( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )

proof end;

theorem Th17: :: SCMPDS_8:19

for a being Int_position

for i being Integer

for I being Program of SCMPDS holds

( (while>0 (a,i,I)) . 0 = (a,i) <=0_goto ((card I) + 2) & (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )

for i being Integer

for I being Program of SCMPDS holds

( (while>0 (a,i,I)) . 0 = (a,i) <=0_goto ((card I) + 2) & (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )

proof end;

theorem Th18: :: SCMPDS_8:20

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )

proof end;

theorem Th19: :: SCMPDS_8:21

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, c being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

IExec ((while>0 (a,i,I)),P,s) = s +* (Start-At (((card I) + 2),SCMPDS))

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, c being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

IExec ((while>0 (a,i,I)),P,s) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem :: SCMPDS_8:22

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

IC (IExec ((while>0 (a,i,I)),P,s)) = (card I) + 2

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

IC (IExec ((while>0 (a,i,I)),P,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_8:23

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

(IExec ((while>0 (a,i,I)),P,s)) . b = s . b

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds

(IExec ((while>0 (a,i,I)),P,s)) . b = s . b

proof end;

Lm4: for I being Program of SCMPDS

for a being Int_position

for i being Integer holds Shift (I,1) c= while>0 (a,i,I)

proof end;

scheme :: SCMPDS_8:sch 3

WhileGHalt{ F_{1}( State of SCMPDS) -> Nat, F_{2}() -> 0 -started State of SCMPDS, F_{3}() -> Instruction-Sequence of SCMPDS, F_{4}() -> halt-free shiftable Program of SCMPDS, F_{5}() -> Int_position, F_{6}() -> Integer, P_{1}[ State of SCMPDS] } :

WhileGHalt{ F

( while>0 (F_{5}(),F_{6}(),F_{4}()) is_closed_on F_{2}(),F_{3}() & while>0 (F_{5}(),F_{6}(),F_{4}()) is_halting_on F_{2}(),F_{3}() )

provided
A1:
for t being 0 -started State of SCMPDS st P_{1}[t] & F_{1}(t) = 0 holds

t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) <= 0
and

A2: P_{1}[F_{2}()]
and

A3: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P_{1}[t] & t . F_{5}() = F_{2}() . F_{5}() & t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) > 0 holds

( (IExec (F_{4}(),Q,t)) . F_{5}() = t . F_{5}() & F_{4}() is_closed_on t,Q & F_{4}() is_halting_on t,Q & F_{1}((Initialize (IExec (F_{4}(),Q,t)))) < F_{1}(t) & P_{1}[ Initialize (IExec (F_{4}(),Q,t))] )

t . (DataLoc ((F

A2: P

A3: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P

( (IExec (F

proof end;

scheme :: SCMPDS_8:sch 4

WhileGExec{ F_{1}( State of SCMPDS) -> Nat, F_{2}() -> 0 -started State of SCMPDS, F_{3}() -> Instruction-Sequence of SCMPDS, F_{4}() -> halt-free shiftable Program of SCMPDS, F_{5}() -> Int_position, F_{6}() -> Integer, P_{1}[ State of SCMPDS] } :

WhileGExec{ F

IExec ((while>0 (F_{5}(),F_{6}(),F_{4}())),F_{3}(),F_{2}()) = IExec ((while>0 (F_{5}(),F_{6}(),F_{4}())),F_{3}(),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))

provided
A1:
F_{2}() . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) > 0
and

A2: for t being 0 -started State of SCMPDS st P_{1}[t] & F_{1}(t) = 0 holds

t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) <= 0
and

A3: P_{1}[F_{2}()]
and

A4: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P_{1}[t] & t . F_{5}() = F_{2}() . F_{5}() & t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) > 0 holds

( (IExec (F_{4}(),Q,t)) . F_{5}() = t . F_{5}() & F_{4}() is_closed_on t,Q & F_{4}() is_halting_on t,Q & F_{1}((Initialize (IExec (F_{4}(),Q,t)))) < F_{1}(t) & P_{1}[ Initialize (IExec (F_{4}(),Q,t))] )

A2: for t being 0 -started State of SCMPDS st P

t . (DataLoc ((F

A3: P

A4: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P

( (IExec (F

proof end;

theorem Th22: :: SCMPDS_8:24

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )

proof end;

theorem Th23: :: SCMPDS_8:25

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

proof end;

theorem :: SCMPDS_8:26

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

proof end;

theorem Th25: :: SCMPDS_8:27

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set st ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set st ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

proof end;

theorem :: SCMPDS_8:28

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set st ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i being Integer

for X being set st ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

proof end;

theorem :: SCMPDS_8:29

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X being set st ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X being set st ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )

proof end;