let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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-down (a,i,n,I);
set pFOR = stop (for-down (a,i,n,I));
set s1 = Initialize s;
set ps = ProgramPart s;
set P1 = P +* (stop (for-down (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-down (a,i,n,I)))),(Initialize s),1);
set P4 = P +* (stop (for-down (a,i,n,I)));
A3: IC (Initialize s) = 0 by COMPOS_1:def 16;
A4: not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
set m0 = LifeSpan ((P +* (stop (for-down (a,i,n,I)))),(Initialize s));
set l2 = (card I) + 2;
set sI = Initialize s;
set PI = P +* (stop I);
set m1 = (LifeSpan ((P +* (stop I)),(Initialize s))) + 3;
set J = I ';' (AddTo (a,i,(- n)));
set sJ = Initialize 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-down (a,i,n,I)));
set m2 = LifeSpan ((P +* (stop (for-down (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:26;
B7: Start-At (0,SCMPDS) c= Initialize s by FUNCT_4:26;
A8: dom (ProgramPart s) = NAT by COMPOS_1:34;
A9: not a in dom (s | NAT) by A8, SCMPDS_2:53;
A10: not DataLoc ((s . a),i) in dom (s | NAT) by A8, SCMPDS_2:53;
A11: for-down (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)),(Initialize s));
set s5 = Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P5 = P +* (stop (for-down (a,i,n,I)));
set l1 = (card I) + 1;
set m3 = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1;
set s6 = Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1));
set P6 = P +* (stop (for-down (a,i,n,I)));
set s7 = Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1));
set P7 = P +* (stop (for-down (a,i,n,I)));
A12: stop (for-down (a,i,n,I)) c= P +* (stop (for-down (a,i,n,I))) by FUNCT_4:26;
for-down (a,i,n,I) c= stop (for-down (a,i,n,I)) by AFINSQ_1:78;
then A13: for-down (a,i,n,I) c= P +* (stop (for-down (a,i,n,I))) by A12, XBOOLE_1:1;
Shift (I,1) c= for-down (a,i,n,I) by Lm5;
then Shift (I,1) c= P +* (stop (for-down (a,i,n,I))) by A13, XBOOLE_1:1;
then A14: Shift (I,1) c= P +* (stop (for-down (a,i,n,I))) ;
(card I) + 2 < (card I) + 3 by XREAL_1:8;
then A15: (card I) + 2 in dom (for-down (a,i,n,I)) by Th61;
set m5 = (((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1) + 1;
set s8 = Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1) + 1));
A16: dom (ProgramPart s) = (dom s) /\ NAT by RELAT_1:90
.= (({(IC )} \/ SCM-Data-Loc) \/ NAT) /\ NAT by SCMPDS_4:19
.= NAT by XBOOLE_1:21 ;
(card I) + 1 < (card I) + 3 by XREAL_1:8;
then A17: (card I) + 1 in dom (for-down (a,i,n,I)) by Th61;
assume A18: not DataLoc ((s . a),i) in X ; :: thesis:
assume A19: n > 0 ; :: thesis:
assume A21: a <> DataLoc ((s . a),i) ; :: thesis:
assume A22: 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 ) ) ; :: thesis:
then for-down (a,i,n,I) is_halting_on s,P by A2, A18, A19, A21, Th67;
then A23: P +* (stop (for-down (a,i,n,I))) halts_on Initialize s by SCMPDS_6:def 3;
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;
A26: (IExec (I,P,s)) . a = s . a by A22, A24;
A27: DataLoc ((s . a),i) = DataLoc (((IExec (I,P,s)) . a),i) by A22, A24;
A28: (IExec (I,P,s)) . a = s . a by A22, A24;
A29: Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(0 + 1)) = Following ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),0))) by EXTPRO_1:4
.= Following ((P +* (stop (for-down (a,i,n,I)))),(Initialize s)) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 3)),(Initialize s)) by A11, SCMPDS_6:22 ;
not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
then (Initialize s) . (DataLoc (((Initialize s) . a),i)) = (Initialize s) . (DataLoc ((s . a),i)) by FUNCT_4:12
.= s . (DataLoc ((s . a),i)) by A4, FUNCT_4:12 ;
then A30: IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)) = succ (IC (Initialize s)) by A2, A29, SCMPDS_2:68
.= 0 + 1 by A3 ;

now

let a be Int_position ; :: thesis:
thus (Initialize s) . a = (Initialize s) . a
.= (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)) . a by A29, SCMPDS_2:68 ; :: thesis:

end;

then A32: DataPart (Initialize s) = DataPart (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)) by SCMPDS_4:23;
A33: I is_halting_on s,P by A22, A24;
then A34: P +* (stop I) halts_on Initialize s by SCMPDS_6:def 3;
P +* (stop I) = (P +* (stop I)) +* (stop I) by A7, FUNCT_4:104;
then (P +* (stop I)) +* (stop I) halts_on Initialize (Initialize s) by A34;
then A36: I is_halting_on Initialize s,P +* (stop I) by SCMPDS_6:def 3;
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:60
.= (s . (DataLoc ((s . a),i))) + (- n) by A22, A24 ;
A39: (P +* (stop (for-down (a,i,n,I)))) /. (IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) = (P +* (stop (for-down (a,i,n,I)))) . (IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by PBOOLE:158;
A40: I is_closed_on Initialize s,P +* (stop I) by A37, SCMPDS_6:38;
then A41: IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) = (card I) + 1 by A7, B7, A36, A30, A32, A14, Th36;
A42: Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)) = Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s)))) by EXTPRO_1:5;
then A43: CurInstr ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) = (P +* (stop (for-down (a,i,n,I)))) . ((card I) + 1) by A7, B7, A36, A40, A30, A32, A14, Th36, A39
.= (P +* (stop (for-down (a,i,n,I)))) . ((card I) + 1)
.= (P +* (stop (for-down (a,i,n,I)))) . ((card I) + 1)
.= (for-down (a,i,n,I)) . ((card I) + 1) by A17, A13, GRFUNC_1:8
.= AddTo (a,i,(- n)) by Th62 ;
A44: DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A7, B7, A36, A40, A30, A32, A14, Th36;
then A45: (Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by SCMPDS_4:23
.= (Result ((P +* (stop I)),(Initialize s))) . a by A34, EXTPRO_1:23
.= s . a by A28, A9, FUNCT_4:12 ;
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:60 ;

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-down (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,(- n)))),P,s),P by Th63; :: 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 0 -started State of SCMPDS; :: thesis:
let Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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:60
.= s . x by A22, A24, A51 ;
:: thesis:

end;

hence (IExec (I,Q,t)) . a = t . a by A22, A46, A49; :: thesis:
thus (IExec (I,Q,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,t)) . y = t . y ) ) by A22, A46, A49, A50; :: thesis:

end;

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

end;

then A52: P +* (stop (for-down (a,i,n,I))) halts_on Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s)) by SCMPDS_6:def 3;
A53: (P +* (stop (for-down (a,i,n,I)))) /. (IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)))) = (P +* (stop (for-down (a,i,n,I)))) . (IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)))) by PBOOLE:158;
A55: Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)) = Following ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by EXTPRO_1:4
.= Exec ((AddTo (a,i,(- n))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by A43 ;
then A56: IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) = succ (IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by SCMPDS_2:60
.= ((card I) + 1) + 1 by A41, A42, NAT_1:39
.= (card I) + (1 + 1) ;
then A57: CurInstr ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)))) = (P +* (stop (for-down (a,i,n,I)))) . ((card I) + 2) by A53
.= (for-down (a,i,n,I)) . ((card I) + 2) by A13, A15, GRFUNC_1:8
.= goto (- ((card I) + 2)) by Th62 ;
A59: Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1) + 1)) = Following ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)))) by EXTPRO_1:4
.= Exec ((goto (- ((card I) + 2))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)))) by A57 ;
then IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:66
.= 0 by A56, Th1 ;
then A60: IC (Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))) = IC (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 3))) by COMPOS_1:def 16;
A61: (Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) . (DataLoc ((s . a),i)) = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . (DataLoc ((s . a),i)) by A44, SCMPDS_4:23
.= (Result ((P +* (stop I)),(Initialize s))) . (DataLoc ((s . a),i)) by A34, EXTPRO_1:23
.= s . (DataLoc ((s . a),i)) by A25, A10, FUNCT_4:12 ;
A62: (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) . (DataLoc ((s . a),i)) by A59, SCMPDS_2:66
.= (s . (DataLoc ((s . a),i))) + (- n) by A45, A61, A42, A55, SCMPDS_2:60 ;

now

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

per cases ;

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

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

end;

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

A66: not x in dom (s | NAT) by A8, SCMPDS_2:53;
A67: (Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) . x = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . x by A44, SCMPDS_4:23
.= (Result ((P +* (stop I)),(Initialize s))) . x by A34, EXTPRO_1:23
.= (IExec (I,P,s)) . x by A66, FUNCT_4:12 ;
A68: (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) . x = (Comput ((P +* (stop (for-down (a,i,n,I)))),(Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) . x by A45, A42, A55, A65, SCMPDS_2:60;
(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:60 ;
hence (Comput ((P +* (stop (for-down (a,i,n,I)))),(Initialize s),((((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1) + 1))) . x = (Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))) . x by A59, A64, A67, A68, SCMPDS_2:66; :: thesis:

end;