:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Copyright (c) 1992-2018 Association of Mizar Users

notation
synonym SCM-Halt for 0 ;
end;

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;

definition
coherence
is set
;
end;

:: deftheorem defines SCM-Data-Loc SCM_INST:def 1 :

registration
cluster SCM-Data-Loc -> non empty ;
coherence
not SCM-Data-Loc is empty
;
end;

definition
func SCM-Instr -> non empty set equals :: SCM_INST:def 2
(( \/ { [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
(( \/ { [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;

:: deftheorem defines SCM-Instr SCM_INST:def 2 :
SCM-Instr = (( \/ { [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 Th1: :: SCM_INST:1
proof end;

registration
cluster SCM-Instr -> non empty ;
coherence
not SCM-Instr is empty
;
end;

theorem Th2: :: SCM_INST:2
for a2 being Nat holds [6,<*a2*>,{}] in SCM-Instr
proof end;

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
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
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*>] ;
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 b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b2 = f /. 1 ) holds
b1 = b2
;
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 b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b1 = f /. 2 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b2 = f /. 2 ) holds
b1 = b2
;
;
end;

:: 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 b2 being Element of SCM-Data-Loc holds
( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b2 = f /. 1 ) );

:: 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 b2 being Element of SCM-Data-Loc holds
( b2 = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x 3_3 & b2 = f /. 2 ) );

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
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*>,{}] ;
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 b1 being Nat ex f being FinSequence of NAT st
( f = x 2_3 & b1 = f /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Nat st ex f being FinSequence of NAT st
( f = x 2_3 & b1 = f /. 1 ) & ex f being FinSequence of NAT st
( f = x 2_3 & b2 = f /. 1 ) holds
b1 = b2
;
;
end;

:: 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 b2 being Nat holds
( b2 = x jump_address iff ex f being FinSequence of NAT st
( f = x 2_3 & b2 = f /. 1 ) );

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
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*>] ;
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 b1 being Nat ex mk being Element of NAT st
( <*mk*> = x 2_3 & b1 = <*mk*> /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Nat st ex mk being Element of NAT st
( <*mk*> = x 2_3 & b1 = <*mk*> /. 1 ) & ex mk being Element of NAT st
( <*mk*> = x 2_3 & b2 = <*mk*> /. 1 ) holds
b1 = b2
;
;
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 b1, ml being Element of SCM-Data-Loc st
( <*ml*> = x 3_3 & b1 = <*ml*> /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st
( <*ml*> = x 3_3 & b1 = <*ml*> /. 1 ) & ex ml being Element of SCM-Data-Loc st
( <*ml*> = x 3_3 & b2 = <*ml*> /. 1 ) holds
b1 = b2
;
;
end;

:: 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 b2 being Nat holds
( b2 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x 2_3 & b2 = <*mk*> /. 1 ) );

:: 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 b2 being Element of SCM-Data-Loc holds
( b2 = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b2 = <*ml*> /. 1 ) );

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
proof end;

theorem Th8: :: SCM_INST:8
proof end;

registration end;

theorem Th9: :: SCM_INST:9
for x being Element of SCM-Instr holds
( ( x in & 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
coherence
proof end;
end;

theorem Th10: :: SCM_INST:10
for l being Element of SCM-Instr holds InsCode l <= 8
proof 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 () = Seg 1

proof end;

Lm3: for i being Element of SCM-Instr st InsCode i = 6 holds
dom () = Seg 1

proof end;

registration
coherence
proof end;
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
coherence
proof end;
end;

registration
coherence by Th1;
end;