let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,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 N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,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 IL,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 A3: ( (IC S),loc --> l,h c= s1 & (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))
then A4: ( 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 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 & Computation s2,i = s2 ) 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 A4; :: thesis: verum

end;