let s be State of SCM+FSA; for I being Program of SCM+FSA st I is_closed_on Initialized s & I is_halting_on Initialized s holds
( IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) )
let I be Program of SCM+FSA; ( I is_closed_on Initialized s & I is_halting_on Initialized s implies ( IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) ) )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (Directed I));
set m1 = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)));
assume A1:
I is_closed_on Initialized s
; ( not I is_halting_on Initialized s or ( IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) ) )
Directed I c= Initialized (Directed I)
by SCMFSA6A:26;
then A2:
dom (Directed I) c= dom (Initialized (Directed I))
by GRFUNC_1:8;
A3:
dom I = dom (Directed I)
by FUNCT_4:105;
set l1 = IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))));
A4:
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA)))
by Th13;
then A5:
IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) in dom I
by A1, SCMFSA7B:def 7;
assume A6:
I is_halting_on Initialized s
; ( IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) )
then
IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) in dom I
by A1, A5, Th44, COMPOS_1:24;
then A7:
IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) in dom (Directed I)
by FUNCT_4:105;
A8:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by A6, A4, SCMFSA7B:def 8;
Y:
(ProgramPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) /. (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) = (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by COMPOS_1:38;
TX:
ProgramPart (s +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by AMI_1:123;
I c= Initialized I
by SCMFSA6A:26;
then
dom I c= dom (Initialized I)
by GRFUNC_1:8;
then
(s +* (Initialized I)) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) = (Initialized I) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by A5, FUNCT_4:14;
then A9: I . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) =
(s +* (Initialized I)) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by A5, SCMFSA6A:50
.=
CurInstr ((ProgramPart (s +* (Initialized I))),(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by Y, TX, AMI_1:54
.=
halt SCM+FSA
by A8, EXTPRO_1:def 14
;
IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by A1, A6, Th44, COMPOS_1:24;
then A10: (s +* (Initialized (Directed I))) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) =
(Initialized (Directed I)) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by A7, A2, FUNCT_4:14
.=
(Directed I) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by A5, A3, SCMFSA6A:50
.=
goto (card I)
by A5, A9, FUNCT_4:112
;
Y:
(ProgramPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) /. (IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) = (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . (IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by COMPOS_1:38;
A11: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))),(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) =
(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by A1, A6, Th44, Y, COMPOS_1:24
.=
goto (card I)
by A10, AMI_1:54
;
T:
ProgramPart (s +* (Initialized (Directed I))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by AMI_1:123;
A12: Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)) =
Following ((ProgramPart (s +* (Initialized (Directed I)))),(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by EXTPRO_1:4
.=
Exec ((goto (card I)),(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))))
by A11, T
;
hence
IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I
by SCMFSA_2:95; DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))
A13:
( ( for a being Int-Location holds (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) . a = (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . a ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) . f = (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . f ) )
by A12, SCMFSA_2:95;
DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by A1, A6, Th44, SCMFSA6A:39;
hence
DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))
by A13, SCMFSA6A:38; verum