:: SCMPDS_7 semantic presentation

set A = the Instruction-Locations of SCMPDS ;

set D = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_7:1

for s being State of SCMPDS
for m, n being Nat st IC s = inspos m holds
ICplusConst s,(n - m) = inspos n

proof end;

theorem :: SCMPDS_7:2

for P, Q being FinPartState of SCMPDS st P c= Q holds
ProgramPart P c= ProgramPart Q

proof end;

theorem :: SCMPDS_7:3

for P, Q being programmed FinPartState of SCMPDS
for k being Nat st P c= Q holds
Shift P,k c= Shift Q,k

proof end;

theorem Th4: :: SCMPDS_7:4

for s being State of SCMPDS st IC s = inspos 0 holds
Initialized s = s

proof end;

theorem Th5: :: SCMPDS_7:5

for s being State of SCMPDS
for I being Program-block st IC s = inspos 0 holds
s +* (Initialized I) = s +* I

proof end;

theorem Th6: :: SCMPDS_7:6

for n being Nat
for s being State of SCMPDS holds ((Computation s) . n) | the Instruction-Locations of SCMPDS = s | the Instruction-Locations of SCMPDS

proof end;

theorem Th7: :: SCMPDS_7:7

for s1, s2 being State of SCMPDS st IC s1 = IC s2 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc & s1 | the Instruction-Locations of SCMPDS = s2 | the Instruction-Locations of SCMPDS holds
s1 = s2

proof end;

theorem Th8: :: SCMPDS_7:8

for l being Instruction-Location of SCMPDS
for I being Program-block holds
( l in dom I iff l in dom (Initialized I) )

proof end;

theorem :: SCMPDS_7:9

for x being set
for s being State of SCMPDS
for l being Instruction-Location of SCMPDS
for I being Program-block st x in dom I holds
I . x = (s +* (I +* (Start-At l))) . x

proof end;

theorem Th10: :: SCMPDS_7:10

for s being State of SCMPDS
for loc being Instruction-Location of SCMPDS
for I being Program-block st loc in dom I holds
(s +* (Initialized I)) . loc = I . loc

proof end;

theorem :: SCMPDS_7:11

for a being Int_position
for s being State of SCMPDS
for l being Instruction-Location of SCMPDS
for I being Program-block holds (s +* (I +* (Start-At l))) . a = s . a

proof end;

theorem Th12: :: SCMPDS_7:12

for s being State of SCMPDS
for loc being Instruction-Location of SCMPDS holds (s +* (Start-At loc)) . (IC SCMPDS ) = loc

proof end;

theorem :: SCMPDS_7:13

canceled;

theorem Th14: :: SCMPDS_7:14

for i, j being Instruction of SCMPDS
for I being Program-block holds ((I ';' i) ';' j) . (inspos (card I)) = i

proof end;

theorem Th15: :: SCMPDS_7:15

for i, j, k being Instruction of SCMPDS
for I being Program-block holds ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)

proof end;

theorem Th16: :: SCMPDS_7:16

for J, I, K being Program-block holds Shift J,(card I) c= (I ';' J) ';' K

proof end;

theorem Th17: :: SCMPDS_7:17

for I, J being Program-block holds I c= stop (I ';' J)

proof end;

theorem Th18: :: SCMPDS_7:18

for n being Nat
for loc being Instruction-Location of SCMPDS
for I being Program-block st loc in dom I holds
(Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n)

proof end;

theorem Th19: :: SCMPDS_7:19

for n being Nat
for I being Program-block st card I > 0 holds
(Shift (stop I),n) . (inspos n) = (Shift I,n) . (inspos n)

proof end;

theorem :: SCMPDS_7:20

for s being State of SCMPDS
for i being Instruction of SCMPDS st InsCode i in {0,4,5,6} holds
(Exec i,s) | SCM-Data-Loc = s | SCM-Data-Loc

proof end;

theorem :: SCMPDS_7:21

for s, ss being State of SCMPDS holds (s +* (ss | the Instruction-Locations of SCMPDS )) | SCM-Data-Loc = s | SCM-Data-Loc

proof end;

theorem :: SCMPDS_7:22

for i being Instruction of SCMPDS holds rng (Load i) = {i}

proof end;

theorem Th23: :: SCMPDS_7:23

for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st IC s1 = IC s2 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
( IC (Exec i,s1) = IC (Exec i,s2) & (Exec i,s1) | SCM-Data-Loc = (Exec i,s2) | SCM-Data-Loc )

proof end;

theorem Th24: :: SCMPDS_7:24

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
for i being Nat holds
( IC ((Computation s1) . i) = IC ((Computation s2) . i) & CurInstr ((Computation s1) . i) = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | SCM-Data-Loc = ((Computation s2) . i) | SCM-Data-Loc )

proof end;

