let s be State of SCM+FSA; :: thesis:
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let I, J be Program of SCM+FSA; :: thesis:
A1: ProgramPart (Directed I) = Directed I by RELAT_1:209;
A2: dom (P +* (I ';' J)) = 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:
set s2 = s +* (Initialize ((intloc 0) .--> 1));
A5: ( s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) & s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) ) by Th13;
A6: (Directed I) ';' J = I ';' J by Th41;
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A7: I is_halting_on Initialized s,P ; :: thesis:
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by Th13;
then A8: (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 = pseudo-LifeSpan ((Initialized s),P,(Directed I)) by A4, A7, Lm2;
A9: Directed I is_pseudo-closed_on Initialized s,P by A4, A7, Lm2;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis:
then A10: k < pseudo-LifeSpan ((Initialized s),P,(Directed I)) by A8, NAT_1:13;
then NPP (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = NPP (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) by A5, A6, A9, Th32;
hence A11: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) by COMPOS_1:230; :: thesis:
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by Th13;
then A12: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom (Directed I) by A9, A10, Def5, A1;
A13: Directed I c= I ';' J by SCMFSA6A:55;
then B14: dom (Directed I) c= dom (I ';' J) by GRFUNC_1:8;
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A3, PARTFUN1:def 8
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A12, FUNCT_4:14
.= (I ';' J) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A12, A13, GRFUNC_1:8
.= (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A11, B14, FUNCT_4:14, A12
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A2, PARTFUN1:def 8 ; :: thesis:

end;

NPP (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = NPP (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A4, A7, A5, A6, A8, Lm2, Th32;
hence ( DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) by COMPOS_1:230, COMPOS_1:138; :: thesis: