:: by Artur Korni{\l}owicz

::

:: Received November 29, 1998

:: Copyright (c) 1998-2018 Association of Mizar Users

definition

let S be non empty 1-sorted ;

((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } is non empty set ;

end;
func SCM-Instr S -> non empty set equals :: SCMRINGI:def 1

((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;

coherence ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;

((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } is non empty set ;

:: deftheorem defines SCM-Instr SCMRINGI:def 1 :

for S being non empty 1-sorted holds SCM-Instr S = ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;

for S being non empty 1-sorted holds SCM-Instr S = ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;

definition

let S be non empty 1-sorted ;

let x be Element of SCM-Instr S;

given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,{},<*mk,ml*>] ;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{1} = f /. 2 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{1} = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{2} = f /. 2 ) holds

b_{1} = b_{2}
;

end;
let x be Element of SCM-Instr S;

given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,{},<*mk,ml*>] ;

func x address_1 -> Element of SCM-Data-Loc means :Def2: :: SCMRINGI:def 2

ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x address_2 -> Element of SCM-Data-Loc means :Def3: :: SCMRINGI:def 3

ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & it = f /. 2 );

existence ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & it = f /. 2 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def2 defines address_1 SCMRINGI:def 2 :

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds

for b_{3} being Element of SCM-Data-Loc holds

( b_{3} = x address_1 iff ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{3} = f /. 1 ) );

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def3 defines address_2 SCMRINGI:def 3 :

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds

for b_{3} being Element of SCM-Data-Loc holds

( b_{3} = x address_2 iff ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{3} = f /. 2 ) );

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMRINGI:1

for I being Element of Segm 8

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds

( x address_1 = mk & x address_2 = ml )

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds

( x address_1 = mk & x address_2 = ml )

proof end;

definition

let R be non empty 1-sorted ;

let x be Element of SCM-Instr R;

given mk being Element of NAT , I being Element of Segm 8 such that A1: x = [I,<*mk*>,{}] ;

ex b_{1} being Element of NAT ex f being FinSequence of NAT st

( f = x `2_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of NAT st ex f being FinSequence of NAT st

( f = x `2_3 & b_{1} = f /. 1 ) & ex f being FinSequence of NAT st

( f = x `2_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

end;
let x be Element of SCM-Instr R;

given mk being Element of NAT , I being Element of Segm 8 such that A1: x = [I,<*mk*>,{}] ;

func x jump_address -> Element of NAT means :Def4: :: SCMRINGI:def 4

ex f being FinSequence of NAT st

( f = x `2_3 & it = f /. 1 );

existence ex f being FinSequence of NAT st

( f = x `2_3 & it = f /. 1 );

ex b

( f = x `2_3 & b

proof end;

uniqueness for b

( f = x `2_3 & b

( f = x `2_3 & b

b

:: deftheorem Def4 defines jump_address SCMRINGI:def 4 :

for R being non empty 1-sorted

for x being Element of SCM-Instr R st ex mk being Element of NAT ex I being Element of Segm 8 st x = [I,<*mk*>,{}] holds

for b_{3} being Element of NAT holds

( b_{3} = x jump_address iff ex f being FinSequence of NAT st

( f = x `2_3 & b_{3} = f /. 1 ) );

for R being non empty 1-sorted

for x being Element of SCM-Instr R st ex mk being Element of NAT ex I being Element of Segm 8 st x = [I,<*mk*>,{}] holds

for b

( b

( f = x `2_3 & b

theorem :: SCMRINGI:2

for I being Element of Segm 8

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk being Nat st x = [I,<*mk*>,{}] holds

x jump_address = mk

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk being Nat st x = [I,<*mk*>,{}] holds

x jump_address = mk

proof end;

definition

let S be non empty 1-sorted ;

let x be Element of SCM-Instr S;

given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk*>,<*ml*>] ;

ex b_{1}, mk being Element of NAT st

( <*mk*> = x `2_3 & b_{1} = <*mk*> /. 1 )

for b_{1}, b_{2} being Element of NAT st ex mk being Element of NAT st

( <*mk*> = x `2_3 & b_{1} = <*mk*> /. 1 ) & ex mk being Element of NAT st

( <*mk*> = x `2_3 & b_{2} = <*mk*> /. 1 ) holds

b_{1} = b_{2}
;

ex b_{1}, ml being Element of SCM-Data-Loc st

( <*ml*> = x `3_3 & b_{1} = <*ml*> /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st

( <*ml*> = x `3_3 & b_{1} = <*ml*> /. 1 ) & ex ml being Element of SCM-Data-Loc st

( <*ml*> = x `3_3 & b_{2} = <*ml*> /. 1 ) holds

b_{1} = b_{2}
;

end;
let x be Element of SCM-Instr S;

given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk*>,<*ml*>] ;

func x cjump_address -> Element of NAT means :Def5: :: SCMRINGI:def 5

ex mk being Element of NAT st

( <*mk*> = x `2_3 & it = <*mk*> /. 1 );

existence ex mk being Element of NAT st

( <*mk*> = x `2_3 & it = <*mk*> /. 1 );

ex b

( <*mk*> = x `2_3 & b

proof end;

uniqueness for b

( <*mk*> = x `2_3 & b

( <*mk*> = x `2_3 & b

b

func x cond_address -> Element of SCM-Data-Loc means :Def6: :: SCMRINGI:def 6

ex ml being Element of SCM-Data-Loc st

( <*ml*> = x `3_3 & it = <*ml*> /. 1 );

existence ex ml being Element of SCM-Data-Loc st

( <*ml*> = x `3_3 & it = <*ml*> /. 1 );

ex b

( <*ml*> = x `3_3 & b

proof end;

uniqueness for b

( <*ml*> = x `3_3 & b

( <*ml*> = x `3_3 & b

b

:: deftheorem Def5 defines cjump_address SCMRINGI:def 5 :

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds

for b_{3} being Element of NAT holds

( b_{3} = x cjump_address iff ex mk being Element of NAT st

( <*mk*> = x `2_3 & b_{3} = <*mk*> /. 1 ) );

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds

for b

( b

( <*mk*> = x `2_3 & b

:: deftheorem Def6 defines cond_address SCMRINGI:def 6 :

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds

for b_{3} being Element of SCM-Data-Loc holds

( b_{3} = x cond_address iff ex ml being Element of SCM-Data-Loc st

( <*ml*> = x `3_3 & b_{3} = <*ml*> /. 1 ) );

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds

for b

( b

( <*ml*> = x `3_3 & b

theorem :: SCMRINGI:3

for I being Element of Segm 8

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk being Element of NAT

for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk being Element of NAT

for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

proof end;

definition

let S be non empty 1-sorted ;

let d be Element of SCM-Data-Loc ;

let s be Element of S;

:: original: <*

redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;

coherence

<*d,s*> is FinSequence of SCM-Data-Loc \/ the carrier of S

end;
let d be Element of SCM-Data-Loc ;

let s be Element of S;

:: original: <*

redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;

coherence

<*d,s*> is FinSequence of SCM-Data-Loc \/ the carrier of S

proof end;

definition

let S be non empty 1-sorted ;

let x be Element of SCM-Instr S;

given mk being Element of SCM-Data-Loc , r being Element of S, I being Element of Segm 8 such that A1: x = [I,{},<*mk,r*>] ;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

ex b_{1} being Element of S ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{1} = f /. 2 )

for b_{1}, b_{2} being Element of S st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{1} = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{2} = f /. 2 ) holds

b_{1} = b_{2}
;

end;
let x be Element of SCM-Instr S;

given mk being Element of SCM-Data-Loc , r being Element of S, I being Element of Segm 8 such that A1: x = [I,{},<*mk,r*>] ;

func x const_address -> Element of SCM-Data-Loc means :Def7: :: SCMRINGI:def 7

ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x const_value -> Element of S means :Def8: :: SCMRINGI:def 8

ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & it = f /. 2 );

existence ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & it = f /. 2 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def7 defines const_address SCMRINGI:def 7 :

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds

for b_{3} being Element of SCM-Data-Loc holds

( b_{3} = x const_address iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{3} = f /. 1 ) );

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def8 defines const_value SCMRINGI:def 8 :

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds

for b_{3} being Element of S holds

( b_{3} = x const_value iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st

( f = x `3_3 & b_{3} = f /. 2 ) );

for S being non empty 1-sorted

for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMRINGI:4

for I being Element of Segm 8

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk being Element of SCM-Data-Loc

for r being Element of S st x = [I,{},<*mk,r*>] holds

( x const_address = mk & x const_value = r )

for S being non empty 1-sorted

for x being Element of SCM-Instr S

for mk being Element of SCM-Data-Loc

for r being Element of S st x = [I,{},<*mk,r*>] holds

( x const_address = mk & x const_value = r )

proof end;

registration
end;

theorem Th7: :: SCMRINGI:7

for S being non empty 1-sorted

for x being Element of SCM-Instr S holds

( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Nat : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )

for x being Element of SCM-Instr S holds

( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Nat : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )

proof end;

registration

ex b_{1} being Ring st

( b_{1} is strict & b_{1} is trivial )
end;

cluster non empty trivial right_complementable strict V95() V96() V97() V106() V107() V120() for Ring;

existence ex b

( b

proof end;

Lm1: for R being Ring

for i being Element of SCM-Instr R holds InsCode i <= 7

proof end;

Lm2: for S being non empty 1-sorted

for i being Element of SCM-Instr S st not not InsCode i = 1 & ... & not InsCode i = 4 holds

JumpPart i = {}

proof end;

Lm3: for S being non empty 1-sorted

for i being Element of SCM-Instr S st InsCode i = 5 holds

JumpPart i = {}

proof end;

Lm4: for R being Ring

for I being Element of SCM-Instr R st InsCode I = 6 holds

dom (JumpPart I) = Seg 1

proof end;

Lm5: for R being Ring

for I being Element of SCM-Instr R st InsCode I = 7 holds

dom (JumpPart I) = Seg 1

proof end;

theorem :: SCMRINGI:8

for S being non empty 1-sorted

for x being set

for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

for x being set

for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

proof end;

theorem :: SCMRINGI:9

for S being non empty 1-sorted

for t being Element of S

for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S

for t being Element of S

for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S

proof end;

theorem :: SCMRINGI:11

for S being non empty 1-sorted

for d1 being Element of SCM-Data-Loc

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

for d1 being Element of SCM-Data-Loc

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

proof end;