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 non empty FinPartState of S st IC in dom p holds
for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 non empty FinPartState of S st IC in dom p holds
for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 non empty FinPartState of S st IC in dom p holds
for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)

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

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

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

then A2: Start-At ((IC p),S) c= p by FUNCOP_1:84;
let s be State of S; :: thesis: ( p c= s & IncIC (p,k) is Reloc (q,k) -autonomic implies for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) )

assume that
A3: p c= s and
A4: IncIC (p,k) is Reloc (q,k) -autonomic ; :: thesis: for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)

let P be Instruction-Sequence of S; :: thesis: ( q c= P implies for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) )
assume A5: q c= P ; :: thesis: for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
defpred S1[ Nat] means Comput (P,s,\$1) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),\$1)),k);
A6: for i being Nat st S1[i] holds
S1[i + 1]
proof
reconsider pp = q as preProgram of S ;
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A7: Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) ; :: thesis: S1[i + 1]
reconsider kk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Nat ;
reconsider jk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Nat ;
A8: IncIC (p,k) c= s +* (IncIC (p,k)) by FUNCT_4:25;
A9: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;
A10: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) in dom (Reloc (q,k)) by A4, Def4, A8, A9;
then A11: jk in { (j + k) where j is Nat : j in dom q } by COMPOS_1:33;
A12: IC in dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k),S)) by TARSKI:def 1;
consider j being Nat such that
A13: jk = j + k and
A14: j in dom q by A11;
A15: dom (P +* (Reloc (q,k))) = NAT by PARTFUN1:def 2;
A16: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;
A17: Reloc (q,k) = IncAddr ((Shift (q,k)),k) by COMPOS_1:34;
dom (Shift (pp,k)) = { (m + k) where m is Nat : m in dom pp } by VALUED_1:def 12;
then A18: j + k in dom (Shift (q,k)) by A14;
then A19: IncAddr (((Shift (q,k)) /. kk),k) = (Reloc (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by
.= (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by
.= CurInstr ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by ;
A20: (j + k) -' k = j by NAT_D:34;
A21: dom P = NAT by PARTFUN1:def 2;
A22: IC (DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)) = (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k),S)) . () by
.= (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k by FUNCOP_1:72 ;
CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by
.= q . (IC (Comput (P,s,i))) by
.= (Shift (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by
.= (Shift (q,k)) /. kk by ;
then A23: ( 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))) & Exec ((CurInstr (P,(Comput (P,s,i)))),(DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k))) = DecIC ((Following ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)))),k) ) by ;
thus Comput (P,s,(i + 1)) = Following (P,(Comput (P,s,i))) by EXTPRO_1:3
.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),(i + 1))),k) by ; :: thesis: verum
end;
A24: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A25: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)) = IC (IncIC (p,k)) by ;
A26: DataPart p c= p by RELAT_1:59;
set DP = DataPart p;
set IP = Start-At (((IC p) + k),S);
set PP = q;
set IS = Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S);
A27: dom (Start-At (((IC p) + k),S)) = {()} ;
set PR = Reloc (q,k);
set SD = s | (dom (Reloc (q,k)));
A28: {()} misses dom () by MEMSTR_0:4;
A29: dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) = {()} ;
A30: dom (Start-At (((IC p) + k),S)) misses dom () by A28;
A31: (Start-At (((IC p) + k),S)) +* () = () +* (Start-At (((IC p) + k),S)) by
.= IncIC (p,k) by ;
Comput (P,s,0) = s +* (Start-At ((IC p),S)) by
.= s +* (Start-At ((((IC p) + k) -' k),S)) by NAT_D:34
.= s +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by
.= (s +* ()) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by
.= ((s +* ()) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by
.= (s +* (() +* (Start-At (((IC p) + k),S)))) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by FUNCT_4:14
.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)),k) by ;
then A32: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A32, A6); :: thesis: verum