scm_inst.miz
begin
reserve x,y,z for
set;
notation
synonym
SCM-Halt for
0 ;
end
definition
:: original:
SCM-Halt
redefine
func
SCM-Halt ->
Element of (
Segm 9) ;
correctness by
NAT_1: 44;
end
definition
::
SCM_INST:def1
func
SCM-Data-Loc ->
set equals
[:
{1},
NAT :];
coherence ;
end
registration
cluster
SCM-Data-Loc -> non
empty;
coherence ;
end
reserve I,J,K for
Element of (
Segm 9),
i,a,a1,a2 for
Nat,
b,b1,b2,c,c1 for
Element of
SCM-Data-Loc ;
definition
::
SCM_INST:def2
func
SCM-Instr -> non
empty
set equals (((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} })
\/ {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} });
coherence ;
end
theorem ::
SCM_INST:1
Th1:
[
0 ,
{} ,
{} ]
in
SCM-Instr
proof
[
0 ,
{} ,
{} ]
in
{
[
SCM-Halt ,
{} ,
{} ]} by
TARSKI:def 1;
then
[
0 ,
{} ,
{} ]
in (
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 }) by
XBOOLE_0:def 3;
then
[
0 ,
{} ,
{} ]
in ((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} }) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
registration
cluster
SCM-Instr -> non
empty;
coherence ;
end
theorem ::
SCM_INST:2
Th2:
[6,
<*a2*>,
{} ]
in
SCM-Instr
proof
reconsider x = 6 as
Element of (
Segm 9) by
NAT_1: 44;
[x,
<*a2*>,
{} ]
in {
[J,
<*a*>,
{} ] : J
= 6 };
then
[x,
<*a2*>,
{} ]
in (
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 }) by
XBOOLE_0:def 3;
then
[x,
<*a2*>,
{} ]
in ((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} }) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
SCM_INST:3
Th3: x
in
{7, 8} implies
[x,
<*a2*>,
<*b2*>]
in
SCM-Instr
proof
assume
A1: x
in
{7, 8};
then x
= 7 or x
= 8 by
TARSKI:def 2;
then
reconsider x as
Element of (
Segm 9) by
NAT_1: 44;
[x,
<*a2*>,
<*b2*>]
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} } by
A1;
then
[x,
<*a2*>,
<*b2*>]
in ((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} }) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
SCM_INST:4
Th4: x
in
{1, 2, 3, 4, 5} implies
[x,
{} ,
<*b1, c1*>]
in
SCM-Instr
proof
assume
A1: x
in
{1, 2, 3, 4, 5};
then x
= 1 or x
= 2 or x
= 3 or x
= 4 or x
= 5 by
ENUMSET1:def 3;
then
reconsider x as
Element of (
Segm 9) by
NAT_1: 44;
[x,
{} ,
<*b1, c1*>]
in {
[J,
{} ,
<*b, c*>] : J
in
{1, 2, 3, 4, 5} } by
A1;
hence thesis by
XBOOLE_0:def 3;
end;
definition
let x be
Element of
SCM-Instr ;
given mk,ml be
Element of
SCM-Data-Loc , I such that
A1: x
=
[I,
{} ,
<*mk, ml*>];
::
SCM_INST:def3
func x
address_1 ->
Element of
SCM-Data-Loc means
:
Def3: ex f be
FinSequence of
SCM-Data-Loc st f
= (x
`3_3 ) & it
= (f
/. 1);
existence
proof
take mk,
<*mk, ml*>;
thus thesis by
A1,
FINSEQ_4: 17;
end;
uniqueness ;
::
SCM_INST:def4
func x
address_2 ->
Element of
SCM-Data-Loc means
:
Def4: ex f be
FinSequence of
SCM-Data-Loc st f
= (x
`3_3 ) & it
= (f
/. 2);
existence
proof
take ml,
<*mk, ml*>;
thus thesis by
A1,
FINSEQ_4: 17;
end;
correctness ;
end
theorem ::
SCM_INST:5
for x be
Element of
SCM-Instr , mk,ml be
Element of
SCM-Data-Loc , I st x
=
[I,
{} ,
<*mk, ml*>] holds (x
address_1 )
= mk & (x
address_2 )
= ml
proof
let x be
Element of
SCM-Instr , mk,ml be
Element of
SCM-Data-Loc , I;
assume
A1: x
=
[I,
{} ,
<*mk, ml*>];
then
consider f be
FinSequence of
SCM-Data-Loc such that
A2: f
= (x
`3_3 ) and
A3: (x
address_1 )
= (f
/. 1) by
Def3;
f
=
<*mk, ml*> by
A1,
A2;
hence (x
address_1 )
= mk by
A3,
FINSEQ_4: 17;
consider f be
FinSequence of
SCM-Data-Loc such that
A4: f
= (x
`3_3 ) and
A5: (x
address_2 )
= (f
/. 2) by
A1,
Def4;
f
=
<*mk, ml*> by
A1,
A4;
hence thesis by
A5,
FINSEQ_4: 17;
end;
definition
let x be
Element of
SCM-Instr ;
given mk be
Nat, I such that
A1: x
=
[I,
<*mk*>,
{} ];
::
SCM_INST:def5
func x
jump_address ->
Nat means
:
Def5: ex f be
FinSequence of
NAT st f
= (x
`2_3 ) & it
= (f
/. 1);
existence
proof
reconsider mk as
Element of
NAT by
ORDINAL1:def 12;
take mk,
<*mk*>;
thus thesis by
A1,
FINSEQ_4: 16;
end;
correctness ;
end
theorem ::
SCM_INST:6
for x be
Element of
SCM-Instr , mk be
Nat, I st x
=
[I,
<*mk*>,
{} ] holds (x
jump_address )
= mk
proof
let x be
Element of
SCM-Instr , mk be
Nat, I;
assume
A1: x
=
[I,
<*mk*>,
{} ];
then
consider f be
FinSequence of
NAT such that
A2: f
= (x
`2_3 ) and
A3: (x
jump_address )
= (f
/. 1) by
Def5;
reconsider mk as
Element of
NAT by
ORDINAL1:def 12;
f
=
<*mk*> by
A1,
A2;
hence thesis by
A3,
FINSEQ_4: 16;
end;
definition
let x be
Element of
SCM-Instr ;
given mk be
Nat, ml be
Element of
SCM-Data-Loc , I such that
A1: x
=
[I,
<*mk*>,
<*ml*>];
::
SCM_INST:def6
func x
cjump_address ->
Nat means
:
Def6: ex mk be
Element of
NAT st
<*mk*>
= (x
`2_3 ) & it
= (
<*mk*>
/. 1);
existence
proof
reconsider mk as
Element of
NAT by
ORDINAL1:def 12;
take mk, mk;
thus thesis by
A1,
FINSEQ_4: 16;
end;
correctness ;
::
SCM_INST:def7
func x
cond_address ->
Element of
SCM-Data-Loc means
:
Def7: ex ml be
Element of
SCM-Data-Loc st
<*ml*>
= (x
`3_3 ) & it
= (
<*ml*>
/. 1);
existence
proof
take ml, ml;
thus thesis by
A1,
FINSEQ_4: 16;
end;
correctness ;
end
theorem ::
SCM_INST:7
for x be
Element of
SCM-Instr , mk be
Nat, ml be
Element of
SCM-Data-Loc , I st x
=
[I,
<*mk*>,
<*ml*>] holds (x
cjump_address )
= mk & (x
cond_address )
= ml
proof
let x be
Element of
SCM-Instr , mk be
Nat, ml be
Element of
SCM-Data-Loc , I;
reconsider mkk = mk as
Element of
NAT by
ORDINAL1:def 12;
assume
A1: x
=
[I,
<*mk*>,
<*ml*>];
then
consider mk9 be
Element of
NAT such that
A2:
<*mk9*>
= (x
`2_3 ) and
A3: (x
cjump_address )
= (
<*mk9*>
/. 1) by
Def6;
<*mk9*>
=
<*mkk*> by
A1,
A2;
hence (x
cjump_address )
= mk by
A3,
FINSEQ_4: 16;
consider ml9 be
Element of
SCM-Data-Loc such that
A4:
<*ml9*>
= (x
`3_3 ) and
A5: (x
cond_address )
= (
<*ml9*>
/. 1) by
A1,
Def7;
<*ml9*>
=
<*ml*> by
A1,
A4;
hence thesis by
A5,
FINSEQ_4: 16;
end;
theorem ::
SCM_INST:8
Th8:
SCM-Instr
c=
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):]
proof
let x be
object;
assume
A1: x
in
SCM-Instr ;
per cases by
A1,
XBOOLE_0:def 3;
suppose
A2: x
in ((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a2*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} });
per cases by
A2,
XBOOLE_0:def 3;
suppose
A3: x
in (
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a2*>,
{} ] : J
= 6 });
per cases by
A3,
XBOOLE_0:def 3;
suppose x
in
{
[
SCM-Halt ,
{} ,
{} ]};
then
A4: x
=
[
SCM-Halt ,
{} ,
{} ] by
TARSKI:def 1;
then
SCM-Halt
in
NAT &
{}
in (
NAT
* ) &
{}
in (
proj2
SCM-Instr ) by
A1,
FINSEQ_1: 49,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):] by
A4,
DOMAIN_1: 3;
end;
suppose x
in {
[J,
<*a2*>,
{} ] : J
= 6 };
then
consider J, a such that
A5: x
=
[J,
<*a*>,
{} ] & J
= 6;
J
in
NAT &
<*a*>
in (
NAT
* ) &
{}
in (
proj2
SCM-Instr ) by
A1,
A5,
FUNCT_7: 18,
XTUPLE_0:def 13,
ORDINAL1:def 12;
hence x
in
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):] by
A5,
DOMAIN_1: 3;
end;
end;
suppose x
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} };
then
consider K, a1, b1 such that
A6: x
=
[K,
<*a1*>,
<*b1*>] & K
in
{7, 8};
K
in
NAT &
<*a1*>
in (
NAT
* ) &
<*b1*>
in (
proj2
SCM-Instr ) by
A1,
A6,
FUNCT_7: 18,
XTUPLE_0:def 13,
ORDINAL1:def 12;
hence x
in
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):] by
A6,
DOMAIN_1: 3;
end;
end;
suppose x
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} };
then
consider I, b, c such that
A7: x
=
[I,
{} ,
<*b, c*>] & I
in
{1, 2, 3, 4, 5};
I
in
NAT &
{}
in (
NAT
* ) &
<*b, c*>
in (
proj2
SCM-Instr ) by
A1,
A7,
FINSEQ_1: 49,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):] by
A7,
DOMAIN_1: 3;
end;
end;
registration
cluster (
proj2
SCM-Instr ) ->
FinSequence-membered;
coherence
proof
let f be
object;
assume f
in (
proj2
SCM-Instr );
then
consider y be
object such that
A1:
[y, f]
in
SCM-Instr by
XTUPLE_0:def 13;
set x =
[y, f];
per cases by
A1,
XBOOLE_0:def 3;
suppose
A2: x
in ((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a2*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} });
per cases by
A2,
XBOOLE_0:def 3;
suppose
A3: x
in (
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a2*>,
{} ] : J
= 6 });
per cases by
A3,
XBOOLE_0:def 3;
suppose x
in
{
[
SCM-Halt ,
{} ,
{} ]};
then x
=
[
SCM-Halt ,
{} ,
{} ] by
TARSKI:def 1;
hence f is
FinSequence by
XTUPLE_0: 1;
end;
suppose x
in {
[J,
<*a2*>,
{} ] : J
= 6 };
then ex J, a st x
=
[J,
<*a*>,
{} ] & J
= 6;
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
suppose x
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} };
then ex K, a1, b1 st x
=
[K,
<*a1*>,
<*b1*>] & K
in
{7, 8};
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
suppose x
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} };
then ex I, b, c st x
=
[I,
{} ,
<*b, c*>] & I
in
{1, 2, 3, 4, 5};
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
end
theorem ::
SCM_INST:9
Th9: for x be
Element of
SCM-Instr holds x
in
{
[
SCM-Halt ,
{} ,
{} ]} & (
InsCode x)
=
0 or x
in {
[J,
<*a*>,
{} ] : J
= 6 } & (
InsCode x)
= 6 or x
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} } & ((
InsCode x)
= 7 or (
InsCode x)
= 8) or x
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} } & ((
InsCode x)
= 1 or (
InsCode x)
= 2 or (
InsCode x)
= 3 or (
InsCode x)
= 4 or (
InsCode x)
= 5)
proof
let x be
Element of
SCM-Instr ;
x
in ((
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 })
\/ {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} }) or x
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} } by
XBOOLE_0:def 3;
then x
in (
{
[
SCM-Halt ,
{} ,
{} ]}
\/ {
[J,
<*a*>,
{} ] : J
= 6 }) or x
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} } or x
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} } by
XBOOLE_0:def 3;
per cases by
XBOOLE_0:def 3;
case x
in
{
[
SCM-Halt ,
{} ,
{} ]};
then x
=
[
SCM-Halt ,
{} ,
{} ] by
TARSKI:def 1;
hence thesis;
end;
case x
in {
[J,
<*a*>,
{} ] : J
= 6 };
then ex J, a st x
=
[J,
<*a*>,
{} ] & J
= 6;
hence thesis;
end;
case x
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} };
then
consider K, a1, b1 such that
A1: x
=
[K,
<*a1*>,
<*b1*>] and
A2: K
in
{7, 8};
(
InsCode x)
= K by
A1;
hence thesis by
A2,
TARSKI:def 2;
end;
case x
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} };
then
consider I, b, c such that
A3: x
=
[I,
{} ,
<*b, c*>] and
A4: I
in
{1, 2, 3, 4, 5};
(
InsCode x)
= I by
A3;
hence thesis by
A4,
ENUMSET1:def 3;
end;
end;
begin
reserve i,j,k for
Nat;
registration
cluster
SCM-Instr ->
standard-ins;
coherence
proof
consider X be non
empty
set such that
A1: (
proj2
SCM-Instr )
c= (X
* ) by
FINSEQ_1: 85;
take X;
A2:
SCM-Instr
c=
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):] by
Th8;
[:
NAT , (
NAT
* ), (
proj2
SCM-Instr ):]
c=
[:
NAT , (
NAT
* ), (X
* ):] by
A1,
MCART_1: 73;
hence
SCM-Instr
c=
[:
NAT , (
NAT
* ), (X
* ):] by
A2;
end;
end
reserve I,J,K for
Element of (
Segm 9),
a,a1,a2 for
Nat,
b,b1,b2,c,c1 for
Element of
SCM-Data-Loc ;
theorem ::
SCM_INST:10
Th10: for l be
Element of
SCM-Instr holds (
InsCode l)
<= 8
proof
let l be
Element of
SCM-Instr ;
(
InsCode l)
=
0 or (
InsCode l)
= 1 or (
InsCode l)
= 2 or (
InsCode l)
= 3 or (
InsCode l)
= 4 or (
InsCode l)
= 5 or (
InsCode l)
= 6 or (
InsCode l)
= 7 or (
InsCode l)
= 8 by
Th9;
hence thesis;
end;
Lm1: for i be
Element of
SCM-Instr st (
InsCode i)
= 1 or (
InsCode i)
= 2 or (
InsCode i)
= 3 or (
InsCode i)
= 4 or (
InsCode i)
= 5 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCM-Instr ;
assume (
InsCode i)
= 1 or (
InsCode i)
= 2 or (
InsCode i)
= 3 or (
InsCode i)
= 4 or (
InsCode i)
= 5;
then i
in {
[I,
{} ,
<*b, c*>] : I
in
{1, 2, 3, 4, 5} } by
Th9;
then ex I, b, c st i
=
[I,
{} ,
<*b, c*>] & I
in
{1, 2, 3, 4, 5};
hence thesis;
end;
Lm2: for i be
Element of
SCM-Instr st (
InsCode i)
= 7 or (
InsCode i)
= 8 holds (
dom (
JumpPart i))
= (
Seg 1)
proof
let i be
Element of
SCM-Instr ;
assume (
InsCode i)
= 7 or (
InsCode i)
= 8;
then i
in {
[K,
<*a1*>,
<*b1*>] : K
in
{7, 8} } by
Th9;
then
consider K, a1, b1 such that
A1: i
=
[K,
<*a1*>,
<*b1*>] and K
in
{7, 8};
(
JumpPart i)
=
<*a1*> by
A1;
hence thesis by
FINSEQ_1: 38;
end;
Lm3: for i be
Element of
SCM-Instr st (
InsCode i)
= 6 holds (
dom (
JumpPart i))
= (
Seg 1)
proof
let i be
Element of
SCM-Instr ;
assume (
InsCode i)
= 6;
then i
in {
[J,
<*a*>,
{} ] : J
= 6 } by
Th9;
then
consider J, a such that
A1: i
=
[J,
<*a*>,
{} ] and J
= 6;
(
JumpPart i)
=
<*a*> by
A1;
hence thesis by
FINSEQ_1: 38;
end;
registration
cluster
SCM-Instr ->
homogeneous;
coherence
proof
let i,j be
Element of
SCM-Instr such that
A1: (
InsCode i)
= (
InsCode j);
(
InsCode i)
<= 8 by
Th10;
then (
InsCode i)
=
0 or ... or (
InsCode i)
= 8 by
NAT_1: 60;
per cases ;
suppose (
InsCode i)
=
0 ;
then i
in
{
[
SCM-Halt ,
{} ,
{} ]} & j
in
{
[
SCM-Halt ,
{} ,
{} ]} by
A1,
Th9;
then i
=
[
SCM-Halt ,
{} ,
{} ] & j
=
[
SCM-Halt ,
{} ,
{} ] by
TARSKI:def 1;
hence thesis;
end;
suppose (
InsCode i)
= 1 or ... or (
InsCode i)
= 5;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm1;
hence thesis;
end;
suppose (
InsCode i)
= 7 or (
InsCode i)
= 8;
then (
dom (
JumpPart i))
= (
Seg 1) & (
dom (
JumpPart j))
= (
Seg 1) by
A1,
Lm2;
hence thesis;
end;
suppose (
InsCode i)
= 6;
then (
dom (
JumpPart i))
= (
Seg 1) & (
dom (
JumpPart j))
= (
Seg 1) by
A1,
Lm3;
hence thesis;
end;
end;
end
Lm4: for T be
InsType of
SCM-Instr holds T
=
0 or ... or T
= 8
proof
let T be
InsType of
SCM-Instr ;
consider y be
object such that
A1:
[T, y]
in (
proj1
SCM-Instr ) by
XTUPLE_0:def 12;
consider x be
object such that
A2:
[
[T, y], x]
in
SCM-Instr by
A1,
XTUPLE_0:def 12;
reconsider I =
[T, y, x] as
Element of
SCM-Instr by
A2;
T
= (
InsCode I);
hence thesis by
Th10,
NAT_1: 60;
end;
reserve T for
InsType of
SCM-Instr ,
I for
Element of
SCM-Instr ;
Lm5: T
=
0 implies (
JumpParts T)
=
{
{} }
proof
assume
A1: T
=
0 ;
hereby
let a be
object;
assume a
in (
JumpParts T);
then
consider I such that
A2: a
= (
JumpPart I) and
A3: (
InsCode I)
= T;
I
in
{
[
SCM-Halt ,
{} ,
{} ]} by
A1,
A3,
Th9;
then I
=
[
SCM-Halt ,
{} ,
{} ] by
TARSKI:def 1;
then a
=
{} by
A2;
hence a
in
{
{} } by
TARSKI:def 1;
end;
let a be
object;
assume a
in
{
{} };
then
A4: a
=
{} by
TARSKI:def 1;
A5: (
JumpPart
[
SCM-Halt ,
{} ,
{} ])
=
{} ;
A6: (
InsCode
[
SCM-Halt ,
{} ,
{} ])
=
SCM-Halt ;
[
SCM-Halt ,
{} ,
{} ]
in
SCM-Instr by
Th1;
hence a
in (
JumpParts T) by
A1,
A4,
A5,
A6;
end;
Lm6: T
= 1 or ... or T
= 5 implies (
JumpParts T)
=
{
{} }
proof
assume
A1: T
= 1 or ... or T
= 5;
hereby
let x be
object;
assume x
in (
JumpParts T);
then
consider I be
Element of
SCM-Instr such that
A2: x
= (
JumpPart I) and
A3: (
InsCode I)
= T;
I
in {
[J,
{} ,
<*b, c*>] where J be
Element of (
Segm 9), b be
Element of
SCM-Data-Loc , c be
Element of
SCM-Data-Loc : J
in
{1, 2, 3, 4, 5} } by
A1,
A3,
Th9;
then
consider J be
Element of (
Segm 9), b be
Element of
SCM-Data-Loc , c be
Element of
SCM-Data-Loc such that
A4: I
=
[J,
{} ,
<*b, c*>] and J
in
{1, 2, 3, 4, 5};
x
=
{} by
A2,
A4;
hence x
in
{
{} } by
TARSKI:def 1;
end;
set a = the
Element of
SCM-Data-Loc ;
let x be
object;
assume x
in
{
{} };
then
A5: x
=
{} by
TARSKI:def 1;
A6: (
JumpPart
[T,
{} ,
<*a, a*>])
=
{} ;
A7: (
InsCode
[T,
{} ,
<*a, a*>])
= T;
T
in
{1, 2, 3, 4, 5} by
A1,
ENUMSET1:def 3;
then
[T,
{} ,
<*a, a*>]
in
SCM-Instr by
Th4;
hence thesis by
A5,
A6,
A7;
end;
registration
cluster
SCM-Instr ->
J/A-independent;
coherence
proof
let T be
InsType of
SCM-Instr , f1,f2 be
natural-valued
Function such that
A1: f1
in (
JumpParts T) and
A2: (
dom f1)
= (
dom f2);
let p be
object such that
A3:
[T, f1, p]
in
SCM-Instr ;
T
=
0 or ... or T
= 8 by
Lm4;
per cases ;
suppose T
=
0 ;
then (
JumpParts T)
=
{
{} } by
Lm5;
then f1
=
{} by
A1,
TARSKI:def 1;
then f1
= f2 by
A2;
hence
[T, f2, p]
in
SCM-Instr by
A3;
end;
suppose T
= 1 or ... or T
= 5;
then
A4: (
JumpParts T)
=
{
{} } by
Lm6;
f1
=
{} by
A4,
A1,
TARSKI:def 1;
then f1
= f2 by
A2;
hence
[T, f2, p]
in
SCM-Instr by
A3;
end;
suppose
A5: T
= 6;
reconsider J =
[T, f1, p] as
Element of
SCM-Instr by
A3;
(
InsCode J)
= 6 by
A5;
then J
in {
[K,
<*i1*>,
{} ] where K be
Element of (
Segm 9), i1 be
Nat : K
= 6 } by
Th9;
then
consider K be
Element of (
Segm 9), i1 be
Nat such that
A6: J
=
[K,
<*i1*>,
{} ] & K
= 6;
A7: p
=
{} by
A6,
XTUPLE_0: 3;
f1
=
<*i1*> by
A6,
XTUPLE_0: 3;
then
A8: (
dom f2)
=
{1} by
A2,
FINSEQ_1: 2,
FINSEQ_1: 38;
reconsider l = (f2
. 1) as
Nat;
set I =
[T, f2,
{} ];
I
=
[6,
<*l*>,
{} ] by
A5,
A8,
FINSEQ_1: 2,
FINSEQ_1:def 8;
then
reconsider I as
Element of
SCM-Instr by
Th2;
f2
= (
JumpPart I);
hence
[T, f2, p]
in
SCM-Instr by
A7;
end;
suppose
A9: T
= 7 or T
= 8;
reconsider J =
[T, f1, p] as
Element of
SCM-Instr by
A3;
(
InsCode J)
= T;
then J
in {
[K,
<*i1*>,
<*a*>] where K be
Element of (
Segm 9), i1 be
Nat, a be
Element of
SCM-Data-Loc : K
in
{7, 8} } by
A9,
Th9;
then
consider K be
Element of (
Segm 9), i1 be
Nat, a be
Element of
SCM-Data-Loc such that
A10: J
=
[K,
<*i1*>,
<*a*>] and K
in
{7, 8};
A11: p
=
<*a*> by
A10,
XTUPLE_0: 3;
f1
=
<*i1*> by
A10,
XTUPLE_0: 3;
then
A12: (
dom f2)
=
{1} by
A2,
FINSEQ_1: 2,
FINSEQ_1: 38;
reconsider l = (f2
. 1) as
Nat;
set I =
[T, f2, p];
A13: T
in
{7, 8} by
A9,
TARSKI:def 2;
I
=
[T,
<*l*>,
<*a*>] by
A11,
A12,
FINSEQ_1: 2,
FINSEQ_1:def 8;
then
reconsider I as
Element of
SCM-Instr by
A13,
Th3;
(
InsCode I)
= T;
then I
in {
[L,
<*i2*>,
<*b*>] where L be
Element of (
Segm 9), i2 be
Nat, b be
Element of
SCM-Data-Loc : L
in
{7, 8} } by
A9,
Th9;
then
consider L be
Element of (
Segm 9), i2 be
Nat, b be
Element of
SCM-Data-Loc such that
A14: I
=
[L,
<*i2*>,
<*b*>] and L
in
{7, 8};
L
= (
InsCode I) by
A14
.= T;
then
A15: I
=
[T,
<*i2*>,
<*b*>] by
A14;
thus
[T, f2, p]
in
SCM-Instr by
A15;
end;
end;
end
registration
cluster
SCM-Instr ->
with_halt;
coherence by
Th1;
end