begin
:: deftheorem defines SCM+FSA-Data*-Loc SCMFSA_1:def 1 :
SCM+FSA-Data*-Loc = INT \ NAT ;
:: deftheorem defines SCM+FSA-Memory SCMFSA_1:def 2 :
SCM+FSA-Memory = SCM-Memory \/ SCM+FSA-Data*-Loc ;
theorem Th1:
:: deftheorem SCMFSA_1:def 3 :
canceled;
definition
func SCM+FSA-Instr -> non
empty set equals
(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 non empty set
;
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 Th2:
LmX:
SCM+FSA-Instr c= [:NAT ,(NAT * ),(proj2 SCM+FSA-Instr ):]
theorem Th3:
theorem
:: deftheorem SCMFSA_1:def 5 :
canceled;
:: deftheorem defines SCM+FSA-OK SCMFSA_1:def 6 :
SCM+FSA-OK = ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ));
Lm1:
dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= NAT
Lm2:
rng (SCM-OK | NAT ) c= {SCM-Instr }
Lm3:
NAT c= dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))
theorem Th5:
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
Lm4:
SCM+FSA-Data*-Loc misses SCM-Memory
theorem Th12:
theorem Th13:
theorem
theorem
theorem
theorem
theorem Th18:
theorem Th19:
:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 7 :
for s being SCM+FSA-State
for u being Nat holds SCM+FSA-Chg s,u = s +* (NAT .--> u);
:: 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);
:: 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 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
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 `3_3 &
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 `3_3 & b1 = c )
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 `3_3 & 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 `3_3 & b2 = c ) holds
b1 = b2
func x int_addr2 -> Element of
SCM+FSA-Data-Loc means
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 `3_3 &
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 `3_3 & b1 = b )
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 `3_3 & 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 `3_3 & b2 = b ) holds
b1 = b2;
func x coll_addr1 -> Element of
SCM+FSA-Data*-Loc means
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 `3_3 &
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 `3_3 & b1 = f )
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 `3_3 & 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 `3_3 & b2 = f ) holds
b1 = b2;
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 `3_3 & 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 `3_3 & 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 `3_3 & 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
ex
c being
Element of
SCM+FSA-Data-Loc ex
f being
Element of
SCM+FSA-Data*-Loc st
(
<*c,f*> = x `3_3 &
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 `3_3 & b1 = c )
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 `3_3 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = c ) holds
b1 = b2
func x coll_addr2 -> Element of
SCM+FSA-Data*-Loc means
ex
c being
Element of
SCM+FSA-Data-Loc ex
f being
Element of
SCM+FSA-Data*-Loc st
(
<*c,f*> = x `3_3 &
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 `3_3 & b1 = f )
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 `3_3 & b1 = f ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = f ) holds
b1 = b2;
canceled;
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 `3_3 & 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 `3_3 & b2 = f ) );
:: deftheorem SCMFSA_1:def 15 :
canceled;
:: deftheorem defines IC SCMFSA_1:def 16 :
for s being SCM+FSA-State holds IC s = s . NAT ;
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
ex
x9 being
Element of
SCM-Instr ex
s9 being
SCM-State st
(
x = x9 &
s9 = (s | SCM-Memory ) +* (NAT --> x9) &
it = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) )
if x `1_3 <= 8
ex
i being
Integer ex
k being
Element of
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),
(succ (IC s)) )
if x `1_3 = 9
ex
f being
FinSequence of
INT ex
k being
Element of
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),
(succ (IC s)) )
if x `1_3 = 10
it = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),
(succ (IC s)) if x `1_3 = 11
ex
f being
FinSequence of
INT ex
k being
Element of
NAT st
(
k = abs (s . (x int_addr3 )) &
f = k |-> 0 &
it = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),
(succ (IC s)) )
if x `1_3 = 12
otherwise it = s;
existence
( ( x `1_3 <= 8 implies ex b1 being SCM+FSA-State ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) ) & ( x `1_3 = 9 implies ex b1 being SCM+FSA-State ex i being Integer ex k being Element of 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),(succ (IC s)) ) ) & ( x `1_3 = 10 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) ) & ( x `1_3 = 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 )))),(succ (IC s)) ) & ( x `1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 implies ex b1 being SCM+FSA-State st b1 = s ) )
uniqueness
for b1, b2 being SCM+FSA-State holds
( ( x `1_3 <= 8 & ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) & ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b2 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) implies b1 = b2 ) & ( x `1_3 = 9 & ex i being Integer ex k being Element of 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),(succ (IC s)) ) & ex i being Integer ex k being Element of 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),(succ (IC s)) ) implies b1 = b2 ) & ( x `1_3 = 10 & ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) & ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) implies b1 = b2 ) & ( x `1_3 = 11 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) & b2 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) implies b1 = b2 ) & ( x `1_3 = 12 & ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) & ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b2 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) implies b1 = b2 ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & b1 = s & b2 = s implies b1 = b2 ) )
;
consistency
for b1 being SCM+FSA-State holds
( ( x `1_3 <= 8 & x `1_3 = 9 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) iff ex i being Integer ex k being Element of 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),(succ (IC s)) ) ) ) & ( x `1_3 <= 8 & x `1_3 = 10 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) iff ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) ) ) & ( x `1_3 <= 8 & x `1_3 = 11 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( x `1_3 <= 8 & x `1_3 = 12 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( x `1_3 = 9 & x `1_3 = 10 implies ( ex i being Integer ex k being Element of 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),(succ (IC s)) ) iff ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) ) ) & ( x `1_3 = 9 & x `1_3 = 11 implies ( ex i being Integer ex k being Element of 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),(succ (IC s)) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( x `1_3 = 9 & x `1_3 = 12 implies ( ex i being Integer ex k being Element of 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),(succ (IC s)) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( x `1_3 = 10 & x `1_3 = 11 implies ( ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( x `1_3 = 10 & x `1_3 = 12 implies ( ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( x `1_3 = 11 & x `1_3 = 12 implies ( b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (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
( ( x `1_3 <= 8 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory ) +* (NAT --> x9) & b3 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ) ) ) & ( x `1_3 = 9 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex i being Integer ex k being Element of 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),(succ (IC s)) ) ) ) & ( x `1_3 = 10 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex f being FinSequence of INT ex k being Element of 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),(succ (IC s)) ) ) ) & ( x `1_3 = 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 )))),(succ (IC s)) ) ) & ( x `1_3 = 12 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b3 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 implies ( b3 = SCM+FSA-Exec-Res x,s iff b3 = s ) ) );
:: deftheorem defines SCM+FSA-Exec SCMFSA_1:def 18 :
for b1 being Action of SCM+FSA-Instr ,(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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem