:: 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;