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 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 4;
A3: dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
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 8;
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 7;
B8: NPP (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = NPP (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 COMPOS_1:230, A7;
then A8: IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom (Directed I) by FUNCT_4:105;
I c= P +* I by FUNCT_4:26;
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 GRFUNC_1:8, A7
.= CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A2, PARTFUN1:def 8
.= halt SCM+FSA by A6, EXTPRO_1:def 14 ;
IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) by COMPOS_1:230, 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:14
.= goto (card I) by A7, A9, FUNCT_4:112 ;
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 8
.= goto (card I) by A10, COMPOS_1:230, 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:4
.= 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:95; :: 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:95;
DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) by COMPOS_1:138, 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:38; :: thesis: verum