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_{1} -valued finite non halt-free Function

for p being b_{2} -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_{1} -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

for q being NAT -defined the InstructionsF of b

for p being b

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

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