theorem Th25: :: SCMPDS_7:25

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
for k being Nat holds
( (Computation (s1 +* (Initialized (stop I)))) . k,(Computation (s2 +* (Initialized (stop I)))) . k equal_outside the Instruction-Locations of SCMPDS & CurInstr ((Computation (s1 +* (Initialized (stop I)))) . k) = CurInstr ((Computation (s2 +* (Initialized (stop I)))) . k) )

proof end;

theorem Th26: :: SCMPDS_7:26

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
for k being Nat holds
( (Computation s1) . k,(Computation s2) . k equal_outside the Instruction-Locations of SCMPDS & CurInstr ((Computation s1) . k) = CurInstr ((Computation s2) . k) )

proof end;

theorem :: SCMPDS_7:27

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
LifeSpan s1 = LifeSpan s2

proof end;

theorem Th28: :: SCMPDS_7:28

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside the Instruction-Locations of SCMPDS )

proof end;

theorem Th29: :: SCMPDS_7:29

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & I is_halting_on s1 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside the Instruction-Locations of SCMPDS )

proof end;

theorem :: SCMPDS_7:30

for s1, s2 being State of SCMPDS
for I being Program-block st I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & ex k being Nat st (Computation s1) . k,s2 equal_outside the Instruction-Locations of SCMPDS holds
Result s1, Result s2 equal_outside the Instruction-Locations of SCMPDS

proof end;

registration

let I be Program-block;
cluster Initialized I -> initial ;
correctness

proof end;

end;

theorem Th31: :: SCMPDS_7:31

for s being State of SCMPDS
for I being Program-block
for a being Int_position st I is_halting_on s holds
(IExec I,s) . a = ((Computation (s +* (Initialized (stop I)))) . (LifeSpan (s +* (Initialized (stop I))))) . a

proof end;

theorem :: SCMPDS_7:32

for s being State of SCMPDS
for I being parahalting Program-block
for a being Int_position holds (IExec I,s) . a = ((Computation (s +* (Initialized (stop I)))) . (LifeSpan (s +* (Initialized (stop I))))) . a

proof end;

theorem Th33: :: SCMPDS_7:33

for s being State of SCMPDS
for I being Program-block
for i being Nat st Initialized (stop I) c= s & I is_closed_on s & I is_halting_on s & i < LifeSpan s holds
IC ((Computation s) . i) in dom I

proof end;

theorem Th34: :: SCMPDS_7:34

for s1, s2 being State of SCMPDS
for I being shiftable Program-block st Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 holds
for n being Nat st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
for i being Nat st i < LifeSpan s1 holds
( (IC ((Computation s1) . i)) + n = IC ((Computation s2) . i) & CurInstr ((Computation s1) . i) = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | SCM-Data-Loc = ((Computation s2) . i) | SCM-Data-Loc )

proof end;

theorem Th35: :: SCMPDS_7:35

for s being State of SCMPDS
for I being No-StopCode Program-block st Initialized (stop I) c= s & I is_halting_on s & card I > 0 holds
LifeSpan s > 0

proof end;

theorem Th36: :: SCMPDS_7:36

for s1, s2 being State of SCMPDS
for I being shiftable No-StopCode Program-block st Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 holds
for n being Nat st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
( IC ((Computation s2) . (LifeSpan s1)) = inspos ((card I) + n) & ((Computation s1) . (LifeSpan s1)) | SCM-Data-Loc = ((Computation s2) . (LifeSpan s1)) | SCM-Data-Loc )

proof end;

theorem Th37: :: SCMPDS_7:37

for s being State of SCMPDS
for I being Program-block
for n being Nat st IC ((Computation (s +* (Initialized I))) . n) = inspos 0 holds
((Computation (s +* (Initialized I))) . n) +* (Initialized I) = (Computation (s +* (Initialized I))) . n

proof end;

theorem Th38: :: SCMPDS_7:38

for s being State of SCMPDS
for I, J being Program-block
for k being Nat st I is_closed_on s & I is_halting_on s & k <= LifeSpan (s +* (Initialized (stop I))) holds
(Computation (s +* (Initialized (stop I)))) . k,(Computation (s +* ((I ';' J) +* (Start-At (inspos 0))))) . k equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th39: :: SCMPDS_7:39

for s being State of SCMPDS
for I, J being Program-block
for k being Nat st I c= J & I is_closed_on s & I is_halting_on s & k <= LifeSpan (s +* (Initialized (stop I))) holds
(Computation (s +* (Initialized J))) . k,(Computation (s +* (Initialized (stop I)))) . k equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th40: :: SCMPDS_7:40

for s being State of SCMPDS
for I, J being Program-block
for k being Nat st k <= LifeSpan (s +* (Initialized (stop I))) & I c= J & I is_closed_on s & I is_halting_on s holds
IC ((Computation (s +* (Initialized J))) . k) in dom (stop I)

