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
not IC A in Out_\_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
not IC A in Out_\_Inp I
let I be Instruction of A; :: thesis: ( I is sequential implies not IC A in Out_\_Inp I )
consider t being State of A;
assume A1: for s being State of A holds (Exec I,s) . (IC A) = NextLoc (IC s) ; :: according to AMISTD_1:def 16 :: thesis: not IC A in Out_\_Inp I
set l = IC A;
NextLoc (IC t) in NAT by AMI_1:def 4;
then reconsider w = NextLoc (IC t) as Element of ObjectKind (IC A) by AMI_1:def 11;
set s = t +* (IC A),w;
A2: ( (Exec I,t) . (IC A) = NextLoc (IC t) & (Exec I,(t +* (IC A),w)) . (IC A) = NextLoc (IC (t +* (IC A),w)) ) by A1;
dom t = the carrier of A by AMI_1:79;
then Exec I,t <> Exec I,(t +* (IC A),w) by A2, AMISTD_1:35, FUNCT_7:33;
hence not IC A in Out_\_Inp I by Def4; :: thesis: verum