:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

notation
synonym  SCM-Halt for  {} ;
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
func SCM-Data-Loc  ->  set  equals :: SCM_INST:def 1
[:{1},NAT:];
coherence
 [:{1},NAT:] is set ;
end;

:: deftheorem  defines SCM-Data-Loc SCM_INST:def_1_:_
 SCM-Data-Loc = [:{1},NAT:];

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
(({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of 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 Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of 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 = (({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of 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
[0,{},{}] in SCM-Instr
proofend;

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

theorem Th2: :: SCM_INST:2
for a2 being Element of NAT holds [6,<*a2*>,{}] in SCM-Instr
proofend;

theorem Th3: :: SCM_INST:3
for x being set
for a2 being Element of NAT
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
proofend;

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
proofend;

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*>] ;
funcx 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 &amp; 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 &amp; b1 = f /. 1 )
proofend;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b1 = f /. 1 ) &amp; ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b2 = f /. 1 ) holds
b1 = b2 ;
funcx 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 &amp; 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 &amp; b1 = f /. 2 )
proofend;
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 &amp; b1 = f /. 2 ) &amp; ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; 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 &amp; 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 &amp; 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
( x address_1 = mk &amp; x address_2 = ml )
proofend;

definition
let x be Element of SCM-Instr ;
given mk being Element of NAT , I being Element of Segm 9 such that A1: x = [I,<*mk*>,{}] ;
funcx jump_address  ->  Element of NAT  means :Def5: :: SCM_INST:def 5
 ex f being FinSequence of NAT st
( f = x `2_3 &amp; it = f /. 1 );
existence
 ex b1 being Element of NAT ex f being FinSequence of NAT st
( f = x `2_3 &amp; b1 = f /. 1 )
proofend;
correctness
uniqueness
for b1, b2 being Element of NAT st ex f being FinSequence of NAT st
( f = x `2_3 &amp; b1 = f /. 1 ) &amp; ex f being FinSequence of NAT st
( f = x `2_3 &amp; 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 Element of NAT ex I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
for b2 being Element of NAT holds
( b2 = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 &amp; b2 = f /. 1 ) );

theorem :: SCM_INST:6
for x being Element of SCM-Instr
for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
proofend;

definition
let x be Element of SCM-Instr ;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk*>,<*ml*>] ;
funcx cjump_address  ->  Element of NAT  means :Def6: :: SCM_INST:def 6
 ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; it = <*mk*> /. 1 );
existence
 ex b1, mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b1 = <*mk*> /. 1 )
proofend;
correctness
uniqueness
for b1, b2 being Element of NAT st ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b1 = <*mk*> /. 1 ) &amp; ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b2 = <*mk*> /. 1 ) holds
b1 = b2;
;
funcx 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 &amp; it = <*ml*> /. 1 );
existence
 ex b1, ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; b1 = <*ml*> /. 1 )
proofend;
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 &amp; b1 = <*ml*> /. 1 ) &amp; ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; 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 Element of 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 NAT holds
( b2 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b2 = <*mk*> /. 1 ) );

:: deftheorem Def7 defines cond_address SCM_INST:def_7_:_
 for x being Element of SCM-Instr st ex mk being Element of 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 &amp; b2 = <*ml*> /. 1 ) );

theorem :: SCM_INST:7
for x being Element of SCM-Instr
for mk being Element of 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 &amp; x cond_address = ml )
proofend;

theorem Th8: :: SCM_INST:8
SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):]
proofend;

registration
cluster proj2 SCM-Instr ->  FinSequence-membered ;
coherence
 proj2 SCM-Instr is FinSequence-membered
proofend;
end;

theorem Th9: :: SCM_INST:9
for x being Element of SCM-Instr holds
( ( x in {[SCM-Halt,{},{}]} &amp; InsCode x = 0 ) or ( x in  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  &amp; InsCode x = 6 ) or ( x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  &amp; ( 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}  }  &amp; ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) ) )
proofend;

begin

registration
cluster SCM-Instr  ->  non empty standard-ins ;
coherence
 SCM-Instr is standard-ins
proofend;
end;

theorem Th10: :: SCM_INST:10
for l being Element of SCM-Instr holds InsCode l <= 8
proofend;

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 = {}
proofend;

Lm2:  for i being Element of SCM-Instr st ( InsCode i = 7 or InsCode i = 8 ) holds
dom (JumpPart i) = Seg 1
proofend;

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

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

Lm4:  for T being InsType of SCM-Instr holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
proofend;

Lm5:  for T being InsType of SCM-Instr st T = 0 holds
JumpParts T = {0}
proofend;

Lm6:  for T being InsType of SCM-Instr st ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) holds
JumpParts T = {{}}
proofend;

registration
cluster SCM-Instr  ->  non empty J/A-independent ;
coherence
 SCM-Instr is J/A-independent
proofend;
end;

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