let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for f being Element of NAT
for I being Instruction of A st ( for s being State of A
for p being NAT -defined FinPartState of holds Exec (I,(s +* p)) = (Exec (I,s)) +* p ) holds
not f in Out_U_Inp I
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for f being Element of NAT
for I being Instruction of A st ( for s being State of A
for p being NAT -defined FinPartState of holds Exec (I,(s +* p)) = (Exec (I,s)) +* p ) holds
not f in Out_U_Inp I
let f be Element of NAT ; :: thesis: for I being Instruction of A st ( for s being State of A
for p being NAT -defined FinPartState of holds Exec (I,(s +* p)) = (Exec (I,s)) +* p ) holds
not f in Out_U_Inp I
let I be Instruction of A; :: thesis: ( ( for s being State of A
for p being NAT -defined FinPartState of holds Exec (I,(s +* p)) = (Exec (I,s)) +* p ) implies not f in Out_U_Inp I )
assume A1: for s being State of A
for p being NAT -defined FinPartState of holds Exec (I,(s +* p)) = (Exec (I,s)) +* p ; :: thesis: not f in Out_U_Inp I
assume Z: f in Out_U_Inp I ; :: thesis: contradiction
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;
consider s being State of A, w being Element of ObjectKind ff such that
A2: Exec (I,(s +* (ff,w))) <> (Exec (I,s)) +* (ff,w) by Z, Def5;
set p = ff .--> w;
( f in NAT & dom (ff .--> w) = {f} ) by FUNCOP_1:19;
then dom (ff .--> w) c= NAT by ZFMISC_1:37;
then reconsider p = ff .--> w as NAT -defined FinPartState of ;
dom s = the carrier of A by PARTFUN1:def 4;
then A3: ( dom (Exec (I,s)) = the carrier of A & s +* (f,w) = s +* p ) by FUNCT_7:def 3, PARTFUN1:def 4;
Exec (I,(s +* p)) = (Exec (I,s)) +* p by A1;
hence contradiction by A2, A3, FUNCT_7:def 3; :: thesis: verum