let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: thesis:
let a be Int_position ; :: thesis:
let i be Integer; :: thesis:
let n be Element of NAT ; :: thesis:
let X be set ; :: thesis:
set b = DataLoc ((s . a),i);
set FOR = for-up (a,i,n,I);
set pFOR = stop (for-up (a,i,n,I));
set s1 = s;
set P1 = P +* (stop (for-up (a,i,n,I)));
set i1 = (a,i) >=0_goto ((card I) + 3);
set i2 = AddTo (a,i,n);
set i3 = goto (- ((card I) + 2));
assume A2: s . (DataLoc ((s . a),i)) < 0 ; :: thesis:
set s4 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,1);
set P4 = P +* (stop (for-up (a,i,n,I)));
A3: IC s = 0 by MEMSTR_0:def 8;
set m0 = LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s);
set l2 = (card I) + 2;
set sI = s;
set PI = P +* (stop I);
set m1 = (LifeSpan ((P +* (stop I)),s)) + 3;
set J = I ';' (AddTo (a,i,n));
set sJ = s;
set PJ = P +* (stop (I ';' (AddTo (a,i,n))));
set s2 = Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s));
set P2 = P +* (stop (for-up (a,i,n,I)));
set m2 = LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))));
set Es = IExec ((I ';' (AddTo (a,i,n))),P,s);
set bj = DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i);
A7: stop I c= P +* (stop I) by FUNCT_4:25;
A11: for-up (a,i,n,I) = ((a,i) >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)))) by Th15;
set mI = LifeSpan ((P +* (stop I)),s);
set s5 = Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)));
set P5 = P +* (stop (for-up (a,i,n,I)));
set l1 = (card I) + 1;
set m3 = (LifeSpan ((P +* (stop I)),s)) + 1;
set s6 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1));
set P6 = P +* (stop (for-up (a,i,n,I)));
set s7 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1));
set P7 = P +* (stop (for-up (a,i,n,I)));
A12: stop (for-up (a,i,n,I)) c= P +* (stop (for-up (a,i,n,I))) by FUNCT_4:25;
for-up (a,i,n,I) c= stop (for-up (a,i,n,I)) by AFINSQ_1:74;
then A13: for-up (a,i,n,I) c= P +* (stop (for-up (a,i,n,I))) by A12, XBOOLE_1:1;
Shift (I,1) c= for-up (a,i,n,I) by Lm3;
then A14: Shift (I,1) c= P +* (stop (for-up (a,i,n,I))) by A13, XBOOLE_1:1;
(card I) + 2 < (card I) + 3 by XREAL_1:6;
then A15: (card I) + 2 in dom (for-up (a,i,n,I)) by Th52;
set m5 = (((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1;
set s8 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1));
(card I) + 1 < (card I) + 3 by XREAL_1:6;
then A17: (card I) + 1 in dom (for-up (a,i,n,I)) by Th52;
assume A18: not DataLoc ((s . a),i) in X ; :: thesis:
assume A19: n > 0 ; :: thesis:
assume A21: a <> DataLoc ((s . a),i) ; :: thesis:
I: Initialize s = s by MEMSTR_0:44;
assume A22: 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 ) ) ; :: thesis:
then for-up (a,i,n,I) is_halting_on s,P by A2, A18, A19, A21, Th58;
then A23: P +* (stop (for-up (a,i,n,I))) halts_on s by SCMPDS_6:def 3, I;
A24: for x being Int_position st x in X holds
s . x = s . x ;
then A25: (IExec (I,P,s)) . (DataLoc ((s . a),i)) = s . (DataLoc ((s . a),i)) by A22, I;
A26: (IExec (I,P,s)) . a = s . a by A22, A24, I;
A27: DataLoc ((s . a),i) = DataLoc (((IExec (I,P,s)) . a),i) by A22, A24, I;
A28: (IExec (I,P,s)) . a = s . a by A22, A24, I;
A29: Comput ((P +* (stop (for-up (a,i,n,I)))),s,(0 + 1)) = Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,0))) by EXTPRO_1:3
.= Following ((P +* (stop (for-up (a,i,n,I)))),s) by EXTPRO_1:2
.= Exec (((a,i) >=0_goto ((card I) + 3)),s) by A11, SCMPDS_6:11, I ;
A30: IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)) = succ (IC s) by A2, A29, SCMPDS_2:57
.= 0 + 1 by A3 ;
for a being Int_position holds s . a = (Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)) . a by A29, SCMPDS_2:57;
then A32: DataPart s = DataPart (Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)) by SCMPDS_4:8;
A33: I is_halting_on s,P by A22, A24;
then A34: P +* (stop I) halts_on s by SCMPDS_6:def 3, I;
(P +* (stop I)) +* (stop I) halts_on s by A34, FUNCT_4:25, FUNCT_4:98;
then A36: I is_halting_on s,P +* (stop I) by SCMPDS_6:def 3, I;
A37: I is_closed_on s,P by A22, A24;
then A38: (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc ((s . a),i)) = (Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . (DataLoc ((s . a),i)) by A33, Th50
.= ((IExec (I,P,s)) . (DataLoc ((s . a),i))) + n by A26, SCMPDS_2:48
.= (s . (DataLoc ((s . a),i))) + n by A22, A24, I ;
A39: I is_closed_on s,P +* (stop I) by A22, A24;
then A40: IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) = (card I) + 1 by A7, A36, A30, A32, A14, Th36;
A41: (P +* (stop (for-up (a,i,n,I)))) /. (IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (for-up (a,i,n,I)))) . (IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;
A42: Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s))) by EXTPRO_1:4;
then A43: CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (for-up (a,i,n,I)))) . ((card I) + 1) by A7, A36, A39, A30, A32, A14, Th36, A41
.= (for-up (a,i,n,I)) . ((card I) + 1) by A17, A13, GRFUNC_1:2
.= AddTo (a,i,n) by Th53 ;
A44: DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) by A7, A36, A39, A30, A32, A14, Th36;
then A45: (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . a = (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . a by SCMPDS_4:8
.= s . a by A28, A34, EXTPRO_1:23 ;
A46: (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a = (Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . a by A37, A33, Th50
.= s . a by A21, A26, SCMPDS_2:48 ;

now

per cases ) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) >= 0 or (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) < 0 ) ;

suppose (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) >= 0 ; :: thesis:

hence for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),P by Th54; :: thesis:

