:: SCMFSA_1 semantic presentation

definition
func SCM+FSA-Data-Loc -> Subset of INT equals :: SCMFSA_1:def 1
 SCM-Data-Loc ;
coherence
SCM-Data-Loc is Subset of INT by NUMBERS:17, XBOOLE_1:1;
func SCM+FSA-Data*-Loc -> Subset of INT equals :: SCMFSA_1:def 2
INT \ NAT ;
coherence
INT \ NAT is Subset of INT by XBOOLE_1:36;
func SCM+FSA-Instr-Loc -> Subset of INT equals :: SCMFSA_1:def 3
 SCM-Instr-Loc ;
coherence
SCM-Instr-Loc is Subset of INT by NUMBERS:17, XBOOLE_1:1;
end;

:: deftheorem Def1 defines SCM+FSA-Data-Loc SCMFSA_1:def 1 :
SCM+FSA-Data-Loc = SCM-Data-Loc ;

:: deftheorem Def2 defines SCM+FSA-Data*-Loc SCMFSA_1:def 2 :
SCM+FSA-Data*-Loc = INT \ NAT ;

:: deftheorem Def3 defines SCM+FSA-Instr-Loc SCMFSA_1:def 3 :
SCM+FSA-Instr-Loc = SCM-Instr-Loc ;

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

definition
func SCM+FSA-Instr -> Subset of [:(Segm 13),(((union {INT ,(INT * )}) \/ INT ) * ):] equals :: SCMFSA_1:def 4
(SCM-Instr \/ { [b1,<*b2,b4,b3*>] where B is Element of Segm 13, B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 13, B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } ;
coherence
(SCM-Instr \/ { [b1,<*b2,b4,b3*>] where B is Element of Segm 13, B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 13, B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is Subset of [:(Segm 13),(((union {INT ,(INT * )}) \/ INT ) * ):]
proof end;
end;

:: deftheorem Def4 defines SCM+FSA-Instr SCMFSA_1:def 4 :
SCM+FSA-Instr = (SCM-Instr \/ { [b1,<*b2,b4,b3*>] where B is Element of Segm 13, B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 13, B is Element of SCM+FSA-Data-Loc , B is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } ;

theorem Th1: :: SCMFSA_1:1
canceled;

theorem Th2: :: SCMFSA_1:2
SCM-Instr c= SCM+FSA-Instr
proof end;

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

definition
let c1 be Element of SCM+FSA-Instr ;
func InsCode c1 -> Nat equals :: SCMFSA_1:def 5
a1 `1 ;
coherence
c1 `1 is Nat
proof end;
end;

:: deftheorem Def5 defines InsCode SCMFSA_1:def 5 :
for b1 being Element of SCM+FSA-Instr holds InsCode b1 = b1 `1 ;

theorem Th3: :: SCMFSA_1:3
for b1 being Element of SCM+FSA-Instr st InsCode b1 <= 8 holds
b1 in SCM-Instr
proof end;

theorem Th4: :: SCMFSA_1:4
[0,{} ] in SCM+FSA-Instr by Th2, AMI_2:2;

definition
func SCM+FSA-OK -> Function of INT ,{INT ,(INT * )} \/ {SCM+FSA-Instr ,SCM+FSA-Instr-Loc } equals :: SCMFSA_1:def 6
((INT --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | SCM-Instr-Loc ));
coherence
((INT --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | SCM-Instr-Loc )) is Function of INT ,{INT ,(INT * )} \/ {SCM+FSA-Instr ,SCM+FSA-Instr-Loc }
proof end;
end;

:: deftheorem Def6 defines SCM+FSA-OK SCMFSA_1:def 6 :
SCM+FSA-OK = ((INT --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | SCM-Instr-Loc ));

Lemma3: dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | SCM-Instr-Loc )) c= SCM-Instr-Loc
proof end;

Lemma4: rng (SCM-OK | SCM-Instr-Loc ) c= {SCM-Instr }
proof end;

Lemma5: SCM-Instr-Loc c= dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | SCM-Instr-Loc ))
proof end;

theorem Th5: :: SCMFSA_1:5
canceled;

theorem Th6: :: SCMFSA_1:6
for b1 being set
for b2, b3 being Element of SCM+FSA-Data-Loc
for b4 being Element of SCM+FSA-Data*-Loc st b1 in {9,10} holds
[b1,<*b2,b4,b3*>] in SCM+FSA-Instr
proof end;

theorem Th7: :: SCMFSA_1:7
for b1 being set
for b2 being Element of SCM+FSA-Data-Loc
for b3 being Element of SCM+FSA-Data*-Loc st b1 in {11,12} holds
[b1,<*b2,b3*>] in SCM+FSA-Instr
proof end;

theorem Th8: :: SCMFSA_1:8
INT = (({0} \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc ) \/ SCM+FSA-Instr-Loc
proof end;

theorem Th9: :: SCMFSA_1:9
SCM+FSA-OK . 0 = SCM+FSA-Instr-Loc
proof end;

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

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

theorem Th12: :: SCMFSA_1:12
for b1 being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . b1 = INT *
proof end;

theorem Th13: :: SCMFSA_1:13
( SCM+FSA-Instr-Loc <> INT & SCM+FSA-Instr <> INT & SCM+FSA-Instr-Loc <> SCM+FSA-Instr & SCM+FSA-Instr-Loc <> INT * & SCM+FSA-Instr <> INT * )
proof end;

theorem Th14: :: SCMFSA_1:14
for b1 being Integer st SCM+FSA-OK . b1 = SCM+FSA-Instr-Loc holds
b1 = 0
proof end;

theorem Th15: :: SCMFSA_1:15
for b1 being Integer st SCM+FSA-OK . b1 = INT holds
b1 in SCM+FSA-Data-Loc
proof end;

theorem Th16: :: SCMFSA_1:16
for b1 being Integer st SCM+FSA-OK . b1 = SCM+FSA-Instr holds
b1 in SCM+FSA-Instr-Loc
proof end;

theorem Th17: :: SCMFSA_1:17
for b1 being Integer st SCM+FSA-OK . b1 = INT * holds
b1 in SCM+FSA-Data*-Loc
proof end;

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

theorem Th18: :: SCMFSA_1:18
for b1 being SCM+FSA-State
for b2 being Element of SCM-Instr holds (b1 | NAT ) +* (SCM-Instr-Loc --> b2) is SCM-State
proof end;

theorem Th19: :: SCMFSA_1:19
for b1 being SCM+FSA-State
for b2 being SCM-State holds (b1 +* b2) +* (b1 | SCM+FSA-Instr-Loc ) is SCM+FSA-State
proof end;

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

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

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

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

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

:: deftheorem Def9 defines SCM+FSA-Chg SCMFSA_1:def 9 :
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data*-Loc
for b3 being FinSequence of INT holds SCM+FSA-Chg b1,b2,b3 = b1 +* (b2 .--> b3);

definition
let c1 be SCM+FSA-State;
let c2 be Element of SCM+FSA-Data-Loc ;
redefine func . as c1 . c2 -> Integer;
coherence
c1 . c2 is Integer
proof end;
end;

definition
let c1 be SCM+FSA-State;
let c2 be Element of SCM+FSA-Data*-Loc ;
redefine func . as c1 . c2 -> FinSequence of INT ;
coherence
c1 . c2 is FinSequence of INT
proof end;
end;

definition
let c1 be Element of SCM+FSA-Instr ;
given c2 being Element of SCM+FSA-Data-Loc , c3 being Element of SCM+FSA-Data*-Loc , c4 being Element of SCM+FSA-Data-Loc , c5 being Element of Segm 13 such that E14: c1 = [c5,<*c2,c3,c4*>] ;
func c1 int_addr1 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 10
ex b1 being Element of SCM+FSA-Data-Loc ex b2 being Element of SCM+FSA-Data*-Loc ex b3 being Element of SCM+FSA-Data-Loc st
( <*b1,b2,b3*> = a1 `2 & a2 = b1 );
existence
ex b1, b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of SCM+FSA-Data-Loc st
( <*b2,b3,b4*> = c1 `2 & b1 = b2 )
proof end;
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = c1 `2 & b1 = b3 ) & ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = c1 `2 & b2 = b3 ) holds
b1 = b2
proof end;
func c1 int_addr2 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 11
ex b1 being Element of SCM+FSA-Data-Loc ex b2 being Element of SCM+FSA-Data*-Loc ex b3 being Element of SCM+FSA-Data-Loc st
( <*b1,b2,b3*> = a1 `2 & a2 = b3 );
existence
ex b1, b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of SCM+FSA-Data-Loc st
( <*b2,b3,b4*> = c1 `2 & b1 = b4 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = c1 `2 & b1 = b5 ) & ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = c1 `2 & b2 = b5 ) holds
b1 = b2;
proof end;
func c1 coll_addr1 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 12
ex b1 being Element of SCM+FSA-Data-Loc ex b2 being Element of SCM+FSA-Data*-Loc ex b3 being Element of SCM+FSA-Data-Loc st
( <*b1,b2,b3*> = a1 `2 & a2 = b2 );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of SCM+FSA-Data-Loc st
( <*b2,b3,b4*> = c1 `2 & b1 = b3 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = c1 `2 & b1 = b4 ) & ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = c1 `2 & b2 = b4 ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def10 defines int_addr1 SCMFSA_1:def 10 :
for b1 being Element of SCM+FSA-Instr st ex b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of SCM+FSA-Data-Loc ex b5 being Element of Segm 13 st b1 = [b5,<*b2,b3,b4*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = b1 int_addr1 iff ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = b1 `2 & b2 = b3 ) );

