let N be non empty 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 Element of NAT
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 N; :: thesis: for il being Element of NAT
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 Element of NAT ; :: 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
A2: dom f = {il} by A1, FUNCOP_1:19;
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 (Comput (ProgramPart s1),s1,b₁) | (proj1 f) = (Comput (ProgramPart s2),s2,b₁) | (proj1 f) )
assume that
A3: f c= s1 and
A4: f c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 f) = (Comput (ProgramPart s2),s2,b₁) | (proj1 f)
let i be Element of NAT ; :: thesis: (Comput (ProgramPart s1),s1,i) | (proj1 f) = (Comput (ProgramPart s2),s2,i) | (proj1 f)
set a = (Comput (ProgramPart s1),s1,i) | (dom f);
set b = (Comput (ProgramPart s2),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
((Comput (ProgramPart s1),s1,i) | (dom f)) . x = ((Comput (ProgramPart s2),s2,i) | (dom f)) . x

proof

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

end;

X: il in NAT ;
NAT c= the carrier of S by AMI_1:def 3;
then il in the carrier of S by X;
then A10: {il} c= the carrier of S by ZFMISC_1:37;
then {il} c= dom (Comput (ProgramPart s2),s2,i) by PARTFUN1:def 4;
then A11: dom ((Comput (ProgramPart s2),s2,i) | (dom f)) = {il} by A2, RELAT_1:91;
{il} c= dom (Comput (ProgramPart s1),s1,i) by A10, PARTFUN1:def 4;
then dom ((Comput (ProgramPart s1),s1,i) | (dom f)) = {il} by A2, RELAT_1:91;
hence (Comput (ProgramPart s1),s1,i) | (dom f) = (Comput (ProgramPart s2),s2,i) | (dom f) by A11, A7, FUNCT_1:9; :: thesis: verum