:: The Construction and Computation of For-loop Programs for SCMPDS
:: by JingChao Chen and Piotr Rudnicki
::
:: Received December 27, 1999
:: Copyright (c) 1999-2021 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 Nat st IC s = m holds
ICplusConst (s,(n - m)) = n
proof end;

theorem Th2: :: SCMPDS_7:2
for i, j, k being Instruction of SCMPDS
for I being Program of holds ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)
proof end;

theorem Th3: :: SCMPDS_7:3
for I, J, K being Program of holds Shift (J,(card I)) c= (I ';' J) ';' K
proof end;

theorem Th4: :: SCMPDS_7:4
for I, J being Program of holds I c= stop (I ';' J)
proof end;

theorem :: SCMPDS_7:5
canceled;

theorem :: SCMPDS_7:6
canceled;

::$CT 2
theorem :: SCMPDS_7:7
for s being State of SCMPDS
for i being Instruction of SCMPDS st InsCode i in {0,4,5,6,14} holds
DataPart (Exec (i,s)) = DataPart s
proof end;

theorem Th6: :: SCMPDS_7:8
for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being State of SCMPDS
for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Nat holds
( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )
proof end;

theorem Th7: :: SCMPDS_7:9
for P1, P2 being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of st I is_closed_on s,P1 & stop I c= P1 & stop I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
proof end;

theorem Th8: :: SCMPDS_7:10
for P1, P2 being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
proof end;

theorem Th9: :: SCMPDS_7:11
for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being State of SCMPDS
for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )
proof end;

theorem :: SCMPDS_7:12
for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being 0 -started State of SCMPDS
for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds
Result (P1,s1) = Result (P2,s2)
proof end;

theorem Th11: :: SCMPDS_7:13
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position st I is_halting_on s,P holds
(IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_6:def 3, EXTPRO_1:23;

theorem :: SCMPDS_7:14
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being parahalting Program of
for a being Int_position holds (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_6:21, Th11;

theorem Th13: :: SCMPDS_7:15
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of
for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
proof end;

theorem Th14: :: SCMPDS_7:16
for s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat st i < LifeSpan (P1,s1) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
proof end;

theorem Th15: :: SCMPDS_7:17
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of st stop I c= P & I is_halting_on s,P holds
LifeSpan (P,s) > 0
proof end;

theorem Th16: :: SCMPDS_7:18
for s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for I being halt-free shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )
proof end;

theorem Th17: :: SCMPDS_7:19
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
proof end;

theorem Th18: :: SCMPDS_7:20
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)
proof end;

theorem Th19: :: SCMPDS_7:21
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for k being Nat st k <= LifeSpan ((P +* (stop I)),(Initialize s)) & I c= J & I is_closed_on s,P & I is_halting_on s,P holds
IC (Comput ((P +* J),(Initialize s),k)) in dom (stop I)
proof end;

theorem Th20: :: SCMPDS_7:22
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
proof end;

theorem Th21: :: SCMPDS_7:23
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I, J being Program of st I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) )
proof end;

theorem Th22: :: SCMPDS_7:24
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I being Program of
for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
proof end;

theorem Th23: :: SCMPDS_7:25
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I being halt-free Program of
for J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
proof end;

theorem :: SCMPDS_7:26
for P being Instruction-Sequence of SCMPDS
for I being Program of
for s being State of SCMPDS
for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
proof end;

theorem Th25: :: SCMPDS_7:27
for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for s being 0 -started State of SCMPDS
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k))) <> halt SCMPDS
proof end;

