:: 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

begin

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 = m holds
ICplusConst (s,(n - m)) = n

proof end;

theorem :: SCMPDS_7:2

canceled;

theorem :: SCMPDS_7:3

canceled;

theorem :: SCMPDS_7:4

canceled;

theorem :: SCMPDS_7:5

canceled;

theorem :: SCMPDS_7:6

canceled;

theorem Th7: :: SCMPDS_7:7

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

proof end;

theorem :: SCMPDS_7:8

canceled;

theorem :: SCMPDS_7:9

canceled;

theorem :: SCMPDS_7:10

canceled;

theorem :: SCMPDS_7:11

canceled;

theorem :: SCMPDS_7:12

canceled;

theorem :: SCMPDS_7:13

canceled;

theorem :: SCMPDS_7:14

canceled;

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, loc being Element of NAT
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)) . n = (Shift (I,n)) . 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

canceled;

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 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),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
( Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT & CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (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 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),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 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),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 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) & Result ((ProgramPart s1),s1), Result ((ProgramPart s2),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 ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) & Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))), Result ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (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 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & ex k being Element of NAT st Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT holds
Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT

proof 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 = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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 = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . a by Th31, SCMPDS_6:35;

theorem Th33: :: SCMPDS_7:33

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

proof end;

theorem Th35: :: SCMPDS_7:35

for s being State of SCMPDS
for I being halt-free Program of SCMPDS st Initialize (stop I) c= s & I is_halting_on s & card I > 0 holds
LifeSpan ((ProgramPart s),s) > 0

proof end;

theorem Th36: :: SCMPDS_7:36

for s1, s2 being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS st Initialize (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 = n & DataPart s1 = DataPart s2 holds
( IC (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = (card I) + n & DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) )

proof end;

theorem Th37: :: SCMPDS_7:37

for s being 0 -started State of SCMPDS
for I being Program of SCMPDS
for n being Element of NAT st IC (Comput ((ProgramPart (s +* I)),(s +* I),n)) = 0 holds
(Initialize (Comput ((ProgramPart (s +* I)),(s +* I),n))) +* I = Comput ((ProgramPart (s +* I)),(s +* 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 ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),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 ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),k), Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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 ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) & I c= J & I is_closed_on s & I is_halting_on s holds
IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* 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 ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS holds
IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = 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 Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) & J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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 halt-free 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 (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = 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 ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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 ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))) <> halt SCMPDS

proof end;

Lm1: for I being halt-free 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 = (Initialize s) +* (stop (I ';' J)) & s1 = (Initialize s) +* (stop I) holds
( IC (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s2),s2) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )

proof end;

theorem :: SCMPDS_7:47

for s being State of SCMPDS
for I being halt-free 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 ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J)))) = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) by Lm1;

theorem Th48: :: SCMPDS_7:48

for s being State of SCMPDS
for I being halt-free 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)),SCMPDS))

proof end;

theorem Th49: :: SCMPDS_7:49

for a being Int_position
for s being State of SCMPDS
for I being halt-free 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 halt-free 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;

begin

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)));

begin

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 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)) . 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 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 (((card I) + 3),SCMPDS))

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)) = (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 halt-free shiftable 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 halt-free shiftable 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 halt-free 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) -> halt-free ;
correctness
coherence
for-up (a,i,n,I) is halt-free ;

proof end;

end;

begin

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)));

begin

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 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)) . 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 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 (((card I) + 3),SCMPDS))

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)) = (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 halt-free shiftable 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 0 -started 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 0 -started State of SCMPDS
for I being halt-free shiftable 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 0 -started 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 halt-free 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) -> halt-free ;
correctness
coherence
for-down (a,i,n,I) is halt-free ;

proof end;

end;

begin

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 0 -started 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 0 -started 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 0 -started 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 0 -started 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 0 -started 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 0 -started 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;