let s1, s2 be State of SCMPDS; :: thesis: for I being Program of SCMPDS st I is_closed_on s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT & CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds
( Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT & CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) ) )
assume A1: I is_closed_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Element of NAT holds
( Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT & CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) ) )
set pI = stop I;
set ss1 = (Initialize s1) +* (stop I);
set ss2 = (Initialize s2) +* (stop I);
I1: (Initialize s1) +* (stop I) = s1 +* (Initialize (stop I)) by COMPOS_1:125;
I2: (Initialize s2) +* (stop I) = s2 +* (Initialize (stop I)) by COMPOS_1:125;
A2: stop I c= Initialize (stop I) by COMPOS_1:126;
Initialize (stop I) c= (Initialize s2) +* (stop I) by I2, FUNCT_4:26;
then A3: stop I c= (Initialize s2) +* (stop I) by A2, XBOOLE_1:1;
Initialize (stop I) c= (Initialize s1) +* (stop I) by I1, FUNCT_4:26;
then A4: stop I c= (Initialize s1) +* (stop I) by A2, XBOOLE_1:1;
assume A5: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds
( Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT & CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) )
let k be Element of NAT ; :: thesis: ( Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT & CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) )
A6: IC (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)) in dom (stop I) by A1, SCMPDS_6:def 2;
A7: I is_closed_on s2 by A1, A5, SCMPDS_6:36;
then A8: for m being Element of NAT st m < k holds
IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),m)) in dom (stop I) by SCMPDS_6:def 2;
(Initialize s1) +* (stop I),(Initialize s2) +* (stop I) equal_outside NAT by A5, SCMPDS_6:12;
hence Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k), Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) equal_outside NAT by A4, A3, A8, SCMPDS_4:67; :: thesis: CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)))
then A9: IC (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)) = IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)) by COMPOS_1:24;
A10: IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)) in dom (stop I) by A7, SCMPDS_6:def 2;
Y: (ProgramPart (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) /. (IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) = (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)) . (IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) /. (IC (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) = (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)) . (IC (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) by COMPOS_1:38;
TX2: ProgramPart ((Initialize s2) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)) by AMI_1:123;
TX1: ProgramPart ((Initialize s1) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)) by AMI_1:123;
thus CurInstr ((ProgramPart ((Initialize s2) +* (stop I))),(Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) = ((Initialize s2) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) by Y, TX2, AMI_1:54
.= (stop I) . (IC (Comput ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k))) by A3, A10, GRFUNC_1:8
.= ((Initialize s1) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) by A4, A9, A6, GRFUNC_1:8
.= CurInstr ((ProgramPart ((Initialize s1) +* (stop I))),(Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k))) by Z, TX1, AMI_1:54 ; :: thesis: verum