let N be with_zero set ; 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 IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let S be 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 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 IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let k be Nat; 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 IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; 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 Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let p be q -autonomic FinPartState of S; ( 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 Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A1:
IC in dom p
; 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 Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let s be State of S; ( IncIC (p,k) c= s implies for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A2:
IncIC (p,k) c= s
; for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
let P be Instruction-Sequence of S; ( Reloc (q,k) c= P implies for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k) )
assume A3:
Reloc (q,k) c= P
; for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)
defpred S1[ Nat] means Comput (P,s,$1) = IncIC ((Comput ((P +* q),(s +* p),$1)),k);
A4:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A5:
Comput (
P,
s,
i)
= IncIC (
(Comput ((P +* q),(s +* p),i)),
k)
;
S1[i + 1]
reconsider kk =
IC (Comput ((P +* q),(s +* p),i)) as
Nat ;
A6:
IC in dom (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S))
by TARSKI:def 1;
A7:
p c= s +* p
by FUNCT_4:25;
A8:
q c= P +* q
by FUNCT_4:25;
not
p is
empty
by A1;
then A9:
IC (Comput ((P +* q),(s +* p),i)) in dom q
by Def4, A7, A8;
then A10:
IC (Comput ((P +* q),(s +* p),i)) in dom (IncAddr (q,k))
by COMPOS_1:def 21;
A11:
(IC (Comput ((P +* q),(s +* p),i))) + k in dom (Reloc (q,k))
by A9, COMPOS_1:46;
reconsider kk =
IC (Comput ((P +* q),(s +* p),i)) as
Nat ;
A12:
IC (Comput (P,s,i)) =
IC (Start-At (((IC (Comput ((P +* q),(s +* p),i))) + k),S))
by A5, A6, FUNCT_4:13
.=
(IC (Comput ((P +* q),(s +* p),i))) + k
by FUNCOP_1:72
;
A13:
q c= P +* q
by FUNCT_4:25;
A14:
q /. kk = q . kk
by A9, PARTFUN1:def 6;
A15:
dom (P +* q) = NAT
by PARTFUN1:def 2;
dom P = NAT
by PARTFUN1:def 2;
then A16:
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 A3, A11, A12, GRFUNC_1:2
.=
(IncAddr (q,k)) . kk
by A10, A12, VALUED_1:def 12
.=
IncAddr (
(q /. kk),
k)
by A9, COMPOS_1:def 21
.=
IncAddr (
((P +* q) . (IC (Comput ((P +* q),(s +* p),i)))),
k)
by A9, A14, A13, GRFUNC_1:2
.=
IncAddr (
(CurInstr ((P +* q),(Comput ((P +* q),(s +* p),i)))),
k)
by A15, PARTFUN1:def 6
;
thus Comput (
P,
s,
(i + 1)) =
Following (
P,
(Comput (P,s,i)))
by EXTPRO_1:3
.=
IncIC (
(Following ((P +* q),(Comput ((P +* q),(s +* p),i)))),
k)
by A5, A16, Th4
.=
IncIC (
(Comput ((P +* q),(s +* p),(i + 1))),
k)
by EXTPRO_1:3
;
verum
end;
set IP = Start-At ((IC p),S);
A17:
dom (Start-At ((IC p),S)) = {(IC )}
;
A18:
Start-At (((IC p) + k),S) c= IncIC (p,k)
by MEMSTR_0:55;
A19:
IC (Comput ((P +* q),(s +* p),0)) = IC p
by A1, FUNCT_4:13;
set DP = DataPart p;
DataPart (IncIC (p,k)) c= IncIC (p,k)
by RELAT_1:59;
then
DataPart (IncIC (p,k)) c= s
by A2, XBOOLE_1:1;
then A20:
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);
A21:
dom (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S)) = {(IC )}
;
Comput (P,s,0) =
s +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S))
by A19, A2, A18, FUNCT_4:98, XBOOLE_1:1
.=
(s +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S))
by A20, FUNCT_4:98
.=
((s +* (DataPart p)) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* q),(s +* p),0))) + k),S))
by A21, A17, 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
.=
IncIC ((Comput ((P +* q),(s +* p),0)),k)
by A1, MEMSTR_0:26
;
then A22:
S1[ 0 ]
;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A22, A4); verum