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) +* (stop (for-down (a,i,n,I)));
set ps = ProgramPart s;
I1: s +* (Initialize (stop (for-down (a,i,n,I)))) = (Initialize s) +* (stop (for-down (a,i,n,I))) by COMPOS_1:125;
set i1 = (a,i) <=0_goto ((card I) + 3);
set i2 = AddTo (a,i,(- n));
set i3 = goto (- ((card I) + 2));
assume A1: s . (DataLoc ((s . a),i)) > 0 ; :: thesis:
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1);
A2: IC ((Initialize s) +* (stop (for-down (a,i,n,I)))) = 0 by SCMPDS_6:21;
A3: not DataLoc ((s . a),i) in dom (Initialize (stop (for-down (a,i,n,I)))) by SCMPDS_4:31;
set m0 = LifeSpan ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))));
set l2 = (card I) + 2;
set sI = (Initialize s) +* (stop I);
set m1 = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3;
set J = I ';' (AddTo (a,i,(- n)));
set sJ = (Initialize s) +* (stop (I ';' (AddTo (a,i,(- n)))));
set s2 = (Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)));
set m2 = LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))));
I2: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
I4: (IExec ((I ';' (AddTo (a,i,(- n)))),s)) +* (Initialize (stop (for-down (a,i,n,I)))) = (Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))) by COMPOS_1:125;
set Es = IExec ((I ';' (AddTo (a,i,(- n)))),s);
set bj = DataLoc (((IExec ((I ';' (AddTo (a,i,(- n)))),s)) . a),i);
A4: Initialize (stop I) c= (Initialize s) +* (stop I) by I2, FUNCT_4:26;
A5: dom (ProgramPart s) = NAT by COMPOS_1:34;
A6: not a in dom (s | NAT) by A5, SCMPDS_2:53;
A7: not DataLoc ((s . a),i) in dom (s | NAT) by A5, SCMPDS_2:53;
A8: 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 ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set s5 = Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
set l1 = (card I) + 1;
set m3 = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1;
set s6 = Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1));
set s7 = Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1));
A9: Initialize (stop (for-down (a,i,n,I))) c= (Initialize s) +* (stop (for-down (a,i,n,I))) by I1, FUNCT_4:26;
for-down (a,i,n,I) c= Initialize (stop (for-down (a,i,n,I))) by SCMPDS_6:17;
then A10: for-down (a,i,n,I) c= (Initialize s) +* (stop (for-down (a,i,n,I))) by A9, XBOOLE_1:1;
Shift (I,1) c= for-down (a,i,n,I) by Lm5;
then Shift (I,1) c= (Initialize s) +* (stop (for-down (a,i,n,I))) by A10, XBOOLE_1:1;
then A11: Shift (I,1) c= Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1) by AMI_1:81;
(card I) + 2 < (card I) + 3 by XREAL_1:8;
then A12: (card I) + 2 in dom (for-down (a,i,n,I)) by Th61;
set m5 = (((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1;
set s8 = Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1));
A13: dom (ProgramPart s) = (dom s) /\ NAT by RELAT_1:90
.= (({(IC SCMPDS)} \/ 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 A14: (card I) + 1 in dom (for-down (a,i,n,I)) by Th61;
assume A15: not DataLoc ((s . a),i) in X ; :: thesis:
assume A16: n > 0 ; :: thesis:
assume A17: card I > 0 ; :: thesis:
assume A18: a <> DataLoc ((s . a),i) ; :: thesis:
assume A19: 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 ) ) ; :: thesis:
then for-down (a,i,n,I) is_halting_on s by A1, A15, A16, A17, A18, Th67;
then A20: ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) halts_on (Initialize s) +* (stop (for-down (a,i,n,I))) by SCMPDS_6:def 3;
A21: for x being Int_position st x in X holds
s . x = s . x ;
then A22: (IExec (I,s)) . (DataLoc ((s . a),i)) = s . (DataLoc ((s . a),i)) by A19;
A23: (IExec (I,s)) . a = s . a by A19, A21;
A24: DataLoc ((s . a),i) = DataLoc (((IExec (I,s)) . a),i) by A19, A21;
A25: (IExec (I,s)) . a = s . a by A19, A21;
A26: Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(0 + 1)) = Following ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I))))) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 3)),((Initialize s) +* (stop (for-down (a,i,n,I))))) by A8, I1, SCMPDS_6:22 ;
not a in dom (Initialize (stop (for-down (a,i,n,I)))) by SCMPDS_4:31;
then ((Initialize s) +* (stop (for-down (a,i,n,I)))) . (DataLoc ((((Initialize s) +* (stop (for-down (a,i,n,I)))) . a),i)) = ((Initialize s) +* (stop (for-down (a,i,n,I)))) . (DataLoc ((s . a),i)) by I1, FUNCT_4:12
.= s . (DataLoc ((s . a),i)) by A3, I1, FUNCT_4:12 ;
then A27: IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)) = succ (IC ((Initialize s) +* (stop (for-down (a,i,n,I))))) by A1, A26, SCMPDS_2:68
.= 0 + 1 by A2 ;
A28: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) by COMPOS_1:138, FUNCT_7:134;

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