end;

suppose A47: (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) < 0 ; :: thesis:

now

let t be State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A48: for x being Int_position st x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x and
A49: t . a = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a ; :: thesis:

A50: now

let x be Int_position ; :: thesis:
assume A51: x in X ; :: thesis:
hence t . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x by A48
.= (Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . x by A37, A33, Th50
.= (IExec (I,P,s)) . x by A18, A26, A51, SCMPDS_2:48
.= s . x by A22, A24, A51, I ;
:: thesis:

end;

hence (IExec (I,Q,(Initialize t))) . a = t . a by A22, A46, A49; :: thesis:
thus (IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) by A22, A46, A49, A50; :: thesis:
thus ( 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 ) ) by A22, A46, A49, A50; :: thesis:

end;

hence for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),P by A18, A19, A21, A46, A47, Th58; :: thesis:

end;

then A52: P +* (stop (for-up (a,i,n,I))) halts_on Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)) by SCMPDS_6:def 3;
A55: Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)) = Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by EXTPRO_1:3
.= Exec ((AddTo (a,i,n)),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by A43 ;
then A56: IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) = succ (IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by SCMPDS_2:48
.= ((card I) + 1) + 1 by A40, A42, NAT_1:38
.= (card I) + (1 + 1) ;
then A57: CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)))) = (P +* (stop (for-up (a,i,n,I)))) . ((card I) + 2) by PBOOLE:143
.= (for-up (a,i,n,I)) . ((card I) + 2) by A13, A15, GRFUNC_1:2
.= goto (- ((card I) + 2)) by Th53 ;
A59: Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1)) = Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card I) + 2))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)))) by A57 ;
then IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:54
.= 0 by A56, Th1 ;
then A60: IC (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) = IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 3))) by MEMSTR_0:def 8;
A61: (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . (DataLoc ((s . a),i)) = (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . (DataLoc ((s . a),i)) by A44, SCMPDS_4:8
.= s . (DataLoc ((s . a),i)) by A25, A34, EXTPRO_1:23 ;
A62: (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . (DataLoc ((s . a),i)) by A59, SCMPDS_2:54
.= (s . (DataLoc ((s . a),i))) + n by A45, A61, A42, A55, SCMPDS_2:48 ;

now

let x be Int_position ; :: thesis:
A63: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
then A64: (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x by FUNCT_4:11;

per cases ;

suppose x = DataLoc ((s . a),i) ; :: thesis:

hence (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . x = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . x by A62, A38, A63, FUNCT_4:11; :: thesis:

end;

suppose A65: x <> DataLoc ((s . a),i) ; :: thesis:

A67: (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x = (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . x by A44, SCMPDS_4:8
.= (IExec (I,P,s)) . x by A34, EXTPRO_1:23 ;
A68: (Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x by A45, A42, A55, A65, SCMPDS_2:48;
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . x = (Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . x by A37, A33, Th50
.= (IExec (I,P,s)) . x by A27, A65, SCMPDS_2:48 ;
hence (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . x = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . x by A59, A64, A67, A68, SCMPDS_2:54; :: thesis:

end;

then A69: DataPart (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) = DataPart (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) by SCMPDS_4:8;
A71: Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 3)) = Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)) by A69, A60, MEMSTR_0:78;
then CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 3)))) = (a,i) >=0_goto ((card I) + 3) by A11, SCMPDS_6:11;
then LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s) > (LifeSpan ((P +* (stop I)),s)) + 3 by A23, EXTPRO_1:36;
then consider nn being Nat such that
A72: LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s) = ((LifeSpan ((P +* (stop I)),s)) + 3) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 12;
Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 3) + (LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))))) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),(LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))))) by A71, EXTPRO_1:4;
then CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 3) + (LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))))))) = halt SCMPDS by A52, EXTPRO_1:def 15;
then ((LifeSpan ((P +* (stop I)),s)) + 3) + (LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))) >= LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s) by A23, EXTPRO_1:def 15;
then A74: LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) >= nn by A72, XREAL_1:6;
A75: Comput ((P +* (stop (for-up (a,i,n,I)))),s,(LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s))) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),nn) by A71, A72, EXTPRO_1:4;
then CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),nn))) = halt SCMPDS by A23, EXTPRO_1:def 15;
then nn >= LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) by A52, EXTPRO_1:def 15;
then nn = LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) by A74, XXREAL_0:1;
then Result ((P +* (stop (for-up (a,i,n,I)))),s) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),(LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))))) by A23, A75, EXTPRO_1:23;
hence 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)))) by A52, EXTPRO_1:23; :: thesis: