:: Model Checking, Part {I}
:: by Kazuhisa Ishida
::
:: Received November 14, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

Lm1: for m, n, k being Nat st m < n & n <= k + 1 holds
m <= k

proof end;

definition
let x, S be set ;
let a be Element of S;
func k_id (x,S,a) -> Element of S equals :Def1: :: MODELC_1:def 1
x if x in S
otherwise a;
correctness
coherence
( ( x in S implies x is Element of S ) & ( not x in S implies a is Element of S ) )
;
consistency
for b1 being Element of S holds verum
;
;
end;

:: 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 ) );

definition
let x be set ;
func k_nat x -> Element of NAT equals :Def2: :: MODELC_1:def 2
x if x in NAT
otherwise 0 ;
correctness
coherence
( ( x in NAT implies x is Element of NAT ) & ( not x in NAT implies 0 is Element of NAT ) )
;
consistency
for b1 being Element of NAT holds verum
;
;
end;

:: 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 ) );

definition
let f be Function;
let x, a be set ;
func UnivF (x,f,a) -> set equals :Def3: :: MODELC_1:def 3
f . x if x in dom f
otherwise a;
correctness
coherence
( ( x in dom f implies f . x is set ) & ( not x in dom f implies a is set ) )
;
consistency
for b1 being set holds verum
;
;
end;

:: 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 ) );

definition
let a be set ;
func Castboolean a -> boolean set equals :Def4: :: MODELC_1:def 4
a if a is boolean set
otherwise FALSE ;
correctness
coherence
( ( a is boolean set implies a is boolean set ) & ( a is not boolean set implies FALSE is boolean set ) )
;
consistency
for b1 being boolean set holds verum
;
;
end;

:: 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 ) );

definition
let X, a be set ;
func CastBool (a,X) -> Subset of X equals :Def5: :: MODELC_1:def 5
a if a c= X
otherwise {} ;
correctness
coherence
( ( a c= X implies a is Subset of X ) & ( not a c= X implies {} is Subset of X ) )
;
consistency
for b1 being Subset of X holds verum
;
by XBOOLE_1:2;
end;

:: 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) = {} ) );

:: The operations to make CTL-formulae
definition
let n be Element of NAT ;
func atom. n -> FinSequence of NAT equals :: MODELC_1:def 6
<*(5 + n)*>;
coherence
<*(5 + n)*> is FinSequence of NAT
;
end;

:: deftheorem defines atom. MODELC_1:def 6 :
for n being Element of NAT holds atom. n = <*(5 + n)*>;

definition
let p be FinSequence of NAT ;
func 'not' p -> FinSequence of NAT equals :: MODELC_1:def 7
<*0*> ^ p;
coherence
<*0*> ^ p is FinSequence of NAT
;
let q be FinSequence of NAT ;
func p '&' q -> FinSequence of NAT equals :: MODELC_1:def 8
(<*1*> ^ p) ^ q;
coherence
(<*1*> ^ p) ^ q is FinSequence of NAT
;
end;

:: 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;

definition
let p be FinSequence of NAT ;
func EX p -> FinSequence of NAT equals :: MODELC_1:def 9
<*2*> ^ p;
coherence
<*2*> ^ p is FinSequence of NAT
;
func EG p -> FinSequence of NAT equals :: MODELC_1:def 10
<*3*> ^ p;
coherence
<*3*> ^ p is FinSequence of NAT
;
let q be FinSequence of NAT ;
func p EU q -> FinSequence of NAT equals :: MODELC_1:def 11
(<*4*> ^ p) ^ q;
coherence
(<*4*> ^ p) ^ q is FinSequence of NAT
;
end;

:: 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)

proof end;

:: The set of all well formed formulae of CTL-language
definition
func CTL_WFF -> non empty set means :Def12: :: MODELC_1:def 12
( ( 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 ) )
proof end;
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
proof end;
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 ) ) );

definition
let IT be FinSequence of NAT ;
attr IT is CTL-formula-like means :Def13: :: MODELC_1:def 13
IT is Element of CTL_WFF ;
end;

:: 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 );

registration
cluster Relation-like NAT -defined NAT -valued Function-like FinSequence-like CTL-formula-like for FinSequence of NAT ;
existence
ex b1 being FinSequence of NAT st b1 is CTL-formula-like
proof end;
end;

definition
mode CTL-formula is CTL-formula-like FinSequence of NAT ;
end;

theorem Th1: :: MODELC_1:1
for a being set holds
( a is CTL-formula iff a in CTL_WFF )
proof end;

registration
let n be Element of NAT ;
cluster atom. n -> CTL-formula-like ;
coherence
atom. n is CTL-formula-like
proof end;
end;

registration
let H be CTL-formula;
cluster 'not' H -> CTL-formula-like ;
coherence
'not' H is CTL-formula-like
proof end;
cluster EX H -> CTL-formula-like ;
coherence
EX H is CTL-formula-like
proof end;
cluster EG H -> CTL-formula-like ;
coherence
EG H is CTL-formula-like
proof end;
let G be CTL-formula;
cluster H '&' G -> CTL-formula-like ;
coherence
H '&' G is CTL-formula-like
proof end;
cluster H EU G -> CTL-formula-like ;
coherence
H EU G is CTL-formula-like
proof end;
end;

