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 :
:: deftheorem Def3 defines UnivF MODELC_1:def 3 :
:: deftheorem Def4 defines Castboolean MODELC_1:def 4 :
:: deftheorem Def5 defines CastBool MODELC_1:def 5 :
:: deftheorem defines atom. MODELC_1:def 6 :
:: deftheorem defines 'not' MODELC_1:def 7 :
:: deftheorem defines '&' MODELC_1:def 8 :
:: deftheorem defines EX MODELC_1:def 9 :
:: deftheorem defines EG MODELC_1:def 10 :
:: deftheorem defines EU MODELC_1:def 11 :
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 :
:: deftheorem Def13 defines CTL-formula-like MODELC_1:def 13 :
theorem Th1:
:: deftheorem Def14 defines atomic MODELC_1:def 14 :
:: deftheorem Def15 defines negative MODELC_1:def 15 :
:: deftheorem Def16 defines conjunctive MODELC_1:def 16 :
:: deftheorem Def17 defines ExistNext MODELC_1:def 17 :
:: deftheorem Def18 defines ExistGlobal MODELC_1:def 18 :
:: deftheorem Def19 defines ExistUntill MODELC_1:def 19 :
:: deftheorem defines 'or' MODELC_1:def 20 :
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 :
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 :
:: deftheorem Def23 defines the_right_argument_of MODELC_1:def 23 :
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 :
:: deftheorem defines atomic_WFF MODELC_1:def 25 :
:: deftheorem Def26 defines is-Evaluation-for MODELC_1:def 26 :
:: deftheorem Def27 defines is-PreEvaluation-for MODELC_1:def 27 :
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
Assignations 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
Not of
V . (h . (the_argument_of H)) if (
len H = n + 1 &
H is
negative )
the
And 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 Not of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is conjunctive implies the And 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 Not 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 And 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 Not 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 And 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 Not of V . (h . (the_argument_of H)) iff b1 = the And 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 Not 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 Not 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 Not 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 Not 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 And 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 And 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 And 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 And 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
Assignations 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
Not of
V . (h . (the_argument_of H)) ) & (
len H = n + 1 &
H is
conjunctive implies
GraftEval V,
Kai,
f,
h,
n,
H = the
And of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) ) & (
len H = n + 1 &
H is
ExistNext implies
GraftEval V,
Kai,
f,
h,
n,
H = the
EneXt of
V . (h . (the_argument_of H)) ) & (
len H = n + 1 &
H is
ExistGlobal implies
GraftEval V,
Kai,
f,
h,
n,
H = the
EGlobal of
V . (h . (the_argument_of H)) ) & (
len H = n + 1 &
H is
ExistUntill implies
GraftEval V,
Kai,
f,
h,
n,
H = the
EUntill of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) ) & (
len H < n + 1 implies
GraftEval V,
Kai,
f,
h,
n,
H = h . H ) & ( not
len H > n + 1 & ( not
len H = n + 1 or not
H is
atomic ) & ( not
len H = n + 1 or not
H is
negative ) & ( not
len H = n + 1 or not
H is
conjunctive ) & ( not
len H = n + 1 or not
H is
ExistNext ) & ( not
len H = n + 1 or not
H is
ExistGlobal ) & ( not
len H = n + 1 or not
H is
ExistUntill ) & not
len H < n + 1 implies
GraftEval V,
Kai,
f,
h,
n,
H = {} ) );
Lm24:
for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f being Function of CTL_WFF ,the Assignations of V holds f is-PreEvaluation-for 0 ,Kai
Lm25:
for n being Element of NAT
for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f being Function of CTL_WFF ,the Assignations 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 CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f being Function of CTL_WFF ,the Assignations 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 CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f1, f2 being Function of CTL_WFF ,the Assignations 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 CTLModelStr
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 Assignations of V st f is-PreEvaluation-for n,Kai
Lm29:
for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f being Function of CTL_WFF ,the Assignations 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 29 :
:: deftheorem Def30 defines CastEval MODELC_1:def 30 :
definition
let V be
CTLModelStr ;
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 Assignations 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 Assignations 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 Assignations 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 Assignations 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 31 :
Lm30:
for n being Element of NAT
for V being CTLModelStr
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 32 :
:: deftheorem defines 'not' MODELC_1:def 33 :
:: deftheorem defines '&' MODELC_1:def 34 :
:: deftheorem defines EX MODELC_1:def 35 :
:: deftheorem defines EG MODELC_1:def 36 :
:: deftheorem defines EU MODELC_1:def 37 :
:: deftheorem defines 'or' MODELC_1:def 38 :
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
Lm31:
for S being set
for R being Relation of , 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 , 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 ,
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 ,
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 39 :
:: deftheorem defines ModelSP MODELC_1:def 40 :
:: deftheorem Def41 defines Fid MODELC_1:def 41 :
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 42 :
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 43 :
:: deftheorem Def44 defines EneXt_univ MODELC_1:def 44 :
definition
let S be non
empty set ;
let R be
total Relation of ,;
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 45 :
Lm38:
for S being non empty set
for R being total Relation of , 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 ,
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 46 :
:: deftheorem Def47 defines EGlobal_univ MODELC_1:def 47 :
definition
let S be non
empty set ;
let R be
total Relation of ,;
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 48 :
Lm40:
for S being non empty set
for R being total Relation of , 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 ,
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 49 :
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 50 :
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 51 :
:: deftheorem Def52 defines EUntill_univ MODELC_1:def 52 :
definition
let S be non
empty set ;
let R be
total Relation of ,;
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 53 :
for
S being non
empty set for
R being
total Relation of ,
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 , 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 ,
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 ,;
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 54 :
:: deftheorem Def55 defines F_LABEL MODELC_1:def 55 :
:: deftheorem Def56 defines Label_ MODELC_1:def 56 :
:: deftheorem defines KModel MODELC_1:def 57 :
definition
let S be non
empty set ;
let R be
total Relation of ,;
let BASSIGN be non
empty Subset of ;
func CTLModel 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 CTLModel MODELC_1:def 58 :
:: deftheorem Def59 defines |= MODELC_1:def 59 :
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem Def60 defines |= MODELC_1:def 60 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th25:
theorem
:: deftheorem Def61 defines PrePath MODELC_1:def 61 :
theorem Th27:
theorem Th28:
:: deftheorem defines Pred MODELC_1:def 62 :
:: deftheorem defines SIGMA MODELC_1:def 63 :
Lm46:
for S being non empty set
for R being total Relation of ,
for BASSIGN being non empty Subset of
for f being Assign of (CTLModel 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 ,
for BASSIGN being non empty Subset of
for f, g being Assign of (CTLModel 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 ,;
let BASSIGN be non
empty Subset of ;
let T be
Subset of ;
func Tau T,
R,
BASSIGN -> Assign of
(CTLModel 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 (CTLModel 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 (CTLModel 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 64 :
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
:: deftheorem defines Fax MODELC_1:def 65 :
theorem Th36:
definition
let S be non
empty set ;
let R be
total Relation of ,;
let BASSIGN be non
empty Subset of ;
let f be
Assign of
(CTLModel R,BASSIGN);
let G be
Subset of ;
func SigFaxTau f,
G,
R,
BASSIGN -> Subset of
equals
SIGMA (Fax f,(Tau G,R,BASSIGN));
coherence
SIGMA (Fax f,(Tau G,R,BASSIGN)) is Subset of
;
end;
:: deftheorem defines SigFaxTau MODELC_1:def 66 :
theorem Th37:
:: deftheorem Def67 defines PathShift MODELC_1:def 67 :
:: deftheorem Def68 defines PathChange MODELC_1:def 68 :
definition
let S be non
empty set ;
let R be
total Relation of ,;
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 69 :
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
definition
let S be non
empty set ;
let R be
total Relation of ,;
let BASSIGN be non
empty Subset of ;
let f be
Assign of
(CTLModel R,BASSIGN);
func TransEG f -> V217()
Function of
bool S,
bool S means :
Def70:
for
G being
Subset of holds
it . G = SigFaxTau f,
G,
R,
BASSIGN;
existence
ex b1 being V217() Function of bool S, bool S st
for G being Subset of holds b1 . G = SigFaxTau f,G,R,BASSIGN
uniqueness
for b1, b2 being V217() Function of bool S, bool S st ( for G being Subset of holds b1 . G = SigFaxTau f,G,R,BASSIGN ) & ( for G being Subset of holds b2 . G = SigFaxTau f,G,R,BASSIGN ) holds
b1 = b2
end;
:: deftheorem Def70 defines TransEG MODELC_1:def 70 :
theorem Th42:
theorem
definition
let S be non
empty set ;
let R be
total Relation of ,;
let BASSIGN be non
empty Subset of ;
let f,
g,
h be
Assign of
(CTLModel R,BASSIGN);
func Foax g,
f,
h -> Assign of
(CTLModel R,BASSIGN) equals
g 'or' (Fax f,h);
coherence
g 'or' (Fax f,h) is Assign of (CTLModel R,BASSIGN)
;
end;
:: deftheorem defines Foax MODELC_1:def 71 :
theorem Th44:
definition
let S be non
empty set ;
let R be
total Relation of ,;
let BASSIGN be non
empty Subset of ;
let f,
g be
Assign of
(CTLModel R,BASSIGN);
let H be
Subset of ;
func SigFoaxTau g,
f,
H,
R,
BASSIGN -> Subset of
equals
SIGMA (Foax g,f,(Tau H,R,BASSIGN));
coherence
SIGMA (Foax g,f,(Tau H,R,BASSIGN)) is Subset of
;
end;
:: deftheorem defines SigFoaxTau MODELC_1:def 72 :
for
S being non
empty set for
R being
total Relation of ,
for
BASSIGN being non
empty Subset of
for
f,
g being
Assign of
(CTLModel R,BASSIGN) for
H being
Subset of 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 ,
for
BASSIGN being non
empty Subset of
for
f,
g being
Assign of
(CTLModel R,BASSIGN) for
H1,
H2 being
Subset of 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 ,;
let BASSIGN be non
empty Subset of ;
let f,
g be
Assign of
(CTLModel R,BASSIGN);
func TransEU f,
g -> V217()
Function of
bool S,
bool S means :
Def73:
for
H being
Subset of holds
it . H = SigFoaxTau g,
f,
H,
R,
BASSIGN;
existence
ex b1 being V217() Function of bool S, bool S st
for H being Subset of holds b1 . H = SigFoaxTau g,f,H,R,BASSIGN
uniqueness
for b1, b2 being V217() Function of bool S, bool S st ( for H being Subset of holds b1 . H = SigFoaxTau g,f,H,R,BASSIGN ) & ( for H being Subset of holds b2 . H = SigFoaxTau g,f,H,R,BASSIGN ) holds
b1 = b2
end;
:: deftheorem Def73 defines TransEU MODELC_1:def 73 :
theorem Th48:
theorem
theorem Th50:
theorem
theorem