:: by Kazuhisa Ishida

::

:: Received April 21, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

definition

let x be set ;

correctness

coherence

( ( x is Nat implies x is Nat ) & ( x is not Nat implies 0 is Nat ) );

consistency

for b_{1} being Nat holds verum;

;

end;
correctness

coherence

( ( x is Nat implies x is Nat ) & ( x is not Nat implies 0 is Nat ) );

consistency

for b

;

:: deftheorem Def1 defines CastNat MODELC_2:def 1 :

for x being set holds

( ( x is Nat implies CastNat x = x ) & ( x is not Nat implies CastNat x = 0 ) );

for x being set holds

( ( x is Nat implies CastNat x = x ) & ( x is not Nat implies CastNat x = 0 ) );

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

m <= k

proof end;

:: The operations to make LTL-formulae

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 ;

coherence

(<*2*> ^ 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 ;

coherence

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

:: deftheorem defines 'not' MODELC_2:def 3 :

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_2:def 4 :

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;

:: deftheorem defines 'or' MODELC_2:def 5 :

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

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

definition

let p be FinSequence of NAT ;

coherence

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

let q be FinSequence of NAT ;

coherence

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

coherence

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

end;
coherence

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

let q be FinSequence of NAT ;

coherence

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

coherence

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

:: deftheorem defines 'U' MODELC_2:def 7 :

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

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

:: deftheorem defines 'R' MODELC_2:def 8 :

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

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

Lm2: for n being 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 LTL-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 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, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

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

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

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

p 'R' 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 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' 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 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, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

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

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

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

p 'R' 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 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' 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 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, q being FinSequence of NAT st p in b_{2} & q in b_{2} holds

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

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

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

p 'R' 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 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' q in D ) holds

b_{2} c= D ) holds

b_{1} = b_{2}
end;

func LTL_WFF -> non empty set means :Def9: :: MODELC_2:def 9

( ( for a being set st a in it holds

a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in it & q in it holds

p 'or' q in it ) & ( for p being FinSequence of NAT st p in it holds

'X' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds

p 'U' q in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds

p 'R' 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 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' 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 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, q being FinSequence of NAT st p in it & q in it holds

p 'or' q in it ) & ( for p being FinSequence of NAT st p in it holds

'X' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds

p 'U' q in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds

p 'R' 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 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' 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 Nat holds atom. n in b

'not' p in b

p '&' q in b

p 'or' q in b

'X' p in b

p 'U' q in b

p 'R' q in b

a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' q in D ) holds

b

proof end;

uniqueness for b

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

'not' p in b

p '&' q in b

p 'or' q in b

'X' p in b

p 'U' q in b

p 'R' q in b

a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' q in D ) holds

b

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

'not' p in b

p '&' q in b

p 'or' q in b

'X' p in b

p 'U' q in b

p 'R' q in b

a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' q in D ) holds

b

b

proof end;

:: deftheorem Def9 defines LTL_WFF MODELC_2:def 9 :

for b_{1} being non empty set holds

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

a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

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

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

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

p 'R' 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 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' q in D ) holds

b_{1} c= D ) ) );

for b

