:: The Construction and Computation of For-loop Programs for SCMPDS
:: by JingChao Chen and Piotr Rudnicki
::
:: Received December 27, 1999
:: Copyright (c) 1999-2011 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 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

canceled;

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 P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1,P1 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & stop I c= P1 & stop I c= P2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = 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 Th25: :: SCMPDS_7:25

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (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 Th26: :: SCMPDS_7:26

for s1, s2 being State of SCMPDS
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS st I is_closed_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 holds
for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) )

proof end;

theorem :: SCMPDS_7:27

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan (P1,s1) = LifeSpan (P2,s2)

proof end;

theorem Th28: :: SCMPDS_7:28

for s1, s2 being State of SCMPDS
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )

proof end;

theorem Th29: :: SCMPDS_7:29

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s1, s2 being State of SCMPDS
for I being Program of SCMPDS 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)) & NPP (Result ((P1 +* (stop I)),(Initialize s1))) = NPP (Result ((P2 +* (stop I)),(Initialize s2))) )

proof end;

theorem :: SCMPDS_7:30

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & ex k being Element of NAT st NPP (Comput (P1,s1,k)) = NPP s2 holds
NPP (Result (P1,s1)) = NPP (Result (P2,s2))

proof end;

theorem Th31: :: SCMPDS_7:31

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position st I is_halting_on s,P holds
(IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a

proof end;

theorem :: SCMPDS_7:32

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for a being Int_position holds (IExec (I,P,s)) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by Th31, SCMPDS_6:35;

theorem Th33: :: SCMPDS_7:33

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS
for i being Element of NAT st stop I c= P & Start-At (0,SCMPDS) c= s & 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 Th34: :: SCMPDS_7:34

for s1, s2 being State of SCMPDS
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being shiftable Program of SCMPDS st stop I c= P1 & Start-At (0,SCMPDS) c= s1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Element of NAT st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of 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 Th35: :: SCMPDS_7:35

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS st stop I c= P & Start-At (0,SCMPDS) c= s & I is_halting_on s,P holds
LifeSpan (P,s) > 0

proof end;

theorem Th36: :: SCMPDS_7:36

for s1, s2 being State of SCMPDS
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free shiftable Program of SCMPDS st stop I c= P1 & Start-At (0,SCMPDS) c= s1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Element of 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 Th37: :: SCMPDS_7:37

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 0 -started State of SCMPDS
for I being Program of SCMPDS
for n being Element of NAT st IC (Comput ((P +* I),s,n)) = 0 holds
Initialize (Comput ((P +* I),s,n)) = Comput ((P +* I),s,n) by COMPOS_1:84;

theorem Th38: :: SCMPDS_7:38

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))

proof end;

theorem Th39: :: SCMPDS_7:39

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS
for k being Element of 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
NPP (Comput ((P +* J),(Initialize s),k)) = NPP (Comput ((P +* (stop I)),(Initialize s),k))

proof end;

theorem Th40: :: SCMPDS_7:40

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS
for k being Element of 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 Th41: :: SCMPDS_7:41

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS 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 Th42: :: SCMPDS_7:42

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS st 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
( 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 Th43: :: SCMPDS_7:43

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS
for J being shiftable Program 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 holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )

proof end;

theorem Th44: :: SCMPDS_7:44

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
for J being Program of SCMPDS 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:45

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS
for s being State of SCMPDS
for k being Element of 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 Th46: :: SCMPDS_7:46

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k))) <> halt SCMPDS

proof end;

Lm1: for P, P2, P1 being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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 & s2 = Initialize s & s1 = Initialize s & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = card I & DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) = DataPart (Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s2) = (LifeSpan (P1,s1)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s1))))) )

proof end;

theorem :: SCMPDS_7:47

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
for J being shiftable Program 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 holds
LifeSpan ((P +* (stop (I ';' J))),(Initialize s)) = (LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),(Initialize s)))))) by Lm1;

theorem Th48: :: SCMPDS_7:48

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
for J being shiftable Program 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 holds
IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))

proof end;

theorem Th49: :: SCMPDS_7:49

for a being Int_position
for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
for J being shiftable Program 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 holds
(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a

proof end;

theorem Th50: :: SCMPDS_7:50

for a being Int_position
for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
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;

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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,P & for-up (a,i,n,I) is_halting_on s,P )

proof end;

theorem Th55: :: SCMPDS_7:55

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,s) = s +* (Start-At (((card I) + 3),SCMPDS))

proof end;

theorem :: SCMPDS_7:56

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,s)) = (card I) + 3

proof end;

theorem :: SCMPDS_7:57

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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-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:59

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(IExec ((I ';' (AddTo (a,i,n))),P,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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,P & for-down (a,i,n,I) is_halting_on s,P )

proof end;

theorem Th64: :: SCMPDS_7:64

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,s) = s +* (Start-At (((card I) + 3),SCMPDS))

proof end;

theorem :: SCMPDS_7:65

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,s)) = (card I) + 3

proof end;

theorem Th66: :: SCMPDS_7:66

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 & a <> DataLoc ((s . a),i) & ( for t being 0 -started State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 Th68: :: SCMPDS_7:68

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 & a <> DataLoc ((s . a),i) & ( for t being 0 -started State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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,(IExec ((I ';' (AddTo (a,i,(- n)))),P,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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th70: :: SCMPDS_7:70

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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))))),P,s)) . (intpos 3) = n

proof end;

theorem :: SCMPDS_7:71

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 0 -started State of SCMPDS
for n being Element of NAT holds (IExec ((sum n),P,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 P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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 Th73: :: SCMPDS_7:73

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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))))),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f

proof end;

theorem :: SCMPDS_7:74

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f

proof end;