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

proof

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

end;

A7: 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 A8: x in {il} ; :: thesis: ((Computation s1,i) | (dom f)) . x = ((Computation s2,i) | (dom f)) . x
then A9: x = il by TARSKI:def 1;
thus ((Computation s1,i) | (dom f)) . x = (Computation s1,i) . x by A2, A8, FUNCT_1:72
.= I by A1, A3, A5, A9, AMI_1:81
.= (Computation s2,i) . x by A1, A4, A5, A9, AMI_1:81
.= ((Computation s2,i) | (dom f)) . x by A2, A8, FUNCT_1:72 ; :: thesis: verum

end;

A10: {il} c= the carrier of S ;
then {il} c= dom (Computation s2,i) by AMI_1:79;
then A11: dom ((Computation s2,i) | (dom f)) = {il} by A2, RELAT_1:91;
{il} c= dom (Computation s1,i) by A10, AMI_1:79;
then dom ((Computation s1,i) | (dom f)) = {il} by A2, RELAT_1:91;
hence (Computation s1,i) | (dom f) = (Computation s2,i) | (dom f) by A11, A7, FUNCT_1:9; :: thesis: verum