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

correctness

coherence

( ( x in S implies x is Element of S ) & ( not x in S implies a is Element of S ) );

consistency

for b_{1} being Element of S holds verum;

;

end;
let a be Element of S;

correctness

coherence

( ( x in S implies x is Element of S ) & ( not x in S implies a is Element of S ) );

consistency

for b

;

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

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 ;

correctness

coherence

( ( x in NAT implies x is Element of NAT ) & ( not x in NAT implies 0 is Element of NAT ) );

consistency

for b_{1} being Element of NAT holds verum;

;

end;
correctness

coherence

( ( x in NAT implies x is Element of NAT ) & ( not x in NAT implies 0 is Element of NAT ) );

consistency

for b

;

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

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 ;

correctness

coherence

( ( x in dom f implies f . x is set ) & ( not x in dom f implies a is set ) );

consistency

for b_{1} being set holds verum;

;

end;
let x, a be set ;

correctness

coherence

( ( x in dom f implies f . x is set ) & ( not x in dom f implies a is set ) );

consistency

for b

;

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

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 ;

coherence

( ( a is boolean set implies a is boolean set ) & ( a is not boolean set implies FALSE is boolean set ) );

consistency

for b_{1} being boolean set holds verum;

;

end;
func Castboolean a -> boolean set equals :Def4: :: MODELC_1:def 4

a if a is boolean set

otherwise FALSE ;

correctness a if a is boolean set

otherwise FALSE ;

coherence

( ( a is boolean set implies a is boolean set ) & ( a is not boolean set implies FALSE is boolean set ) );

consistency

for b

;

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

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 ;

correctness

coherence

( ( a c= X implies a is Subset of X ) & ( not a c= X implies {} is Subset of X ) );

consistency

for b_{1} being Subset of X holds verum;

by XBOOLE_1:2;

end;
correctness

coherence

( ( a c= X implies a is Subset of X ) & ( not a c= X implies {} is Subset of X ) );

consistency

for b

by XBOOLE_1:2;

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

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

:: deftheorem defines atom. MODELC_1:def 6 :

for n being Element of NAT holds atom. n = <*(5 + n)*>;

for n being Element of NAT holds atom. n = <*(5 + n)*>;

definition

let p be FinSequence of NAT ;

coherence

<*0*> ^ p is FinSequence of NAT ;

let q be FinSequence of NAT ;

coherence

(<*1*> ^ p) ^ q is FinSequence of NAT ;

end;
coherence

<*0*> ^ p is FinSequence of NAT ;

let q be FinSequence of NAT ;

coherence

(<*1*> ^ p) ^ q is FinSequence of NAT ;

:: deftheorem defines 'not' MODELC_1:def 7 :

for p being FinSequence of NAT holds 'not' p = <*0*> ^ p;

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;

for p, q being FinSequence of NAT holds p '&' q = (<*1*> ^ p) ^ q;

definition

let p be FinSequence of NAT ;

coherence

<*2*> ^ p is FinSequence of NAT ;

coherence

<*3*> ^ p is FinSequence of NAT ;

let q be FinSequence of NAT ;

coherence

(<*4*> ^ p) ^ q is FinSequence of NAT ;

end;
coherence

<*2*> ^ p is FinSequence of NAT ;

coherence

<*3*> ^ p is FinSequence of NAT ;

let q be FinSequence of NAT ;

coherence

(<*4*> ^ p) ^ q is FinSequence of NAT ;

:: deftheorem defines EU MODELC_1:def 11 :

for p, q being FinSequence of NAT holds p EU q = (<*4*> ^ p) ^ q;

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

ex b_{1} being non empty set st

( ( for a being set st a in b_{1} holds

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

'not' p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p '&' q in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

EX p in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

EG p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p EU q in b_{1} ) & ( 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

b_{1} c= D ) )

for b_{1}, b_{2} being non empty set st ( for a being set st a in b_{1} holds

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

'not' p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p '&' q in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

EX p in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

EG p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p EU q in b_{1} ) & ( 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

b_{1} c= D ) & ( for a being set st a in b_{2} holds

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b_{2} ) & ( for p being FinSequence of NAT st p in b_{2} holds

'not' p in b_{2} ) & ( for p, q being FinSequence of NAT st p in b_{2} & q in b_{2} holds

p '&' q in b_{2} ) & ( for p being FinSequence of NAT st p in b_{2} holds

EX p in b_{2} ) & ( for p being FinSequence of NAT st p in b_{2} holds

EG p in b_{2} ) & ( for p, q being FinSequence of NAT st p in b_{2} & q in b_{2} holds

p EU q in b_{2} ) & ( 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

b_{2} c= D ) holds

b_{1} = b_{2}
end;

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

ex b

