let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS
for n being Element of NAT st IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) = 0 holds
(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* (Initialized I) = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n
let I be Program of SCMPDS ; :: thesis: for n being Element of NAT st IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) = 0 holds
(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* (Initialized I) = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n
let n be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) = 0 implies (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* (Initialized I) = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n )
set II = Initialized I;
set sn = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n;
A1: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
I c= I +* (Start-At 0 ,SCMPDS ) by SCMPDS_6:6;
then I c= s +* (Initialized I) by A1, XBOOLE_1:1;
then A2: I c= Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n by AMI_1:81;
assume IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) = 0 ; :: thesis: (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* (Initialized I) = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n
then (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* (Initialized I) = (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* I by Th5;
hence (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) +* (Initialized I) = Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n by A2, FUNCT_4:79; :: thesis: verum