let p be Instruction-Sequence of SCM+FSA; 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)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
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)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
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)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
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)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) )
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)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
set Is = Initialized s;
A5:
(Initialized s) . (intloc 0) = 1
by SCMFSA6A:38;
set s1 = Initialized s;
set p1 = p +* Ig;
set m1 = LifeSpan ((p +* Ig),(Initialized s));
set s3 = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))));
set p3 = (p +* Ig) +* J;
A6:
((p +* Ig) +* J) +* J = (p +* Ig) +* J
by FUNCT_4:93;
Initialized s = Initialized (Initialized s)
;
then A8:
Initialized s = Initialize (Initialized s)
by A5, SCMFSA8C:4;
then A9:
p +* Ig halts_on Initialized s
by A1, SCMFSA7B:def 7;
then A10:
Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s)))
by EXTPRO_1:23;
set s2 = Initialized s;
set p2 = p +* (Ig ';' J);
A11:
Ig ';' J c= p +* (Ig ';' J)
by FUNCT_4:25;
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),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) . (intloc 0) = 1
by A3, A5, A8, SCMFSA8C:68;
then A14:
Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by SCMFSA8C:4;
then
Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by FUNCT_4:25;
then A15:
Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
by FUNCT_4:98;
DataPart (IExec (Ig,p,s)) =
DataPart (Result ((p +* Ig),(Initialized s)))
by SCMFSA6B:def 1
.=
DataPart (Result ((p +* Ig),(Initialized s)))
.=
DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by A9, EXTPRO_1:23
;
then A16:
DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
by A14, MEMSTR_0:79;
then A17:
J is_halting_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J
by A2, A4, SCMFSA8B:5;
Initialize (Initialized s) = Initialized s
by MEMSTR_0:44;
then
Result (((p +* (Ig ';' J)) +* Ig),(Initialized s)) = Result ((p +* Ig),(Initialized s))
by A1, A3, A12, SCMFSA8C:72;
then
Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))) = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by A10;
then A20:
DataPart (Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s)))) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
;
A21: DataPart (IExec (Ig,p,s)) =
DataPart (IExec (Ig,p,(Initialized s)))
by SCMFSA8C:3
.=
DataPart (IExec (Ig,(p +* (Ig ';' J)),(Initialized s)))
by A1, A3, A5, A12, SCMFSA8C:20
;
then A22:
J is_closed_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J)
by A2, A4, SCMFSA8B:5;
A23:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A24:
Ig is_closed_on Initialized s,p +* (Ig ';' J)
by A3, A12, SCMFSA8B:3;
A25:
J is_halting_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J)
by A2, A4, A21, SCMFSA8B:5;
Ig is_halting_on Initialized s,p +* (Ig ';' J)
by A1, A3, A12, SCMFSA8B:5;
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:25, MEMSTR_0:50;
then A27:
Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))) = Initialize (Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))))
by FUNCT_4:98;
A28:
J is_closed_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J
by A4, A16, SCMFSA8B:3;
A29:
LifeSpan (((p +* (Ig ';' J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s))
by A1, A3, A8, A12, SCMFSA8C:72;
LifeSpan ((((p +* (Ig ';' J)) +* Ig) +* J),(Initialized (Result (((p +* (Ig ';' J)) +* Ig),(Initialized s))))) = LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))
by A28, A17, A15, A27, A20, A6, SCMFSA8C:72;
hence
LifeSpan ((p +* (Ig ';' J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))
by A10, A26, A29; verum