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

hereby :: thesis:

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

end;

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