let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on Initialize s & I is_halting_on Initialize s implies ( IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) ) )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (Directed I));
set m1 = LifeSpan (s +* (Initialized I));
assume A1: I is_closed_on Initialize s ; :: thesis: ( not I is_halting_on Initialize s or ( IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) ) )
assume A2: I is_halting_on Initialize s ; :: thesis: ( IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) )
A3: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by Th13;
then A4: s +* (Initialized I) is halting by A2, SCMFSA7B:def 8;
A6: DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) by A1, A2, Th44, SCMFSA6A:39;
set l1 = IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))));
A7: IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) in dom I by A1, A3, SCMFSA7B:def 7;
then ( IC (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) in dom I & Directed I c= Initialized (Directed I) ) by A1, A2, Th44, AMI_1:121, SCMFSA6A:26;
then A8: ( IC (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) in dom (Directed I) & dom (Directed I) c= dom (Initialized (Directed I)) ) by FUNCT_4:105, GRFUNC_1:8;
A9: IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = IC (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) by A1, A2, Th44, AMI_1:121;
I c= Initialized I by SCMFSA6A:26;
then dom I c= dom (Initialized I) by GRFUNC_1:8;
then (s +* (Initialized I)) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) = (Initialized I) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A7, FUNCT_4:14;
then A10: I . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) = (s +* (Initialized I)) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A7, SCMFSA6A:50
.= CurInstr (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) by AMI_1:54
.= halt SCM+FSA by A4, AMI_1:def 46 ;
A13: dom I = dom (Directed I) by FUNCT_4:105;
A14: (s +* (Initialized (Directed I))) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) = (Initialized (Directed I)) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A8, A9, FUNCT_4:14
.= (Directed I) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A7, A13, SCMFSA6A:50
.= goto (insloc (card I)) by A7, A10, FUNCT_4:112 ;
A15: CurInstr (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) = (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A1, A2, Th44, AMI_1:121
.= goto (insloc (card I)) by A14, AMI_1:54 ;
A16: Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1) = Following (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) by AMI_1:14
.= Exec (goto (insloc (card I))),(Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) by A15 ;
hence IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) by SCMFSA_2:95; :: thesis: DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1))
( ( for a being Int-Location holds (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) . a = (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) . a ) & ( for f being FinSeq-Location holds (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) . f = (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) . f ) ) by A16, SCMFSA_2:95;
hence DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) by A6, SCMFSA6A:38; :: thesis: verum