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-up a,i,n,I),s = IExec (for-up 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-up a,i,n,I),s = IExec (for-up 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-up a,i,n,I),s = IExec (for-up 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-up a,i,n,I),s = IExec (for-up 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-up a,i,n,I),s = IExec (for-up 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) )
set b = DataLoc (s . a),i;
set FOR = for-up a,i,n,I;
set iFOR = Initialized (stop (for-up a,i,n,I));
set iI = Initialized (stop I);
set s1 = s +* (Initialized (stop (for-up 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) )
assume A2: 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) )
assume A3: 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) )
assume A4: 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) )
assume A5: 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s) )
assume A6: 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-up a,i,n,I),s = IExec (for-up a,i,n,I),(IExec (I ';' (AddTo a,i,n)),s)
then for-up a,i,n,I is_halting_on s by A1, A2, A3, A4, A5, Th58;
then A7: s +* (Initialized (stop (for-up a,i,n,I))) is halting by SCMPDS_6:def 3;
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-up a,i,n,I)));
set m2 = LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up 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;
A8: ( ( for x being Int_position st x in X holds
s . x = s . x ) & s . a = s . a ) ;
then A9: ( I is_closed_on s & I is_halting_on s ) by A6;
A10: (IExec I,s) . a = s . a by A6, A8;
A11: (IExec (I ';' (AddTo a,i,n)),s) . a = (Exec (AddTo a,i,n),(IExec I,s)) . a by A9, Th50
.= s . a by A5, A10, SCMPDS_2:60 ;
A12: 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-up a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,n)),s
hence for-up a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,n)),s by Th54; :: thesis: verum
end;
suppose A13: (IExec (I ';' (AddTo a,i,n)),s) . (DataLoc ((IExec (I ';' (AddTo a,i,n)),s) . a),i) < 0 ; :: thesis: for-up 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 A14: ( ( 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 ) ; :: 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 ) )
A15: now
let x be Int_position ; :: thesis: ( x in X implies t . x = s . x )
assume A16: x in X ; :: thesis: t . x = s . x
hence t . x = (IExec (I ';' (AddTo a,i,n)),s) . x by A14
.= (Exec (AddTo a,i,n),(IExec I,s)) . x by A9, Th50
.= (IExec I,s) . x by A2, A10, A16, SCMPDS_2:60
.= s . x by A6, A8, A16 ;
:: thesis: verum
end;
hence (IExec I,t) . a = t . a by A6, A11, A14; :: 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 A6, A11, A14, A15; :: 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 A6, A11, A14, A15; :: thesis: verum
end;
hence for-up a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,n)),s by A2, A3, A4, A5, A11, A13, Th58; :: thesis: verum
end;
end;
end;
set s4 = Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1;
A17: ( (IExec I,s) . a = s . a & (IExec I,s) . (DataLoc (s . a),i) = s . (DataLoc (s . a),i) ) by A6, A8;
A18: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A19: s +* (Initialized (stop I)) is halting by A9, SCMPDS_6:def 3;
then (s +* (Initialized (stop I))) +* (Initialized (stop I)) is halting by A18, FUNCT_4:79;
then A20: I is_halting_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
A21: I is_closed_on s +* (Initialized (stop I)) by A9, SCMPDS_6:38;
A22: IC (s +* (Initialized (stop (for-up a,i,n,I)))) = inspos 0 by SCMPDS_6:21;
A23: for-up a,i,n,I = (a,i >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo a,i,n)) ';' (goto (- ((card I) + 2)))) by Th15;
A24: Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(0 + 1) = Following (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),0 ) by AMI_1:14
.= Following (s +* (Initialized (stop (for-up a,i,n,I)))) by AMI_1:13
.= Exec (a,i >=0_goto ((card I) + 3)),(s +* (Initialized (stop (for-up a,i,n,I)))) by A23, SCMPDS_6:22 ;
A25: ( not a in dom (Initialized (stop (for-up a,i,n,I))) & a in dom s ) by SCMPDS_2:49, SCMPDS_4:31;
A26: ( not DataLoc (s . a),i in dom (Initialized (stop (for-up a,i,n,I))) & DataLoc (s . a),i in dom s ) by SCMPDS_2:49, SCMPDS_4:31;
(s +* (Initialized (stop (for-up a,i,n,I)))) . (DataLoc ((s +* (Initialized (stop (for-up a,i,n,I)))) . a),i) = (s +* (Initialized (stop (for-up a,i,n,I)))) . (DataLoc (s . a),i) by A25, FUNCT_4:12
.= s . (DataLoc (s . a),i) by A26, FUNCT_4:12 ;
then A27: IC (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1) = Next (IC (s +* (Initialized (stop (for-up a,i,n,I))))) by A1, A24, SCMPDS_2:69
.= inspos (0 + 1) by A22 ;
A28: DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (for-up a,i,n,I)))) by SCMPDS_4:24, SCMPDS_4:36;
now
let a be Int_position ; :: thesis: (s +* (Initialized (stop I))) . a = (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1) . a
thus (s +* (Initialized (stop I))) . a = (s +* (Initialized (stop (for-up a,i,n,I)))) . a by A28, SCMPDS_4:23
.= (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1) . a by A24, SCMPDS_2:69 ; :: thesis: verum
end;
then A29: DataPart (s +* (Initialized (stop I))) = DataPart (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1) by SCMPDS_4:23;
set mI = LifeSpan (s +* (Initialized (stop I)));
set s5 = Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))));
set l1 = inspos ((card I) + 1);
A30: dom (s | NAT ) = NAT by SCMPDS_6:1;
A31: now
assume a in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = a as Instruction-Location of SCMPDS by A30, AMI_1:def 4;
l = a ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
A32: now
assume DataLoc (s . a),i in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = DataLoc (s . a),i as Instruction-Location of SCMPDS by A30, AMI_1:def 4;
l = DataLoc (s . a),i ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
(card I) + 1 < (card I) + 3 by XREAL_1:8;
then A33: inspos ((card I) + 1) in dom (for-up a,i,n,I) by Th52;
A34: for-up a,i,n,I c= Initialized (stop (for-up a,i,n,I)) by SCMPDS_6:17;
Initialized (stop (for-up a,i,n,I)) c= s +* (Initialized (stop (for-up a,i,n,I))) by FUNCT_4:26;
then A35: for-up a,i,n,I c= s +* (Initialized (stop (for-up a,i,n,I))) by A34, XBOOLE_1:1;
Shift I,1 c= for-up a,i,n,I by Lm3;
then Shift I,1 c= s +* (Initialized (stop (for-up a,i,n,I))) by A35, XBOOLE_1:1;
then A36: Shift I,1 c= Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1 by AMI_1:81;
then A37: DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) by A4, A18, A20, A21, A27, A29, Th36;
then A38: (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . a by A19, AMI_1:122
.= s . a by A17, A31, FUNCT_4:12 ;
A39: (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . (DataLoc (s . a),i) = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . (DataLoc (s . a),i) by A37, SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . (DataLoc (s . a),i) by A19, AMI_1:122
.= s . (DataLoc (s . a),i) by A17, A32, FUNCT_4:12 ;
set m3 = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set s6 = Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1);
A40: IC (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = inspos ((card I) + 1) by A4, A18, A20, A21, A27, A29, A36, Th36;
A41: Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:51;
then A42: CurInstr (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . (inspos ((card I) + 1)) by A4, A18, A20, A21, A27, A29, A36, Th36
.= (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1) . (inspos ((card I) + 1)) by AMI_1:54
.= (s +* (Initialized (stop (for-up a,i,n,I)))) . (inspos ((card I) + 1)) by AMI_1:54
.= (for-up a,i,n,I) . (inspos ((card I) + 1)) by A33, A35, GRFUNC_1:8
.= AddTo a,i,n by Th53 ;
set s7 = Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1);
A43: Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) = Following (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:14
.= Exec (AddTo a,i,n),(Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A42 ;
then A44: IC (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = Next (IC (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) by SCMPDS_2:60
.= inspos (((card I) + 1) + 1) by A40, A41, NAT_1:39
.= inspos ((card I) + (1 + 1)) ;
set l2 = inspos ((card I) + 2);
(card I) + 2 < (card I) + 3 by XREAL_1:8;
then A45: inspos ((card I) + 2) in dom (for-up a,i,n,I) by Th52;
A46: CurInstr (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = (s +* (Initialized (stop (for-up a,i,n,I)))) . (inspos ((card I) + 2)) by A44, AMI_1:54
.= (for-up a,i,n,I) . (inspos ((card I) + 2)) by A35, A45, GRFUNC_1:8
.= goto (- ((card I) + 2)) by Th53 ;
set m5 = (((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1;
set s8 = Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1);
A47: Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1) = Following (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 2))),(Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) by A46 ;
then A48: IC (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) = ICplusConst (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)),(0 - ((card I) + 2)) by SCMPDS_2:66
.= inspos 0 by A44, Th1 ;
A49: (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . (DataLoc (s . a),i) = (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . (DataLoc (s . a),i) by A47, SCMPDS_2:66
.= (s . (DataLoc (s . a),i)) + n by A38, A39, A41, A43, SCMPDS_2:60 ;
A50: DataLoc (s . a),i = DataLoc ((IExec I,s) . a),i by A6, A8;
A51: (IExec (I ';' (AddTo a,i,n)),s) . (DataLoc (s . a),i) = (Exec (AddTo a,i,n),(IExec I,s)) . (DataLoc (s . a),i) by A9, Th50
.= ((IExec I,s) . (DataLoc (s . a),i)) + n by A10, SCMPDS_2:60
.= (s . (DataLoc (s . a),i)) + n by A6, A8 ;
now
let x be Int_position ; :: thesis: (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . b1 = ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) . b1
A52: ( not x in dom (Initialized (stop (for-up a,i,n,I))) & x in dom (IExec (I ';' (AddTo a,i,n)),s) ) by SCMPDS_2:49, SCMPDS_4:31;
then A53: ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up 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: (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . b1 = ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) . b1
hence (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . x = ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) . x by A49, A51, A52, FUNCT_4:12; :: thesis: verum
end;
suppose A54: x <> DataLoc (s . a),i ; :: thesis: (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . b1 = ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) . b1
A55: now
assume x in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of SCMPDS by A30, AMI_1:def 4;
l = x ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
A56: (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . x = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . x by A37, SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . x by A19, AMI_1:122
.= (IExec I,s) . x by A55, FUNCT_4:12 ;
A57: (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . x = (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . x by A38, A41, A43, A54, SCMPDS_2:60;
(IExec (I ';' (AddTo a,i,n)),s) . x = (Exec (AddTo a,i,n),(IExec I,s)) . x by A9, Th50
.= (IExec I,s) . x by A50, A54, SCMPDS_2:60 ;
hence (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) . x = ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) . x by A47, A53, A56, A57, SCMPDS_2:66; :: thesis: verum
end;
end;
end;
then A58: DataPart (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) + 1)) = DataPart ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) by SCMPDS_4:23;
A59: IC ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) = IC (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3)) by A48, SCMPDS_6:21;
A60: (IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))) is halting by A12, SCMPDS_6:def 3;
A61: 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 ;
((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) | NAT = (((Result (s +* (Initialized (stop (I ';' (AddTo a,i,n)))))) +* (s | NAT )) | NAT ) +* ((Initialized (stop (for-up a,i,n,I))) | NAT ) by FUNCT_4:75
.= (s | NAT ) +* ((Initialized (stop (for-up a,i,n,I))) | NAT ) by A61, FUNCT_4:24
.= (s +* (Initialized (stop (for-up a,i,n,I)))) | NAT by FUNCT_4:75
.= (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3)) | NAT by Th6 ;
then A62: Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3) = (IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))) by A58, A59, Th7;
then A63: CurInstr (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 3)) = a,i >=0_goto ((card I) + 3) by A23, SCMPDS_6:22;
set m0 = LifeSpan (s +* (Initialized (stop (for-up a,i,n,I))));
LifeSpan (s +* (Initialized (stop (for-up a,i,n,I)))) > (LifeSpan (s +* (Initialized (stop I)))) + 3 by A7, A63, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A64: LifeSpan (s +* (Initialized (stop (for-up 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;
A65: Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(LifeSpan (s +* (Initialized (stop (for-up a,i,n,I))))) = Computation ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))),nn by A62, A64, AMI_1:51;
then CurInstr (Computation ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))),nn) = halt SCMPDS by A7, AMI_1:def 46;
then A66: nn >= LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) by A60, AMI_1:def 46;
Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))))) = Computation ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))),(LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))))) by A62, AMI_1:51;
then CurInstr (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))))))) = halt SCMPDS by A60, AMI_1:def 46;
then ((LifeSpan (s +* (Initialized (stop I)))) + 3) + (LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))))) >= LifeSpan (s +* (Initialized (stop (for-up a,i,n,I)))) by A7, AMI_1:def 46;
then LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) >= nn by A64, XREAL_1:8;
then nn = LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) by A66, XXREAL_0:1;
then A67: Result (s +* (Initialized (stop (for-up a,i,n,I)))) = Computation ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))),(LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))))) by A7, A65, AMI_1:122;
(IExec (I ';' (AddTo a,i,n)),s) | NAT = s | NAT by A61, 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 A60, A67, AMI_1:122; :: thesis: verum