:: AMI_2 semantic presentation

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 GR_CY_1:12;
canceled;
end;

:: deftheorem AMI_2:def 1 :
canceled;

definition
func SCM-Data-Loc -> set equals :: AMI_2:def 2
{ ((2 * k) + 1) where k is Element of NAT : verum } ;
coherence
{ ((2 * k) + 1) where k is Element of NAT : verum } is set ;
func SCM-Instr-Loc -> set equals :: AMI_2:def 3
{ (2 * k) where k is Element of NAT : k > 0 } ;
coherence
{ (2 * k) where k is Element of NAT : k > 0 } is set ;
end;

:: deftheorem defines SCM-Data-Loc AMI_2:def 2 :
SCM-Data-Loc = { ((2 * k) + 1) where k is Element of NAT : verum } ;

:: deftheorem defines SCM-Instr-Loc AMI_2:def 3 :
SCM-Instr-Loc = { (2 * k) where k is Element of NAT : k > 0 } ;

definition
:: original: SCM-Data-Loc
redefine func SCM-Data-Loc -> Subset of NAT ;
coherence
SCM-Data-Loc is Subset of NAT
proof end;
:: original: SCM-Instr-Loc
redefine func SCM-Instr-Loc -> Subset of NAT ;
coherence
SCM-Instr-Loc is Subset of NAT
proof end;
end;

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

definition
func SCM-Instr -> Subset of [:(Segm 9),(((union {INT }) \/ NAT ) * ):] equals :: AMI_2:def 4
(({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of SCM-Instr-Loc : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of SCM-Instr-Loc , 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 SCM-Instr-Loc : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of SCM-Instr-Loc , 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 Subset of [:(Segm 9),(((union {INT }) \/ NAT ) * ):]
proof end;
end;

:: deftheorem defines SCM-Instr AMI_2:def 4 :
SCM-Instr = (({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of SCM-Instr-Loc : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of SCM-Instr-Loc , 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 :: AMI_2:1
canceled;

theorem :: AMI_2:2
[0,{} ] in SCM-Instr
proof end;

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

theorem :: AMI_2:3
for a2 being Element of SCM-Instr-Loc holds [6,<*a2*>] in SCM-Instr
proof end;

theorem :: AMI_2:4
for x being set
for a2 being Element of SCM-Instr-Loc
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2,b2*>] in SCM-Instr
proof end;

theorem :: AMI_2:5
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;

Lm1: now
let k be Element of NAT ;
consider i being Element of NAT such that
A1: ( k = 2 * i or k = (2 * i) + 1 ) by SCHEME1:1;
now
assume A2: k = 2 * i ;
A3: ( i = 0 or ex j being Element of NAT st i = j + 1 )
proof
assume i <> 0 ;
then consider j being Nat such that
A4: i = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
take j ;
thus i = j + 1 by A4;
end;
now
given j being Element of NAT such that A5: i = j + 1 ;
take j = j;
thus k = (2 * j) + (2 * 1) by A2, A5;
end;
hence ( k = 0 or ex j being Element of NAT st k = (2 * j) + 2 ) by A2, A3;
end;
hence ( k = 0 or ex j being Element of NAT st k = (2 * j) + 1 or ex j being Element of NAT st k = (2 * j) + 2 ) by A1;
end;

Lm2: now
let k be Element of NAT ;
thus ( ex j being Element of NAT st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 2 ) ) )
proof
given j being Element of NAT such that A1: k = (2 * j) + 1 ;
thus k <> 0 by A1;
given i being Element of NAT such that A2: k = (2 * i) + 2 ;
A3: (2 * i) + (2 * 1) = (2 * (i + 1)) + 0 ;
1 = ((2 * i) + 2) mod 2 by A1, A2, NAT_D:def 2
.= 0 by A3, NAT_D:def 2 ;
hence contradiction ;
end;
given j being Element of NAT such that A4: k = (2 * j) + (1 + 1) ;
thus k <> 0 by A4;
given i being Element of NAT such that A5: k = (2 * i) + 1 ;
A6: (2 * j) + (2 * 1) = (2 * (j + 1)) + 0 ;
1 = ((2 * j) + 2) mod 2 by A4, A5, NAT_D:def 2
.= 0 by A6, NAT_D:def 2 ;
hence contradiction ;
end;

definition
func SCM-OK -> Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } means :Def5: :: AMI_2:def 5
( it . 0 = SCM-Instr-Loc & ( for k being Element of NAT holds
( it . ((2 * k) + 1) = INT & it . ((2 * k) + 2) = SCM-Instr ) ) );
existence
ex b1 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & ( for k being Element of NAT holds
( b1 . ((2 * k) + 1) = INT & b1 . ((2 * k) + 2) = SCM-Instr ) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } st b1 . 0 = SCM-Instr-Loc & ( for k being Element of NAT holds
( b1 . ((2 * k) + 1) = INT & b1 . ((2 * k) + 2) = SCM-Instr ) ) & b2 . 0 = SCM-Instr-Loc & ( for k being Element of NAT holds
( b2 . ((2 * k) + 1) = INT & b2 . ((2 * k) + 2) = SCM-Instr ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines SCM-OK AMI_2:def 5 :
for b1 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } holds
( b1 = SCM-OK iff ( b1 . 0 = SCM-Instr-Loc & ( for k being Element of NAT holds
( b1 . ((2 * k) + 1) = INT & b1 . ((2 * k) + 2) = SCM-Instr ) ) ) );

theorem Th6: :: AMI_2:6
( SCM-Instr-Loc <> INT & SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr )
proof end;

theorem Th7: :: AMI_2:7
for i being Element of NAT holds
( SCM-OK . i = SCM-Instr-Loc iff i = 0 )
proof end;

theorem Th8: :: AMI_2:8
for i being Element of NAT holds
( SCM-OK . i = INT iff ex k being Element of NAT st i = (2 * k) + 1 )
proof end;

theorem Th9: :: AMI_2:9
for i being Element of NAT holds
( SCM-OK . i = SCM-Instr iff ex k being Element of NAT st i = (2 * k) + 2 )
proof end;

definition
mode SCM-State is Element of product SCM-OK ;
end;

theorem Th10: :: AMI_2:10
for a being Element of SCM-Data-Loc holds SCM-OK . a = INT
proof end;

theorem Th11: :: AMI_2:11
for a being Element of SCM-Instr-Loc holds SCM-OK . a = SCM-Instr
proof end;

theorem :: AMI_2:12
for a being Element of SCM-Instr-Loc
for t being Element of SCM-Data-Loc holds a <> t
proof end;

theorem Th13: :: AMI_2:13
pi (product SCM-OK ),0 = SCM-Instr-Loc
proof end;

theorem Th14: :: AMI_2:14
for a being Element of SCM-Data-Loc holds pi (product SCM-OK ),a = INT
proof end;

theorem :: AMI_2:15
for a being Element of SCM-Instr-Loc holds pi (product SCM-OK ),a = SCM-Instr
proof end;

definition
let s be SCM-State;
func IC s -> Element of SCM-Instr-Loc equals :: AMI_2:def 6
s . 0;
coherence
s . 0 is Element of SCM-Instr-Loc by Th13, CARD_3:def 6;
end;

:: deftheorem defines IC AMI_2:def 6 :
for s being SCM-State holds IC s = s . 0;

definition
let s be SCM-State;
let u be Element of SCM-Instr-Loc ;
func SCM-Chg s,u -> SCM-State equals :: AMI_2:def 7
s +* (0 .--> u);
coherence
s +* (0 .--> u) is SCM-State
proof end;
end;

:: deftheorem defines SCM-Chg AMI_2:def 7 :
for s being SCM-State
for u being Element of SCM-Instr-Loc holds SCM-Chg s,u = s +* (0 .--> u);

theorem :: AMI_2:16
for s being SCM-State
for u being Element of SCM-Instr-Loc holds (SCM-Chg s,u) . 0 = u
proof end;

theorem :: AMI_2:17
for s being SCM-State
for u being Element of SCM-Instr-Loc
for mk being Element of SCM-Data-Loc holds (SCM-Chg s,u) . mk = s . mk
proof end;

theorem :: AMI_2:18
for s being SCM-State
for u, v being Element of SCM-Instr-Loc holds (SCM-Chg s,u) . v = s . v
proof end;

definition
let s be SCM-State;
let t be Element of SCM-Data-Loc ;
let u be Integer;
func SCM-Chg s,t,u -> SCM-State equals :: AMI_2:def 8
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM-State
proof end;
end;

:: deftheorem defines SCM-Chg AMI_2:def 8 :
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds SCM-Chg s,t,u = s +* (t .--> u);

theorem :: AMI_2:19
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg s,t,u) . 0 = s . 0
proof end;

theorem :: AMI_2:20
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg s,t,u) . t = u
proof end;

theorem :: AMI_2:21
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg s,t,u) . mk = s . mk
proof end;

theorem :: AMI_2:22
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer
for v being Element of SCM-Instr-Loc holds (SCM-Chg s,t,u) . v = s . v
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 :Def9: :: AMI_2:def 9
 ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & 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 `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
func x address_2 -> Element of SCM-Data-Loc means :Def10: :: AMI_2:def 10
 ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & 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 `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2;
;
end;

:: deftheorem Def9 defines address_1 AMI_2:def 9 :
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 `2 & b2 = f /. 1 ) );

:: deftheorem Def10 defines address_2 AMI_2:def 10 :
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 `2 & b2 = f /. 2 ) );

theorem :: AMI_2:23
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 )
proof end;

definition
let x be Element of SCM-Instr ;
given mk being Element of SCM-Instr-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk*>] ;
func x jump_address -> Element of SCM-Instr-Loc means :Def11: :: AMI_2:def 11
 ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Instr-Loc ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b1 = f /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2;
;
end;

:: deftheorem Def11 defines jump_address AMI_2:def 11 :
for x being Element of SCM-Instr st ex mk being Element of SCM-Instr-Loc ex I being Element of Segm 9 st x = [I,<*mk*>] holds
for b2 being Element of SCM-Instr-Loc holds
( b2 = x jump_address iff ex f being FinSequence of SCM-Instr-Loc st
( f = x `2 & b2 = f /. 1 ) );

theorem :: AMI_2:24
for x being Element of SCM-Instr
for mk being Element of SCM-Instr-Loc
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 Element of SCM-Instr-Loc , ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk,ml*>] ;
func x cjump_address -> Element of SCM-Instr-Loc means :Def12: :: AMI_2:def 12
 ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & it = <*mk,ml*> /. 1 );
existence
ex b1, mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 1 ) & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 1 ) holds
b1 = b2;
;
func x cond_address -> Element of SCM-Data-Loc means :Def13: :: AMI_2:def 13
 ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & it = <*mk,ml*> /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 2 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 2 ) & ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 2 ) holds
b1 = b2;
;
end;

:: deftheorem Def12 defines cjump_address AMI_2:def 12 :
for x being Element of SCM-Instr st ex mk being Element of SCM-Instr-Loc 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-Instr-Loc holds
( b2 = x cjump_address iff ex mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 1 ) );

:: deftheorem Def13 defines cond_address AMI_2:def 13 :
for x being Element of SCM-Instr st ex mk being Element of SCM-Instr-Loc 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 mk being Element of SCM-Instr-Loc ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 2 ) );

theorem :: AMI_2:25
for x being Element of SCM-Instr
for mk being Element of SCM-Instr-Loc
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;

registration
let s be SCM-State;
let a be Element of SCM-Data-Loc ;
cluster s . a -> integer ;
coherence