let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let P be Instruction-Sequence of SCM+FSA; for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let I be really-closed Program of SCM+FSA; ( I is_halting_on s,P implies ( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan ((P +* I),(Initialize s));
A1:
dom (P +* I) = NAT
by PARTFUN1:def 2;
A2:
dom (P +* (Directed I)) = NAT
by PARTFUN1:def 2;
assume A3:
I is_halting_on s,P
; ( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
A4:
P +* I halts_on Initialize s
by A3, SCMFSA7B:def 7;
set l1 = IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))));
IC (Initialize s) = 0
by MEMSTR_0:47;
then A5:
IC (Initialize s) in dom I
by AFINSQ_1:65;
A6:
I c= P +* I
by FUNCT_4:25;
A7:
IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I
by A5, A6, AMISTD_1:21;
A8:
Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) = Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))
by A3, Th12;
then
IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I
by A7;
then A9:
IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom (Directed I)
by FUNCT_4:99;
I c= P +* I
by FUNCT_4:25;
then A10: I . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) =
(P +* I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))))
by A7, GRFUNC_1:2
.=
CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))))
by A1, PARTFUN1:def 6
.=
halt SCM+FSA
by A4, EXTPRO_1:def 15
;
IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))
by A8;
then A11: (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) =
(Directed I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))))
by A9, FUNCT_4:13
.=
goto (card I)
by A7, A10, FUNCT_4:106
;
A12: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) =
(P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))))
by A2, PARTFUN1:def 6
.=
goto (card I)
by A11, A8
;
A13: Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) =
Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))))
by EXTPRO_1:3
.=
Exec ((goto (card I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))))
by A12
;
hence
IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I
by SCMFSA_2:69; DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))
A14:
( ( for a being Int-Location holds (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a = (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f = (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) . f ) )
by A13, SCMFSA_2:69;
DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))
by A8;
hence
DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))
by A14, SCMFSA_M:2; verum