let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF 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 non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N; :: thesis: for q being NAT -defined the InstructionsF 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 InstructionsF 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 A1: IC in dom p ; :: thesis: IC p in dom q
then A2: not p is empty ;
consider s being State of S such that
A3: p c= s by PBOOLE:141;
set P = the Instruction-Sequence of S +* q;
A4: 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 A4, Def4, A2, A3;
hence IC p in dom q by A3, A1, GRFUNC_1:2; :: thesis: verum