let s be 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 = (Initialize s) +* (stop (for-up a,i,n,I));
set ps = ProgramPart s;
set i1 = a,i >=0_goto ((card I) + 3);
set i2 = AddTo a,i,n;
set i3 = goto (- ((card I) + 2));
I1: s +* (Initialize (stop (for-up a,i,n,I))) = (Initialize s) +* (stop (for-up a,i,n,I)) by SCMPDS_4:5;
assume A1: s . (DataLoc (s . a),i) < 0 ; :: thesis:
set s4 = Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1;
A2: IC ((Initialize s) +* (stop (for-up a,i,n,I))) = 0 by SCMPDS_6:21;
A3: not DataLoc (s . a),i in dom (Initialize (stop (for-up a,i,n,I))) by SCMPDS_4:31;
set m0 = LifeSpan (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I));
set m2 = LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)));
I2: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by SCMPDS_4:5;
I4: (IExec (I ';' (AddTo a,i,n)),s) +* (Initialize (stop (for-up a,i,n,I))) = (Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)) by SCMPDS_4:5;
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-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 (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));
set s5 = Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1);
set s7 = Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1);
A9: Initialize (stop (for-up a,i,n,I)) c= (Initialize s) +* (stop (for-up a,i,n,I)) by I1, FUNCT_4:26;
for-up a,i,n,I c= Initialize (stop (for-up a,i,n,I)) by SCMPDS_6:17;
then A10: for-up a,i,n,I c= (Initialize s) +* (stop (for-up a,i,n,I)) by A9, XBOOLE_1:1;
Shift I,1 c= for-up a,i,n,I by Lm3;
then Shift I,1 c= (Initialize s) +* (stop (for-up a,i,n,I)) by A10, XBOOLE_1:1;
then A11: Shift I,1 c= Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I) by Th52;
set m5 = (((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1) + 1;
set s8 = Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I) by Th52;
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 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-up a,i,n,I is_halting_on s by A1, A15, A16, A17, A18, Th58;
then A20: ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I))) halts_on (Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(0 + 1) = Following (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))) by AMI_1:13
.= Exec (a,i >=0_goto ((card I) + 3)),((Initialize s) +* (stop (for-up a,i,n,I))) by A8, I1, SCMPDS_6:22 ;
not a in dom (Initialize (stop (for-up a,i,n,I))) by SCMPDS_4:31;
then ((Initialize s) +* (stop (for-up a,i,n,I))) . (DataLoc (((Initialize s) +* (stop (for-up a,i,n,I))) . a),i) = ((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1) = succ (IC ((Initialize s) +* (stop (for-up a,i,n,I)))) by A1, A26, SCMPDS_2:69
.= 0 + 1 by A2 ;
A28: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (for-up a,i,n,I))) by FUNCT_7:134, SCMPDS_4:24;

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

end;

then A29: DataPart ((Initialize s) +* (stop I)) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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 SCMPDS_4:5;
(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 ;
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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) = (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) by COMPOS_1:38;
ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1) by AMI_1:123;
then A37: Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) = Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by AMI_1:51;
then A38: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1) . ((card I) + 1) by AMI_1:54
.= ((Initialize s) +* (stop (for-up a,i,n,I))) . ((card I) + 1) by AMI_1:54
.= (for-up a,i,n,I) . ((card I) + 1) by A14, A10, GRFUNC_1:8
.= AddTo a,i,n by Th53 ;
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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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, AMI_1:122
.= 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-up a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,n)),s by Th54; :: 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 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-up a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,n)),s by A15, A16, A17, A18, A41, A42, Th58; :: thesis:

end;

end;

end;

then A47: ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))) halts_on (Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)) by SCMPDS_6:def 3;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1))) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1))) = (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1) = Following (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:14
.= Exec (AddTo a,i,n),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) = succ (IC (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) = ((Initialize s) +* (stop (for-up a,i,n,I))) . ((card I) + 2) by Y, AMI_1:54
.= (for-up a,i,n,I) . ((card I) + 2) by A10, A12, GRFUNC_1:8
.= goto (- ((card I) + 2)) by Th53 ;
T: ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1) + 1) = Following (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 2))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1) + 1)) = ICplusConst (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I))) = IC (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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, AMI_1:122
.= s . (DataLoc (s . a),i) by A22, A7, FUNCT_4:12 ;
A54: (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I))) by SCMPDS_4:31;
then A56: ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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, AMI_1:122
.= (IExec I,s) . x by A58, FUNCT_4:12 ;
A60: (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I))) by SCMPDS_4:23;
TX1: ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up 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-up a,i,n,I)))) by I4, FUNCT_4:75
.= (ProgramPart s) +* (ProgramPart (Initialize (stop (for-up a,i,n,I)))) by A13, FUNCT_4:24
.= ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I))) by I1, FUNCT_4:75
.= ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)) by A61, A52, Th7;
then CurInstr (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 3)) = a,i >=0_goto ((card I) + 3) by A8, TX1, I4, SCMPDS_6:22;
then LifeSpan (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))) > (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 3 by A20, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A63: LifeSpan (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I))) = ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))) by A62, AMI_1:123;
then Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))))) = Comput (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))),(LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))) by A62, AMI_1:51;
then CurInstr (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up 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-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))))) = halt SCMPDS by A47, T, AMI_1:def 46;
then ((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 3) + (LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))) >= LifeSpan (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))) by A20, AMI_1:def 46;
then A64: LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))) >= nn by A63, XREAL_1:8;
A65: Comput (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))),(LifeSpan (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I)))) = Comput (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))),nn by A62, A63, T, AMI_1:51;
then CurInstr (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),(Comput (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))),nn) = halt SCMPDS by A20, T, AMI_1:def 46;
then nn >= LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))) by A47, AMI_1:def 46;
then nn = LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))) by A64, XXREAL_0:1;
then A66: Result (ProgramPart ((Initialize s) +* (stop (for-up a,i,n,I)))),((Initialize s) +* (stop (for-up a,i,n,I))) = Comput (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I))),(LifeSpan (ProgramPart ((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))),((Initialize (IExec (I ';' (AddTo a,i,n)),s)) +* (stop (for-up a,i,n,I)))) by A20, A65, AMI_1:122;
(IExec (I ';' (AddTo a,i,n)),s) | NAT = ProgramPart s by A13, FUNCT_4:24;
hence IExec (for-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) by A47, A66, AMI_1:122; :: thesis: