let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let s be State of SCM+FSA; for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let J be Program of SCM+FSA; for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let Ig be good Program of SCM+FSA; ( Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p implies LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) )
set I = Ig;
assume that
A1:
Ig is_halting_on Initialized s,p
and
A2:
J is_halting_on IExec (Ig,p,s),p
and
A3:
Ig is_closed_on Initialized s,p
and
A4:
J is_closed_on IExec (Ig,p,s),p
; LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
set Is = Initialized s;
A5:
(Initialized s) . (intloc 0) = 1
by SCMFSA6C:3;
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set p1 = p +* Ig;
set m1 = LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))));
set s3 = (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1));
set p3 = (p +* Ig) +* J;
A6:
((p +* Ig) +* J) +* J = (p +* Ig) +* J
by FUNCT_4:99;
s +* (Initialize ((intloc 0) .--> 1)) = (Initialized s) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:99;
then A8:
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s)
by A5, SCMFSA8C:18;
then A9:
p +* Ig halts_on s +* (Initialize ((intloc 0) .--> 1))
by A1, SCMFSA7B:def 8;
then A10:
(Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))
by EXTPRO_1:23;
set s2 = Initialized s;
set p2 = p +* (Ig ';' J);
A11:
Ig ';' J c= p +* (Ig ';' J)
by FUNCT_4:26;
A12:
DataPart (Initialized s) = DataPart (Initialized s)
;
A13:
(Initialized s) . (intloc 0) = 1
by A5;
set JAt = Start-At (0,SCM+FSA);
(Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) = 1
by A3, A5, A8, SCMFSA8C:97;
then A14:
(Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))
by SCMFSA8C:18;
then
Start-At (0,SCM+FSA) c= (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
then A15:
(Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = Initialize ((Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:103, FUNCT_4:104;
DataPart (IExec (Ig,p,s)) =
DataPart ((Result ((p +* Ig),(Initialized s))) +* (s | NAT))
by SCMFSA6B:def 1
.=
DataPart (Result ((p +* Ig),(Initialized s)))
by COMPOS_1:82
.=
DataPart (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A9, EXTPRO_1:23
;
then A16:
DataPart (IExec (Ig,p,s)) = DataPart ((Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by A14, SCMFSA8A:10;
then A17:
J is_halting_on (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)),(p +* Ig) +* J
by A2, A4, SCMFSA8B:8;
Initialize (Initialized s) = Initialized s
by SCMFSA6A:83;
then
NPP (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))) = NPP (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))
by A1, A3, A12, SCMFSA8C:101;
then
NPP (Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s)))) = NPP ((Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by A10, COMPOS_1:235;
then A20:
DataPart ((Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))) +* (Initialize ((intloc 0) .--> 1))) = DataPart ((Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by COMPOS_1:138;
A21: DataPart (IExec (Ig,p,s)) =
DataPart (IExec (Ig,p,(Initialized s)))
by SCMFSA8C:17
.=
DataPart (IExec (Ig,(p +* (Ig ';' J)),(Initialized s)))
by A1, A3, A5, A12, SCMFSA8C:46
;
then A22:
J is_closed_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J)
by A2, A4, SCMFSA8B:8;
A23:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A24:
Ig is_closed_on Initialized s,p +* (Ig ';' J)
by A3, A12, SCMFSA8B:6;
A25:
J is_halting_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J)
by A2, A4, A21, SCMFSA8B:8;
Ig is_halting_on Initialized s,p +* (Ig ';' J)
by A1, A3, A12, SCMFSA8B:8;
then A26:
LifeSpan ((p +* (Ig ';' J)),(Initialized s)) = ((LifeSpan (((p +* (Ig ';' J)) +* Ig),(Initialized s))) + 1) + (LifeSpan ((((p +* (Ig ';' J)) +* Ig) +* J),(Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))))))
by A24, A13, A22, A25, A23, Lm1, A11;
Start-At (0,SCM+FSA) c= Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s)))
by FUNCT_4:26, SCMFSA6B:8;
then A27:
Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))) = Initialize (Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))))
by FUNCT_4:103, FUNCT_4:104;
A28:
J is_closed_on (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)),(p +* Ig) +* J
by A4, A16, SCMFSA8B:6;
A29:
LifeSpan (((p +* (Ig ';' J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))
by A1, A3, A8, A12, SCMFSA8C:101;
LifeSpan ((((p +* (Ig ';' J)) +* Ig) +* J),((Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))
by A28, A17, A15, A27, A20, A6, SCMFSA8C:101;
hence
LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
by A10, A26, A29; verum