:: The Construction and Computation of For-loop Programs for SCMPDS
:: by JingChao Chen and Piotr Rudnicki
::
:: Received December 27, 1999
:: Copyright (c) 1999 Association of Mizar Users

set A = NAT ;

set D = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_7:1

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

proof end;

theorem :: SCMPDS_7:2

canceled;

theorem :: SCMPDS_7:3

canceled;

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 of SCMPDS st IC s = inspos 0 holds
s +* (Initialized I) = s +* I

proof end;

theorem Th6: :: SCMPDS_7:6

for n being Element of NAT
for s being State of SCMPDS holds (Computation s,n) | NAT = s | NAT

proof end;

theorem Th7: :: SCMPDS_7:7

for s1, s2 being State of SCMPDS st IC s1 = IC s2 & DataPart s1 = DataPart s2 & s1 | NAT = s2 | NAT holds
s1 = s2

proof end;

theorem Th8: :: SCMPDS_7:8

for I being Program of SCMPDS
for l being Nat 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 of SCMPDS 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 of SCMPDS 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 of SCMPDS 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 :: SCMPDS_7:14

for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds ((I ';' i) ';' j) . (inspos (card I)) = i by SCMP_GCD:11;

theorem Th15: :: SCMPDS_7:15

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

proof end;

theorem Th16: :: SCMPDS_7:16

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

proof end;

theorem Th17: :: SCMPDS_7:17

for I, J being Program of SCMPDS holds I c= stop (I ';' J)

proof end;

theorem Th18: :: SCMPDS_7:18

for n being Element of NAT
for loc being Instruction-Location of SCMPDS
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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
DataPart (Exec i,s) = DataPart s

proof end;

theorem :: SCMPDS_7:21

for s, ss being State of SCMPDS holds (s +* (ss | NAT )) | SCM-Data-Loc = DataPart s

proof end;

theorem :: SCMPDS_7:22

for i being Instruction of SCMPDS holds rng (Load i) = {i} by FUNCOP_1:14;

theorem Th23: :: SCMPDS_7:23

for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
( IC (Exec i,s1) = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

proof end;

theorem Th24: :: SCMPDS_7:24

for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )

proof end;

theorem Th25: :: SCMPDS_7:25

for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT & 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 of SCMPDS st I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Computation s1,k, Computation s2,k equal_outside NAT & 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 of SCMPDS st I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan s1 = LifeSpan s2

proof end;

theorem Th28: :: SCMPDS_7:28

for s1, s2 being State of SCMPDS
for I being Program of SCMPDS 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 NAT holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside NAT )

proof end;

theorem Th29: :: SCMPDS_7:29

for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 holds
( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT )

proof end;

theorem :: SCMPDS_7:30

for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & ex k being Element of NAT st Computation s1,k,s2 equal_outside NAT holds
Result s1, Result s2 equal_outside NAT

proof end;

registration

let I be Program of SCMPDS ;
cluster Initialized I -> initial ;
correctness
coherence
Initialized I is initial;

proof end;

end;

theorem Th31: :: SCMPDS_7:31

for s being State of SCMPDS
for I being Program of SCMPDS
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 of SCMPDS
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 of SCMPDS
for i being Element of 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 of SCMPDS st Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 holds
for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
for i being Element of NAT st i < LifeSpan s1 holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )

proof end;

theorem Th35: :: SCMPDS_7:35

for s being State of SCMPDS
for I being No-StopCode Program of SCMPDS 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 of SCMPDS st Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 holds
for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
( IC (Computation s2,(LifeSpan s1)) = inspos ((card I) + n) & DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) )

proof end;

theorem Th37: :: SCMPDS_7:37

for s being State of SCMPDS
for I being Program of SCMPDS
for n being Element of 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 of SCMPDS
for k being Element of 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 NAT

proof end;

theorem Th39: :: SCMPDS_7:39

for s being State of SCMPDS
for I, J being Program of SCMPDS
for k being Element of 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 NAT

proof end;

theorem Th40: :: SCMPDS_7:40

for s being State of SCMPDS
for I, J being Program of SCMPDS
for k being Element of 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 of SCMPDS 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 of SCMPDS 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 of SCMPDS
for J being shiftable Program 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 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 of SCMPDS
for J being Program of SCMPDS 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 of SCMPDS
for s being State of SCMPDS
for k being Element of 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 of SCMPDS
for s being State of SCMPDS
for k being Element of 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 of SCMPDS
for J being shiftable Program of SCMPDS
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) & DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & 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 of SCMPDS
for J being shiftable Program 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 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 of SCMPDS
for J being shiftable Program 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 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 of SCMPDS
for J being shiftable Program 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 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 of SCMPDS
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 Element of NAT ;
let I be Program of SCMPDS ;
func for-up a,i,n,I -> Program of SCMPDS 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))) is Program of SCMPDS ;

end;

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

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

theorem Th51: :: SCMPDS_7:51

for a being Int_position
for i being Integer
for n being Element of NAT
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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;

theorem Th54: :: SCMPDS_7:54

for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a, c being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a, b being Int_position
for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) >= 0 holds
(IExec (for-up a,i,n,I),s) . b = s . b

proof end;

Lm3: for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS ;
let a be Int_position ;
let i be Integer;
let n be Element of NAT ;
cluster for-up a,i,n,I -> shiftable ;
correctness
coherence
for-up a,i,n,I is shiftable;

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let i be Integer;
let n be Element of NAT ;
cluster for-up a,i,n,I -> No-StopCode ;
correctness
coherence
for-up a,i,n,I is No-StopCode;

proof end;

end;

definition

let a be Int_position ;
let i be Integer;
let n be Element of NAT ;
let I be Program of SCMPDS ;
func for-down a,i,n,I -> Program of SCMPDS 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))) is Program of SCMPDS ;

end;

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

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

theorem Th60: :: SCMPDS_7:60

for a being Int_position
for i being Integer
for n being Element of NAT
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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 Element of NAT
for I being Program of SCMPDS 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;

theorem Th63: :: SCMPDS_7:63

for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a, c being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a, b being Int_position
for i being Integer
for n being Element of NAT st s . (DataLoc (s . a),i) <= 0 holds
(IExec (for-down a,i,n,I),s) . b = s . b

proof end;

Lm5: for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS
for a being Int_position
for i being Integer
for n being Element of 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 of SCMPDS ;
let a be Int_position ;
let i be Integer;
let n be Element of NAT ;
cluster for-down a,i,n,I -> shiftable ;
correctness
coherence
for-down a,i,n,I is shiftable;

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let i be Integer;
let n be Element of NAT ;
cluster for-down a,i,n,I -> No-StopCode ;
correctness
coherence
for-down a,i,n,I is No-StopCode;

proof end;

end;

definition

let n be Element of NAT ;
func sum n -> Program of SCMPDS 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))) is Program of SCMPDS ;

end;

:: deftheorem defines sum SCMPDS_7:def 3 :

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

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 Element of 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 Element of NAT holds (IExec (sum n),s) . (intpos 3) = n

proof end;

definition

let sp, control, result, pp, pData be Element of NAT ;
func sum sp,control,result,pp,pData -> Program of SCMPDS 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))) is Program of SCMPDS ;

end;

:: deftheorem defines sum SCMPDS_7:def 4 :

for sp, control, result, pp, pData being Element of 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 Th72: :: SCMPDS_7:72

for s being State of SCMPDS
for sp, cv, result, pp, pD being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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;