let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of A st I is sequential holds
IC in Out_U_Inp I
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; :: thesis: for I being Instruction of A st I is sequential holds
IC in Out_U_Inp I
let I be Instruction of A; :: thesis: ( I is sequential implies IC in Out_U_Inp I )
set s = the State of A;
assume for s being State of A holds (Exec (I,s)) . (IC ) = (IC s) + 1 ; :: according to AMISTD_1:def 8 :: thesis: IC in Out_U_Inp I
then (Exec (I, the State of A)) . (IC ) = (IC the State of A) + 1 ;
then (Exec (I, the State of A)) . (IC ) <> IC the State of A by NAT_1:16;
hence IC in Out_U_Inp I by Th17; :: thesis: verum