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 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;
A6:
((p +* Ig) +* J) +* J = (p +* Ig) +* J
;
Initialized s = Initialized (Initialized s)
;
then A7:
Initialized s = Initialize (Initialized s)
by A5, SCMFSA_M:18;
then A8:
p +* Ig halts_on Initialized s
by A1, SCMFSA7B:def 7;
then A9:
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);
A10:
Ig ";" J c= p +* (Ig ";" J)
by FUNCT_4:25;
A11:
DataPart (Initialized s) = DataPart (Initialized s)
;
A12:
(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, A7, SCMFSA8C:68;
then A13:
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 A14:
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 A8, EXTPRO_1:23
;
then A15:
DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
by A13, MEMSTR_0:79;
then A16:
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, A11, SCMFSA8C:72;
then
Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
by A9;
then A17:
DataPart (Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))
;
A18: 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, A11, SCMFSA8C:20
;
then A19:
J is_closed_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J)
by A2, A4, SCMFSA8B:5;
A20:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
A21:
Ig is_closed_on Initialized s,p +* (Ig ";" J)
by A3, A11, SCMFSA8B:3;
A22:
J is_halting_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J)
by A2, A4, A18, SCMFSA8B:5;
Ig is_halting_on Initialized s,p +* (Ig ";" J)
by A1, A3, A11, SCMFSA8B:5;
then A23:
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 A21, A12, A19, A22, A20, Lm1, A10;
Start-At (0,SCM+FSA) c= Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s)))
by FUNCT_4:25, MEMSTR_0:50;
then A24:
Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))) = Initialize (Initialized (Result (((p +* (Ig ";" J)) +* Ig),(Initialized s))))
by FUNCT_4:98;
A25:
J is_closed_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J
by A4, A15, SCMFSA8B:3;
A26:
LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s))
by A1, A3, A7, A11, 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 A25, A16, A14, A24, A17, 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 A9, A23, A26; verum