let N be non empty with_non-empty_elements set ; :: thesis: for S being standard-ins non empty IC-Ins-separated halting IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for q being NAT -defined the Instructions of b₁ -valued finite non halt-free Function
for p being b₂ -autonomic FinPartState of S st IC in dom p holds
IC p in dom q
let S be standard-ins non empty IC-Ins-separated halting IC-recognized AMI-Struct of N; :: thesis: ( S is CurIns-recognized implies for q being NAT -defined the Instructions of S -valued finite non halt-free Function
for p being b₁ -autonomic FinPartState of S st IC in dom p holds
IC p in dom q )
assume A1: S is CurIns-recognized ; :: thesis: for q being NAT -defined the Instructions of S -valued finite non halt-free Function
for p being b₁ -autonomic FinPartState of S st IC in dom p holds
IC p in dom q
let q be NAT -defined the Instructions of S -valued finite non halt-free Function; :: thesis: for p being q -autonomic FinPartState of S st IC in dom p holds
IC p in dom q
let p be q -autonomic FinPartState of S; :: thesis: ( IC in dom p implies IC p in dom q )
assume A2: IC in dom p ; :: thesis: IC p in dom q
then B2: not p is empty ;
consider s being State of S such that
A4: p c= s by PBOOLE:141;
B4: p c= s by A4;
set P = the Instruction-Sequence of S +* q;
A5: q c= the Instruction-Sequence of S +* q by FUNCT_4:25;
IC (Comput (( the Instruction-Sequence of S +* q),s,0)) in dom q by A5, A1, Def4, B4, B2;
then IC s in dom q by EXTPRO_1:2;
hence IC p in dom q by A4, A2, GRFUNC_1:2; :: thesis: verum