Lm1: for P, P1, P2 being Instruction-Sequence of SCMPDS
for I being halt-free Program of
for J being shiftable Program of
for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P & P2 = P +* (stop (I ';' J)) & P1 = P +* (stop I) holds
( IC (Comput (P2,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P2,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P2 & LifeSpan (P2,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
proof end;

theorem :: SCMPDS_7:28
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of
for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds
LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) by Lm1;

theorem Th27: :: SCMPDS_7:29
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of
for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds
IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
proof end;

theorem Th28: :: SCMPDS_7:30
for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of
for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds
(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a
proof end;

theorem Th29: :: SCMPDS_7:31
for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
(IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
proof end;

:: while (a,i)<=0 do { I, (a,i)+=n }
definition
let a be Int_position;
let i be Integer;
let n be Nat;
let I be Program of ;
func for-up (a,i,n,I) -> Program of equals :: SCMPDS_7:def 1
((((a,i) >=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)));
coherence
((((a,i) >=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2))) is Program of ;
end;

:: deftheorem defines for-up SCMPDS_7:def 1 :
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds for-up (a,i,n,I) = ((((a,i) >=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)));

theorem Th30: :: SCMPDS_7:32
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3
proof end;

Lm2: for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4
proof end;

theorem Th31: :: SCMPDS_7:33
for a being Int_position
for i being Integer
for n, m being Nat
for I being Program of holds
( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )
proof end;

theorem Th32: :: SCMPDS_7:34
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds
( (for-up (a,i,n,I)) . 0 = (a,i) >=0_goto ((card I) + 3) & (for-up (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,n) & (for-up (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
proof end;

theorem Th33: :: SCMPDS_7:35
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
proof end;

theorem Th34: :: SCMPDS_7:36
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a, c being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
IExec ((for-up (a,i,n,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))
proof end;

theorem :: SCMPDS_7:37
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
IC (IExec ((for-up (a,i,n,I)),P,(Initialize s))) = (card I) + 3
proof end;

theorem :: SCMPDS_7:38
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a, b being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) >= 0 holds
(IExec ((for-up (a,i,n,I)),P,(Initialize s))) . b = s . b
proof end;

Lm3: for I being Program of
for a being Int_position
for i being Integer
for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)
proof end;

theorem Th37: :: SCMPDS_7:39
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
proof end;

theorem :: SCMPDS_7:40
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
proof end;

registration
let I be shiftable Program of ;
let a be Int_position;
let i be Integer;
let n be 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 ;
let a be Int_position;
let i be Integer;
let n be Nat;
cluster for-up (a,i,n,I) -> halt-free ;
correctness
coherence
for-up (a,i,n,I) is halt-free ;
proof end;
end;

:: while (a,i)>=0 do { I, (a,i)-=n }
definition
let a be Int_position;
let i be Integer;
let n be Nat;
let I be Program of ;
func for-down (a,i,n,I) -> Program of equals :: SCMPDS_7:def 2
((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2)));
coherence
((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))) is Program of ;
end;

:: deftheorem defines for-down SCMPDS_7:def 2 :
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds for-down (a,i,n,I) = ((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2)));

theorem Th39: :: SCMPDS_7:41
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3
proof end;

Lm4: for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds card (stop (for-down (a,i,n,I))) = (card I) + 4
proof end;

theorem Th40: :: SCMPDS_7:42
for a being Int_position
for i being Integer
for n, m being Nat
for I being Program of holds
( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )
proof end;

theorem Th41: :: SCMPDS_7:43
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
proof end;

theorem Th42: :: SCMPDS_7:44
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) <= 0 holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
proof end;

theorem Th43: :: SCMPDS_7:45
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a, c being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) <= 0 holds
IExec ((for-down (a,i,n,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS))
proof end;

theorem :: SCMPDS_7:46
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) <= 0 holds
IC (IExec ((for-down (a,i,n,I)),P,(Initialize s))) = (card I) + 3
proof end;

theorem Th45: :: SCMPDS_7:47
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a, b being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) <= 0 holds
(IExec ((for-down (a,i,n,I)),P,(Initialize s))) . b = s . b
proof end;

Lm5: for I being Program of
for a being Int_position
for i being Integer
for n being Nat holds Shift (I,1) c= for-down (a,i,n,I)
proof end;

theorem Th46: :: SCMPDS_7:48
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) > 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,t)) . y = t . y ) ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
proof end;

theorem Th47: :: SCMPDS_7:49
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) > 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,t)) . y = t . y ) ) ) holds
IExec ((for-down (a,i,n,I)),P,s) = IExec ((for-down (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))))
proof end;

registration
let I be shiftable Program of ;
let a be Int_position;
let i be Integer;
let n be 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 ;
let a be Int_position;
let i be Integer;
let n be Nat;
cluster for-down (a,i,n,I) -> halt-free ;
correctness
coherence
for-down (a,i,n,I) is halt-free ;
proof end;
end;

:: n=Sum 1+1+...+1
definition
let n be Nat;
func sum n -> Program of equals :: SCMPDS_7:def 3
(((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))));
coherence
(((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)) ';' (for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))) is Program of ;
end;

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

theorem Th48: :: SCMPDS_7:50
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . GBP = 0 holds
( for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on s,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P )
proof end;

theorem Th49: :: SCMPDS_7:51
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Nat st s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n
proof end;

theorem :: SCMPDS_7:52
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n
proof end;

:: sum=Sum x1+x2+...+x2
definition
let sp, control, result, pp, pData be Nat;
func sum (sp,control,result,pp,pData) -> Program of equals :: SCMPDS_7:def 4
((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1)))));
coherence
((((intpos sp),result) := 0) ';' ((intpos pp) := pData)) ';' (for-down ((intpos sp),control,1,((AddTo ((intpos sp),result,(intpos pData),0)) ';' (AddTo ((intpos pp),0,1))))) is Program of ;
end;

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

theorem Th51: :: SCMPDS_7:53
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Nat st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) holds
( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )
proof end;

theorem Th52: :: SCMPDS_7:54
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Nat
for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),result)) = 0 & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
proof end;

theorem :: SCMPDS_7:55
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Nat
for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
proof end;