let INS be Instruction of (SCM R); AMISTD_5:def 2 INS is relocable
let j, k be Nat; AMISTD_5:def 1 for b1 being set holds Exec ((IncAddr (INS,(j + k))),(IncIC (b1,k))) = IncIC ((Exec ((IncAddr (INS,j)),b1)),k)
reconsider k = k as Element of NAT by ORDINAL1:def 12;
let s be State of (SCM R); Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
A1: IC (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) =
(IC (Exec ((IncAddr (INS,j)),s))) + k
by MEMSTR_0:53
.=
IC (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))))
by AMISTD_2:def 3
;
not not InsCode INS = 0 & ... & not InsCode INS = 7
by SCMRING3:39;
per cases then
( InsCode INS = 0 or InsCode INS = 1 or InsCode INS = 2 or InsCode INS = 3 or InsCode INS = 4 or InsCode INS = 5 or InsCode INS = 6 or InsCode INS = 7 )
;
suppose
InsCode INS = 0
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then A2:
INS = halt (SCM R)
by SCMRING3:12;
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k))) =
IncIC (
s,
k)
by A2, EXTPRO_1:def 3
.=
IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A2, EXTPRO_1:def 3
;
hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
;
verum end; suppose
InsCode INS = 1
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da,
db being
Data-Location of
R such that A3:
INS = da := db
by SCMRING3:13;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da = d or da <> d )
;
suppose A4:
da = d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A3, COMPOS_0:4
.=
(IncIC (s,k)) . db
by A3, A4, SCMRING2:11
.=
s . db
by Th5
.=
(Exec (INS,s)) . d
by A3, A4, SCMRING2:11
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A3, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; suppose A5:
da <> d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A3, COMPOS_0:4
.=
(IncIC (s,k)) . d
by A3, A5, SCMRING2:11
.=
s . d
by Th5
.=
(Exec (INS,s)) . d
by A3, A5, SCMRING2:11
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A3, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by Th6, A1;
verum end; suppose
InsCode INS = 2
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da,
db being
Data-Location of
R such that A6:
INS = AddTo (
da,
db)
by SCMRING3:14;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da = d or da <> d )
;
suppose A7:
da = d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A6, COMPOS_0:4
.=
((IncIC (s,k)) . da) + ((IncIC (s,k)) . db)
by A7, A6, SCMRING2:12
.=
(s . da) + ((IncIC (s,k)) . db)
by Th5
.=
(s . da) + (s . db)
by Th5
.=
(Exec (INS,s)) . d
by A6, A7, SCMRING2:12
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A6, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; suppose A8:
da <> d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A6, COMPOS_0:4
.=
(IncIC (s,k)) . d
by A6, A8, SCMRING2:12
.=
s . d
by Th5
.=
(Exec (INS,s)) . d
by A6, A8, SCMRING2:12
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A6, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by Th6, A1;
verum end; suppose
InsCode INS = 3
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da,
db being
Data-Location of
R such that A9:
INS = SubFrom (
da,
db)
by SCMRING3:15;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da = d or da <> d )
;
suppose A10:
da = d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A9, COMPOS_0:4
.=
((IncIC (s,k)) . da) - ((IncIC (s,k)) . db)
by A10, A9, SCMRING2:13
.=
(s . da) - ((IncIC (s,k)) . db)
by Th5
.=
(s . da) - (s . db)
by Th5
.=
(Exec (INS,s)) . d
by A9, A10, SCMRING2:13
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A9, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; suppose A11:
da <> d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A9, COMPOS_0:4
.=
(IncIC (s,k)) . d
by A9, A11, SCMRING2:13
.=
s . d
by Th5
.=
(Exec (INS,s)) . d
by A9, A11, SCMRING2:13
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A9, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by Th6, A1;
verum end; suppose
InsCode INS = 4
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da,
db being
Data-Location of
R such that A12:
INS = MultBy (
da,
db)
by SCMRING3:16;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da = d or da <> d )
;
suppose A13:
da = d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A12, COMPOS_0:4
.=
((IncIC (s,k)) . da) * ((IncIC (s,k)) . db)
by A13, A12, SCMRING2:14
.=
(s . da) * ((IncIC (s,k)) . db)
by Th5
.=
(s . da) * (s . db)
by Th5
.=
(Exec (INS,s)) . d
by A12, A13, SCMRING2:14
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A12, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; suppose A14:
da <> d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A12, COMPOS_0:4
.=
(IncIC (s,k)) . d
by A12, A14, SCMRING2:14
.=
s . d
by Th5
.=
(Exec (INS,s)) . d
by A12, A14, SCMRING2:14
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A12, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by Th6, A1;
verum end; suppose
InsCode INS = 5
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da being
Data-Location of
R,
r being
Element of
R such that A15:
INS = da := r
by SCMRING3:17;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da = d or da <> d )
;
suppose A16:
da = d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A15, COMPOS_0:4
.=
r
by A16, A15, SCMRING2:17
.=
(Exec (INS,s)) . d
by A15, A16, SCMRING2:17
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; suppose A17:
da <> d
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(Exec (INS,(IncIC (s,k)))) . d
by A15, COMPOS_0:4
.=
(IncIC (s,k)) . d
by A15, A17, SCMRING2:17
.=
s . d
by Th5
.=
(Exec (INS,s)) . d
by A15, A17, SCMRING2:17
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by Th6, A1;
verum end; suppose
InsCode INS = 6
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider loc being
Nat such that A18:
INS = goto (
loc,
R)
by SCMRING3:18;
A19:
IncAddr (
INS,
(j + k))
= goto (
(loc + (j + k)),
R)
by A18, SCMRING3:37;
A20:
IncAddr (
INS,
j)
= goto (
(loc + j),
R)
by A18, SCMRING3:37;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dthus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(IncIC (s,k)) . d
by A19, SCMRING2:15
.=
s . d
by Th5
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A20, SCMRING2:15
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by Th6, A1;
verum end; suppose
InsCode INS = 7
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da being
Data-Location of
R,
loc being
Nat such that A21:
INS = da =0_goto loc
by SCMRING3:19;
A22:
IncAddr (
INS,
(j + k))
= da =0_goto (loc + (j + k))
by A21, SCMRING3:38;
A23:
IncAddr (
INS,
j)
= da =0_goto (loc + j)
by A21, SCMRING3:38;
now for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location of
R;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dthus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d =
(IncIC (s,k)) . d
by A22, SCMRING2:16
.=
s . d
by Th5
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A23, SCMRING2:16
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by Th5
;
verum end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, Th6;
verum end; end;