let s1, s2 be State of SCMPDS; :: thesis: for I being Program of SCMPDS st I is_closed_on s1 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
set pI = stop I;
assume that
A1: I is_closed_on s1 and
A2: Initialize (stop I) c= s1 and
A3: Initialize (stop I) c= s2 and
A4: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A5: IC SCMPDS in dom (Initialize (stop I)) by COMPOS_1:def 16;
then A6: IC s1 = (Initialize (stop I)) . (IC SCMPDS) by A2, GRFUNC_1:8
.= IC s2 by A3, A5, GRFUNC_1:8 ;
defpred S₁[ Element of NAT ] means ( IC (Comput ((ProgramPart s1),s1,$1)) = IC (Comput ((ProgramPart s2),s2,$1)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,$1))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,$1))) & DataPart (Comput ((ProgramPart s1),s1,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) );
stop I c= Initialize (stop I) by COMPOS_1:126;
then A7: dom (stop I) c= dom (Initialize (stop I)) by GRFUNC_1:8;
I1: s1 +* (Initialize (stop I)) = (Initialize s1) +* (stop I) by COMPOS_1:125;
A8: s1 = (Initialize s1) +* (stop I) by A2, I1, FUNCT_4:79;
then IC (Comput ((ProgramPart s1),s1,0)) in dom (stop I) by A1, SCMPDS_6:def 2;
then A9: IC s1 in dom (stop I) by EXTPRO_1:3;
then A10: s1 . (IC s1) = (Initialize (stop I)) . (IC s1) by A2, A7, GRFUNC_1:8
.= s2 . (IC s2) by A3, A7, A9, A6, GRFUNC_1:8 ;
A11: DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart s2 by A4, EXTPRO_1:3
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ;
u: Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
v: Comput ((ProgramPart s2),s2,0) = s2 by EXTPRO_1:3;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
Z: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
A12: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,0))) = CurInstr ((ProgramPart s1),s1) by u
.= CurInstr ((ProgramPart s2),s2) by A10, Y, Z
.= CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,0))) by v ;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: S₁[k] ; :: thesis: S₁[k + 1]
set l = IC (Comput ((ProgramPart s1),s1,(k + 1)));
A15: IC (Comput ((ProgramPart s1),s1,(k + 1))) in dom (stop I) by A1, A8, SCMPDS_6:def 2;
set i = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)));
S: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
S1: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,(k + 1))) by AMI_1:123;
A16: Comput ((ProgramPart s1),s1,(k + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s1),s1,k))) by S ;
T1: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,(k + 1))) by AMI_1:123;
A17: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s2),s2,k))) by A14, S ;
hence IC (Comput ((ProgramPart s1),s1,(k + 1))) = IC (Comput ((ProgramPart s2),s2,(k + 1))) by A14, A16, Th23; :: thesis: ( CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + 1)))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
Y: (ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))) /. (IC (Comput ((ProgramPart s1),s1,(k + 1)))) = (Comput ((ProgramPart s1),s1,(k + 1))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))) /. (IC (Comput ((ProgramPart s2),s2,(k + 1)))) = (Comput ((ProgramPart s2),s2,(k + 1))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by COMPOS_1:38;
thus CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + 1)))) = s1 . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by Y, S1, AMI_1:54
.= (Initialize (stop I)) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by A2, A7, A15, GRFUNC_1:8
.= s2 . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by A3, A7, A15, GRFUNC_1:8
.= (Comput ((ProgramPart s2),s2,(k + 1))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by AMI_1:54
.= CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(k + 1)))) by A14, A16, A17, Th23, Z, T1 ; :: thesis: DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1)))
thus DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) by A14, A16, A17, Th23; :: thesis: verum

end;

IC (Comput ((ProgramPart s1),s1,0)) = IC s1 by EXTPRO_1:3
.= IC (Comput ((ProgramPart s2),s2,0)) by A6, EXTPRO_1:3 ;
then A18: S₁[ 0 ] by A12, A11;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A18, A13); :: thesis: verum