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 N
for f being Instruction-Location of A
for I being Instruction of 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 N; :: thesis: for f being Instruction-Location of A
for I being Instruction of holds not f in Out_\_Inp I
let f be Instruction-Location of A; :: thesis: for I being Instruction of holds not f in Out_\_Inp I
let I be Instruction of ; :: thesis: not f in Out_\_Inp I
consider t being State of ;
consider J being set such that
A1: J in the Instructions of A and
A2: 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;
A3: dom t = the carrier of A by AMI_1:79;
A4: (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 A3, FUNCT_7:33 ;
hence not f in Out_\_Inp I by A2, A4, Def4; :: thesis: verum