let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds

IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds

IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P implies IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) )

set s1 = Initialized s;

assume A1: I is_halting_on Initialized s,P ; :: thesis: IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

then A2: P +* I halts_on Initialized s by A1, SCMFSA7B:def 7;

( P +* (I ";" (Stop SCM+FSA)) halts_on Initialized s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (LifeSpan ((P +* I),(Initialized s))) + 1 ) by A1, Lm4;

then A3: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 1)) by EXTPRO_1:23;

then DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, Lm4;

then A4: DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Result ((P +* I),(Initialized s))) by A2, EXTPRO_1:23

.= DataPart ((Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))) by MEMSTR_0:79 ;

IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = card I by A1, A3, Lm4

.= IC ((Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))) by FUNCT_4:113 ;

then A5: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A4, MEMSTR_0:78;

A6: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A5;

thus IExec ((I ";" (Stop SCM+FSA)),P,s) = Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) by SCMFSA6B:def 1

.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A6

.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))

.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))

.= (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) by SCMFSA6B:def 1 ; :: thesis: verum

for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds

IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds

IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P implies IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) )

set s1 = Initialized s;

assume A1: I is_halting_on Initialized s,P ; :: thesis: IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

then A2: P +* I halts_on Initialized s by A1, SCMFSA7B:def 7;

( P +* (I ";" (Stop SCM+FSA)) halts_on Initialized s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (LifeSpan ((P +* I),(Initialized s))) + 1 ) by A1, Lm4;

then A3: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 1)) by EXTPRO_1:23;

then DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, Lm4;

then A4: DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Result ((P +* I),(Initialized s))) by A2, EXTPRO_1:23

.= DataPart ((Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))) by MEMSTR_0:79 ;

IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = card I by A1, A3, Lm4

.= IC ((Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))) by FUNCT_4:113 ;

then A5: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A4, MEMSTR_0:78;

A6: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A5;

thus IExec ((I ";" (Stop SCM+FSA)),P,s) = Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) by SCMFSA6B:def 1

.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A6

.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))

.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))

.= (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) by SCMFSA6B:def 1 ; :: thesis: verum