:: deftheorem Def11 defines int_addr2 SCMFSA_1:def 11 :
for b1 being Element of SCM+FSA-Instr st ex b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of SCM+FSA-Data-Loc ex b5 being Element of Segm 13 st b1 = [b5,<*b2,b3,b4*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = b1 int_addr2 iff ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = b1 `2 & b2 = b5 ) );

:: deftheorem Def12 defines coll_addr1 SCMFSA_1:def 12 :
for b1 being Element of SCM+FSA-Instr st ex b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of SCM+FSA-Data-Loc ex b5 being Element of Segm 13 st b1 = [b5,<*b2,b3,b4*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = b1 coll_addr1 iff ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc ex b5 being Element of SCM+FSA-Data-Loc st
( <*b3,b4,b5*> = b1 `2 & b2 = b4 ) );

definition
let c1 be Element of SCM+FSA-Instr ;
given c2 being Element of SCM+FSA-Data-Loc , c3 being Element of SCM+FSA-Data*-Loc , c4 being Element of Segm 13 such that E14: c1 = [c4,<*c2,c3*>] ;
func c1 int_addr3 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 13
ex b1 being Element of SCM+FSA-Data-Loc ex b2 being Element of SCM+FSA-Data*-Loc st
( <*b1,b2*> = a1 `2 & a2 = b1 );
existence
ex b1, b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc st
( <*b2,b3*> = c1 `2 & b1 = b2 )
proof end;
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc st
( <*b3,b4*> = c1 `2 & b1 = b3 ) & ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc st
( <*b3,b4*> = c1 `2 & b2 = b3 ) holds
b1 = b2
proof end;
func c1 coll_addr2 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 14
ex b1 being Element of SCM+FSA-Data-Loc ex b2 being Element of SCM+FSA-Data*-Loc st
( <*b1,b2*> = a1 `2 & a2 = b2 );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc st
( <*b2,b3*> = c1 `2 & b1 = b3 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc st
( <*b3,b4*> = c1 `2 & b1 = b4 ) & ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc st
( <*b3,b4*> = c1 `2 & b2 = b4 ) holds
b1 = b2;
proof end;
end;

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

:: deftheorem Def14 defines coll_addr2 SCMFSA_1:def 14 :
for b1 being Element of SCM+FSA-Instr st ex b2 being Element of SCM+FSA-Data-Loc ex b3 being Element of SCM+FSA-Data*-Loc ex b4 being Element of Segm 13 st b1 = [b4,<*b2,b3*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = b1 coll_addr2 iff ex b3 being Element of SCM+FSA-Data-Loc ex b4 being Element of SCM+FSA-Data*-Loc st
( <*b3,b4*> = b1 `2 & b2 = b4 ) );

definition
let c1 be Element of SCM+FSA-Instr-Loc ;
func Next c1 -> Element of SCM+FSA-Instr-Loc means :: SCMFSA_1:def 15
ex b1 being Element of SCM-Instr-Loc st
( b1 = a1 & a2 = Next b1 );
existence
ex b1 being Element of SCM+FSA-Instr-Loc ex b2 being Element of SCM-Instr-Loc st
( b2 = c1 & b1 = Next b2 )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Instr-Loc st ex b3 being Element of SCM-Instr-Loc st
( b3 = c1 & b1 = Next b3 ) & ex b3 being Element of SCM-Instr-Loc st
( b3 = c1 & b2 = Next b3 ) holds
b1 = b2;
;
end;

:: deftheorem Def15 defines Next SCMFSA_1:def 15 :
for b1, b2 being Element of SCM+FSA-Instr-Loc holds
( b2 = Next b1 iff ex b3 being Element of SCM-Instr-Loc st
( b3 = b1 & b2 = Next b3 ) );

definition
let c1 be SCM+FSA-State;
func IC c1 -> Element of SCM+FSA-Instr-Loc equals :: SCMFSA_1:def 16
a1 . 0;
coherence
c1 . 0 is Element of SCM+FSA-Instr-Loc
proof end;
end;

:: deftheorem Def16 defines IC SCMFSA_1:def 16 :
for b1 being SCM+FSA-State holds IC b1 = b1 . 0;

definition
let c1 be Element of SCM+FSA-Instr ;
let c2 be SCM+FSA-State;
func SCM+FSA-Exec-Res c1,c2 -> SCM+FSA-State means :: SCMFSA_1:def 17
ex b1 being Element of SCM-Instr ex b2 being SCM-State st
( a1 = b1 & b2 = (a2 | NAT ) +* (SCM-Instr-Loc --> b1) & a3 = (a2 +* (SCM-Exec-Res b1,b2)) +* (a2 | SCM+FSA-Instr-Loc ) ) if InsCode a1 <= 8
ex b1 being Integerex b2 being Nat st
( b2 = abs (a2 . (a1 int_addr2 )) & b1 = (a2 . (a1 coll_addr1 )) /. b2 & a3 = SCM+FSA-Chg (SCM+FSA-Chg a2,(a1 int_addr1 ),b1),(Next (IC a2)) ) if InsCode a1 = 9
ex b1 being FinSequence of INT ex b2 being Nat st
( b2 = abs (a2 . (a1 int_addr2 )) & b1 = (a2 . (a1 coll_addr1 )) +* b2,(a2 . (a1 int_addr1 )) & a3 = SCM+FSA-Chg (SCM+FSA-Chg a2,(a1 coll_addr1 ),b1),(Next (IC a2)) ) if InsCode a1 = 10
a3 = SCM+FSA-Chg (SCM+FSA-Chg a2,(a1 int_addr3 ),(len (a2 . (a1 coll_addr2 )))),(Next (IC a2)) if InsCode a1 = 11
ex b1 being FinSequence of INT ex b2 being Nat st
( b2 = abs (a2 . (a1 int_addr3 )) & b1 = b2 |-> 0 & a3 = SCM+FSA-Chg (SCM+FSA-Chg a2,(a1 coll_addr2 ),b1),(Next (IC a2)) ) if InsCode a1 = 12
otherwise a3 = a2;
existence
( ( InsCode c1 <= 8 implies ex b1 being SCM+FSA-Stateex b2 being Element of SCM-Instr ex b3 being SCM-State st
( c1 = b2 & b3 = (c2 | NAT ) +* (SCM-Instr-Loc --> b2) & b1 = (c2 +* (SCM-Exec-Res b2,b3)) +* (c2 | SCM+FSA-Instr-Loc ) ) ) & ( InsCode c1 = 9 implies ex b1 being SCM+FSA-Stateex b2 being Integerex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) /. b3 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b2),(Next (IC c2)) ) ) & ( InsCode c1 = 10 implies ex b1 being SCM+FSA-Stateex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) +* b3,(c2 . (c1 int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b2),(Next (IC c2)) ) ) & ( InsCode c1 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) ) & ( InsCode c1 = 12 implies ex b1 being SCM+FSA-Stateex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr3 )) & b2 = b3 |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b2),(Next (IC c2)) ) ) & ( not InsCode c1 <= 8 & not InsCode c1 = 9 & not InsCode c1 = 10 & not InsCode c1 = 11 & not InsCode c1 = 12 implies ex b1 being SCM+FSA-State st b1 = c2 ) )
proof end;
uniqueness
for b1, b2 being SCM+FSA-State holds
( ( InsCode c1 <= 8 & ex b3 being Element of SCM-Instr ex b4 being SCM-State st
( c1 = b3 & b4 = (c2 | NAT ) +* (SCM-Instr-Loc --> b3) & b1 = (c2 +* (SCM-Exec-Res b3,b4)) +* (c2 | SCM+FSA-Instr-Loc ) ) & ex b3 being Element of SCM-Instr ex b4 being SCM-State st
( c1 = b3 & b4 = (c2 | NAT ) +* (SCM-Instr-Loc --> b3) & b2 = (c2 +* (SCM-Exec-Res b3,b4)) +* (c2 | SCM+FSA-Instr-Loc ) ) implies b1 = b2 ) & ( InsCode c1 = 9 & ex b3 being Integerex b4 being Nat st
( b4 = abs (c2 . (c1 int_addr2 )) & b3 = (c2 . (c1 coll_addr1 )) /. b4 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b3),(Next (IC c2)) ) & ex b3 being Integerex b4 being Nat st
( b4 = abs (c2 . (c1 int_addr2 )) & b3 = (c2 . (c1 coll_addr1 )) /. b4 & b2 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b3),(Next (IC c2)) ) implies b1 = b2 ) & ( InsCode c1 = 10 & ex b3 being FinSequence of INT ex b4 being Nat st
( b4 = abs (c2 . (c1 int_addr2 )) & b3 = (c2 . (c1 coll_addr1 )) +* b4,(c2 . (c1 int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b3),(Next (IC c2)) ) & ex b3 being FinSequence of INT ex b4 being Nat st
( b4 = abs (c2 . (c1 int_addr2 )) & b3 = (c2 . (c1 coll_addr1 )) +* b4,(c2 . (c1 int_addr1 )) & b2 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b3),(Next (IC c2)) ) implies b1 = b2 ) & ( InsCode c1 = 11 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) & b2 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) implies b1 = b2 ) & ( InsCode c1 = 12 & ex b3 being FinSequence of INT ex b4 being Nat st
( b4 = abs (c2 . (c1 int_addr3 )) & b3 = b4 |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b3),(Next (IC c2)) ) & ex b3 being FinSequence of INT ex b4 being Nat st
( b4 = abs (c2 . (c1 int_addr3 )) & b3 = b4 |-> 0 & b2 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b3),(Next (IC c2)) ) implies b1 = b2 ) & ( not InsCode c1 <= 8 & not InsCode c1 = 9 & not InsCode c1 = 10 & not InsCode c1 = 11 & not InsCode c1 = 12 & b1 = c2 & b2 = c2 implies b1 = b2 ) ) ;
consistency
for b1 being SCM+FSA-State holds
( ( InsCode c1 <= 8 & InsCode c1 = 9 implies ( ex b2 being Element of SCM-Instr ex b3 being SCM-State st
( c1 = b2 & b3 = (c2 | NAT ) +* (SCM-Instr-Loc --> b2) & b1 = (c2 +* (SCM-Exec-Res b2,b3)) +* (c2 | SCM+FSA-Instr-Loc ) ) iff ex b2 being Integerex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) /. b3 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b2),(Next (IC c2)) ) ) ) & ( InsCode c1 <= 8 & InsCode c1 = 10 implies ( ex b2 being Element of SCM-Instr ex b3 being SCM-State st
( c1 = b2 & b3 = (c2 | NAT ) +* (SCM-Instr-Loc --> b2) & b1 = (c2 +* (SCM-Exec-Res b2,b3)) +* (c2 | SCM+FSA-Instr-Loc ) ) iff ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) +* b3,(c2 . (c1 int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b2),(Next (IC c2)) ) ) ) & ( InsCode c1 <= 8 & InsCode c1 = 11 implies ( ex b2 being Element of SCM-Instr ex b3 being SCM-State st
( c1 = b2 & b3 = (c2 | NAT ) +* (SCM-Instr-Loc --> b2) & b1 = (c2 +* (SCM-Exec-Res b2,b3)) +* (c2 | SCM+FSA-Instr-Loc ) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) ) ) & ( InsCode c1 <= 8 & InsCode c1 = 12 implies ( ex b2 being Element of SCM-Instr ex b3 being SCM-State st
( c1 = b2 & b3 = (c2 | NAT ) +* (SCM-Instr-Loc --> b2) & b1 = (c2 +* (SCM-Exec-Res b2,b3)) +* (c2 | SCM+FSA-Instr-Loc ) ) iff ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr3 )) & b2 = b3 |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b2),(Next (IC c2)) ) ) ) & ( InsCode c1 = 9 & InsCode c1 = 10 implies ( ex b2 being Integerex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) /. b3 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b2),(Next (IC c2)) ) iff ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) +* b3,(c2 . (c1 int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b2),(Next (IC c2)) ) ) ) & ( InsCode c1 = 9 & InsCode c1 = 11 implies ( ex b2 being Integerex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) /. b3 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b2),(Next (IC c2)) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) ) ) & ( InsCode c1 = 9 & InsCode c1 = 12 implies ( ex b2 being Integerex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) /. b3 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr1 ),b2),(Next (IC c2)) ) iff ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr3 )) & b2 = b3 |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b2),(Next (IC c2)) ) ) ) & ( InsCode c1 = 10 & InsCode c1 = 11 implies ( ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) +* b3,(c2 . (c1 int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b2),(Next (IC c2)) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) ) ) & ( InsCode c1 = 10 & InsCode c1 = 12 implies ( ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr2 )) & b2 = (c2 . (c1 coll_addr1 )) +* b3,(c2 . (c1 int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr1 ),b2),(Next (IC c2)) ) iff ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr3 )) & b2 = b3 |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b2),(Next (IC c2)) ) ) ) & ( InsCode c1 = 11 & InsCode c1 = 12 implies ( b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 int_addr3 ),(len (c2 . (c1 coll_addr2 )))),(Next (IC c2)) iff ex b2 being FinSequence of INT ex b3 being Nat st
( b3 = abs (c2 . (c1 int_addr3 )) & b2 = b3 |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg c2,(c1 coll_addr2 ),b2),(Next (IC c2)) ) ) ) ) ;
end;

:: deftheorem Def17 defines SCM+FSA-Exec-Res SCMFSA_1:def 17 :
for b1 being Element of SCM+FSA-Instr
for b2, b3 being SCM+FSA-State holds
( ( InsCode b1 <= 8 implies ( b3 = SCM+FSA-Exec-Res b1,b2 iff ex b4 being Element of SCM-Instr ex b5 being SCM-State st
( b1 = b4 & b5 = (b2 | NAT ) +* (SCM-Instr-Loc --> b4) & b3 = (b2 +* (SCM-Exec-Res b4,b5)) +* (b2 | SCM+FSA-Instr-Loc ) ) ) ) & ( InsCode b1 = 9 implies ( b3 = SCM+FSA-Exec-Res b1,b2 iff ex b4 being Integerex b5 being Nat st
( b5 = abs (b2 . (b1 int_addr2 )) & b4 = (b2 . (b1 coll_addr1 )) /. b5 & b3 = SCM+FSA-Chg (SCM+FSA-Chg b2,(b1 int_addr1 ),b4),(Next (IC b2)) ) ) ) & ( InsCode b1 = 10 implies ( b3 = SCM+FSA-Exec-Res b1,b2 iff ex b4 being FinSequence of INT ex b5 being Nat st
( b5 = abs (b2 . (b1 int_addr2 )) & b4 = (b2 . (b1 coll_addr1 )) +* b5,(b2 . (b1 int_addr1 )) & b3 = SCM+FSA-Chg (SCM+FSA-Chg b2,(b1 coll_addr1 ),b4),(Next (IC b2)) ) ) ) & ( InsCode b1 = 11 implies ( b3 = SCM+FSA-Exec-Res b1,b2 iff b3 = SCM+FSA-Chg (SCM+FSA-Chg b2,(b1 int_addr3 ),(len (b2 . (b1 coll_addr2 )))),(Next (IC b2)) ) ) & ( InsCode b1 = 12 implies ( b3 = SCM+FSA-Exec-Res b1,b2 iff ex b4 being FinSequence of INT ex b5 being Nat st
( b5 = abs (b2 . (b1 int_addr3 )) & b4 = b5 |-> 0 & b3 = SCM+FSA-Chg (SCM+FSA-Chg b2,(b1 coll_addr2 ),b4),(Next (IC b2)) ) ) ) & ( not InsCode b1 <= 8 & not InsCode b1 = 9 & not InsCode b1 = 10 & not InsCode b1 = 11 & not InsCode b1 = 12 implies ( b3 = SCM+FSA-Exec-Res b1,b2 iff b3 = b2 ) ) );

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

:: deftheorem Def18 defines SCM+FSA-Exec SCMFSA_1:def 18 :
for b1 being Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) holds
( b1 = SCM+FSA-Exec iff for b2 being Element of SCM+FSA-Instr
for b3 being SCM+FSA-State holds (b1 . b2) . b3 = SCM+FSA-Exec-Res b2,b3 );

theorem Th20: :: SCMFSA_1:20
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg b1,b2) . 0 = b2
proof end;

theorem Th21: :: SCMFSA_1:21
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Instr-Loc
for b3 being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg b1,b2) . b3 = b1 . b3
proof end;

theorem Th22: :: SCMFSA_1:22
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Instr-Loc
for b3 being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg b1,b2) . b3 = b1 . b3
proof end;

theorem Th23: :: SCMFSA_1:23
for b1 being SCM+FSA-State
for b2, b3 being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg b1,b2) . b3 = b1 . b3
proof end;

theorem Th24: :: SCMFSA_1:24
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data-Loc
for b3 being Integer holds (SCM+FSA-Chg b1,b2,b3) . 0 = b1 . 0
proof end;

theorem Th25: :: SCMFSA_1:25
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data-Loc
for b3 being Integer holds (SCM+FSA-Chg b1,b2,b3) . b2 = b3
proof end;

theorem Th26: :: SCMFSA_1:26
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data-Loc
for b3 being Integer
for b4 being Element of SCM+FSA-Data-Loc st b4 <> b2 holds
(SCM+FSA-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th27: :: SCMFSA_1:27
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data-Loc
for b3 being Integer
for b4 being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th28: :: SCMFSA_1:28
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data-Loc
for b3 being Integer
for b4 being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th29: :: SCMFSA_1:29
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data*-Loc
for b3 being FinSequence of INT holds (SCM+FSA-Chg b1,b2,b3) . b2 = b3
proof end;

theorem Th30: :: SCMFSA_1:30
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data*-Loc
for b3 being FinSequence of INT
for b4 being Element of SCM+FSA-Data*-Loc st b4 <> b2 holds
(SCM+FSA-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th31: :: SCMFSA_1:31
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data*-Loc
for b3 being FinSequence of INT
for b4 being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th32: :: SCMFSA_1:32
for b1 being SCM+FSA-State
for b2 being Element of SCM+FSA-Data*-Loc
for b3 being FinSequence of INT
for b4 being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg b1,b2,b3) . b4 = b1 . b4
proof end;