let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st ex s being State of A st (Exec I,s) . (IC A) <> IC s holds
IC A in Out_U_Inp I
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for I being Instruction of A st ex s being State of A st (Exec I,s) . (IC A) <> IC s holds
IC A in Out_U_Inp I
let I be Instruction of A; :: thesis: ( ex s being State of A st (Exec I,s) . (IC A) <> IC s implies IC A in Out_U_Inp I )
assume ex s being State of A st (Exec I,s) . (IC A) <> IC s ; :: thesis: IC A in Out_U_Inp I
then A1: IC A in Output I by Def3;
Output I c= Out_U_Inp I by Th11;
hence IC A in Out_U_Inp I by A1; :: thesis: verum