:: by JingChao Chen and Piotr Rudnicki

::

:: Received December 27, 1999

:: Copyright (c) 1999-2018 Association of Mizar Users

set A = NAT ;

set D = SCM-Data-Loc ;

theorem Th2: :: SCMPDS_7:2

for i, j, k being Instruction of SCMPDS

for I being Program of holds ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)

for I being Program of holds ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)

proof end;

::$CT 2

theorem :: SCMPDS_7:7

for s being State of SCMPDS

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

DataPart (Exec (i,s)) = DataPart s

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

DataPart (Exec (i,s)) = DataPart s

proof end;

theorem Th6: :: SCMPDS_7:8

for P1, P2 being Instruction-Sequence of SCMPDS

for s1, s2 being State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

for s1, s2 being State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

proof end;

theorem Th7: :: SCMPDS_7:9

for P1, P2 being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

for s being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

proof end;

theorem Th8: :: SCMPDS_7:10

for P1, P2 being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

for s being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

proof end;

theorem Th9: :: SCMPDS_7:11

for P1, P2 being Instruction-Sequence of SCMPDS

for s1, s2 being State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

( LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

for s1, s2 being State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

( LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

proof end;

theorem :: SCMPDS_7:12

for P1, P2 being Instruction-Sequence of SCMPDS

for s1, s2 being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

for s1, s2 being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

proof end;

theorem Th11: :: SCMPDS_7:13

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a being Int_position st I is_halting_on s,P holds

(IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_6:def 3, EXTPRO_1:23;

for s being State of SCMPDS

for I being Program of

for a being Int_position st I is_halting_on s,P holds

(IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_6:def 3, EXTPRO_1:23;

theorem :: SCMPDS_7:14

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being parahalting Program of

for a being Int_position holds (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_6:21, Th11;

for s being State of SCMPDS

for I being parahalting Program of

for a being Int_position holds (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_6:21, Th11;

theorem Th13: :: SCMPDS_7:15

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of

for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds

IC (Comput (P,s,i)) in dom I

for s being 0 -started State of SCMPDS

for I being Program of

for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds

IC (Comput (P,s,i)) in dom I

proof end;

theorem Th14: :: SCMPDS_7:16

for s2 being State of SCMPDS

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat st i < LifeSpan (P1,s1) holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat st i < LifeSpan (P1,s1) holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;

theorem Th15: :: SCMPDS_7:17

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds

LifeSpan (P,s) > 0

for s being 0 -started State of SCMPDS

for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds

LifeSpan (P,s) > 0

proof end;

theorem Th16: :: SCMPDS_7:18

for s2 being State of SCMPDS

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for I being halt-free shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for I being halt-free shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )

proof end;

theorem Th17: :: SCMPDS_7:19

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)

proof end;

theorem Th18: :: SCMPDS_7:20

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

proof end;

theorem Th19: :: SCMPDS_7:21

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for k being Nat st k <= LifeSpan ((P +* (stop I)),(Initialize s)) & I c= J & I is_closed_on s,P & I is_halting_on s,P holds

IC (Comput ((P +* J),(Initialize s),k)) in dom (stop I)

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for k being Nat st k <= LifeSpan ((P +* (stop I)),(Initialize s)) & I c= J & I is_closed_on s,P & I is_halting_on s,P holds

IC (Comput ((P +* J),(Initialize s),k)) in dom (stop I)

proof end;

theorem Th20: :: SCMPDS_7:22

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds

IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

for P being Instruction-Sequence of SCMPDS

for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds

IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

proof end;

theorem Th21: :: SCMPDS_7:23

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I, J being Program of st I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds

( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) )

for P being Instruction-Sequence of SCMPDS

for I, J being Program of st I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds

( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) )

proof end;

theorem Th22: :: SCMPDS_7:24

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I being Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds

( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )

for P being Instruction-Sequence of SCMPDS

for I being Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds

( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )

proof end;

theorem Th23: :: SCMPDS_7:25

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I being halt-free Program of

for J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P holds

IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

for P being Instruction-Sequence of SCMPDS

for I being halt-free Program of

for J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P holds

IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

proof end;

theorem :: SCMPDS_7:26

for P being Instruction-Sequence of SCMPDS

for I being Program of

for s being State of SCMPDS

for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS

for I being Program of

for s being State of SCMPDS

for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS

proof end;

theorem Th25: :: SCMPDS_7:27

for P being Instruction-Sequence of SCMPDS

for I, J being Program of

for s being 0 -started State of SCMPDS

for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),s) holds

CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k))) <> halt SCMPDS

for I, J being Program of

for s being 0 -started State of SCMPDS

for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),s) holds

CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k))) <> halt SCMPDS

