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 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),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 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
let q be NAT -defined the Instructions 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 Element of 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) )
assume A3: 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
then B4: 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) )
assume that
A5: p c= s and
A6: IncIC (p,k) is Reloc (q,k) -autonomic ; :: thesis: for P being Instruction-Sequence of S st q c= P holds
for i being Element of 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 Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k) )
assume A7: q c= P ; :: thesis: for i being Element of NAT holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)
defpred S1[ Element of NAT ] means Comput (P,s,$1) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),$1)),k);
A9: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp = q as preProgram of S ;
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A10: 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 Element of NAT ;
reconsider jk = IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) as Element of NAT ;
A11: IncIC (p,k) c= s +* (IncIC (p,k)) by FUNCT_4:25;
A12: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;
A13: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)) in dom (Reloc (q,k)) by A6, A1, Def4, A11, A12;
then A14: jk in { (j + k) where j is Element of NAT : j in dom q } by COMPOS_1:33;
dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) -' k),S)) = {(IC )} by FUNCOP_1:13;
then A16: 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 Element of NAT such that
A17: jk = j + k and
A18: j in dom q by A14;
A19: dom (P +* (Reloc (q,k))) = NAT by PARTFUN1:def 2;
A20: Reloc (q,k) c= P +* (Reloc (q,k)) by FUNCT_4:25;
dom (Shift (pp,k)) = { (m + k) where m is Element of NAT : m in dom pp } by VALUED_1:def 12;
then A21: j + k in dom (Shift (q,k)) by A18;
then A22: IncAddr (((Shift (q,k)) /. kk),k) = (Reloc (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A17, COMPOS_1:def 19
.= (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A13, A20, GRFUNC_1:2
.= CurInstr ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A19, PARTFUN1:def 6 ;
A23: (j + k) -' k = j by NAT_D:34;
A24: dom P = NAT by PARTFUN1:def 2;
A25: 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)) . (IC ) by A16, FUNCT_4:13
.= (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 A24, PARTFUN1:def 6
.= q . (IC (Comput (P,s,i))) by A10, A17, A18, A23, A7, A25, GRFUNC_1:2
.= (Shift (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A17, A18, A23, A10, A25, VALUED_1:def 12
.= (Shift (q,k)) /. kk by A17, A21, PARTFUN1:def 6 ;
then A26: ( 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 A17, A22, Th5, EXTPRO_1:3;
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 A10, A26 ; :: thesis: verum
end;
B27: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A28: IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)) = IC (s +* (IncIC (p,k))) by EXTPRO_1:2
.= IC (IncIC (p,k)) by B27, FUNCT_4:13 ;
B29: 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);
A32: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13;
set PR = Reloc (q,k);
set SD = s | (dom (Reloc (q,k)));
A33: {(IC )} misses dom (DataPart p) by MEMSTR_0:4;
A36: dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) = {(IC )} by FUNCOP_1:13;
A41: dom (Start-At (((IC p) + k),S)) misses dom (DataPart p) by A33, FUNCOP_1:13;
A42: (Start-At (((IC p) + k),S)) +* (DataPart p) = (DataPart p) +* (Start-At (((IC p) + k),S)) by A41, FUNCT_4:35
.= IncIC (p,k) by A3, MEMSTR_0:56
.= IncIC (p,k) ;
Comput (P,s,0) = s by EXTPRO_1:2
.= s +* (Start-At ((IC p),S)) by A5, B4, FUNCT_4:98, XBOOLE_1:1
.= 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 A28, MEMSTR_0:53
.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by B29, A5, FUNCT_4:98, XBOOLE_1:1
.= ((s +* (DataPart p)) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A36, A32, FUNCT_4:74
.= (s +* ((DataPart p) +* (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
.= (s +* ((Start-At (((IC p) + k),S)) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A32, A33, FUNCT_4:35
.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)),k) by A42, EXTPRO_1:2 ;
then A43: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A43, A9); :: thesis: verum