definition
let H be CTL-formula;
attr H is atomic means :Def14: :: MODELC_1:def 14
ex n being Element of NAT st H = atom. n;
attr H is negative means :Def15: :: MODELC_1:def 15
ex H1 being CTL-formula st H = 'not' H1;
attr H is conjunctive means :Def16: :: MODELC_1:def 16
ex F, G being CTL-formula st H = F '&' G;
attr H is ExistNext means :Def17: :: MODELC_1:def 17
ex H1 being CTL-formula st H = EX H1;
attr H is ExistGlobal means :Def18: :: MODELC_1:def 18
ex H1 being CTL-formula st H = EG H1;
attr H is ExistUntill means :Def19: :: MODELC_1:def 19
ex F, G being CTL-formula st H = F EU G;
end;

:: 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 );

definition
let F, G be CTL-formula;
func F 'or' G -> CTL-formula equals :: MODELC_1:def 20
'not' (('not' F) '&' ('not' G));
coherence
'not' (('not' F) '&' ('not' G)) is CTL-formula
;
end;

:: deftheorem defines 'or' MODELC_1:def 20 :
for F, G being CTL-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));

theorem Th2: :: MODELC_1:2
for H being CTL-formula holds
( H is atomic or H is negative or H is conjunctive or H is ExistNext or H is ExistGlobal or H is ExistUntill )
proof end;

Lm3: for H being CTL-formula st H is negative holds
H . 1 = 0

proof end;

Lm4: for H being CTL-formula st H is conjunctive holds
H . 1 = 1

proof end;

Lm5: for H being CTL-formula st H is ExistNext holds
H . 1 = 2

proof end;

Lm6: for H being CTL-formula st H is ExistGlobal holds
H . 1 = 3

proof end;

Lm7: for H being CTL-formula st H is ExistUntill holds
H . 1 = 4

proof end;

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 )

proof end;

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 ) )

proof end;

Lm10: for H being CTL-formula holds 1 <= len H
proof end;

Lm11: for H, F being CTL-formula
for sq being FinSequence st H = F ^ sq holds
H = F

proof end;

Lm12: for H, G, H1, G1 being CTL-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )

proof end;

Lm13: for H, G, H1, G1 being CTL-formula st H EU G = H1 EU G1 holds
( H = H1 & G = G1 )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

definition
let H be CTL-formula;
assume A1: ( H is negative or H is ExistNext or H is ExistGlobal ) ;
func the_argument_of H -> CTL-formula means :Def21: :: MODELC_1:def 21
'not' it = H if H is negative
EX it = H if H is ExistNext
otherwise EG it = H;
existence
( ( H is negative implies ex b1 being CTL-formula st 'not' b1 = H ) & ( H is ExistNext implies ex b1 being CTL-formula st EX b1 = H ) & ( not H is negative & not H is ExistNext implies ex b1 being CTL-formula st EG b1 = H ) )
by A1, Def15, Def17, Def18;
uniqueness
for b1, b2 being CTL-formula holds
( ( H is negative & 'not' b1 = H & 'not' b2 = H implies b1 = b2 ) & ( H is ExistNext & EX b1 = H & EX b2 = H implies b1 = b2 ) & ( not H is negative & not H is ExistNext & EG b1 = H & EG b2 = H implies b1 = b2 ) )
by FINSEQ_1:33;
consistency
for b1 being CTL-formula st H is negative & H is ExistNext holds
( 'not' b1 = H iff EX b1 = H )
by Lm15;
end;

:: 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: :: MODELC_1:def 22
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: :: MODELC_1:def 23
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 ) )
proof end;
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)

proof end;

Lm20: for H being CTL-formula st H is conjunctive holds
H = (the_left_argument_of H) '&' (the_right_argument_of H)

proof end;

Lm21: for H being CTL-formula st H is ExistUntill holds
H = (the_left_argument_of H) EU (the_right_argument_of H)

proof end;

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

proof end;

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 )

proof end;

definition
let x be set ;
func CastCTLformula x -> CTL-formula equals :Def24: :: MODELC_1:def 24
x if x in CTL_WFF
otherwise atom. 0;
correctness
coherence
( ( x in CTL_WFF implies x is CTL-formula ) & ( not x in CTL_WFF implies atom. 0 is CTL-formula ) )
;
consistency
for b1 being CTL-formula holds verum
;
by Th1;
end;

:: 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 ) );

::***************************************************
::**
::** definition of Kripke structure & CTL model structure.
::**
::****************************************************
definition
let Prop be set ;
attr c2 is strict ;
struct KripkeStr over Prop -> RelStr ;
aggr KripkeStr(# carrier, Starts, InternalRel, Label #) -> KripkeStr over Prop;
sel Starts c2 -> Subset of the carrier of c2;
sel Label c2 -> Function of the carrier of c2,(bool Prop);
end;

definition
attr c1 is strict ;
struct CTLModelStr -> ComplULattStr ;
aggr CTLModelStr(# carrier, BasicAssign, L_meet, Compl, EneXt, EGlobal, EUntill #) -> CTLModelStr ;
sel BasicAssign c1 -> Subset of the carrier of c1;
sel EneXt c1 -> UnOp of the carrier of c1;
sel EGlobal c1 -> UnOp of the carrier of c1;
sel EUntill c1 -> BinOp of the carrier of c1;
end;

definition
let V be CTLModelStr ;
mode Assign of V is Element of the carrier of V;
end;

:: Preparation to define semantics for CTL-language
:: definition of evaluate function of CTL
definition
func atomic_WFF -> Subset of CTL_WFF equals :: MODELC_1:def 25
{ x where x is CTL-formula : x is atomic } ;
correctness
coherence
{ x where x is CTL-formula : x is atomic } is Subset of CTL_WFF
;
proof end;
end;

:: deftheorem defines atomic_WFF MODELC_1:def 25 :
atomic_WFF = { x where x is CTL-formula : x is atomic } ;

definition
let V be CTLModelStr ;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let f be Function of CTL_WFF, the carrier of V;
pred f is-Evaluation-for Kai means :Def26: :: MODELC_1:def 26
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))) ) );
end;

