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, AMI_1:def 46
;
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 AMI_1:14
.=
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