( ( for a being set st a in b

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b

'not' p in b

p '&' q in b

EX p in b

EG p in b

p EU q in b

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

b

proof end;

uniqueness for b

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b

'not' p in b

p '&' q in b

EX p in b

EG p in b

p EU q in b

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

b

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b

'not' p in b

p '&' q in b

EX p in b

EG p in b

p EU q in b

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

b

b

proof end;

:: deftheorem Def12 defines CTL_WFF MODELC_1:def 12 :

for b_{1} being non empty set holds

( b_{1} = CTL_WFF iff ( ( for a being set st a in b_{1} holds

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

'not' p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p '&' q in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

EX p in b_{1} ) & ( for p being FinSequence of NAT st p in b_{1} holds

EG p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p EU q in b_{1} ) & ( 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

b_{1} c= D ) ) );

for b

( b

a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b

'not' p in b

p '&' q in b

EX p in b

EG p in b

p EU q in b

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

b

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

for IT being FinSequence of NAT holds

( IT is CTL-formula-like iff IT is Element of CTL_WFF );

registration

ex b_{1} being FinSequence of NAT st b_{1} is CTL-formula-like
end;

cluster Relation-like NAT -defined NAT -valued Function-like FinSequence-like CTL-formula-like for FinSequence of NAT ;

existence ex b

proof end;

registration

let H be CTL-formula;

coherence

'not' H is CTL-formula-like

EX H is CTL-formula-like

EG H is CTL-formula-like

coherence

H '&' G is CTL-formula-like

H EU G is CTL-formula-like

end;
coherence

'not' H is CTL-formula-like

proof end;

coherence EX H is CTL-formula-like

proof end;

coherence EG H is CTL-formula-like

proof end;

let G be CTL-formula;coherence

H '&' G is CTL-formula-like

proof end;

coherence H EU G is CTL-formula-like

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

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

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

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

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

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

for H being CTL-formula holds

( H is ExistUntill iff ex F, G being CTL-formula st H = F EU G );

:: deftheorem defines 'or' MODELC_1:def 20 :

for F, G being CTL-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));

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 )

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

( ( H is negative implies ex b_{1} being CTL-formula st 'not' b_{1} = H ) & ( H is ExistNext implies ex b_{1} being CTL-formula st EX b_{1} = H ) & ( not H is negative & not H is ExistNext implies ex b_{1} being CTL-formula st EG b_{1} = H ) )
by A1, Def15, Def17, Def18;

uniqueness

for b_{1}, b_{2} being CTL-formula holds

( ( H is negative & 'not' b_{1} = H & 'not' b_{2} = H implies b_{1} = b_{2} ) & ( H is ExistNext & EX b_{1} = H & EX b_{2} = H implies b_{1} = b_{2} ) & ( not H is negative & not H is ExistNext & EG b_{1} = H & EG b_{2} = H implies b_{1} = b_{2} ) )
by FINSEQ_1:33;

consistency

for b_{1} being CTL-formula st H is negative & H is ExistNext holds

( 'not' b_{1} = H iff EX b_{1} = H )
by Lm15;

end;
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 'not' it = H if H is negative

EX it = H if H is ExistNext

otherwise EG it = H;

