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