let s be State of SCMPDS ; :: thesis: for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for i being Integer
for n being Element of NAT
for X being set st s . (DataLoc (s . a),i) > 0 & not DataLoc (s . a),i in X & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( 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 ) ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let I be shiftable No-StopCode Program of SCMPDS ; :: thesis: for a being Int_position
for i being Integer
for n being Element of NAT
for X being set st s . (DataLoc (s . a),i) > 0 & not DataLoc (s . a),i in X & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( 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 ) ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT
for X being set st s . (DataLoc (s . a),i) > 0 & not DataLoc (s . a),i in X & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( 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 ) ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let i be Integer; :: thesis: for n being Element of NAT
for X being set st s . (DataLoc (s . a),i) > 0 & not DataLoc (s . a),i in X & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( 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 ) ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let n be Element of NAT ; :: thesis: for X being set st s . (DataLoc (s . a),i) > 0 & not DataLoc (s . a),i in X & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( 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 ) ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let X be set ; :: thesis: ( s . (DataLoc (s . a),i) > 0 & not DataLoc (s . a),i in X & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( 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 ) ) ) implies IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
set b = DataLoc (s . a),i;
set FOR = for-down a,i,n,I;
set iFOR = Initialized (stop (for-down a,i,n,I));
set iI = Initialized (stop I);
set s1 = s +* (Initialized (stop (for-down a,i,n,I)));
set ps = s | NAT ;
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: ( DataLoc (s . a),i in X or not n > 0 or not card I > 0 or not a <> DataLoc (s . a),i or ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & not ( (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 ) ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
set s4 = Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1;
A2: IC (s +* (Initialized (stop (for-down a,i,n,I)))) = 0 by SCMPDS_6:21;
A3: not DataLoc (s . a),i in dom (Initialized (stop (for-down a,i,n,I))) by SCMPDS_4:31;
set m0 = LifeSpan (s +* (Initialized (stop (for-down a,i,n,I))));
set l2 = (card I) + 2;
set sI = s +* (Initialized (stop I));
set m1 = (LifeSpan (s +* (Initialized (stop I)))) + 3;
set J = I ';' (AddTo a,i,(- n));
set sJ = s +* (Initialized (stop (I ';' (AddTo a,i,(- n)))));
set s2 = (IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)));
set m2 = LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))));
set Es = IExec (I ';' (AddTo a,i,(- n))),s;
set bj = DataLoc ((IExec (I ';' (AddTo a,i,(- n))),s) . a),i;
A4: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A5: dom (s | NAT ) = NAT by SCMPDS_6:1;
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 (s +* (Initialized (stop I)));
set s5 = Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))));
set l1 = (card I) + 1;
set m3 = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set s6 = Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1);
set s7 = Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1);
A9: Initialized (stop (for-down a,i,n,I)) c= s +* (Initialized (stop (for-down a,i,n,I))) by FUNCT_4:26;
for-down a,i,n,I c= Initialized (stop (for-down a,i,n,I)) by SCMPDS_6:17;
then A10: for-down a,i,n,I c= s +* (Initialized (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= s +* (Initialized (stop (for-down a,i,n,I))) by A10, XBOOLE_1:1;
then A11: Shift I,1 c= Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (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 (s +* (Initialized (stop I)))) + 1) + 1) + 1;
set s8 = Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1);
A13: dom (s | NAT ) = (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: ( not n > 0 or not card I > 0 or not a <> DataLoc (s . a),i or ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & not ( (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 ) ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
assume A16: n > 0 ; :: thesis: ( not card I > 0 or not a <> DataLoc (s . a),i or ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & not ( (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 ) ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
assume A17: card I > 0 ; :: thesis: ( not a <> DataLoc (s . a),i or ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & not ( (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 ) ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
assume A18: a <> DataLoc (s . a),i ; :: thesis: ( ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & not ( (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 ) ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
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: IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
then for-down a,i,n,I is_halting_on s by A1, A15, A16, A17, A18, Th67;
then A20: ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) halts_on s +* (Initialized (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 (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(0 + 1) = Following (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))) by AMI_1:13
.= Exec (a,i <=0_goto ((card I) + 3)),(s +* (Initialized (stop (for-down a,i,n,I)))) by A8, SCMPDS_6:22 ;
not a in dom (Initialized (stop (for-down a,i,n,I))) by SCMPDS_4:31;
then (s +* (Initialized (stop (for-down a,i,n,I)))) . (DataLoc ((s +* (Initialized (stop (for-down a,i,n,I)))) . a),i) = (s +* (Initialized (stop (for-down a,i,n,I)))) . (DataLoc (s . a),i) by FUNCT_4:12
.= s . (DataLoc (s . a),i) by A3, FUNCT_4:12 ;
then A27: IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) = succ (IC (s +* (Initialized (stop (for-down a,i,n,I))))) by A1, A26, SCMPDS_2:68
.= 0 + 1 by A2 ;
A28: DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (for-down a,i,n,I)))) by SCMPDS_4:24, SCMPDS_4:36;
now
let a be Int_position ; :: thesis: (s +* (Initialized (stop I))) . a = (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) . a
thus (s +* (Initialized (stop I))) . a = (s +* (Initialized (stop (for-down a,i,n,I)))) . a by A28, SCMPDS_4:23
.= (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) . a by A26, SCMPDS_2:68 ; :: thesis: verum
end;
then A29: DataPart (s +* (Initialized (stop I))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) by SCMPDS_4:23;
A30: I is_halting_on s by A19, A21;
then A31: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
s +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A4, FUNCT_4:79;
then ProgramPart ((s +* (Initialized (stop I))) +* (Initialized (stop I))) halts_on (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A31;
then A32: I is_halting_on s +* (Initialized (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 (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) = (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) by AMI_1:150;
A35: I is_closed_on s +* (Initialized (stop I)) by A33, SCMPDS_6:38;
then A36: IC (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = (card I) + 1 by A17, A4, A32, A27, A29, A11, Th36;
ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) by AMI_1:144;
then A37: Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:51;
then A38: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . ((card I) + 1) by A17, A4, A32, A35, A27, A29, A11, Th36, Y
.= (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1) . ((card I) + 1) by AMI_1:54
.= (s +* (Initialized (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 (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) by A17, A4, A32, A35, A27, A29, A11, Th36;
then A40: (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . a = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by SCMPDS_4:23
.= (Result (s +* (Initialized (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 ;
now
per cases ( (IExec (I ';' (AddTo a,i,(- n))),s) . (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: for-down a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,(- n))),s
hence for-down a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,(- n))),s by Th63; :: thesis: verum
end;
suppose A42: (IExec (I ';' (AddTo a,i,(- n))),s) . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),s) . a),i) > 0 ; :: thesis: for-down a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,(- n))),s
now
let t be State of SCMPDS ; :: thesis: ( ( for x being Int_position st x in X holds
t . x = (IExec (I ';' (AddTo a,i,(- n))),s) . x ) & t . a = (IExec (I ';' (AddTo a,i,(- n))),s) . a implies ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),s) . a),i) = t . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),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 ) ) )
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: ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),s) . a),i) = t . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),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 ) )
A45: now
let x be Int_position ; :: thesis: ( x in X implies t . x = s . x )
assume A46: x in X ; :: thesis: t . x = s . x
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: verum
end;
hence (IExec I,t) . a = t . a by A19, A41, A44; :: thesis: ( (IExec I,t) . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),s) . a),i) = t . (DataLoc ((IExec (I ';' (AddTo a,i,(- n))),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 ) )
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: ( 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 ) )
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: verum
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: verum
end;
end;
end;
then A47: ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) halts_on (IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))) by SCMPDS_6:def 3;
Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1))) = (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1))) by AMI_1:150;
T: ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:144;
A48: Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) = Following (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:14
.= Exec (AddTo a,i,(- n)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A38, T ;
then A49: IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = succ (IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = (s +* (Initialized (stop (for-down a,i,n,I)))) . ((card I) + 2) by AMI_1:54, Y
.= (for-down a,i,n,I) . ((card I) + 2) by A10, A12, GRFUNC_1:8
.= goto (- ((card I) + 2)) by Th62 ;
T: ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) by AMI_1:144;
A51: Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1) = Following (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 2))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) by A50, T ;
then IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) = ICplusConst (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)),(0 - ((card I) + 2)) by SCMPDS_2:66
.= 0 by A49, Th1 ;
then A52: IC ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) = IC (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3)) by SCMPDS_6:21;
A53: (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . (DataLoc (s . a),i) = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . (DataLoc (s . a),i) by A39, SCMPDS_4:23
.= (Result (s +* (Initialized (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 (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . (DataLoc (s . a),i) = (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (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 ;
now
let x be Int_position ; :: thesis: (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . b1 = ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) . b1
A55: not x in dom (Initialized (stop (for-down a,i,n,I))) by SCMPDS_4:31;
then A56: ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) . x = (IExec (I ';' (AddTo a,i,(- n))),s) . x by FUNCT_4:12;
per cases ( x = DataLoc (s . a),i or x <> DataLoc (s . a),i ) ;
suppose x = DataLoc (s . a),i ; :: thesis: (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . b1 = ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) . b1
hence (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . x = ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) . x by A54, A34, A55, FUNCT_4:12; :: thesis: verum
end;
suppose A57: x <> DataLoc (s . a),i ; :: thesis: (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . b1 = ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) . b1
A58: not x in dom (s | NAT ) by A5, SCMPDS_2:53;
A59: (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . x = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . x by A39, SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . x by A31, AMI_1:122
.= (IExec I,s) . x by A58, FUNCT_4:12 ;
A60: (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . x = (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),1),(LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . x = ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) . x by A51, A56, A59, A60, SCMPDS_2:66; :: thesis: verum
end;
end;
end;
then A61: DataPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) = DataPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) by SCMPDS_4:23;
((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) | NAT = (((Result (s +* (Initialized (stop (I ';' (AddTo a,i,(- n))))))) +* (s | NAT )) | NAT ) +* ((Initialized (stop (for-down a,i,n,I))) | NAT ) by FUNCT_4:75
.= (s | NAT ) +* ((Initialized (stop (for-down a,i,n,I))) | NAT ) by A13, FUNCT_4:24
.= (s +* (Initialized (stop (for-down a,i,n,I)))) | NAT by FUNCT_4:75
.= (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3)) | NAT by Th6 ;
then A62: Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3) = (IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))) by A61, A52, Th7;
then CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3)) = a,i <=0_goto ((card I) + 3) by A8, SCMPDS_6:22;
then LifeSpan (s +* (Initialized (stop (for-down a,i,n,I)))) > (LifeSpan (s +* (Initialized (stop I)))) + 3 by A20, SCMPDS_6:2, SCMPDS_6:30;
then consider nn being Nat such that
A63: LifeSpan (s +* (Initialized (stop (for-down a,i,n,I)))) = ((LifeSpan (s +* (Initialized (stop I)))) + 3) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
T: ProgramPart (s +* (Initialized (stop (for-down a,i,n,I)))) = ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) by A62, AMI_1:144;
then Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))))) = Comput (ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))),((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))),(LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))) by A62, AMI_1:51;
then CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))))))),(Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))))) = halt SCMPDS by A47, AMI_1:def 46;
then ((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))) >= LifeSpan (s +* (Initialized (stop (for-down a,i,n,I)))) by A20, AMI_1:def 46;
then A64: LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) >= nn by A63, XREAL_1:8;
A65: Comput (ProgramPart (s +* (Initialized (stop (for-down a,i,n,I))))),(s +* (Initialized (stop (for-down a,i,n,I)))),(LifeSpan (s +* (Initialized (stop (for-down a,i,n,I))))) = Comput (ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))),((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))),nn by A62, A63, AMI_1:51, T;
then CurInstr (ProgramPart (Comput (ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))),((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))),nn)),(Comput (ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))),((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))),nn) = halt SCMPDS by A20, AMI_1:def 46;
then nn >= LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) by A47, AMI_1:def 46;
then nn = LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))) by A64, XXREAL_0:1;
then A66: Result (s +* (Initialized (stop (for-down a,i,n,I)))) = Comput (ProgramPart ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))),((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I)))),(LifeSpan ((IExec (I ';' (AddTo a,i,(- n))),s) +* (Initialized (stop (for-down a,i,n,I))))) by A20, A65, AMI_1:122;
(IExec (I ';' (AddTo a,i,(- n))),s) | NAT = s | NAT 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, AMI_1:122; :: thesis: verum