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 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; 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; 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; 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; ( 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
; 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; ( 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
; 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; ( 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
; 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;
( S1[i] implies S1[i + 1] )
assume A7:
Comput (
P,
s,
i)
= DecIC (
(Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),
k)
;
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
;
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); verum