let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS 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; for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS 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 SCMPDS; for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
let J be parahalting shiftable Program of SCMPDS; 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))))));
A2:
stop J c= (P +* (stop I)) +* (stop J)
by FUNCT_4:25;
then A3:
(P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))
by SCMPDS_4:def 7;
A6:
s = s
by MEMSTR_0:44;
A9:
stop J c= P +* (stop J)
by FUNCT_4:25;
A11:
stop I c= P +* (stop I)
by FUNCT_4:25;
then
P +* (stop I) halts_on s
by SCMPDS_4:def 7;
then A12:
Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (IExec (I,P,s))
by EXTPRO_1:23;
B13:
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 A2, A9, Th21, A12;
A15:
stop I c= (P +* (stop (I ';' J))) +* (stop I)
by FUNCT_4:25;
A16:
s = s
by MEMSTR_0:44;
A19: ((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 Th17
;
A20:
LifeSpan (((P +* (stop (I ';' J))) +* (stop I)),s) = LifeSpan ((P +* (stop I)),s)
by A11, A15, Th21;
set S1 = s;
set E1 = (P +* (stop (I ';' J))) +* (stop I);
X2:
Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))
by FUNCT_4:25, Th24;
B21: (P +* (stop I)) +* (stop (I ';' J)) =
P +* ((stop I) +* (stop (I ';' J)))
by FUNCT_4:14
.=
P +* ((stop (I ';' J)) +* (stop (I ';' J)))
by Th17
.=
((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J))
by A19, FUNCT_4:14
;
A22:
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 B21, X2, FUNCT_4:25, A20, Th24;
A23:
stop (I ';' J) c= P +* (stop (I ';' J))
by FUNCT_4:25;
then A24: 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 A20, Lm4, A16
.=
DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))
by MEMSTR_0:45
;
A25:
Shift ((stop J),(card I)) c= P +* (stop (I ';' J))
by A23, A15, Lm4;
A26:
IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I
by A23, A20, Lm4, A16;
B29:
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 A22, A24, MEMSTR_0:45;
then A27:
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 A25, A2, A26, SCMPDS_4:29;
A29:
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 A26, A25, A2, B29, SCMPDS_4:29;
A30:
P +* (stop I) halts_on s
by A11, SCMPDS_4:def 7;
then A31:
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);
A33:
IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) = IC (Result ((P +* (stop J)),(Initialize (IExec (I,P,s)))))
by Th21, A2, A9;
B34:
P +* (stop (I ';' J)) halts_on s
by A23, SCMPDS_4:def 7;
A35: IC (IExec ((I ';' J),P,s)) =
IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s))))
by A6, B34, 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 A31, Th37, A6
.=
(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 A27, EXTPRO_1:4
.=
(IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))) + (card I)
by A3, EXTPRO_1:23
.=
(IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I)
by A33, A30, EXTPRO_1:23
;
IExec ((I ';' J),P,s) =
Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s)))
by A6, B34, 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 A31, Th37, A6
;
then A36: 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 A29, EXTPRO_1:4
.=
DataPart (IExec (J,P,(Initialize (IExec (I,P,s)))))
by B13, A3, EXTPRO_1:23
;
hereby verum
reconsider l =
(IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) as
Element of
NAT ;
A37:
dom (Start-At (l,SCMPDS)) = {(IC )}
by FUNCOP_1:13;
A38:
now let x be
set ;
( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1 )assume A39:
x in dom (IExec ((I ';' J),P,s))
;
(IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1per cases
( x is Int_position or x = IC )
by A39, SCMPDS_4:6;
suppose A40:
x is
Int_position
;
(IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1then
x <> IC
by SCMPDS_2:43;
then A41:
not
x in dom (Start-At (l,SCMPDS))
by A37, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(Initialize (IExec (I,P,s))))) . x
by A36, A40, SCMPDS_4:8;
hence
(IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x
by A41, FUNCT_4:11;
verum end; suppose A42:
x = IC
;
(IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1then
x in {(IC )}
by TARSKI:def 1;
then A43:
x in dom (Start-At (l,SCMPDS))
by FUNCOP_1:13;
thus (IExec ((I ';' J),P,s)) . x =
(Start-At (l,SCMPDS)) . (IC )
by A35, A42, FUNCOP_1:72
.=
(IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x
by A42, A43, FUNCT_4:13
;
verum 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 A38, FUNCT_1:2;
verum
end;