:: On the Composition of Macro Instructions of Standard Computers
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users
begin
theorem
:: AMISTD_2:1
for
N
being
with_zero
set
for
I
being
Instruction
of
(
STC
N
)
holds
JumpPart
I
=
0
;
definition
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
;
let
I
be
Instruction
of
S
;
attr
I
is
with_explicit_jumps
means
:
Def1
:
:: AMISTD_2:def 1
JUMP
I
=
rng
(
JumpPart
I
)
;
end;
::
deftheorem
Def1
defines
with_explicit_jumps
AMISTD_2:def 1 :
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
for
I
being
Instruction
of
S
holds
(
I
is
with_explicit_jumps
iff
JUMP
I
=
rng
(
JumpPart
I
)
);
definition
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
;
attr
S
is
with_explicit_jumps
means
:
Def2
:
:: AMISTD_2:def 2
for
I
being
Instruction
of
S
holds
I
is
with_explicit_jumps
;
end;
::
deftheorem
Def2
defines
with_explicit_jumps
AMISTD_2:def 2 :
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
holds
(
S
is
with_explicit_jumps
iff for
I
being
Instruction
of
S
holds
I
is
with_explicit_jumps
);
registration
let
N
be
with_zero
set
;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
standard
for
AMI-Struct
over
N
;
existence
ex
b
1
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
st
b
1
is
standard
proof
end;
end;
theorem
Th2
:
:: AMISTD_2:2
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
standard
AMI-Struct
over
N
for
I
being
Instruction
of
S
st ( for
f
being
Element
of
NAT
holds
NIC
(
I
,
f
)
=
{
(
succ
f
)
}
) holds
JUMP
I
is
empty
proof
end;
registration
let
N
be
with_zero
set
;
let
I
be
Instruction
of
(
STC
N
)
;
cluster
JUMP
I
->
empty
;
coherence
JUMP
I
is
empty
proof
end;
end;
theorem
:: AMISTD_2:3
for
N
being
with_zero
set
for
T
being
InsType
of the
InstructionsF
of
(
STC
N
)
holds
JumpParts
T
=
{
0
}
proof
end;
Lm1
:
for
N
being
with_zero
set
for
I
being
Instruction
of
(
Trivial-AMI
N
)
holds
JumpPart
I
=
0
proof
end;
Lm2
:
for
N
being
with_zero
set
for
T
being
InsType
of the
InstructionsF
of
(
Trivial-AMI
N
)
holds
JumpParts
T
=
{
0
}
proof
end;
registration
let
N
be
with_zero
set
;
cluster
STC
N
->
with_explicit_jumps
;
coherence
STC
N
is
with_explicit_jumps
proof
end;
end;
registration
let
N
be
with_zero
set
;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
with_explicit_jumps
for
AMI-Struct
over
N
;
existence
ex
b
1
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
st
(
b
1
is
standard
&
b
1
is
halting
&
b
1
is
with_explicit_jumps
)
proof
end;
end;
registration
let
N
be
with_zero
set
;
let
I
be
Instruction
of
(
Trivial-AMI
N
)
;
cluster
JUMP
I
->
empty
;
coherence
JUMP
I
is
empty
proof
end;
end;
registration
let
N
be
with_zero
set
;
cluster
Trivial-AMI
N
->
with_explicit_jumps
;
coherence
Trivial-AMI
N
is
with_explicit_jumps
proof
end;
end;
registration
let
N
be
with_zero
set
;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
for
AMI-Struct
over
N
;
existence
ex
b
1
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
st
(
b
1
is
with_explicit_jumps
&
b
1
is
halting
)
proof
end;
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
with_explicit_jumps
AMI-Struct
over
N
;
cluster
->
with_explicit_jumps
for
Element
of the
InstructionsF
of
S
;
coherence
for
b
1
being
Instruction
of
S
holds
b
1
is
with_explicit_jumps
by
Def2
;
end;
theorem
Th4
:
:: AMISTD_2:4
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
for
I
being
Instruction
of
S
st
I
is
halting
holds
JUMP
I
is
empty
proof
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
AMI-Struct
over
N
;
let
I
be
halting
Instruction
of
S
;
cluster
JUMP
I
->
empty
;
coherence
JUMP
I
is
empty
by
Th4
;
end;
theorem
:: AMISTD_2:5
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
AMI-Struct
over
N
for
I
being
Instruction
of
S
st
I
is
ins-loc-free
holds
JUMP
I
is
empty
proof
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
with_explicit_jumps
AMI-Struct
over
N
;
cluster
halting
->
ins-loc-free
for
Element
of the
InstructionsF
of
S
;
coherence
for
b
1
being
Instruction
of
S
st
b
1
is
halting
holds
b
1
is
ins-loc-free
proof
end;
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
with_explicit_jumps
AMI-Struct
over
N
;
cluster
sequential
->
ins-loc-free
for
Element
of the
InstructionsF
of
S
;
coherence
for
b
1
being
Instruction
of
S
st
b
1
is
sequential
holds
b
1
is
ins-loc-free
proof
end;
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
AMI-Struct
over
N
;
cluster
Stop
S
->
really-closed
;
coherence
Stop
S
is
really-closed
by
AMISTD_1:16
;
end;
begin
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
AMI-Struct
over
N
;
let
I
be
halting
Instruction
of
S
;
let
k
be
Nat
;
cluster
IncAddr
(
I
,
k
)
->
halting
;
coherence
IncAddr
(
I
,
k
) is
halting
by
COMPOS_0:4
;
end;
theorem
:: AMISTD_2:6
for
k
being
Nat
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
with_explicit_jumps
AMI-Struct
over
N
for
I
being
Instruction
of
S
st
I
is
sequential
holds
IncAddr
(
I
,
k
) is
sequential
by
COMPOS_0:4
;
definition
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
AMI-Struct
over
N
;
let
I
be
Instruction
of
S
;
attr
I
is
IC-relocable
means
:
Def3
:
:: AMISTD_2:def 3
for
j
,
k
being
Nat
for
s
being
State
of
S
holds
(
IC
(
Exec
(
(
IncAddr
(
I
,
j
)
)
,
s
)
)
)
+
k
=
IC
(
Exec
(
(
IncAddr
(
I
,
(
j
+
k
)
)
)
,
(
IncIC
(
s
,
k
)
)
)
)
;
end;
::
deftheorem
Def3
defines
IC-relocable
AMISTD_2:def 3 :
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
halting
AMI-Struct
over
N
for
I
being
Instruction
of
S
holds
(
I
is
IC-relocable
iff for
j
,
k
being
Nat
for
s
being
State
of
S
holds
(
IC
(
Exec
(
(
IncAddr
(
I
,
j
)
)
,
s
)
)
)
+
k
=
IC
(
Exec
(
(
IncAddr
(
I
,
(
j
+
k
)
)
)
,
(
IncIC
(
s
,
k
)
)
)
)
);
definition
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
AMI-Struct
over
N
;
attr
S
is
IC-relocable
means
:
Def4
:
:: AMISTD_2:def 4
for
I
being
Instruction
of
S
holds
I
is
IC-relocable
;
end;
::
deftheorem
Def4
defines
IC-relocable
AMISTD_2:def 4 :
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
halting
AMI-Struct
over
N
holds
(
S
is
IC-relocable
iff for
I
being
Instruction
of
S
holds
I
is
IC-relocable
);
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
AMI-Struct
over
N
;
cluster
sequential
->
IC-relocable
for
Element
of the
InstructionsF
of
S
;
coherence
for
b
1
being
Instruction
of
S
st
b
1
is
sequential
holds
b
1
is
IC-relocable
proof
end;
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
AMI-Struct
over
N
;
cluster
halting
->
IC-relocable
for
Element
of the
InstructionsF
of
S
;
coherence
for
b
1
being
Instruction
of
S
st
b
1
is
halting
holds
b
1
is
IC-relocable
proof
end;
end;
registration
let
N
be
with_zero
set
;
cluster
STC
N
->
IC-relocable
;
coherence
STC
N
is
IC-relocable
proof
end;
end;
registration
let
N
be
with_zero
set
;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
with_explicit_jumps
for
AMI-Struct
over
N
;
existence
ex
b
1
being non
empty
with_non-empty_values
IC-Ins-separated
standard
AMI-Struct
over
N
st
(
b
1
is
halting
&
b
1
is
with_explicit_jumps
)
proof
end;
end;
registration
let
N
be
with_zero
set
;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
with_explicit_jumps
IC-relocable
for
AMI-Struct
over
N
;
existence
ex
b
1
being non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
with_explicit_jumps
AMI-Struct
over
N
st
b
1
is
IC-relocable
proof
end;
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
IC-relocable
AMI-Struct
over
N
;
cluster
->
IC-relocable
for
Element
of the
InstructionsF
of
S
;
coherence
for
b
1
being
Instruction
of
S
holds
b
1
is
IC-relocable
by
Def4
;
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
AMI-Struct
over
N
;
cluster
with_explicit_jumps
IC-relocable
for
Element
of the
InstructionsF
of
S
;
existence
ex
b
1
being
Instruction
of
S
st
b
1
is
IC-relocable
proof
end;
end;
theorem
Th7
:
:: AMISTD_2:7
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
AMI-Struct
over
N
for
I
being
IC-relocable
Instruction
of
S
for
k
being
Nat
for
s
being
State
of
S
holds
(
IC
(
Exec
(
I
,
s
)
)
)
+
k
=
IC
(
Exec
(
(
IncAddr
(
I
,
k
)
)
,
(
IncIC
(
s
,
k
)
)
)
)
proof
end;
registration
let
N
be
with_zero
set
;
let
S
be non
empty
with_non-empty_values
IC-Ins-separated
halting
standard
with_explicit_jumps
IC-relocable
AMI-Struct
over
N
;
let
F
,
G
be
NAT
-defined
the
InstructionsF
of
S
-valued
non
empty
finite
initial
really-closed
Function
;
cluster
F
';'
G
->
really-closed
;
coherence
F
';'
G
is
really-closed
proof
end;
end;
theorem
:: AMISTD_2:8
for
N
being
with_zero
set
for
I
being
Instruction
of
(
Trivial-AMI
N
)
holds
JumpPart
I
=
0
by
Lm1
;
theorem
:: AMISTD_2:9
for
N
being
with_zero
set
for
T
being
InsType
of the
InstructionsF
of
(
Trivial-AMI
N
)
holds
JumpParts
T
=
{
0
}
by
Lm2
;
theorem
:: AMISTD_2:10
for
N
being
with_zero
set
for
n
being
Element
of
NAT
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
AMI-Struct
over
N
for
s
being
State
of
S
for
I
being
Program
of
for
P1
,
P2
being
Instruction-Sequence
of
S
st
I
c=
P1
&
I
c=
P2
& ( for
m
being
Element
of
NAT
st
m
<
n
holds
IC
(
Comput
(
P2
,
s
,
m
)
)
in
dom
I
) holds
for
m
being
Element
of
NAT
st
m
<=
n
holds
Comput
(
P1
,
s
,
m
)
=
Comput
(
P2
,
s
,
m
)
proof
end;
theorem
:: AMISTD_2:11
for
N
being
with_zero
set
for
S
being non
empty
with_non-empty_values
IC-Ins-separated
halting
AMI-Struct
over
N
for
P
being
Instruction-Sequence
of
S
for
s
being
State
of
S
st
s
=
Following
(
P
,
s
) holds
for
n
being
Element
of
NAT
holds
Comput
(
P
,
s
,
n
)
=
s
proof
end;