let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan ((P +* I),(Initialize s));
A2: dom (P +* I) = NAT by PARTFUN1:def 2;
A3: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
assume that
A4: I is_closed_on s,P and
A5: I is_halting_on s,P ; :: thesis: ( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
A6: P +* I halts_on Initialize s by A5, SCMFSA7B:def 7;
set l1 = IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))));
A7: IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I by A4, SCMFSA7B:def 6;
B8: Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) = Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) by A4, A5, Th35;
then IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I by A7;
then A8: IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom (Directed I) by FUNCT_4:99;
I c= P +* I by FUNCT_4:25;
then A9: I . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A7, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A2, PARTFUN1:def 6
.= halt SCM+FSA by A6, EXTPRO_1:def 15 ;
IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) by B8;
then A10: (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (Directed I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A8, FUNCT_4:13
.= goto (card I) by A7, A9, FUNCT_4:106 ;
A11: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A3, PARTFUN1:def 6
.= goto (card I) by A10, B8 ;
A12: Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A11 ;
hence IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I by SCMFSA_2:69; :: thesis: DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))
A13: ( ( for a being Int-Location holds (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a = (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f = (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) . f ) ) by A12, SCMFSA_2:69;
DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) by B8;
hence DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A13, SCMFSA6A:7; :: thesis: verum