let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of 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 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;
set l = IC A;
reconsider sICt = succ (IC t) as Element of NAT ;
reconsider w = sICt as Element of ObjectKind (IC A) by COMPOS_1:def 6;
set s = t +* ((IC A),w);
assume for s being State of A holds (Exec (I,s)) . (IC A) = succ (IC s) ; :: according to AMISTD_1:def 16 :: thesis: not IC A in Out_\_Inp I
then A1: ( (Exec (I,t)) . (IC A) = succ (IC t) & (Exec (I,(t +* ((IC A),w)))) . (IC A) = succ (IC (t +* ((IC A),w))) ) ;
dom t = the carrier of A by PARTFUN1:def 4;
then Exec (I,t) <> Exec (I,(t +* ((IC A),w))) by A1, FUNCT_7:33, ORDINAL1:14;
hence not IC A in Out_\_Inp I by Def4; :: thesis: verum