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