let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of
for J being parahalting shiftable Program of holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of
for J being parahalting shiftable Program of holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
let I be halt-free parahalting Program of ; :: thesis: for J being parahalting shiftable Program of holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
let J be parahalting shiftable Program of ; :: thesis: IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
set A = NAT ;
set D = SCM-Data-Loc ;
set sI = stop I;
set sIJ = stop (I ';' J);
set P1 = P +* (stop I);
set m1 = LifeSpan ((P +* (stop I)),s);
set P2 = P +* (stop (I ';' J));
set s3 = Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))));
A1: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
then A2: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by SCMPDS_4:def 7;
A3: stop J c= P +* (stop J) by FUNCT_4:25;
A4: stop I c= P +* (stop I) by FUNCT_4:25;
then P +* (stop I) halts_on s by SCMPDS_4:def 7;
then A5: Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (IExec (I,P,s)) by EXTPRO_1:23;
A6: Result ((P +* (stop J)),(Initialize (IExec (I,P,s)))) = Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))) by A1, A3, Th6, A5;
A7: stop I c= (P +* (stop (I ';' J))) +* (stop I) by FUNCT_4:25;
A8: ((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J)) = (P +* (stop (I ';' J))) +* ((stop I) +* (stop (I ';' J))) by FUNCT_4:14
.= (P +* (stop (I ';' J))) +* (stop (I ';' J)) by Th3 ;
A9: LifeSpan (((P +* (stop (I ';' J))) +* (stop I)),s) = LifeSpan ((P +* (stop I)),s) by A4, A7, Th6;
set S1 = s;
set E1 = (P +* (stop (I ';' J))) +* (stop I);
A10: Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s))) by Th8, FUNCT_4:25;
A11: (P +* (stop I)) +* (stop (I ';' J)) = P +* ((stop I) +* (stop (I ';' J))) by FUNCT_4:14
.= P +* ((stop (I ';' J)) +* (stop (I ';' J))) by Th3
.= ((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J)) by A8 ;
A12: DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by A11, A10, A9, Th8, FUNCT_4:25;
A13: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25;
then A14: DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Initialize (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A9, Lm4
.= DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by MEMSTR_0:45 ;
A15: Shift ((stop J),(card I)) c= P +* (stop (I ';' J)) by A13, A7, Lm4;
A16: IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A13, A9, Lm4;
A17: DataPart (Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) by A12, A14, MEMSTR_0:45;
then A18: IC (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) + (card I) by A15, A1, A16, SCMPDS_4:29;
A19: DataPart (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) = DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A16, A15, A1, A17, SCMPDS_4:29;
A20: P +* (stop I) halts_on s by A4, SCMPDS_4:def 7;
then A21: Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (Result ((P +* (stop I)),s)) by EXTPRO_1:23;
set SS1 = (Initialize (Result ((P +* (stop I)),s))) +* (stop J);
set SS2 = (Initialize (IExec (I,P,s))) +* (stop J);
A22: IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) = IC (Result ((P +* (stop J)),(Initialize (IExec (I,P,s))))) by Th6, A1, A3;
A23: P +* (stop (I ';' J)) halts_on s by A13, SCMPDS_4:def 7;
A24: IC (IExec ((I ';' J),P,s)) = IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s)))) by A23, EXTPRO_1:23
.= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) by A21, Th21
.= (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) + (card I) by A18, EXTPRO_1:4
.= (IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))) + (card I) by A2, EXTPRO_1:23
.= (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) by A22, A20, EXTPRO_1:23 ;
IExec ((I ';' J),P,s) = Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s))) by A23, EXTPRO_1:23
.= Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A21, Th21 ;
then A25: DataPart (IExec ((I ';' J),P,s)) = DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A19, EXTPRO_1:4
.= DataPart (IExec (J,P,(Initialize (IExec (I,P,s))))) by A6, A2, EXTPRO_1:23 ;

hereby :: thesis: verum

reconsider l = (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) as Nat ;
A26: dom (Start-At (l,SCMPDS)) = {(IC )} by FUNCOP_1:13;

A27: now :: thesis: for x being object st x in dom (IExec ((I ';' J),P,s)) holds
(IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x

let x be object ; :: thesis: ( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁ )
assume A28: x in dom (IExec ((I ';' J),P,s)) ; :: thesis: (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁

per cases ( x is Int_position or x = IC ) by A28, SCMPDS_4:6;

suppose A29: x is Int_position ; :: thesis: (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁

then x <> IC by SCMPDS_2:43;
then A30: not x in dom (Start-At (l,SCMPDS)) by A26, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(Initialize (IExec (I,P,s))))) . x by A25, A29, SCMPDS_4:8;
hence (IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A30, FUNCT_4:11; :: thesis: verum

end;

suppose A31: x = IC ; :: thesis: (IExec ((I ';' J),P,s)) . b₁ = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b₁

then x in {(IC )} by TARSKI:def 1;
then A32: x in dom (Start-At (l,SCMPDS)) by FUNCOP_1:13;
thus (IExec ((I ';' J),P,s)) . x = (Start-At (l,SCMPDS)) . (IC ) by A24, A31, FUNCOP_1:72
.= (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A31, A32, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

dom (IExec ((I ';' J),P,s)) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) by PARTFUN1:def 2 ;
hence IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) by A27, FUNCT_1:2; :: thesis: verum

end;