let N be with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for I being Instruction of A st I is sequential holds
IC A in Out_U_Inp I
let A be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for I being Instruction of A st I is sequential holds
IC A in Out_U_Inp I
let I be Instruction of A; :: thesis: ( I is sequential implies IC A in Out_U_Inp I )
assume A1: for s being State of A holds (Exec I,s) . (IC A) = NextLoc (IC s) ; :: according to AMISTD_1:def 16 :: thesis: IC A in Out_U_Inp I
consider s being State of A;
(Exec I,s) . (IC A) = NextLoc (IC s) by A1;
then (Exec I,s) . (IC A) <> IC s by AMISTD_1:35;
hence IC A in Out_U_Inp I by Th26; :: thesis: verum