let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Nat
for P being NAT -defined the InstructionsF of b₁ -valued Function st l .--> (halt S) c= P holds
for p being b₂ -started PartState of S holds p is P -autonomic
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for l being Nat
for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being b₁ -started PartState of S holds p is P -autonomic
let l be Nat; :: thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S holds p is P -autonomic
set h = halt S;
set p = Start-At (l,S);
let P be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -autonomic )
assume A1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S holds p is P -autonomic
let p be l -started PartState of S; :: thesis: p is P -autonomic
set I = p +* P;
let Q1, Q2 be Instruction-Sequence of S; :: according to EXTPRO_1:def 10 :: thesis: ( P c= Q1 & P c= Q2 implies for s1, s2 being State of S st p c= s1 & p c= s2 holds
for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )
assume A2: ( P c= Q1 & P c= Q2 ) ; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds
for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)
let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )
assume that
A3: p c= s1 and
A4: p c= s2 ; :: thesis: for i being Nat holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)
let i be Nat; :: thesis: (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)
A5: ( l .--> (halt S) c= Q1 & l .--> (halt S) c= Q2 ) by A1, A2, XBOOLE_1:1;
hence (Comput (Q1,s1,i)) | (dom p) = s1 | (dom p) by A3, Th11
.= p by A3, GRFUNC_1:23
.= s2 | (dom p) by A4, GRFUNC_1:23
.= (Comput (Q2,s2,i)) | (dom p) by A4, Th11, A5 ;
:: thesis: verum