let s be State of SCM+FSA; for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) )
let I be Program of SCM+FSA; ( I is_closed_on s,P & I is_halting_on s,P implies ( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) ) )
set s1 = s +* (Initialize I);
set s2 = s +* (Initialize (Directed I));
set m1 = LifeSpan ((P +* I),(s +* (Initialize I)));
A1:
ProgramPart I = I
by RELAT_1:209;
A2:
dom (P +* I) = NAT
by PARTFUN1:def 4;
A3:
dom (P +* (Directed I)) = NAT
by PARTFUN1:def 4;
assume that
A4:
I is_closed_on s,P
and
A5:
I is_halting_on s,P
; ( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) )
A6:
P +* I halts_on s +* (Initialize I)
by A5, SCMFSA7B:def 8, A1;
set l1 = IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))));
A7:
IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) in dom I
by A4, SCMFSA7B:def 7, A1;
then
IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))) in dom I
by A4, A5, Th35, COMPOS_1:24;
then A8:
IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))) in dom (Directed I)
by FUNCT_4:105;
I c= P +* I
by FUNCT_4:26;
then A9: I . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) =
(P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by GRFUNC_1:8, A7
.=
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by A2, PARTFUN1:def 8
.=
halt SCM+FSA
by A6, EXTPRO_1:def 14
;
IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))
by A4, A5, Th35, COMPOS_1:24;
then A10: (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) =
(Directed I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by A8, FUNCT_4:14
.=
(Directed I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
.=
goto (card I)
by A7, A9, FUNCT_4:112
;
A11: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) =
(P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by A3, PARTFUN1:def 8
.=
(P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by A4, A5, Th35, COMPOS_1:24
.=
goto (card I)
by A10
;
A12: Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)) =
Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by EXTPRO_1:4
.=
Exec ((goto (card I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
by A11
;
hence
IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I
by SCMFSA_2:95; DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)))
A13:
( ( for a being Int-Location holds (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) . a = (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) . f = (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I)))))) . f ) )
by A12, SCMFSA_2:95;
DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))
by A4, A5, Th35, COMPOS_1:138;
hence
DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)))
by A13, SCMFSA6A:38; verum