let P1, P2 be Instruction-Sequence of SCM+FSA; for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )
let s1, s2 be State of SCM+FSA; for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )
set D = Data-Locations ;
let I be really-closed Program of SCM+FSA; ( I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) ) )
set ss2 = Initialize s2;
set PP2 = P2 +* I;
set ss1 = Initialize s1;
set PP1 = P1 +* I;
assume A1:
I is_halting_on s1,P1
; ( not DataPart s1 = DataPart s2 or ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) ) )
then A2:
P1 +* I halts_on Initialize s1
;
then A3:
Result ((P1 +* I),(Initialize s1)) = Comput ((P1 +* I),(Initialize s1),(LifeSpan ((P1 +* I),(Initialize s1))))
by EXTPRO_1:23;
assume A4:
DataPart s1 = DataPart s2
; ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )
then
I is_halting_on s2,P2
by A1, SCMFSA8B:5;
then A5:
P2 +* I halts_on Initialize s2
;
A6:
now for l being Nat st CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),l))) = halt SCM+FSA holds
LifeSpan ((P1 +* I),(Initialize s1)) <= llet l be
Nat;
( CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),l))) = halt SCM+FSA implies LifeSpan ((P1 +* I),(Initialize s1)) <= l )assume A7:
CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),l)))
= halt SCM+FSA
;
LifeSpan ((P1 +* I),(Initialize s1)) <= l
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),l)))
= CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),l)))
by A1, A4, Th62;
hence
LifeSpan (
(P1 +* I),
(Initialize s1))
<= l
by A2, A7, EXTPRO_1:def 15;
verum end;
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(LifeSpan ((P1 +* I),(Initialize s1)))))) =
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(LifeSpan ((P1 +* I),(Initialize s1))))))
by A1, A4, Th62
.=
halt SCM+FSA
by A2, EXTPRO_1:def 15
;
hence
LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2))
by A6, A5, EXTPRO_1:def 15; Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2))
then
Result ((P2 +* I),(Initialize s2)) = Comput ((P2 +* I),(Initialize s2),(LifeSpan ((P1 +* I),(Initialize s1))))
by A5, EXTPRO_1:23;
hence
Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2))
by A1, A4, A3, Th62; verum