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 Defx 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 Def30 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 :
Def31:
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 Def31 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 Def32 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 Def39 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 Def41 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 :
Def42:
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 Def42 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 Def43 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 Def44 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 :
Def45:
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 Def45 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 Def46 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 Def47 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 :
Def48:
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 Def48 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 Def49 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 :
Def50:
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 Def50 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 :
Def51:
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 Def51 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 Def52 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 :
Def53:
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 Def53 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 :
Def54:
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 Def54 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 Def55 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 Def56 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 Def59 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 Def60 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 Def61 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 :
Def64:
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 Def64 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 Def67 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 Def68 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 :
Def69:
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 Def69 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 :
Def70:
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 Def70 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 :
Def73:
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 Def73 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