let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N
for k being Nat
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being b3 -autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N; :: thesis: for k being Nat
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b2 -autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

let k be Nat; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

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
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

let p be q -autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) )

assume A1: IC in dom p ; :: thesis: for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

let s be State of S; :: thesis: ( p c= s implies for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) )

assume A2: p c= s ; :: thesis: for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

let P be Instruction-Sequence of S; :: thesis: ( q c= P implies for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) )
assume A3: q c= P ; :: thesis: for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)
defpred S1[ Nat] means Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),\$1) = IncIC ((Comput (P,s,\$1)),k);
A4: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k) ; :: thesis: S1[i + 1]
reconsider kk = IC (Comput (P,s,i)) as Nat ;
A6: IC in dom (Start-At (((IC (Comput (P,s,i))) + k),S)) by TARSKI:def 1;
A7: IC (IncIC ((Comput (P,s,i)),k)) = IC (Start-At (((IC (Comput (P,s,i))) + k),S)) by
.= (IC (Comput (P,s,i))) + k by FUNCOP_1:72 ;
not p is empty by A1;
then A8: IC (Comput (P,s,i)) in dom q by A3, Def4, A2;
then A9: IC (Comput (P,s,i)) in dom (IncAddr (q,k)) by COMPOS_1:def 21;
A10: q /. kk = q . (IC (Comput (P,s,i))) by
.= P . (IC (Comput (P,s,i))) by ;
reconsider kk = IC (Comput (P,s,i)) as Nat ;
A11: (IC (Comput (P,s,i))) + k in dom (Reloc (q,k)) by ;
A12: CurInstr ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) = (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by PBOOLE:143
.= (Reloc (q,k)) . ((IC (Comput (P,s,i))) + k) by
.= (IncAddr (q,k)) . kk by
.= IncAddr ((q /. kk),k) by
.= IncAddr ((CurInstr (P,(Comput (P,s,i)))),k) by ;
thus Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),(i + 1)) = Following ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by EXTPRO_1:3
.= IncIC ((Following (P,(Comput (P,s,i)))),k) by A5, A12, Th4
.= IncIC ((Comput (P,s,(i + 1))),k) by EXTPRO_1:3 ; :: thesis: verum
end;
A13: IC p = IC s by ;
A14: DataPart p c= p by MEMSTR_0:12;
Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0) = s +* (() +* (Start-At (((IC p) + k),S))) by
.= (s +* ()) +* (Start-At (((IC p) + k),S)) by FUNCT_4:14
.= IncIC ((Comput (P,s,0)),k) by ;
then A15: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A15, A4); :: thesis: verum