end;

then A29: DataPart ((Initialize s) +* (stop I)) = DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)) by SCMPDS_4:23;
A30: I is_halting_on s by A19, A21;
then A31: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
I5: (Initialize ((Initialize s) +* (stop I))) +* (stop I) = ((Initialize s) +* (stop I)) +* (Initialize (stop I)) by COMPOS_1:125;
(Initialize s) +* (stop I) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A4, I5, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop I)) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A31;
then A32: I is_halting_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
A33: I is_closed_on s by A19, A21;
then A34: (IExec ((I ';' (AddTo (a,i,(- n)))),s)) . (DataLoc ((s . a),i)) = (Exec ((AddTo (a,i,(- n))),(IExec (I,s)))) . (DataLoc ((s . a),i)) by A30, Th50
.= ((IExec (I,s)) . (DataLoc ((s . a),i))) + (- n) by A23, SCMPDS_2:60
.= (s . (DataLoc ((s . a),i))) + (- n) by A19, A21 ;
Y: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) = (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) by COMPOS_1:38;
A35: I is_closed_on (Initialize s) +* (stop I) by A33, SCMPDS_6:38;
then A36: IC (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = (card I) + 1 by A17, A4, A32, A27, A29, A11, Th36;
ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)) by AMI_1:123;
then A37: Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)) = Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by EXTPRO_1:5;
then A38: CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) = (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . ((card I) + 1) by A17, A4, A32, A35, A27, A29, A11, Th36, Y
.= (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)) . ((card I) + 1) by AMI_1:54
.= ((Initialize s) +* (stop (for-down (a,i,n,I)))) . ((card I) + 1) by AMI_1:54
.= (for-down (a,i,n,I)) . ((card I) + 1) by A14, A10, GRFUNC_1:8
.= AddTo (a,i,(- n)) by Th62 ;
A39: DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = DataPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by A17, A4, A32, A35, A27, A29, A11, Th36;
then A40: (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . a = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . a by SCMPDS_4:23
.= (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a by A31, EXTPRO_1:23
.= s . a by A25, A6, FUNCT_4:12 ;
A41: (IExec ((I ';' (AddTo (a,i,(- n)))),s)) . a = (Exec ((AddTo (a,i,(- n))),(IExec (I,s)))) . a by A33, A30, Th50
.= s . a by A18, A23, SCMPDS_2:60 ;

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

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

hence for-down (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,(- n)))),s) by Th63; :: thesis:

end;

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

let t be 0 -started State of SCMPDS; :: thesis:
assume that
A43: for x being Int_position st x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,(- n)))),s)) . x and
A44: t . a = (IExec ((I ';' (AddTo (a,i,(- n)))),s)) . a ; :: thesis:

A45: now

let x be Int_position ; :: thesis:
assume A46: x in X ; :: thesis:
hence t . x = (IExec ((I ';' (AddTo (a,i,(- n)))),s)) . x by A43
.= (Exec ((AddTo (a,i,(- n))),(IExec (I,s)))) . x by A33, A30, Th50
.= (IExec (I,s)) . x by A15, A23, A46, SCMPDS_2:60
.= s . x by A19, A21, A46 ;
:: thesis:

end;

hence (IExec (I,t)) . a = t . a by A19, A41, A44; :: thesis:
thus (IExec (I,t)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,(- n)))),s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,(- n)))),s)) . a),i)) by A19, A41, A44, A45; :: thesis:
thus ( 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 ) ) by A19, A41, A44, A45; :: thesis:

end;

hence for-down (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,(- n)))),s) by A15, A16, A17, A18, A41, A42, Th67; :: thesis:

end;

end;

end;

