:: SCMFSA_1 semantic presentation

begin


notation
synonym  SCM+FSA-Data-Loc for  SCM-Data-Loc ;
end;

definition
canceled;
func SCM+FSA-Memory  ->  set  equals :: SCMFSA_1:def 2
SCM-Memory \/ SCM+FSA-Data*-Loc;
coherence
 SCM-Memory \/ SCM+FSA-Data*-Loc is set ;
end;

:: deftheorem  SCMFSA_1:def_1_:_
canceled;

:: deftheorem  defines SCM+FSA-Memory SCMFSA_1:def_2_:_
 SCM+FSA-Memory = SCM-Memory \/ SCM+FSA-Data*-Loc;

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

theorem Th1: :: SCMFSA_1:1
SCM-Memory c= SCM+FSA-Memory by XBOOLE_1:7;

definition
:: original: SCM+FSA-Data-Loc
redefine func SCM+FSA-Data-Loc  ->  Subset of SCM+FSA-Memory;
coherence
 SCM+FSA-Data-Loc is Subset of SCM+FSA-Memory
proof
 SCM-Data-Loc c= SCM-Memory ;
hence  SCM+FSA-Data-Loc is Subset of SCM+FSA-Memory by Th1, XBOOLE_1:1; ::_thesis: verum
end;
end;

definition
:: original: SCM+FSA-Data*-Loc
redefine func SCM+FSA-Data*-Loc  ->  Subset of SCM+FSA-Memory;
coherence
 SCM+FSA-Data*-Loc is Subset of SCM+FSA-Memory by XBOOLE_1:7;
end;

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


definition
canceled;
func SCM+FSA-OK  ->  Function of SCM+FSA-Memory,3 equals :: SCMFSA_1:def 4
(SCM+FSA-Memory --> 2) +* SCM-OK;
coherence
 (SCM+FSA-Memory --> 2) +* SCM-OK is Function of SCM+FSA-Memory,3
proof
A1: rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= 3
proof
 rng (SCM+FSA-Memory --> 2) = {2} by FUNCOP_1:8;
then A2: rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= {2} \/ (rng SCM-OK) by FUNCT_4:17;
 rng SCM-OK c= 2 by RELAT_1:def_19;
then  {2} \/ (rng SCM-OK) c= 2 \/ {2} by XBOOLE_1:9;
then  rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= 2 \/ {2} by A2, XBOOLE_1:1;
then  rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= succ 2 by ORDINAL1:def_1;
hence  rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= 3 ; ::_thesis: verum
end;
dom ((SCM+FSA-Memory --> 2) +* SCM-OK) = (dom (SCM+FSA-Memory --> 2)) \/ (dom SCM-OK) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ (dom SCM-OK) by FUNCOP_1:13
.= SCM+FSA-Memory \/ SCM-Memory by FUNCT_2:def_1
.= SCM+FSA-Memory by XBOOLE_1:7, XBOOLE_1:12 ;
then  dom ((SCM+FSA-Memory --> 2) +* SCM-OK) = SCM+FSA-Memory
.= SCM+FSA-Memory ;
hence  (SCM+FSA-Memory --> 2) +* SCM-OK is Function of SCM+FSA-Memory,3 by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

:: deftheorem  SCMFSA_1:def_3_:_
canceled;

:: deftheorem  defines SCM+FSA-OK SCMFSA_1:def_4_:_
 SCM+FSA-OK = (SCM+FSA-Memory --> 2) +* SCM-OK;

theorem :: SCMFSA_1:2
canceled;

theorem :: SCMFSA_1:3
canceled;

theorem :: SCMFSA_1:4
canceled;

theorem Th5: :: SCMFSA_1:5
NAT in SCM+FSA-Memory
proof
 NAT in {NAT} by TARSKI:def_1;
then  NAT in {NAT} \/ SCM-Data-Loc by XBOOLE_0:def_3;
then  NAT in SCM-Memory ;
hence  NAT in SCM+FSA-Memory by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: SCMFSA_1:6
canceled;

theorem :: SCMFSA_1:7
canceled;

theorem :: SCMFSA_1:8
SCM+FSA-Memory = ({NAT} \/ SCM+FSA-Data-Loc) \/ SCM+FSA-Data*-Loc ;

definition
func SCM*-VAL  ->  ManySortedSet of 3 equals :: SCMFSA_1:def 5
<%NAT,INT,(INT *)%>;
coherence
 <%NAT,INT,(INT *)%> is ManySortedSet of 3 ;
end;

:: deftheorem  defines SCM*-VAL SCMFSA_1:def_5_:_
 SCM*-VAL = <%NAT,INT,(INT *)%>;

Lm1:  SCM+FSA-Data*-Loc misses SCM-Memory
proof
assume  SCM+FSA-Data*-Loc meets SCM-Memory ; ::_thesis: contradiction
then consider x being set  such that
A1: x in SCM+FSA-Data*-Loc and
A2: x in SCM-Memory by XBOOLE_0:3;
A3: ( x in {NAT} \/ SCM-Data-Loc or x in NAT ) by A2;
 x in (NAT \/ [:{0},NAT:]) \ {[0,0]} by A1, NUMBERS:def_4;
then A4: ( x in NAT or x in [:{0},NAT:] ) by XBOOLE_0:def_3;
percases ( x in {NAT} or x in SCM-Data-Loc or x in NAT ) by A3, XBOOLE_0:def_3;
supposeA5: x in {NAT} ; ::_thesis: contradiction
then  ex y, z being set st x = [y,z] by A4, RELAT_1:def_1, TARSKI:def_1;
hence  contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
suppose x in SCM-Data-Loc ; ::_thesis: contradiction
then A6: ex k being Element of NAT st x = [1,k] by AMI_2:23;
then consider y, z being set  such that
A7: y in {0} and
 z in NAT and
A8: x = [y,z] by A4, ZFMISC_1:84;
 y = 0 by A7, TARSKI:def_1;
hence  contradiction by A6, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose x in NAT ; ::_thesis: contradiction
hence  contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;

Lm2:  dom SCM-OK c= dom SCM+FSA-OK
proof
 dom SCM+FSA-OK = (dom (SCM+FSA-Memory --> 2)) \/ (dom SCM-OK) by FUNCT_4:def_1;
hence  dom SCM-OK c= dom SCM+FSA-OK by XBOOLE_1:7; ::_thesis: verum
end;

Lm3:  NAT in dom SCM+FSA-OK
proof
A1: NAT in dom SCM-OK by AMI_2:22, FUNCT_2:def_1;
 dom SCM-OK c= dom SCM+FSA-OK by Lm2;
hence  NAT in dom SCM+FSA-OK by A1; ::_thesis: verum
end;

Lm4:  SCM+FSA-OK . NAT = 0
proof
A1: NAT in dom SCM-OK by AMI_2:22, FUNCT_2:def_1;
thus SCM+FSA-OK . NAT = ((SCM+FSA-Memory --> 2) +* SCM-OK) . NAT
.= SCM-OK . NAT by A1, FUNCT_4:13
.= 0 by AMI_2:22, AMI_2:def_4 ; ::_thesis: verum
end;

theorem Th9: :: SCMFSA_1:9
(SCM*-VAL * SCM+FSA-OK) . NAT = NAT
proof
A1: SCM+FSA-OK . NAT = 0 by Lm4;
thus (SCM*-VAL * SCM+FSA-OK) . NAT = SCM*-VAL . (SCM+FSA-OK . NAT) by Lm3, FUNCT_1:13
.= NAT by A1, AFINSQ_1:39 ; ::_thesis: verum
end;

Lm5:  for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = 1
proof
let b be Element of SCM+FSA-Data-Loc ; ::_thesis: SCM+FSA-OK . b = 1
A1: b in SCM-Data-Loc ;
then  b in SCM-Memory ;
then A2: b in dom SCM-OK by FUNCT_2:def_1;
thus SCM+FSA-OK . b = ((SCM+FSA-Memory --> 2) +* SCM-OK) . b
.= SCM-OK . b by A2, FUNCT_4:13
.= 1 by A1, AMI_2:def_4 ; ::_thesis: verum
end;

theorem Th10: :: SCMFSA_1:10
for b being Element of SCM+FSA-Data-Loc holds (SCM*-VAL * SCM+FSA-OK) . b = INT
proof
let b be Element of SCM+FSA-Data-Loc ; ::_thesis: (SCM*-VAL * SCM+FSA-OK) . b = INT
 b in SCM-Data-Loc ;
then  b in SCM-Memory ;
then A1: b in dom SCM-OK by FUNCT_2:def_1;
A2: SCM+FSA-OK . b = 1 by Lm5;
A3: b in dom SCM+FSA-OK by A1, Lm2;
thus (SCM*-VAL * SCM+FSA-OK) . b = SCM*-VAL . (SCM+FSA-OK . b) by A3, FUNCT_1:13
.= SCM*-VAL . 1 by A2
.= INT by AFINSQ_1:39 ; ::_thesis: verum
end;

Lm6:  for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = 2
proof
let f be Element of SCM+FSA-Data*-Loc ; ::_thesis: SCM+FSA-OK . f = 2
 not f in SCM-Memory by Lm1, XBOOLE_0:3;
then A1: not f in dom SCM-OK by FUNCT_2:def_1;
thus SCM+FSA-OK . f = ((SCM+FSA-Memory --> 2) +* SCM-OK) . f
.= (SCM+FSA-Memory --> 2) . f by A1, FUNCT_4:11
.= 2 by FUNCOP_1:7 ; ::_thesis: verum
end;

theorem Th11: :: SCMFSA_1:11
for f being Element of SCM+FSA-Data*-Loc holds (SCM*-VAL * SCM+FSA-OK) . f = INT *
proof
let f be Element of SCM+FSA-Data*-Loc ; ::_thesis: (SCM*-VAL * SCM+FSA-OK) . f = INT *
A1: SCM+FSA-OK . f = 2 by Lm6;
 f in SCM+FSA-Memory ;
then A2: f in dom SCM+FSA-OK by FUNCT_2:def_1;
thus (SCM*-VAL * SCM+FSA-OK) . f = SCM*-VAL . (SCM+FSA-OK . f) by A2, FUNCT_1:13
.= SCM*-VAL . 2 by A1
.= INT * by AFINSQ_1:39 ; ::_thesis: verum
end;

Lm7:  dom SCM+FSA-OK = SCM+FSA-Memory
by PARTFUN1:def_2;

 len <%NAT,INT,(INT *)%> = 3
by AFINSQ_1:39;

then  rng SCM+FSA-OK c= dom SCM*-VAL
by RELAT_1:def_19;

then Lm8:  dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory
by Lm7, RELAT_1:27;

registration
clusterSCM+FSA-OK * SCM*-VAL ->  non-empty ;
coherence
 SCM*-VAL * SCM+FSA-OK is non-empty
proof
set F = SCM*-VAL * SCM+FSA-OK;
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in proj1 (SCM*-VAL * SCM+FSA-OK) or not (SCM*-VAL * SCM+FSA-OK) . n is empty )
assume A1: n in dom (SCM*-VAL * SCM+FSA-OK) ; ::_thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty
 dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then  ( n in SCM-Memory or n in SCM+FSA-Data*-Loc ) by A1, XBOOLE_0:def_3;
percasesthen  ( n = NAT or n in SCM-Data-Loc or n in SCM+FSA-Data*-Loc ) by AMI_2:26;
suppose n = NAT ; ::_thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty
then  (SCM*-VAL * SCM+FSA-OK) . n = NAT by Th9;
hence  not (SCM*-VAL * SCM+FSA-OK) . n is empty ; ::_thesis: verum
end;
suppose n in SCM-Data-Loc ; ::_thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty
then  (SCM*-VAL * SCM+FSA-OK) . n = INT by Th10;
hence  not (SCM*-VAL * SCM+FSA-OK) . n is empty ; ::_thesis: verum
end;
suppose n in SCM+FSA-Data*-Loc ; ::_thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty
then  (SCM*-VAL * SCM+FSA-OK) . n = INT * by Th11;
hence  not (SCM*-VAL * SCM+FSA-OK) . n is empty ; ::_thesis: verum
end;
end;
end;
end;

definition
mode SCM+FSA-State is Element of product (SCM*-VAL * SCM+FSA-OK);
end;

theorem :: SCMFSA_1:12
canceled;

theorem :: SCMFSA_1:13
canceled;

theorem :: SCMFSA_1:14
canceled;

theorem :: SCMFSA_1:15
canceled;

theorem :: SCMFSA_1:16
canceled;

theorem Th17: :: SCMFSA_1:17
for s being SCM+FSA-State
for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State
proof
let s be SCM+FSA-State; ::_thesis: for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State
let I be Element of SCM-Instr ; ::_thesis: s | SCM-Memory is SCM-State
A1: dom (s | SCM-Memory) = (dom s) /\ SCM-Memory by RELAT_1:61
.= SCM+FSA-Memory /\ SCM-Memory by Lm8, CARD_3:9
.= SCM-Memory by XBOOLE_1:21 ;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(SCM-VAL_*_SCM-OK)_holds_
(s_|_SCM-Memory)_._x_in_(SCM-VAL_*_SCM-OK)_._x
let x be set ; ::_thesis: ( x in dom (SCM-VAL * SCM-OK) implies (s | SCM-Memory) . b1 in (SCM-VAL * SCM-OK) . b1 )
assume  x in dom (SCM-VAL * SCM-OK) ; ::_thesis: (s | SCM-Memory) . b1 in (SCM-VAL * SCM-OK) . b1
then A3: x in SCM-Memory by AMI_2:27;
then A4: x in {NAT} \/ SCM-Data-Loc ;
percases ( x in {NAT} or x in SCM-Data-Loc ) by A4, XBOOLE_0:def_3;
supposeA5: x in {NAT} ; ::_thesis: (s | SCM-Memory) . b1 in (SCM-VAL * SCM-OK) . b1
A6: (s | SCM-Memory) . x = (s | SCM-Memory) . x
.= s . x by A1, A3, FUNCT_1:47 ;
reconsider a = x as Element of SCM+FSA-Memory by A3, Th1;
A7: s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def_6;
A8: x = NAT by A5, TARSKI:def_1;
 dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then  pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = NAT by A8, Th9, CARD_3:12;
hence  (s | SCM-Memory) . x in (SCM-VAL * SCM-OK) . x by A8, A6, A7, AMI_2:6; ::_thesis: verum
end;
supposeA9: x in SCM-Data-Loc ; ::_thesis: (s | SCM-Memory) . b1 in (SCM-VAL * SCM-OK) . b1
A10: (s | SCM-Memory) . x = (s | SCM-Memory) . x
.= s . x by A1, A3, FUNCT_1:47 ;
reconsider a = x as Element of SCM+FSA-Memory by A3, Th1;
 dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then A11: pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = (SCM*-VAL * SCM+FSA-OK) . a by CARD_3:12
.= INT by A9, Th10 ;
 s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def_6;
hence  (s | SCM-Memory) . x in (SCM-VAL * SCM-OK) . x by A9, A10, A11, AMI_2:8; ::_thesis: verum
end;
end;
end;
dom (s | SCM-Memory) = dom (s | SCM-Memory)
.= SCM-Memory by A1
.= dom (SCM-VAL * SCM-OK) by AMI_2:27 ;
hence  s | SCM-Memory is SCM-State by A2, CARD_3:9; ::_thesis: verum
end;

theorem Th18: :: SCMFSA_1:18
for s being SCM+FSA-State
for s1 being SCM-State holds s +* s1 is SCM+FSA-State
proof
let s be SCM+FSA-State; ::_thesis: for s1 being SCM-State holds s +* s1 is SCM+FSA-State
let s1 be SCM-State; ::_thesis: s +* s1 is SCM+FSA-State
A1: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then reconsider f = SCM*-VAL * SCM+FSA-OK as non-empty ManySortedSet of SCM+FSA-Memory by PARTFUN1:def_2;
A2: dom s1 = dom (SCM-VAL * SCM-OK) by CARD_3:9
.= SCM-Memory by AMI_2:27 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_s1_holds_
s1_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom s1 implies s1 . b1 in f . b1 )
assume A3: x in dom s1 ; ::_thesis: s1 . b1 in f . b1
then A4: x in {NAT} \/ SCM-Data-Loc by A2;
percases ( x in {NAT} or x in SCM-Data-Loc ) by A4, XBOOLE_0:def_3;
supposeA5: x in {NAT} ; ::_thesis: s1 . b1 in f . b1
reconsider a = x as Element of SCM-Memory by A2, A3;
A6: s1 . a in pi ((product (SCM-VAL * SCM-OK)),a) by CARD_3:def_6;
A7: x = NAT by A5, TARSKI:def_1;
 dom (SCM-VAL * SCM-OK) = SCM-Memory by AMI_2:27;
then  pi ((product (SCM-VAL * SCM-OK)),a) = (SCM-VAL * SCM-OK) . a by CARD_3:12
.= NAT by A7, AMI_2:6 ;
hence  s1 . x in f . x by A5, A6, Th9, TARSKI:def_1; ::_thesis: verum
end;
supposeA8: x in SCM-Data-Loc ; ::_thesis: s1 . b1 in f . b1
reconsider a = x as Element of SCM-Memory by A2, A3;
A9: s1 . a in pi ((product (SCM-VAL * SCM-OK)),a) by CARD_3:def_6;
 dom (SCM-VAL * SCM-OK) = SCM-Memory by AMI_2:27;
then A10: pi ((product (SCM-VAL * SCM-OK)),a) = (SCM-VAL * SCM-OK) . a by CARD_3:12;
 (SCM*-VAL * SCM+FSA-OK) . x = INT by A8, Th10;
hence  s1 . x in f . x by A8, A10, A9, AMI_2:8; ::_thesis: verum
end;
end;
end;
then  s +* s1 is SCM+FSA-State by A1, A2, PRE_CIRC:6, XBOOLE_1:7;
hence  s +* s1 is SCM+FSA-State ; ::_thesis: verum
end;

definition
let s be SCM+FSA-State;
let u be Nat;
func SCM+FSA-Chg (s,u) ->  SCM+FSA-State equals :: SCMFSA_1:def 6
s +* (NAT .--> u);
coherence
 s +* (NAT .--> u) is SCM+FSA-State
proof
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(SCM*-VAL_*_SCM+FSA-OK)_holds_
(s_+*_(NAT_.-->_u))_._x_in_(SCM*-VAL_*_SCM+FSA-OK)_._x
let x be set ; ::_thesis: ( x in dom (SCM*-VAL * SCM+FSA-OK) implies (s +* (NAT .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1 )
assume A2: x in dom (SCM*-VAL * SCM+FSA-OK) ; ::_thesis: (s +* (NAT .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
percases ( x = NAT or x <> NAT ) ;
supposeA3: x = NAT ; ::_thesis: (s +* (NAT .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  NAT in dom (NAT .--> u) by TARSKI:def_1;
then (s +* (NAT .--> u)) . NAT = (NAT .--> u) . NAT by FUNCT_4:13
.= u by FUNCOP_1:72 ;
hence  (s +* (NAT .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A3, Th9, ORDINAL1:def_12; ::_thesis: verum
end;
supposeA4: x <> NAT ; ::_thesis: (s +* (NAT .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  not x in dom (NAT .--> u) by A4, TARSKI:def_1;
then  (s +* (NAT .--> u)) . x = s . x by FUNCT_4:11;
hence  (s +* (NAT .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
A5: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then  dom s = SCM+FSA-Memory by CARD_3:9;
then  dom (s +* (NAT .--> u)) = SCM+FSA-Memory \/ (dom (NAT .--> u)) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ {NAT} by FUNCOP_1:13
.= dom (SCM*-VAL * SCM+FSA-OK) by A5, Th5, ZFMISC_1:40 ;
hence  s +* (NAT .--> u) is SCM+FSA-State by A1, CARD_3:9; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM+FSA-Chg SCMFSA_1:def_6_:_
 for s being SCM+FSA-State
for u being Nat holds SCM+FSA-Chg (s,u) = s +* (NAT .--> 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 7
s +* (t .--> u);
coherence
 s +* (t .--> u) is SCM+FSA-State
proof
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(SCM*-VAL_*_SCM+FSA-OK)_holds_
(s_+*_(t_.-->_u))_._x_in_(SCM*-VAL_*_SCM+FSA-OK)_._x
let x be set ; ::_thesis: ( x in dom (SCM*-VAL * SCM+FSA-OK) implies (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1 )
assume A2: x in dom (SCM*-VAL * SCM+FSA-OK) ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
percases ( x = t or x <> t ) ;
supposeA3: x = t ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  t in dom (t .--> u) by TARSKI:def_1;
then (s +* (t .--> u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
then  (s +* (t .--> u)) . t in INT by INT_1:def_2;
hence  (s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A3, Th10; ::_thesis: verum
end;
supposeA4: x <> t ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  not x in dom (t .--> u) by A4, TARSKI:def_1;
then  (s +* (t .--> u)) . x = s . x by FUNCT_4:11;
hence  (s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
A5: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then  dom s = SCM+FSA-Memory by CARD_3:9;
then  dom (s +* (t .--> u)) = SCM+FSA-Memory \/ (dom (t .--> u)) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ {t} by FUNCOP_1:13
.= dom (SCM*-VAL * SCM+FSA-OK) by A5, ZFMISC_1:40 ;
hence  s +* (t .--> u) is SCM+FSA-State by A1, CARD_3:9; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM+FSA-Chg SCMFSA_1:def_7_:_
 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 8
s +* (t .--> u);
coherence
 s +* (t .--> u) is SCM+FSA-State
proof
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(SCM*-VAL_*_SCM+FSA-OK)_holds_
(s_+*_(t_.-->_u))_._x_in_(SCM*-VAL_*_SCM+FSA-OK)_._x
let x be set ; ::_thesis: ( x in dom (SCM*-VAL * SCM+FSA-OK) implies (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1 )
assume A2: x in dom (SCM*-VAL * SCM+FSA-OK) ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
percases ( x = t or x <> t ) ;
supposeA3: x = t ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  t in dom (t .--> u) by TARSKI:def_1;
then (s +* (t .--> u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
then  (s +* (t .--> u)) . t in INT * by FINSEQ_1:def_11;
hence  (s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A3, Th11; ::_thesis: verum
end;
supposeA4: x <> t ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM*-VAL * SCM+FSA-OK) . b1
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  not x in dom (t .--> u) by A4, TARSKI:def_1;
then  (s +* (t .--> u)) . x = s . x by FUNCT_4:11;
hence  (s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
A5: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then  dom s = SCM+FSA-Memory by CARD_3:9;
then  dom (s +* (t .--> u)) = SCM+FSA-Memory \/ (dom (t .--> u)) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ {t} by FUNCOP_1:13
.= dom (SCM*-VAL * SCM+FSA-OK) by A5, ZFMISC_1:40 ;
hence  s +* (t .--> u) is SCM+FSA-State by A1, CARD_3:9; ::_thesis: verum
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 FinSequence of INT holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u);

registration
let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data-Loc ;
clusters . a ->  integer ;
coherence
 s . a is integer
proof
 dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then A1: pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = (SCM*-VAL * SCM+FSA-OK) . a by CARD_3:12
.= INT by Th10 ;
 s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def_6;
hence  s . a is integer by A1; ::_thesis: verum
end;
end;

definition
let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data*-Loc ;
:: original: .
redefine funcs . a ->  FinSequence of INT ;
coherence
 s . a is FinSequence of INT
proof
 dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then A1: pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = (SCM*-VAL * SCM+FSA-OK) . a by CARD_3:12
.= INT * by Th11 ;
 s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def_6;
hence  s . a is FinSequence of INT by A1, FINSEQ_1:def_11; ::_thesis: verum
end;
end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let s be SCM+FSA-State;
func IC s ->  Element of NAT  equals :: SCMFSA_1:def 15
s . NAT;
coherence
 s . NAT is Element of NAT
proof
reconsider z = NAT as Element of SCM+FSA-Memory by Th5;
 dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then  pi ((product (SCM*-VAL * SCM+FSA-OK)),NAT) = (SCM*-VAL * SCM+FSA-OK) . z by CARD_3:12
.= NAT by Th9 ;
hence  s . NAT is Element of NAT by CARD_3:def_6; ::_thesis: verum
end;
end;

:: deftheorem  SCMFSA_1:def_9_:_
canceled;

:: deftheorem  SCMFSA_1:def_10_:_
canceled;

:: deftheorem  SCMFSA_1:def_11_:_
canceled;

:: deftheorem  SCMFSA_1:def_12_:_
canceled;

:: deftheorem  SCMFSA_1:def_13_:_
canceled;

:: deftheorem  SCMFSA_1:def_14_:_
canceled;

:: deftheorem  defines IC SCMFSA_1:def_15_:_
 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 :: SCMFSA_1:def 16
 ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & it = s +* (SCM-Exec-Res (x9,s9)) ) 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
ex i being Integer st
( i = 1 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) if x `1_3 = 13
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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) ) & ( 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))) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
proof
hereby  ::_thesis: ( ( 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))) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
assume  x `1_3 <= 8 ; ::_thesis: ex s1 being SCM+FSA-State ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )
then reconsider x9 = x as Element of SCM-Instr by SCMFSA_I:2;
reconsider s9 = s | SCM-Memory as SCM-State by Th17;
reconsider s1 = s +* (SCM-Exec-Res (x9,s9)) as SCM+FSA-State by Th18;
take s1 = s1; ::_thesis: ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )
take x9 = x9; ::_thesis: ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )
take s9 = s9; ::_thesis: ( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )
thus  x = x9 ; ::_thesis: ( s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )
thus  s9 = s | SCM-Memory ; ::_thesis: s1 = s +* (SCM-Exec-Res (x9,s9))
thus  s1 = s +* (SCM-Exec-Res (x9,s9)) ; ::_thesis: verum
end;
hereby  ::_thesis: ( ( 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))) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
reconsider k = abs (s . (x int_addr2)) as Element of NAT ;
assume  x `1_3 = 9 ; ::_thesis: ex s1 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 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))) )
reconsider i = (s . (x coll_addr1)) /. k as Integer ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))); ::_thesis: ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2)) & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))) )
take i = i; ::_thesis: ex k being Element of NAT st
( k = abs (s . (x int_addr2)) & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))) )
take k = k; ::_thesis: ( k = abs (s . (x int_addr2)) & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))) )
thus  ( k = abs (s . (x int_addr2)) & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))) ) ; ::_thesis: verum
end;
hereby  ::_thesis: ( ( 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))) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
reconsider k = abs (s . (x int_addr2)) as Element of NAT ;
assume  x `1_3 = 10 ; ::_thesis: ex s1 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))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
percases ( k in dom (s . (x coll_addr1)) or not k in dom (s . (x coll_addr1)) ) ;
supposeA1: k in dom (s . (x coll_addr1)) ; ::_thesis: ex s1 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))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
set f = (s . (x coll_addr1)) +* (k .--> (s . (x int_addr1)));
A2: {k} c= dom (s . (x coll_addr1)) by A1, ZFMISC_1:31;
dom ((s . (x coll_addr1)) +* (k .--> (s . (x int_addr1)))) = (dom (s . (x coll_addr1))) \/ (dom (k .--> (s . (x int_addr1)))) by FUNCT_4:def_1
.= (dom (s . (x coll_addr1))) \/ {k} by FUNCOP_1:13
.= dom (s . (x coll_addr1)) by A2, XBOOLE_1:12
.= Seg (len (s . (x coll_addr1))) by FINSEQ_1:def_3 ;
then reconsider f = (s . (x coll_addr1)) +* (k .--> (s . (x int_addr1))) as FinSequence by FINSEQ_1:def_2;
 ( s . (x int_addr1) in INT & rng (k .--> (s . (x int_addr1))) = {(s . (x int_addr1))} ) by FUNCOP_1:8, INT_1:def_2;
then  ( rng (s . (x coll_addr1)) c= INT & rng (k .--> (s . (x int_addr1))) c= INT ) by FINSEQ_1:def_4, ZFMISC_1:31;
then  ( rng f c= (rng (s . (x coll_addr1))) \/ (rng (k .--> (s . (x int_addr1)))) & (rng (s . (x coll_addr1))) \/ (rng (k .--> (s . (x int_addr1)))) c= INT ) by FUNCT_4:17, XBOOLE_1:8;
then  rng f c= INT by XBOOLE_1:1;
then reconsider f = f as FinSequence of INT by FINSEQ_1:def_4;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))); ::_thesis: 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))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
take f = f; ::_thesis: ex k being Element of NAT st
( k = abs (s . (x int_addr2)) & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
take k = k; ::_thesis: ( k = abs (s . (x int_addr2)) & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
thus  k = abs (s . (x int_addr2)) ; ::_thesis: ( f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
thus  f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) by A1, FUNCT_7:def_3; ::_thesis: s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s)))
thus  s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) ; ::_thesis: verum
end;
supposeA3: not k in dom (s . (x coll_addr1)) ; ::_thesis: ex s1 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))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
reconsider f = s . (x coll_addr1) as FinSequence of INT ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))); ::_thesis: 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))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
take f = f; ::_thesis: ex k being Element of NAT st
( k = abs (s . (x int_addr2)) & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
take k = k; ::_thesis: ( k = abs (s . (x int_addr2)) & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
thus  k = abs (s . (x int_addr2)) ; ::_thesis: ( f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) )
thus  f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) by A3, FUNCT_7:def_3; ::_thesis: s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s)))
thus  s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) ; ::_thesis: verum
end;
end;
end;
thus  ( x `1_3 = 11 implies ex s1 being SCM+FSA-State st s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),(succ (IC s))) ) ; ::_thesis: ( ( 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))) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
hereby  ::_thesis: ( ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
reconsider k = abs (s . (x int_addr3)) as Element of NAT ;
assume  x `1_3 = 12 ; ::_thesis: ex s1 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 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))) )
 0 in INT by INT_1:def_2;
then A4: {0} c= INT by ZFMISC_1:31;
 k |-> 0 = (Seg k) --> 0 by FINSEQ_2:def_2;
then  rng (k |-> 0) c= {0} by FUNCOP_1:13;
then  rng (k |-> 0) c= INT by A4, XBOOLE_1:1;
then reconsider f = k |-> 0 as FinSequence of INT by FINSEQ_1:def_4;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))); ::_thesis: ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3)) & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))) )
take f = f; ::_thesis: ex k being Element of NAT st
( k = abs (s . (x int_addr3)) & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))) )
take k = k; ::_thesis: ( k = abs (s . (x int_addr3)) & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))) )
thus  ( k = abs (s . (x int_addr3)) & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))) ) ; ::_thesis: verum
end;
hereby  ::_thesis: ( 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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s )
assume  x `1_3 = 13 ; ::_thesis: ex s1 being SCM+FSA-State ex i being Integer st
( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) )
reconsider i = 1 as Integer ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))); ::_thesis: ex i being Integer st
( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) )
take i = i; ::_thesis: ( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) )
thus  ( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ; ::_thesis: verum
end;
thus  ( 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 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) ; ::_thesis: verum
end;
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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) & ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & b2 = s +* (SCM-Exec-Res (x9,s9)) ) 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 ) & ( x `1_3 = 13 & ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) & ex i being Integer st
( i = 1 & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 & 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 <= 8 & x `1_3 = 13 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) iff ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 = 9 & x `1_3 = 13 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 i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 = 10 & x `1_3 = 13 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 i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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))) ) ) ) & ( x `1_3 = 11 & x `1_3 = 13 implies ( b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),(succ (IC s))) iff ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) & ( x `1_3 = 12 & x `1_3 = 13 implies ( 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))) ) iff ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) ) ;
end;

:: deftheorem  defines SCM+FSA-Exec-Res SCMFSA_1:def_16_:_
 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 & b3 = s +* (SCM-Exec-Res (x9,s9)) ) ) ) & ( 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))) ) ) ) & ( x `1_3 = 13 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex i being Integer st
( i = 1 & b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(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 & not x `1_3 = 13 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff b3 = s ) ) );

definition
func SCM+FSA-Exec  ->  Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) means :: SCMFSA_1:def 17
 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 Action of SCM+FSA-Instr,(product (SCM*-VAL * 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
deffunc H1( Element of SCM+FSA-Instr , SCM+FSA-State) ->  SCM+FSA-State = SCM+FSA-Exec-Res ($1,$2);
consider f being Function of [:SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)):],(product (SCM*-VAL * SCM+FSA-OK)) such that
A1: for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  curry f ; ::_thesis: for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds ((curry f) . x) . y = SCM+FSA-Exec-Res (x,y)
let x be Element of SCM+FSA-Instr ; ::_thesis: for y being SCM+FSA-State holds ((curry f) . x) . y = SCM+FSA-Exec-Res (x,y)
let y be SCM+FSA-State; ::_thesis: ((curry f) . x) . y = SCM+FSA-Exec-Res (x,y)
thus ((curry f) . x) . y = f . (x,y) by FUNCT_5:69
.= SCM+FSA-Exec-Res (x,y) by A1 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Action of SCM+FSA-Instr,(product (SCM*-VAL * 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
let f, g be Function of SCM+FSA-Instr,(Funcs ((product (SCM*-VAL * SCM+FSA-OK)),(product (SCM*-VAL * SCM+FSA-OK)))); ::_thesis: ( ( for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (f . x) . y = SCM+FSA-Exec-Res (x,y) ) & ( for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (g . x) . y = SCM+FSA-Exec-Res (x,y) ) implies f = g )
assume that
A2: for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (f . x) . y = SCM+FSA-Exec-Res (x,y) and
A3: for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (g . x) . y = SCM+FSA-Exec-Res (x,y) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_SCM+FSA-Instr_holds_f_._x_=_g_._x
let x be Element of SCM+FSA-Instr ; ::_thesis: f . x = g . x
reconsider gx = g . x, fx = f . x as Function of (product (SCM*-VAL * SCM+FSA-OK)),(product (SCM*-VAL * SCM+FSA-OK)) ;
now__::_thesis:_for_y_being_SCM+FSA-State_holds_fx_._y_=_gx_._y
let y be SCM+FSA-State; ::_thesis: fx . y = gx . y
thus fx . y = SCM+FSA-Exec-Res (x,y) by A2
.= gx . y by A3 ; ::_thesis: verum
end;
hence  f . x = g . x by FUNCT_2:63; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM+FSA-Exec SCMFSA_1:def_17_:_
 for b1 being Action of SCM+FSA-Instr,(product (SCM*-VAL * 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:19
for s being SCM+FSA-State
for u being Element of NAT holds (SCM+FSA-Chg (s,u)) . NAT = u
proof
let s be SCM+FSA-State; ::_thesis: for u being Element of NAT holds (SCM+FSA-Chg (s,u)) . NAT = u
let u be Element of NAT ; ::_thesis: (SCM+FSA-Chg (s,u)) . NAT = u
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  NAT in dom (NAT .--> u) by TARSKI:def_1;
hence (SCM+FSA-Chg (s,u)) . NAT = (NAT .--> u) . NAT by FUNCT_4:13
.= u by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: SCMFSA_1:20
for s being SCM+FSA-State
for u being Element of NAT
for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk
proof
let s be SCM+FSA-State; ::_thesis: for u being Element of NAT
for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk
let u be Element of NAT ; ::_thesis: for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk
let mk be Element of SCM+FSA-Data-Loc ; ::_thesis: (SCM+FSA-Chg (s,u)) . mk = s . mk
 ( (SCM*-VAL * SCM+FSA-OK) . mk = INT & {NAT} = dom (NAT .--> u) ) by Th10, FUNCOP_1:13;
then  not mk in dom (NAT .--> u) by Th9, NUMBERS:27, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:21
for s being SCM+FSA-State
for u being Element of NAT
for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p
proof
let s be SCM+FSA-State; ::_thesis: for u being Element of NAT
for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p
let u be Element of NAT ; ::_thesis: for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p
let mk be Element of SCM+FSA-Data*-Loc ; ::_thesis: (SCM+FSA-Chg (s,u)) . mk = s . mk
A1: {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
A2: SCM+FSA-OK . NAT = 0 by Lm4;
 SCM+FSA-OK . mk = 2 by Lm6;
then  NAT <> mk by A2;
then  not mk in dom (NAT .--> u) by A1, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:22
for s being SCM+FSA-State
for u, v being Element of NAT holds (SCM+FSA-Chg (s,u)) . v = s . v
proof
let s be SCM+FSA-State; ::_thesis: for u, v being Element of NAT holds (SCM+FSA-Chg (s,u)) . v = s . v
let u, v be Element of NAT ; ::_thesis: (SCM+FSA-Chg (s,u)) . v = s . v
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  not v in dom (NAT .--> u) by TARSKI:def_1;
hence  (SCM+FSA-Chg (s,u)) . v = s . v by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:23
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)) . NAT = s . NAT
proof
let s be SCM+FSA-State; ::_thesis: for t being Element of SCM+FSA-Data-Loc
for u being Integer holds (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT
let t be Element of SCM+FSA-Data-Loc ; ::_thesis: for u being Integer holds (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT
let u be Integer; ::_thesis: (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT
 ( (SCM*-VAL * SCM+FSA-OK) . t = INT & {t} = dom (t .--> u) ) by Th10, FUNCOP_1:13;
then  not NAT in dom (t .--> u) by Th9, NUMBERS:27, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:24
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
let s be SCM+FSA-State; ::_thesis: for t being Element of SCM+FSA-Data-Loc
for u being Integer holds (SCM+FSA-Chg (s,t,u)) . t = u
let t be Element of SCM+FSA-Data-Loc ; ::_thesis: for u being Integer holds (SCM+FSA-Chg (s,t,u)) . t = u
let u be Integer; ::_thesis: (SCM+FSA-Chg (s,t,u)) . t = u
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  t in dom (t .--> u) by TARSKI:def_1;
hence (SCM+FSA-Chg (s,t,u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: SCMFSA_1:25
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
let s be SCM+FSA-State; ::_thesis: 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
let t be Element of SCM+FSA-Data-Loc ; ::_thesis: 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
let u be Integer; ::_thesis: for mk being Element of SCM+FSA-Data-Loc st mk <> t holds
(SCM+FSA-Chg (s,t,u)) . mk = s . mk
let mk be Element of SCM+FSA-Data-Loc ; ::_thesis: ( mk <> t implies (SCM+FSA-Chg (s,t,u)) . mk = s . mk )
assume A1: mk <> t ; ::_thesis: (SCM+FSA-Chg (s,t,u)) . mk = s . mk
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  not mk in dom (t .--> u) by A1, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,t,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:26
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
let s be SCM+FSA-State; ::_thesis: 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
let t be Element of SCM+FSA-Data-Loc ; ::_thesis: for u being Integer
for f being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,t,u)) . f = s . f
let u be Integer; ::_thesis: for f being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,t,u)) . f = s . f
let mk be Element of SCM+FSA-Data*-Loc ; ::_thesis: (SCM+FSA-Chg (s,t,u)) . mk = s . mk
A1: {t} = dom (t .--> u) by FUNCOP_1:13;
 ( (SCM*-VAL * SCM+FSA-OK) . t = INT & (SCM*-VAL * SCM+FSA-OK) . mk = INT * ) by Th10, Th11;
then  not mk in dom (t .--> u) by A1, FUNCT_7:16, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,t,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:27
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
let s be SCM+FSA-State; ::_thesis: for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT holds (SCM+FSA-Chg (s,t,u)) . t = u
let t be Element of SCM+FSA-Data*-Loc ; ::_thesis: for u being FinSequence of INT holds (SCM+FSA-Chg (s,t,u)) . t = u
let u be FinSequence of INT ; ::_thesis: (SCM+FSA-Chg (s,t,u)) . t = u
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  t in dom (t .--> u) by TARSKI:def_1;
hence (SCM+FSA-Chg (s,t,u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: SCMFSA_1:28
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
let s be SCM+FSA-State; ::_thesis: 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
let t be Element of SCM+FSA-Data*-Loc ; ::_thesis: 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
let u be FinSequence of INT ; ::_thesis: for mk being Element of SCM+FSA-Data*-Loc st mk <> t holds
(SCM+FSA-Chg (s,t,u)) . mk = s . mk
let mk be Element of SCM+FSA-Data*-Loc ; ::_thesis: ( mk <> t implies (SCM+FSA-Chg (s,t,u)) . mk = s . mk )
assume A1: mk <> t ; ::_thesis: (SCM+FSA-Chg (s,t,u)) . mk = s . mk
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  not mk in dom (t .--> u) by A1, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,t,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:29
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
let s be SCM+FSA-State; ::_thesis: 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
let t be Element of SCM+FSA-Data*-Loc ; ::_thesis: 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
let u be FinSequence of INT ; ::_thesis: for a being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,t,u)) . a = s . a
let mk be Element of SCM+FSA-Data-Loc ; ::_thesis: (SCM+FSA-Chg (s,t,u)) . mk = s . mk
A1: {t} = dom (t .--> u) by FUNCOP_1:13;
 ( (SCM*-VAL * SCM+FSA-OK) . t = INT * & (SCM*-VAL * SCM+FSA-OK) . mk = INT ) by Th10, Th11;
then  not mk in dom (t .--> u) by A1, FUNCT_7:16, TARSKI:def_1;
hence  (SCM+FSA-Chg (s,t,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: SCMFSA_1:30
SCM+FSA-Data*-Loc misses SCM-Memory by Lm1;

theorem :: SCMFSA_1:31
canceled;

theorem :: SCMFSA_1:32
dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;

theorem :: SCMFSA_1:33
for s being SCM+FSA-State holds dom s = SCM+FSA-Memory by Lm8, CARD_3:9;