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