begin
Lm1:
for m, n, k being Nat st m < n & n <= k + 1 holds
m <= k
Lm2:
for n being Element of NAT
for p, q being FinSequence of NAT holds len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q)
definition
existence
ex b1 being non empty set st
( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
EX p in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
EG p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p EU q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
b1 c= D ) )
uniqueness
for b1, b2 being non empty set st ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
EX p in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
EG p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p EU q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
b1 c= D ) & ( for a being set st a in b2 holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p '&' q in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
EX p in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
EG p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p EU q in b2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
b2 c= D ) holds
b1 = b2
end;
Lm3:
for H being CTL-formula st H is negative holds
H . 1 = 0
Lm4:
for H being CTL-formula st H is conjunctive holds
H . 1 = 1
Lm5:
for H being CTL-formula st H is ExistNext holds
H . 1 = 2
Lm6:
for H being CTL-formula st H is ExistGlobal holds
H . 1 = 3
Lm7:
for H being CTL-formula st H is ExistUntill holds
H . 1 = 4
Lm8:
for H being CTL-formula st H is atomic holds
( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 )
Lm9:
for H being CTL-formula holds
( ( H is atomic & H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 ) or ( H is negative & H . 1 = 0 ) or ( H is conjunctive & H . 1 = 1 ) or ( H is ExistNext & H . 1 = 2 ) or ( H is ExistGlobal & H . 1 = 3 ) or ( H is ExistUntill & H . 1 = 4 ) )
Lm10:
for H being CTL-formula holds 1 <= len H
Lm11:
for H, F being CTL-formula
for sq being FinSequence st H = F ^ sq holds
H = F
Lm12:
for H, G, H1, G1 being CTL-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )
Lm13:
for H, G, H1, G1 being CTL-formula st H EU G = H1 EU G1 holds
( H = H1 & G = G1 )
Lm14:
for H being CTL-formula st H is atomic holds
( not H is negative & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )
Lm15:
for H being CTL-formula st H is negative holds
( not H is atomic & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )
Lm16:
for H being CTL-formula st H is conjunctive holds
( not H is atomic & not H is negative & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )
Lm17:
for H being CTL-formula st H is ExistNext holds
( not H is atomic & not H is conjunctive & not H is negative & not H is ExistGlobal & not H is ExistUntill )
Lm18:
for H being CTL-formula st H is ExistGlobal holds
( not H is atomic & not H is conjunctive & not H is negative & not H is ExistNext & not H is ExistUntill )
definition
let H be
CTL-formula;
assume A1:
(
H is
conjunctive or
H is
ExistUntill )
;
existence
( ( H is conjunctive implies ex b1, H1 being CTL-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being CTL-formula st b1 EU H1 = H ) )
by A1, Def16, Def19;
uniqueness
for b1, b2 being CTL-formula holds
( ( H is conjunctive & ex H1 being CTL-formula st b1 '&' H1 = H & ex H1 being CTL-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being CTL-formula st b1 EU H1 = H & ex H1 being CTL-formula st b2 EU H1 = H implies b1 = b2 ) )
by Lm12, Lm13;
consistency
for b1 being CTL-formula holds verum
;
existence
( ( H is conjunctive implies ex b1, H1 being CTL-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being CTL-formula st H1 EU b1 = H ) )
uniqueness
for b1, b2 being CTL-formula holds
( ( H is conjunctive & ex H1 being CTL-formula st H1 '&' b1 = H & ex H1 being CTL-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being CTL-formula st H1 EU b1 = H & ex H1 being CTL-formula st H1 EU b2 = H implies b1 = b2 ) )
by Lm12, Lm13;
consistency
for b1 being CTL-formula holds verum
;
end;
Lm19:
for H being CTL-formula st H is ExistGlobal holds
H = EG (the_argument_of H)
Lm20:
for H being CTL-formula st H is conjunctive holds
H = (the_left_argument_of H) '&' (the_right_argument_of H)
Lm21:
for H being CTL-formula st H is ExistUntill holds
H = (the_left_argument_of H) EU (the_right_argument_of H)
Lm22:
for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds
len (the_argument_of H) < len H
Lm23:
for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds
( len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )
definition
let V be
CTLModelStr ;
let Kai be
Function of
atomic_WFF, the
BasicAssign of
V;
let f,
h be
Function of
CTL_WFF, the
carrier of
V;
let n be
Element of
NAT ;
let H be
CTL-formula;
coherence
( ( len H > n + 1 implies f . H is set ) & ( len H = n + 1 & H is atomic implies Kai . H is set ) & ( len H = n + 1 & H is negative implies the Compl of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is conjunctive implies the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is ExistNext implies the EneXt of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is ExistGlobal implies the EGlobal of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is ExistUntill implies the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H < n + 1 implies h . H is set ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is ExistNext ) & ( not len H = n + 1 or not H is ExistGlobal ) & ( not len H = n + 1 or not H is ExistUntill ) & not len H < n + 1 implies {} is set ) )
;
consistency
for b1 being set holds
( ( len H > n + 1 & len H = n + 1 & H is atomic implies ( b1 = f . H iff b1 = Kai . H ) ) & ( len H > n + 1 & len H = n + 1 & H is negative implies ( b1 = f . H iff b1 = the Compl of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is conjunctive implies ( b1 = f . H iff b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistNext implies ( b1 = f . H iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistGlobal implies ( b1 = f . H iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistUntill implies ( b1 = f . H iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H < n + 1 implies ( b1 = f . H iff b1 = h . H ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is negative implies ( b1 = Kai . H iff b1 = the Compl of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is conjunctive implies ( b1 = Kai . H iff b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistNext implies ( b1 = Kai . H iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistGlobal implies ( b1 = Kai . H iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistUntill implies ( b1 = Kai . H iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H < n + 1 implies ( b1 = Kai . H iff b1 = h . H ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is conjunctive implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistNext implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistGlobal implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistUntill implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H < n + 1 implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistNext implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistGlobal implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistUntill implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is conjunctive & len H < n + 1 implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = h . H ) ) & ( len H = n + 1 & H is ExistNext & len H = n + 1 & H is ExistGlobal implies ( b1 = the EneXt of V . (h . (the_argument_of H)) iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is ExistNext & len H = n + 1 & H is ExistUntill implies ( b1 = the EneXt of V . (h . (the_argument_of H)) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is ExistNext & len H < n + 1 implies ( b1 = the EneXt of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is ExistGlobal & len H = n + 1 & H is ExistUntill implies ( b1 = the EGlobal of V . (h . (the_argument_of H)) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is ExistGlobal & len H < n + 1 implies ( b1 = the EGlobal of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is ExistUntill & len H < n + 1 implies ( b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = h . H ) ) )
by Lm14, Lm15, Lm16, Lm17, Lm18;
end;
::
deftheorem Def28 defines
GraftEval MODELC_1:def 28 :
for V being CTLModelStr
for Kai being Function of atomic_WFF, the BasicAssign of V
for f, h being Function of CTL_WFF, the carrier of V
for n being Element of NAT
for H being CTL-formula holds
( ( len H > n + 1 implies GraftEval (V,Kai,f,h,n,H) = f . H ) & ( len H = n + 1 & H is atomic implies GraftEval (V,Kai,f,h,n,H) = Kai . H ) & ( len H = n + 1 & H is negative implies GraftEval (V,Kai,f,h,n,H) = the Compl of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is ExistNext implies GraftEval (V,Kai,f,h,n,H) = the EneXt of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistGlobal implies GraftEval (V,Kai,f,h,n,H) = the EGlobal of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistUntill implies GraftEval (V,Kai,f,h,n,H) = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = h . H ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is ExistNext ) & ( not len H = n + 1 or not H is ExistGlobal ) & ( not len H = n + 1 or not H is ExistUntill ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) );
Lm24:
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V holds f is-PreEvaluation-for 0 ,Kai
Lm25:
for n being Element of NAT
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
Lm26:
for n being Element of NAT
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V st f is-Evaluation-for Kai holds
f is-PreEvaluation-for n,Kai
Lm27:
for n being Element of NAT
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f1, f2 being Function of CTL_WFF, the carrier of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
Lm28:
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for n being Element of NAT ex f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai
Lm29:
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V st ( for n being Element of NAT holds f is-PreEvaluation-for n,Kai ) holds
f is-Evaluation-for Kai
definition
let V be
CTLModel;
let Kai be
Function of
atomic_WFF, the
BasicAssign of
V;
existence
ex b1 being non empty set st
for p being set holds
( p in b1 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) )
uniqueness
for b1, b2 being non empty set st ( for p being set holds
( p in b1 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) ) & ( for p being set holds
( p in b2 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) ) holds
b1 = b2
end;
Lm30:
for n being Element of NAT
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)
Lm31:
for S being set
for R being Relation of S,S st R is total holds
for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R )
Lm32:
for S being set
for R being Relation of S,S st ( for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ) holds
R is total
Lm33:
for S being non empty set
for R being total Relation of S,S
for s being Element of S holds not R .: {s} is empty
Lm34:
for S being non empty set
for R being total Relation of S,S
for s0 being Element of S ex f being Function of NAT,S st
( f . 0 = s0 & ( for n being Element of NAT holds [(f . n),(f . (n + 1))] in R ) )
Lm35:
for S being non empty set
for s being Element of S
for f being set st (Fid (f,S)) . s <> TRUE holds
(Fid (f,S)) . s = FALSE
by TARSKI:def 2;
scheme
UnOpUnique{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3(
set )
-> Element of
F2() } :
for
o1,
o2 being
UnOp of
F2() st ( for
f being
set st
f in F2() holds
o1 . f = F3(
f) ) & ( for
f being
set st
f in F2() holds
o2 . f = F3(
f) ) holds
o1 = o2
Lm36:
for S being non empty set
for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
o1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP S holds
o2 . f = Not_0 (f,S) ) holds
o1 = o2
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let f be
set ;
existence
ex b1 being Element of ModelSP S st
for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE )
uniqueness
for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds
b1 = b2
end;
Lm37:
for S being non empty set
for R being total Relation of S,S
for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
o1 . f = EneXt_0 (f,R) ) & ( for f being set st f in ModelSP S holds
o2 . f = EneXt_0 (f,R) ) holds
o1 = o2
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let f be
set ;
existence
ex b1 being Element of ModelSP S st
for s being set st s in S holds
( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE )
uniqueness
for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds
( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds
b1 = b2
end;
Lm38:
for S being non empty set
for R being total Relation of S,S
for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
o1 . f = EGlobal_0 (f,R) ) & ( for f being set st f in ModelSP S holds
o2 . f = EGlobal_0 (f,R) ) holds
o1 = o2
definition
let S be non
empty set ;
let f,
g be
set ;
existence
ex b1 being Element of ModelSP S st
for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE )
uniqueness
for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds
b1 = b2
end;
Lm39:
for S being non empty set
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = And_0 (f,g,S) ) holds
o1 = o2
definition
let S be non
empty set ;
existence
ex b1 being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
b1 . (f,g) = And_0 (f,g,S)
uniqueness
for b1, b2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b2 . (f,g) = And_0 (f,g,S) ) holds
b1 = b2
by Lm39;
end;
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let f,
g be
set ;
existence
ex b1 being Element of ModelSP S st
for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE )
uniqueness
for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds
b1 = b2
end;
::
deftheorem Def53 defines
EUntill_0 MODELC_1:def 53 :
for S being non empty set
for R being total Relation of S,S
for f, g being set
for b5 being Element of ModelSP S holds
( b5 = EUntill_0 (f,g,R) iff for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b5,S)) . s = TRUE ) );
Lm40:
for S being non empty set
for R being total Relation of S,S
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
existence
ex b1 being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
b1 . (f,g) = EUntill_0 (f,g,R)
uniqueness
for b1, b2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b2 . (f,g) = EUntill_0 (f,g,R) ) holds
b1 = b2
by Lm40;
end;
Lm41:
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }
Lm42:
for X being non empty set
for f, g being Function of X,BOOLEAN st { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } holds
f = g
Lm43:
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds
f = g
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let BASSIGN be non
empty Subset of
(ModelSP S);
let T be
Subset of
S;
existence
ex b1 being Assign of (BASSModel (R,BASSIGN)) st
for s being set st s in S holds
(Fid (b1,S)) . s = (chi (T,S)) . s
uniqueness
for b1, b2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being set st s in S holds
(Fid (b1,S)) . s = (chi (T,S)) . s ) & ( for s being set st s in S holds
(Fid (b2,S)) . s = (chi (T,S)) . s ) holds
b1 = b2
end;
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let pai1,
pai2 be
inf_path of
R;
let k be
Element of
NAT ;
existence
ex b1 being Function of NAT,S st
for n being Element of NAT holds b1 . n = PathChange (pai1,pai2,k,n)
uniqueness
for b1, b2 being Function of NAT,S st ( for n being Element of NAT holds b1 . n = PathChange (pai1,pai2,k,n) ) & ( for n being Element of NAT holds b2 . n = PathChange (pai1,pai2,k,n) ) holds
b1 = b2
end;
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let BASSIGN be non
empty Subset of
(ModelSP S);
let f be
Assign of
(BASSModel (R,BASSIGN));
existence
ex b1 being V226() Function of (bool S),(bool S) st
for G being Subset of S holds b1 . G = SigFaxTau (f,G,R,BASSIGN)
uniqueness
for b1, b2 being V226() Function of (bool S),(bool S) st ( for G being Subset of S holds b1 . G = SigFaxTau (f,G,R,BASSIGN) ) & ( for G being Subset of S holds b2 . G = SigFaxTau (f,G,R,BASSIGN) ) holds
b1 = b2
end;
::
deftheorem defines
SigFoaxTau MODELC_1:def 72 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN))
for H being Subset of S holds SigFoaxTau (g,f,H,R,BASSIGN) = SIGMA (Foax (g,f,(Tau (H,R,BASSIGN))));
theorem Th45:
for
S being non
empty set for
R being
total Relation of
S,
S for
BASSIGN being non
empty Subset of
(ModelSP S) for
f,
g being
Assign of
(BASSModel (R,BASSIGN)) for
H1,
H2 being
Subset of
S st
H1 c= H2 holds
SigFoaxTau (
g,
f,
H1,
R,
BASSIGN)
c= SigFoaxTau (
g,
f,
H2,
R,
BASSIGN)
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let BASSIGN be non
empty Subset of
(ModelSP S);
let f,
g be
Assign of
(BASSModel (R,BASSIGN));
existence
ex b1 being V226() Function of (bool S),(bool S) st
for H being Subset of S holds b1 . H = SigFoaxTau (g,f,H,R,BASSIGN)
uniqueness
for b1, b2 being V226() Function of (bool S),(bool S) st ( for H being Subset of S holds b1 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) & ( for H being Subset of S holds b2 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) holds
b1 = b2
end;