let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic
let IL be non empty set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N; :: thesis: for il being Instruction-Location of S
for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic
let il be Instruction-Location of S; :: thesis: for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic
let I be Element of the Instructions of S; :: thesis: for f being FinPartState of S st f = il .--> I holds
f is autonomic
let f be FinPartState of S; :: thesis: ( f = il .--> I implies f is autonomic )
assume A1: f = il .--> I ; :: thesis: f is autonomic
let s1, s2 be State of S; :: according to AMI_1:def 25 :: thesis: ( not f c= s1 or not f c= s2 or for b₁ being Element of NAT holds (Computation s1,b₁) | (dom f) = (Computation s2,b₁) | (dom f) )
assume that
A2: f c= s1 and
A3: f c= s2 ; :: thesis: for b₁ being Element of NAT holds (Computation s1,b₁) | (dom f) = (Computation s2,b₁) | (dom f)
let i be Element of NAT ; :: thesis: (Computation s1,i) | (dom f) = (Computation s2,i) | (dom f)
A4: dom f = {il} by A1, FUNCOP_1:19;
A5: for s being Function st f c= s holds
s . il = I

proof

let s be Function; :: thesis: ( f c= s implies s . il = I )
assume A6: f c= s ; :: thesis: s . il = I
il in {il} by TARSKI:def 1;
hence s . il = f . il by A4, A6, GRFUNC_1:8
.= I by A1, FUNCOP_1:87 ;
:: thesis: verum

end;

set a = (Computation s1,i) | (dom f);
set b = (Computation s2,i) | (dom f);
A7: {il} c= the carrier of S ;
then {il} c= dom (Computation s1,i) by AMI_1:79;
then A8: dom ((Computation s1,i) | (dom f)) = {il} by A4, RELAT_1:91;
{il} c= dom (Computation s2,i) by A7, AMI_1:79;
then A9: dom ((Computation s2,i) | (dom f)) = {il} by A4, RELAT_1:91;
for x being set st x in {il} holds
((Computation s1,i) | (dom f)) . x = ((Computation s2,i) | (dom f)) . x

proof

let x be set ; :: thesis: ( x in {il} implies ((Computation s1,i) | (dom f)) . x = ((Computation s2,i) | (dom f)) . x )
assume A10: x in {il} ; :: thesis: ((Computation s1,i) | (dom f)) . x = ((Computation s2,i) | (dom f)) . x
then A11: x = il by TARSKI:def 1;
thus ((Computation s1,i) | (dom f)) . x = (Computation s1,i) . x by A4, A10, FUNCT_1:72
.= I by A1, A2, A5, A11, AMI_1:81
.= (Computation s2,i) . x by A1, A3, A5, A11, AMI_1:81
.= ((Computation s2,i) | (dom f)) . x by A4, A10, FUNCT_1:72 ; :: thesis: verum

end;

hence (Computation s1,i) | (dom f) = (Computation s2,i) | (dom f) by A8, A9, FUNCT_1:9; :: thesis: verum