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 A13, A17, COMPOS_1:def 21
.= (P +* (Reloc (q,k))) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A10, A16, GRFUNC_1:2
.= CurInstr ((P +* (Reloc (q,k))),(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A15, PARTFUN1:def 6 ;
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)) . (IC ) by A12, 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 A21, PARTFUN1:def 6
.= q . (IC (Comput (P,s,i))) by A7, A13, A14, A20, A5, A22, GRFUNC_1:2
.= (Shift (q,k)) . (IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i))) by A13, A14, A20, A7, A22, VALUED_1:def 12
.= (Shift (q,k)) /. kk by A13, A18, PARTFUN1:def 6 ;
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 A13, A19, 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 A7, A23 ; :: 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 A24, FUNCT_4:13;
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)) = {(IC )} ;
set PR = Reloc (q,k);
set SD = s | (dom (Reloc (q,k)));
A28: {(IC )} misses dom (DataPart p) by MEMSTR_0:4;
A29: dom (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) = {(IC )} ;
A30: dom (Start-At (((IC p) + k),S)) misses dom (DataPart p) by A28;
A31: (Start-At (((IC p) + k),S)) +* (DataPart p) = (DataPart p) +* (Start-At (((IC p) + k),S)) by A30, FUNCT_4:35
.= IncIC (p,k) by A1, MEMSTR_0:56 ;
Comput (P,s,0) = s +* (Start-At ((IC p),S)) by A3, A2, 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 A25, MEMSTR_0:53
.= (s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0))) -' k),S)) by A26, A3, 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 A29, A27, 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
.= DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),0)),k) by A31, A27, A28, FUNCT_4:35 ;
then A32: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A32, A6); :: thesis: verum