:: 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))) ) ) );

definition
let V be CTLModelStr ;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let f be Function of CTL_WFF, the carrier of V;
let n be Element of NAT ;
pred f is-PreEvaluation-for n,Kai means :Def27: :: MODELC_1:def 27
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))) ) );
end;

:: 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: :: MODELC_1:def 28
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) = {} ) );

definition
let C be CTLModelStr ;
attr C is with_basic means :Def29: :: MODELC_1:def 29
not the BasicAssign of C is empty ;
end;

:: 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 :: MODELC_1:def 30
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 #);

registration
cluster TrivialCTLModel -> non empty strict with_basic ;
coherence
( TrivialCTLModel is with_basic & TrivialCTLModel is strict & not TrivialCTLModel is empty )
proof end;
end;

registration
cluster non empty for CTLModelStr ;
existence
not for b1 being CTLModelStr holds b1 is empty
proof end;
end;

registration
cluster non empty with_basic for CTLModelStr ;
existence
ex b1 being non empty CTLModelStr st b1 is with_basic
proof end;
end;

definition
mode CTLModel is non empty with_basic CTLModelStr ;
end;

registration
let C be CTLModel;
cluster the BasicAssign of C -> non empty ;
coherence
not the BasicAssign of C is empty
by Def29;
end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

definition
let V be CTLModel;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let n be Element of NAT ;
func EvalSet (V,Kai,n) -> non empty set equals :: MODELC_1:def 31
{ h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;
correctness
coherence
{ h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } is non empty set
;
proof end;
end;

:: 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 } ;

definition
let V be CTLModel;
let v0 be Element of the carrier of V;
let x be set ;
func CastEval (V,x,v0) -> Function of CTL_WFF, the carrier of V equals :Def32: :: MODELC_1:def 32
x if x in Funcs (CTL_WFF, the carrier of V)
otherwise CTL_WFF --> v0;
correctness
coherence
( ( x in Funcs (CTL_WFF, the carrier of V) implies x is Function of CTL_WFF, the carrier of V ) & ( not x in Funcs (CTL_WFF, the carrier of V) implies CTL_WFF --> v0 is Function of CTL_WFF, the carrier of V ) )
;
consistency
for b1 being Function of CTL_WFF, the carrier of V holds verum
;
by FUNCT_2:66;
end;

:: 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: :: MODELC_1:def 33
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) ) )
proof end;
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
proof end;
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)

proof end;

theorem Th3: :: MODELC_1:3
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V ex f being Function of CTL_WFF, the carrier of V st f is-Evaluation-for Kai
proof end;

theorem Th4: :: MODELC_1:4
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-Evaluation-for Kai & f2 is-Evaluation-for Kai holds
f1 = f2
proof end;

definition
let V be CTLModel;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let H be CTL-formula;
func Evaluate (H,Kai) -> Assign of V means :Def34: :: MODELC_1:def 34
ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & it = f . H );
existence
ex b1 being Assign of V ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b1 = f . H )
proof end;
uniqueness
for b1, b2 being Assign of V st ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b1 = f . H ) & ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b2 = f . H ) holds
b1 = b2
by Th4;
end;

:: 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 ) );

notation
let V be CTLModel;
let f be Assign of V;
synonym 'not' f for f ` ;
let g be Assign of V;
synonym f '&' g for f "/\" g;
end;

definition
let V be CTLModel;
let f be Assign of V;
func EX f -> Assign of V equals :: MODELC_1:def 35
the EneXt of V . f;
correctness
coherence
the EneXt of V . f is Assign of V
;
;
func EG f -> Assign of V equals :: MODELC_1:def 36
the EGlobal of V . f;
correctness
coherence
the EGlobal of V . f is Assign of V
;
;
end;

:: deftheorem defines EX MODELC_1:def 35 :
for V being CTLModel
for f being Assign of V holds EX f = the EneXt of V . f;

:: deftheorem defines EG MODELC_1:def 36 :
for V being CTLModel
for f being Assign of V holds EG f = the EGlobal of V . f;

definition
let V be CTLModel;
let f, g be Assign of V;
func f EU g -> Assign of V equals :: MODELC_1:def 37
the EUntill of V . (f,g);
correctness
coherence
the EUntill of V . (f,g) is Assign of V
;
;
func f 'or' g -> Assign of V equals :: MODELC_1:def 38
'not' (('not' f) '&' ('not' g));
correctness
coherence
'not' (('not' f) '&' ('not' g)) is Assign of V
;
;
end;

:: deftheorem defines EU MODELC_1:def 37 :
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 38 :
for V being CTLModel
for f, g being Assign of V holds f 'or' g = 'not' (('not' f) '&' ('not' g));

::Some properties of evaluate function of CTL
theorem Th5: :: MODELC_1:5
for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))
proof end;

theorem Th6: :: MODELC_1:6
for H1, H2 being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 '&' H2),Kai) = (Evaluate (H1,Kai)) '&' (Evaluate (H2,Kai))
proof end;

theorem Th7: :: MODELC_1:7
for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EX H),Kai) = EX (Evaluate (H,Kai))
proof end;

theorem Th8: :: MODELC_1:8
for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai))
proof end;

theorem Th9: :: MODELC_1:9
for H1, H2 being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai))
proof end;

theorem Th10: :: MODELC_1:10
for H1, H2 being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))
proof end;

notation
let f be Function;
let n be Nat;
synonym f |** n for iter (f,n);
end;

definition
let S be set ;
let f be Function of S,S;
let n be Nat;
:: original: |**
redefine func f |** n -> Function of S,S;
coherence
f |** n is Function of S,S
proof end;
end;

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 )

proof end;

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

proof end;

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

proof end;

:: scheme for path with condition F
scheme :: MODELC_1:sch 1
ExistPath{ F1() -> non empty set , F2() -> total Relation of F1(),F1(), F3() -> Element of F1(), F4( Element of F1()) -> set } :
ex f being Function of NAT,F1() st
( f . 0 = F3() & ( for n being Element of NAT holds
( [(f . n),(f . (n + 1))] in F2() & f . (n + 1) in F4((f . n)) ) ) )
provided
A1: for s being Element of F1() holds (Im (F2(),s)) /\ F4(s) is non empty Subset of F1()
proof end;

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 ) )

proof end;

:: definition of infinity path
definition
let S be non empty set ;
let R be total Relation of S,S;
mode inf_path of R -> Function of NAT,S means :Def39: :: MODELC_1:def 39
for n being Element of NAT holds [(it . n),(it . (n + 1))] in R;
existence
ex b1 being Function of NAT,S st
for n being Element of NAT holds [(b1 . n),(b1 . (n + 1))] in R
proof end;
end;

:: deftheorem Def39 defines inf_path MODELC_1:def 39 :
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 );

::definition of concrete object of CTL model
definition
let S be non empty set ;
func ModelSP S -> set equals :: MODELC_1:def 40
Funcs (S,BOOLEAN);
correctness
coherence
Funcs (S,BOOLEAN) is set
;
;
end;

:: deftheorem defines ModelSP MODELC_1:def 40 :
for S being non empty set holds ModelSP S = Funcs (S,BOOLEAN);

registration
let S be non empty set ;
cluster ModelSP S -> non empty ;
coherence
not ModelSP S is empty
;
end;

:: definition Fid:ModelSP(S) -> Function of S,BOOLEAN
definition
let S be non empty set ;
let f be set ;
func Fid (f,S) -> Function of S,BOOLEAN equals :Def41: :: MODELC_1:def 41
f if f in ModelSP S
otherwise S --> FALSE;
correctness
coherence
( ( f in ModelSP S implies f is Function of S,BOOLEAN ) & ( not f in ModelSP S implies S --> FALSE is Function of S,BOOLEAN ) )
;
consistency
for b1 being Function of S,BOOLEAN holds verum
;
by FUNCT_2:66;
end;

:: deftheorem Def41 defines Fid MODELC_1:def 41 :
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;

::schemes for existence & uniqueness of 1 Operand functor
scheme :: MODELC_1:sch 2
Func1EX{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3( set , Function of F1(),BOOLEAN) -> boolean set } :
ex g being set st
( g in ModelSP F1() & ( for s being set st s in F1() holds
( F3(s,F2()) = TRUE iff (Fid (g,F1())) . s = TRUE ) ) )
proof end;

scheme :: MODELC_1:sch 3
Func1Unique{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3( set , Function of F1(),BOOLEAN) -> boolean set } :
for g1, g2 being set st g1 in ModelSP F1() & ( for s being set st s in F1() holds
( F3(s,F2()) = TRUE iff (Fid (g1,F1())) . s = TRUE ) ) & g2 in ModelSP F1() & ( for s being set st s in F1() holds
( F3(s,F2()) = TRUE iff (Fid (g2,F1())) . s = TRUE ) ) holds
g1 = g2
proof end;

::schemes for existence & uniqueness of Unary Operation
scheme :: MODELC_1:sch 4
UnOpEX{ F1() -> non empty set , F2( set ) -> Element of F1() } :
ex o being UnOp of F1() st
for f being set st f in F1() holds
o . f = F2(f)
proof end;

scheme :: MODELC_1:sch 5
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
proof end;

::schemes for existence & uniqueness of 2 Operands functor .
scheme :: MODELC_1:sch 6
Func2EX{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3() -> Function of F1(),BOOLEAN, F4( set , Function of F1(),BOOLEAN, Function of F1(),BOOLEAN) -> boolean set } :
ex h being set st
( h in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h,F1())) . s = TRUE ) ) )
proof end;

scheme :: MODELC_1:sch 7
Func2Unique{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3() -> Function of F1(),BOOLEAN, F4( set , Function of F1(),BOOLEAN, Function of F1(),BOOLEAN) -> boolean set } :
for h1, h2 being set st h1 in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h1,F1())) . s = TRUE ) ) & h2 in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h2,F1())) . s = TRUE ) ) holds
h1 = h2
proof end;

:: definition of Not_ unary operation of Model Space.
definition
let S be non empty set ;
let f be set ;
func Not_0 (f,S) -> Element of ModelSP S means :Def42: :: MODELC_1:def 42
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 )
proof end;
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
proof end;
end;

:: deftheorem Def42 defines Not_0 MODELC_1:def 42 :
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
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

proof end;

definition
let S be non empty set ;
func Not_ S -> UnOp of (ModelSP S) means :Def43: :: MODELC_1:def 43
for f being set st f in ModelSP S holds
it . f = Not_0 (f,S);
existence
ex b1 being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
b1 . f = Not_0 (f,S)
proof end;
uniqueness
for b1, b2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
b1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP S holds
b2 . f = Not_0 (f,S) ) holds
b1 = b2
by Lm36;
end;

:: deftheorem Def43 defines Not_ MODELC_1:def 43 :
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) );

:: definition of EneXt_ unary operation of Model Space.
definition
let S be non empty set ;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be set ;
func EneXt_univ (x,f,R) -> Element of BOOLEAN equals :Def44: :: MODELC_1:def 44
TRUE if ( x in S & ex pai being inf_path of R st
( pai . 0 = x & f . (pai . 1) = TRUE ) )
otherwise FALSE ;
correctness
coherence
( ( x in S & ex pai being inf_path of R st
( pai . 0 = x & f . (pai . 1) = TRUE ) implies TRUE is Element of BOOLEAN ) & ( ( not x in S or for pai being inf_path of R holds
( not pai . 0 = x or not f . (pai . 1) = TRUE ) ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def44 defines EneXt_univ MODELC_1:def 44 :
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: :: MODELC_1:def 45
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 )
proof end;
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
proof end;
end;

:: deftheorem Def45 defines EneXt_0 MODELC_1:def 45 :
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 ) );

Lm37: for S being non empty set
for R being total Relation of S,S
for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
o1 . f = EneXt_0 (f,R) ) & ( for f being set st f in ModelSP S holds
o2 . f = EneXt_0 (f,R) ) holds
o1 = o2

proof end;

definition
let S be non empty set ;
let R be total Relation of S,S;
func EneXt_ R -> UnOp of (ModelSP S) means :Def46: :: MODELC_1:def 46
for f being set st f in ModelSP S holds
it . f = EneXt_0 (f,R);
existence
ex b1 being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
b1 . f = EneXt_0 (f,R)
proof end;
uniqueness
for b1, b2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
b1 . f = EneXt_0 (f,R) ) & ( for f being set st f in ModelSP S holds
b2 . f = EneXt_0 (f,R) ) holds
b1 = b2
by Lm37;
end;

:: deftheorem Def46 defines EneXt_ MODELC_1:def 46 :
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) );

:: definition of EGlobal_ unary operation of Model Space.
definition
let S be non empty set ;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be set ;
func EGlobal_univ (x,f,R) -> Element of BOOLEAN equals :Def47: :: MODELC_1:def 47
TRUE if ( 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 ) ) )
otherwise FALSE ;
correctness
coherence
( ( 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 TRUE is Element of BOOLEAN ) & ( ( 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 FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def47 defines EGlobal_univ MODELC_1:def 47 :
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: :: MODELC_1:def 48
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 )
proof end;
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
proof end;
end;

:: deftheorem Def48 defines EGlobal_0 MODELC_1:def 48 :
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 ) );

Lm38: for S being non empty set
for R being total Relation of S,S
for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
o1 . f = EGlobal_0 (f,R) ) & ( for f being set st f in ModelSP S holds
o2 . f = EGlobal_0 (f,R) ) holds
o1 = o2

proof end;

definition
let S be non empty set ;
let R be total Relation of S,S;
func EGlobal_ R -> UnOp of (ModelSP S) means :Def49: :: MODELC_1:def 49
for f being set st f in ModelSP S holds
it . f = EGlobal_0 (f,R);
existence
ex b1 being UnOp of (ModelSP S) st
for f being set st f in ModelSP S holds
b1 . f = EGlobal_0 (f,R)
proof end;
uniqueness
for b1, b2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds
b1 . f = EGlobal_0 (f,R) ) & ( for f being set st f in ModelSP S holds
b2 . f = EGlobal_0 (f,R) ) holds
b1 = b2
by Lm38;
end;

:: deftheorem Def49 defines EGlobal_ MODELC_1:def 49 :
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 of And_ Binary Operation of Model Space.
definition
let S be non empty set ;
let f, g be set ;
func And_0 (f,g,S) -> Element of ModelSP S means :Def50: :: MODELC_1:def 50
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 )
proof end;
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
proof end;
end;

:: deftheorem Def50 defines And_0 MODELC_1:def 50 :
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 ) );

Lm39: for S being non empty set
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = And_0 (f,g,S) ) holds
o1 = o2

proof end;

definition
let S be non empty set ;
func And_ S -> BinOp of (ModelSP S) means :Def51: :: MODELC_1:def 51
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)
proof end;
uniqueness
for b1, b2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b2 . (f,g) = And_0 (f,g,S) ) holds
b1 = b2
by Lm39;
end;

:: deftheorem Def51 defines And_ MODELC_1:def 51 :
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) );

:: definition of EUntill_ Binary Operation of Model Space.
definition
let S be non empty set ;
let R be total Relation of S,S;
let f, g be Function of S,BOOLEAN;
let x be set ;
func EUntill_univ (x,f,g,R) -> Element of BOOLEAN equals :Def52: :: MODELC_1:def 52
TRUE if ( 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 ) ) )
otherwise FALSE ;
correctness
coherence
( ( 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 TRUE is Element of BOOLEAN ) & ( ( 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 FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def52 defines EUntill_univ MODELC_1:def 52 :
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: :: MODELC_1:def 53
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 )
proof end;
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
proof end;
end;

:: deftheorem Def53 defines EUntill_0 MODELC_1:def 53 :
for S being non empty set
for R being total Relation of S,S
for f, g being set
for b5 being Element of ModelSP S holds
( b5 = EUntill_0 (f,g,R) iff for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b5,S)) . s = TRUE ) );

Lm40: for S being non empty set
for R being total Relation of S,S
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2

proof end;

definition
let S be non empty set ;
let R be total Relation of S,S;
func EUntill_ R -> BinOp of (ModelSP S) means :Def54: :: MODELC_1:def 54
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)
proof end;
uniqueness
for b1, b2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
b2 . (f,g) = EUntill_0 (f,g,R) ) holds
b1 = b2
by Lm40;
end;

:: deftheorem Def54 defines EUntill_ MODELC_1:def 54 :
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) );

:: definition of concrete object of CTL model by ModelSP
definition
let S be non empty set ;
let X be non empty Subset of (ModelSP S);
let s be set ;
func F_LABEL (s,X) -> Subset of X means :Def55: :: MODELC_1:def 55
for x being set holds
( x in it iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) );
existence
ex b1 being Subset of X st
for x being set holds
( x in b1 iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) )
proof end;
uniqueness
for b1, b2 being Subset of X st ( for x being set holds
( x in b1 iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def55 defines F_LABEL MODELC_1:def 55 :
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 ) ) ) );

definition
let S be non empty set ;
let X be non empty Subset of (ModelSP S);
func Label_ X -> Function of S,(bool X) means :Def56: :: MODELC_1:def 56
for x being set st x in S holds
it . x = F_LABEL (x,X);
existence
ex b1 being Function of S,(bool X) st
for x being set st x in S holds
b1 . x = F_LABEL (x,X)
proof end;
uniqueness
for b1, b2 being Function of S,(bool X) st ( for x being set st x in S holds
b1 . x = F_LABEL (x,X) ) & ( for x being set st x in S holds
b2 . x = F_LABEL (x,X) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def56 defines Label_ MODELC_1:def 56 :
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) );

definition
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);
func KModel (R,S0,Prop) -> KripkeStr over Prop equals :: MODELC_1:def 57
KripkeStr(# S,S0,R,(Label_ Prop) #);
coherence
KripkeStr(# S,S0,R,(Label_ Prop) #) is KripkeStr over Prop
;
end;

:: deftheorem defines KModel MODELC_1:def 57 :
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 the carrier of (KModel (R,S0,Prop)) -> non empty ;
coherence
not the carrier of (KModel (R,S0,Prop)) is empty
;
end;

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 for 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 :: MODELC_1:def 58
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 58 :
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) #);

registration
let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
cluster BASSModel (R,BASSIGN) -> non empty with_basic ;
coherence
( BASSModel (R,BASSIGN) is with_basic & not BASSModel (R,BASSIGN) is empty )
proof end;
end;

:: definition of correctness of Assign of BASSModel(R,BASSIGN)
definition
let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let s be Element of S;
let f be Assign of (BASSModel (R,BASSIGN));
pred s |= f means :Def59: :: MODELC_1:def 59
(Fid (f,S)) . s = TRUE ;
end;

:: deftheorem Def59 defines |= MODELC_1:def 59 :
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 );

notation
let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let s be Element of S;
let f be Assign of (BASSModel (R,BASSIGN));
antonym s |/= f for s |= f;
end;

theorem Th11: :: MODELC_1:11
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
proof end;

theorem Th12: :: MODELC_1:12
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= 'not' f iff s |/= f )
proof end;

theorem Th13: :: MODELC_1:13
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f '&' g iff ( s |= f & s |= g ) )
proof end;

theorem Th14: :: MODELC_1:14
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )
proof end;

theorem Th15: :: MODELC_1:15
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )
proof end;

theorem Th16: :: MODELC_1:16
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f EU g iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g ) ) )
proof end;

theorem Th17: :: MODELC_1:17
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
proof end;

:: definition of correctness of CTL-formula & its basic properties.
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 kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN));
let s be Element of S;
let H be CTL-formula;
pred s,kai |= H means :Def60: :: MODELC_1:def 60
s |= Evaluate (H,kai);
end;

:: deftheorem Def60 defines |= 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)
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) );

notation
let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN));
let s be Element of S;
let H be CTL-formula;
antonym s,kai |/= H for s,kai |= H;
end;

theorem :: MODELC_1:18
for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
proof end;

theorem :: MODELC_1:19
for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= 'not' H iff s,kai |/= H )
proof end;

theorem :: MODELC_1:20
for H1, H2 being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 '&' H2 iff ( s,kai |= H1 & s,kai |= H2 ) )
proof end;

theorem :: MODELC_1:21
for H1, H2 being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
proof end;

theorem :: MODELC_1:22
for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
proof end;

theorem :: MODELC_1:23
for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
proof end;

theorem :: MODELC_1:24
for H1, H2 being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
proof end;

::Some basic theorems for external Mizar files.
theorem Th25: :: MODELC_1:25
for S being non empty set
for R being total Relation of S,S
for s0 being Element of S ex pai being inf_path of R st pai . 0 = s0
proof end;

theorem :: MODELC_1:26
for S being non empty set
for R being Relation of S,S holds
( R is total iff for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ) by Lm31, Lm32;

::*************
::
::Verification of the basic algorithm
:: for Model checking based on CTL.
::
::the basic algorithm is solver to get
:: {s where s is Element of S: s,kai|=H}
::
::*************
definition
let S be non empty set ;
let R be total Relation of S,S;
let s0 be Element of S;
let pai be inf_path of R;
let n be set ;
func PrePath (n,s0,pai) -> Element of S equals :Def61: :: MODELC_1:def 61
s0 if n = 0
otherwise pai . (k_nat ((k_nat n) - 1));
correctness
coherence
( ( n = 0 implies s0 is Element of S ) & ( not n = 0 implies pai . (k_nat ((k_nat n) - 1)) is Element of S ) )
;
consistency
for b1 being Element of S holds verum
;
;
end;

:: deftheorem Def61 defines PrePath MODELC_1:def 61 :
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: :: MODELC_1:27
for S being non empty set
for R being total Relation of S,S
for s0, s1 being Element of S st [s0,s1] in R holds
ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
proof end;

theorem Th28: :: MODELC_1:28
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= EX f iff ex s1 being Element of S st
( [s,s1] in R & s1 |= f ) )
proof end;

:: definition of predecessor
definition
let S be non empty set ;
let R be total Relation of S,S;
let H be Subset of S;
func Pred (H,R) -> Subset of S equals :: MODELC_1:def 62
{ s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R )
}
;
coherence
{ s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R )
}
is Subset of S
proof end;
end;

:: deftheorem defines Pred MODELC_1:def 62 :
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 )
}
;

:: definition of SIGMA
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 SIGMA f -> Subset of S equals :: MODELC_1:def 63
{ s where s is Element of S : s |= f } ;
correctness
coherence
{ s where s is Element of S : s |= f } is Subset of S
;
proof end;
end;

:: deftheorem defines SIGMA MODELC_1:def 63 :
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 } ;

Lm41: for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }

proof end;

Lm42: for X being non empty set
for f, g being Function of X,BOOLEAN st { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } holds
f = g

proof end;

Lm43: for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds
f = g

proof end;

:: SIGMA is one to one.
theorem :: MODELC_1:29
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 SIGMA f = SIGMA g holds
f = g
proof end;

:: definition of Tau (inverse of SIGMA).
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: :: MODELC_1:def 64
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
proof end;
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
proof end;
end;

:: deftheorem Def64 defines Tau MODELC_1:def 64 :
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 );

:: Tau is one to one.
theorem :: MODELC_1:30
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for T1, T2 being Subset of S st Tau (T1,R,BASSIGN) = Tau (T2,R,BASSIGN) holds
T1 = T2
proof end;

:: Tau is on to.
theorem Th31: :: MODELC_1:31
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 Tau ((SIGMA f),R,BASSIGN) = f
proof end;

:: SIGMA is on to.
theorem Th32: :: MODELC_1:32
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 holds SIGMA (Tau (T,R,BASSIGN)) = T
proof end;

:: SIGMA is homomorphism .
theorem Th33: :: MODELC_1:33
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
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )
proof end;

:: Tau is monotonic.
theorem Th34: :: MODELC_1:34
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for G1, G2 being Subset of S st G1 c= G2 holds
for s being Element of S st s |= Tau (G1,R,BASSIGN) holds
s |= Tau (G2,R,BASSIGN)
proof end;

:: SIGMA is monotonic.
theorem Th35: :: MODELC_1:35
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f1, f2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= f1 holds
s |= f2 ) holds
SIGMA f1 c= SIGMA f2
proof end;

:: theorems for translation
:: problem of
:: (1)find status s st s |= EG(f)
:: (2)find status s st s |= f EU g
:: to "find fixpoint of some function of bool S -> bool S".
:: definition Fax(f,*):carrier ->carrier
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 Fax (f,g) -> Assign of (BASSModel (R,BASSIGN)) equals :: MODELC_1:def 65
f '&' (EX g);
correctness
coherence
f '&' (EX g) is Assign of (BASSModel (R,BASSIGN))
;
;
end;

:: deftheorem defines Fax 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, g being Assign of (BASSModel (R,BASSIGN)) holds Fax (f,g) = f '&' (EX g);

:: Fax(f,*) is monotonic.
theorem Th36: :: MODELC_1:36
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, g1, g2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= g1 holds
s |= g2 ) holds
for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2)
proof end;

::commutative
:: Fax(f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFaxTau(f,*)
::
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 :: MODELC_1:def 66
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 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 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))));

:: SigFaxTau(f,*) is monotonic.
theorem Th37: :: MODELC_1:37
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 G1, G2 being Subset of S st G1 c= G2 holds
SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)
proof end;

:: Some tools to treat path.
definition
let S be non empty set ;
let R be total Relation of S,S;
let pai be inf_path of R;
let k be Element of NAT ;
func PathShift (pai,k) -> inf_path of R means :Def67: :: MODELC_1:def 67
for n being Element of NAT holds it . n = pai . (n + k);
existence
ex b1 being inf_path of R st
for n being Element of NAT holds b1 . n = pai . (n + k)
proof end;
uniqueness
for b1, b2 being inf_path of R st ( for n being Element of NAT holds b1 . n = pai . (n + k) ) & ( for n being Element of NAT holds b2 . n = pai . (n + k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def67 defines PathShift MODELC_1:def 67 :
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) );

definition
let S be non empty set ;
let R be total Relation of S,S;
let pai1, pai2 be inf_path of R;
let n, k be Element of NAT ;
func PathChange (pai1,pai2,k,n) -> set equals :Def68: :: MODELC_1:def 68
pai1 . n if n < k
otherwise pai2 . (n - k);
correctness
coherence
( ( n < k implies pai1 . n is set ) & ( not n < k implies pai2 . (n - k) is set ) )
;
consistency
for b1 being set holds verum
;
;
end;

:: deftheorem Def68 defines PathChange MODELC_1:def 68 :
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: :: MODELC_1:def 69
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)
proof end;
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
proof end;
end;

:: deftheorem Def69 defines PathConc MODELC_1:def 69 :
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: :: MODELC_1:38
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 st pai1 . k = pai2 . 0 holds
PathConc (pai1,pai2,k) is inf_path of R
proof end;

:: EG(f) is fixpoint of Fax(f,*).
theorem Th39: :: MODELC_1:39
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 s being Element of S holds
( s |= EG f iff s |= Fax (f,(EG f)) )
proof end;

:: Existence path for fixpoint of Fax(f,*).
theorem Th40: :: MODELC_1:40
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for g being Assign of (BASSModel (R,BASSIGN))
for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) holds
ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Element of NAT holds pai . n |= g ) )
proof end;

:: EG(f) is the maximum fixpoint of Fax(f,*)
theorem Th41: :: MODELC_1:41
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 ( for s being Element of S holds
( s |= g iff s |= Fax (f,g) ) ) holds
for s being Element of S st s |= g holds
s |= EG f
proof end;

:: definition of TransEG(f)::translated function for EG(f)
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 -> V226() Function of (bool S),(bool S) means :Def70: :: MODELC_1:def 70
for G being Subset of S holds it . G = SigFaxTau (f,G,R,BASSIGN);
existence
ex b1 being V226() Function of (bool S),(bool S) st
for G being Subset of S holds b1 . G = SigFaxTau (f,G,R,BASSIGN)
proof end;
uniqueness
for b1, b2 being V226() Function of (bool S),(bool S) st ( for G being Subset of S holds b1 . G = SigFaxTau (f,G,R,BASSIGN) ) & ( for G being Subset of S holds b2 . G = SigFaxTau (f,G,R,BASSIGN) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def70 defines TransEG MODELC_1:def 70 :
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 V226() 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) );

:: fixpoint of TransEG(f)
theorem Th42: :: MODELC_1:42
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
( ( for s being Element of S holds
( s |= g iff s |= Fax (f,g) ) ) iff SIGMA g is_a_fixpoint_of TransEG f )
proof end;

theorem :: MODELC_1:43
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 (EG f) = gfp (S,(TransEG f))
proof end;

:: definition Foax(g,f,*):carrier ->carrier
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 :: MODELC_1:def 71
g 'or' (Fax (f,h));
coherence
g 'or' (Fax (f,h)) is Assign of (BASSModel (R,BASSIGN))
;
end;

:: deftheorem defines Foax MODELC_1:def 71 :
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));

:: Foax(g,f,*) is monotonic.
theorem Th44: :: MODELC_1:44
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, h1, h2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2)
proof end;

::commutative
:: Foax(g,f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFoaxTau(g,f,*)
::
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 :: MODELC_1:def 72
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 72 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN))
for H being Subset of S holds SigFoaxTau (g,f,H,R,BASSIGN) = SIGMA (Foax (g,f,(Tau (H,R,BASSIGN))));

:: SigFoaxTau(g,f,*) is monotonic.
theorem Th45: :: MODELC_1:45
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)
proof end;

:: f EU g is fixpoint of Foax(g,f,*).
theorem Th46: :: MODELC_1:46
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 s being Element of S holds
( s |= f EU g iff s |= Foax (g,f,(f EU g)) )
proof end;

:: f EU g is the minimum fixpoint of Foax(g,f,*)
theorem Th47: :: MODELC_1:47
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)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
proof end;

:: definition of TransEU(f,g)::translated function for f EU g
definition
let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f, g be Assign of (BASSModel (R,BASSIGN));
func TransEU (f,g) -> V226() Function of (bool S),(bool S) means :Def73: :: MODELC_1:def 73
for H being Subset of S holds it . H = SigFoaxTau (g,f,H,R,BASSIGN);
existence
ex b1 being V226() Function of (bool S),(bool S) st
for H being Subset of S holds b1 . H = SigFoaxTau (g,f,H,R,BASSIGN)
proof end;
uniqueness
for b1, b2 being V226() Function of (bool S),(bool S) st ( for H being Subset of S holds b1 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) & ( for H being Subset of S holds b2 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def73 defines TransEU 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 being Assign of (BASSModel (R,BASSIGN))
for b6 being V226() 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) );

:: fixpoint of TransEU(f,g)
theorem Th48: :: MODELC_1:48
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
( ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) iff SIGMA h is_a_fixpoint_of TransEU (f,g) )
proof end;

theorem :: MODELC_1:49
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 SIGMA (f EU g) = lfp (S,(TransEU (f,g)))
proof end;

:: Solver for EX and TransEG,TransEU
theorem Th50: :: MODELC_1:50
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 (EX f) = Pred ((SIGMA f),R)
proof end;

theorem :: MODELC_1:51
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 X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R))
proof end;

theorem :: MODELC_1:52
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 X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R)))
proof end;