let s be State of ; :: thesis: for I being Program of 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 ; :: 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)) ) )
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 (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))));
A4: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by Th13;
then A5: IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) in dom I by A1, SCMFSA7B:def 7;
assume A6: 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)) )
then IC (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) in dom I by A1, A5, Th44, AMI_1:121;
then A7: IC (Computation (s +* (Initialized (Directed I))),(LifeSpan (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;
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 A5, FUNCT_4:14;
then A9: I . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) = (s +* (Initialized I)) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A5, SCMFSA6A:50
.= CurInstr (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) by AMI_1:54
.= halt SCM+FSA by A8, AMI_1:def 46 ;
IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = IC (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) by A1, A6, Th44, AMI_1:121;
then A10: (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 A7, A2, FUNCT_4:14
.= (Directed I) . (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) by A5, A3, SCMFSA6A:50
.= goto (insloc (card I)) by A5, A9, FUNCT_4:112 ;
A11: 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, A6, Th44, AMI_1:121
.= goto (insloc (card I)) by A10, AMI_1:54 ;
A12: 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 A11 ;
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))
A13: ( ( 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 A12, SCMFSA_2:95;
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),(LifeSpan (s +* (Initialized I)))) by A1, A6, Th44, SCMFSA6A:39;
hence DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) by A13, SCMFSA6A:38; :: thesis: verum