proof end;

theorem Th41: :: SCMPDS_7:41

for s being State of SCMPDS
for I, J being Program-block st I c= J & I is_closed_on s & I is_halting_on s & not CurInstr ((Computation (s +* (Initialized J))) . (LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS holds
IC ((Computation (s +* (Initialized J))) . (LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)

proof end;

theorem Th42: :: SCMPDS_7:42

for s being State of SCMPDS
for I, J being Program-block st I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
( J is_closed_on (Computation (s +* (Initialized (stop I)))) . (LifeSpan (s +* (Initialized (stop I)))) & J is_halting_on (Computation (s +* (Initialized (stop I)))) . (LifeSpan (s +* (Initialized (stop I)))) )

proof end;

theorem Th43: :: SCMPDS_7:43

for s being State of SCMPDS
for I being Program-block
for J being shiftable Program-block st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )

proof end;

theorem Th44: :: SCMPDS_7:44

for s being State of SCMPDS
for I being No-StopCode Program-block
for J being Program-block st I c= J & I is_closed_on s & I is_halting_on s holds
IC ((Computation (s +* (Initialized J))) . (LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)

proof end;

theorem :: SCMPDS_7:45

for I being Program-block
for s being State of SCMPDS
for k being Nat st I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr ((Computation (s +* (Initialized (stop I)))) . k) <> halt SCMPDS

proof end;

theorem Th46: :: SCMPDS_7:46

for I, J being Program-block
for s being State of SCMPDS
for k being Nat st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr ((Computation (s +* (Initialized (stop (I ';' J))))) . k) <> halt SCMPDS

proof end;

Lm1: for I being No-StopCode Program-block
for J being shiftable Program-block
for s, s1, s2 being State of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = s +* (Initialized (stop (I ';' J))) & s1 = s +* (Initialized (stop I)) holds
( IC ((Computation s2) . (LifeSpan s1)) = inspos (card I) & ((Computation s2) . (LifeSpan s1)) | SCM-Data-Loc = (((Computation s1) . (LifeSpan s1)) +* (Initialized (stop J))) | SCM-Data-Loc & Shift (stop J),(card I) c= (Computation s2) . (LifeSpan s1) & LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )

proof end;

theorem :: SCMPDS_7:47

for s being State of SCMPDS
for I being No-StopCode Program-block
for J being shiftable Program-block st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) by Lm1;

theorem Th48: :: SCMPDS_7:48

for s being State of SCMPDS
for I being No-StopCode Program-block
for J being shiftable Program-block st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))

proof end;

theorem Th49: :: SCMPDS_7:49

for a being Int_position
for s being State of SCMPDS
for I being No-StopCode Program-block
for J being shiftable Program-block st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
(IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a

proof end;

theorem Th50: :: SCMPDS_7:50

for a being Int_position
for s being State of SCMPDS
for I being No-StopCode Program-block
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s & I is_halting_on s holds
(IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a

proof end;

definition

let a be Int_position ;
let i be Integer;
let n be Nat;
let I be Program-block;
func for-up a,i,n,I -> Program-block equals :: SCMPDS_7:def 1
(((a,i >=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,n)) ';' (goto (- ((card I) + 2)));
coherence ;

end;

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

theorem Th51: :: SCMPDS_7:51

for a being Int_position
for i being Integer
for n being Nat
for I being Program-block 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-block holds card (stop (for-up a,i,n,I)) = (card I) + 4

proof end;

theorem Th52: :: SCMPDS_7:52

for a being Int_position
for i being Integer
for n, m being Nat
for I being Program-block holds
( m < (card I) + 3 iff inspos m in dom (for-up a,i,n,I) )

proof end;

theorem Th53: :: SCMPDS_7:53

for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds
( (for-up a,i,n,I) . (inspos 0) = a,i >=0_goto ((card I) + 3) & (for-up a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,n & (for-up a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )

proof end;

Lm3: for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds for-up a,i,n,I = (a,i >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo a,i,n)) ';' (goto (- ((card I) + 2))))
by Th15;

theorem Th54: :: SCMPDS_7:54

for s being State of SCMPDS
for I being Program-block
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 & for-up a,i,n,I is_halting_on s )

proof end;

theorem Th55: :: SCMPDS_7:55

for s being State of SCMPDS
for I being Program-block
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),s = s +* (Start-At (inspos ((card I) + 3)))

proof end;

theorem :: SCMPDS_7:56

for s being State of SCMPDS
for I being Program-block
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),s) = inspos ((card I) + 3)

proof end;

theorem :: SCMPDS_7:57

for s being State of SCMPDS
for I being Program-block
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),s) . b = s . b

proof end;

Lm4: for I being Program-block
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 Th58: :: SCMPDS_7:58

for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for y being Int_position st y in X holds
(IExec I,t) . y = t . y ) ) ) holds
( for-up a,i,n,I is_closed_on s & for-up a,i,n,I is_halting_on s )

proof end;

theorem :: SCMPDS_7:59

for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for y being Int_position st y in X holds
(IExec I,t) . y = t . y ) ) ) holds
IExec (for-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s)

proof end;

registration

let I be shiftable Program-block;
let a be Int_position ;
let i be Integer;
let n be Nat;
cluster for-up a,i,n,I -> shiftable ;
correctness

proof end;

end;

registration

let I be No-StopCode Program-block;
let a be Int_position ;
let i be Integer;
let n be Nat;
cluster for-up a,i,n,I -> No-StopCode ;
correctness

proof end;

end;

definition

let a be Int_position ;
let i be Integer;
let n be Nat;
let I be Program-block;
func for-down a,i,n,I -> Program-block equals :: SCMPDS_7:def 2
(((a,i <=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 2)));
coherence ;

end;

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

theorem Th60: :: SCMPDS_7:60

for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds card (for-down a,i,n,I) = (card I) + 3

proof end;

Lm5: for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds card (stop (for-down a,i,n,I)) = (card I) + 4

proof end;

theorem Th61: :: SCMPDS_7:61

for a being Int_position
for i being Integer
for n, m being Nat
for I being Program-block holds
( m < (card I) + 3 iff inspos m in dom (for-down a,i,n,I) )

proof end;

theorem Th62: :: SCMPDS_7:62

for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds
( (for-down a,i,n,I) . (inspos 0) = a,i <=0_goto ((card I) + 3) & (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) & (for-down a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )

proof end;

Lm6: for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds for-down a,i,n,I = (a,i <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 2))))
by Th15;

theorem Th63: :: SCMPDS_7:63

for s being State of SCMPDS
for I being Program-block
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 & for-down a,i,n,I is_halting_on s )

proof end;

theorem Th64: :: SCMPDS_7:64

for s being State of SCMPDS
for I being Program-block
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),s = s +* (Start-At (inspos ((card I) + 3)))

proof end;

theorem :: SCMPDS_7:65

for s being State of SCMPDS
for I being Program-block
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),s) = inspos ((card I) + 3)

proof end;

theorem Th66: :: SCMPDS_7:66

for s being State of SCMPDS
for I being Program-block
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),s) . b = s . b

proof end;

Lm7: for I being Program-block
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 Th67: :: SCMPDS_7:67

for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for y being Int_position st y in X holds
(IExec I,t) . y = t . y ) ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )

proof end;

theorem Th68: :: SCMPDS_7:68

for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for y being Int_position st y in X holds
(IExec I,t) . y = t . y ) ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)

proof end;

registration

let I be shiftable Program-block;
let a be Int_position ;
let i be Integer;
let n be Nat;
cluster for-down a,i,n,I -> shiftable ;
correctness

proof end;

end;

registration

let I be No-StopCode Program-block;
let a be Int_position ;
let i be Integer;
let n be Nat;
cluster for-down a,i,n,I -> No-StopCode ;
correctness

proof end;

end;

definition

let n be Nat;
func sum n -> Program-block equals :: SCMPDS_7:def 3
(((GBP := 0) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0)) ';' (for-down GBP ,2,1,(Load (AddTo GBP ,3,1)));
coherence ;

end;

:: deftheorem defines sum SCMPDS_7:def 3 :

theorem Th69: :: SCMPDS_7:69

for s being State of SCMPDS st s . GBP = 0 holds
( for-down GBP ,2,1,(Load (AddTo GBP ,3,1)) is_closed_on s & for-down GBP ,2,1,(Load (AddTo GBP ,3,1)) is_halting_on s )

proof end;

theorem Th70: :: SCMPDS_7:70

for s being 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))),s) . (intpos 3) = n

proof end;

theorem :: SCMPDS_7:71

for s being State of SCMPDS
for n being Nat holds (IExec (sum n),s) . (intpos 3) = n

proof end;

definition

let sp, control, result, pp, pData be Nat;
func sum sp,control,result,pp,pData -> Program-block 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 ;

end;

:: deftheorem defines sum SCMPDS_7:def 4 :

theorem Th72: :: SCMPDS_7:72

for s being 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 & for-down (intpos sp),cv,1,((AddTo (intpos sp),result,(intpos pD),0) ';' (AddTo (intpos pp),0,1)) is_halting_on s )

proof end;

theorem Th73: :: SCMPDS_7:73

for s being 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))),s) . (DataLoc (s . (intpos sp)),result) = Sum f

proof end;

theorem :: SCMPDS_7:74

for s being 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),s) . (DataLoc (s . (intpos sp)),result) = Sum f

proof end;