( ( H is negative implies ex b

uniqueness

for b

( ( H is negative & 'not' b

consistency

for b

( 'not' b

:: 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 b_{2} being CTL-formula holds

( ( H is negative implies ( b_{2} = the_argument_of H iff 'not' b_{2} = H ) ) & ( H is ExistNext implies ( b_{2} = the_argument_of H iff EX b_{2} = H ) ) & ( not H is negative & not H is ExistNext implies ( b_{2} = the_argument_of H iff EG b_{2} = H ) ) );

for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds

for b

( ( H is negative implies ( b

definition

let H be CTL-formula;

assume A1: ( H is conjunctive or H is ExistUntill ) ;

( ( H is conjunctive implies ex b_{1}, H1 being CTL-formula st b_{1} '&' H1 = H ) & ( not H is conjunctive implies ex b_{1}, H1 being CTL-formula st b_{1} EU H1 = H ) )
by A1, Def16, Def19;

uniqueness

for b_{1}, b_{2} being CTL-formula holds

( ( H is conjunctive & ex H1 being CTL-formula st b_{1} '&' H1 = H & ex H1 being CTL-formula st b_{2} '&' H1 = H implies b_{1} = b_{2} ) & ( not H is conjunctive & ex H1 being CTL-formula st b_{1} EU H1 = H & ex H1 being CTL-formula st b_{2} EU H1 = H implies b_{1} = b_{2} ) )
by Lm12, Lm13;

consistency

for b_{1} being CTL-formula holds verum
;

( ( H is conjunctive implies ex b_{1}, H1 being CTL-formula st H1 '&' b_{1} = H ) & ( not H is conjunctive implies ex b_{1}, H1 being CTL-formula st H1 EU b_{1} = H ) )

for b_{1}, b_{2} being CTL-formula holds

( ( H is conjunctive & ex H1 being CTL-formula st H1 '&' b_{1} = H & ex H1 being CTL-formula st H1 '&' b_{2} = H implies b_{1} = b_{2} ) & ( not H is conjunctive & ex H1 being CTL-formula st H1 EU b_{1} = H & ex H1 being CTL-formula st H1 EU b_{2} = H implies b_{1} = b_{2} ) )
by Lm12, Lm13;

consistency

for b_{1} being CTL-formula holds verum
;

end;
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 ex H1 being CTL-formula st it '&' H1 = H if H is conjunctive

otherwise ex H1 being CTL-formula st it EU H1 = H;

( ( H is conjunctive implies ex b

uniqueness

for b

( ( H is conjunctive & ex H1 being CTL-formula st b

consistency

for b

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 ex H1 being CTL-formula st H1 '&' it = H if H is conjunctive

otherwise ex H1 being CTL-formula st H1 EU it = H;

( ( H is conjunctive implies ex b

proof end;

uniqueness for b

( ( H is conjunctive & ex H1 being CTL-formula st H1 '&' b

consistency

for b

:: 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 b_{2} being CTL-formula holds

( ( H is conjunctive implies ( b_{2} = the_left_argument_of H iff ex H1 being CTL-formula st b_{2} '&' H1 = H ) ) & ( not H is conjunctive implies ( b_{2} = the_left_argument_of H iff ex H1 being CTL-formula st b_{2} EU H1 = H ) ) );

for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds

for b

( ( H is conjunctive implies ( b

:: 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 b_{2} being CTL-formula holds

( ( H is conjunctive implies ( b_{2} = the_right_argument_of H iff ex H1 being CTL-formula st H1 '&' b_{2} = H ) ) & ( not H is conjunctive implies ( b_{2} = the_right_argument_of H iff ex H1 being CTL-formula st H1 EU b_{2} = H ) ) );

for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds

for b

( ( H is conjunctive implies ( b

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 ;

coherence

( ( x in CTL_WFF implies x is CTL-formula ) & ( not x in CTL_WFF implies atom. 0 is CTL-formula ) );

consistency

for b_{1} being CTL-formula holds verum;

by Th1;

end;
func CastCTLformula x -> CTL-formula equals :Def24: :: MODELC_1:def 24

x if x in CTL_WFF

otherwise atom. 0;

correctness x if x in CTL_WFF

otherwise atom. 0;

coherence

( ( x in CTL_WFF implies x is CTL-formula ) & ( not x in CTL_WFF implies atom. 0 is CTL-formula ) );

consistency

for b

by Th1;

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

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 of Kripke structure & CTL model structure.

::**

::****************************************************

definition

let Prop be set ;

attr c_{2} is strict ;

struct KripkeStr over Prop -> RelStr ;

aggr KripkeStr(# carrier, Starts, InternalRel, Label #) -> KripkeStr over Prop;

sel Starts c_{2} -> Subset of the carrier of c_{2};

sel Label c_{2} -> Function of the carrier of c_{2},(bool Prop);

end;
attr c

struct KripkeStr over Prop -> RelStr ;

aggr KripkeStr(# carrier, Starts, InternalRel, Label #) -> KripkeStr over Prop;

sel Starts c

sel Label c

definition

attr c_{1} is strict ;

struct CTLModelStr -> ComplULattStr ;

aggr CTLModelStr(# carrier, BasicAssign, L_meet, Compl, EneXt, EGlobal, EUntill #) -> CTLModelStr ;

sel BasicAssign c_{1} -> Subset of the carrier of c_{1};

sel EneXt c_{1} -> UnOp of the carrier of c_{1};

sel EGlobal c_{1} -> UnOp of the carrier of c_{1};

sel EUntill c_{1} -> BinOp of the carrier of c_{1};

end;
struct CTLModelStr -> ComplULattStr ;

aggr CTLModelStr(# carrier, BasicAssign, L_meet, Compl, EneXt, EGlobal, EUntill #) -> CTLModelStr ;

sel BasicAssign c

sel EneXt c

sel EGlobal c

sel EUntill c

:: Preparation to define semantics for CTL-language

:: definition of evaluate function of CTL

:: definition of evaluate function of CTL

definition

coherence

{ x where x is CTL-formula : x is atomic } is Subset of CTL_WFF;

end;

func atomic_WFF -> Subset of CTL_WFF equals :: MODELC_1:def 25

{ x where x is CTL-formula : x is atomic } ;

correctness { x where x is CTL-formula : x is atomic } ;

coherence

{ x where x is CTL-formula : x is atomic } is Subset of CTL_WFF;

proof end;

:: deftheorem defines atomic_WFF MODELC_1:def 25 :

atomic_WFF = { x where x is CTL-formula : x is atomic } ;

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;

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

for H being CTL-formula holds

( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

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

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 ;

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

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

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

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;

( ( 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 b_{1} being set holds

( ( len H > n + 1 & len H = n + 1 & H is atomic implies ( b_{1} = f . H iff b_{1} = Kai . H ) ) & ( len H > n + 1 & len H = n + 1 & H is negative implies ( b_{1} = f . H iff b_{1} = the Compl of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is conjunctive implies ( b_{1} = f . H iff b_{1} = 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 ( b_{1} = f . H iff b_{1} = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistGlobal implies ( b_{1} = f . H iff b_{1} = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistUntill implies ( b_{1} = f . H iff b_{1} = 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 ( b_{1} = f . H iff b_{1} = h . H ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is negative implies ( b_{1} = Kai . H iff b_{1} = the Compl of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is conjunctive implies ( b_{1} = Kai . H iff b_{1} = 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 ( b_{1} = Kai . H iff b_{1} = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistGlobal implies ( b_{1} = Kai . H iff b_{1} = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistUntill implies ( b_{1} = Kai . H iff b_{1} = 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 ( b_{1} = Kai . H iff b_{1} = h . H ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is conjunctive implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = 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 ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistGlobal implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistUntill implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = 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 ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = h . H ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistNext implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistGlobal implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistUntill implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = 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 ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = h . H ) ) & ( len H = n + 1 & H is ExistNext & len H = n + 1 & H is ExistGlobal implies ( b_{1} = the EneXt of V . (h . (the_argument_of H)) iff b_{1} = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is ExistNext & len H = n + 1 & H is ExistUntill implies ( b_{1} = the EneXt of V . (h . (the_argument_of H)) iff b_{1} = 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 ( b_{1} = the EneXt of V . (h . (the_argument_of H)) iff b_{1} = h . H ) ) & ( len H = n + 1 & H is ExistGlobal & len H = n + 1 & H is ExistUntill implies ( b_{1} = the EGlobal of V . (h . (the_argument_of H)) iff b_{1} = 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 ( b_{1} = the EGlobal of V . (h . (the_argument_of H)) iff b_{1} = h . H ) ) & ( len H = n + 1 & H is ExistUntill & len H < n + 1 implies ( b_{1} = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = h . H ) ) )
by Lm14, Lm15, Lm16, Lm17, Lm18;

end;
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 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 {} ;

( ( 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 b

( ( len H > n + 1 & len H = n + 1 & H is atomic implies ( b

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

for V being CTLModelStr

for Kai being Function of atomic_WFF, the BasicAssign of V

for f, h being Function of CTL_WFF, the carrier of V

for n being Element of NAT

for H being CTL-formula holds

( ( len H > n + 1 implies GraftEval (V,Kai,f,h,n,H) = f . H ) & ( len H = n + 1 & H is atomic implies GraftEval (V,Kai,f,h,n,H) = Kai . H ) & ( len H = n + 1 & H is negative implies GraftEval (V,Kai,f,h,n,H) = the Compl of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is ExistNext implies GraftEval (V,Kai,f,h,n,H) = the EneXt of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistGlobal implies GraftEval (V,Kai,f,h,n,H) = the EGlobal of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistUntill implies GraftEval (V,Kai,f,h,n,H) = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = h . H ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is ExistNext ) & ( not len H = n + 1 or not H is ExistGlobal ) & ( not len H = n + 1 or not H is ExistUntill ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) );

:: deftheorem Def29 defines with_basic MODELC_1:def 29 :

for C being CTLModelStr holds

( C is with_basic iff not the BasicAssign of C is empty );

for C being CTLModelStr holds

( C is with_basic iff not the BasicAssign of C is empty );

definition

CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #) is CTLModelStr ;

end;

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

CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #) is CTLModelStr ;

:: deftheorem defines TrivialCTLModel MODELC_1:def 30 :

TrivialCTLModel = CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #);

TrivialCTLModel = CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #);

registration

coherence

( TrivialCTLModel is with_basic & TrivialCTLModel is strict & not TrivialCTLModel is empty )

end;
( TrivialCTLModel is with_basic & TrivialCTLModel is strict & not TrivialCTLModel is empty )

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

coherence

{ h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } is non empty set ;

end;
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 { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;

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;

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

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 ;

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 b_{1} being Function of CTL_WFF, the carrier of V holds verum;

by FUNCT_2:66;

end;
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 x if x in Funcs (CTL_WFF, the carrier of V)

otherwise CTL_WFF --> v0;

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 b

by FUNCT_2:66;

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

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;

ex b_{1} being non empty set st

for p being set holds

( p in b_{1} iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) )

for b_{1}, b_{2} being non empty set st ( for p being set holds

( p in b_{1} 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 b_{2} iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) ) holds

b_{1} = b_{2}

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

ex b

for p being set holds

( p in b

proof end;

uniqueness for b

( p in b

( p in b

b

proof 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 b_{3} being non empty set holds

( b_{3} = EvalFamily (V,Kai) iff for p being set holds

( p in b_{3} iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) );

for V being CTLModel

for Kai being Function of atomic_WFF, the BasicAssign of V

for b

( b

( p in b

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

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

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;

ex b_{1} being Assign of V ex f being Function of CTL_WFF, the carrier of V st

( f is-Evaluation-for Kai & b_{1} = f . H )

for b_{1}, b_{2} being Assign of V st ex f being Function of CTL_WFF, the carrier of V st

( f is-Evaluation-for Kai & b_{1} = f . H ) & ex f being Function of CTL_WFF, the carrier of V st

( f is-Evaluation-for Kai & b_{2} = f . H ) holds

b_{1} = b_{2}
by Th4;

end;
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 f being Function of CTL_WFF, the carrier of V st

( f is-Evaluation-for Kai & it = f . H );

ex b

( f is-Evaluation-for Kai & b

proof end;

uniqueness for b

( f is-Evaluation-for Kai & b

( f is-Evaluation-for Kai & b

b

:: 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 b_{4} being Assign of V holds

( b_{4} = Evaluate (H,Kai) iff ex f being Function of CTL_WFF, the carrier of V st

( f is-Evaluation-for Kai & b_{4} = f . H ) );

for V being CTLModel

for Kai being Function of atomic_WFF, the BasicAssign of V

for H being CTL-formula

for b

( b

( f is-Evaluation-for Kai & b

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;
let f be Assign of V;

synonym 'not' f for f ` ;

let g be Assign of V;

synonym f '&' g for f "/\" g;

definition

let V be CTLModel;

let f be Assign of V;

correctness

coherence

the EneXt of V . f is Assign of V;

;

correctness

coherence

the EGlobal of V . f is Assign of V;

;

end;
let f be Assign of V;

correctness

coherence

the EneXt of V . f is Assign of V;

;

correctness

coherence

the EGlobal of V . f is Assign of V;

;

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

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;

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;

correctness

coherence

the EUntill of V . (f,g) is Assign of V;

;

correctness

coherence

'not' (('not' f) '&' ('not' g)) is Assign of V;

;

end;
let f, g be Assign of V;

correctness

coherence

the EUntill of V . (f,g) is Assign of V;

;

correctness

coherence

'not' (('not' f) '&' ('not' g)) is Assign of V;

;

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

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

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

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

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

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

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

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

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;

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

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

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{ F_{1}() -> non empty set , F_{2}() -> total Relation of F_{1}(),F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}( Element of F_{1}()) -> set } :

ExistPath{ F

ex f being Function of NAT,F_{1}() st

( f . 0 = F_{3}() & ( for n being Element of NAT holds

( [(f . n),(f . (n + 1))] in F_{2}() & f . (n + 1) in F_{4}((f . n)) ) ) )

provided( f . 0 = F

( [(f . n),(f . (n + 1))] in F

A1:
for s being Element of F_{1}() holds (Im (F_{2}(),s)) /\ F_{4}(s) is non empty Subset of F_{1}()

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;

ex b_{1} being Function of NAT,S st

for n being Element of NAT holds [(b_{1} . n),(b_{1} . (n + 1))] in R

end;
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 for n being Element of NAT holds [(it . n),(it . (n + 1))] in R;

ex b

for n being Element of NAT holds [(b

proof 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 b_{3} being Function of NAT,S holds

( b_{3} is inf_path of R iff for n being Element of NAT holds [(b_{3} . n),(b_{3} . (n + 1))] in R );

for S being non empty set

for R being total Relation of S,S

for b

( b

::definition of concrete object of CTL model

:: deftheorem defines ModelSP MODELC_1:def 40 :

for S being non empty set holds ModelSP S = Funcs (S,BOOLEAN);

for S being non empty set holds ModelSP S = Funcs (S,BOOLEAN);

registration
end;

:: definition Fid:ModelSP(S) -> Function of S,BOOLEAN

definition

let S be non empty set ;

let f be set ;

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 b_{1} being Function of S,BOOLEAN holds verum;

by FUNCT_2:66;

end;
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 f if f in ModelSP S

otherwise S --> FALSE;

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 b

by FUNCT_2:66;

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

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{ F_{1}() -> non empty set , F_{2}() -> Function of F_{1}(),BOOLEAN, F_{3}( set , Function of F_{1}(),BOOLEAN) -> boolean set } :

Func1EX{ F

ex g being set st

( g in ModelSP F_{1}() & ( for s being set st s in F_{1}() holds

( F_{3}(s,F_{2}()) = TRUE iff (Fid (g,F_{1}())) . s = TRUE ) ) )

( g in ModelSP F

( F

proof end;

scheme :: MODELC_1:sch 3

Func1Unique{ F_{1}() -> non empty set , F_{2}() -> Function of F_{1}(),BOOLEAN, F_{3}( set , Function of F_{1}(),BOOLEAN) -> boolean set } :

Func1Unique{ F

for g1, g2 being set st g1 in ModelSP F_{1}() & ( for s being set st s in F_{1}() holds

( F_{3}(s,F_{2}()) = TRUE iff (Fid (g1,F_{1}())) . s = TRUE ) ) & g2 in ModelSP F_{1}() & ( for s being set st s in F_{1}() holds

( F_{3}(s,F_{2}()) = TRUE iff (Fid (g2,F_{1}())) . s = TRUE ) ) holds

g1 = g2

( F

( F

g1 = g2

proof end;

::schemes for existence & uniqueness of Unary Operation

scheme :: MODELC_1:sch 5

UnOpUnique{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}() } :

UnOpUnique{ F

for o1, o2 being UnOp of F_{2}() st ( for f being set st f in F_{2}() holds

o1 . f = F_{3}(f) ) & ( for f being set st f in F_{2}() holds

o2 . f = F_{3}(f) ) holds

o1 = o2

o1 . f = F

o2 . f = F

o1 = o2

proof end;

::schemes for existence & uniqueness of 2 Operands functor .

scheme :: MODELC_1:sch 6

Func2EX{ F_{1}() -> non empty set , F_{2}() -> Function of F_{1}(),BOOLEAN, F_{3}() -> Function of F_{1}(),BOOLEAN, F_{4}( set , Function of F_{1}(),BOOLEAN, Function of F_{1}(),BOOLEAN) -> boolean set } :

Func2EX{ F

ex h being set st

( h in ModelSP F_{1}() & ( for s being set st s in F_{1}() holds

( F_{4}(s,F_{2}(),F_{3}()) = TRUE iff (Fid (h,F_{1}())) . s = TRUE ) ) )

( h in ModelSP F

( F

proof end;

scheme :: MODELC_1:sch 7

Func2Unique{ F_{1}() -> non empty set , F_{2}() -> Function of F_{1}(),BOOLEAN, F_{3}() -> Function of F_{1}(),BOOLEAN, F_{4}( set , Function of F_{1}(),BOOLEAN, Function of F_{1}(),BOOLEAN) -> boolean set } :

Func2Unique{ F

for h1, h2 being set st h1 in ModelSP F_{1}() & ( for s being set st s in F_{1}() holds

( F_{4}(s,F_{2}(),F_{3}()) = TRUE iff (Fid (h1,F_{1}())) . s = TRUE ) ) & h2 in ModelSP F_{1}() & ( for s being set st s in F_{1}() holds

( F_{4}(s,F_{2}(),F_{3}()) = TRUE iff (Fid (h2,F_{1}())) . s = TRUE ) ) holds

h1 = h2

( F

( F

h1 = h2

proof end;

:: definition of Not_ unary operation of Model Space.

definition

let S be non empty set ;

let f be set ;

ex b_{1} being Element of ModelSP S st

for s being set st s in S holds

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b_{1},S)) . s = TRUE )

for b_{1}, b_{2} being Element of ModelSP S st ( for s being set st s in S holds

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b_{1},S)) . s = TRUE ) ) & ( for s being set st s in S holds

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b_{2},S)) . s = TRUE ) ) holds

b_{1} = b_{2}

end;
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 for s being set st s in S holds

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (it,S)) . s = TRUE );

ex b

for s being set st s in S holds

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b

proof end;

uniqueness for b

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b

b

proof end;

:: deftheorem Def42 defines Not_0 MODELC_1:def 42 :

for S being non empty set

for f being set

for b_{3} being Element of ModelSP S holds

( b_{3} = Not_0 (f,S) iff for s being set st s in S holds

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b_{3},S)) . s = TRUE ) );

for S being non empty set

for f being set

for b

( b

( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b

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 ;

ex b_{1} being UnOp of (ModelSP S) st

for f being set st f in ModelSP S holds

b_{1} . f = Not_0 (f,S)

for b_{1}, b_{2} being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds

b_{1} . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP S holds

b_{2} . f = Not_0 (f,S) ) holds

b_{1} = b_{2}
by Lm36;

end;
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 for f being set st f in ModelSP S holds

it . f = Not_0 (f,S);

ex b

for f being set st f in ModelSP S holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def43 defines Not_ MODELC_1:def 43 :

for S being non empty set

for b_{2} being UnOp of (ModelSP S) holds

( b_{2} = Not_ S iff for f being set st f in ModelSP S holds

b_{2} . f = Not_0 (f,S) );

for S being non empty set

for b

( b

b

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

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 b_{1} being Element of BOOLEAN holds verum;

;

end;
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 TRUE if ( x in S & ex pai being inf_path of R st

( pai . 0 = x & f . (pai . 1) = TRUE ) )

otherwise FALSE ;

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 b

;

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

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 ;

ex b_{1} 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 (b_{1},S)) . s = TRUE )

for b_{1}, b_{2} 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 (b_{1},S)) . s = TRUE ) ) & ( for s being set st s in S holds

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b_{2},S)) . s = TRUE ) ) holds

b_{1} = b_{2}

end;
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 for s being set st s in S holds

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE );

ex b

for s being set st s in S holds

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

proof end;

uniqueness for b

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

b

proof 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 b_{4} being Element of ModelSP S holds

( b_{4} = EneXt_0 (f,R) iff for s being set st s in S holds

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b_{4},S)) . s = TRUE ) );

for S being non empty set

for R being total Relation of S,S

for f being set

for b

( b

( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

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;

ex b_{1} being UnOp of (ModelSP S) st

for f being set st f in ModelSP S holds

b_{1} . f = EneXt_0 (f,R)

for b_{1}, b_{2} being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds

b_{1} . f = EneXt_0 (f,R) ) & ( for f being set st f in ModelSP S holds

b_{2} . f = EneXt_0 (f,R) ) holds

b_{1} = b_{2}
by Lm37;

end;
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 for f being set st f in ModelSP S holds

it . f = EneXt_0 (f,R);

ex b

for f being set st f in ModelSP S holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def46 defines EneXt_ MODELC_1:def 46 :

for S being non empty set

for R being total Relation of S,S

for b_{3} being UnOp of (ModelSP S) holds

( b_{3} = EneXt_ R iff for f being set st f in ModelSP S holds

b_{3} . f = EneXt_0 (f,R) );

for S being non empty set

for R being total Relation of S,S

for b

( b

b

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

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 b_{1} being Element of BOOLEAN holds verum;

;

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

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 b

;

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

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 ;

ex b_{1} 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 (b_{1},S)) . s = TRUE )

for b_{1}, b_{2} 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 (b_{1},S)) . s = TRUE ) ) & ( for s being set st s in S holds

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b_{2},S)) . s = TRUE ) ) holds

b_{1} = b_{2}

end;
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 for s being set st s in S holds

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE );

ex b

for s being set st s in S holds

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

proof end;

uniqueness for b

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

b

proof 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 b_{4} being Element of ModelSP S holds

( b_{4} = EGlobal_0 (f,R) iff for s being set st s in S holds

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b_{4},S)) . s = TRUE ) );

for S being non empty set

for R being total Relation of S,S

for f being set

for b

( b

( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b

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;

ex b_{1} being UnOp of (ModelSP S) st

for f being set st f in ModelSP S holds

b_{1} . f = EGlobal_0 (f,R)

for b_{1}, b_{2} being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds

b_{1} . f = EGlobal_0 (f,R) ) & ( for f being set st f in ModelSP S holds

b_{2} . f = EGlobal_0 (f,R) ) holds

b_{1} = b_{2}
by Lm38;

end;
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 for f being set st f in ModelSP S holds

it . f = EGlobal_0 (f,R);

ex b

for f being set st f in ModelSP S holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def49 defines EGlobal_ MODELC_1:def 49 :

for S being non empty set

for R being total Relation of S,S

for b_{3} being UnOp of (ModelSP S) holds

( b_{3} = EGlobal_ R iff for f being set st f in ModelSP S holds

b_{3} . f = EGlobal_0 (f,R) );

for S being non empty set

for R being total Relation of S,S

for b

( b

b

:: definition of And_ Binary Operation of Model Space.

definition

let S be non empty set ;

let f, g be set ;

ex b_{1} 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 (b_{1},S)) . s = TRUE )

for b_{1}, b_{2} 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 (b_{1},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 (b_{2},S)) . s = TRUE ) ) holds

b_{1} = b_{2}

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

ex b

for s being set st s in S holds

( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b

proof end;

uniqueness for b

( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b

( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b

b

proof end;

:: deftheorem Def50 defines And_0 MODELC_1:def 50 :

for S being non empty set

for f, g being set

for b_{4} being Element of ModelSP S holds

( b_{4} = 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 (b_{4},S)) . s = TRUE ) );

for S being non empty set

for f, g being set

for b

( b

( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b

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 ;

ex b_{1} being BinOp of (ModelSP S) st

for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{1} . (f,g) = And_0 (f,g,S)

for b_{1}, b_{2} being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{1} . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{2} . (f,g) = And_0 (f,g,S) ) holds

b_{1} = b_{2}
by Lm39;

end;
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 for f, g being set st f in ModelSP S & g in ModelSP S holds

it . (f,g) = And_0 (f,g,S);

ex b

for f, g being set st f in ModelSP S & g in ModelSP S holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def51 defines And_ MODELC_1:def 51 :

for S being non empty set

for b_{2} being BinOp of (ModelSP S) holds

( b_{2} = And_ S iff for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{2} . (f,g) = And_0 (f,g,S) );

for S being non empty set

for b

( b

b

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

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 b_{1} being Element of BOOLEAN holds verum;

;

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

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 b

;

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

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 ;

ex b_{1} 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 (b_{1},S)) . s = TRUE )

for b_{1}, b_{2} 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 (b_{1},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 (b_{2},S)) . s = TRUE ) ) holds

b_{1} = b_{2}

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

ex b

for s being set st s in S holds

( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b

proof end;

uniqueness for b

( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b

( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b

b

proof 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 b_{5} being Element of ModelSP S holds

( b_{5} = 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 (b_{5},S)) . s = TRUE ) );

for S being non empty set

for R being total Relation of S,S

for f, g being set

for b

( b

( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b

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;

ex b_{1} being BinOp of (ModelSP S) st

for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{1} . (f,g) = EUntill_0 (f,g,R)

for b_{1}, b_{2} being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{1} . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{2} . (f,g) = EUntill_0 (f,g,R) ) holds

b_{1} = b_{2}
by Lm40;

end;
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 for f, g being set st f in ModelSP S & g in ModelSP S holds

it . (f,g) = EUntill_0 (f,g,R);

ex b

for f, g being set st f in ModelSP S & g in ModelSP S holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def54 defines EUntill_ MODELC_1:def 54 :

for S being non empty set

for R being total Relation of S,S

for b_{3} being BinOp of (ModelSP S) holds

( b_{3} = EUntill_ R iff for f, g being set st f in ModelSP S & g in ModelSP S holds

b_{3} . (f,g) = EUntill_0 (f,g,R) );

for S being non empty set

for R being total Relation of S,S

for b

( b

b

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

ex b_{1} being Subset of X st

for x being set holds

( x in b_{1} iff ( x in X & ex f being Function of S,BOOLEAN st

( f = x & f . s = TRUE ) ) )

for b_{1}, b_{2} being Subset of X st ( for x being set holds

( x in b_{1} iff ( x in X & ex f being Function of S,BOOLEAN st

( f = x & f . s = TRUE ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & ex f being Function of S,BOOLEAN st

( f = x & f . s = TRUE ) ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being set holds

( x in b

( f = x & f . s = TRUE ) ) )

proof end;

uniqueness for b

( x in b

( f = x & f . s = TRUE ) ) ) ) & ( for x being set holds

( x in b

( f = x & f . s = TRUE ) ) ) ) holds

b

proof 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 b_{4} being Subset of X holds

( b_{4} = F_LABEL (s,X) iff for x being set holds

( x in b_{4} iff ( x in X & ex f being Function of S,BOOLEAN st

( f = x & f . s = TRUE ) ) ) );

for S being non empty set

for X being non empty Subset of (ModelSP S)

for s being set

for b

( b

( x in b

( f = x & f . s = TRUE ) ) ) );

definition

let S be non empty set ;

let X be non empty Subset of (ModelSP S);

ex b_{1} being Function of S,(bool X) st

for x being set st x in S holds

b_{1} . x = F_LABEL (x,X)

for b_{1}, b_{2} being Function of S,(bool X) st ( for x being set st x in S holds

b_{1} . x = F_LABEL (x,X) ) & ( for x being set st x in S holds

b_{2} . x = F_LABEL (x,X) ) holds

b_{1} = b_{2}

end;
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 for x being set st x in S holds

it . x = F_LABEL (x,X);

ex b

for x being set st x in S holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being Function of S,(bool X) holds

( b_{3} = Label_ X iff for x being set st x in S holds

b_{3} . x = F_LABEL (x,X) );

for S being non empty set

for X being non empty Subset of (ModelSP S)

for b

( b

b

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

KripkeStr(# S,S0,R,(Label_ Prop) #) is KripkeStr over Prop ;

end;
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) #);

KripkeStr(# S,S0,R,(Label_ Prop) #) is KripkeStr over Prop ;

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

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

coherence

not the carrier of (KModel (R,S0,Prop)) is empty ;

end;
let S0 be Subset of S;

let R be total Relation of S,S;

let Prop be non empty Subset of (ModelSP S);

coherence

not the carrier of (KModel (R,S0,Prop)) is empty ;

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

for b_{1} being Subset of (Funcs ( the carrier of (KModel (R,S0,Prop)),BOOLEAN)) st b_{1} = ModelSP the carrier of (KModel (R,S0,Prop)) holds

not b_{1} is empty
;

end;
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 b

not b

definition

let S be non empty set ;

let R be total Relation of S,S;

let BASSIGN be non empty Subset of (ModelSP S);

CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #) is CTLModelStr ;

end;
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) #);

CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #) is CTLModelStr ;

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

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

coherence

( BASSModel (R,BASSIGN) is with_basic & not BASSModel (R,BASSIGN) is empty )

end;
let R be total Relation of S,S;

let BASSIGN be non empty Subset of (ModelSP S);

coherence

( BASSModel (R,BASSIGN) is with_basic & not BASSModel (R,BASSIGN) is empty )

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

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

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

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

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 )

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 )

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

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

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

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

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

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;

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

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

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

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 )

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 )

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

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

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

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

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

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

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

::*************

::

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

::

::*************

::

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

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 b_{1} being Element of S holds verum;

;

end;
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 s0 if n = 0

otherwise pai . (k_nat ((k_nat n) - 1));

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 b

;

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

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 )

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

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;

{ 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

end;
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 ) } ;

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

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

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

correctness

coherence

{ s where s is Element of S : s |= f } is Subset of S;

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

correctness

coherence

{ s where s is Element of S : s |= f } is Subset of S;

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

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

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;

ex b_{1} being Assign of (BASSModel (R,BASSIGN)) st

for s being set st s in S holds

(Fid (b_{1},S)) . s = (chi (T,S)) . s

for b_{1}, b_{2} being Assign of (BASSModel (R,BASSIGN)) st ( for s being set st s in S holds

(Fid (b_{1},S)) . s = (chi (T,S)) . s ) & ( for s being set st s in S holds

(Fid (b_{2},S)) . s = (chi (T,S)) . s ) holds

b_{1} = b_{2}

end;
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 for s being set st s in S holds

(Fid (it,S)) . s = (chi (T,S)) . s;

ex b

for s being set st s in S holds

(Fid (b

proof end;

uniqueness for b

(Fid (b

(Fid (b

b

proof 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 b_{5} being Assign of (BASSModel (R,BASSIGN)) holds

( b_{5} = Tau (T,R,BASSIGN) iff for s being set st s in S holds

(Fid (b_{5},S)) . s = (chi (T,S)) . s );

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 b

( b

(Fid (b

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

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

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

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

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)

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

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

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

correctness

coherence

f '&' (EX g) is Assign of (BASSModel (R,BASSIGN));

;

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

correctness

coherence

f '&' (EX g) is Assign of (BASSModel (R,BASSIGN));

;

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

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)

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

::

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

SIGMA (Fax (f,(Tau (G,R,BASSIGN)))) is Subset of S ;

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

SIGMA (Fax (f,(Tau (G,R,BASSIGN)))) is Subset of S ;

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

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)

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 ;

ex b_{1} being inf_path of R st

for n being Element of NAT holds b_{1} . n = pai . (n + k)

for b_{1}, b_{2} being inf_path of R st ( for n being Element of NAT holds b_{1} . n = pai . (n + k) ) & ( for n being Element of NAT holds b_{2} . n = pai . (n + k) ) holds

b_{1} = b_{2}

end;
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 for n being Element of NAT holds it . n = pai . (n + k);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being inf_path of R holds

( b_{5} = PathShift (pai,k) iff for n being Element of NAT holds b_{5} . n = pai . (n + k) );

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 b

( b

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 ;

coherence

( ( n < k implies pai1 . n is set ) & ( not n < k implies pai2 . (n - k) is set ) );

consistency

for b_{1} being set holds verum;

;

end;
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 pai1 . n if n < k

otherwise pai2 . (n - k);

coherence

( ( n < k implies pai1 . n is set ) & ( not n < k implies pai2 . (n - k) is set ) );

consistency

for b

;

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

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 ;

ex b_{1} being Function of NAT,S st

for n being Element of NAT holds b_{1} . n = PathChange (pai1,pai2,k,n)

for b_{1}, b_{2} being Function of NAT,S st ( for n being Element of NAT holds b_{1} . n = PathChange (pai1,pai2,k,n) ) & ( for n being Element of NAT holds b_{2} . n = PathChange (pai1,pai2,k,n) ) holds

b_{1} = b_{2}

end;
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 for n being Element of NAT holds it . n = PathChange (pai1,pai2,k,n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof 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 b_{6} being Function of NAT,S holds

( b_{6} = PathConc (pai1,pai2,k) iff for n being Element of NAT holds b_{6} . n = PathChange (pai1,pai2,k,n) );

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 b

( b

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

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

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

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

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

ex b_{1} being V226() Function of (bool S),(bool S) st

for G being Subset of S holds b_{1} . G = SigFaxTau (f,G,R,BASSIGN)

for b_{1}, b_{2} being V226() Function of (bool S),(bool S) st ( for G being Subset of S holds b_{1} . G = SigFaxTau (f,G,R,BASSIGN) ) & ( for G being Subset of S holds b_{2} . G = SigFaxTau (f,G,R,BASSIGN) ) holds

b_{1} = b_{2}

end;
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 for G being Subset of S holds it . G = SigFaxTau (f,G,R,BASSIGN);

ex b

for G being Subset of S holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being V226() Function of (bool S),(bool S) holds

( b_{5} = TransEG f iff for G being Subset of S holds b_{5} . G = SigFaxTau (f,G,R,BASSIGN) );

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 b

( b

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

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

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

coherence

g 'or' (Fax (f,h)) is Assign of (BASSModel (R,BASSIGN)) ;

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

coherence

g 'or' (Fax (f,h)) is Assign of (BASSModel (R,BASSIGN)) ;

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

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)

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

::

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

SIGMA (Foax (g,f,(Tau (H,R,BASSIGN)))) is Subset of S ;

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

SIGMA (Foax (g,f,(Tau (H,R,BASSIGN)))) is Subset of S ;

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

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)

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

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

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

ex b_{1} being V226() Function of (bool S),(bool S) st

for H being Subset of S holds b_{1} . H = SigFoaxTau (g,f,H,R,BASSIGN)

for b_{1}, b_{2} being V226() Function of (bool S),(bool S) st ( for H being Subset of S holds b_{1} . H = SigFoaxTau (g,f,H,R,BASSIGN) ) & ( for H being Subset of S holds b_{2} . H = SigFoaxTau (g,f,H,R,BASSIGN) ) holds

b_{1} = b_{2}

end;
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 for H being Subset of S holds it . H = SigFoaxTau (g,f,H,R,BASSIGN);

ex b

for H being Subset of S holds b

proof end;

uniqueness for b

b

proof 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 b_{6} being V226() Function of (bool S),(bool S) holds

( b_{6} = TransEU (f,g) iff for H being Subset of S holds b_{6} . H = SigFoaxTau (g,f,H,R,BASSIGN) );

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 b

( b

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

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

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)

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

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

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;