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));
A1: s +* (Initialize (stop (for-up (a,i,n,I)))) = (Initialize s) +* (stop (for-up (a,i,n,I))) by COMPOS_1:125;
assume A2: 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);
A3: IC ((Initialize s) +* (stop (for-up (a,i,n,I)))) = 0 by SCMPDS_6:21;
A4: 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)))));
A5: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
A6: (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 COMPOS_1:125;
set Es = IExec ((I ';' (AddTo (a,i,n))),s);
set bj = DataLoc (((IExec ((I ';' (AddTo (a,i,n))),s)) . a),i);
A7: Initialize (stop I) c= (Initialize s) +* (stop I) by A5, 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-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));
A12: Initialize (stop (for-up (a,i,n,I))) c= (Initialize s) +* (stop (for-up (a,i,n,I))) by A1, FUNCT_4:26;
for-up (a,i,n,I) c= Initialize (stop (for-up (a,i,n,I))) by SCMPDS_6:17;
then A13: for-up (a,i,n,I) c= (Initialize s) +* (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 Shift (I,1) c= (Initialize s) +* (stop (for-up (a,i,n,I))) by A13, XBOOLE_1:1;
then A14: 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 A15: (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));
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-up (a,i,n,I)) by Th52;
assume A18: not DataLoc ((s . a),i) in X ; :: thesis:
assume A19: n > 0 ; :: thesis:
assume A20: card I > 0 ; :: thesis:
assume A21: a <> DataLoc ((s . a),i) ; :: thesis:
assume A22: 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 A2, A18, A19, A20, A21, Th58;
then A23: 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;
A24: for x being Int_position st x in X holds
s . x = s . x ;
then A25: (IExec (I,s)) . (DataLoc ((s . a),i)) = s . (DataLoc ((s . a),i)) by A22;
A26: (IExec (I,s)) . a = s . a by A22, A24;
A27: DataLoc ((s . a),i) = DataLoc (((IExec (I,s)) . a),i) by A22, A24;
A28: (IExec (I,s)) . a = s . a by A22, A24;
A29: 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 EXTPRO_1:4
.= Following ((ProgramPart ((Initialize s) +* (stop (for-up (a,i,n,I))))),((Initialize s) +* (stop (for-up (a,i,n,I))))) by EXTPRO_1:3
.= Exec (((a,i) >=0_goto ((card I) + 3)),((Initialize s) +* (stop (for-up (a,i,n,I))))) by A11, A1, 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 A1, FUNCT_4:12
.= s . (DataLoc ((s . a),i)) by A4, A1, FUNCT_4:12 ;
then A30: 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 A2, A29, SCMPDS_2:69
.= 0 + 1 by A3 ;
A31: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (for-up (a,i,n,I)))) by COMPOS_1:138, FUNCT_7:134;

now

let a be Int_position ; :: thesis:
thus ((Initialize s) +* (stop I)) . a = ((Initialize s) +* (stop (for-up (a,i,n,I)))) . a by A31, 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 A29, SCMPDS_2:69 ; :: thesis:

end;

now

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 A47: (IExec ((I ';' (AddTo (a,i,n))),s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),s)) . a),i)) < 0 ; :: thesis:

now

let t be State of SCMPDS; :: thesis:
assume that
A48: for x being Int_position st x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,n))),s)) . x and
A49: t . a = (IExec ((I ';' (AddTo (a,i,n))),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))),s)) . x by A48
.= (Exec ((AddTo (a,i,n)),(IExec (I,s)))) . x by A37, A33, Th50
.= (IExec (I,s)) . x by A18, A26, A51, SCMPDS_2:60
.= s . x by A22, A24, A51 ;
:: thesis:

end;

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

end;

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

end;

now

let x be Int_position ; :: thesis:
A63: not x in dom (Initialize (stop (for-up (a,i,n,I)))) by SCMPDS_4:31;
then A64: ((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 A6, FUNCT_4:12;

per cases ;

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 A62, A38, A63, A6, FUNCT_4:12; :: thesis:

end;

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

end;