let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is autonomic
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is autonomic
let loc be Instruction-Location of S; :: thesis: for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is autonomic
let l be Element of ObjectKind (IC S); :: thesis: ( l = loc implies for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is autonomic )
assume A1: l = loc ; :: thesis: for h being Element of ObjectKind loc st h = halt S holds
(IC S),loc --> l,h is autonomic
let h be Element of ObjectKind loc; :: thesis: ( h = halt S implies (IC S),loc --> l,h is autonomic )
assume A2: h = halt S ; :: thesis: (IC S),loc --> l,h is autonomic
thus (IC S),loc --> l,h is autonomic :: thesis: verum

proof

let s1, s2 be State of S; :: according to AMI_1:def 25 :: thesis: ( (IC S),loc --> l,h c= s1 & (IC S),loc --> l,h c= s2 implies for i being Element of NAT holds (Computation s1,i) | (dom ((IC S),loc --> l,h)) = (Computation s2,i) | (dom ((IC S),loc --> l,h)) )
assume that
A3: (IC S),loc --> l,h c= s1 and
A4: (IC S),loc --> l,h c= s2 ; :: thesis: for i being Element of NAT holds (Computation s1,i) | (dom ((IC S),loc --> l,h)) = (Computation s2,i) | (dom ((IC S),loc --> l,h))
A5: ( s1 | (dom ((IC S),loc --> l,h)) = (IC S),loc --> l,h & s2 | (dom ((IC S),loc --> l,h)) = (IC S),loc --> l,h ) by A3, A4, GRFUNC_1:64;
let i be Element of NAT ; :: thesis: (Computation s1,i) | (dom ((IC S),loc --> l,h)) = (Computation s2,i) | (dom ((IC S),loc --> l,h))
Computation s1,i = s1 by A1, A2, A3, Th66;
hence (Computation s1,i) | (dom ((IC S),loc --> l,h)) = (Computation s2,i) | (dom ((IC S),loc --> l,h)) by A1, A2, A4, A5, Th66; :: thesis: verum

end;