let s be State of ; :: thesis: for I being shiftable No-StopCode Program of
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 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 ; :: 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 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 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 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 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 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 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) )
set s4 = Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1;
A2: IC (s +* (Initialized (stop (for-up a,i,n,I)))) = inspos 0 by SCMPDS_6:21;
A3: not DataLoc (s . a),i in dom (Initialized (stop (for-up a,i,n,I))) by SCMPDS_4:31;
set m0 = LifeSpan (s +* (Initialized (stop (for-up a,i,n,I))));
set l2 = inspos ((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-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;
A4: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A5: dom (s | NAT ) = NAT by SCMPDS_6:1;
A6: now
assume a in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = a as Instruction-Location of SCMPDS by A5, AMI_1:def 4;
l = a ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
A7: 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 A5, AMI_1:def 4;
l = DataLoc (s . a),i ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
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 (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);
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);
set s7 = Computation (s +* (Initialized (stop (for-up a,i,n,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1);
A9: Initialized (stop (for-up a,i,n,I)) c= s +* (Initialized (stop (for-up a,i,n,I))) by FUNCT_4:26;
for-up a,i,n,I c= Initialized (stop (for-up a,i,n,I)) by SCMPDS_6:17;
then A10: for-up a,i,n,I c= s +* (Initialized (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= s +* (Initialized (stop (for-up a,i,n,I))) by A10, XBOOLE_1:1;
then A11: Shift I,1 c= Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1 by AMI_1:81;
(card I) + 2 < (card I) + 3 by XREAL_1:8;
then A12: inspos ((card I) + 2) in dom (for-up a,i,n,I) by Th52;
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);
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: inspos ((card I) + 1) in dom (for-up a,i,n,I) by Th52;
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 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 A16: n > 0 ; :: thesis: ( not card I > 0 or not a <> DataLoc (s . a),i or ex t being State of 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 A17: card I > 0 ; :: thesis: ( not a <> DataLoc (s . a),i or ex t being State of 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 A18: a <> DataLoc (s . a),i ; :: thesis: ( ex t being State of 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 A19: for t being State of 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, A15, A16, A17, A18, Th58;
then A20: ProgramPart (s +* (Initialized (stop (for-up a,i,n,I)))) halts_on s +* (Initialized (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: 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 A8, SCMPDS_6:22 ;
not a in dom (Initialized (stop (for-up a,i,n,I))) by SCMPDS_4:31;
then (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 FUNCT_4:12
.= s . (DataLoc (s . a),i) by A3, 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, A26, SCMPDS_2:69
.= inspos (0 + 1) by A2 ;
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 A26, 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;
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 A4, FUNCT_4:79, 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 ;
A35: I is_closed_on s +* (Initialized (stop I)) by A33, SCMPDS_6:38;
then A36: IC (Computation (Computation (s +* (Initialized (stop (for-up a,i,n,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = inspos ((card I) + 1) by A17, A4, A32, A27, A29, A11, Th36;
A37: 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 A38: 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 A17, A4, A32, A35, A27, A29, A11, 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 A14, A10, GRFUNC_1:8
.= AddTo a,i,n by Th53 ;
A39: 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 A17, A4, A32, A35, A27, A29, A11, Th36;
then A40: (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 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-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 A42: (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 ; :: 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-up a,i,n,I is_halting_on IExec (I ';' (AddTo a,i,n)),s by A15, A16, A17, A18, A41, A42, Th58; :: thesis: verum
end;
end;
end;
then A47: ProgramPart ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) halts_on (IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I))) by SCMPDS_6:def 3;
A48: 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 A38 ;
then A49: 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 A36, A37, NAT_1:39
.= inspos ((card I) + (1 + 1)) ;
then A50: 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 AMI_1:54
.= (for-up a,i,n,I) . (inspos ((card I) + 2)) by A10, A12, GRFUNC_1:8
.= goto (- ((card I) + 2)) by Th53 ;
A51: 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 A50 ;
then 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 A49, Th1 ;
then A52: 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 SCMPDS_6:21;
A53: (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 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: (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 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: (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: not x in dom (Initialized (stop (for-up a,i,n,I))) by SCMPDS_4:31;
then A56: ((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 A54, A34, A55, FUNCT_4:12; :: thesis: verum
end;
suppose A57: 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
A58: now
assume x in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of SCMPDS by A5, AMI_1:def 4;
l = x ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
A59: (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 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: (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 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 (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 A51, A56, A59, A60, SCMPDS_2:66; :: thesis: verum
end;
end;
end;
then A61: 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;
((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 A13, 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 A61, A52, Th7;
then 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 A8, SCMPDS_6:22;
then LifeSpan (s +* (Initialized (stop (for-up a,i,n,I)))) > (LifeSpan (s +* (Initialized (stop I)))) + 3 by A20, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A63: 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;
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 A47, 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 A20, AMI_1:def 46;
then A64: LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) >= nn by A63, XREAL_1:8;
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, A63, 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 A20, AMI_1:def 46;
then nn >= LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) by A47, AMI_1:def 46;
then nn = LifeSpan ((IExec (I ';' (AddTo a,i,n)),s) +* (Initialized (stop (for-up a,i,n,I)))) by A64, XXREAL_0:1;
then A66: 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 A20, A65, AMI_1:122;
(IExec (I ';' (AddTo a,i,n)),s) | NAT = s | NAT 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: verum