let I, J be Program of SCMPDS ; :: thesis: for s being State of SCMPDS
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = CurInstr (ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)
let s be State of SCMPDS ; :: thesis: for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = CurInstr (ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)
let k be Element of NAT ; :: thesis: ( I is_closed_on s & I is_halting_on s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) implies CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = CurInstr (ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) )
set s1 = (Initialize s) +* (stop I);
set s2 = (Initialize s) +* (stop (I ';' J));
set s3 = Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k;
set s4 = Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k;
set SS = Stop SCMPDS ;
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by SCMPDS_4:5;
I2: s +* (Initialize (stop (I ';' J))) = (Initialize s) +* (stop (I ';' J)) by SCMPDS_4:5;
assume that
A1: I is_closed_on s and
A2: ( I is_halting_on s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) ) ; :: thesis: CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = CurInstr (ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)
A3: IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) in dom I by A1, A2, Th40;
A4: IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) by A1, A2, Th39;
A6: IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) in dom (stop I) by A1, Def2;
( Initialize (stop (I ';' J)) c= (Initialize s) +* (stop (I ';' J)) & stop (I ';' J) c= Initialize (stop (I ';' J)) ) by I2, FUNCT_4:26, SCMPDS_4:9;
then A7: ( dom (stop I) c= dom (stop (I ';' J)) & stop (I ';' J) c= (Initialize s) +* (stop (I ';' J)) ) by SCMPDS_5:16, XBOOLE_1:1;
( Initialize (stop I) c= (Initialize s) +* (stop I) & stop I c= Initialize (stop I) ) by I1, FUNCT_4:26, SCMPDS_4:9;
then A8: stop I c= (Initialize s) +* (stop I) by XBOOLE_1:1;
A9: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS )
.= I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46 ;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) = (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) by COMPOS_1:38;
TX: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) by AMI_1:123;
SX: ProgramPart ((Initialize s) +* (stop (I ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) by AMI_1:123;
thus CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = ((Initialize s) +* (stop I)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by Y, TX, AMI_1:54
.= (stop I) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by A6, A8, GRFUNC_1:8
.= I . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by A3, SCMPDS_4:37
.= (stop (I ';' J)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by A3, A9, SCMPDS_4:37
.= ((Initialize s) +* (stop (I ';' J))) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) by A4, A6, A7, GRFUNC_1:8
.= CurInstr (ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) by Z, SX, AMI_1:54 ; :: thesis: verum