let s be State of ; for I being Program of st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) )
let I be Program of ; ( I is_closed_on s & I is_halting_on s implies ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) ) )
set s1 = s +* (I +* (Start-At (insloc 0 )));
set s2 = s +* ((Directed I) +* (Start-At (insloc 0 )));
set m1 = LifeSpan (s +* (I +* (Start-At (insloc 0 ))));
assume that
A1:
I is_closed_on s
and
A2:
I is_halting_on s
; ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) )
A3:
ProgramPart (s +* (I +* (Start-At (insloc 0 )))) halts_on s +* (I +* (Start-At (insloc 0 )))
by A2, SCMFSA7B:def 8;
set l1 = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))));
A4:
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) in dom I
by A1, SCMFSA7B:def 7;
then
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) in dom I
by A1, A2, Th35, AMI_1:121;
then A5:
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) in dom (Directed I)
by FUNCT_4:105;
Directed I c= (Directed I) +* (Start-At (insloc 0 ))
by Th9;
then A6:
dom (Directed I) c= dom ((Directed I) +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
A7:
dom I = dom (Directed I)
by FUNCT_4:105;
I c= I +* (Start-At (insloc 0 ))
by Th9;
then
dom I c= dom (I +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
then
(s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))) = (I +* (Start-At (insloc 0 ))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))))
by A4, FUNCT_4:14;
then A8: I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))) =
(s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))))
by A4, SCMFSA6B:7
.=
CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))
by AMI_1:54
.=
halt SCM+FSA
by A3, AMI_1:def 46
;
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))
by A1, A2, Th35, AMI_1:121;
then A9: (s +* ((Directed I) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))) =
((Directed I) +* (Start-At (insloc 0 ))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))))
by A5, A6, FUNCT_4:14
.=
(Directed I) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))))
by A4, A7, SCMFSA6B:7
.=
goto (insloc (card I))
by A4, A8, FUNCT_4:112
;
A10: CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) =
(Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))))
by A1, A2, Th35, AMI_1:121
.=
goto (insloc (card I))
by A9, AMI_1:54
;
A11: Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) =
Following (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))
by AMI_1:14
.=
Exec (goto (insloc (card I))),(Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))
by A10
;
hence
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I)
by SCMFSA_2:95; DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1))
A12:
( ( for a being Int-Location holds (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) . a = (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . a ) & ( for f being FinSeq-Location holds (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) . f = (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . f ) )
by A11, SCMFSA_2:95;
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))
by A1, A2, Th35, SCMFSA6A:39;
hence
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1))
by A12, SCMFSA6A:38; verum