let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies ( IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) ) )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (Directed I));
set m1 = LifeSpan ((P +* I),(s +* (Initialized I)));
A1: ProgramPart I = I by RELAT_1:209;
A2: dom (P +* I) = NAT by PARTFUN1:def 4;
A3: dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
assume A4: I is_closed_on Initialized s,P ; :: thesis: ( not I is_halting_on Initialized s,P or ( IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) ) )
set l1 = IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))));
A5: s +* (Initialized I) = (Initialized s) +* (Initialize I) by Th13;
then A6: IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) in dom I by A4, SCMFSA7B:def 7, A1;
assume A7: I is_halting_on Initialized s,P ; :: thesis: ( IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) )
then IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) in dom I by A4, A6, Th44, COMPOS_1:24;
then A8: IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) in dom (Directed I) by FUNCT_4:105;
A9: P +* I halts_on s +* (Initialized I) by A7, A5, SCMFSA7B:def 8, A1;
A10: I c= P +* I by FUNCT_4:26;
A11: I . (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by A6, A10, GRFUNC_1:8
.= CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by A2, PARTFUN1:def 8
.= halt SCM+FSA by A9, EXTPRO_1:def 14 ;
IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) by A4, A7, Th44, COMPOS_1:24;
then A12: (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) = (Directed I) . (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by A8, FUNCT_4:14
.= (Directed I) . (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))))
.= goto (card I) by A6, A11, FUNCT_4:112 ;
A13: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I))))))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by A3, PARTFUN1:def 8;
A14: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I))))))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by A4, A7, Th44, A13, COMPOS_1:24
.= goto (card I) by A12 ;
A15: Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by EXTPRO_1:4
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I))))))) by A14 ;
hence IC (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) = card I by SCMFSA_2:95; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1)))
A16: ( ( for a being Int-Location holds (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) . a = (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) . f = (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) . f ) ) by A15, SCMFSA_2:95;
DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),(LifeSpan ((P +* I),(s +* (Initialized I)))))) by A4, A7, Th44, COMPOS_1:138;
hence DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialized (Directed I))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1))) by A16, SCMFSA6A:38; :: thesis: verum