:: SCMFSA_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 defines SCM+FSA-Data-Loc SCMFSA_1:def 1 :
SCM+FSA-Data-Loc = SCM-Data-Loc ;

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

:: deftheorem 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 \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;
coherence
(SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } is Subset of [:(Segm 13),(((union {INT ,(INT * )}) \/ INT ) * ):]
proof end;
end;

:: deftheorem defines SCM+FSA-Instr SCMFSA_1:def 4 :
SCM+FSA-Instr = (SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

theorem :: SCMFSA_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: SCMFSA_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 I be Element of SCM+FSA-Instr ;
func InsCode I -> Nat equals :: SCMFSA_1:def 5
I `1 ;
coherence
I `1 is Nat
proof end;
end;

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

theorem Th3: :: SCMFSA_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Element of SCM+FSA-Instr st InsCode I <= 8 holds
I in SCM-Instr
proof end;

theorem :: SCMFSA_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
[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 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 ));

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

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

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

theorem :: SCMFSA_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SCMFSA_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for c, b being Element of SCM+FSA-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,<*c,f,b*>] in SCM+FSA-Instr
proof end;

theorem :: SCMFSA_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for c being Element of SCM+FSA-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds
[x,<*c,f*>] in SCM+FSA-Instr
proof end;

theorem Th8: :: SCMFSA_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
INT = (({0} \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc ) \/ SCM+FSA-Instr-Loc
proof end;

theorem Th9: :: SCMFSA_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
SCM+FSA-OK . 0 = SCM+FSA-Instr-Loc
proof end;

theorem Th10: :: SCMFSA_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = INT
proof end;

theorem Th11: :: SCMFSA_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Element of SCM+FSA-Instr-Loc holds SCM+FSA-OK . a = SCM+FSA-Instr
proof end;

theorem Th12: :: SCMFSA_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = INT *
proof end;

theorem Th13: :: SCMFSA_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 :: SCMFSA_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer st SCM+FSA-OK . i = SCM+FSA-Instr-Loc holds
i = 0
proof end;

theorem :: SCMFSA_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer st SCM+FSA-OK . i = INT holds
i in SCM+FSA-Data-Loc
proof end;

theorem :: SCMFSA_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer st SCM+FSA-OK . i = SCM+FSA-Instr holds
i in SCM+FSA-Instr-Loc
proof end;

theorem :: SCMFSA_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer st SCM+FSA-OK . i = INT * holds
i 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for I being Element of SCM-Instr holds (s | NAT ) +* (SCM-Instr-Loc --> I) is SCM-State
proof end;

theorem Th19: :: SCMFSA_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for s' being SCM-State holds (s +* s') +* (s | SCM+FSA-Instr-Loc ) is SCM+FSA-State
proof end;

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

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

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

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

definition
let s be SCM+FSA-State;
let t be Element of SCM+FSA-Data*-Loc ;
let u be FinSequence of INT ;
func SCM+FSA-Chg s,t,u -> SCM+FSA-State equals :: SCMFSA_1:def 9
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM+FSA-State
proof end;
end;

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

definition
let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data-Loc ;
:: original: .
redefine func s . a -> Integer;
coherence
s . a is Integer
proof end;
end;

definition
let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data*-Loc ;
:: original: .
redefine func s . a -> FinSequence of INT ;
coherence
s . a is FinSequence of INT
proof end;
end;

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM+FSA-Data-Loc , f being Element of SCM+FSA-Data*-Loc , b being Element of SCM+FSA-Data-Loc , J being Element of Segm 13 such that A1: x = [J,<*c,f,b*>] ;
func x int_addr1 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 10
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & it = c );
existence
ex b1, c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = c )
proof end;
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = c ) holds
b1 = b2
proof end;
func x int_addr2 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 11
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & it = b );
existence
ex b1, c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = b )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = b ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = b ) holds
b1 = b2;
proof end;
func x coll_addr1 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 12
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & it = f );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = f )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = f ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = f ) holds
b1 = b2;
proof end;
end;

:: deftheorem defines int_addr1 SCMFSA_1:def 10 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc ex J being Element of Segm 13 st x = [J,<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = x int_addr1 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = c ) );

:: deftheorem defines int_addr2 SCMFSA_1:def 11 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc ex J being Element of Segm 13 st x = [J,<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = x int_addr2 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = b ) );

:: deftheorem defines coll_addr1 SCMFSA_1:def 12 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc ex J being Element of Segm 13 st x = [J,<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = x coll_addr1 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = f ) );

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM+FSA-Data-Loc , f being Element of SCM+FSA-Data*-Loc , J being Element of Segm 13 such that A1: x = [J,<*c,f*>] ;
func x int_addr3 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 13
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & it = c );
existence
ex b1, c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = c )
proof end;
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b2 = c ) holds
b1 = b2
proof end;
func x coll_addr2 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 14
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & it = f );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = f )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = f ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b2 = f ) holds
b1 = b2;
proof end;
end;

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

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

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

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

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

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

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

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

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 x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (it . x) . y = SCM+FSA-Exec-Res x,y;
existence
ex b1 being Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) st
for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res x,y
proof end;
uniqueness
for b1, b2 being Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) st ( for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res x,y ) & ( for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b2 . x) . y = SCM+FSA-Exec-Res x,y ) holds
b1 = b2
proof end;
end;

:: deftheorem 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 x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res x,y );

theorem :: SCMFSA_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for u being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg s,u) . 0 = u
proof end;

theorem :: SCMFSA_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for u being Element of SCM+FSA-Instr-Loc
for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg s,u) . mk = s . mk
proof end;

theorem :: SCMFSA_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for u being Element of SCM+FSA-Instr-Loc
for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg s,u) . p = s . p
proof end;

theorem :: SCMFSA_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for u, v being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg s,u) . v = s . v
proof end;

theorem :: SCMFSA_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data-Loc
for u being Integer holds (SCM+FSA-Chg s,t,u) . 0 = s . 0
proof end;

theorem :: SCMFSA_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data-Loc
for u being Integer holds (SCM+FSA-Chg s,t,u) . t = u
proof end;

theorem :: SCMFSA_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data-Loc
for u being Integer
for mk being Element of SCM+FSA-Data-Loc st mk <> t holds
(SCM+FSA-Chg s,t,u) . mk = s . mk
proof end;

theorem :: SCMFSA_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data-Loc
for u being Integer
for f being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg s,t,u) . f = s . f
proof end;

theorem :: SCMFSA_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data-Loc
for u being Integer
for v being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg s,t,u) . v = s . v
proof end;

theorem :: SCMFSA_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT holds (SCM+FSA-Chg s,t,u) . t = u
proof end;

theorem :: SCMFSA_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT
for mk being Element of SCM+FSA-Data*-Loc st mk <> t holds
(SCM+FSA-Chg s,t,u) . mk = s . mk
proof end;

theorem :: SCMFSA_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT
for a being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg s,t,u) . a = s . a
proof end;

theorem :: SCMFSA_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT
for v being Element of SCM+FSA-Instr-Loc holds (SCM+FSA-Chg s,t,u) . v = s . v
proof end;