:: SCMFSA_M semantic presentation
begin
set SA0 = Start-At (0,SCM+FSA);
set q = (intloc 0) .--> 1;
set f = the_Values_of SCM+FSA;
registration
let n be Nat;
let i be Integer;
cluster(intloc n) .--> i -> the_Values_of SCM+FSA -compatible ;
coherence
(intloc n) .--> i is the_Values_of SCM+FSA -compatible
proof
set q = (intloc n) .--> i;
A1: dom ((intloc n) .--> i) = {(intloc n)} by FUNCOP_1:13;
i in INT by INT_1:def_2;
then A2: ( rng ((intloc n) .--> i) = {i} & {i} c= INT ) by FUNCOP_1:8, ZFMISC_1:31;
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom ((intloc n) .--> i) or ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x )
assume A3: x in dom ((intloc n) .--> i) ; ::_thesis: ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x
reconsider l = x as Int-Location by A1, A3, TARSKI:def_1;
A4: (the_Values_of SCM+FSA) . l = Values l
.= INT by SCMFSA_2:11 ;
((intloc n) .--> i) . x in rng ((intloc n) .--> i) by A3, FUNCT_1:def_3;
hence ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x by A4, A2; ::_thesis: verum
end;
end;
definition
let I be PartState of SCM+FSA;
func Initialized I -> PartState of SCM+FSA equals :: SCMFSA_M:def 1
I +* (Initialize ((intloc 0) .--> 1));
coherence
I +* (Initialize ((intloc 0) .--> 1)) is PartState of SCM+FSA ;
projectivity
for b1, b2 being PartState of SCM+FSA st b1 = b2 +* (Initialize ((intloc 0) .--> 1)) holds
b1 = b1 +* (Initialize ((intloc 0) .--> 1))
proof
let IT, s be PartState of SCM+FSA; ::_thesis: ( IT = s +* (Initialize ((intloc 0) .--> 1)) implies IT = IT +* (Initialize ((intloc 0) .--> 1)) )
assume Z: IT = s +* (Initialize ((intloc 0) .--> 1)) ; ::_thesis: IT = IT +* (Initialize ((intloc 0) .--> 1))
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A2: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A3: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then A5: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
A6: not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
B1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize (s +* ((intloc 0) .--> 1))) . (intloc 0) by FUNCT_4:14
.= (s +* ((intloc 0) .--> 1)) . (intloc 0) by A6, FUNCT_4:11
.= ((intloc 0) .--> 1) . (intloc 0) by A5, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
(Start-At (0,SCM+FSA)) . (IC ) = 0 by FUNCOP_1:72;
then B2: IC IT = 0 by Z, A2, A3, FUNCT_4:13;
A3: IC in dom IT by Z, MEMSTR_0:49;
X1: dom IT = (dom s) \/ (dom (Initialize ((intloc 0) .--> 1))) by Z, FUNCT_4:def_1;
X2: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
then intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by X2, XBOOLE_0:def_3;
then A4: intloc 0 in dom IT by X1, XBOOLE_0:def_3;
thus IT +* (Initialize ((intloc 0) .--> 1)) = Initialize (IT +* ((intloc 0) .--> 1)) by FUNCT_4:14
.= IT +* ((IC ) .--> 0) by B1, A4, Z, FUNCT_7:109
.= IT by B2, A3, FUNCT_7:109 ; ::_thesis: verum
end;
end;
:: deftheorem defines Initialized SCMFSA_M:def_1_:_
for I being PartState of SCM+FSA holds Initialized I = I +* (Initialize ((intloc 0) .--> 1));
registration
let I be PartState of SCM+FSA;
cluster Initialized I -> 0 -started ;
coherence
Initialized I is 0 -started ;
end;
registration
let I be FinPartState of SCM+FSA;
cluster Initialized I -> finite ;
coherence
Initialized I is finite ;
end;
scheme :: SCMFSA_M:sch 1
SCMFSAEx{ F1( set ) -> Integer, F2( set ) -> FinSequence of INT , F3() -> Element of NAT } :
ex S being State of SCM+FSA st
( IC S = F3() & ( for i being Element of NAT holds
( S . (intloc i) = F1(i) & S . (fsloc i) = F2(i) ) ) )
proof
defpred S1[ set , set ] means ex m being Element of NAT st
( ( $1 = IC & $2 = F3() ) or ( $1 = intloc m & $2 = F1(m) ) or ( $1 = fsloc m & $2 = F2(m) ) );
A1: for e being set st e in the carrier of SCM+FSA holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in the carrier of SCM+FSA implies ex u being set st S1[e,u] )
assume e in the carrier of SCM+FSA ; ::_thesis: ex u being set st S1[e,u]
then e in (Data-Locations ) \/ {(IC )} by STRUCT_0:4;
then A2: ( e in Data-Locations or e in {(IC )} ) by XBOOLE_0:def_3;
now__::_thesis:_(_(_e_in_{(IC_)}_&_e_=_IC_)_or_(_e_in_Int-Locations_&_ex_m_being_Element_of_NAT_st_e_=_intloc_m_)_or_(_e_in_FinSeq-Locations_&_ex_m_being_Element_of_NAT_st_e_=_fsloc_m_)_)
percases ( e in {(IC )} or e in Int-Locations or e in FinSeq-Locations ) by A2, SCMFSA_2:100, XBOOLE_0:def_3;
case e in {(IC )} ; ::_thesis: e = IC
hence e = IC by TARSKI:def_1; ::_thesis: verum
end;
case e in Int-Locations ; ::_thesis: ex m being Element of NAT st e = intloc m
then e is Int-Location by AMI_2:def_16;
hence ex m being Element of NAT st e = intloc m by SCMFSA_2:8; ::_thesis: verum
end;
case e in FinSeq-Locations ; ::_thesis: ex m being Element of NAT st e = fsloc m
then e is FinSeq-Location by SCMFSA_2:def_5;
hence ex m being Element of NAT st e = fsloc m by SCMFSA_2:9; ::_thesis: verum
end;
end;
end;
then consider m being Element of NAT such that
A3: ( e = IC or e = intloc m or e = fsloc m ) ;
percases ( e = IC or e = intloc m or e = fsloc m ) by A3;
supposeA4: e = IC ; ::_thesis: ex u being set st S1[e,u]
take u = F3(); ::_thesis: S1[e,u]
thus S1[e,u] by A4; ::_thesis: verum
end;
supposeA6: e = intloc m ; ::_thesis: ex u being set st S1[e,u]
take u = F1(m); ::_thesis: S1[e,u]
thus S1[e,u] by A6; ::_thesis: verum
end;
supposeA7: e = fsloc m ; ::_thesis: ex u being set st S1[e,u]
take u = F2(m); ::_thesis: S1[e,u]
thus S1[e,u] by A7; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A8: dom f = the carrier of SCM+FSA and
A9: for e being set st e in the carrier of SCM+FSA holds
S1[e,f . e] from CLASSES1:sch_1(A1);
A10: dom the Object-Kind of SCM+FSA = the carrier of SCM+FSA by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_the_Object-Kind_of_SCM+FSA_holds_
f_._x_in_(the_Values_of_SCM+FSA)_._x
let x be set ; ::_thesis: ( x in dom the Object-Kind of SCM+FSA implies f . b1 in (the_Values_of SCM+FSA) . b1 )
assume A11: x in dom the Object-Kind of SCM+FSA ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then consider m being Element of NAT such that
A12: ( ( x = IC & f . x = F3() ) or ( x = intloc m & f . x = F1(m) ) or ( x = fsloc m & f . x = F2(m) ) ) by A9, A10;
x in (Data-Locations ) \/ {(IC )} by A11, A10, STRUCT_0:4;
then A13: ( x in Data-Locations or x in {(IC )} ) by XBOOLE_0:def_3;
percases ( x in Int-Locations or x in FinSeq-Locations or x in {(IC )} ) by A13, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then A14: x is Int-Location by AMI_2:def_16;
then (the_Values_of SCM+FSA) . x = Values (intloc m) by A12, SCMFSA_2:56, SCMFSA_2:58
.= INT by SCMFSA_2:11 ;
hence f . x in (the_Values_of SCM+FSA) . x by A12, A14, INT_1:def_2, SCMFSA_2:58; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then A15: x is FinSeq-Location by SCMFSA_2:def_5;
then (the_Values_of SCM+FSA) . x = Values (fsloc m) by A12, SCMFSA_2:57, SCMFSA_2:58
.= INT * by SCMFSA_2:12 ;
hence f . x in (the_Values_of SCM+FSA) . x by A12, A15, FINSEQ_1:def_11, SCMFSA_2:57, SCMFSA_2:58; ::_thesis: verum
end;
supposeA16: x in {(IC )} ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then A17: (the_Values_of SCM+FSA) . x = Values (IC ) by TARSKI:def_1
.= NAT by MEMSTR_0:def_6 ;
x = IC by A16, TARSKI:def_1;
hence f . x in (the_Values_of SCM+FSA) . x by A12, A17, SCMFSA_2:56, SCMFSA_2:57; ::_thesis: verum
end;
end;
end;
then reconsider f = f as State of SCM+FSA by A8, A10, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
take f ; ::_thesis: ( IC f = F3() & ( for i being Element of NAT holds
( f . (intloc i) = F1(i) & f . (fsloc i) = F2(i) ) ) )
ex m being Element of NAT st
( ( IC = IC & f . (IC ) = F3() ) or ( IC = intloc m & f . (IC ) = F1(m) ) or ( IC = fsloc m & f . (IC ) = F2(m) ) ) by A9;
hence IC f = F3() by SCMFSA_2:56, SCMFSA_2:57; ::_thesis: for i being Element of NAT holds
( f . (intloc i) = F1(i) & f . (fsloc i) = F2(i) )
let i be Element of NAT ; ::_thesis: ( f . (intloc i) = F1(i) & f . (fsloc i) = F2(i) )
ex m being Element of NAT st
( ( intloc i = IC & f . (intloc i) = F3() ) or ( intloc i = intloc m & f . (intloc i) = F1(m) ) or ( intloc i = fsloc m & f . (intloc i) = F2(m) ) ) by A9;
hence f . (intloc i) = F1(i) by AMI_3:10, SCMFSA_2:56, SCMFSA_2:58; ::_thesis: f . (fsloc i) = F2(i)
ex m being Element of NAT st
( ( fsloc i = IC & f . (fsloc i) = F3() ) or ( fsloc i = intloc m & f . (fsloc i) = F1(m) ) or ( fsloc i = fsloc m & f . (fsloc i) = F2(m) ) ) by A9;
hence f . (fsloc i) = F2(i) by SCMFSA_2:57, SCMFSA_2:58; ::_thesis: verum
end;
theorem Th1: :: SCMFSA_M:1
for s being State of SCM+FSA
for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
proof
let s be State of SCM+FSA; ::_thesis: for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
let x be set ; ::_thesis: ( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
assume A1: x in dom s ; ::_thesis: ( x is Int-Location or x is FinSeq-Location or x = IC )
x in (Data-Locations ) \/ {(IC )} by A1, MEMSTR_0:13;
then ( x in Data-Locations or x in {(IC )} ) by XBOOLE_0:def_3;
then ( x in Int-Locations or x in FinSeq-Locations or x = IC ) by SCMFSA_2:100, TARSKI:def_1, XBOOLE_0:def_3;
hence ( x is Int-Location or x is FinSeq-Location or x = IC ) by AMI_2:def_16, SCMFSA_2:def_5; ::_thesis: verum
end;
theorem :: SCMFSA_M:2
for s1, s2 being State of SCM+FSA holds
( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 )
proof
let s1, s2 be State of SCM+FSA; ::_thesis: ( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 )
A2: now__::_thesis:_(_(_for_a_being_Int-Location_holds_s1_._a_=_s2_._a_)_&_(_for_f_being_FinSeq-Location_holds_s1_._f_=_s2_._f_)_implies_for_x_being_set_st_x_in_Data-Locations_holds_
s1_._x_=_s2_._x_)
assume that
A3: for a being Int-Location holds s1 . a = s2 . a and
A4: for f being FinSeq-Location holds s1 . f = s2 . f ; ::_thesis: for x being set st x in Data-Locations holds
s1 . x = s2 . x
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in Data-Locations implies s1 . b1 = s2 . b1 )
assume A5: x in Data-Locations ; ::_thesis: s1 . b1 = s2 . b1
percases ( x in Int-Locations or not x in Int-Locations ) ;
suppose x in Int-Locations ; ::_thesis: s1 . b1 = s2 . b1
then x is Int-Location by AMI_2:def_16;
hence s1 . x = s2 . x by A3; ::_thesis: verum
end;
suppose not x in Int-Locations ; ::_thesis: s1 . b1 = s2 . b1
then x in FinSeq-Locations by A5, SCMFSA_2:100, XBOOLE_0:def_3;
then x is FinSeq-Location by SCMFSA_2:def_5;
hence s1 . x = s2 . x by A4; ::_thesis: verum
end;
end;
end;
end;
A6: now__::_thesis:_(_(_for_x_being_set_st_x_in_Data-Locations_holds_
s1_._x_=_s2_._x_)_implies_(_(_for_a_being_Int-Location_holds_s1_._a_=_s2_._a_)_&_(_for_f_being_FinSeq-Location_holds_s1_._f_=_s2_._f_)_)_)
assume A7: for x being set st x in Data-Locations holds
s1 . x = s2 . x ; ::_thesis: ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) )
hereby ::_thesis: for f being FinSeq-Location holds s1 . f = s2 . f
let a be Int-Location; ::_thesis: s1 . a = s2 . a
a in Int-Locations by AMI_2:def_16;
then a in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
hence s1 . a = s2 . a by A7; ::_thesis: verum
end;
hereby ::_thesis: verum
let f be FinSeq-Location ; ::_thesis: s1 . f = s2 . f
f in FinSeq-Locations by SCMFSA_2:def_5;
then f in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
hence s1 . f = s2 . f by A7; ::_thesis: verum
end;
end;
dom s2 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then A8: Data-Locations c= dom s2 by XBOOLE_1:7;
dom s1 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then Data-Locations c= dom s1 by XBOOLE_1:7;
hence ( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 ) by A8, A2, A6, FUNCT_1:95; ::_thesis: verum
end;
theorem Th43: :: SCMFSA_M:3
for p being PartState of SCM+FSA holds dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}
proof
let p be PartState of SCM+FSA; ::_thesis: dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}
A1: ( dom ((intloc 0) .--> 1) = {(intloc 0)} & dom (Start-At (0,SCM+FSA)) = {(IC )} ) by FUNCOP_1:13;
Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
hence dom (Initialized p) = (dom (p +* ((intloc 0) .--> 1))) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1
.= ((dom p) \/ {(intloc 0)}) \/ {(IC )} by A1, FUNCT_4:def_1 ;
::_thesis: verum
end;
registration
let s be State of SCM+FSA;
cluster Initialized s -> total ;
coherence
Initialized s is total ;
end;
theorem Th4: :: SCMFSA_M:4
for p being PartState of SCM+FSA holds intloc 0 in dom (Initialized p)
proof
let p be PartState of SCM+FSA; ::_thesis: intloc 0 in dom (Initialized p)
A1: ( dom ((intloc 0) .--> 1) = {(intloc 0)} & dom (Start-At (0,SCM+FSA)) = {(IC )} ) by FUNCOP_1:13;
intloc 0 in {(intloc 0)} by TARSKI:def_1;
then A2: intloc 0 in (dom p) \/ {(intloc 0)} by XBOOLE_0:def_3;
Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
then dom (Initialized p) = (dom (p +* ((intloc 0) .--> 1))) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1
.= ((dom p) \/ {(intloc 0)}) \/ {(IC )} by A1, FUNCT_4:def_1 ;
hence intloc 0 in dom (Initialized p) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: SCMFSA_M:5
for p being PartState of SCM+FSA holds
( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )
proof
let p be PartState of SCM+FSA; ::_thesis: ( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )
intloc 0 in {(intloc 0)} by TARSKI:def_1;
then A1: intloc 0 in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
A2: Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
intloc 0 <> IC by SCMFSA_2:56;
then not intloc 0 in {(IC )} by TARSKI:def_1;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
hence (Initialized p) . (intloc 0) = (p +* ((intloc 0) .--> 1)) . (intloc 0) by A2, FUNCT_4:11
.= ((intloc 0) .--> 1) . (intloc 0) by A1, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
::_thesis: (Initialized p) . (IC ) = 0
IC in {(IC )} by TARSKI:def_1;
then IC in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
hence (Initialized p) . (IC ) = (Start-At (0,SCM+FSA)) . (IC ) by A2, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
::_thesis: verum
end;
theorem :: SCMFSA_M:6
for p being PartState of SCM+FSA
for a being Int-Location st a <> intloc 0 & not a in dom p holds
not a in dom (Initialized p)
proof
let p be PartState of SCM+FSA; ::_thesis: for a being Int-Location st a <> intloc 0 & not a in dom p holds
not a in dom (Initialized p)
let a be Int-Location; ::_thesis: ( a <> intloc 0 & not a in dom p implies not a in dom (Initialized p) )
assume that
A1: a <> intloc 0 and
Z: not a in dom p ; ::_thesis: not a in dom (Initialized p)
assume a in dom (Initialized p) ; ::_thesis: contradiction
then a in ((dom p) \/ {(intloc 0)}) \/ {(IC )} by Th43;
then A2: ( a in (dom p) \/ {(intloc 0)} or a in {(IC )} ) by XBOOLE_0:def_3;
percases ( a in {(intloc 0)} or a in {(IC )} ) by A2, Z, XBOOLE_0:def_3;
suppose a in {(intloc 0)} ; ::_thesis: contradiction
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
suppose a in {(IC )} ; ::_thesis: contradiction
then a = IC by TARSKI:def_1;
hence contradiction by SCMFSA_2:56; ::_thesis: verum
end;
end;
end;
theorem :: SCMFSA_M:7
for p being PartState of SCM+FSA
for f being FinSeq-Location st not f in dom p holds
not f in dom (Initialized p)
proof
let p be PartState of SCM+FSA; ::_thesis: for f being FinSeq-Location st not f in dom p holds
not f in dom (Initialized p)
let f be FinSeq-Location ; ::_thesis: ( not f in dom p implies not f in dom (Initialized p) )
assume Z: not f in dom p ; ::_thesis: not f in dom (Initialized p)
assume f in dom (Initialized p) ; ::_thesis: contradiction
then f in ((dom p) \/ {(intloc 0)}) \/ {(IC )} by Th43;
then A1: ( f in (dom p) \/ {(intloc 0)} or f in {(IC )} ) by XBOOLE_0:def_3;
percases ( f in {(intloc 0)} or f in {(IC )} ) by A1, Z, XBOOLE_0:def_3;
suppose f in {(intloc 0)} ; ::_thesis: contradiction
then f = intloc 0 by TARSKI:def_1;
hence contradiction by SCMFSA_2:58; ::_thesis: verum
end;
suppose f in {(IC )} ; ::_thesis: contradiction
then f = IC by TARSKI:def_1;
hence contradiction by SCMFSA_2:57; ::_thesis: verum
end;
end;
end;
theorem :: SCMFSA_M:8
for s being State of SCM+FSA st s . (intloc 0) = 1 & IC s = 0 holds
Initialized s = s
proof
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 & IC s = 0 implies Initialized s = s )
assume A1: s . (intloc 0) = 1 ; ::_thesis: ( not IC s = 0 or Initialized s = s )
assume A2: IC s = 0 ; ::_thesis: Initialized s = s
A3: IC in dom s by MEMSTR_0:2;
A4: intloc 0 in dom s by SCMFSA_2:42;
thus Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14
.= s +* ((IC ) .--> 0) by A1, A4, FUNCT_7:109
.= s by A2, A3, FUNCT_7:109 ; ::_thesis: verum
end;
theorem :: SCMFSA_M:9
for p being PartState of SCM+FSA holds (Initialized p) . (intloc 0) = 1
proof
let p be PartState of SCM+FSA; ::_thesis: (Initialized p) . (intloc 0) = 1
A1: ((intloc 0) .--> 1) . (intloc 0) = 1 by FUNCOP_1:72;
A3: Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then A5: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialized p) . (intloc 0) = (p +* ((intloc 0) .--> 1)) . (intloc 0) by A3, FUNCT_4:11
.= 1 by A5, A1, FUNCT_4:13 ;
::_thesis: verum
end;
theorem Th10: :: SCMFSA_M:10
intloc 0 in dom (Initialize ((intloc 0) .--> 1))
proof
A: dom (Initialize ((intloc 0) .--> 1)) = (dom (Start-At (0,SCM+FSA))) \/ (dom ((intloc 0) .--> 1)) by FUNCT_4:def_1;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
hence intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by A, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th11: :: SCMFSA_M:11
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
proof
thus dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1
.= (dom ((intloc 0) .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {(intloc 0)} \/ {(IC )} by FUNCOP_1:13
.= {(intloc 0),(IC )} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem Th12: :: SCMFSA_M:12
(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1
proof
not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
::_thesis: verum
end;
theorem :: SCMFSA_M:13
for p being PartState of SCM+FSA holds Initialize ((intloc 0) .--> 1) c= Initialized p by FUNCT_4:25;
begin
registration
cluster Int-Locations -> non empty ;
coherence
not Int-Locations is empty ;
end;
definition
let IT be Int-Location;
attrIT is read-only means :Def2: :: SCMFSA_M:def 2
IT = intloc 0;
end;
:: deftheorem Def2 defines read-only SCMFSA_M:def_2_:_
for IT being Int-Location holds
( IT is read-only iff IT = intloc 0 );
notation
let IT be Int-Location;
antonym read-write IT for read-only ;
end;
registration
cluster intloc 0 -> read-only ;
coherence
intloc 0 is read-only by Def2;
end;
registration
cluster Int-like read-write for Element of the carrier of SCM+FSA;
existence
ex b1 being Int-Location st b1 is read-write
proof
take intloc 1 ; ::_thesis: intloc 1 is read-write
intloc 1 <> intloc 0 by AMI_3:10;
hence intloc 1 is read-write by Def2; ::_thesis: verum
end;
end;
definition
let L be finite Subset of Int-Locations;
func FirstNotIn L -> Int-Location means :Def6: :: SCMFSA_M:def 3
ex sn being non empty Subset of NAT st
( it = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } );
existence
ex b1 being Int-Location ex sn being non empty Subset of NAT st
( b1 = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )
proof
defpred S1[ Element of NAT ] means not intloc $1 in L;
set sn = { k where k is Element of NAT : S1[k] } ;
A1: { k where k is Element of NAT : S1[k] } is Subset of NAT from DOMAIN_1:sch_7();
Int-Locations = [:{1},NAT:] by SCM_INST:def_1;
then not Int-Locations c= L ;
then consider x being set such that
A2: x in Int-Locations and
A3: not x in L by TARSKI:def_3;
reconsider x = x as Int-Location by A2, AMI_2:def_16;
consider k being Element of NAT such that
A4: x = intloc k by SCMFSA_2:8;
k in { k where k is Element of NAT : S1[k] } by A3, A4;
then reconsider sn = { k where k is Element of NAT : S1[k] } as non empty Subset of NAT by A1;
take intloc (min sn) ; ::_thesis: ex sn being non empty Subset of NAT st
( intloc (min sn) = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )
take sn ; ::_thesis: ( intloc (min sn) = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )
thus ( intloc (min sn) = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Int-Location st ex sn being non empty Subset of NAT st
( b1 = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) & ex sn being non empty Subset of NAT st
( b2 = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) holds
b1 = b2 ;
end;
:: deftheorem Def6 defines FirstNotIn SCMFSA_M:def_3_:_
for L being finite Subset of Int-Locations
for b2 being Int-Location holds
( b2 = FirstNotIn L iff ex sn being non empty Subset of NAT st
( b2 = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) );
theorem :: SCMFSA_M:14
for L being finite Subset of Int-Locations holds not FirstNotIn L in L
proof
let L be finite Subset of Int-Locations; ::_thesis: not FirstNotIn L in L
set FNI = FirstNotIn L;
consider sn being non empty Subset of NAT such that
A1: FirstNotIn L = intloc (min sn) and
A2: sn = { k where k is Element of NAT : not intloc k in L } by Def6;
min sn in sn by XXREAL_2:def_7;
then ex k being Element of NAT st
( k = min sn & not intloc k in L ) by A2;
hence not FirstNotIn L in L by A1; ::_thesis: verum
end;
theorem :: SCMFSA_M:15
for m, n being Element of NAT
for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n
proof
let m, n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n
let L be finite Subset of Int-Locations; ::_thesis: ( FirstNotIn L = intloc m & not intloc n in L implies m <= n )
consider sn being non empty Subset of NAT such that
A1: ( FirstNotIn L = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) by Def6;
assume ( FirstNotIn L = intloc m & not intloc n in L ) ; ::_thesis: m <= n
then ( m = min sn & n in sn ) by A1, AMI_3:10;
hence m <= n by XXREAL_2:def_7; ::_thesis: verum
end;
definition
let L be finite Subset of FinSeq-Locations;
func First*NotIn L -> FinSeq-Location means :Def8: :: SCMFSA_M:def 4
ex sn being non empty Subset of NAT st
( it = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } );
existence
ex b1 being FinSeq-Location ex sn being non empty Subset of NAT st
( b1 = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )
proof
defpred S1[ Element of NAT ] means not fsloc $1 in L;
set sn = { k where k is Element of NAT : S1[k] } ;
A1: { k where k is Element of NAT : S1[k] } is Subset of NAT from DOMAIN_1:sch_7();
not FinSeq-Locations c= L ;
then consider x being set such that
A2: x in FinSeq-Locations and
A3: not x in L by TARSKI:def_3;
reconsider x = x as FinSeq-Location by A2, SCMFSA_2:def_5;
consider k being Element of NAT such that
A4: x = fsloc k by SCMFSA_2:9;
k in { k where k is Element of NAT : S1[k] } by A3, A4;
then reconsider sn = { k where k is Element of NAT : S1[k] } as non empty Subset of NAT by A1;
take fsloc (min sn) ; ::_thesis: ex sn being non empty Subset of NAT st
( fsloc (min sn) = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )
take sn ; ::_thesis: ( fsloc (min sn) = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )
thus ( fsloc (min sn) = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSeq-Location st ex sn being non empty Subset of NAT st
( b1 = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) & ex sn being non empty Subset of NAT st
( b2 = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) holds
b1 = b2 ;
end;
:: deftheorem Def8 defines First*NotIn SCMFSA_M:def_4_:_
for L being finite Subset of FinSeq-Locations
for b2 being FinSeq-Location holds
( b2 = First*NotIn L iff ex sn being non empty Subset of NAT st
( b2 = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) );
theorem :: SCMFSA_M:16
for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L
proof
let L be finite Subset of FinSeq-Locations; ::_thesis: not First*NotIn L in L
set FNI = First*NotIn L;
consider sn being non empty Subset of NAT such that
A1: First*NotIn L = fsloc (min sn) and
A2: sn = { k where k is Element of NAT : not fsloc k in L } by Def8;
min sn in sn by XXREAL_2:def_7;
then ex k being Element of NAT st
( k = min sn & not fsloc k in L ) by A2;
hence not First*NotIn L in L by A1; ::_thesis: verum
end;
theorem :: SCMFSA_M:17
for m, n being Element of NAT
for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n
proof
let m, n be Element of NAT ; ::_thesis: for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n
let L be finite Subset of FinSeq-Locations; ::_thesis: ( First*NotIn L = fsloc m & not fsloc n in L implies m <= n )
assume that
A1: First*NotIn L = fsloc m and
A2: not fsloc n in L ; ::_thesis: m <= n
consider sn being non empty Subset of NAT such that
A3: First*NotIn L = fsloc (min sn) and
A4: sn = { k where k is Element of NAT : not fsloc k in L } by Def8;
n in sn by A2, A4;
hence m <= n by A1, A3, XXREAL_2:def_7; ::_thesis: verum
end;
registration
let s be State of SCM+FSA;
let li be Int-Location;
let k be Integer;
clusters +* (li,k) -> the_Values_of SCM+FSA -compatible ;
coherence
s +* (li,k) is the_Values_of SCM+FSA -compatible
proof
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom (s +* (li,k)) or (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x )
assume x in dom (s +* (li,k)) ; ::_thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then A2: x in dom s by FUNCT_7:30;
percases ( x = li or x <> li ) ;
supposeA3: x = li ; ::_thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then A4: (the_Values_of SCM+FSA) . x = Values li
.= INT by SCMFSA_2:11 ;
(s +* (li,k)) . x = k by A3, A2, FUNCT_7:31;
hence (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x by A4, INT_1:def_2; ::_thesis: verum
end;
suppose x <> li ; ::_thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then (s +* (li,k)) . x = s . x by FUNCT_7:32;
hence (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x by A2, FUNCT_1:def_14; ::_thesis: verum
end;
end;
end;
end;
begin
registration
let a be Int-Location;
let n be Nat;
clustera .--> n -> data-only for PartState of SCM+FSA;
coherence
for b1 being PartState of SCM+FSA st b1 = a .--> n holds
b1 is data-only ;
end;
theorem :: SCMFSA_M:18
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
Initialize s = Initialized s
proof
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies Initialize s = Initialized s )
A1: intloc 0 in dom s by SCMFSA_2:42;
assume s . (intloc 0) = 1 ; ::_thesis: Initialize s = Initialized s
then A2: s = s +* ((intloc 0) .--> 1) by A1, FUNCT_7:109;
thus Initialized s = Initialize s by A2, FUNCT_4:14; ::_thesis: verum
end;
theorem :: SCMFSA_M:19
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (Initialized s) = DataPart s
proof
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies DataPart (Initialized s) = DataPart s )
assume A1: s . (intloc 0) = 1 ; ::_thesis: DataPart (Initialized s) = DataPart s
A2: intloc 0 in dom s by SCMFSA_2:42;
Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
then Initialized s = Initialize s by A1, A2, FUNCT_7:109;
hence DataPart (Initialized s) = DataPart s by MEMSTR_0:79; ::_thesis: verum
end;
theorem :: SCMFSA_M:20
for s1, s2 being State of SCM+FSA st s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart s1 = DataPart s2
proof
let s1, s2 be State of SCM+FSA; ::_thesis: ( s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies DataPart s1 = DataPart s2 )
set D = Data-Locations ;
assume A1: s1 . (intloc 0) = s2 . (intloc 0) ; ::_thesis: ( ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
assume A2: for a being read-write Int-Location holds s1 . a = s2 . a ; ::_thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
A3: dom (DataPart s1) = (dom s1) /\ (Data-Locations ) by RELAT_1:61
.= ((Data-Locations ) \/ {(IC )}) /\ (Data-Locations ) by MEMSTR_0:13
.= (dom s2) /\ (Data-Locations ) by MEMSTR_0:13
.= dom (DataPart s2) by RELAT_1:61 ;
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; ::_thesis: DataPart s1 = DataPart s2
now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_s1)_holds_
(DataPart_s1)_._x_=_(DataPart_s2)_._x
let x be set ; ::_thesis: ( x in dom (DataPart s1) implies (DataPart s1) . b1 = (DataPart s2) . b1 )
assume A5: x in dom (DataPart s1) ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
then A6: x in (dom s1) /\ (Data-Locations ) by RELAT_1:61;
then A7: x in dom s1 by XBOOLE_0:def_4;
percases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A7, Th1;
supposeA9: x is Int-Location ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
hereby ::_thesis: verum
percases ( x is read-write Int-Location or not x is read-write Int-Location ) ;
supposeA10: x is read-write Int-Location ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A2, A10
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; ::_thesis: verum
end;
supposeA11: x is not read-write Int-Location ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
reconsider a = x as Int-Location by A9;
a = intloc 0 by A11, Def2;
hence (DataPart s1) . x = s2 . a by A1, A5, FUNCT_1:47
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ;
::_thesis: verum
end;
end;
end;
end;
supposeA12: x is FinSeq-Location ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A4, A12
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; ::_thesis: verum
end;
suppose x = IC ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
then not x in Data-Locations by STRUCT_0:3;
hence (DataPart s1) . x = (DataPart s2) . x by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then DataPart s1 c= DataPart s2 by A3, GRFUNC_1:2;
hence DataPart s1 = DataPart s2 by A3, GRFUNC_1:3; ::_thesis: verum
end;
theorem :: SCMFSA_M:21
for s being State of SCM+FSA
for a being Int-Location
for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
proof
let s be State of SCM+FSA; ::_thesis: for a being Int-Location
for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let a be Int-Location; ::_thesis: for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let l be Element of NAT ; ::_thesis: (s +* (Start-At (l,SCM+FSA))) . a = s . a
not a in dom (Start-At (l,SCM+FSA)) by SCMFSA_2:102;
hence (s +* (Start-At (l,SCM+FSA))) . a = s . a by FUNCT_4:11; ::_thesis: verum
end;
begin
definition
let d be Int-Location;
:: original: {
redefine func{d} -> Subset of Int-Locations;
coherence
{d} is Subset of Int-Locations
proof
d in SCM-Data-Loc by AMI_2:def_16;
hence {d} is Subset of Int-Locations by SUBSET_1:33; ::_thesis: verum
end;
let e be Int-Location;
:: original: {
redefine func{d,e} -> Subset of Int-Locations;
coherence
{d,e} is Subset of Int-Locations
proof
A1: e in SCM-Data-Loc by AMI_2:def_16;
d in SCM-Data-Loc by AMI_2:def_16;
hence {d,e} is Subset of Int-Locations by A1, SUBSET_1:34; ::_thesis: verum
end;
let f be Int-Location;
:: original: {
redefine func{d,e,f} -> Subset of Int-Locations;
coherence
{d,e,f} is Subset of Int-Locations
proof
A2: f in SCM-Data-Loc by AMI_2:def_16;
A3: e in SCM-Data-Loc by AMI_2:def_16;
d in SCM-Data-Loc by AMI_2:def_16;
hence {d,e,f} is Subset of Int-Locations by A3, A2, SUBSET_1:35; ::_thesis: verum
end;
let g be Int-Location;
:: original: {
redefine func{d,e,f,g} -> Subset of Int-Locations;
coherence
{d,e,f,g} is Subset of Int-Locations
proof
A4: g in SCM-Data-Loc by AMI_2:def_16;
A5: f in SCM-Data-Loc by AMI_2:def_16;
A6: e in SCM-Data-Loc by AMI_2:def_16;
d in SCM-Data-Loc by AMI_2:def_16;
hence {d,e,f,g} is Subset of Int-Locations by A6, A5, A4, SUBSET_1:36; ::_thesis: verum
end;
end;
definition
let L be finite Subset of Int-Locations;
func RWNotIn-seq L -> Function of NAT,(bool NAT) means :Def2: :: SCMFSA_M:def 5
( it . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st it . i = sn holds
it . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds it . i is infinite ) );
existence
ex b1 being Function of NAT,(bool NAT) st
( b1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b1 . i = sn holds
b1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b1 . i is infinite ) )
proof
set M = L \/ {(intloc 0)};
defpred S1[ Element of NAT ] means ( not intloc $1 in L & $1 <> 0 );
set sn = { k where k is Element of NAT : S1[k] } ;
A1: { k where k is Element of NAT : S1[k] } is Subset of NAT from DOMAIN_1:sch_7();
not Int-Locations c= L \/ {(intloc 0)} by AMI_3:27;
then consider x being set such that
A2: x in Int-Locations and
A3: not x in L \/ {(intloc 0)} by TARSKI:def_3;
reconsider x = x as Int-Location by A2, AMI_2:def_16;
consider k being Element of NAT such that
A4: x = intloc k by SCMFSA_2:8;
not intloc k in {(intloc 0)} by A3, A4, XBOOLE_0:def_3;
then A5: k <> 0 by TARSKI:def_1;
not intloc k in L by A3, A4, XBOOLE_0:def_3;
then k in { k where k is Element of NAT : S1[k] } by A5;
then reconsider sn = { k where k is Element of NAT : S1[k] } as non empty Subset of NAT by A1;
defpred S2[ Element of NAT , Subset of NAT, Subset of NAT] means for N being non empty Subset of NAT st N = $2 holds
$3 = $2 \ {(min N)};
A6: now__::_thesis:_for_n_being_Element_of_NAT_
for_x_being_Subset_of_NAT_ex_y_being_Subset_of_NAT_st_S2[n,x,y]
let n be Element of NAT ; ::_thesis: for x being Subset of NAT ex y being Subset of NAT st S2[y,b3,b4]
let x be Subset of NAT; ::_thesis: ex y being Subset of NAT st S2[y,b2,b3]
percases ( x is empty or not x is empty ) ;
suppose x is empty ; ::_thesis: ex y being Subset of NAT st S2[y,b2,b3]
then S2[n,x, {} NAT] ;
hence ex y being Subset of NAT st S2[n,x,y] ; ::_thesis: verum
end;
suppose not x is empty ; ::_thesis: ex y being Subset of NAT st S2[y,b2,b3]
then reconsider x9 = x as non empty Subset of NAT ;
now__::_thesis:_ex_t_being_Subset_of_NAT_st_
for_N_being_non_empty_Subset_of_NAT_st_N_=_x_holds_
t_=_x_\_{(min_N)}
reconsider mx9 = {(min x9)} as Subset of NAT ;
reconsider t = x9 \ mx9 as Subset of NAT ;
take t = t; ::_thesis: for N being non empty Subset of NAT st N = x holds
t = x \ {(min N)}
let N be non empty Subset of NAT; ::_thesis: ( N = x implies t = x \ {(min N)} )
assume N = x ; ::_thesis: t = x \ {(min N)}
hence t = x \ {(min N)} ; ::_thesis: verum
end;
hence ex y being Subset of NAT st S2[n,x,y] ; ::_thesis: verum
end;
end;
end;
consider f being Function of NAT,(bool NAT) such that
A7: f . 0 = sn and
A8: for n being Element of NAT holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A6);
take f ; ::_thesis: ( f . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds f . i is infinite ) )
thus f . 0 = { v where v is Element of NAT : ( not intloc v in L & v <> 0 ) } by A7; ::_thesis: ( ( for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds f . i is infinite ) )
thus for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} by A8; ::_thesis: for i being Element of NAT holds f . i is infinite
defpred S3[ Element of NAT ] means f . $1 is infinite ;
A9: S3[ 0 ]
proof
deffunc H1( Element of NAT ) -> Element of the carrier of SCM+FSA = intloc $1;
set Isn = { H1(v) where v is Element of NAT : v in sn } ;
assume f . 0 is finite ; ::_thesis: contradiction
then A10: sn is finite by A7;
{ H1(v) where v is Element of NAT : v in sn } is finite from FRAENKEL:sch_21(A10);
then reconsider Isn = { H1(v) where v is Element of NAT : v in sn } as finite set ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(L_\/_{(intloc_0)})_\/_Isn_implies_x_in_Int-Locations_)_&_(_x_in_Int-Locations_implies_x_in_(L_\/_{(intloc_0)})_\/_Isn_)_)
let x be set ; ::_thesis: ( ( x in (L \/ {(intloc 0)}) \/ Isn implies x in Int-Locations ) & ( x in Int-Locations implies x in (L \/ {(intloc 0)}) \/ Isn ) )
hereby ::_thesis: ( x in Int-Locations implies x in (L \/ {(intloc 0)}) \/ Isn )
assume A11: x in (L \/ {(intloc 0)}) \/ Isn ; ::_thesis: x in Int-Locations
percases ( x in L \/ {(intloc 0)} or x in Isn ) by A11, XBOOLE_0:def_3;
suppose x in L \/ {(intloc 0)} ; ::_thesis: x in Int-Locations
hence x in Int-Locations ; ::_thesis: verum
end;
suppose x in Isn ; ::_thesis: x in Int-Locations
then ex k being Element of NAT st
( intloc k = x & k in sn ) ;
hence x in Int-Locations by AMI_2:def_16; ::_thesis: verum
end;
end;
end;
assume x in Int-Locations ; ::_thesis: x in (L \/ {(intloc 0)}) \/ Isn
then reconsider x9 = x as Int-Location by AMI_2:def_16;
consider i being Element of NAT such that
A12: x9 = intloc i by SCMFSA_2:8;
now__::_thesis:_(_not_x_in_L_\/_{(intloc_0)}_implies_x_in_Isn_)
assume A13: not x in L \/ {(intloc 0)} ; ::_thesis: x in Isn
then not x9 in {(intloc 0)} by XBOOLE_0:def_3;
then A14: i <> 0 by A12, TARSKI:def_1;
not intloc i in L by A12, A13, XBOOLE_0:def_3;
then i in sn by A14;
hence x in Isn by A12; ::_thesis: verum
end;
hence x in (L \/ {(intloc 0)}) \/ Isn by XBOOLE_0:def_3; ::_thesis: verum
end;
hence contradiction by AMI_3:27, TARSKI:1; ::_thesis: verum
end;
A15: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A16: f . n is infinite ; ::_thesis: S3[n + 1]
then reconsider sn = f . n as non empty Subset of NAT ;
min sn in sn by XXREAL_2:def_7;
then A17: {(min sn)} c= sn by ZFMISC_1:31;
assume f . (n + 1) is finite ; ::_thesis: contradiction
then reconsider sn1 = f . (n + 1) as finite set ;
A18: sn1 \/ {(min sn)} is finite ;
f . (n + 1) = sn \ {(min sn)} by A8;
hence contradiction by A16, A17, A18, XBOOLE_1:45; ::_thesis: verum
end;
thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A9, A15); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of NAT,(bool NAT) st b1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b1 . i = sn holds
b1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b1 . i is infinite ) & b2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b2 . i is infinite ) holds
b1 = b2
proof
let IT1, IT2 be Function of NAT,(bool NAT); ::_thesis: ( IT1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st IT1 . i = sn holds
IT1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds IT1 . i is infinite ) & IT2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st IT2 . i = sn holds
IT2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds IT2 . i is infinite ) implies IT1 = IT2 )
assume that
A19: IT1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } and
A20: for i being Element of NAT
for sn being non empty Subset of NAT st IT1 . i = sn holds
IT1 . (i + 1) = sn \ {(min sn)} and
for i being Element of NAT holds IT1 . i is infinite and
A21: IT2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } and
A22: for i being Element of NAT
for sn being non empty Subset of NAT st IT2 . i = sn holds
IT2 . (i + 1) = sn \ {(min sn)} and
A23: for i being Element of NAT holds IT2 . i is infinite ; ::_thesis: IT1 = IT2
now__::_thesis:_(_NAT_=_dom_IT1_&_NAT_=_dom_IT2_&_(_for_x_being_set_st_x_in_NAT_holds_
IT1_._x_=_IT2_._x_)_)
defpred S1[ Element of NAT ] means IT1 . $1 = IT2 . $1;
thus NAT = dom IT1 by FUNCT_2:def_1; ::_thesis: ( NAT = dom IT2 & ( for x being set st x in NAT holds
IT1 . x = IT2 . x ) )
thus NAT = dom IT2 by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds
IT1 . x = IT2 . x
A24: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A25: IT1 . n = IT2 . n ; ::_thesis: S1[n + 1]
then reconsider IT1n = IT1 . n as non empty Subset of NAT by A23;
thus IT1 . (n + 1) = IT1n \ {(min IT1n)} by A20
.= IT2 . (n + 1) by A22, A25 ; ::_thesis: verum
end;
A26: S1[ 0 ] by A19, A21;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A26, A24);
hence for x being set st x in NAT holds
IT1 . x = IT2 . x ; ::_thesis: verum
end;
hence IT1 = IT2 by FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines RWNotIn-seq SCMFSA_M:def_5_:_
for L being finite Subset of Int-Locations
for b2 being Function of NAT,(bool NAT) holds
( b2 = RWNotIn-seq L iff ( b2 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b2 . i is infinite ) ) );
registration
let L be finite Subset of Int-Locations;
let n be Element of NAT ;
cluster(RWNotIn-seq L) . n -> non empty ;
coherence
not (RWNotIn-seq L) . n is empty by Def2;
end;
theorem Th18: :: SCMFSA_M:22
for n being Element of NAT
for L being finite Subset of Int-Locations holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
proof
let n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
let L be finite Subset of Int-Locations; ::_thesis: ( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
set RL = RWNotIn-seq L;
defpred S1[ Element of NAT ] means ( not 0 in (RWNotIn-seq L) . $1 & ( for m being Element of NAT st m in (RWNotIn-seq L) . $1 holds
not intloc m in L ) );
A1: S1[ 0 ]
proof
A2: (RWNotIn-seq L) . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } by Def2;
hereby ::_thesis: for m being Element of NAT st m in (RWNotIn-seq L) . 0 holds
not intloc m in L
assume 0 in (RWNotIn-seq L) . 0 ; ::_thesis: contradiction
then ex k being Element of NAT st
( k = 0 & not intloc k in L & k <> 0 ) by A2;
hence contradiction ; ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: ( m in (RWNotIn-seq L) . 0 implies not intloc m in L )
assume m in (RWNotIn-seq L) . 0 ; ::_thesis: not intloc m in L
then ex k being Element of NAT st
( k = m & not intloc k in L & k <> 0 ) by A2;
hence not intloc m in L ; ::_thesis: verum
end;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A4: not 0 in (RWNotIn-seq L) . n and
A5: for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ; ::_thesis: S1[n + 1]
reconsider sn = (RWNotIn-seq L) . n as non empty Subset of NAT ;
A6: (RWNotIn-seq L) . (n + 1) = sn \ {(min sn)} by Def2;
hence not 0 in (RWNotIn-seq L) . (n + 1) by A4, XBOOLE_0:def_5; ::_thesis: for m being Element of NAT st m in (RWNotIn-seq L) . (n + 1) holds
not intloc m in L
let m be Element of NAT ; ::_thesis: ( m in (RWNotIn-seq L) . (n + 1) implies not intloc m in L )
assume m in (RWNotIn-seq L) . (n + 1) ; ::_thesis: not intloc m in L
then m in (RWNotIn-seq L) . n by A6, XBOOLE_0:def_5;
hence not intloc m in L by A5; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A3);
hence ( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) ) ; ::_thesis: verum
end;
theorem Th19: :: SCMFSA_M:23
for n being Element of NAT
for L being finite Subset of Int-Locations holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
proof
let n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
let L be finite Subset of Int-Locations; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
set RL = RWNotIn-seq L;
set sn = (RWNotIn-seq L) . n;
set sn1 = (RWNotIn-seq L) . (n + 1);
assume A1: min ((RWNotIn-seq L) . n) >= min ((RWNotIn-seq L) . (n + 1)) ; ::_thesis: contradiction
A2: (RWNotIn-seq L) . (n + 1) = ((RWNotIn-seq L) . n) \ {(min ((RWNotIn-seq L) . n))} by Def2;
then min ((RWNotIn-seq L) . n) <= min ((RWNotIn-seq L) . (n + 1)) by XBOOLE_1:36, XXREAL_2:60;
then min ((RWNotIn-seq L) . n) = min ((RWNotIn-seq L) . (n + 1)) by A1, XXREAL_0:1;
then A3: min ((RWNotIn-seq L) . (n + 1)) in {(min ((RWNotIn-seq L) . n))} by TARSKI:def_1;
min ((RWNotIn-seq L) . (n + 1)) in (RWNotIn-seq L) . (n + 1) by XXREAL_2:def_7;
hence contradiction by A2, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th20: :: SCMFSA_M:24
for n, m being Element of NAT
for L being finite Subset of Int-Locations st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)
proof
let n, m be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)
let L be finite Subset of Int-Locations; ::_thesis: ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) )
set RL = RWNotIn-seq L;
now__::_thesis:_for_n,_n_being_Element_of_NAT_holds_S1[n]
let n be Element of NAT ; ::_thesis: for n being Element of NAT holds S1[n]
defpred S1[ Element of NAT ] means ( n < $1 implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . $1) );
A1: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) ) ; ::_thesis: S1[m + 1]
assume n < m + 1 ; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
then A3: n <= m by NAT_1:13;
percases ( n = m or n < m ) by A3, XXREAL_0:1;
suppose n = m ; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
hence min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1)) by Th19; ::_thesis: verum
end;
suppose n < m ; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
hence min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1)) by A2, Th19, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A4: S1[ 0 ] by NAT_1:2;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); ::_thesis: verum
end;
hence ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) ) ; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
funcn -thRWNotIn L -> Int-Location equals :: SCMFSA_M:def 6
intloc (min ((RWNotIn-seq L) . n));
correctness
coherence
intloc (min ((RWNotIn-seq L) . n)) is Int-Location;
;
end;
:: deftheorem defines -thRWNotIn SCMFSA_M:def_6_:_
for n being Element of NAT
for L being finite Subset of Int-Locations holds n -thRWNotIn L = intloc (min ((RWNotIn-seq L) . n));
notation
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
synonym n -stRWNotIn L for n -thRWNotIn L;
synonym n -ndRWNotIn L for n -thRWNotIn L;
synonym n -rdRWNotIn L for n -thRWNotIn L;
end;
registration
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
clustern -thRWNotIn L -> read-write ;
coherence
not n -thRWNotIn L is read-only
proof
set sn = (RWNotIn-seq L) . n;
A1: min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def_7;
assume n -thRWNotIn L = intloc 0 ; :: according to SCMFSA_M:def_2 ::_thesis: contradiction
then min ((RWNotIn-seq L) . n) = 0 by AMI_3:10;
hence contradiction by A1, Th18; ::_thesis: verum
end;
end;
theorem :: SCMFSA_M:25
for n being Element of NAT
for L being finite Subset of Int-Locations holds not n -thRWNotIn L in L
proof
let n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations holds not n -thRWNotIn L in L
let L be finite Subset of Int-Locations; ::_thesis: not n -thRWNotIn L in L
set FNI = n -thRWNotIn L;
set sn = (RWNotIn-seq L) . n;
min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def_7;
hence not n -thRWNotIn L in L by Th18; ::_thesis: verum
end;
theorem :: SCMFSA_M:26
for n, m being Element of NAT
for L being finite Subset of Int-Locations st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L
proof
let n, m be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L
let L be finite Subset of Int-Locations; ::_thesis: ( n <> m implies n -thRWNotIn L <> m -thRWNotIn L )
assume n <> m ; ::_thesis: n -thRWNotIn L <> m -thRWNotIn L
then ( n < m or m < n ) by XXREAL_0:1;
then A1: min ((RWNotIn-seq L) . n) <> min ((RWNotIn-seq L) . m) by Th20;
assume n -thRWNotIn L = m -thRWNotIn L ; ::_thesis: contradiction
hence contradiction by A1, AMI_3:10; ::_thesis: verum
end;
begin
theorem Th6: :: SCMFSA_M:27
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
proof
let s1, s2 be State of SCM+FSA; ::_thesis: for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
let Iloc be Subset of Int-Locations; ::_thesis: for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
let Floc be Subset of FinSeq-Locations; ::_thesis: ( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
FinSeq-Locations c= dom s1 by SCMFSA_2:46;
then A1: Floc c= dom s1 by XBOOLE_1:1;
FinSeq-Locations c= dom s2 by SCMFSA_2:46;
then A2: Floc c= dom s2 by XBOOLE_1:1;
Int-Locations c= dom s2 by SCMFSA_2:45;
then A3: Iloc c= dom s2 by XBOOLE_1:1;
then A4: Iloc \/ Floc c= dom s2 by A2, XBOOLE_1:8;
Int-Locations c= dom s1 by SCMFSA_2:45;
then A5: Iloc c= dom s1 by XBOOLE_1:1;
then A6: Iloc \/ Floc c= dom s1 by A1, XBOOLE_1:8;
hereby ::_thesis: ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) implies s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) )
assume A7: s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) ; ::_thesis: ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) )
hereby ::_thesis: for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x
let x be Int-Location; ::_thesis: ( x in Iloc implies s1 . x = s2 . x )
assume x in Iloc ; ::_thesis: s1 . x = s2 . x
then x in Iloc \/ Floc by XBOOLE_0:def_3;
hence s1 . x = s2 . x by A6, A4, A7, FUNCT_1:95; ::_thesis: verum
end;
let x be FinSeq-Location ; ::_thesis: ( x in Floc implies s1 . x = s2 . x )
assume x in Floc ; ::_thesis: s1 . x = s2 . x
then x in Iloc \/ Floc by XBOOLE_0:def_3;
hence s1 . x = s2 . x by A6, A4, A7, FUNCT_1:95; ::_thesis: verum
end;
assume that
A8: for x being Int-Location st x in Iloc holds
s1 . x = s2 . x and
A9: for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ; ::_thesis: s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc)
A10: now__::_thesis:_(_(_for_x_being_set_st_x_in_Iloc_holds_
s1_._x_=_s2_._x_)_&_(_for_x_being_set_st_x_in_Floc_holds_
s1_._x_=_s2_._x_)_)
hereby ::_thesis: for x being set st x in Floc holds
s1 . x = s2 . x
let x be set ; ::_thesis: ( x in Iloc implies s1 . x = s2 . x )
assume A11: x in Iloc ; ::_thesis: s1 . x = s2 . x
then x in Int-Locations ;
then reconsider x9 = x as Int-Location by AMI_2:def_16;
thus s1 . x = s2 . x9 by A8, A11
.= s2 . x ; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in Floc implies s1 . x = s2 . x )
assume A12: x in Floc ; ::_thesis: s1 . x = s2 . x
then x in FinSeq-Locations ;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5;
thus s1 . x = s2 . x9 by A9, A12
.= s2 . x ; ::_thesis: verum
end;
then A13: s1 | Floc = s2 | Floc by A1, A2, FUNCT_1:95;
s1 | Iloc = s2 | Iloc by A5, A3, A10, FUNCT_1:95;
hence s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) by A13, RELAT_1:150; ::_thesis: verum
end;
theorem :: SCMFSA_M:28
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
proof
let s1, s2 be State of SCM+FSA; ::_thesis: for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
set FSL = FinSeq-Locations ;
let Iloc be Subset of Int-Locations; ::_thesis: ( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
A1: ( ( for x being FinSeq-Location holds s1 . x = s2 . x ) implies for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ) ;
A2: ( ( for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ) implies for x being FinSeq-Location holds s1 . x = s2 . x )
proof
assume A3: for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ; ::_thesis: for x being FinSeq-Location holds s1 . x = s2 . x
let x be FinSeq-Location ; ::_thesis: s1 . x = s2 . x
x in FinSeq-Locations by SCMFSA_2:def_5;
hence s1 . x = s2 . x by A3; ::_thesis: verum
end;
[#] FinSeq-Locations = FinSeq-Locations ;
hence ( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) ) by A1, A2, Th6; ::_thesis: verum
end;
begin
theorem :: SCMFSA_M:29
for x being set
for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
proof
let x be set ; ::_thesis: for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
let i, m, n be Element of NAT ; ::_thesis: ( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
set iS = ((intloc i) .--> m) +* (Start-At (n,SCM+FSA));
( dom ((intloc i) .--> m) = {(intloc i)} & dom (Start-At (n,SCM+FSA)) = {(IC )} ) by FUNCOP_1:13;
then A1: dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) = {(intloc i)} \/ {(IC )} by FUNCT_4:def_1;
assume x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) ; ::_thesis: ( x = intloc i or x = IC )
then ( x in {(intloc i)} or x in {(IC )} ) by A1, XBOOLE_0:def_3;
hence ( x = intloc i or x = IC ) by TARSKI:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_M:30
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
s . (intloc 0) = 1
proof
let s be State of SCM+FSA; ::_thesis: ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 )
set iS = Initialize ((intloc 0) .--> 1);
Y: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
intloc 0 in dom ((intloc 0) .--> 1) by FUNCOP_1:74;
then A1: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by Y, XBOOLE_0:def_3;
C: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
IC <> intloc 0 by SCMFSA_2:56;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by C, TARSKI:def_1;
then (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
hence ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 ) by A1, GRFUNC_1:2; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster intloc (n + 1) -> read-write ;
coherence
not intloc (n + 1) is read-only
proof
thus intloc (n + 1) <> intloc 0 by AMI_3:10; :: according to SCMFSA_M:def_2 ::_thesis: verum
end;
end;
begin
registration
let f be FinSeq-Location ;
let t be FinSequence of INT ;
clusterf .--> t -> the_Values_of SCM+FSA -compatible ;
coherence
f .--> t is the_Values_of SCM+FSA -compatible
proof
A1: t is Element of INT * by FINSEQ_1:def_11;
Values f = INT * by SCMFSA_2:12;
hence f .--> t is the_Values_of SCM+FSA -compatible by A1; ::_thesis: verum
end;
end;
theorem :: SCMFSA_M:31
for w being FinSequence of INT
for f being FinSeq-Location holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
proof
let w be FinSequence of INT ; ::_thesis: for f being FinSeq-Location holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
let f be FinSeq-Location ; ::_thesis: dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
dom (Initialized (f .--> w)) = (dom (Initialize ((intloc 0) .--> 1))) \/ (dom (f .--> w)) by FUNCT_4:def_1
.= {(intloc 0),(IC )} \/ {f} by Th11, FUNCOP_1:13 ;
hence dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f} by ENUMSET1:3; ::_thesis: verum
end;
theorem :: SCMFSA_M:32
for t being FinSequence of INT
for f being FinSeq-Location holds dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
proof
let t be FinSequence of INT ; ::_thesis: for f being FinSeq-Location holds dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
let f be FinSeq-Location ; ::_thesis: dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
set x = f .--> t;
A1: dom (f .--> t) = {f} by FUNCOP_1:13;
set DI = dom (Initialize ((intloc 0) .--> 1));
assume (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider y being set such that
A2: y in (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) by XBOOLE_0:def_1;
A3: y in dom (Initialize ((intloc 0) .--> 1)) by A2, XBOOLE_0:def_4;
y in dom (f .--> t) by A2, XBOOLE_0:def_4;
then A4: y = f by A1, TARSKI:def_1;
( y = intloc 0 or y = IC ) by A3, Th11, TARSKI:def_2;
hence contradiction by A4, SCMFSA_2:57, SCMFSA_2:58; ::_thesis: verum
end;
theorem :: SCMFSA_M:33
for w being FinSequence of INT
for f being FinSeq-Location
for s being State of SCM+FSA st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
proof
let w be FinSequence of INT ; ::_thesis: for f being FinSeq-Location
for s being State of SCM+FSA st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let s be State of SCM+FSA; ::_thesis: ( Initialized (f .--> w) c= s implies ( s . f = w & s . (intloc 0) = 1 ) )
set t = f .--> w;
set p = Initialized (f .--> w);
assume A2: Initialized (f .--> w) c= s ; ::_thesis: ( s . f = w & s . (intloc 0) = 1 )
reconsider pt = Initialized (f .--> w) as PartState of SCM+FSA ;
dom (f .--> w) = {f} by FUNCOP_1:13;
then B3: f in dom (f .--> w) by TARSKI:def_1;
A4: f in dom pt by B3, FUNCT_4:12;
A5: intloc 0 in dom pt by Th4;
ex i being Element of NAT st f = fsloc i by SCMFSA_2:9;
then f <> intloc 0 by SCMFSA_2:99;
then not f in {(intloc 0)} by TARSKI:def_1;
then A6: not f in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
A7: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
then A8: not f in dom (Initialize ((intloc 0) .--> 1)) by A6, A7, XBOOLE_0:def_3;
thus s . f = pt . f by A2, A4, GRFUNC_1:2
.= (f .--> w) . f by A8, FUNCT_4:11
.= w by FUNCOP_1:72 ; ::_thesis: s . (intloc 0) = 1
thus s . (intloc 0) = (Initialized (f .--> w)) . (intloc 0) by A2, A5, GRFUNC_1:2
.= 1 by Th12, Th10, FUNCT_4:13 ; ::_thesis: verum
end;
theorem :: SCMFSA_M:34
for f being FinSeq-Location
for a being Int-Location
for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
proof
let f be FinSeq-Location ; ::_thesis: for a being Int-Location
for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
let a be Int-Location; ::_thesis: for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
let s be State of SCM+FSA; ::_thesis: {a,(IC ),f} c= dom s
A1: a in dom s by SCMFSA_2:42;
IC in dom s by MEMSTR_0:2;
then A2: {a,(IC )} c= dom s by A1, ZFMISC_1:32;
f in dom s by SCMFSA_2:43;
then {f} c= dom s by ZFMISC_1:31;
then {a,(IC )} \/ {f} c= dom s by A2, XBOOLE_1:8;
hence {a,(IC ),f} c= dom s by ENUMSET1:3; ::_thesis: verum
end;
definition
func Sorting-Function -> PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) means :Def3: :: SCMFSA_M:def 7
for p, q being FinPartState of SCM+FSA holds
( [p,q] in it iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) );
existence
ex b1 being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st
for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )
proof
defpred S1[ set , set ] means ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & $1 = (fsloc 0) .--> t & $2 = (fsloc 0) .--> u );
A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let p, q1, q2 be set ; ::_thesis: ( S1[p,q1] & S1[p,q2] implies q1 = q2 )
given t1 being FinSequence of INT , u1 being FinSequence of REAL such that A2: t1,u1 are_fiberwise_equipotent and
u1 is FinSequence of INT and
A3: u1 is non-increasing and
A4: p = (fsloc 0) .--> t1 and
A5: q1 = (fsloc 0) .--> u1 ; ::_thesis: ( not S1[p,q2] or q1 = q2 )
given t2 being FinSequence of INT , u2 being FinSequence of REAL such that A6: t2,u2 are_fiberwise_equipotent and
u2 is FinSequence of INT and
A7: u2 is non-increasing and
A8: p = (fsloc 0) .--> t2 and
A9: q2 = (fsloc 0) .--> u2 ; ::_thesis: q1 = q2
t1 = ((fsloc 0) .--> t1) . (fsloc 0) by FUNCOP_1:72
.= t2 by A4, A8, FUNCOP_1:72 ;
hence q1 = q2 by A2, A3, A5, A6, A7, A9, CLASSES1:76, RFINSEQ:23; ::_thesis: verum
end;
consider f being Function such that
A10: for p, q being set holds
( [p,q] in f iff ( p in FinPartSt SCM+FSA & S1[p,q] ) ) from FUNCT_1:sch_1(A1);
A11: dom f c= FinPartSt SCM+FSA
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom f or e in FinPartSt SCM+FSA )
assume e in dom f ; ::_thesis: e in FinPartSt SCM+FSA
then [e,(f . e)] in f by FUNCT_1:1;
hence e in FinPartSt SCM+FSA by A10; ::_thesis: verum
end;
rng f c= FinPartSt SCM+FSA
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng f or q in FinPartSt SCM+FSA )
assume q in rng f ; ::_thesis: q in FinPartSt SCM+FSA
then consider p being set such that
A12: [p,q] in f by XTUPLE_0:def_13;
consider t being FinSequence of INT , u being FinSequence of REAL such that
t,u are_fiberwise_equipotent and
A13: u is FinSequence of INT and
u is non-increasing and
p = (fsloc 0) .--> t and
A14: q = (fsloc 0) .--> u by A10, A12;
reconsider u = u as FinSequence of INT by A13;
(fsloc 0) .--> u is FinPartState of SCM+FSA ;
hence q in FinPartSt SCM+FSA by A14, MEMSTR_0:75; ::_thesis: verum
end;
then reconsider f = f as PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) by A11, RELSET_1:4;
take f ; ::_thesis: for p, q being FinPartState of SCM+FSA holds
( [p,q] in f iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )
let p, q be FinPartState of SCM+FSA; ::_thesis: ( [p,q] in f iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )
thus ( [p,q] in f implies ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) by A10; ::_thesis: ( ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) implies [p,q] in f )
given t being FinSequence of INT , u being FinSequence of REAL such that A15: t,u are_fiberwise_equipotent and
A16: u is FinSequence of INT and
A17: u is non-increasing and
A18: p = (fsloc 0) .--> t and
A19: q = (fsloc 0) .--> u ; ::_thesis: [p,q] in f
p in FinPartSt SCM+FSA by MEMSTR_0:75;
hence [p,q] in f by A10, A15, A16, A17, A18, A19; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) & ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) holds
b1 = b2
proof
let IT1, IT2 be PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA); ::_thesis: ( ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) & ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) implies IT1 = IT2 )
assume that
A20: for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) and
A21: for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ; ::_thesis: IT1 = IT2
defpred S1[ set , set ] means ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & $1 = (fsloc 0) .--> t & $2 = (fsloc 0) .--> u );
A22: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT1 iff S1[p,q] )
proof
let p, q be Element of FinPartSt SCM+FSA; ::_thesis: ( [p,q] in IT1 iff S1[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
( [p,q] in IT1 iff S1[p,q] ) by A20;
hence ( [p,q] in IT1 iff S1[p,q] ) ; ::_thesis: verum
end;
A23: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT2 iff S1[p,q] )
proof
let p, q be Element of FinPartSt SCM+FSA; ::_thesis: ( [p,q] in IT2 iff S1[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
( [p,q] in IT2 iff S1[p,q] ) by A21;
hence ( [p,q] in IT2 iff S1[p,q] ) ; ::_thesis: verum
end;
thus IT1 = IT2 from RELSET_1:sch_4(A22, A23); ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Sorting-Function SCMFSA_M:def_7_:_
for b1 being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) holds
( b1 = Sorting-Function iff for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) );
theorem :: SCMFSA_M:35
for p being set holds
( p in dom Sorting-Function iff ex t being FinSequence of INT st p = (fsloc 0) .--> t )
proof
set f = Sorting-Function ;
let p be set ; ::_thesis: ( p in dom Sorting-Function iff ex t being FinSequence of INT st p = (fsloc 0) .--> t )
hereby ::_thesis: ( ex t being FinSequence of INT st p = (fsloc 0) .--> t implies p in dom Sorting-Function )
set q = Sorting-Function . p;
assume A1: p in dom Sorting-Function ; ::_thesis: ex t being FinSequence of INT st p = (fsloc 0) .--> t
then A2: [p,(Sorting-Function . p)] in Sorting-Function by FUNCT_1:1;
dom Sorting-Function c= FinPartSt SCM+FSA by RELAT_1:def_18;
then A3: p is FinPartState of SCM+FSA by A1, MEMSTR_0:76;
Sorting-Function . p in FinPartSt SCM+FSA by A1, PARTFUN1:4;
then Sorting-Function . p is FinPartState of SCM+FSA by MEMSTR_0:76;
then consider t being FinSequence of INT , u being FinSequence of REAL such that
t,u are_fiberwise_equipotent and
u is FinSequence of INT and
u is non-increasing and
A4: p = (fsloc 0) .--> t and
Sorting-Function . p = (fsloc 0) .--> u by A2, A3, Def3;
take t = t; ::_thesis: p = (fsloc 0) .--> t
thus p = (fsloc 0) .--> t by A4; ::_thesis: verum
end;
given t being FinSequence of INT such that A5: p = (fsloc 0) .--> t ; ::_thesis: p in dom Sorting-Function
consider u being FinSequence of REAL such that
A6: t,u are_fiberwise_equipotent and
A7: u is FinSequence of INT and
A8: u is non-increasing by RFINSEQ:33;
reconsider u1 = u as FinSequence of INT by A7;
set q = (fsloc 0) .--> u1;
[p,((fsloc 0) .--> u1)] in Sorting-Function by A5, A6, A8, Def3;
hence p in dom Sorting-Function by FUNCT_1:1; ::_thesis: verum
end;
theorem :: SCMFSA_M:36
for t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u )
proof
let t be FinSequence of INT ; ::_thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u )
consider u being FinSequence of REAL such that
A1: t,u are_fiberwise_equipotent and
A2: u is FinSequence of INT and
A3: u is non-increasing by RFINSEQ:33;
reconsider u = u as FinSequence of INT by A2;
set p = (fsloc 0) .--> t;
set q = (fsloc 0) .--> u;
[((fsloc 0) .--> t),((fsloc 0) .--> u)] in Sorting-Function by A1, A3, Def3;
then Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u by FUNCT_1:1;
hence ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u ) by A1, A3; ::_thesis: verum
end;
theorem :: SCMFSA_M:37
for s being State of SCM+FSA holds
( ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )
proof
let s be State of SCM+FSA; ::_thesis: ( ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )
A1: Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
A2: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
hereby ::_thesis: for f being FinSeq-Location holds (Initialized s) . f = s . f
let a be read-write Int-Location; ::_thesis: (Initialized s) . a = s . a
A3: not a in dom ((intloc 0) .--> 1) by A2, TARSKI:def_1;
not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialized s) . a = (s +* ((intloc 0) .--> 1)) . a by A1, FUNCT_4:11
.= s . a by A3, FUNCT_4:11 ;
::_thesis: verum
end;
hereby ::_thesis: verum
let f be FinSeq-Location ; ::_thesis: (Initialized s) . f = s . f
intloc 0 <> f by SCMFSA_2:58;
then A4: not f in dom ((intloc 0) .--> 1) by A2, TARSKI:def_1;
not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
hence (Initialized s) . f = (s +* ((intloc 0) .--> 1)) . f by A1, FUNCT_4:11
.= s . f by A4, FUNCT_4:11 ;
::_thesis: verum
end;
end;