( b

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

'not' p in b

p '&' q in b

p 'or' q in b

'X' p in b

p 'U' q in b

p 'R' q in b

a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in D & q in D holds

p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds

'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p 'R' q in D ) holds

b

:: deftheorem Def10 defines LTL-formula-like MODELC_2:def 10 :

for IT being FinSequence of NAT holds

( IT is LTL-formula-like iff IT is Element of LTL_WFF );

for IT being FinSequence of NAT holds

( IT is LTL-formula-like iff IT is Element of LTL_WFF );

registration

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

cluster Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like LTL-formula-like for FinSequence of NAT ;

existence ex b

proof end;

registration

let H be LTL-formula;

coherence

'not' H is LTL-formula-like

'X' H is LTL-formula-like

coherence

H '&' G is LTL-formula-like

H 'or' G is LTL-formula-like

H 'U' G is LTL-formula-like

H 'R' G is LTL-formula-like

end;
coherence

'not' H is LTL-formula-like

proof end;

coherence 'X' H is LTL-formula-like

proof end;

let G be LTL-formula;coherence

H '&' G is LTL-formula-like

proof end;

coherence H 'or' G is LTL-formula-like

proof end;

coherence H 'U' G is LTL-formula-like

proof end;

coherence H 'R' G is LTL-formula-like

proof end;

:: deftheorem Def11 defines atomic MODELC_2:def 11 :

for H being LTL-formula holds

( H is atomic iff ex n being Nat st H = atom. n );

for H being LTL-formula holds

( H is atomic iff ex n being Nat st H = atom. n );

:: deftheorem Def12 defines negative MODELC_2:def 12 :

for H being LTL-formula holds

( H is negative iff ex H1 being LTL-formula st H = 'not' H1 );

for H being LTL-formula holds

( H is negative iff ex H1 being LTL-formula st H = 'not' H1 );

:: deftheorem Def13 defines conjunctive MODELC_2:def 13 :

for H being LTL-formula holds

( H is conjunctive iff ex F, G being LTL-formula st H = F '&' G );

for H being LTL-formula holds

( H is conjunctive iff ex F, G being LTL-formula st H = F '&' G );

:: deftheorem Def14 defines disjunctive MODELC_2:def 14 :

for H being LTL-formula holds

( H is disjunctive iff ex F, G being LTL-formula st H = F 'or' G );

for H being LTL-formula holds

( H is disjunctive iff ex F, G being LTL-formula st H = F 'or' G );

:: deftheorem Def15 defines next MODELC_2:def 15 :

for H being LTL-formula holds

( H is next iff ex H1 being LTL-formula st H = 'X' H1 );

for H being LTL-formula holds

( H is next iff ex H1 being LTL-formula st H = 'X' H1 );

:: deftheorem Def16 defines Until MODELC_2:def 16 :

for H being LTL-formula holds

( H is Until iff ex F, G being LTL-formula st H = F 'U' G );

for H being LTL-formula holds

( H is Until iff ex F, G being LTL-formula st H = F 'U' G );

:: deftheorem Def17 defines Release MODELC_2:def 17 :

for H being LTL-formula holds

( H is Release iff ex F, G being LTL-formula st H = F 'R' G );

for H being LTL-formula holds

( H is Release iff ex F, G being LTL-formula st H = F 'R' G );

theorem Th2: :: MODELC_2:2

for H being LTL-formula holds

( H is atomic or H is negative or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

( H is atomic or H is negative or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

proof end;

Lm3: for H being LTL-formula st H is negative holds

H . 1 = 0

proof end;

Lm4: for H being LTL-formula st H is conjunctive holds

H . 1 = 1

proof end;

Lm5: for H being LTL-formula st H is disjunctive holds

H . 1 = 2

proof end;

Lm6: for H being LTL-formula st H is next holds

H . 1 = 3

proof end;

Lm7: for H being LTL-formula st H is Until holds

H . 1 = 4

proof end;

Lm8: for H being LTL-formula st H is Release holds

H . 1 = 5

proof end;

Lm9: for H being LTL-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 & not H . 1 = 5 )

proof end;

Lm10: for H being LTL-formula holds

( ( H is atomic & H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 & H . 1 <> 5 ) or ( H is negative & H . 1 = 0 ) or ( H is conjunctive & H . 1 = 1 ) or ( H is disjunctive & H . 1 = 2 ) or ( H is next & H . 1 = 3 ) or ( H is Until & H . 1 = 4 ) or ( H is Release & H . 1 = 5 ) )

proof end;

Lm11: for H, F being LTL-formula

for sq being FinSequence st H = F ^ sq holds

H = F

proof end;

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

( H = H1 & G = G1 )

proof end;

Lm13: for H, G, H1, G1 being LTL-formula st H 'or' G = H1 'or' G1 holds

( H = H1 & G = G1 )

proof end;

Lm14: for H, G, H1, G1 being LTL-formula st H 'U' G = H1 'U' G1 holds

( H = H1 & G = G1 )

proof end;

Lm15: for H, G, H1, G1 being LTL-formula st H 'R' G = H1 'R' G1 holds

( H = H1 & G = G1 )

proof end;

Lm16: for H being LTL-formula st H is negative holds

( not H is atomic & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release )

proof end;

Lm17: for H being LTL-formula st H is conjunctive holds

( not H is atomic & not H is negative & not H is disjunctive & not H is next & not H is Until & not H is Release )

proof end;

Lm18: for H being LTL-formula st H is disjunctive holds

( not H is atomic & not H is negative & not H is conjunctive & not H is next & not H is Until & not H is Release )

proof end;

Lm19: for H being LTL-formula st H is next holds

( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is Until & not H is Release )

proof end;

Lm20: for H being LTL-formula st H is Until holds

( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Release )

proof end;

Lm21: for H being LTL-formula st H is Release holds

( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until )

proof end;

definition

let H be LTL-formula;

assume A1: ( H is negative or H is next ) ;

( ( H is negative implies ex b_{1} being LTL-formula st 'not' b_{1} = H ) & ( not H is negative implies ex b_{1} being LTL-formula st 'X' b_{1} = H ) )
by A1, Def12, Def15;

uniqueness

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

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

consistency

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

end;
assume A1: ( H is negative or H is next ) ;

func the_argument_of H -> LTL-formula means :Def18: :: MODELC_2:def 18

'not' it = H if H is negative

otherwise 'X' it = H;

existence 'not' it = H if H is negative

otherwise 'X' it = H;

( ( H is negative implies ex b

uniqueness

for b

( ( H is negative & 'not' b

consistency

for b

:: deftheorem Def18 defines the_argument_of MODELC_2:def 18 :

for H being LTL-formula st ( H is negative or H is next ) holds

for b_{2} being LTL-formula holds

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

for H being LTL-formula st ( H is negative or H is next ) holds

for b

( ( H is negative implies ( b

definition

let H be LTL-formula;

assume A1: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) ;

( ( H is conjunctive implies ex b_{1}, H1 being LTL-formula st b_{1} '&' H1 = H ) & ( H is disjunctive implies ex b_{1}, H1 being LTL-formula st b_{1} 'or' H1 = H ) & ( H is Until implies ex b_{1}, H1 being LTL-formula st b_{1} 'U' H1 = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b_{1}, H1 being LTL-formula st b_{1} 'R' H1 = H ) )
by A1, Def13, Def14, Def16, Def17;

uniqueness

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

( ( H is conjunctive & ex H1 being LTL-formula st b_{1} '&' H1 = H & ex H1 being LTL-formula st b_{2} '&' H1 = H implies b_{1} = b_{2} ) & ( H is disjunctive & ex H1 being LTL-formula st b_{1} 'or' H1 = H & ex H1 being LTL-formula st b_{2} 'or' H1 = H implies b_{1} = b_{2} ) & ( H is Until & ex H1 being LTL-formula st b_{1} 'U' H1 = H & ex H1 being LTL-formula st b_{2} 'U' H1 = H implies b_{1} = b_{2} ) & ( not H is conjunctive & not H is disjunctive & not H is Until & ex H1 being LTL-formula st b_{1} 'R' H1 = H & ex H1 being LTL-formula st b_{2} 'R' H1 = H implies b_{1} = b_{2} ) )
by Lm12, Lm13, Lm14, Lm15;

consistency

for b_{1} being LTL-formula holds

( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st b_{1} '&' H1 = H iff ex H1 being LTL-formula st b_{1} 'or' H1 = H ) ) & ( H is conjunctive & H is Until implies ( ex H1 being LTL-formula st b_{1} '&' H1 = H iff ex H1 being LTL-formula st b_{1} 'U' H1 = H ) ) & ( H is disjunctive & H is Until implies ( ex H1 being LTL-formula st b_{1} 'or' H1 = H iff ex H1 being LTL-formula st b_{1} 'U' H1 = H ) ) )
by Lm17, Lm18;

( ( H is conjunctive implies ex b_{1}, H1 being LTL-formula st H1 '&' b_{1} = H ) & ( H is disjunctive implies ex b_{1}, H1 being LTL-formula st H1 'or' b_{1} = H ) & ( H is Until implies ex b_{1}, H1 being LTL-formula st H1 'U' b_{1} = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b_{1}, H1 being LTL-formula st H1 'R' b_{1} = H ) )

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

( ( H is conjunctive & ex H1 being LTL-formula st H1 '&' b_{1} = H & ex H1 being LTL-formula st H1 '&' b_{2} = H implies b_{1} = b_{2} ) & ( H is disjunctive & ex H1 being LTL-formula st H1 'or' b_{1} = H & ex H1 being LTL-formula st H1 'or' b_{2} = H implies b_{1} = b_{2} ) & ( H is Until & ex H1 being LTL-formula st H1 'U' b_{1} = H & ex H1 being LTL-formula st H1 'U' b_{2} = H implies b_{1} = b_{2} ) & ( not H is conjunctive & not H is disjunctive & not H is Until & ex H1 being LTL-formula st H1 'R' b_{1} = H & ex H1 being LTL-formula st H1 'R' b_{2} = H implies b_{1} = b_{2} ) )
by Lm12, Lm13, Lm14, Lm15;

consistency

for b_{1} being LTL-formula holds

( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st H1 '&' b_{1} = H iff ex H1 being LTL-formula st H1 'or' b_{1} = H ) ) & ( H is conjunctive & H is Until implies ( ex H1 being LTL-formula st H1 '&' b_{1} = H iff ex H1 being LTL-formula st H1 'U' b_{1} = H ) ) & ( H is disjunctive & H is Until implies ( ex H1 being LTL-formula st H1 'or' b_{1} = H iff ex H1 being LTL-formula st H1 'U' b_{1} = H ) ) )
by Lm18, Lm20;

end;
assume A1: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) ;

func the_left_argument_of H -> LTL-formula means :Def19: :: MODELC_2:def 19

ex H1 being LTL-formula st it '&' H1 = H if H is conjunctive

ex H1 being LTL-formula st it 'or' H1 = H if H is disjunctive

ex H1 being LTL-formula st it 'U' H1 = H if H is Until

otherwise ex H1 being LTL-formula st it 'R' H1 = H;

existence ex H1 being LTL-formula st it '&' H1 = H if H is conjunctive

ex H1 being LTL-formula st it 'or' H1 = H if H is disjunctive

ex H1 being LTL-formula st it 'U' H1 = H if H is Until

otherwise ex H1 being LTL-formula st it 'R' H1 = H;

( ( H is conjunctive implies ex b

uniqueness

for b

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

consistency

for b

( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st b

func the_right_argument_of H -> LTL-formula means :Def20: :: MODELC_2:def 20

ex H1 being LTL-formula st H1 '&' it = H if H is conjunctive

ex H1 being LTL-formula st H1 'or' it = H if H is disjunctive

ex H1 being LTL-formula st H1 'U' it = H if H is Until

otherwise ex H1 being LTL-formula st H1 'R' it = H;

existence ex H1 being LTL-formula st H1 '&' it = H if H is conjunctive

ex H1 being LTL-formula st H1 'or' it = H if H is disjunctive

ex H1 being LTL-formula st H1 'U' it = H if H is Until

otherwise ex H1 being LTL-formula st H1 'R' it = H;

( ( H is conjunctive implies ex b

proof end;

uniqueness for b

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

consistency

for b

( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st H1 '&' b

:: deftheorem Def19 defines the_left_argument_of MODELC_2:def 19 :

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

for b_{2} being LTL-formula holds

( ( H is conjunctive implies ( b_{2} = the_left_argument_of H iff ex H1 being LTL-formula st b_{2} '&' H1 = H ) ) & ( H is disjunctive implies ( b_{2} = the_left_argument_of H iff ex H1 being LTL-formula st b_{2} 'or' H1 = H ) ) & ( H is Until implies ( b_{2} = the_left_argument_of H iff ex H1 being LTL-formula st b_{2} 'U' H1 = H ) ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ( b_{2} = the_left_argument_of H iff ex H1 being LTL-formula st b_{2} 'R' H1 = H ) ) );

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

for b

( ( H is conjunctive implies ( b

:: deftheorem Def20 defines the_right_argument_of MODELC_2:def 20 :

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

for b_{2} being LTL-formula holds

( ( H is conjunctive implies ( b_{2} = the_right_argument_of H iff ex H1 being LTL-formula st H1 '&' b_{2} = H ) ) & ( H is disjunctive implies ( b_{2} = the_right_argument_of H iff ex H1 being LTL-formula st H1 'or' b_{2} = H ) ) & ( H is Until implies ( b_{2} = the_right_argument_of H iff ex H1 being LTL-formula st H1 'U' b_{2} = H ) ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ( b_{2} = the_right_argument_of H iff ex H1 being LTL-formula st H1 'R' b_{2} = H ) ) );

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

for b

( ( H is conjunctive implies ( b

theorem :: MODELC_2:4

theorem Th6: :: MODELC_2:6

for H being LTL-formula st H is conjunctive holds

H = (the_left_argument_of H) '&' (the_right_argument_of H)

H = (the_left_argument_of H) '&' (the_right_argument_of H)

proof end;

theorem Th7: :: MODELC_2:7

for H being LTL-formula st H is disjunctive holds

H = (the_left_argument_of H) 'or' (the_right_argument_of H)

H = (the_left_argument_of H) 'or' (the_right_argument_of H)

proof end;

theorem Th8: :: MODELC_2:8

for H being LTL-formula st H is Until holds

H = (the_left_argument_of H) 'U' (the_right_argument_of H)

H = (the_left_argument_of H) 'U' (the_right_argument_of H)

proof end;

theorem Th9: :: MODELC_2:9

for H being LTL-formula st H is Release holds

H = (the_left_argument_of H) 'R' (the_right_argument_of H)

H = (the_left_argument_of H) 'R' (the_right_argument_of H)

proof end;

theorem Th10: :: MODELC_2:10

for H being LTL-formula st ( H is negative or H is next ) holds

( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H )

( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H )

proof end;

theorem Th11: :: MODELC_2:11

for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds

( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

proof end;

::

:: The Immediate Constituents of LTL-formulae

::

:: The Immediate Constituents of LTL-formulae

::

:: deftheorem Def21 defines is_immediate_constituent_of MODELC_2:def 21 :

for H, F being LTL-formula holds

( H is_immediate_constituent_of F iff ( F = 'not' H or F = 'X' H or ex H1 being LTL-formula st

( F = H '&' H1 or F = H1 '&' H or F = H 'or' H1 or F = H1 'or' H or F = H 'U' H1 or F = H1 'U' H or F = H 'R' H1 or F = H1 'R' H ) ) );

for H, F being LTL-formula holds

( H is_immediate_constituent_of F iff ( F = 'not' H or F = 'X' H or ex H1 being LTL-formula st

( F = H '&' H1 or F = H1 '&' H or F = H 'or' H1 or F = H1 'or' H or F = H 'U' H1 or F = H1 'U' H or F = H 'R' H1 or F = H1 'R' H ) ) );

theorem Th12: :: MODELC_2:12

for F, G being LTL-formula holds

( ('not' F) . 1 = 0 & (F '&' G) . 1 = 1 & (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )

( ('not' F) . 1 = 0 & (F '&' G) . 1 = 1 & (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )

proof end;

theorem Th15: :: MODELC_2:15

for H, F, G being LTL-formula holds

( H is_immediate_constituent_of F '&' G iff ( H = F or H = G ) )

( H is_immediate_constituent_of F '&' G iff ( H = F or H = G ) )

proof end;

theorem Th16: :: MODELC_2:16

for H, F, G being LTL-formula holds

( H is_immediate_constituent_of F 'or' G iff ( H = F or H = G ) )

( H is_immediate_constituent_of F 'or' G iff ( H = F or H = G ) )

proof end;

theorem Th17: :: MODELC_2:17

for H, F, G being LTL-formula holds

( H is_immediate_constituent_of F 'U' G iff ( H = F or H = G ) )

( H is_immediate_constituent_of F 'U' G iff ( H = F or H = G ) )

proof end;

theorem Th18: :: MODELC_2:18

for H, F, G being LTL-formula holds

( H is_immediate_constituent_of F 'R' G iff ( H = F or H = G ) )

( H is_immediate_constituent_of F 'R' G iff ( H = F or H = G ) )

proof end;

theorem Th20: :: MODELC_2:20

for F, H being LTL-formula st F is negative holds

( H is_immediate_constituent_of F iff H = the_argument_of F )

( H is_immediate_constituent_of F iff H = the_argument_of F )

proof end;

theorem Th21: :: MODELC_2:21

for F, H being LTL-formula st F is next holds

( H is_immediate_constituent_of F iff H = the_argument_of F )

( H is_immediate_constituent_of F iff H = the_argument_of F )

proof end;

theorem Th22: :: MODELC_2:22

for F, H being LTL-formula st F is conjunctive holds

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

proof end;

theorem Th23: :: MODELC_2:23

for F, H being LTL-formula st F is disjunctive holds

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

proof end;

theorem Th24: :: MODELC_2:24

for F, H being LTL-formula st F is Until holds

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

proof end;

theorem Th25: :: MODELC_2:25

for F, H being LTL-formula st F is Release holds

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )

proof end;

theorem :: MODELC_2:26

for H, F being LTL-formula holds

( not H is_immediate_constituent_of F or F is negative or F is next or F is conjunctive or F is disjunctive or F is Until or F is Release ) by Th2, Th19;

( not H is_immediate_constituent_of F or F is negative or F is next or F is conjunctive or F is disjunctive or F is Until or F is Release ) by Th2, Th19;

definition

let H, F be LTL-formula;

for H being LTL-formula ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = H & ( for k being Nat st 1 <= k & k < n holds

ex H1, F1 being LTL-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )

end;
pred H is_subformula_of F means :Def22: :: MODELC_2:def 22

ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds

ex H1, F1 being LTL-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) );

reflexivity ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds

ex H1, F1 being LTL-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) );

for H being LTL-formula ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = H & ( for k being Nat st 1 <= k & k < n holds

ex H1, F1 being LTL-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )

proof end;

:: deftheorem Def22 defines is_subformula_of MODELC_2:def 22 :

for H, F being LTL-formula holds

( H is_subformula_of F iff ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds

ex H1, F1 being LTL-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );

for H, F being LTL-formula holds

( H is_subformula_of F iff ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds

ex H1, F1 being LTL-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );

definition

let H, F be LTL-formula;

irreflexivity

for H being LTL-formula holds

( not H is_subformula_of H or not H <> H ) ;

end;
irreflexivity

for H being LTL-formula holds

( not H is_subformula_of H or not H <> H ) ;

:: deftheorem Def23 defines is_proper_subformula_of MODELC_2:def 23 :

for H, F being LTL-formula holds

( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );

for H, F being LTL-formula holds

( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );

theorem :: MODELC_2:30

for G being LTL-formula st ( G is negative or G is next ) holds

the_argument_of G is_subformula_of G

the_argument_of G is_subformula_of G

proof end;

theorem :: MODELC_2:31

for G being LTL-formula st ( G is conjunctive or G is disjunctive or G is Until or G is Release ) holds

( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G )

( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G )

proof end;

theorem :: MODELC_2:33

for H, F being LTL-formula st H is_proper_subformula_of F holds

ex G being LTL-formula st G is_immediate_constituent_of F

ex G being LTL-formula st G is_immediate_constituent_of F

proof end;

theorem Th34: :: MODELC_2:34

for F, G, H being LTL-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds

F is_proper_subformula_of H

F is_proper_subformula_of H

proof end;

theorem Th35: :: MODELC_2:35

for F, G, H being LTL-formula st F is_subformula_of G & G is_subformula_of H holds

F is_subformula_of H

F is_subformula_of H

proof end;

theorem Th37: :: MODELC_2:37

for G, F being LTL-formula st ( G is negative or G is next ) & F is_proper_subformula_of G holds

F is_subformula_of the_argument_of G

F is_subformula_of the_argument_of G

proof end;

theorem Th38: :: MODELC_2:38

for G, F being LTL-formula st ( G is conjunctive or G is disjunctive or G is Until or G is Release ) & F is_proper_subformula_of G & not F is_subformula_of the_left_argument_of G holds

F is_subformula_of the_right_argument_of G

F is_subformula_of the_right_argument_of G

proof end;

theorem :: MODELC_2:41

for F, G, H being LTL-formula holds

( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )

( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )

proof end;

theorem :: MODELC_2:42

for F, G, H being LTL-formula holds

( not F is_proper_subformula_of G 'or' H or F is_subformula_of G or F is_subformula_of H )

( not F is_proper_subformula_of G 'or' H or F is_subformula_of G or F is_subformula_of H )

proof end;

theorem :: MODELC_2:43

for F, G, H being LTL-formula holds

( not F is_proper_subformula_of G 'U' H or F is_subformula_of G or F is_subformula_of H )

( not F is_proper_subformula_of G 'U' H or F is_subformula_of G or F is_subformula_of H )

proof end;

theorem :: MODELC_2:44

for F, G, H being LTL-formula holds

( not F is_proper_subformula_of G 'R' H or F is_subformula_of G or F is_subformula_of H )

( not F is_proper_subformula_of G 'R' H or F is_subformula_of G or F is_subformula_of H )

proof end;

::

:: The Set of Subformulae of LTL-formulae

::

:: The Set of Subformulae of LTL-formulae

::

definition

let H be LTL-formula;

ex b_{1} being set st

for a being set holds

( a in b_{1} iff ex F being LTL-formula st

( F = a & F is_subformula_of H ) )

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

( a in b_{1} iff ex F being LTL-formula st

( F = a & F is_subformula_of H ) ) ) & ( for a being set holds

( a in b_{2} iff ex F being LTL-formula st

( F = a & F is_subformula_of H ) ) ) holds

b_{1} = b_{2}

end;
func Subformulae H -> set means :Def24: :: MODELC_2:def 24

for a being set holds

( a in it iff ex F being LTL-formula st

( F = a & F is_subformula_of H ) );

existence for a being set holds

( a in it iff ex F being LTL-formula st

( F = a & F is_subformula_of H ) );

ex b

for a being set holds

( a in b

( F = a & F is_subformula_of H ) )

proof end;

uniqueness for b

( a in b

( F = a & F is_subformula_of H ) ) ) & ( for a being set holds

( a in b

( F = a & F is_subformula_of H ) ) ) holds

b

proof end;

:: deftheorem Def24 defines Subformulae MODELC_2:def 24 :

for H being LTL-formula

for b_{2} being set holds

( b_{2} = Subformulae H iff for a being set holds

( a in b_{2} iff ex F being LTL-formula st

( F = a & F is_subformula_of H ) ) );

for H being LTL-formula

for b

( b

( a in b

( F = a & F is_subformula_of H ) ) );

theorem :: MODELC_2:47

for a being set

for H being LTL-formula st a is Subset of (Subformulae H) holds

a is Subset of LTL_WFF

for H being LTL-formula st a is Subset of (Subformulae H) holds

a is Subset of LTL_WFF

proof end;

scheme :: MODELC_2:sch 1

LTLInd{ P_{1}[ LTL-formula] } :

provided

LTLInd{ P

provided

A1:
for H being LTL-formula st H is atomic holds

P_{1}[H]
and

A2: for H being LTL-formula st ( H is negative or H is next ) & P_{1}[ the_argument_of H] holds

P_{1}[H]
and

A3: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & P_{1}[ the_left_argument_of H] & P_{1}[ the_right_argument_of H] holds

P_{1}[H]

P

A2: for H being LTL-formula st ( H is negative or H is next ) & P

P

A3: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & P

P

proof end;

scheme :: MODELC_2:sch 2

LTLCompInd{ P_{1}[ LTL-formula] } :

provided

LTLCompInd{ P

provided

A1:
for H being LTL-formula st ( for F being LTL-formula st F is_proper_subformula_of H holds

P_{1}[F] ) holds

P_{1}[H]

P

P

proof end;

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

::**

::** definition of LTL model structure.

::**

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

::**

::** definition of LTL model structure.

::**

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

definition

let x be set ;

correctness

coherence

( ( x in LTL_WFF implies x is LTL-formula ) & ( not x in LTL_WFF implies atom. 0 is LTL-formula ) );

consistency

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

by Th1;

end;
correctness

coherence

( ( x in LTL_WFF implies x is LTL-formula ) & ( not x in LTL_WFF implies atom. 0 is LTL-formula ) );

consistency

for b

by Th1;

:: deftheorem Def25 defines CastLTL MODELC_2:def 25 :

for x being set holds

( ( x in LTL_WFF implies CastLTL x = x ) & ( not x in LTL_WFF implies CastLTL x = atom. 0 ) );

for x being set holds

( ( x in LTL_WFF implies CastLTL x = x ) & ( not x in LTL_WFF implies CastLTL x = atom. 0 ) );

definition

attr c_{1} is strict ;

struct LTLModelStr -> OrthoLattStr ;

aggr LTLModelStr(# carrier, BasicAssign, L_meet, L_join, Compl, NEXT, UNTIL, RELEASE #) -> LTLModelStr ;

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

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

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

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

end;
struct LTLModelStr -> OrthoLattStr ;

aggr LTLModelStr(# carrier, BasicAssign, L_meet, L_join, Compl, NEXT, UNTIL, RELEASE #) -> LTLModelStr ;

sel BasicAssign c

sel NEXT c

sel UNTIL c

sel RELEASE c

:: Preparation to define semantics for LTL-language

:: definition of evaluate function of LTL

:: definition of evaluate function of LTL

definition

coherence

{ x where x is LTL-formula : x is atomic } is Subset of LTL_WFF;

end;

func atomic_LTL -> Subset of LTL_WFF equals :: MODELC_2:def 26

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

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

coherence

{ x where x is LTL-formula : x is atomic } is Subset of LTL_WFF;

proof end;

:: deftheorem defines atomic_LTL MODELC_2:def 26 :

atomic_LTL = { x where x is LTL-formula : x is atomic } ;

atomic_LTL = { x where x is LTL-formula : x is atomic } ;

definition

let V be LTLModelStr ;

let Kai be Function of atomic_LTL, the BasicAssign of V;

let f be Function of LTL_WFF, the carrier of V;

end;
let Kai be Function of atomic_LTL, the BasicAssign of V;

let f be Function of LTL_WFF, the carrier of V;

pred f is-Evaluation-for Kai means :Def27: :: MODELC_2:def 27

for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

:: deftheorem Def27 defines is-Evaluation-for MODELC_2:def 27 :

for V being LTLModelStr

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V holds

( f is-Evaluation-for Kai iff for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) );

for V being LTLModelStr

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V holds

( f is-Evaluation-for Kai iff for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) );

definition

let V be LTLModelStr ;

let Kai be Function of atomic_LTL, the BasicAssign of V;

let f be Function of LTL_WFF, the carrier of V;

let n be Nat;

end;
let Kai be Function of atomic_LTL, the BasicAssign of V;

let f be Function of LTL_WFF, the carrier of V;

let n be Nat;

pred f is-PreEvaluation-for n,Kai means :Def28: :: MODELC_2:def 28

for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

:: deftheorem Def28 defines is-PreEvaluation-for MODELC_2:def 28 :

for V being LTLModelStr

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V

for n being Nat holds

( f is-PreEvaluation-for n,Kai iff for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) );

for V being LTLModelStr

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V

for n being Nat holds

( f is-PreEvaluation-for n,Kai iff for H being LTL-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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) );

definition

let V be LTLModelStr ;

let Kai be Function of atomic_LTL, the BasicAssign of V;

let f, h be Function of LTL_WFF, the carrier of V;

let n be Nat;

let H be LTL-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 disjunctive implies the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is next implies the NEXT of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is Until implies the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is Release implies the RELEASE 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 disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & 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 disjunctive implies ( b_{1} = f . H iff b_{1} = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H = n + 1 & H is next implies ( b_{1} = f . H iff b_{1} = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is Until implies ( b_{1} = f . H iff b_{1} = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H = n + 1 & H is Release implies ( b_{1} = f . H iff b_{1} = the RELEASE 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 disjunctive implies ( b_{1} = Kai . H iff b_{1} = the L_join 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 next implies ( b_{1} = Kai . H iff b_{1} = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is Until implies ( b_{1} = Kai . H iff b_{1} = the UNTIL 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 Release implies ( b_{1} = Kai . H iff b_{1} = the RELEASE 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 disjunctive implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = the L_join 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 next implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Until implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = the UNTIL 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 Release implies ( b_{1} = the Compl of V . (h . (the_argument_of H)) iff b_{1} = the RELEASE 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 disjunctive implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the L_join 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 & H is next implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Until implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the UNTIL 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 & H is Release implies ( b_{1} = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the RELEASE 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 disjunctive & len H = n + 1 & H is next implies ( b_{1} = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Until implies ( b_{1} = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Release implies ( b_{1} = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is disjunctive & len H < n + 1 implies ( b_{1} = the L_join 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 next & len H = n + 1 & H is Until implies ( b_{1} = the NEXT of V . (h . (the_argument_of H)) iff b_{1} = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is next & len H = n + 1 & H is Release implies ( b_{1} = the NEXT of V . (h . (the_argument_of H)) iff b_{1} = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is next & len H < n + 1 implies ( b_{1} = the NEXT of V . (h . (the_argument_of H)) iff b_{1} = h . H ) ) & ( len H = n + 1 & H is Until & len H = n + 1 & H is Release implies ( b_{1} = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is Until & len H < n + 1 implies ( b_{1} = the UNTIL 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 Release & len H < n + 1 implies ( b_{1} = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b_{1} = h . H ) ) )
by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21;

end;
let Kai be Function of atomic_LTL, the BasicAssign of V;

let f, h be Function of LTL_WFF, the carrier of V;

let n be Nat;

let H be LTL-formula;

func GraftEval (V,Kai,f,h,n,H) -> set equals :Def29: :: MODELC_2:def 29

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 L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is disjunctive )

the NEXT of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is next )

the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is Until )

the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is Release )

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 L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is disjunctive )

the NEXT of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is next )

the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is Until )

the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is Release )

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 disjunctive implies the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is next implies the NEXT of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is Until implies the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is Release implies the RELEASE 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 disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & 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 Def29 defines GraftEval MODELC_2:def 29 :

for V being LTLModelStr

for Kai being Function of atomic_LTL, the BasicAssign of V

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

for n being Nat

for H being LTL-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 disjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is next implies GraftEval (V,Kai,f,h,n,H) = the NEXT of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is Until implies GraftEval (V,Kai,f,h,n,H) = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is Release implies GraftEval (V,Kai,f,h,n,H) = the RELEASE 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 disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) );

for V being LTLModelStr

for Kai being Function of atomic_LTL, the BasicAssign of V

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

for n being Nat

for H being LTL-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 disjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is next implies GraftEval (V,Kai,f,h,n,H) = the NEXT of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is Until implies GraftEval (V,Kai,f,h,n,H) = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is Release implies GraftEval (V,Kai,f,h,n,H) = the RELEASE 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 disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) );

:: deftheorem Def30 defines with_basic MODELC_2:def 30 :

for C being LTLModelStr holds

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

for C being LTLModelStr holds

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

definition

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

end;

func TrivialLTLModel -> LTLModelStr equals :: MODELC_2:def 31

LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #);

coherence LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #);

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

:: deftheorem defines TrivialLTLModel MODELC_2:def 31 :

TrivialLTLModel = LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #);

TrivialLTLModel = LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #);

registration

coherence

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

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

proof end;

Lm22: for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V holds f is-PreEvaluation-for 0 ,Kai

proof end;

Lm23: for n being Nat

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds

f is-PreEvaluation-for n,Kai

proof end;

Lm24: for n being Nat

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai holds

f is-PreEvaluation-for n,Kai

proof end;

Lm25: for n being Nat

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for f1, f2 being Function of LTL_WFF, the carrier of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds

for H being LTL-formula st len H <= n holds

f1 . H = f2 . H

proof end;

Lm26: for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for n being Nat ex f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai

proof end;

Lm27: for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for f being Function of LTL_WFF, the carrier of V st ( for n being Nat holds f is-PreEvaluation-for n,Kai ) holds

f is-Evaluation-for Kai

proof end;

definition

let V be LTLModel;

let Kai be Function of atomic_LTL, the BasicAssign of V;

let n be Nat;

coherence

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

end;
let Kai be Function of atomic_LTL, the BasicAssign of V;

let n be Nat;

func EvalSet (V,Kai,n) -> non empty set equals :: MODELC_2:def 32

{ h where h is Function of LTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;

correctness { h where h is Function of LTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;

coherence

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

proof end;

:: deftheorem defines EvalSet MODELC_2:def 32 :

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for n being Nat holds EvalSet (V,Kai,n) = { h where h is Function of LTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for n being Nat holds EvalSet (V,Kai,n) = { h where h is Function of LTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;

definition

let V be LTLModel;

let v0 be Element of the carrier of V;

let x be set ;

coherence

( ( x in Funcs (LTL_WFF, the carrier of V) implies x is Function of LTL_WFF, the carrier of V ) & ( not x in Funcs (LTL_WFF, the carrier of V) implies LTL_WFF --> v0 is Function of LTL_WFF, the carrier of V ) );

consistency

for b_{1} being Function of LTL_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 LTL_WFF, the carrier of V equals :Def33: :: MODELC_2:def 33

x if x in Funcs (LTL_WFF, the carrier of V)

otherwise LTL_WFF --> v0;

correctness x if x in Funcs (LTL_WFF, the carrier of V)

otherwise LTL_WFF --> v0;

coherence

( ( x in Funcs (LTL_WFF, the carrier of V) implies x is Function of LTL_WFF, the carrier of V ) & ( not x in Funcs (LTL_WFF, the carrier of V) implies LTL_WFF --> v0 is Function of LTL_WFF, the carrier of V ) );

consistency

for b

by FUNCT_2:66;

:: deftheorem Def33 defines CastEval MODELC_2:def 33 :

for V being LTLModel

for v0 being Element of the carrier of V

for x being set holds

( ( x in Funcs (LTL_WFF, the carrier of V) implies CastEval (V,x,v0) = x ) & ( not x in Funcs (LTL_WFF, the carrier of V) implies CastEval (V,x,v0) = LTL_WFF --> v0 ) );

for V being LTLModel

for v0 being Element of the carrier of V

for x being set holds

( ( x in Funcs (LTL_WFF, the carrier of V) implies CastEval (V,x,v0) = x ) & ( not x in Funcs (LTL_WFF, the carrier of V) implies CastEval (V,x,v0) = LTL_WFF --> v0 ) );

definition

let V be LTLModel;

let Kai be Function of atomic_LTL, 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 (LTL_WFF, the carrier of V)) & ex n being 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 (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) & ( for p being set holds

( p in b_{2} iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) holds

b_{1} = b_{2}

end;
let Kai be Function of atomic_LTL, the BasicAssign of V;

func EvalFamily (V,Kai) -> non empty set means :Def34: :: MODELC_2:def 34

for p being set holds

( p in it iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) );

existence for p being set holds

( p in it iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being 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 Def34 defines EvalFamily MODELC_2:def 34 :

for V being LTLModel

for Kai being Function of atomic_LTL, 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 (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) );

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for b

( b

( p in b

Lm28: for n being Nat

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)

proof end;

theorem Th48: :: MODELC_2:48

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V ex f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai

for Kai being Function of atomic_LTL, the BasicAssign of V ex f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai

proof end;

theorem Th49: :: MODELC_2:49

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for f1, f2 being Function of LTL_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_LTL, the BasicAssign of V

for f1, f2 being Function of LTL_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 LTLModel;

let Kai be Function of atomic_LTL, the BasicAssign of V;

let H be LTL-formula;

ex b_{1} being Assign of V ex f being Function of LTL_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 LTL_WFF, the carrier of V st

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

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

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

end;
let Kai be Function of atomic_LTL, the BasicAssign of V;

let H be LTL-formula;

func Evaluate (H,Kai) -> Assign of V means :Def35: :: MODELC_2:def 35

ex f being Function of LTL_WFF, the carrier of V st

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

existence ex f being Function of LTL_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 Def35 defines Evaluate MODELC_2:def 35 :

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for H being LTL-formula

for b_{4} being Assign of V holds

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

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

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V

for H being LTL-formula

for b

( b

( f is-Evaluation-for Kai & b

notation

let V be LTLModel;

let f be Assign of V;

synonym 'not' f for f ` ;

let g be Assign of V;

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

synonym f 'or' 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;

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

definition
end;

:: deftheorem defines 'X' MODELC_2:def 36 :

for V being LTLModel

for f being Assign of V holds 'X' f = the NEXT of V . f;

for V being LTLModel

for f being Assign of V holds 'X' f = the NEXT of V . f;

definition

let V be LTLModel;

let f, g be Assign of V;

correctness

coherence

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

;

correctness

coherence

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

;

end;
let f, g be Assign of V;

correctness

coherence

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

;

correctness

coherence

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

;

:: deftheorem defines 'U' MODELC_2:def 37 :

for V being LTLModel

for f, g being Assign of V holds f 'U' g = the UNTIL of V . (f,g);

for V being LTLModel

for f, g being Assign of V holds f 'U' g = the UNTIL of V . (f,g);

:: deftheorem defines 'R' MODELC_2:def 38 :

for V being LTLModel

for f, g being Assign of V holds f 'R' g = the RELEASE of V . (f,g);

for V being LTLModel

for f, g being Assign of V holds f 'R' g = the RELEASE of V . (f,g);

::Some properties of evaluate function of LTL

theorem Th50: :: MODELC_2:50

for H being LTL-formula

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))

proof end;

theorem Th51: :: MODELC_2:51

for H1, H2 being LTL-formula

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 '&' H2),Kai) = (Evaluate (H1,Kai)) '&' (Evaluate (H2,Kai))

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 '&' H2),Kai) = (Evaluate (H1,Kai)) '&' (Evaluate (H2,Kai))

proof end;

theorem Th52: :: MODELC_2:52

for H1, H2 being LTL-formula

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))

proof end;

theorem Th53: :: MODELC_2:53

for H being LTL-formula

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('X' H),Kai) = 'X' (Evaluate (H,Kai))

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('X' H),Kai) = 'X' (Evaluate (H,Kai))

proof end;

theorem Th54: :: MODELC_2:54

for H1, H2 being LTL-formula

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 'U' H2),Kai) = (Evaluate (H1,Kai)) 'U' (Evaluate (H2,Kai))

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 'U' H2),Kai) = (Evaluate (H1,Kai)) 'U' (Evaluate (H2,Kai))

proof end;

theorem Th55: :: MODELC_2:55

for H1, H2 being LTL-formula

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 'R' H2),Kai) = (Evaluate (H1,Kai)) 'R' (Evaluate (H2,Kai))

for V being LTLModel

for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate ((H1 'R' H2),Kai) = (Evaluate (H1,Kai)) 'R' (Evaluate (H2,Kai))

proof end;

::definition of concrete object of LTL model

:: deftheorem defines Inf_seq MODELC_2:def 39 :

for S being non empty set holds Inf_seq S = Funcs (NAT,S);

for S being non empty set holds Inf_seq S = Funcs (NAT,S);

definition

let S be non empty set ;

let t be sequence of S;

correctness

coherence

t is Element of Inf_seq S;

by FUNCT_2:8;

end;
let t be sequence of S;

correctness

coherence

t is Element of Inf_seq S;

by FUNCT_2:8;

:: deftheorem defines CastSeq MODELC_2:def 40 :

for S being non empty set

for t being sequence of S holds CastSeq t = t;

for S being non empty set

for t being sequence of S holds CastSeq t = t;

definition

let S be non empty set ;

let t be set ;

assume A1: t is Element of Inf_seq S ;

correctness

coherence

t is sequence of S;

by A1, FUNCT_2:66;

end;
let t be set ;

assume A1: t is Element of Inf_seq S ;

correctness

coherence

t is sequence of S;

by A1, FUNCT_2:66;

:: deftheorem Def41 defines CastSeq MODELC_2:def 41 :

for S being non empty set

for t being set st t is Element of Inf_seq S holds

CastSeq (t,S) = t;

for S being non empty set

for t being set st t is Element of Inf_seq S holds

CastSeq (t,S) = t;

definition

let S be non empty set ;

let t be set ;

let k be Nat;

coherence

CastSeq ((CastSeq (t,S)) ^\ k) is Element of Inf_seq S;

;

end;
let t be set ;

let k be Nat;

func Shift (t,k,S) -> Element of Inf_seq S equals :: MODELC_2:def 42

CastSeq ((CastSeq (t,S)) ^\ k);

correctness CastSeq ((CastSeq (t,S)) ^\ k);

coherence

CastSeq ((CastSeq (t,S)) ^\ k) is Element of Inf_seq S;

;

:: deftheorem defines Shift MODELC_2:def 42 :

for S being non empty set

for t being set

for k being Nat holds Shift (t,k,S) = CastSeq ((CastSeq (t,S)) ^\ k);

for S being non empty set

for t being set

for k being Nat holds Shift (t,k,S) = CastSeq ((CastSeq (t,S)) ^\ k);

definition

let S be non empty set ;

let t be Element of Inf_seq S;

let k be Nat;

correctness

coherence

Shift (t,k,S) is Element of Inf_seq S;

;

end;
let t be Element of Inf_seq S;

let k be Nat;

correctness

coherence

Shift (t,k,S) is Element of Inf_seq S;

;

:: deftheorem defines Shift MODELC_2:def 43 :

for S being non empty set

for t being Element of Inf_seq S

for k being Nat holds Shift (t,k) = Shift (t,k,S);

for S being non empty set

for t being Element of Inf_seq S

for k being Nat holds Shift (t,k) = Shift (t,k,S);

Lm29: for S being non empty set

for seq being Element of Inf_seq S holds Shift (seq,0) = seq

proof end;

Lm30: for k, n being Nat

for S being non empty set

for seq being Element of Inf_seq S holds Shift ((Shift (seq,k)),n) = Shift (seq,(n + k))

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 (Inf_seq S) st

for t being set st t in Inf_seq S holds

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

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

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

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

b_{1} = b_{2}

end;
let f be set ;

func Not_0 (f,S) -> Element of ModelSP (Inf_seq S) means :Def44: :: MODELC_2:def 44

for t being set st t in Inf_seq S holds

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

existence for t being set st t in Inf_seq S holds

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

ex b

for t being set st t in Inf_seq S holds

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def44 defines Not_0 MODELC_2:def 44 :

for S being non empty set

for f being set

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

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

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

for S being non empty set

for f being set

for b

( b

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

Lm31: for S being non empty set

for o1, o2 being UnOp of (ModelSP (Inf_seq S)) st ( for f being set st f in ModelSP (Inf_seq S) holds

o1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP (Inf_seq 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 (Inf_seq S)) st

for f being set st f in ModelSP (Inf_seq S) holds

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

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

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

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

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

end;
func Not_ S -> UnOp of (ModelSP (Inf_seq S)) means :Def45: :: MODELC_2:def 45

for f being set st f in ModelSP (Inf_seq S) holds

it . f = Not_0 (f,S);

existence for f being set st f in ModelSP (Inf_seq S) holds

it . f = Not_0 (f,S);

ex b

for f being set st f in ModelSP (Inf_seq S) holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def45 defines Not_ MODELC_2:def 45 :

for S being non empty set

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

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

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

for S being non empty set

for b

( b

b

:: definition of next_ unary operation of Model Space.

definition

let S be non empty set ;

let f be Function of (Inf_seq S),BOOLEAN;

let t be set ;

coherence

( ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE implies TRUE is Element of BOOLEAN ) & ( ( not t is Element of Inf_seq S or not f . (Shift (t,1,S)) = TRUE ) implies FALSE is Element of BOOLEAN ) );

consistency

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

;

end;
let f be Function of (Inf_seq S),BOOLEAN;

let t be set ;

func Next_univ (t,f) -> Element of BOOLEAN equals :Def46: :: MODELC_2:def 46

TRUE if ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE )

otherwise FALSE ;

correctness TRUE if ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE )

otherwise FALSE ;

coherence

( ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE implies TRUE is Element of BOOLEAN ) & ( ( not t is Element of Inf_seq S or not f . (Shift (t,1,S)) = TRUE ) implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def46 defines Next_univ MODELC_2:def 46 :

for S being non empty set

for f being Function of (Inf_seq S),BOOLEAN

for t being set holds

( ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE implies Next_univ (t,f) = TRUE ) & ( ( not t is Element of Inf_seq S or not f . (Shift (t,1,S)) = TRUE ) implies Next_univ (t,f) = FALSE ) );

for S being non empty set

for f being Function of (Inf_seq S),BOOLEAN

for t being set holds

( ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE implies Next_univ (t,f) = TRUE ) & ( ( not t is Element of Inf_seq S or not f . (Shift (t,1,S)) = TRUE ) implies Next_univ (t,f) = FALSE ) );

definition

let S be non empty set ;

let f be set ;

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

for t being set st t in Inf_seq S holds

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b_{1},(Inf_seq S))) . t = TRUE )

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

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b_{1},(Inf_seq S))) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b_{2},(Inf_seq S))) . t = TRUE ) ) holds

b_{1} = b_{2}

end;
let f be set ;

func Next_0 (f,S) -> Element of ModelSP (Inf_seq S) means :Def47: :: MODELC_2:def 47

for t being set st t in Inf_seq S holds

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE );

existence for t being set st t in Inf_seq S holds

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE );

ex b

for t being set st t in Inf_seq S holds

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b

proof end;

uniqueness for b

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b

b

proof end;

:: deftheorem Def47 defines Next_0 MODELC_2:def 47 :

for S being non empty set

for f being set

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

( b_{3} = Next_0 (f,S) iff for t being set st t in Inf_seq S holds

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b_{3},(Inf_seq S))) . t = TRUE ) );

for S being non empty set

for f being set

for b

( b

( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b

Lm32: for S being non empty set

for o1, o2 being UnOp of (ModelSP (Inf_seq S)) st ( for f being set st f in ModelSP (Inf_seq S) holds

o1 . f = Next_0 (f,S) ) & ( for f being set st f in ModelSP (Inf_seq S) holds

o2 . f = Next_0 (f,S) ) holds

o1 = o2

proof end;

definition

let S be non empty set ;

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

for f being set st f in ModelSP (Inf_seq S) holds

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

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

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

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

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

end;
func Next_ S -> UnOp of (ModelSP (Inf_seq S)) means :Def48: :: MODELC_2:def 48

for f being set st f in ModelSP (Inf_seq S) holds

it . f = Next_0 (f,S);

existence for f being set st f in ModelSP (Inf_seq S) holds

it . f = Next_0 (f,S);

ex b

for f being set st f in ModelSP (Inf_seq S) holds

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def48 defines Next_ MODELC_2:def 48 :

for S being non empty set

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

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

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

for S being non empty set

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 (Inf_seq S) st

for t being set st t in Inf_seq S holds

( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b_{1},(Inf_seq S))) . t = TRUE )

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

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

( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b_{2},(Inf_seq S))) . t = TRUE ) ) holds

b_{1} = b_{2}

end;
let f, g be set ;

func And_0 (f,g,S) -> Element of ModelSP (Inf_seq S) means :Def49: :: MODELC_2:def 49

for t being set st t in Inf_seq S holds

( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE );

existence for t being set st t in Inf_seq S holds

( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE );

ex b

for t being set st t in Inf_seq S holds

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def49 defines And_0 MODELC_2:def 49 :

for S being non empty set

for f, g being set

for b_{4} being Element of ModelSP (Inf_seq S) holds

( b_{4} = And_0 (f,g,S) iff for t being set st t in Inf_seq S holds

( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b_{4},(Inf_seq S))) . t = TRUE ) );

for S being non empty set

for f, g being set

for b

( b

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

Lm33: for S being non empty set

for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq 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 (Inf_seq S)) st

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

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

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

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

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

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

end;
func And_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def50: :: MODELC_2:def 50

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

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

existence for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

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

ex b

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

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def50 defines And_ MODELC_2:def 50 :

for S being non empty set

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

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

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

for S being non empty set

for b

( b

b

:: definition of Until_ Binary Operation of Model Space.

definition

let S be non empty set ;

let f, g be Function of (Inf_seq S),BOOLEAN;

let t be set ;

coherence

( ( t is Element of Inf_seq S & ex m being Nat st

( ( for j being Nat st j < m holds

f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) implies TRUE is Element of BOOLEAN ) & ( ( not t is Element of Inf_seq S or for m being Nat holds

( ex j being Nat st

( j < m & not f . (Shift (t,j,S)) = TRUE ) or not g . (Shift (t,m,S)) = TRUE ) ) implies FALSE is Element of BOOLEAN ) );

consistency

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

;

end;
let f, g be Function of (Inf_seq S),BOOLEAN;

let t be set ;

func Until_univ (t,f,g,S) -> Element of BOOLEAN equals :Def51: :: MODELC_2:def 51

TRUE if ( t is Element of Inf_seq S & ex m being Nat st

( ( for j being Nat st j < m holds

f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) )

otherwise FALSE ;

correctness TRUE if ( t is Element of Inf_seq S & ex m being Nat st

( ( for j being Nat st j < m holds

f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) )

otherwise FALSE ;

coherence

( ( t is Element of Inf_seq S & ex m being Nat st

( ( for j being Nat st j < m holds

f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) implies TRUE is Element of BOOLEAN ) & ( ( not t is Element of Inf_seq S or for m being Nat holds

( ex j being Nat st

( j < m & not f . (Shift (t,j,S)) = TRUE ) or not g . (Shift (t,m,S)) = TRUE ) ) implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def51 defines Until_univ MODELC_2:def 51 :

for S being non empty set

for f, g being Function of (Inf_seq S),BOOLEAN

for t being set holds

( ( t is Element of Inf_seq S & ex m being Nat st

( ( for j being Nat st j < m holds

f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) implies Until_univ (t,f,g,S) = TRUE ) & ( ( not t is Element of Inf_seq S or for m being Nat holds

( ex j being Nat st

( j < m & not f . (Shift (t,j,S)) = TRUE ) or not g . (Shift (t,m,S)) = TRUE ) ) implies Until_univ (t,f,g,S) = FALSE ) );

for S being non empty set

for f, g being Function of (Inf_seq S),BOOLEAN

for t being set holds

( ( t is Element of Inf_seq S & ex m being Nat st

( ( for j being Nat st j < m holds

f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) implies Until_univ (t,f,g,S) = TRUE ) & ( ( not t is Element of Inf_seq S or for m being Nat holds

( ex j being Nat st

( j < m & not f . (Shift (t,j,S)) = TRUE ) or not g . (Shift (t,m,S)) = TRUE ) ) implies Until_univ (t,f,g,S) = FALSE ) );

definition

let S be non empty set ;

let f, g be set ;

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

for t being set st t in Inf_seq S holds

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b_{1},(Inf_seq S))) . t = TRUE )

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

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b_{1},(Inf_seq S))) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b_{2},(Inf_seq S))) . t = TRUE ) ) holds

b_{1} = b_{2}

end;
let f, g be set ;

func Until_0 (f,g,S) -> Element of ModelSP (Inf_seq S) means :Def52: :: MODELC_2:def 52

for t being set st t in Inf_seq S holds

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE );

existence for t being set st t in Inf_seq S holds

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE );

ex b

for t being set st t in Inf_seq S holds

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b

proof end;

uniqueness for b

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b

b

proof end;

:: deftheorem Def52 defines Until_0 MODELC_2:def 52 :

for S being non empty set

for f, g being set

for b_{4} being Element of ModelSP (Inf_seq S) holds

( b_{4} = Until_0 (f,g,S) iff for t being set st t in Inf_seq S holds

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b_{4},(Inf_seq S))) . t = TRUE ) );

for S being non empty set

for f, g being set

for b

( b

( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b

Lm34: for S being non empty set

for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o1 . (f,g) = Until_0 (f,g,S) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o2 . (f,g) = Until_0 (f,g,S) ) holds

o1 = o2

proof end;

definition

let S be non empty set ;

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

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

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

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

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

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

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

end;
func Until_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def53: :: MODELC_2:def 53

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

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

existence for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

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

ex b

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

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def53 defines Until_ MODELC_2:def 53 :

for S being non empty set

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

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

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

for S being non empty set

for b

( b

b

Lm35: for S being non empty set

for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o1 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o2 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds

o1 = o2

proof end;

Lm36: for S being non empty set

for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o1 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

o2 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds

o1 = o2

proof end;

definition

let S be non empty set ;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end;
func Or_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def54: :: MODELC_2:def 54

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

it . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g)));

existence for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

it . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g)));

ex b

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

b

proof end;

uniqueness for b

b

b

b

func Release_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def55: :: MODELC_2:def 55

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

it . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g)));

existence for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds

it . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g)));

ex b

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

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def54 defines Or_ MODELC_2:def 54 :

for S being non empty set

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

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

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

for S being non empty set

for b

( b

b

:: deftheorem Def55 defines Release_ MODELC_2:def 55 :

for S being non empty set

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

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

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

for S being non empty set

for b

( b

b

:: definition of concrete object of LTL model by ModelSP

definition

let S be non empty set ;

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

LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #) is LTLModelStr ;

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

func Inf_seqModel (S,BASSIGN) -> LTLModelStr equals :: MODELC_2:def 56

LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #);

coherence LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #);

LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #) is LTLModelStr ;

:: deftheorem defines Inf_seqModel MODELC_2:def 56 :

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) holds Inf_seqModel (S,BASSIGN) = LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #);

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) holds Inf_seqModel (S,BASSIGN) = LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #);

registration

let S be non empty set ;

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

coherence

( Inf_seqModel (S,BASSIGN) is with_basic & Inf_seqModel (S,BASSIGN) is strict & not Inf_seqModel (S,BASSIGN) is empty )

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

coherence

( Inf_seqModel (S,BASSIGN) is with_basic & Inf_seqModel (S,BASSIGN) is strict & not Inf_seqModel (S,BASSIGN) is empty )

proof end;

:: definition of correctness of Assign of Inf_seqModel(S,BASSIGN)

definition

let S be non empty set ;

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

let t be Element of Inf_seq S;

let f be Assign of (Inf_seqModel (S,BASSIGN));

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

let t be Element of Inf_seq S;

let f be Assign of (Inf_seqModel (S,BASSIGN));

:: deftheorem Def57 defines |= MODELC_2:def 57 :

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f iff (Fid (f,(Inf_seq S))) . t = TRUE );

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f iff (Fid (f,(Inf_seq S))) . t = TRUE );

notation

let S be non empty set ;

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

let t be Element of Inf_seq S;

let f be Assign of (Inf_seqModel (S,BASSIGN));

antonym t |/= f for t |= f;

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

let t be Element of Inf_seq S;

let f be Assign of (Inf_seqModel (S,BASSIGN));

antonym t |/= f for t |= f;

theorem :: MODELC_2:56

theorem Th57: :: MODELC_2:57

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= 'not' f iff t |/= f )

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= 'not' f iff t |/= f )

proof end;

theorem Th58: :: MODELC_2:58

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f '&' g iff ( t |= f & t |= g ) )

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f '&' g iff ( t |= f & t |= g ) )

proof end;

theorem Th59: :: MODELC_2:59

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= 'X' f iff Shift (t,1) |= f )

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= 'X' f iff Shift (t,1) |= f )

proof end;

theorem Th60: :: MODELC_2:60

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f 'U' g iff ex m being Nat st

( ( for j being Nat st j < m holds

Shift (t,j) |= f ) & Shift (t,m) |= g ) )

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f 'U' g iff ex m being Nat st

( ( for j being Nat st j < m holds

Shift (t,j) |= f ) & Shift (t,m) |= g ) )

proof end;

theorem Th61: :: MODELC_2:61

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f 'or' g iff ( t |= f or t |= g ) )

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f 'or' g iff ( t |= f or t |= g ) )

proof end;

theorem Th62: :: MODELC_2:62

for S being non empty set

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds

Shift (t,j) |= 'not' f ) holds

Shift (t,m) |= g )

for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))

for t being Element of Inf_seq S

for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds

( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds

Shift (t,j) |= 'not' f ) holds

Shift (t,m) |= g )

proof end;

:: definition of correctness of LTL-formula & its basic properties.

definition

let a, t be set ;

coherence

( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies TRUE is Element of BOOLEAN ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies FALSE is Element of BOOLEAN ) );

consistency

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

;

end;
func AtomicFunc (a,t) -> Element of BOOLEAN equals :Def59: :: MODELC_2:def 59

TRUE if ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 )

otherwise FALSE ;

correctness TRUE if ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 )

otherwise FALSE ;

coherence

( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies TRUE is Element of BOOLEAN ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies FALSE is Element of BOOLEAN ) );

consistency

for b

;

:: deftheorem Def59 defines AtomicFunc MODELC_2:def 59 :

for a, t being set holds

( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies AtomicFunc (a,t) = TRUE ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies AtomicFunc (a,t) = FALSE ) );

for a, t being set holds

( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies AtomicFunc (a,t) = TRUE ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies AtomicFunc (a,t) = FALSE ) );

Lm37: for S being non empty set

for f1, f2 being set st f1 in ModelSP S & f2 in ModelSP S & Fid (f1,S) = Fid (f2,S) holds

f1 = f2

proof end;

definition

let a be set ;

ex b_{1} being Element of ModelSP (Inf_seq AtomicFamily) st

for t being set st t in Inf_seq AtomicFamily holds

(Fid (b_{1},(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t)

for b_{1}, b_{2} being Element of ModelSP (Inf_seq AtomicFamily) st ( for t being set st t in Inf_seq AtomicFamily holds

(Fid (b_{1},(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ) & ( for t being set st t in Inf_seq AtomicFamily holds

(Fid (b_{2},(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ) holds

b_{1} = b_{2}

end;
func AtomicAsgn a -> Element of ModelSP (Inf_seq AtomicFamily) means :Def60: :: MODELC_2:def 60

for t being set st t in Inf_seq AtomicFamily holds

(Fid (it,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t);

existence for t being set st t in Inf_seq AtomicFamily holds

(Fid (it,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t);

ex b

for t being set st t in Inf_seq AtomicFamily holds

(Fid (b

proof end;

uniqueness for b

(Fid (b

(Fid (b

b

proof end;

:: deftheorem Def60 defines AtomicAsgn MODELC_2:def 60 :

for a being set

for b_{2} being Element of ModelSP (Inf_seq AtomicFamily) holds

( b_{2} = AtomicAsgn a iff for t being set st t in Inf_seq AtomicFamily holds

(Fid (b_{2},(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) );

for a being set

for b

( b

(Fid (b

definition

coherence

{ x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } is non empty Subset of (ModelSP (Inf_seq AtomicFamily));

end;

func AtomicBasicAsgn -> non empty Subset of (ModelSP (Inf_seq AtomicFamily)) equals :: MODELC_2:def 61

{ x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ;

correctness { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ;

coherence

{ x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } is non empty Subset of (ModelSP (Inf_seq AtomicFamily));

proof end;

:: deftheorem defines AtomicBasicAsgn MODELC_2:def 61 :

AtomicBasicAsgn = { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ;

AtomicBasicAsgn = { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ;

definition

ex b_{1} being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) st

for a being set st a in atomic_LTL holds

b_{1} . a = AtomicAsgn a

for b_{1}, b_{2} being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) st ( for a being set st a in atomic_LTL holds

b_{1} . a = AtomicAsgn a ) & ( for a being set st a in atomic_LTL holds

b_{2} . a = AtomicAsgn a ) holds

b_{1} = b_{2}
end;

func AtomicKai -> Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) means :Def62: :: MODELC_2:def 62

for a being set st a in atomic_LTL holds

it . a = AtomicAsgn a;

existence for a being set st a in atomic_LTL holds

it . a = AtomicAsgn a;

ex b

for a being set st a in atomic_LTL holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def62 defines AtomicKai MODELC_2:def 62 :

for b_{1} being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) holds

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

b_{1} . a = AtomicAsgn a );

for b

( b

b

:: deftheorem Def63 defines |= MODELC_2:def 63 :

for r being Element of Inf_seq AtomicFamily

for H being LTL-formula holds

( r |= H iff r |= Evaluate (H,AtomicKai) );

for r being Element of Inf_seq AtomicFamily

for H being LTL-formula holds

( r |= H iff r |= Evaluate (H,AtomicKai) );

notation
end;

:: deftheorem Def64 defines |= MODELC_2:def 64 :

for r being Element of Inf_seq AtomicFamily

for W being Subset of LTL_WFF holds

( r |= W iff for H being LTL-formula st H in W holds

r |= H );

for r being Element of Inf_seq AtomicFamily

for W being Subset of LTL_WFF holds

( r |= W iff for H being LTL-formula st H in W holds

r |= H );

notation
end;

definition

let W be Subset of LTL_WFF;

coherence

{ x where x is LTL-formula : ex u being LTL-formula st

( u in W & x = 'X' u ) } is Subset of LTL_WFF;

end;
func 'X' W -> Subset of LTL_WFF equals :: MODELC_2:def 65

{ x where x is LTL-formula : ex u being LTL-formula st

( u in W & x = 'X' u ) } ;

correctness { x where x is LTL-formula : ex u being LTL-formula st

( u in W & x = 'X' u ) } ;

coherence

{ x where x is LTL-formula : ex u being LTL-formula st

( u in W & x = 'X' u ) } is Subset of LTL_WFF;

proof end;

:: deftheorem defines 'X' MODELC_2:def 65 :

for W being Subset of LTL_WFF holds 'X' W = { x where x is LTL-formula : ex u being LTL-formula st

( u in W & x = 'X' u ) } ;

for W being Subset of LTL_WFF holds 'X' W = { x where x is LTL-formula : ex u being LTL-formula st

( u in W & x = 'X' u ) } ;

theorem :: MODELC_2:63

for H being LTL-formula

for r being Element of Inf_seq AtomicFamily st H is atomic holds

( r |= H iff H in (CastSeq (r,AtomicFamily)) . 0 )

for r being Element of Inf_seq AtomicFamily st H is atomic holds

( r |= H iff H in (CastSeq (r,AtomicFamily)) . 0 )

proof end;

theorem Th64: :: MODELC_2:64

for H being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= 'not' H iff r |/= H )

for r being Element of Inf_seq AtomicFamily holds

( r |= 'not' H iff r |/= H )

proof end;

theorem Th65: :: MODELC_2:65

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 '&' H2 iff ( r |= H1 & r |= H2 ) )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 '&' H2 iff ( r |= H1 & r |= H2 ) )

proof end;

theorem Th66: :: MODELC_2:66

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'or' H2 iff ( r |= H1 or r |= H2 ) )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'or' H2 iff ( r |= H1 or r |= H2 ) )

proof end;

theorem Th67: :: MODELC_2:67

for H being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= 'X' H iff Shift (r,1) |= H )

for r being Element of Inf_seq AtomicFamily holds

( r |= 'X' H iff Shift (r,1) |= H )

proof end;

theorem Th68: :: MODELC_2:68

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'U' H2 iff ex m being Nat st

( ( for j being Nat st j < m holds

Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'U' H2 iff ex m being Nat st

( ( for j being Nat st j < m holds

Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) )

proof end;

theorem :: MODELC_2:69

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'R' H2 iff for m being Nat st ( for j being Nat st j < m holds

Shift (r,j) |= 'not' H1 ) holds

Shift (r,m) |= H2 )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'R' H2 iff for m being Nat st ( for j being Nat st j < m holds

Shift (r,j) |= 'not' H1 ) holds

Shift (r,m) |= H2 )

proof end;

theorem Th70: :: MODELC_2:70

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= 'not' (H1 'or' H2) iff r |= ('not' H1) '&' ('not' H2) )

for r being Element of Inf_seq AtomicFamily holds

( r |= 'not' (H1 'or' H2) iff r |= ('not' H1) '&' ('not' H2) )

proof end;

theorem Th71: :: MODELC_2:71

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= 'not' (H1 '&' H2) iff r |= ('not' H1) 'or' ('not' H2) )

for r being Element of Inf_seq AtomicFamily holds

( r |= 'not' (H1 '&' H2) iff r |= ('not' H1) 'or' ('not' H2) )

proof end;

theorem Th72: :: MODELC_2:72

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) )

proof end;

theorem :: MODELC_2:73

for H being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |/= 'not' H iff r |= H ) by Th64;

for r being Element of Inf_seq AtomicFamily holds

( r |/= 'not' H iff r |= H ) by Th64;

theorem Th74: :: MODELC_2:74

for H being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= 'X' ('not' H) iff r |= 'not' ('X' H) )

for r being Element of Inf_seq AtomicFamily holds

( r |= 'X' ('not' H) iff r |= 'not' ('X' H) )

proof end;

theorem Th75: :: MODELC_2:75

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'U' H2 iff r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'U' H2 iff r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) )

proof end;

theorem :: MODELC_2:76

for H1, H2 being LTL-formula

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'R' H2 iff r |= (H1 '&' H2) 'or' (H2 '&' ('X' (H1 'R' H2))) )

for r being Element of Inf_seq AtomicFamily holds

( r |= H1 'R' H2 iff r |= (H1 '&' H2) 'or' (H2 '&' ('X' (H1 'R' H2))) )

proof end;

theorem :: MODELC_2:77

for r being Element of Inf_seq AtomicFamily

for W being Subset of LTL_WFF holds

( r |= 'X' W iff Shift (r,1) |= W )

for W being Subset of LTL_WFF holds

( r |= 'X' W iff Shift (r,1) |= W )

proof end;

:: theorems for external articles

theorem :: MODELC_2:78

for H being LTL-formula holds

( ( H is atomic implies ( not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is negative implies ( not H is atomic & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is conjunctive implies ( not H is atomic & not H is negative & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is disjunctive implies ( not H is atomic & not H is negative & not H is conjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is next implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is Until & not H is Release ) ) & ( H is Until implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Release ) ) & ( H is Release implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until ) ) ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21;

( ( H is atomic implies ( not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is negative implies ( not H is atomic & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is conjunctive implies ( not H is atomic & not H is negative & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is disjunctive implies ( not H is atomic & not H is negative & not H is conjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is next implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is Until & not H is Release ) ) & ( H is Until implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Release ) ) & ( H is Release implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until ) ) ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21;

theorem :: MODELC_2:79

theorem :: MODELC_2:80

theorem :: MODELC_2:81

theorem :: MODELC_2:82

theorem :: MODELC_2:83

for H being LTL-formula

for r being Element of Inf_seq AtomicFamily

for W being Subset of LTL_WFF st H in W & 'not' H in W holds

r |/= W

for r being Element of Inf_seq AtomicFamily

for W being Subset of LTL_WFF st H in W & 'not' H in W holds

r |/= W

proof end;