let s be State of SCM+FSA; :: thesis:
let I, J be Program of SCM+FSA; :: thesis:
assume A1: I is_closed_on s ; :: thesis:
set s2 = s +* ((I ';' J) +* (Start-At (0,SCM+FSA)));
A2: (Directed I) ';' J = I ';' J by Th41;
set s1 = s +* (I +* (Start-At (0,SCM+FSA)));
assume A3: I is_halting_on s ; :: thesis:
then A4: (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 = pseudo-LifeSpan (s,(Directed I)) by A1, Lm2;
A5: Directed I is_pseudo-closed_on s by A1, A3, Lm2;

hereby :: thesis:

A6: I ';' J c= (I ';' J) +* (Start-At (0,SCM+FSA)) by Th9;
then A7: dom (I ';' J) c= dom ((I ';' J) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
let k be Element of NAT ; :: thesis:
A8: Directed I c= (Directed I) +* (Start-At (0,SCM+FSA)) by Th9;
then A9: dom (Directed I) c= dom ((Directed I) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
assume k <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) ; :: thesis:
then A10: k < pseudo-LifeSpan (s,(Directed I)) by A4, NAT_1:13;
then A11: IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) in dom (Directed I) by A5, Def5;
thus A12: IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k)) by A2, A5, A10, Th32, COMPOS_1:24; :: thesis:
Y: (ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))) by COMPOS_1:38;
A13: Directed I c= I ';' J by SCMFSA6A:55;
then A14: dom (Directed I) c= dom (I ';' J) by GRFUNC_1:8;
then A15: IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) in dom (I ';' J) by A11;
thus CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) = (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by Y, AMI_1:54
.= ((Directed I) +* (Start-At (0,SCM+FSA))) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by A11, A9, FUNCT_4:14
.= (Directed I) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by A11, A8, GRFUNC_1:8
.= (I ';' J) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by A11, A13, GRFUNC_1:8
.= ((I ';' J) +* (Start-At (0,SCM+FSA))) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k))) by A11, A14, A6, GRFUNC_1:8
.= (s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))) by A12, A15, A7, FUNCT_4:14
.= CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),k))) by Z, AMI_1:54 ; :: thesis:

end;

Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1)), Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1)) equal_outside NAT by A1, A3, A2, A4, Lm2, Th32;
hence ( DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = DataPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) & IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) = IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1))) ) by COMPOS_1:24, SCMFSA6A:39; :: thesis: