let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_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 Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_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 really-closed Program of SCM+FSA; for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_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 really-closed Program of SCM+FSA; ( Ig is_halting_on Initialized s,p & J is_halting_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
; 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;
A3:
(Initialized s) . (intloc 0) = 1
by SCMFSA_M:9;
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;
Initialized s = Initialized (Initialized s)
;
then A4:
Initialized s = Initialize (Initialized s)
by A3, SCMFSA_M:18;
then A5:
p +* Ig halts_on Initialized s
by A1;
then A6:
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);
A7:
Ig ";" J c= p +* (Ig ";" J)
by FUNCT_4:25;
A8:
DataPart (Initialized s) = DataPart (Initialized s)
;
A9:
(Initialized s) . (intloc 0) = 1
by A3;
set JAt = Start-At (0,SCM+FSA);
(Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) . (intloc 0) = 1
by A3, A4, SCMFSA8C:68;
then A10:
Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by SCMFSA_M:18;
then
Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by FUNCT_4:25;
then A11:
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 A5, EXTPRO_1:23
;
then
DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
by A10, MEMSTR_0:79;
then A12:
J is_halting_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J
by A2, 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, A8, SCMFSA8C:72;
then
Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by A6;
then A13:
DataPart (Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
;
A14: 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, A8, SCMFSA8C:20
;
A15:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A16:
J is_halting_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J)
by A2, A14, SCMFSA8B:5;
Ig is_halting_on Initialized s,p +* (Ig ";" J)
by A1, A8, SCMFSA8B:5;
then A17:
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 A9, A16, A15, Lm1, A7;
Start-At (0,SCM+FSA) c= Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))
by FUNCT_4:25, MEMSTR_0:50;
then A18:
Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) = Initialize (Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))))
by FUNCT_4:98;
A19:
LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s))
by A1, A4, A8, 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 A12, A11, A18, A13, 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 A6, A17, A19; verum