let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite steady-programmed with_non_trivial_Instructions AMI-Struct of N
for f being Element of NAT
for I being Instruction of A holds not f in Out_\_Inp I
let A be non empty stored-program IC-Ins-separated definite steady-programmed with_non_trivial_Instructions AMI-Struct of N; :: thesis: for f being Element of NAT
for I being Instruction of A holds not f in Out_\_Inp I
let f be Element of NAT ; :: 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 and
A2: t . f <> J by YELLOW15:4;
X: f in NAT ;
NAT c= the carrier of A by COMPOS_1:def 2;
then reconsider ff = f as Object of A by X;
reconsider J = J as Element of ObjectKind ff by A1, COMPOS_1:def 8;
reconsider s = t +* ff,J as State of A ;
A3: dom t = the carrier of A by PARTFUN1:def 4;
A4: (Exec I,t) . f = t . f by AMI_1:def 13;
(Exec I,s) . ff = s . ff by AMI_1:def 13
.= J by A3, FUNCT_7:33 ;
hence not f in Out_\_Inp I by A2, A4, Def4; :: thesis: verum