then A47: ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) halts_on (Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))) by SCMPDS_6:def 3;
Y: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))) = (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))) by COMPOS_1:38;
T: ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) by AMI_1:123;
A48: Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)) = Following ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) by EXTPRO_1:4
.= Exec ((AddTo (a,i,(- n))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) by A38, T ;
then A49: IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) = succ (IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) by SCMPDS_2:60
.= ((card I) + 1) + 1 by A36, A37, NAT_1:39
.= (card I) + (1 + 1) ;
then A50: CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))) = ((Initialize s) +* (stop (for-down (a,i,n,I)))) . ((card I) + 2) by Y, AMI_1:54
.= (for-down (a,i,n,I)) . ((card I) + 2) by A10, A12, GRFUNC_1:8
.= goto (- ((card I) + 2)) by Th62 ;
T: ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) by AMI_1:123;
A51: Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1)) = Following ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))) by EXTPRO_1:4
.= Exec ((goto (- ((card I) + 2))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)))) by A50, T ;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1))) = ICplusConst ((Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:66
.= 0 by A49, Th1 ;
then A52: IC ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) = IC (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3))) by SCMPDS_6:21;
A53: (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (DataLoc ((s . a),i)) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (DataLoc ((s . a),i)) by A39, SCMPDS_4:23
.= (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . (DataLoc ((s . a),i)) by A31, EXTPRO_1:23
.= s . (DataLoc ((s . a),i)) by A22, A7, FUNCT_4:12 ;
A54: (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) . (DataLoc ((s . a),i)) by A51, SCMPDS_2:66
.= (s . (DataLoc ((s . a),i))) + (- n) by A40, A53, A37, A48, SCMPDS_2:60 ;

let x be Int_position ; :: thesis:
A55: not x in dom (Initialize (stop (for-down (a,i,n,I)))) by SCMPDS_4:31;
then A56: ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) . x = (IExec ((I ';' (AddTo (a,i,(- n)))),s)) . x by I4, FUNCT_4:12;

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

hence (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1))) . x = ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) . x by A54, A34, A55, I4, FUNCT_4:12; :: thesis:

end;

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

A58: not x in dom (s | NAT) by A5, SCMPDS_2:53;
A59: (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . x = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . x by A39, SCMPDS_4:23
.= (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x by A31, EXTPRO_1:23
.= (IExec (I,s)) . x by A58, FUNCT_4:12 ;
A60: (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) . x = (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . x by A40, A37, A48, A57, SCMPDS_2:60;
(IExec ((I ';' (AddTo (a,i,(- n)))),s)) . x = (Exec ((AddTo (a,i,(- n))),(IExec (I,s)))) . x by A33, A30, Th50
.= (IExec (I,s)) . x by A24, A57, SCMPDS_2:60 ;
hence (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1))) . x = ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) . x by A51, A56, A59, A60, SCMPDS_2:66; :: thesis:

end;

end;

end;

then A61: DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1) + 1))) = DataPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) by SCMPDS_4:23;
TX: ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3))) by AMI_1:123;
ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) = (ProgramPart ((Result ((ProgramPart ((Initialize s) +* (stop (I ';' (AddTo (a,i,(- n))))))),((Initialize s) +* (stop (I ';' (AddTo (a,i,(- n)))))))) +* (ProgramPart s))) +* (ProgramPart (Initialize (stop (for-down (a,i,n,I))))) by I4, FUNCT_4:75
.= (ProgramPart s) +* (ProgramPart (Initialize (stop (for-down (a,i,n,I))))) by A13, FUNCT_4:24
.= ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) by I1, FUNCT_4:75
.= ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3))) by AMI_1:123 ;
then A62: Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3)) = (Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))) by A61, A52, Th7;
then CurInstr ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3)))) = (a,i) <=0_goto ((card I) + 3) by A8, TX, I4, SCMPDS_6:22;
then LifeSpan ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I))))) > (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3 by A20, SCMPDS_6:2, SCMPDS_6:30;
then consider nn being Nat such that
A63: LifeSpan ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I))))) = ((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
T: ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I)))) = ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))) by A62, AMI_1:123;
then Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3) + (LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))))))) = Comput ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))),(LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))))) by A62, EXTPRO_1:5;
then CurInstr ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3) + (LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))))))))) = halt SCMPDS by A47, T, EXTPRO_1:def 14;
then ((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 3) + (LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))))) >= LifeSpan ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I))))) by A20, EXTPRO_1:def 14;
then A64: LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))) >= nn by A63, XREAL_1:8;
A65: Comput ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I))))))) = Comput ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))),nn) by A62, A63, T, EXTPRO_1:5;
then CurInstr ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),(Comput ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))),nn))) = halt SCMPDS by A20, T, EXTPRO_1:def 14;
then nn >= LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))) by A47, EXTPRO_1:def 14;
then nn = LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))) by A64, XXREAL_0:1;
then A66: Result ((ProgramPart ((Initialize s) +* (stop (for-down (a,i,n,I))))),((Initialize s) +* (stop (for-down (a,i,n,I))))) = Comput ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I)))),(LifeSpan ((ProgramPart ((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))),((Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),s))) +* (stop (for-down (a,i,n,I))))))) by A20, A65, EXTPRO_1:23;
(IExec ((I ';' (AddTo (a,i,(- n)))),s)) | NAT = ProgramPart s by A13, FUNCT_4:24;
hence IExec ((for-down (a,i,n,I)),s) = IExec ((for-down (a,i,n,I)),(IExec ((I ';' (AddTo (a,i,(- n)))),s))) by A47, A66, EXTPRO_1:23; :: thesis: