:: AMI_2 semantic presentation

definition
func SCM-Halt -> Element of Segm 9 equals :: AMI_2:def 1
0;
correctness
coherence
0 is Element of Segm 9;
by GR_CY_1:12;
end;

:: deftheorem Def1 defines SCM-Halt AMI_2:def 1 :
SCM-Halt = 0;

definition
func SCM-Data-Loc -> Subset of NAT equals :: AMI_2:def 2
{ ((2 * b1) + 1) where B is Nat : verum } ;
coherence
{ ((2 * b1) + 1) where B is Nat : verum } is Subset of NAT
proof end;
func SCM-Instr-Loc -> Subset of NAT equals :: AMI_2:def 3
{ (2 * b1) where B is Nat : b1 > 0 } ;
coherence
{ (2 * b1) where B is Nat : b1 > 0 } is Subset of NAT
proof end;
end;

:: deftheorem Def2 defines SCM-Data-Loc AMI_2:def 2 :
SCM-Data-Loc = { ((2 * b1) + 1) where B is Nat : verum } ;

:: deftheorem Def3 defines SCM-Instr-Loc AMI_2:def 3 :
SCM-Instr-Loc = { (2 * b1) where B is Nat : b1 > 0 } ;

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 ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ;
coherence
(({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } is Subset of [:(Segm 9),(((union {INT }) \/ NAT ) * ):]
proof end;
end;

:: deftheorem Def4 defines SCM-Instr AMI_2:def 4 :
SCM-Instr = (({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ;

theorem Th1: :: AMI_2:1
canceled;

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

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

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

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

theorem Th5: :: AMI_2:5
for b1 being set
for b2, b3 being Element of SCM-Data-Loc st b1 in {1,2,3,4,5} holds
[b1,<*b2,b3*>] in SCM-Instr
proof end;

E1: now
let c1 be Nat;
consider c2 being Nat such that
E2: ( c1 = 2 * c2 or c1 = (2 * c2) + 1 ) by SCHEME1:1;
now
assume E3: c1 = 2 * c2 ;
E4: ( c2 = 0 or ex b1 being Nat st c2 = b1 + 1 ) by NAT_1:22;
now
given c3 being Nat such that E5: c2 = c3 + 1 ;
take c4 = c3;
thus c1 = (2 * c4) + (2 * 1) by E3, E5;
end;
hence ( c1 = 0 or ex b1 being Nat st c1 = (2 * b1) + 2 ) by E3, E4;
end;
hence ( c1 = 0 or ex b1 being Nat st c1 = (2 * b1) + 1 or ex b1 being Nat st c1 = (2 * b1) + 2 ) by E2;
end;

E2: now
let c1 be Nat;
thus ( ex b1 being Nat st c1 = (2 * b1) + 1 implies ( c1 <> 0 & ( for b1 being Nat holds not c1 = (2 * b1) + 2 ) ) )
proof
given c2 being Nat such that E3: c1 = (2 * c2) + 1 ;
thus c1 <> 0 by E3;
given c3 being Nat such that E4: c1 = (2 * c3) + 2 ;
E5: (2 * c3) + (2 * 1) = (2 * (c3 + 1)) + 0 ;
1 = ((2 * c3) + 2) mod 2 by E3, E4, NAT_1:def 2
.= 0 by E5, NAT_1:def 2 ;
hence contradiction ;
end;
given c2 being Nat such that E3: c1 = (2 * c2) + (1 + 1) ;
thus c1 <> 0 by E3;
given c3 being Nat such that E4: c1 = (2 * c3) + 1 ;
E5: (2 * c2) + (2 * 1) = (2 * (c2 + 1)) + 0 ;
1 = ((2 * c2) + 2) mod 2 by E3, E4, NAT_1:def 2
.= 0 by E5, NAT_1:def 2 ;
hence contradiction ;
end;

definition
func SCM-OK -> Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } means :Def5: :: AMI_2:def 5
( a1 . 0 = SCM-Instr-Loc & ( for b1 being Nat holds
( a1 . ((2 * b1) + 1) = INT & a1 . ((2 * b1) + 2) = SCM-Instr ) ) );
existence
ex b1 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & ( for b2 being Nat holds
( b1 . ((2 * b2) + 1) = INT & b1 . ((2 * b2) + 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 b3 being Nat holds
( b1 . ((2 * b3) + 1) = INT & b1 . ((2 * b3) + 2) = SCM-Instr ) ) & b2 . 0 = SCM-Instr-Loc & ( for b3 being Nat holds
( b2 . ((2 * b3) + 1) = INT & b2 . ((2 * b3) + 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 b2 being Nat holds
( b1 . ((2 * b2) + 1) = INT & b1 . ((2 * b2) + 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 b1 being Nat holds
( SCM-OK . b1 = SCM-Instr-Loc iff b1 = 0 )
proof end;

theorem Th8: :: AMI_2:8
for b1 being Nat holds
( SCM-OK . b1 = INT iff ex b2 being Nat st b1 = (2 * b2) + 1 )
proof end;

theorem Th9: :: AMI_2:9
for b1 being Nat holds
( SCM-OK . b1 = SCM-Instr iff ex b2 being Nat st b1 = (2 * b2) + 2 )
proof end;

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

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

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

theorem Th12: :: AMI_2:12
for b1 being Element of SCM-Instr-Loc
for b2 being Element of SCM-Data-Loc holds b1 <> b2
proof end;

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

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

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

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

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

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

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

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

theorem Th17: :: AMI_2:17
for b1 being SCM-State
for b2 being Element of SCM-Instr-Loc
for b3 being Element of SCM-Data-Loc holds (SCM-Chg b1,b2) . b3 = b1 . b3
proof end;

theorem Th18: :: AMI_2:18
for b1 being SCM-State
for b2, b3 being Element of SCM-Instr-Loc holds (SCM-Chg b1,b2) . b3 = b1 . b3
proof end;

definition
let c1 be SCM-State;
let c2 be Element of SCM-Data-Loc ;
let c3 be Integer;
func SCM-Chg c1,c2,c3 -> SCM-State equals :: AMI_2:def 8
a1 +* (a2 .--> a3);
coherence
c1 +* (c2 .--> c3) is SCM-State
proof end;
end;

:: deftheorem Def8 defines SCM-Chg AMI_2:def 8 :
for b1 being SCM-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer holds SCM-Chg b1,b2,b3 = b1 +* (b2 .--> b3);

theorem Th19: :: AMI_2:19
for b1 being SCM-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer holds (SCM-Chg b1,b2,b3) . 0 = b1 . 0
proof end;

theorem Th20: :: AMI_2:20
for b1 being SCM-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer holds (SCM-Chg b1,b2,b3) . b2 = b3
proof end;

theorem Th21: :: AMI_2:21
for b1 being SCM-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer
for b4 being Element of SCM-Data-Loc st b4 <> b2 holds
(SCM-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th22: :: AMI_2:22
for b1 being SCM-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer
for b4 being Element of SCM-Instr-Loc holds (SCM-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

definition
let c1 be Element of SCM-Instr ;
given c2, c3 being Element of SCM-Data-Loc , c4 being Element of Segm 9 such that E12: c1 = [c4,<*c2,c3*>] ;
func c1 address_1 -> Element of SCM-Data-Loc means :Def9: :: AMI_2:def 9
ex b1 being FinSequence of SCM-Data-Loc st
( b1 = a1 `2 & a2 = b1 /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc st
( b2 = c1 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c1 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c1 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
func c1 address_2 -> Element of SCM-Data-Loc means :Def10: :: AMI_2:def 10
ex b1 being FinSequence of SCM-Data-Loc st
( b1 = a1 `2 & a2 = b1 /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc st
( b2 = c1 `2 & b1 = b2 /. 2 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c1 `2 & b1 = b3 /. 2 ) & ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c1 `2 & b2 = b3 /. 2 ) holds
b1 = b2;
;
end;

:: deftheorem Def9 defines address_1 AMI_2:def 9 :
for b1 being Element of SCM-Instr st ex b2, b3 being Element of SCM-Data-Loc ex b4 being Element of Segm 9 st b1 = [b4,<*b2,b3*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = b1 address_1 iff ex b3 being FinSequence of SCM-Data-Loc st
( b3 = b1 `2 & b2 = b3 /. 1 ) );

:: deftheorem Def10 defines address_2 AMI_2:def 10 :
for b1 being Element of SCM-Instr st ex b2, b3 being Element of SCM-Data-Loc ex b4 being Element of Segm 9 st b1 = [b4,<*b2,b3*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = b1 address_2 iff ex b3 being FinSequence of SCM-Data-Loc st
( b3 = b1 `2 & b2 = b3 /. 2 ) );

theorem Th23: :: AMI_2:23
for b1 being Element of SCM-Instr
for b2, b3 being Element of SCM-Data-Loc
for b4 being Element of Segm 9 st b1 = [b4,<*b2,b3*>] holds
( b1 address_1 = b2 & b1 address_2 = b3 )
proof end;

definition
let c1 be Element of SCM-Instr ;
given c2 being Element of SCM-Instr-Loc , c3 being Element of Segm 9 such that E14: c1 = [c3,<*c2*>] ;
func c1 jump_address -> Element of SCM-Instr-Loc means :Def11: :: AMI_2:def 11
ex b1 being FinSequence of SCM-Instr-Loc st
( b1 = a1 `2 & a2 = b1 /. 1 );
existence
ex b1 being Element of SCM-Instr-Loc ex b2 being FinSequence of SCM-Instr-Loc st
( b2 = c1 `2 & b1 = b2 /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex b3 being FinSequence of SCM-Instr-Loc st
( b3 = c1 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Instr-Loc st
( b3 = c1 `2 & b2 = b3 /. 1 ) holds
b1 = b2;
;
end;

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

theorem Th24: :: AMI_2:24
for b1 being Element of SCM-Instr
for b2 being Element of SCM-Instr-Loc
for b3 being Element of Segm 9 st b1 = [b3,<*b2*>] holds
b1 jump_address = b2
proof end;

definition
let c1 be Element of SCM-Instr ;
given c2 being Element of SCM-Instr-Loc , c3 being Element of SCM-Data-Loc , c4 being Element of Segm 9 such that E15: c1 = [c4,<*c2,c3*>] ;
func c1 cjump_address -> Element of SCM-Instr-Loc means :Def12: :: AMI_2:def 12
ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st
( <*b1,b2*> = a1 `2 & a2 = <*b1,b2*> /. 1 );
existence
ex b1, b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st
( <*b2,b3*> = c1 `2 & b1 = <*b2,b3*> /. 1 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c1 `2 & b1 = <*b3,b4*> /. 1 ) & ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c1 `2 & b2 = <*b3,b4*> /. 1 ) holds
b1 = b2;
;
func c1 cond_address -> Element of SCM-Data-Loc means :Def13: :: AMI_2:def 13
ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st
( <*b1,b2*> = a1 `2 & a2 = <*b1,b2*> /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st
( <*b2,b3*> = c1 `2 & b1 = <*b2,b3*> /. 2 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c1 `2 & b1 = <*b3,b4*> /. 2 ) & ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c1 `2 & b2 = <*b3,b4*> /. 2 ) holds
b1 = b2;
;
end;

:: deftheorem Def12 defines cjump_address AMI_2:def 12 :
for b1 being Element of SCM-Instr st ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc ex b4 being Element of Segm 9 st b1 = [b4,<*b2,b3*>] holds
for b2 being Element of SCM-Instr-Loc holds
( b2 = b1 cjump_address iff ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = b1 `2 & b2 = <*b3,b4*> /. 1 ) );

:: deftheorem Def13 defines cond_address AMI_2:def 13 :
for b1 being Element of SCM-Instr st ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc ex b4 being Element of Segm 9 st b1 = [b4,<*b2,b3*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = b1 cond_address iff ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = b1 `2 & b2 = <*b3,b4*> /. 2 ) );

theorem Th25: :: AMI_2:25
for b1 being Element of SCM-Instr
for b2 being Element of SCM-Instr-Loc
for b3 being Element of SCM-Data-Loc
for b4 being Element of Segm 9 st b1 = [b4,<*b2,b3*>] holds
( b1 cjump_address = b2 & b1 cond_address = b3 )
proof end;

registration
let c1 be SCM-State;
let c2 be Element of SCM-Data-Loc ;
cluster a1 . a2 -> integer ;
coherence
c1 . c2 is integer
proof end;
end;

definition
let c1 be non empty set ;
let c2, c3 be real number ;
let c4, c5 be Element of c1;
func IFGT c2,c3,c4,c5 -> Element of a1 equals :: AMI_2:def 14
a4 if a2 > a3
otherwise a5;
correctness
coherence
( ( c2 > c3 implies c4 is Element of c1 ) & ( not c2 > c3 implies c5 is Element of c1 ) );
consistency
for b1 being Element of c1 holds verum;
;
end;

:: deftheorem Def14 defines IFGT AMI_2:def 14 :
for b1 being non empty set
for b2, b3 being real number
for b4, b5 being Element of b1 holds
( ( b2 > b3 implies IFGT b2,b3,b4,b5 = b4 ) & ( not b2 > b3 implies IFGT b2,b3,b4,b5 = b5 ) );

definition
let c1 be Element of SCM-Instr-Loc ;
func Next c1 -> Element of SCM-Instr-Loc equals :: AMI_2:def 15
a1 + 2;
coherence
c1 + 2 is Element of SCM-Instr-Loc
proof end;
end;

:: deftheorem Def15 defines Next AMI_2:def 15 :
for b1 being Element of SCM-Instr-Loc holds Next b1 = b1 + 2;

definition
let c1 be Element of SCM-Instr ;
let c2 be SCM-State;
func SCM-Exec-Res c1,c2 -> SCM-State equals :: AMI_2:def 16
 SCM-Chg (SCM-Chg a2,(a1 address_1 ),(a2 . (a1 address_2 ))),(Next (IC a2)) if ex b1, b2 being Element of SCM-Data-Loc st a1 = [1,<*b1,b2*>]
SCM-Chg (SCM-Chg a2,(a1 address_1 ),((a2 . (a1 address_1 )) + (a2 . (a1 address_2 )))),(Next (IC a2)) if ex b1, b2 being Element of SCM-Data-Loc st a1 = [2,<*b1,b2*>]
SCM-Chg (SCM-Chg a2,(a1 address_1 ),((a2 . (a1 address_1 )) - (a2 . (a1 address_2 )))),(Next (IC a2)) if ex b1, b2 being Element of SCM-Data-Loc st a1 = [3,<*b1,b2*>]
SCM-Chg (SCM-Chg a2,(a1 address_1 ),((a2 . (a1 address_1 )) * (a2 . (a1 address_2 )))),(Next (IC a2)) if ex b1, b2 being Element of SCM-Data-Loc st a1 = [4,<*b1,b2*>]
SCM-Chg (SCM-Chg (SCM-Chg a2,(a1 address_1 ),((a2 . (a1 address_1 )) div (a2 . (a1 address_2 )))),(a1 address_2 ),((a2 . (a1 address_1 )) mod (a2 . (a1 address_2 )))),(Next (IC a2)) if ex b1, b2 being Element of SCM-Data-Loc st a1 = [5,<*b1,b2*>]
SCM-Chg a2,(a1 jump_address ) if ex b1 being Element of SCM-Instr-Loc st a1 = [6,<*b1*>]
SCM-Chg a2,(IFEQ (a2 . (a1 cond_address )),0,(a1 cjump_address ),(Next (IC a2))) if ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st a1 = [7,<*b1,b2*>]
SCM-Chg a2,(IFGT (a2 . (a1 cond_address )),0,(a1 cjump_address ),(Next (IC a2))) if ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st a1 = [8,<*b1,b2*>]
otherwise a2;
consistency
for b1 being SCM-State holds
( ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg c2,(c1 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [1,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(c1 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [2,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(c1 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [3,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(c1 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [4,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(c1 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c1 = [5,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg c2,(c1 jump_address ) iff b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2 being Element of SCM-Instr-Loc st c1 = [6,<*b2*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg c2,(c1 jump_address ) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) & ( ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [7,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c1 = [8,<*b2,b3*>] implies ( b1 = SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) iff b1 = SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) ) ) ) by ZFMISC_1:33;
coherence
( ( ex b1, b2 being Element of SCM-Data-Loc st c1 = [1,<*b1,b2*>] implies SCM-Chg (SCM-Chg c2,(c1 address_1 ),(c2 . (c1 address_2 ))),(Next (IC c2)) is SCM-State ) & ( ex b1, b2 being Element of SCM-Data-Loc st c1 = [2,<*b1,b2*>] implies SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) + (c2 . (c1 address_2 )))),(Next (IC c2)) is SCM-State ) & ( ex b1, b2 being Element of SCM-Data-Loc st c1 = [3,<*b1,b2*>] implies SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) - (c2 . (c1 address_2 )))),(Next (IC c2)) is SCM-State ) & ( ex b1, b2 being Element of SCM-Data-Loc st c1 = [4,<*b1,b2*>] implies SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) * (c2 . (c1 address_2 )))),(Next (IC c2)) is SCM-State ) & ( ex b1, b2 being Element of SCM-Data-Loc st c1 = [5,<*b1,b2*>] implies SCM-Chg (SCM-Chg (SCM-Chg c2,(c1 address_1 ),((c2 . (c1 address_1 )) div (c2 . (c1 address_2 )))),(c1 address_2 ),((c2 . (c1 address_1 )) mod (c2 . (c1 address_2 )))),(Next (IC c2)) is SCM-State ) & ( ex b1 being Element of SCM-Instr-Loc st c1 = [6,<*b1*>] implies SCM-Chg c2,(c1 jump_address ) is SCM-State ) & ( ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st c1 = [7,<*b1,b2*>] implies SCM-Chg c2,(IFEQ (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) is SCM-State ) & ( ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st c1 = [8,<*b1,b2*>] implies SCM-Chg c2,(IFGT (c2 . (c1 cond_address )),0,(c1 cjump_address ),(Next (IC c2))) is SCM-State ) & ( ( for b1, b2 being Element of SCM-Data-Loc holds not c1 = [1,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c1 = [2,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c1 = [3,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c1 = [4,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c1 = [5,<*b1,b2*>] ) & ( for b1 being Element of SCM-Instr-Loc holds not c1 = [6,<*b1*>] ) & ( for b1 being Element of SCM-Instr-Loc
for b2 being Element of SCM-Data-Loc holds not c1 = [7,<*b1,b2*>] ) & ( for b1 being Element of SCM-Instr-Loc
for b2 being Element of SCM-Data-Loc holds not c1 = [8,<*b1,b2*>] ) implies c2 is SCM-State ) ) ;
end;

:: deftheorem Def16 defines SCM-Exec-Res AMI_2:def 16 :
for b1 being Element of SCM-Instr
for b2 being SCM-State holds
( ( ex b3, b4 being Element of SCM-Data-Loc st b1 = [1,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg (SCM-Chg b2,(b1 address_1 ),(b2 . (b1 address_2 ))),(Next (IC b2)) ) & ( ex b3, b4 being Element of SCM-Data-Loc st b1 = [2,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg (SCM-Chg b2,(b1 address_1 ),((b2 . (b1 address_1 )) + (b2 . (b1 address_2 )))),(Next (IC b2)) ) & ( ex b3, b4 being Element of SCM-Data-Loc st b1 = [3,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg (SCM-Chg b2,(b1 address_1 ),((b2 . (b1 address_1 )) - (b2 . (b1 address_2 )))),(Next (IC b2)) ) & ( ex b3, b4 being Element of SCM-Data-Loc st b1 = [4,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg (SCM-Chg b2,(b1 address_1 ),((b2 . (b1 address_1 )) * (b2 . (b1 address_2 )))),(Next (IC b2)) ) & ( ex b3, b4 being Element of SCM-Data-Loc st b1 = [5,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg (SCM-Chg (SCM-Chg b2,(b1 address_1 ),((b2 . (b1 address_1 )) div (b2 . (b1 address_2 )))),(b1 address_2 ),((b2 . (b1 address_1 )) mod (b2 . (b1 address_2 )))),(Next (IC b2)) ) & ( ex b3 being Element of SCM-Instr-Loc st b1 = [6,<*b3*>] implies SCM-Exec-Res b1,b2 = SCM-Chg b2,(b1 jump_address ) ) & ( ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st b1 = [7,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg b2,(IFEQ (b2 . (b1 cond_address )),0,(b1 cjump_address ),(Next (IC b2))) ) & ( ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st b1 = [8,<*b3,b4*>] implies SCM-Exec-Res b1,b2 = SCM-Chg b2,(IFGT (b2 . (b1 cond_address )),0,(b1 cjump_address ),(Next (IC b2))) ) & ( ( for b3, b4 being Element of SCM-Data-Loc holds not b1 = [1,<*b3,b4*>] ) & ( for b3, b4 being Element of SCM-Data-Loc holds not b1 = [2,<*b3,b4*>] ) & ( for b3, b4 being Element of SCM-Data-Loc holds not b1 = [3,<*b3,b4*>] ) & ( for b3, b4 being Element of SCM-Data-Loc holds not b1 = [4,<*b3,b4*>] ) & ( for b3, b4 being Element of SCM-Data-Loc holds not b1 = [5,<*b3,b4*>] ) & ( for b3 being Element of SCM-Instr-Loc holds not b1 = [6,<*b3*>] ) & ( for b3 being Element of SCM-Instr-Loc
for b4 being Element of SCM-Data-Loc holds not b1 = [7,<*b3,b4*>] ) & ( for b3 being Element of SCM-Instr-Loc
for b4 being Element of SCM-Data-Loc holds not b1 = [8,<*b3,b4*>] ) implies SCM-Exec-Res b1,b2 = b2 ) );

definition
func SCM-Exec -> Function of SCM-Instr , Funcs (product SCM-OK ),(product SCM-OK ) means :: AMI_2:def 17
for b1 being Element of SCM-Instr
for b2 being SCM-State holds (a1 . b1) . b2 = SCM-Exec-Res b1,b2;
existence
ex b1 being Function of SCM-Instr , Funcs (product SCM-OK ),(product SCM-OK ) st
for b2 being Element of SCM-Instr
for b3 being SCM-State holds (b1 . b2) . b3 = SCM-Exec-Res b2,b3
proof end;
uniqueness
for b1, b2 being Function of SCM-Instr , Funcs (product SCM-OK ),(product SCM-OK ) st ( for b3 being Element of SCM-Instr
for b4 being SCM-State holds (b1 . b3) . b4 = SCM-Exec-Res b3,b4 ) & ( for b3 being Element of SCM-Instr
for b4 being SCM-State holds (b2 . b3) . b4 = SCM-Exec-Res b3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines SCM-Exec AMI_2:def 17 :
for b1 being Function of SCM-Instr , Funcs (product SCM-OK ),(product SCM-OK ) holds
( b1 = SCM-Exec iff for b2 being Element of SCM-Instr
for b3 being SCM-State holds (b1 . b2) . b3 = SCM-Exec-Res b2,b3 );