proof end;

Lm1: for P, P1, P2 being Instruction-Sequence of SCMPDS

for I being halt-free Program of

for J being shiftable Program of

for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds

( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )

proof end;

theorem :: SCMPDS_7:28

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds

LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) by Lm1;

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds

LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) by Lm1;

theorem Th27: :: SCMPDS_7:29

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds

IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds

IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))

proof end;

theorem Th28: :: SCMPDS_7:30

for a being Int_position

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds

(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds

(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a

proof end;

theorem Th29: :: SCMPDS_7:31

for a being Int_position

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

(IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of

for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

(IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

proof end;

:: while (a,i)<=0 do { I, (a,i)+=n }

definition

let a be Int_position;

let i be Integer;

let n be Nat;

let I be Program of ;

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

end;
let i be Integer;

let n be Nat;

let I be Program of ;

func for-up (a,i,n,I) -> Program of equals :: SCMPDS_7:def 1

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

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

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

:: deftheorem defines for-up SCMPDS_7:def 1 :

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds for-up (a,i,n,I) = ((((a,i) >=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)));

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds for-up (a,i,n,I) = ((((a,i) >=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)));

theorem Th30: :: SCMPDS_7:32

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

for i being Integer

for n being Nat

for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

proof end;

Lm2: for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

proof end;

theorem Th31: :: SCMPDS_7:33

for a being Int_position

for i being Integer

for n, m being Nat

for I being Program of holds

( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )

for i being Integer

for n, m being Nat

for I being Program of holds

( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )

proof end;

theorem Th32: :: SCMPDS_7:34

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds

( (for-up (a,i,n,I)) . 0 = (a,i) >=0_goto ((card I) + 3) & (for-up (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,n) & (for-up (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )

for i being Integer

for n being Nat

for I being Program of holds

( (for-up (a,i,n,I)) . 0 = (a,i) >=0_goto ((card I) + 3) & (for-up (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,n) & (for-up (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )

proof end;

theorem Th33: :: SCMPDS_7:35

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

proof end;

theorem Th34: :: SCMPDS_7:36

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a, c being Int_position

for i being Integer

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

IExec ((for-up (a,i,n,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))

for s being State of SCMPDS

for I being Program of

for a, c being Int_position

for i being Integer

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

IExec ((for-up (a,i,n,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))

proof end;

theorem :: SCMPDS_7:37

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

IC (IExec ((for-up (a,i,n,I)),P,(Initialize s))) = (card I) + 3

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

IC (IExec ((for-up (a,i,n,I)),P,(Initialize s))) = (card I) + 3

proof end;

theorem :: SCMPDS_7:38

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a, b being Int_position

for i being Integer

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

(IExec ((for-up (a,i,n,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of

for a, b being Int_position

for i being Integer

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

(IExec ((for-up (a,i,n,I)),P,(Initialize s))) . b = s . b

proof end;

Lm3: for I being Program of

for a being Int_position

for i being Integer

for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

proof end;

theorem Th37: :: SCMPDS_7:39

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds

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

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

for s being State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds

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

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

proof end;

theorem :: SCMPDS_7:40

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds

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

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds

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

(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds

IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))

proof end;

registration

let I be shiftable Program of ;

let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-up (a,i,n,I) is shiftable ;

end;
let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-up (a,i,n,I) is shiftable ;

proof end;

registration

let I be halt-free Program of ;

let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-up (a,i,n,I) is halt-free ;

end;
let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-up (a,i,n,I) is halt-free ;

proof end;

:: while (a,i)>=0 do { I, (a,i)-=n }

definition

let a be Int_position;

let i be Integer;

let n be Nat;

let I be Program of ;

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

end;
let i be Integer;

let n be Nat;

let I be Program of ;

func for-down (a,i,n,I) -> Program of equals :: SCMPDS_7:def 2

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

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

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

:: deftheorem defines for-down SCMPDS_7:def 2 :

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds for-down (a,i,n,I) = ((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2)));

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds for-down (a,i,n,I) = ((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2)));

theorem Th39: :: SCMPDS_7:41

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3

for i being Integer

for n being Nat

for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3

proof end;

Lm4: for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds card (stop (for-down (a,i,n,I))) = (card I) + 4

proof end;

theorem Th40: :: SCMPDS_7:42

for a being Int_position

for i being Integer

for n, m being Nat

for I being Program of holds

( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )

for i being Integer

for n, m being Nat

for I being Program of holds

( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )

proof end;

theorem Th41: :: SCMPDS_7:43

for a being Int_position

for i being Integer

for n being Nat

for I being Program of holds

( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )

for i being Integer

for n being Nat

for I being Program of holds

( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )

proof end;

theorem Th42: :: SCMPDS_7:44

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )

proof end;

theorem Th43: :: SCMPDS_7:45

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a, c being Int_position

for i being Integer

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

IExec ((for-down (a,i,n,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))

for s being State of SCMPDS

for I being Program of

for a, c being Int_position

for i being Integer

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

IExec ((for-down (a,i,n,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))

proof end;

theorem :: SCMPDS_7:46

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

IC (IExec ((for-down (a,i,n,I)),P,(Initialize s))) = (card I) + 3

for s being State of SCMPDS

for I being Program of

for a being Int_position

for i being Integer

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

IC (IExec ((for-down (a,i,n,I)),P,(Initialize s))) = (card I) + 3

proof end;

theorem Th45: :: SCMPDS_7:47

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of

for a, b being Int_position

for i being Integer

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

(IExec ((for-down (a,i,n,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of

for a, b being Int_position

for i being Integer

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

(IExec ((for-down (a,i,n,I)),P,(Initialize s))) . b = s . b

proof end;

Lm5: for I being Program of

for a being Int_position

for i being Integer

for n being Nat holds Shift (I,1) c= for-down (a,i,n,I)

proof end;

theorem Th46: :: SCMPDS_7:48

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) > 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> 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 = s . x ) & t . a = s . a 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 y being Int_position st y in X holds

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

( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )

for s being State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) > 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> 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 = s . x ) & t . a = s . a 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 y being Int_position st y in X holds

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

( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )

proof end;

theorem Th47: :: SCMPDS_7:49

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) > 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> 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 = s . x ) & t . a = s . a 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 y being Int_position st y in X holds

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

IExec ((for-down (a,i,n,I)),P,s) = IExec ((for-down (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of

for a being Int_position

for i being Integer

for n being Nat

for X being set st s . (DataLoc ((s . a),i)) > 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> 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 = s . x ) & t . a = s . a 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 y being Int_position st y in X holds

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

IExec ((for-down (a,i,n,I)),P,s) = IExec ((for-down (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))))

proof end;

registration

let I be shiftable Program of ;

let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-down (a,i,n,I) is shiftable ;

end;
let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-down (a,i,n,I) is shiftable ;

proof end;

registration

let I be halt-free Program of ;

let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-down (a,i,n,I) is halt-free ;

end;
let a be Int_position;

let i be Integer;

let n be Nat;

correctness

coherence

for-down (a,i,n,I) is halt-free ;

proof end;

:: n=Sum 1+1+...+1

definition

let n be Nat;

(((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))) is Program of ;

end;
func sum n -> Program of equals :: SCMPDS_7:def 3

(((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))));

coherence (((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))));

(((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))) is Program of ;

:: deftheorem defines sum SCMPDS_7:def 3 :

for n being Nat holds sum n = (((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))));

for n being Nat holds sum n = (((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))));

theorem Th48: :: SCMPDS_7:50

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS st s . GBP = 0 holds

( for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on s,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P )

for s being 0 -started State of SCMPDS st s . GBP = 0 holds

( for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on s,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P )

proof end;

theorem Th49: :: SCMPDS_7:51

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for n being Nat st s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 holds

(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n

for s being 0 -started State of SCMPDS

for n being Nat st s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 holds

(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n

proof end;

theorem :: SCMPDS_7:52

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n

for s being 0 -started State of SCMPDS

for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n

proof end;

:: sum=Sum x1+x2+...+x2

definition

let sp, control, result, pp, pData be Nat;

((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1))))) is Program of ;

end;
func sum (sp,control,result,pp,pData) -> Program of equals :: SCMPDS_7:def 4

((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));

coherence ((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));

((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1))))) is Program of ;

:: deftheorem defines sum SCMPDS_7:def 4 :

for sp, control, result, pp, pData being Nat holds sum (sp,control,result,pp,pData) = ((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));

for sp, control, result, pp, pData being Nat holds sum (sp,control,result,pp,pData) = ((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));

theorem Th51: :: SCMPDS_7:53

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for sp, cv, result, pp, pD being Nat st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) holds

( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for sp, cv, result, pp, pD being Nat st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) holds

( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )

proof end;

theorem Th52: :: SCMPDS_7:54

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for sp, cv, result, pp, pD being Nat

for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),result)) = 0 & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds

f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds

(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f

for s being 0 -started State of SCMPDS

for sp, cv, result, pp, pD being Nat

for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),result)) = 0 & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds

f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds

(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f

proof end;

theorem :: SCMPDS_7:55

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for sp, cv, result, pp, pD being Nat

for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds

f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds

(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f

for s being 0 -started State of SCMPDS

for sp, cv, result, pp, pD being Nat

for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds

f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds

(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f

proof end;