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: