:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received December 29, 1992

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

definition

:: original: SCM-Halt

redefine func SCM-Halt -> Element of Segm 9;

correctness

coherence

SCM-Halt is Element of Segm 9;

by NAT_1:44;

end;
redefine func SCM-Halt -> Element of Segm 9;

correctness

coherence

SCM-Halt is Element of Segm 9;

by NAT_1:44;

definition
end;

definition

(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } is non empty set ;

end;

func SCM-Instr -> non empty set equals :: SCM_INST:def 2

(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;

coherence (({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;

(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } is non empty set ;

:: deftheorem defines SCM-Instr SCM_INST:def 2 :

SCM-Instr = (({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;

SCM-Instr = (({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;

theorem Th3: :: SCM_INST:3

for x being set

for a2 being Nat

for b2 being Element of SCM-Data-Loc st x in {7,8} holds

[x,<*a2*>,<*b2*>] in SCM-Instr

for a2 being Nat

for b2 being Element of SCM-Data-Loc st x in {7,8} holds

[x,<*a2*>,<*b2*>] in SCM-Instr

proof end;

theorem Th4: :: SCM_INST:4

for x being set

for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds

[x,{},<*b1,c1*>] in SCM-Instr

for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds

[x,{},<*b1,c1*>] in SCM-Instr

proof end;

definition

let x be Element of SCM-Instr ;

given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 9 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 )

uniqueness

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;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,{},<*mk,ml*>] ;

func x address_1 -> Element of SCM-Data-Loc means :Def3: :: SCM_INST:def 3

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 :Def4: :: SCM_INST:def 4

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;

correctness uniqueness

for b

( f = x `3_3 & b

( f = x `3_3 & b

b

;

:: deftheorem Def3 defines address_1 SCM_INST:def 3 :

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

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

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

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

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

for b

( b

( f = x `3_3 & b

:: deftheorem Def4 defines address_2 SCM_INST:def 4 :

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

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

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

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

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

for b

( b

( f = x `3_3 & b

theorem :: SCM_INST:5

for x being Element of SCM-Instr

for mk, ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds

( x address_1 = mk & x address_2 = ml )

for mk, ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds

( x address_1 = mk & x address_2 = ml )

proof end;

definition

let x be Element of SCM-Instr ;

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

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

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

uniqueness

for b_{1}, b_{2} being 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;
given mk being Nat, I being Element of Segm 9 such that A1: x = [I,<*mk*>,{}] ;

func x jump_address -> Nat means :Def5: :: SCM_INST:def 5

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;

correctness uniqueness

for b

( f = x `2_3 & b

( f = x `2_3 & b

b

;

:: deftheorem Def5 defines jump_address SCM_INST:def 5 :

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

for b_{2} being Nat holds

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

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

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

for b

( b

( f = x `2_3 & b

theorem :: SCM_INST:6

for x being Element of SCM-Instr

for mk being Nat

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

x jump_address = mk

for mk being Nat

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

x jump_address = mk

proof end;

definition

let x be Element of SCM-Instr ;

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

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

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

uniqueness

for b_{1}, b_{2} being 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 )

uniqueness

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;
given mk being Nat, ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk*>,<*ml*>] ;

func x cjump_address -> Nat means :Def6: :: SCM_INST:def 6

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;

correctness uniqueness

for b

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

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

b

;

func x cond_address -> Element of SCM-Data-Loc means :Def7: :: SCM_INST:def 7

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;

correctness uniqueness

for b

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

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

b

;

:: deftheorem Def6 defines cjump_address SCM_INST:def 6 :

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

for b_{2} being Nat holds

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

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

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

for b

( b

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

:: deftheorem Def7 defines cond_address SCM_INST:def 7 :

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

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

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

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

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

for b

( b

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

theorem :: SCM_INST:7

for x being Element of SCM-Instr

for mk being Nat

for ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

for mk being Nat

for ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

proof end;

theorem Th9: :: SCM_INST:9

for x being Element of SCM-Instr holds

( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } & InsCode x = 6 ) or ( x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } & ( InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : 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 ) ) )

( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } & InsCode x = 6 ) or ( x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } & ( InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : 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 end;

registration
end;

Lm1: for i being 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 end;

Lm2: for i being Element of SCM-Instr st ( InsCode i = 7 or InsCode i = 8 ) holds

dom (JumpPart i) = Seg 1

proof end;

Lm3: for i being Element of SCM-Instr st InsCode i = 6 holds

dom (JumpPart i) = Seg 1

proof end;

registration
end;

Lm4: for T being InsType of SCM-Instr holds

not not T = 0 & ... & not T = 8

proof end;

Lm5: for T being InsType of SCM-Instr st T = 0 holds

JumpParts T = {{}}

proof end;

Lm6: for T being InsType of SCM-Instr st not not T = 1 & ... & not T = 5 holds

JumpParts T = {{}}

proof end;

registration
end;

registration
end;