theorem Th17: :: AMISTD_4:17

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds
IC in Out_U_Inp I