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
not IC in Out_\_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
not IC in Out_\_Inp I
let I be Instruction of A; :: thesis: ( I is sequential implies not IC in Out_\_Inp I )
set t = the State of A;
set l = IC ;
reconsider sICt = (IC the State of A) + 1 as Element of NAT ;
reconsider w = sICt as Element of Values (IC ) by MEMSTR_0:def 6;
set s = the State of A +* ((IC ),w);
assume for s being State of A holds (Exec (I,s)) . (IC ) = (IC s) + 1 ; :: according to AMISTD_1:def 8 :: thesis: not IC in Out_\_Inp I
then A1: ( (Exec (I, the State of A)) . (IC ) = (IC the State of A) + 1 & (Exec (I,( the State of A +* ((IC ),w)))) . (IC ) = (IC ( the State of A +* ((IC ),w))) + 1 ) ;
dom the State of A = the carrier of A by PARTFUN1:def 2;
then ( the State of A +* ((IC ),w)) . (IC ) = w by FUNCT_7:31;
then Exec (I, the State of A) <> Exec (I,( the State of A +* ((IC ),w))) by A1, NAT_1:16;
hence not IC in Out_\_Inp I by Def4; :: thesis: verum