let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for l being Nat
for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is autonomic
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N; :: thesis: for l being Nat
for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is autonomic
let l be Nat; :: thesis: for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is autonomic
set h = halt S;
let p be PartState of S; :: thesis: ( p = (IC S),l --> l,(halt S) implies p is autonomic )
assume Z: p = (IC S),l --> l,(halt S) ; :: thesis: p is autonomic
let s1, s2 be State of S; :: according to AMI_1:def 25 :: thesis: ( p c= s1 & p c= s2 implies for i being Element of NAT holds (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s2),s2,i) | (dom p) )
assume that
A3: p c= s1 and
A4: p c= s2 ; :: thesis: for i being Element of NAT holds (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s2),s2,i) | (dom p)
A5: ( s1 | (dom ((IC S),l --> l,(halt S))) = (IC S),l --> l,(halt S) & s2 | (dom ((IC S),l --> l,(halt S))) = (IC S),l --> l,(halt S) ) by Z, A3, A4, GRFUNC_1:64;
let i be Element of NAT ; :: thesis: (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s2),s2,i) | (dom p)
Comput (ProgramPart s1),s1,i = s1 by Z, A3, Th66;
hence (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s2),s2,i) | (dom p) by Z, A4, A5, Th66; :: thesis: verum