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 (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 (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, AMI_1:121; :: 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 AMI_1:150;
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 AMI_1:150;
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 AMI_1:54, Y
.= ((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 (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 (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 (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 (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 (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 (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) ) by AMI_1:121, SCMFSA6A:39; :: thesis: