begin
Lm1:
for m, n, k being Nat st m < n & n <= k + 1 holds
m <= k
:: deftheorem Def1 defines k_id MODELC_1:def 1 :
for x, S being set
for a being Element of S holds
( ( x in S implies k_id (x,S,a) = x ) & ( not x in S implies k_id (x,S,a) = a ) );
:: deftheorem Def2 defines k_nat MODELC_1:def 2 :
for x being set holds
( ( x in NAT implies k_nat x = x ) & ( not x in NAT implies k_nat x = 0 ) );
:: deftheorem Def3 defines UnivF MODELC_1:def 3 :
for f being Function
for x, a being set holds
( ( x in dom f implies UnivF (x,f,a) = f . x ) & ( not x in dom f implies UnivF (x,f,a) = a ) );
:: deftheorem Def4 defines Castboolean MODELC_1:def 4 :
for a being set holds
( ( a is boolean set implies Castboolean a = a ) & ( a is not boolean set implies Castboolean a = FALSE ) );
:: deftheorem Def5 defines CastBool MODELC_1:def 5 :
for X, a being set holds
( ( a c= X implies CastBool (a,X) = a ) & ( not a c= X implies CastBool (a,X) = {} ) );
:: deftheorem defines atom. MODELC_1:def 6 :
for n being Element of NAT holds atom. n = <*(5 + n)*>;
:: deftheorem defines 'not' MODELC_1:def 7 :
for p being FinSequence of NAT holds 'not' p = <*0*> ^ p;
:: deftheorem defines '&' MODELC_1:def 8 :
for p, q being FinSequence of NAT holds p '&' q = (<*1*> ^ p) ^ q;
:: deftheorem defines EX MODELC_1:def 9 :
for p being FinSequence of NAT holds EX p = <*2*> ^ p;
:: deftheorem defines EG MODELC_1:def 10 :
for p being FinSequence of NAT holds EG p = <*3*> ^ p;
:: deftheorem defines EU MODELC_1:def 11 :
for p, q being FinSequence of NAT holds p EU q = (<*4*> ^ p) ^ q;
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
func CTL_WFF -> non
empty set means :
Def12:
( ( for
a being
set st
a in it holds
a is
FinSequence of
NAT ) & ( for
n being
Element of
NAT holds
atom. n in it ) & ( for
p being
FinSequence of
NAT st
p in it holds
'not' p in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p '&' q in it ) & ( for
p being
FinSequence of
NAT st
p in it holds
EX p in it ) & ( for
p being
FinSequence of
NAT st
p in it holds
EG p in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p EU q in it ) & ( 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
it c= D ) );
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;
:: deftheorem Def12 defines CTL_WFF MODELC_1:def 12 :
for b1 being non empty set holds
( b1 = CTL_WFF iff ( ( 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 ) ) );
:: deftheorem Def13 defines CTL-formula-like MODELC_1:def 13 :
for IT being FinSequence of NAT holds
( IT is CTL-formula-like iff IT is Element of CTL_WFF );
theorem Th1:
:: deftheorem Def14 defines atomic MODELC_1:def 14 :
for H being CTL-formula holds
( H is atomic iff ex n being Element of NAT st H = atom. n );
:: deftheorem Def15 defines negative MODELC_1:def 15 :
for H being CTL-formula holds
( H is negative iff ex H1 being CTL-formula st H = 'not' H1 );
:: deftheorem Def16 defines conjunctive MODELC_1:def 16 :
for H being CTL-formula holds
( H is conjunctive iff ex F, G being CTL-formula st H = F '&' G );
:: deftheorem Def17 defines ExistNext MODELC_1:def 17 :
for H being CTL-formula holds
( H is ExistNext iff ex H1 being CTL-formula st H = EX H1 );
:: deftheorem Def18 defines ExistGlobal MODELC_1:def 18 :
for H being CTL-formula holds
( H is ExistGlobal iff ex H1 being CTL-formula st H = EG H1 );
:: deftheorem Def19 defines ExistUntill MODELC_1:def 19 :
for H being CTL-formula holds
( H is ExistUntill iff ex F, G being CTL-formula st H = F EU G );
:: deftheorem defines 'or' MODELC_1:def 20 :
for F, G being CTL-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));
theorem Th2:
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 )
:: deftheorem Def21 defines the_argument_of MODELC_1:def 21 :
for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds
for b2 being CTL-formula holds
( ( H is negative implies ( b2 = the_argument_of H iff 'not' b2 = H ) ) & ( H is ExistNext implies ( b2 = the_argument_of H iff EX b2 = H ) ) & ( not H is negative & not H is ExistNext implies ( b2 = the_argument_of H iff EG b2 = H ) ) );
definition
let H be
CTL-formula;
assume A1:
(
H is
conjunctive or
H is
ExistUntill )
;
func the_left_argument_of H -> CTL-formula means :
Def22:
ex
H1 being
CTL-formula st
it '&' H1 = H if H is
conjunctive otherwise ex
H1 being
CTL-formula st
it EU H1 = H;
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
;
func the_right_argument_of H -> CTL-formula means :
Def23:
ex
H1 being
CTL-formula st
H1 '&' it = H if H is
conjunctive otherwise ex
H1 being
CTL-formula st
H1 EU it = H;
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;
:: deftheorem Def22 defines the_left_argument_of MODELC_1:def 22 :
for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds
for b2 being CTL-formula holds
( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being CTL-formula st b2 '&' H1 = H ) ) & ( not H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being CTL-formula st b2 EU H1 = H ) ) );
:: deftheorem Def23 defines the_right_argument_of MODELC_1:def 23 :
for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds
for b2 being CTL-formula holds
( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being CTL-formula st H1 '&' b2 = H ) ) & ( not H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being CTL-formula st H1 EU b2 = H ) ) );
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 )
:: deftheorem Def24 defines CastCTLformula MODELC_1:def 24 :
for x being set holds
( ( x in CTL_WFF implies CastCTLformula x = x ) & ( not x in CTL_WFF implies CastCTLformula x = atom. 0 ) );
:: deftheorem defines atomic_WFF MODELC_1:def 25 :
atomic_WFF = { x where x is CTL-formula : x is atomic } ;
:: deftheorem Def26 defines is-Evaluation-for MODELC_1:def 26 :
for V being CTLModelStr
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-Evaluation-for Kai iff for H being CTL-formula holds
( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) );
:: deftheorem Def27 defines is-PreEvaluation-for MODELC_1:def 27 :
for V being CTLModelStr
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V
for n being Element of NAT holds
( f is-PreEvaluation-for n,Kai iff for H being CTL-formula st len H <= n holds
( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of 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;
func GraftEval (
V,
Kai,
f,
h,
n,
H)
-> set equals :
Def28:
f . H if len H > n + 1
Kai . H if (
len H = n + 1 &
H is
atomic )
the
Compl of
V . (h . (the_argument_of H)) if (
len H = n + 1 &
H is
negative )
the
L_meet of
V . (
(h . (the_left_argument_of H)),
(h . (the_right_argument_of H)))
if (
len H = n + 1 &
H is
conjunctive )
the
EneXt of
V . (h . (the_argument_of H)) if (
len H = n + 1 &
H is
ExistNext )
the
EGlobal of
V . (h . (the_argument_of H)) if (
len H = n + 1 &
H is
ExistGlobal )
the
EUntill of
V . (
(h . (the_left_argument_of H)),
(h . (the_right_argument_of H)))
if (
len H = n + 1 &
H is
ExistUntill )
h . H if len H < n + 1
otherwise {} ;
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) = {} ) );
:: deftheorem Def29 defines with_basic MODELC_1:def 29 :
for C being CTLModelStr holds
( C is with_basic iff not the BasicAssign of C is empty );
definition
func TrivialCTLModel -> CTLModelStr equals
CTLModelStr(# 1,
([#] 1),
op2,
op1,
op1,
op1,
op2 #);
coherence
CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #) is CTLModelStr
;
end;
:: deftheorem defines TrivialCTLModel MODELC_1:def 30 :
TrivialCTLModel = CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #);
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
:: deftheorem defines EvalSet MODELC_1:def 31 :
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for n being Element of NAT holds EvalSet (V,Kai,n) = { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;
:: deftheorem Def32 defines CastEval MODELC_1:def 32 :
for V being CTLModel
for v0 being Element of the carrier of V
for x being set holds
( ( x in Funcs (CTL_WFF, the carrier of V) implies CastEval (V,x,v0) = x ) & ( not x in Funcs (CTL_WFF, the carrier of V) implies CastEval (V,x,v0) = CTL_WFF --> v0 ) );
definition
let V be
CTLModel;
let Kai be
Function of
atomic_WFF, the
BasicAssign of
V;
func EvalFamily (
V,
Kai)
-> non
empty set means :
Def33:
for
p being
set holds
(
p in it iff (
p in bool (Funcs (CTL_WFF, the carrier of V)) & ex
n being
Element of
NAT st
p = EvalSet (
V,
Kai,
n) ) );
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;
:: deftheorem Def33 defines EvalFamily MODELC_1:def 33 :
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for b3 being non empty set holds
( b3 = EvalFamily (V,Kai) iff for p being set holds
( p in b3 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) );
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)
theorem Th3:
theorem Th4:
:: deftheorem Def34 defines Evaluate MODELC_1:def 34 :
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for H being CTL-formula
for b4 being Assign of V holds
( b4 = Evaluate (H,Kai) iff ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b4 = f . H ) );
:: deftheorem MODELC_1:def 35 :
canceled;
:: deftheorem MODELC_1:def 36 :
canceled;
:: deftheorem defines EX MODELC_1:def 37 :
for V being CTLModel
for f being Assign of V holds EX f = the EneXt of V . f;
:: deftheorem defines EG MODELC_1:def 38 :
for V being CTLModel
for f being Assign of V holds EG f = the EGlobal of V . f;
:: deftheorem defines EU MODELC_1:def 39 :
for V being CTLModel
for f, g being Assign of V holds f EU g = the EUntill of V . (f,g);
:: deftheorem defines 'or' MODELC_1:def 40 :
for V being CTLModel
for f, g being Assign of V holds f 'or' g = 'not' (('not' f) '&' ('not' g));
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
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 ) )
:: deftheorem Def41 defines inf_path MODELC_1:def 41 :
for S being non empty set
for R being total Relation of S,S
for b3 being Function of NAT,S holds
( b3 is inf_path of R iff for n being Element of NAT holds [(b3 . n),(b3 . (n + 1))] in R );
:: deftheorem defines ModelSP MODELC_1:def 42 :
for S being non empty set holds ModelSP S = Funcs (S,BOOLEAN);
:: deftheorem Def43 defines Fid MODELC_1:def 43 :
for S being non empty set
for f being set holds
( ( f in ModelSP S implies Fid (f,S) = f ) & ( not f in ModelSP S implies Fid (f,S) = S --> FALSE ) );
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
definition
let S be non
empty set ;
let f be
set ;
func Not_0 (
f,
S)
-> Element of
ModelSP S means :
Def44:
for
s being
set st
s in S holds
(
'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff
(Fid (it,S)) . s = TRUE );
existence
ex b1 being Element of ModelSP S st
for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,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
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds
b1 = b2
end;
:: deftheorem Def44 defines Not_0 MODELC_1:def 44 :
for S being non empty set
for f being set
for b3 being Element of ModelSP S holds
( b3 = Not_0 (f,S) iff for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b3,S)) . s = TRUE ) );
Lm36:
for S being non empty set ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = Not_0 (f,S)
Lm37:
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
:: deftheorem Def45 defines Not_ MODELC_1:def 45 :
for S being non empty set
for b2 being UnOp of (ModelSP S) holds
( b2 = Not_ S iff for f being set st f in ModelSP S holds
b2 . f = Not_0 (f,S) );
:: deftheorem Def46 defines EneXt_univ MODELC_1:def 46 :
for S being non empty set
for R being total Relation of S,S
for f being Function of S,BOOLEAN
for x being set holds
( ( x in S & ex pai being inf_path of R st
( pai . 0 = x & f . (pai . 1) = TRUE ) implies EneXt_univ (x,f,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds
( not pai . 0 = x or not f . (pai . 1) = TRUE ) ) implies EneXt_univ (x,f,R) = FALSE ) );
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let f be
set ;
func EneXt_0 (
f,
R)
-> Element of
ModelSP S means :
Def47:
for
s being
set st
s in S holds
(
EneXt_univ (
s,
(Fid (f,S)),
R)
= TRUE iff
(Fid (it,S)) . s = TRUE );
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;
:: deftheorem Def47 defines EneXt_0 MODELC_1:def 47 :
for S being non empty set
for R being total Relation of S,S
for f being set
for b4 being Element of ModelSP S holds
( b4 = EneXt_0 (f,R) iff for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b4,S)) . s = TRUE ) );
Lm38:
for S being non empty set
for R being total Relation of S,S ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = EneXt_0 (f,R)
Lm39:
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
:: deftheorem Def48 defines EneXt_ MODELC_1:def 48 :
for S being non empty set
for R being total Relation of S,S
for b3 being UnOp of (ModelSP S) holds
( b3 = EneXt_ R iff for f being set st f in ModelSP S holds
b3 . f = EneXt_0 (f,R) );
:: deftheorem Def49 defines EGlobal_univ MODELC_1:def 49 :
for S being non empty set
for R being total Relation of S,S
for f being Function of S,BOOLEAN
for x being set holds
( ( x in S & ex pai being inf_path of R st
( pai . 0 = x & ( for n being Element of NAT holds f . (pai . n) = TRUE ) ) implies EGlobal_univ (x,f,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds
( not pai . 0 = x or ex n being Element of NAT st not f . (pai . n) = TRUE ) ) implies EGlobal_univ (x,f,R) = FALSE ) );
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let f be
set ;
func EGlobal_0 (
f,
R)
-> Element of
ModelSP S means :
Def50:
for
s being
set st
s in S holds
(
EGlobal_univ (
s,
(Fid (f,S)),
R)
= TRUE iff
(Fid (it,S)) . s = TRUE );
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;
:: deftheorem Def50 defines EGlobal_0 MODELC_1:def 50 :
for S being non empty set
for R being total Relation of S,S
for f being set
for b4 being Element of ModelSP S holds
( b4 = EGlobal_0 (f,R) iff for s being set st s in S holds
( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b4,S)) . s = TRUE ) );
Lm40:
for S being non empty set
for R being total Relation of S,S ex o being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
o . f = EGlobal_0 (f,R)
Lm41:
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
:: deftheorem Def51 defines EGlobal_ MODELC_1:def 51 :
for S being non empty set
for R being total Relation of S,S
for b3 being UnOp of (ModelSP S) holds
( b3 = EGlobal_ R iff for f being set st f in ModelSP S holds
b3 . f = EGlobal_0 (f,R) );
definition
let S be non
empty set ;
let f,
g be
set ;
func And_0 (
f,
g,
S)
-> Element of
ModelSP S means :
Def52:
for
s being
set st
s in S holds
(
(Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff
(Fid (it,S)) . s = TRUE );
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;
:: deftheorem Def52 defines And_0 MODELC_1:def 52 :
for S being non empty set
for f, g being set
for b4 being Element of ModelSP S holds
( b4 = And_0 (f,g,S) iff for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b4,S)) . s = TRUE ) );
Lm42:
for S being non empty set ex o being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
o . (f,g) = And_0 (f,g,S)
Lm43:
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 ;
func And_ S -> BinOp of
(ModelSP S) means :
Def53:
for
f,
g being
set st
f in ModelSP S &
g in ModelSP S holds
it . (
f,
g)
= And_0 (
f,
g,
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) = And_0 (f,g,S)
by Lm42;
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 Lm43;
end;
:: deftheorem Def53 defines And_ MODELC_1:def 53 :
for S being non empty set
for b2 being BinOp of (ModelSP S) holds
( b2 = And_ S iff for f, g being set st f in ModelSP S & g in ModelSP S holds
b2 . (f,g) = And_0 (f,g,S) );
:: deftheorem Def54 defines EUntill_univ MODELC_1:def 54 :
for S being non empty set
for R being total Relation of S,S
for f, g being Function of S,BOOLEAN
for x being set holds
( ( x in S & ex pai being inf_path of R st
( pai . 0 = x & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
f . (pai . j) = TRUE ) & g . (pai . m) = TRUE ) ) implies EUntill_univ (x,f,g,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds
( not pai . 0 = x or for m being Element of NAT holds
( ex j being Element of NAT st
( j < m & not f . (pai . j) = TRUE ) or not g . (pai . m) = TRUE ) ) ) implies EUntill_univ (x,f,g,R) = FALSE ) );
definition
let S be non
empty set ;
let R be
total Relation of
S,
S;
let f,
g be
set ;
func EUntill_0 (
f,
g,
R)
-> Element of
ModelSP S means :
Def55:
for
s being
set st
s in S holds
(
EUntill_univ (
s,
(Fid (f,S)),
(Fid (g,S)),
R)
= TRUE iff
(Fid (it,S)) . s = TRUE );
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 Def55 defines EUntill_0 MODELC_1:def 55 :
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 ) );
Lm44:
for S being non empty set
for R being total Relation of S,S ex o being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
o . (f,g) = EUntill_0 (f,g,R)
Lm45:
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;
func EUntill_ R -> BinOp of
(ModelSP S) means :
Def56:
for
f,
g being
set st
f in ModelSP S &
g in ModelSP S holds
it . (
f,
g)
= EUntill_0 (
f,
g,
R);
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)
by Lm44;
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 Lm45;
end;
:: deftheorem Def56 defines EUntill_ MODELC_1:def 56 :
for S being non empty set
for R being total Relation of S,S
for b3 being BinOp of (ModelSP S) holds
( b3 = EUntill_ R iff for f, g being set st f in ModelSP S & g in ModelSP S holds
b3 . (f,g) = EUntill_0 (f,g,R) );
:: deftheorem Def57 defines F_LABEL MODELC_1:def 57 :
for S being non empty set
for X being non empty Subset of (ModelSP S)
for s being set
for b4 being Subset of X holds
( b4 = F_LABEL (s,X) iff for x being set holds
( x in b4 iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) ) );
:: deftheorem Def58 defines Label_ MODELC_1:def 58 :
for S being non empty set
for X being non empty Subset of (ModelSP S)
for b3 being Function of S,(bool X) holds
( b3 = Label_ X iff for x being set st x in S holds
b3 . x = F_LABEL (x,X) );
:: deftheorem defines KModel MODELC_1:def 59 :
for S being non empty set
for S0 being Subset of S
for R being total Relation of S,S
for Prop being non empty Subset of (ModelSP S) holds KModel (R,S0,Prop) = KripkeStr(# S,S0,R,(Label_ Prop) #);
registration
let S be non
empty set ;
let S0 be
Subset of
S;
let R be
total Relation of
S,
S;
let Prop be non
empty Subset of
(ModelSP S);
cluster ModelSP the
carrier of
(KModel (R,S0,Prop)) -> non
empty Subset of
(Funcs ( the carrier of (KModel (R,S0,Prop)),BOOLEAN));
coherence
for b1 being Subset of (Funcs ( the carrier of (KModel (R,S0,Prop)),BOOLEAN)) st b1 = ModelSP the carrier of (KModel (R,S0,Prop)) holds
not b1 is empty
;
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);
func BASSModel (
R,
BASSIGN)
-> CTLModelStr equals
CTLModelStr(#
(ModelSP S),
BASSIGN,
(And_ S),
(Not_ S),
(EneXt_ R),
(EGlobal_ R),
(EUntill_ R) #);
coherence
CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #) is CTLModelStr
;
end;
:: deftheorem defines BASSModel MODELC_1:def 60 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S) holds BASSModel (R,BASSIGN) = CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #);
:: deftheorem Def61 defines |= MODELC_1:def 61 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for s being Element of S
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f iff (Fid (f,S)) . s = TRUE );
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem Def62 defines |= MODELC_1:def 62 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN))
for s being Element of S
for H being CTL-formula holds
( s,kai |= H iff s |= Evaluate (H,kai) );
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th25:
theorem
:: deftheorem Def63 defines PrePath MODELC_1:def 63 :
for S being non empty set
for R being total Relation of S,S
for s0 being Element of S
for pai being inf_path of R
for n being set holds
( ( n = 0 implies PrePath (n,s0,pai) = s0 ) & ( not n = 0 implies PrePath (n,s0,pai) = pai . (k_nat ((k_nat n) - 1)) ) );
theorem Th27:
theorem Th28:
:: deftheorem defines Pred MODELC_1:def 64 :
for S being non empty set
for R being total Relation of S,S
for H being Subset of S holds Pred (H,R) = { s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } ;
:: deftheorem defines SIGMA MODELC_1:def 65 :
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 : s |= f } ;
Lm46:
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 }
Lm47:
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
Lm48:
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
theorem
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;
func Tau (
T,
R,
BASSIGN)
-> Assign of
(BASSModel (R,BASSIGN)) means :
Def66:
for
s being
set st
s in S holds
(Fid (it,S)) . s = (chi (T,S)) . 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;
:: deftheorem Def66 defines Tau MODELC_1:def 66 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for T being Subset of S
for b5 being Assign of (BASSModel (R,BASSIGN)) holds
( b5 = Tau (T,R,BASSIGN) iff for s being set st s in S holds
(Fid (b5,S)) . s = (chi (T,S)) . s );
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
:: deftheorem defines Fax MODELC_1:def 67 :
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)) holds Fax (f,g) = f '&' (EX g);
theorem Th36:
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));
let G be
Subset of
S;
func SigFaxTau (
f,
G,
R,
BASSIGN)
-> Subset of
S equals
SIGMA (Fax (f,(Tau (G,R,BASSIGN))));
coherence
SIGMA (Fax (f,(Tau (G,R,BASSIGN)))) is Subset of S
;
end;
:: deftheorem defines SigFaxTau MODELC_1:def 68 :
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))
for G being Subset of S holds SigFaxTau (f,G,R,BASSIGN) = SIGMA (Fax (f,(Tau (G,R,BASSIGN))));
theorem Th37:
:: deftheorem Def69 defines PathShift MODELC_1:def 69 :
for S being non empty set
for R being total Relation of S,S
for pai being inf_path of R
for k being Element of NAT
for b5 being inf_path of R holds
( b5 = PathShift (pai,k) iff for n being Element of NAT holds b5 . n = pai . (n + k) );
:: deftheorem Def70 defines PathChange MODELC_1:def 70 :
for S being non empty set
for R being total Relation of S,S
for pai1, pai2 being inf_path of R
for n, k being Element of NAT holds
( ( n < k implies PathChange (pai1,pai2,k,n) = pai1 . n ) & ( not n < k implies PathChange (pai1,pai2,k,n) = pai2 . (n - k) ) );
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 ;
func PathConc (
pai1,
pai2,
k)
-> Function of
NAT,
S means :
Def71:
for
n being
Element of
NAT holds
it . n = PathChange (
pai1,
pai2,
k,
n);
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;
:: deftheorem Def71 defines PathConc MODELC_1:def 71 :
for S being non empty set
for R being total Relation of S,S
for pai1, pai2 being inf_path of R
for k being Element of NAT
for b6 being Function of NAT,S holds
( b6 = PathConc (pai1,pai2,k) iff for n being Element of NAT holds b6 . n = PathChange (pai1,pai2,k,n) );
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
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));
func TransEG f -> V224()
Function of
(bool S),
(bool S) means :
Def72:
for
G being
Subset of
S holds
it . G = SigFaxTau (
f,
G,
R,
BASSIGN);
existence
ex b1 being V224() 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 V224() 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 Def72 defines TransEG 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 being Assign of (BASSModel (R,BASSIGN))
for b5 being V224() Function of (bool S),(bool S) holds
( b5 = TransEG f iff for G being Subset of S holds b5 . G = SigFaxTau (f,G,R,BASSIGN) );
theorem Th42:
theorem
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,
h be
Assign of
(BASSModel (R,BASSIGN));
func Foax (
g,
f,
h)
-> Assign of
(BASSModel (R,BASSIGN)) equals
g 'or' (Fax (f,h));
coherence
g 'or' (Fax (f,h)) is Assign of (BASSModel (R,BASSIGN))
;
end;
:: deftheorem defines Foax MODELC_1:def 73 :
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, h being Assign of (BASSModel (R,BASSIGN)) holds Foax (g,f,h) = g 'or' (Fax (f,h));
theorem Th44:
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));
let H be
Subset of
S;
func SigFoaxTau (
g,
f,
H,
R,
BASSIGN)
-> Subset of
S equals
SIGMA (Foax (g,f,(Tau (H,R,BASSIGN))));
coherence
SIGMA (Foax (g,f,(Tau (H,R,BASSIGN)))) is Subset of S
;
end;
:: deftheorem defines SigFoaxTau MODELC_1:def 74 :
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)
theorem Th46:
theorem Th47:
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));
func TransEU (
f,
g)
-> V224()
Function of
(bool S),
(bool S) means :
Def75:
for
H being
Subset of
S holds
it . H = SigFoaxTau (
g,
f,
H,
R,
BASSIGN);
existence
ex b1 being V224() 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 V224() 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;
:: deftheorem Def75 defines TransEU MODELC_1:def 75 :
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 b6 being V224() Function of (bool S),(bool S) holds
( b6 = TransEU (f,g) iff for H being Subset of S holds b6 . H = SigFoaxTau (g,f,H,R,BASSIGN) );
theorem Th48:
theorem
theorem Th50:
theorem
theorem