let N be non empty with_non-empty_elements set ; :: thesis: for S being standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for k being Element of NAT
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
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let S be standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of N; :: thesis: ( S is CurIns-recognized implies for k being Element of NAT
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
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A1: S is CurIns-recognized ; :: thesis: for k being Element of NAT
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
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let k be Element of NAT ; :: 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
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
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
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let p be q -autonomic FinPartState of S; :: thesis: ( IC in dom p implies for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A2: IC in dom p ; :: thesis: for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
B2: IC in dom p by A2;
let s be State of S; :: thesis: ( IncIC (p,k) c= s implies for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A4: IncIC (p,k) c= s ; :: thesis: for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let P be Instruction-Sequence of S; :: thesis: ( Reloc (q,k) c= P implies for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A5: Reloc (q,k) c= P ; :: thesis: for i being Element of NAT holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
defpred S₁[ Element of NAT ] means Comput (P,s,$1) = IncIC ((Comput ((P +* q),(s +* p),$1)),k);
A6: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) ; :: thesis: S₁[i + 1]
reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Element of NAT ;
dom (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) = {(IC )} by FUNCOP_1:13;
then A8: IC in dom (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) by TARSKI:def 1;
A10: p c= s +* p by FUNCT_4:25;
A11: q c= P +* q by FUNCT_4:25;
not p is empty by A2;
then A12: IC (Comput ((P +* q),(s +* p),i)) in dom q by A1, Def4, A10, A11;
then A13: IC (Comput ((P +* q),(s +* p),i)) in dom (IncAddr (q,k)) by COMPOS_1:def 19;
A14: (IC (Comput ((P +* q),(s +* p),i))) + k in dom (Reloc (q,k)) by A12, COMPOS_1:46;
reconsider kk = IC (Comput ((P +* q),(s +* p),i)) as Element of NAT ;
A15: IC (Comput (P,s,i)) = IC (Comput (P,s,i))
.= IC (IncIC ((Comput ((P +* q),(s +* p),i)),k)) by A7
.= IC (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S)) by A8, FUNCT_4:13
.= (IC (Comput ((P +* q),(s +* p),i))) + k by FUNCOP_1:72 ;
A16: q c= P +* q by FUNCT_4:25;
A17: q /. kk = q . kk by A12, PARTFUN1:def 6;
A18: dom (P +* q) = NAT by PARTFUN1:def 2;
dom P = NAT by PARTFUN1:def 2;
then A19: CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PARTFUN1:def 6
.= (Reloc (q,k)) . (IC (Comput (P,s,i))) by A5, A14, A15, GRFUNC_1:2
.= (Shift ((IncAddr (q,k)),k)) . ((IC (Comput ((P +* q),(s +* p),i))) + k) by A15, COMPOS_1:34
.= (IncAddr (q,k)) . kk by A13, VALUED_1:def 12
.= IncAddr ((q /. kk),k) by A12, COMPOS_1:def 19
.= IncAddr (((P +* q) . (IC (Comput ((P +* q),(s +* p),i)))),k) by A12, A17, A16, GRFUNC_1:2
.= IncAddr ((CurInstr ((P +* q),(Comput ((P +* q),(s +* p),i)))),k) by A18, PARTFUN1:def 6 ;
thus Comput (P,s,(i + 1)) = Following (P,(Comput (P,s,i))) by EXTPRO_1:3
.= Exec ((IncAddr ((CurInstr ((P +* q),(Comput ((P +* q),(s +* p),i)))),k)),(IncIC ((Comput ((P +* q),(s +* p),i)),k))) by A7, A19
.= IncIC ((Following ((P +* q),(Comput ((P +* q),(s +* p),i)))),k) by Th4
.= IncIC ((Comput ((P +* q),(s +* p),(i + 1))),k) by EXTPRO_1:3 ; :: thesis: verum

end;

set IP = Start-At ((IC p),S);
A21: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:13;
B22: Start-At (((IC p) + k),S) c= IncIC (p,k) by MEMSTR_0:55;
B23: IC (Comput ((P +* q),(s +* p),0)) = (s +* p) . (IC ) by EXTPRO_1:2
.= IC p by B2, FUNCT_4:13
.= IC p ;
set DP = DataPart p;
DataPart (IncIC (p,k)) c= IncIC (p,k) by RELAT_1:59;
then DataPart (IncIC (p,k)) c= s by A4, XBOOLE_1:1;
then A29: DataPart p c= s by MEMSTR_0:51;
set PR = Reloc (q,k);
set IS = Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S);
A30: dom (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) = {(IC )} by FUNCOP_1:13;
Comput (P,s,0) = s by EXTPRO_1:2
.= s +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by B23, A4, B22, FUNCT_4:98, XBOOLE_1:1
.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A29, FUNCT_4:98
.= ((s +* (DataPart p)) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A30, A21, FUNCT_4:74
.= (s +* ((DataPart p) +* (Start-At ((IC p),S)))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by FUNCT_4:14
.= (s +* p) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) by A2, MEMSTR_0:26
.= IncIC ((Comput ((P +* q),(s +* p),0)),k) by EXTPRO_1:2 ;
then A31: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A31, A6); :: thesis: verum