let N be with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated steady-programmed definite with_non_trivial_Instructions AMI-Struct of NAT ,N
for f being Instruction-Location of A
for I being Instruction of A holds not f in Out_\_Inp I
let A be non empty stored-program IC-Ins-separated steady-programmed definite with_non_trivial_Instructions AMI-Struct of NAT ,N; :: thesis: for f being Instruction-Location of A
for I being Instruction of A holds not f in Out_\_Inp I
let f be Instruction-Location of A; :: thesis: for I being Instruction of A holds not f in Out_\_Inp I
let I be Instruction of A; :: thesis: not f in Out_\_Inp I
consider t being State of A;
consider J being set such that
A1: ( J in the Instructions of A & t . f <> J ) by YELLOW15:4;
reconsider J = J as Element of ObjectKind f by A1, AMI_1:def 14;
set s = t +* f,J;
A2: dom t = the carrier of A by AMI_1:79;
A3: (Exec I,t) . f = t . f by AMI_1:def 13;
(Exec I,(t +* f,J)) . f = (t +* f,J) . f by AMI_1:def 13
.= J by A2, FUNCT_7:33 ;
hence not f in Out_\_Inp I by A1, A3, Def4; :: thesis: verum