let INS be Instruction of SCM; 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; 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 = 8
by AMI_5:5;
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 or InsCode INS = 8 )
;
suppose
InsCode INS = 0
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then A2:
INS = halt SCM
by AMI_5:7;
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k))) =
Exec (
INS,
(IncIC (s,k)))
by A2, COMPOS_0:4
.=
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 such that A3:
INS = da := db
by AMI_5:8;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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, AMI_3:2
.=
s . db
by AMI_5:16
.=
(Exec (INS,s)) . d
by A3, A4, AMI_3:2
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A3, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
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, AMI_3:2
.=
s . d
by AMI_5:16
.=
(Exec (INS,s)) . d
by A3, A5, AMI_3:2
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A3, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
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 such that A6:
INS = AddTo (
da,
db)
by AMI_5:9;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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, AMI_3:3
.=
(s . da) + ((IncIC (s,k)) . db)
by AMI_5:16
.=
(s . da) + (s . db)
by AMI_5:16
.=
(Exec (INS,s)) . d
by A6, A7, AMI_3:3
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A6, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
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, AMI_3:3
.=
s . d
by AMI_5:16
.=
(Exec (INS,s)) . d
by A6, A8, AMI_3:3
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A6, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
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 such that A9:
INS = SubFrom (
da,
db)
by AMI_5:10;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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, AMI_3:4
.=
(s . da) - ((IncIC (s,k)) . db)
by AMI_5:16
.=
(s . da) - (s . db)
by AMI_5:16
.=
(Exec (INS,s)) . d
by A9, A10, AMI_3:4
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A9, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
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, AMI_3:4
.=
s . d
by AMI_5:16
.=
(Exec (INS,s)) . d
by A9, A11, AMI_3:4
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A9, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
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 such that A12:
INS = MultBy (
da,
db)
by AMI_5:11;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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, AMI_3:5
.=
(s . da) * ((IncIC (s,k)) . db)
by AMI_5:16
.=
(s . da) * (s . db)
by AMI_5:16
.=
(Exec (INS,s)) . d
by A12, A13, AMI_3:5
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A12, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
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, AMI_3:5
.=
s . d
by AMI_5:16
.=
(Exec (INS,s)) . d
by A12, A14, AMI_3:5
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A12, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
verum end; suppose
InsCode INS = 5
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider da,
db being
Data-Location such that A15:
INS = Divide (
da,
db)
by AMI_5:12;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da <> db or da = db )
;
suppose A16:
da <> db
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1hereby verum
per cases
( da = d or db = d or ( da <> d & db <> d ) )
;
suppose A17:
da = d
;
(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 =
(Exec (INS,(IncIC (s,k)))) . d
by A15, COMPOS_0:4
.=
((IncIC (s,k)) . da) div ((IncIC (s,k)) . db)
by A16, A17, A15, AMI_3:6
.=
(s . da) div ((IncIC (s,k)) . db)
by AMI_5:16
.=
(s . da) div (s . db)
by AMI_5:16
.=
(Exec (INS,s)) . d
by A15, A16, A17, AMI_3:6
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; suppose A18:
db = d
;
(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 =
(Exec (INS,(IncIC (s,k)))) . d
by A15, COMPOS_0:4
.=
((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db)
by A18, A15, AMI_3:6
.=
(s . da) mod ((IncIC (s,k)) . db)
by AMI_5:16
.=
(s . da) mod (s . db)
by AMI_5:16
.=
(Exec (INS,s)) . d
by A15, A18, AMI_3:6
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; suppose A19:
(
da <> d &
db <> d )
;
(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 =
(Exec (INS,(IncIC (s,k)))) . d
by A15, COMPOS_0:4
.=
(IncIC (s,k)) . d
by A15, A19, AMI_3:6
.=
s . d
by AMI_5:16
.=
(Exec (INS,s)) . d
by A15, A19, AMI_3:6
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; end;
end; end; suppose A20:
da = db
;
(Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1per cases
( da = d or da <> d )
;
suppose A21:
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)) . da) mod ((IncIC (s,k)) . db)
by A20, A21, A15, AMI_3:6
.=
(s . da) mod ((IncIC (s,k)) . db)
by AMI_5:16
.=
(s . da) mod (s . db)
by AMI_5:16
.=
(Exec (INS,s)) . d
by A15, A20, A21, AMI_3:6
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; suppose A22:
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, A20, A22, AMI_3:6
.=
s . d
by AMI_5:16
.=
(Exec (INS,s)) . d
by A15, A20, A22, AMI_3:6
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A15, COMPOS_0:4
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; end; end; end; end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
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 A23:
INS = SCM-goto loc
by AMI_5:13;
A24:
IncAddr (
INS,
(j + k))
= SCM-goto (loc + (j + k))
by A23, Th1;
A25:
IncAddr (
INS,
j)
= SCM-goto (loc + j)
by A23, Th1;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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 A24, AMI_3:7
.=
s . d
by AMI_5:16
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A25, AMI_3:7
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
verum end; suppose
InsCode INS = 7
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider loc being
Nat,
da being
Data-Location such that A26:
INS = da =0_goto loc
by AMI_5:14;
A27:
IncAddr (
INS,
(j + k))
= da =0_goto (loc + (j + k))
by A26, Th2;
A28:
IncAddr (
INS,
j)
= da =0_goto (loc + j)
by A26, Th2;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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 A27, AMI_3:8
.=
s . d
by AMI_5:16
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A28, AMI_3:8
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
verum end; suppose
InsCode INS = 8
;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)then consider loc being
Nat,
da being
Data-Location such that A29:
INS = da >0_goto loc
by AMI_5:15;
A30:
IncAddr (
INS,
(j + k))
= da >0_goto (loc + (j + k))
by A29, Th3;
A31:
IncAddr (
INS,
j)
= da >0_goto (loc + j)
by A29, Th3;
now for d being Data-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . dlet d be
Data-Location;
(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 A30, AMI_3:9
.=
s . d
by AMI_5:16
.=
(Exec ((IncAddr (INS,j)),s)) . d
by A31, AMI_3:9
.=
(IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
by AMI_5:16
;
verum end; hence
Exec (
(IncAddr (INS,(j + k))),
(IncIC (s,k)))
= IncIC (
(Exec ((IncAddr (INS,j)),s)),
k)
by A1, AMI_5:25;
verum end; end;