scmpds_i.miz
begin
reserve i,j,k for
Element of
NAT ,
I,I2,I3,I4 for
Element of (
Segm 15),
i1 for
Element of
NAT ,
d1,d2,d3,d4,d5 for
Element of
SCM-Data-Loc ,
k1,k2 for
Integer;
theorem ::
SCMPDS_I:1
Th1: for k be
Integer holds k
in (
SCM-Data-Loc
\/
INT )
proof
let k be
Integer;
k
in
INT &
INT
c= (
SCM-Data-Loc
\/
INT ) by
INT_1:def 2,
XBOOLE_1: 7;
hence thesis;
end;
begin
definition
::
SCMPDS_I:def1
func
SCMPDS-Instr ->
set equals (((((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} })
\/ {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} })
\/ {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} });
coherence ;
end
Lm1:
[
0 ,
{} ,
{} ]
in
SCMPDS-Instr
proof
set S1 = the set of all
[14,
{} ,
<*k1*>] where k1 be
Element of
INT ;
set S2 = the set of all
[1,
{} ,
<*d1*>];
set S3 = {
[I2,
{} ,
<*d2, k2*>] where I2 be
Element of (
Segm 15), d2 be
Element of
SCM-Data-Loc , k2 be
Element of
INT : I2
in
{2, 3} };
[
0 ,
{} ,
{} ]
in
{
[
0 ,
{} ,
{} ]} by
TARSKI:def 1;
then
[
0 ,
{} ,
{} ]
in (
{
[
0 ,
{} ,
{} ]}
\/ S1) by
XBOOLE_0:def 3;
then
[
0 ,
{} ,
{} ]
in ((
{
[
0 ,
{} ,
{} ]}
\/ S1)
\/ S2) by
XBOOLE_0:def 3;
then
[
0 ,
{} ,
{} ]
in (((
{
[
0 ,
{} ,
{} ]}
\/ S1)
\/ S2)
\/ S3) by
XBOOLE_0:def 3;
then
[
0 ,
{} ,
{} ]
in ((((
{
[
0 ,
{} ,
{} ]}
\/ S1)
\/ S2)
\/ S3)
\/ {
[I3,
{} ,
<*d3, k3, k4*>] where I3 be
Element of (
Segm 15), d3 be
Element of
SCM-Data-Loc , k3,k4 be
Element of
INT : I3
in
{4, 5, 6, 7, 8} }) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
SCMPDS_I:2
[14,
{} ,
<*
0 *>]
in
SCMPDS-Instr
proof
set S1 = the set of all
[14,
{} ,
<*k1*>] where k1 be
Element of
INT ;
set S2 = the set of all
[1,
{} ,
<*d1*>];
set S3 = {
[I2,
{} ,
<*d2, k2*>] where I2 be
Element of (
Segm 15), d2 be
Element of
SCM-Data-Loc , k2 be
Element of
INT : I2
in
{2, 3} };
0 is
Element of
INT by
INT_1:def 2;
then
[14,
{} ,
<*
0 *>]
in S1;
then
[14,
{} ,
<*
0 *>]
in (
{
[
0 ,
{} ,
{} ]}
\/ S1) by
XBOOLE_0:def 3;
then
[14,
{} ,
<*
0 *>]
in ((
{
[
0 ,
{} ,
{} ]}
\/ S1)
\/ S2) by
XBOOLE_0:def 3;
then
[14,
{} ,
<*
0 *>]
in (((
{
[
0 ,
{} ,
{} ]}
\/ S1)
\/ S2)
\/ S3) by
XBOOLE_0:def 3;
then
[14,
{} ,
<*
0 *>]
in ((((
{
[
0 ,
{} ,
{} ]}
\/ S1)
\/ S2)
\/ S3)
\/ {
[I3,
{} ,
<*d3, k3, k4*>] where I3 be
Element of (
Segm 15), d3 be
Element of
SCM-Data-Loc , k3,k4 be
Element of
INT : I3
in
{4, 5, 6, 7, 8} }) by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
registration
cluster
SCMPDS-Instr -> non
empty;
coherence ;
end
definition
let d be
Element of
SCM-Data-Loc , s be
Integer;
:: original:
<*
redefine
func
<*d,s*> ->
FinSequence of (
SCM-Data-Loc
\/
INT ) ;
coherence
proof
let y be
object;
A1: (
dom
<*d, s*>)
=
{1, 2} by
FINSEQ_1: 2,
FINSEQ_1: 89;
assume y
in (
rng
<*d, s*>);
then
consider x be
object such that
A2: x
in (
dom
<*d, s*>) and
A3: (
<*d, s*>
. x)
= y by
FUNCT_1:def 3;
per cases by
A2,
A1,
TARSKI:def 2;
suppose x
= 1;
then y
= d by
A3,
FINSEQ_1: 44;
hence thesis by
XBOOLE_0:def 3;
end;
suppose
A4: x
= 2;
A5: s
in
INT by
INT_1:def 2;
y
= s by
A3,
A4,
FINSEQ_1: 44;
hence thesis by
A5,
XBOOLE_0:def 3;
end;
end;
end
definition
let x be
Element of
SCMPDS-Instr ;
given mk be
Element of
SCM-Data-Loc , I such that
A1: x
=
[I,
{} ,
<*mk*>];
::
SCMPDS_I:def2
func x
address_1 ->
Element of
SCM-Data-Loc means
:
Def2: ex f be
FinSequence of
SCM-Data-Loc st f
= (x
`3_3 ) & it
= (f
/. 1);
existence
proof
take mk,
<*mk*>;
thus thesis by
A1,
FINSEQ_4: 16;
end;
uniqueness ;
end
theorem ::
SCMPDS_I:3
for x be
Element of
SCMPDS-Instr , mk be
Element of
SCM-Data-Loc st x
=
[I,
{} ,
<*mk*>] holds (x
address_1 )
= mk
proof
let x be
Element of
SCMPDS-Instr , mk be
Element of
SCM-Data-Loc ;
assume
A1: x
=
[I,
{} ,
<*mk*>];
then
consider f be
FinSequence of
SCM-Data-Loc such that
A2: f
= (x
`3_3 ) and
A3: (x
address_1 )
= (f
/. 1) by
Def2;
f
=
<*mk*> by
A1,
A2;
hence thesis by
A3,
FINSEQ_4: 16;
end;
definition
let x be
Element of
SCMPDS-Instr ;
given r be
Integer, I such that
A1: x
=
[I,
{} ,
<*r*>];
::
SCMPDS_I:def3
func x
const_INT ->
Integer means
:
Def3: ex f be
FinSequence of
INT st f
= (x
`3_3 ) & it
= (f
/. 1);
existence
proof
reconsider mm = r as
Element of
INT by
INT_1:def 2;
take r,
<*mm*>;
thus thesis by
A1,
FINSEQ_4: 16;
end;
uniqueness ;
end
theorem ::
SCMPDS_I:4
for x be
Element of
SCMPDS-Instr , k be
Integer st x
=
[I,
{} ,
<*k*>] holds (x
const_INT )
= k
proof
let x be
Element of
SCMPDS-Instr , k be
Integer;
assume
A1: x
=
[I,
{} ,
<*k*>];
then
consider f be
FinSequence of
INT such that
A2: f
= (x
`3_3 ) and
A3: (x
const_INT )
= (f
/. 1) by
Def3;
k is
Element of
INT & f
=
<*k*> by
A1,
A2,
INT_1:def 2;
hence thesis by
A3,
FINSEQ_4: 16;
end;
definition
let x be
Element of
SCMPDS-Instr ;
given mk be
Element of
SCM-Data-Loc , r be
Integer, I such that
A1: x
=
[I,
{} ,
<*mk, r*>];
::
SCMPDS_I:def4
func x
P21address ->
Element of
SCM-Data-Loc means
:
Def4: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 1);
existence
proof
take mk,
<*mk, r*>;
r
in
INT by
INT_1:def 2;
then mk is
Element of (
SCM-Data-Loc
\/
INT ) & r is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
hence thesis by
A1,
FINSEQ_4: 17;
end;
uniqueness ;
::
SCMPDS_I:def5
func x
P22const ->
Integer means
:
Def5: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 2);
existence
proof
take r,
<*mk, r*>;
r
in
INT by
INT_1:def 2;
then mk is
Element of (
SCM-Data-Loc
\/
INT ) & r is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
hence thesis by
A1,
FINSEQ_4: 17;
end;
uniqueness ;
end
theorem ::
SCMPDS_I:5
for x be
Element of
SCMPDS-Instr , mk be
Element of
SCM-Data-Loc , r be
Integer st x
=
[I,
{} ,
<*mk, r*>] holds (x
P21address )
= mk & (x
P22const )
= r
proof
let x be
Element of
SCMPDS-Instr , mk be
Element of
SCM-Data-Loc , r be
Integer;
r
in
INT by
INT_1:def 2;
then
A1: mk is
Element of (
SCM-Data-Loc
\/
INT ) & r is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
assume
A2: x
=
[I,
{} ,
<*mk, r*>];
then
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A3: f
= (x
`3_3 ) and
A4: (x
P21address )
= (f
/. 1) by
Def4;
f
=
<*mk, r*> by
A2,
A3;
hence (x
P21address )
= mk by
A4,
A1,
FINSEQ_4: 17;
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A5: f
= (x
`3_3 ) and
A6: (x
P22const )
= (f
/. 2) by
A2,
Def5;
f
=
<*mk, r*> by
A2,
A5;
hence thesis by
A1,
A6,
FINSEQ_4: 17;
end;
definition
let x be
Element of
SCMPDS-Instr ;
given m1 be
Element of
SCM-Data-Loc , k1,k2 be
Integer, I such that
A1: x
=
[I,
{} ,
<*m1, k1, k2*>];
::
SCMPDS_I:def6
func x
P31address ->
Element of
SCM-Data-Loc means
:
Def6: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 1);
existence
proof
reconsider mm = m1, k1, k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take m1, f =
<*mm, k1, k2*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 18;
end;
uniqueness ;
::
SCMPDS_I:def7
func x
P32const ->
Integer means
:
Def7: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 2);
existence
proof
reconsider m1, mm = k1, k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take k1, f =
<*m1, mm, k2*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 18;
end;
uniqueness ;
::
SCMPDS_I:def8
func x
P33const ->
Integer means
:
Def8: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 3);
existence
proof
reconsider m1, k1, mm = k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take k2, f =
<*m1, k1, mm*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 18;
end;
uniqueness ;
end
theorem ::
SCMPDS_I:6
for x be
Element of
SCMPDS-Instr , d1 be
Element of
SCM-Data-Loc , k1,k2 be
Integer st x
=
[I,
{} ,
<*d1, k1, k2*>] holds (x
P31address )
= d1 & (x
P32const )
= k1 & (x
P33const )
= k2
proof
let x be
Element of
SCMPDS-Instr , d1 be
Element of
SCM-Data-Loc , k1,k2 be
Integer;
k1
in
INT by
INT_1:def 2;
then
A1: d1 is
Element of (
SCM-Data-Loc
\/
INT ) & k1 is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
k2
in
INT by
INT_1:def 2;
then
A2: k2 is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
assume
A3: x
=
[I,
{} ,
<*d1, k1, k2*>];
then
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A4: f
= (x
`3_3 ) and
A5: (x
P31address )
= (f
/. 1) by
Def6;
f
=
<*d1, k1, k2*> by
A3,
A4;
hence (x
P31address )
= d1 by
A1,
A2,
A5,
FINSEQ_4: 18;
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A6: f
= (x
`3_3 ) and
A7: (x
P32const )
= (f
/. 2) by
A3,
Def7;
f
=
<*d1, k1, k2*> by
A3,
A6;
hence (x
P32const )
= k1 by
A1,
A2,
A7,
FINSEQ_4: 18;
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A8: f
= (x
`3_3 ) and
A9: (x
P33const )
= (f
/. 3) by
A3,
Def8;
f
=
<*d1, k1, k2*> by
A3,
A8;
hence thesis by
A1,
A2,
A9,
FINSEQ_4: 18;
end;
definition
let x be
Element of
SCMPDS-Instr ;
given m1,m2 be
Element of
SCM-Data-Loc , k1,k2 be
Integer, I such that
A1: x
=
[I,
{} ,
<*m1, m2, k1, k2*>];
::
SCMPDS_I:def9
func x
P41address ->
Element of
SCM-Data-Loc means
:
Def9: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 1);
existence
proof
reconsider mm = m1, m2, k1, k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take m1, f =
<*mm, m2, k1, k2*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 80;
end;
uniqueness ;
::
SCMPDS_I:def10
func x
P42address ->
Element of
SCM-Data-Loc means
:
Def10: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 2);
existence
proof
reconsider m1, mm = m2, k1, k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take m2, f =
<*m1, mm, k1, k2*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 80;
end;
uniqueness ;
::
SCMPDS_I:def11
func x
P43const ->
Integer means
:
Def11: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 3);
existence
proof
reconsider m1, m2, mm = k1, k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take k1, f =
<*m1, m2, mm, k2*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 80;
end;
uniqueness ;
::
SCMPDS_I:def12
func x
P44const ->
Integer means
:
Def12: ex f be
FinSequence of (
SCM-Data-Loc
\/
INT ) st f
= (x
`3_3 ) & it
= (f
/. 4);
existence
proof
reconsider m1, m2, k1, mm = k2 as
Element of (
SCM-Data-Loc
\/
INT ) by
Th1,
XBOOLE_0:def 3;
take k2, f =
<*m1, m2, k1, mm*>;
thus f
= (x
`3_3 ) by
A1;
thus thesis by
FINSEQ_4: 80;
end;
uniqueness ;
end
theorem ::
SCMPDS_I:7
for x be
Element of
SCMPDS-Instr , d1,d2 be
Element of
SCM-Data-Loc , k1,k2 be
Integer st x
=
[I,
{} ,
<*d1, d2, k1, k2*>] holds (x
P41address )
= d1 & (x
P42address )
= d2 & (x
P43const )
= k1 & (x
P44const )
= k2
proof
let x be
Element of
SCMPDS-Instr , d1,d2 be
Element of
SCM-Data-Loc , k1,k2 be
Integer;
A1: d1 is
Element of (
SCM-Data-Loc
\/
INT ) & d2 is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
k1
in
INT by
INT_1:def 2;
then
A2: k1 is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
k2
in
INT by
INT_1:def 2;
then
A3: k2 is
Element of (
SCM-Data-Loc
\/
INT ) by
XBOOLE_0:def 3;
assume
A4: x
=
[I,
{} ,
<*d1, d2, k1, k2*>];
then
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A5: f
= (x
`3_3 ) and
A6: (x
P41address )
= (f
/. 1) by
Def9;
f
=
<*d1, d2, k1, k2*> by
A4,
A5;
hence (x
P41address )
= d1 by
A1,
A2,
A3,
A6,
FINSEQ_4: 80;
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A7: f
= (x
`3_3 ) and
A8: (x
P42address )
= (f
/. 2) by
A4,
Def10;
f
=
<*d1, d2, k1, k2*> by
A4,
A7;
hence (x
P42address )
= d2 by
A1,
A2,
A3,
A8,
FINSEQ_4: 80;
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A9: f
= (x
`3_3 ) and
A10: (x
P43const )
= (f
/. 3) by
A4,
Def11;
f
=
<*d1, d2, k1, k2*> by
A4,
A9;
hence (x
P43const )
= k1 by
A1,
A2,
A3,
A10,
FINSEQ_4: 80;
consider f be
FinSequence of (
SCM-Data-Loc
\/
INT ) such that
A11: f
= (x
`3_3 ) and
A12: (x
P44const )
= (f
/. 4) by
A4,
Def12;
f
=
<*d1, d2, k1, k2*> by
A4,
A11;
hence thesis by
A1,
A2,
A3,
A12,
FINSEQ_4: 80;
end;
definition
::
SCMPDS_I:def13
func
RetSP ->
Element of
NAT equals
0 ;
coherence ;
::
SCMPDS_I:def14
func
RetIC ->
Element of
NAT equals 1;
coherence ;
end
theorem ::
SCMPDS_I:8
Th8: for x be
Element of
SCMPDS-Instr holds x
in
{
[
0 ,
{} ,
{} ]} & (
InsCode x)
=
0 or x
in the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT & (
InsCode x)
= 14 or x
in the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc & (
InsCode x)
= 1 or x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} } & ((
InsCode x)
= 2 or (
InsCode x)
= 3) or x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} } & ((
InsCode x)
= 4 or (
InsCode x)
= 5 or (
InsCode x)
= 6 or (
InsCode x)
= 7 or (
InsCode x)
= 8) or x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} } & ((
InsCode x)
= 9 or (
InsCode x)
= 10 or (
InsCode x)
= 11 or (
InsCode x)
= 12 or (
InsCode x)
= 13)
proof
let x be
Element of
SCMPDS-Instr ;
x
in ((((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} })
\/ {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} }) or x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} } by
XBOOLE_0:def 3;
then x
in (((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} }) or x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} } or x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} } by
XBOOLE_0:def 3;
then x
in ((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc ) or x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} } or x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} } or x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} } by
XBOOLE_0:def 3;
then x
in (
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT ) or x
in the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc or x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} } or x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} } or x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} } by
XBOOLE_0:def 3;
per cases by
XBOOLE_0:def 3;
case x
in
{
[
0 ,
{} ,
{} ]};
then x
=
[
0 ,
{} ,
{} ] by
TARSKI:def 1;
hence thesis;
end;
case x
in the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT ;
then ex l be
Element of
INT st x
=
[14,
{} ,
<*l*>];
hence thesis;
end;
case x
in the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc ;
then ex sp be
Element of
SCM-Data-Loc st x
=
[1,
{} ,
<*sp*>];
hence thesis;
end;
case x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} };
then
consider I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT such that
A1: x
=
[I,
{} ,
<*v, c*>] and
A2: I
in
{2, 3};
(
InsCode x)
= I by
A1;
hence thesis by
A2,
TARSKI:def 2;
end;
case x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} };
then
consider I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT such that
A3: x
=
[I,
{} ,
<*v, c1, c2*>] and
A4: I
in
{4, 5, 6, 7, 8};
(
InsCode x)
= I by
A3;
hence thesis by
A4,
ENUMSET1:def 3;
end;
case x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} };
then
consider I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT such that
A5: x
=
[I,
{} ,
<*v1, v2, c1, c2*>] and
A6: I
in
{9, 10, 11, 12, 13};
(
InsCode x)
= I by
A5;
hence thesis by
A6,
ENUMSET1:def 3;
end;
end;
begin
reserve x for
set,
k for
Element of
NAT ;
registration
cluster (
proj2
SCMPDS-Instr ) ->
FinSequence-membered;
coherence
proof
let f be
object;
assume f
in (
proj2
SCMPDS-Instr );
then
consider y be
object such that
A1:
[y, f]
in
SCMPDS-Instr by
XTUPLE_0:def 13;
set x =
[y, f];
per cases by
A1,
XBOOLE_0:def 3;
suppose
A2: x
in ((((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} })
\/ {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} });
per cases by
A2,
XBOOLE_0:def 3;
suppose x
in (((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} });
then x
in ((
{
[
0 ,
{} ,
{} ]}
\/ ( the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc ))
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} }) by
XBOOLE_1: 4;
then x
in (
{
[
0 ,
{} ,
{} ]}
\/ ( the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )) or x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} } by
XBOOLE_0:def 3;
per cases by
XBOOLE_0:def 3;
suppose x
in
{
[
0 ,
{} ,
{} ]};
then x
=
[
0 ,
{} ,
{} ] by
TARSKI:def 1;
hence f is
FinSequence by
XTUPLE_0: 1;
end;
suppose
A3: x
in ( the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc );
per cases by
A3,
XBOOLE_0:def 3;
suppose x
in the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT ;
then ex l be
Element of
INT st x
=
[14,
{} ,
<*l*>];
hence f is
FinSequence by
XTUPLE_0: 1;
end;
suppose x
in the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc ;
then ex sp be
Element of
SCM-Data-Loc st x
=
[1,
{} ,
<*sp*>];
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
suppose x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} };
then ex I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT st x
=
[I,
{} ,
<*v, c*>] & I
in
{2, 3};
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
suppose x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} };
then ex I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT st x
=
[I,
{} ,
<*v, c1, c2*>] & I
in
{4, 5, 6, 7, 8};
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
suppose x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} };
then ex I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT st x
=
[I,
{} ,
<*v1, v2, c1, c2*>] & I
in
{9, 10, 11, 12, 13};
hence f is
FinSequence by
XTUPLE_0: 1;
end;
end;
end
registration
cluster
SCMPDS-Instr ->
standard-ins;
coherence
proof
consider X be non
empty
set such that
A1: (
proj2
SCMPDS-Instr )
c= (X
* ) by
FINSEQ_1: 85;
take X;
let x be
object;
assume
A2: x
in
SCMPDS-Instr ;
A3:
{}
in (
NAT
* ) by
FINSEQ_1: 49;
per cases by
A2,
XBOOLE_0:def 3;
suppose x
in ((((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} })
\/ {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} });
per cases by
XBOOLE_0:def 3;
suppose
A4: x
in (((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc )
\/ {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} });
per cases by
A4,
XBOOLE_0:def 3;
suppose
A5: x
in ((
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT )
\/ the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc );
per cases by
A5,
XBOOLE_0:def 3;
suppose x
in (
{
[
0 ,
{} ,
{} ]}
\/ the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT );
per cases by
XBOOLE_0:def 3;
suppose x
in
{
[
0 ,
{} ,
{} ]};
then
A6: x
=
[
0 ,
{} ,
{} ] by
TARSKI:def 1;
{}
in (X
* ) by
FINSEQ_1: 49;
hence x
in
[:
NAT , (
NAT
* ), (X
* ):] by
A6,
A3,
MCART_1: 69;
end;
suppose x
in the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT ;
then
consider l be
Element of
INT such that
A7: x
=
[14,
{} ,
<*l*>];
<*l*>
in (
proj2
SCMPDS-Instr ) by
A2,
A7,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (X
* ):] by
A1,
A7,
A3,
MCART_1: 69;
end;
end;
suppose x
in the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc ;
then
consider sp be
Element of
SCM-Data-Loc such that
A8: x
=
[1,
{} ,
<*sp*>];
<*sp*>
in (
proj2
SCMPDS-Instr ) by
A2,
A8,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (X
* ):] by
A1,
A8,
A3,
MCART_1: 69;
end;
end;
suppose x
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} };
then
consider I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT such that
A9: x
=
[I,
{} ,
<*v, c*>] & I
in
{2, 3};
<*v, c*>
in (
proj2
SCMPDS-Instr ) by
A2,
A9,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (X
* ):] by
A1,
A9,
A3,
MCART_1: 69;
end;
end;
suppose x
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} };
then
consider I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT such that
A10: x
=
[I,
{} ,
<*v, c1, c2*>] & I
in
{4, 5, 6, 7, 8};
<*v, c1, c2*>
in (
proj2
SCMPDS-Instr ) by
A2,
A10,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (X
* ):] by
A1,
A10,
A3,
MCART_1: 69;
end;
end;
suppose x
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} };
then
consider I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT such that
A11: x
=
[I,
{} ,
<*v1, v2, c1, c2*>] & I
in
{9, 10, 11, 12, 13};
<*v1, v2, c1, c2*>
in (
proj2
SCMPDS-Instr ) by
A2,
A11,
XTUPLE_0:def 13;
hence x
in
[:
NAT , (
NAT
* ), (X
* ):] by
A1,
A11,
A3,
MCART_1: 69;
end;
end;
end
Lm2: for l be
Element of
SCMPDS-Instr holds (
InsCode l)
<= 14
proof
let l be
Element of
SCMPDS-Instr ;
(
InsCode l)
=
0 or ... or (
InsCode l)
= 14 by
Th8;
hence thesis;
end;
Lm3: for i be
Element of
SCMPDS-Instr st (
InsCode i)
=
0 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCMPDS-Instr ;
assume (
InsCode i)
=
0 ;
then i
in
{
[
0 ,
{} ,
{} ]} by
Th8;
then i
=
[
0 ,
{} ,
{} ] by
TARSKI:def 1;
hence thesis;
end;
Lm4: for i be
Element of
SCMPDS-Instr st (
InsCode i)
= 14 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCMPDS-Instr ;
assume (
InsCode i)
= 14;
then i
in the set of all
[14,
{} ,
<*l*>] where l be
Element of
INT by
Th8;
then ex l be
Element of
INT st i
=
[14,
{} ,
<*l*>];
hence thesis;
end;
Lm5: for i be
Element of
SCMPDS-Instr st (
InsCode i)
= 1 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCMPDS-Instr ;
assume (
InsCode i)
= 1;
then i
in the set of all
[1,
{} ,
<*sp*>] where sp be
Element of
SCM-Data-Loc by
Th8;
then ex sp be
Element of
SCM-Data-Loc st i
=
[1,
{} ,
<*sp*>];
hence thesis;
end;
Lm6: for i be
Element of
SCMPDS-Instr st (
InsCode i)
= 2 or (
InsCode i)
= 3 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCMPDS-Instr ;
assume (
InsCode i)
= 2 or (
InsCode i)
= 3;
then i
in {
[I,
{} ,
<*v, c*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT : I
in
{2, 3} } by
Th8;
then ex I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c be
Element of
INT st i
=
[I,
{} ,
<*v, c*>] & I
in
{2, 3};
hence thesis;
end;
Lm7: for i be
Element of
SCMPDS-Instr st (
InsCode i)
= 4 or (
InsCode i)
= 5 or (
InsCode i)
= 6 or (
InsCode i)
= 7 or (
InsCode i)
= 8 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCMPDS-Instr ;
assume (
InsCode i)
= 4 or (
InsCode i)
= 5 or (
InsCode i)
= 6 or (
InsCode i)
= 7 or (
InsCode i)
= 8;
then i
in {
[I,
{} ,
<*v, c1, c2*>] where I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{4, 5, 6, 7, 8} } by
Th8;
then ex I be
Element of (
Segm 15), v be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT st i
=
[I,
{} ,
<*v, c1, c2*>] & I
in
{4, 5, 6, 7, 8};
hence thesis;
end;
Lm8: for i be
Element of
SCMPDS-Instr st (
InsCode i)
= 9 or (
InsCode i)
= 10 or (
InsCode i)
= 11 or (
InsCode i)
= 12 or (
InsCode i)
= 13 holds (
JumpPart i)
=
{}
proof
let i be
Element of
SCMPDS-Instr ;
assume (
InsCode i)
= 9 or (
InsCode i)
= 10 or (
InsCode i)
= 11 or (
InsCode i)
= 12 or (
InsCode i)
= 13;
then i
in {
[I,
{} ,
<*v1, v2, c1, c2*>] where I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT : I
in
{9, 10, 11, 12, 13} } by
Th8;
then ex I be
Element of (
Segm 15), v1,v2 be
Element of
SCM-Data-Loc , c1,c2 be
Element of
INT st i
=
[I,
{} ,
<*v1, v2, c1, c2*>] & I
in
{9, 10, 11, 12, 13};
hence thesis;
end;
registration
cluster
SCMPDS-Instr ->
homogeneous;
coherence
proof
let i,j be
Element of
SCMPDS-Instr ;
assume
A1: (
InsCode i)
= (
InsCode j);
(
InsCode i)
=
0 or ... or (
InsCode i)
= 14 by
Lm2,
NAT_1: 60;
per cases ;
suppose (
InsCode i)
=
0 ;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm3;
hence thesis;
end;
suppose (
InsCode i)
= 14;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm4;
hence thesis;
end;
suppose (
InsCode i)
= 1;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm5;
hence thesis;
end;
suppose (
InsCode i)
= 2 or (
InsCode i)
= 3;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm6;
hence thesis;
end;
suppose (
InsCode i)
= 4 or (
InsCode i)
= 5 or (
InsCode i)
= 6 or (
InsCode i)
= 7 or (
InsCode i)
= 8;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm7;
hence thesis;
end;
suppose (
InsCode i)
= 9 or (
InsCode i)
= 10 or (
InsCode i)
= 11 or (
InsCode i)
= 12 or (
InsCode i)
= 13;
then (
JumpPart i)
=
{} & (
JumpPart j)
=
{} by
A1,
Lm8;
hence thesis;
end;
end;
end
registration
cluster
SCMPDS-Instr ->
J/A-independent;
coherence
proof
let T be
InsType of
SCMPDS-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
SCMPDS-Instr ;
reconsider i =
[T, f1, p] as
Element of
SCMPDS-Instr by
A3;
(
InsCode i)
=
0 or ... or (
InsCode i)
= 14 by
Lm2,
NAT_1: 60;
then
A4: (
JumpPart i)
=
{} by
Lm4,
Lm5,
Lm6,
Lm7,
Lm8,
Lm3;
T
= (
InsCode i);
then
A5: (
JumpParts T)
=
{
0 } by
A4,
COMPOS_0: 11;
f1
=
0 by
A5,
A1,
TARSKI:def 1;
then f1
= f2 by
A2;
hence
[T, f2, p]
in
SCMPDS-Instr by
A3;
end;
end
registration
cluster
SCMPDS-Instr ->
with_halt;
coherence by
Lm1;
end