let s be State of SCM+FSA ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
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 A1: ( I is_closed_on s & I is_halting_on s ) ; :: thesis:
then A2: s +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
A4: 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, Th35, SCMFSA6A:39;
set l1 = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))));
A5: 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 & Directed I c= (Directed I) +* (Start-At (insloc 0 )) ) by A1, Th35, Th9, AMI_1:121;
then A6: ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) in dom (Directed I) & dom (Directed I) c= dom ((Directed I) +* (Start-At (insloc 0 ))) ) by FUNCT_4:105, GRFUNC_1:8;
A7: 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, Th35, AMI_1:121;
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 A5, 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 A5, 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 A2, AMI_1:def 46 ;
A11: dom I = dom (Directed I) by FUNCT_4:105;
A12: (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 A6, A7, FUNCT_4:14
.= (Directed I) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))) by A5, A11, SCMFSA6B:7
.= goto (insloc (card I)) by A5, A8, FUNCT_4:112 ;
A13: 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, Th35, AMI_1:121
.= goto (insloc (card I)) by A12, AMI_1:54 ;
A14: 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 A13 ;
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; :: thesis:
( ( 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 A14, SCMFSA_2:95;
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 A4, SCMFSA6A:38; :: thesis: