let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for l being Element of NAT
for P being NAT -defined the Instructions of b₁ -valued Function st l .--> (halt S) c= P holds
for p being b₂ -started PartState of S holds p +* P is autonomic
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N; :: thesis: for l being Element of NAT
for P being NAT -defined the Instructions of S -valued Function st l .--> (halt S) c= P holds
for p being b₁ -started PartState of S holds p +* P is autonomic
let l be Element of NAT ; :: thesis: for P being NAT -defined the Instructions of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S holds p +* P is autonomic
set h = halt S;
set p = Start-At (l,S);
let P be NAT -defined the Instructions of S -valued Function; :: thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p +* P is autonomic )
assume A1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S holds p +* P is autonomic
let p be l -started PartState of S; :: thesis: p +* P is autonomic
set I = p +* P;
let Q1, Q2 be the Instructions of S -valued ManySortedSet of NAT ; :: according to EXTPRO_1:def 9 :: thesis: ( ProgramPart (p +* P) c= Q1 & ProgramPart (p +* P) c= Q2 implies for s1, s2 being State of S st NPP (p +* P) c= s1 & NPP (p +* P) c= s2 holds
for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom (NPP (p +* P))) = (Comput (Q2,s2,i)) | (dom (NPP (p +* P))) )
assume A2: ( ProgramPart (p +* P) c= Q1 & ProgramPart (p +* P) c= Q2 ) ; :: thesis: for s1, s2 being State of S st NPP (p +* P) c= s1 & NPP (p +* P) c= s2 holds
for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom (NPP (p +* P))) = (Comput (Q2,s2,i)) | (dom (NPP (p +* P)))
let s1, s2 be State of S; :: thesis: ( NPP (p +* P) c= s1 & NPP (p +* P) c= s2 implies for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom (NPP (p +* P))) = (Comput (Q2,s2,i)) | (dom (NPP (p +* P))) )
assume that
A3: NPP (p +* P) c= s1 and
A4: NPP (p +* P) c= s2 ; :: thesis: for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom (NPP (p +* P))) = (Comput (Q2,s2,i)) | (dom (NPP (p +* P)))
let i be Element of NAT ; :: thesis: (Comput (Q1,s1,i)) | (dom (NPP (p +* P))) = (Comput (Q2,s2,i)) | (dom (NPP (p +* P)))
A5: P | NAT = P by RELAT_1:209;
A7: NPP (p +* P) c= s1 by A3;
A8: NPP (p +* P) c= s2 by A4;
P c= p +* P by FUNCT_4:26;
then P c= ProgramPart (p +* P) by A5, RELAT_1:105;
then ( P c= Q1 & P c= Q2 ) by A2, XBOOLE_1:1;
then A10: ( l .--> (halt S) c= Q1 & l .--> (halt S) c= Q2 ) by A1, XBOOLE_1:1;
hence (Comput (Q1,s1,i)) | (dom (NPP (p +* P))) = s1 | (dom (NPP (p +* P))) by A3, Th11
.= NPP (p +* P) by A7, GRFUNC_1:64
.= s2 | (dom (NPP (p +* P))) by A8, GRFUNC_1:64
.= (Comput (Q2,s2,i)) | (dom (NPP (p +* P))) by A4, Th11, A10 ;
:: thesis: verum