:: Model Checking, Part II
:: by Kazuhisa Ishida
::
:: Copyright (c) 2008-2021 Association of Mizar Users

definition
let x be object ;
func CastNat x -> Nat equals :Def1: :: MODELC_2:def 1
x if x is Nat
otherwise 0 ;
correctness
coherence
( ( x is Nat implies x is Nat ) & ( x is not Nat implies 0 is Nat ) )
;
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def1 defines CastNat MODELC_2:def 1 :
for x being object 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 n be Nat;
func atom. n -> FinSequence of NAT equals :: MODELC_2:def 2
<*(6 + n)*>;
coherence
<*(6 + n)*> is FinSequence of NAT
proof end;
end;

:: deftheorem defines atom. MODELC_2:def 2 :
for n being Nat holds atom. n = <*(6 + n)*>;

definition
let p be FinSequence of NAT ;
func 'not' p -> FinSequence of NAT equals :: MODELC_2:def 3
^ p;
coherence
^ p is FinSequence of NAT
;
let q be FinSequence of NAT ;
func p '&' q -> FinSequence of NAT equals :: MODELC_2:def 4
(<*1*> ^ p) ^ q;
coherence
(<*1*> ^ p) ^ q is FinSequence of NAT
;
func p 'or' q -> FinSequence of NAT equals :: MODELC_2:def 5
(<*2*> ^ p) ^ q;
coherence
(<*2*> ^ p) ^ q is FinSequence of NAT
;
end;

:: deftheorem defines 'not' MODELC_2:def 3 :
for p being FinSequence of NAT holds 'not' p = ^ p;

:: deftheorem defines '&' MODELC_2:def 4 :
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;

definition
let p be FinSequence of NAT ;
func 'X' p -> FinSequence of NAT equals :: MODELC_2:def 6
<*3*> ^ p;
coherence
<*3*> ^ p is FinSequence of NAT
;
let q be FinSequence of NAT ;
func p 'U' q -> FinSequence of NAT equals :: MODELC_2:def 7
(<*4*> ^ p) ^ q;
coherence
(<*4*> ^ p) ^ q is FinSequence of NAT
;
func p 'R' q -> FinSequence of NAT equals :: MODELC_2:def 8
(<*5*> ^ p) ^ q;
coherence
(<*5*> ^ p) ^ q is FinSequence of NAT
;
end;

:: deftheorem defines 'X' MODELC_2:def 6 :
for p being FinSequence of NAT holds 'X' p = <*3*> ^ p;

:: deftheorem defines 'U' MODELC_2:def 7 :
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;

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
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
ex b1 being non empty set st
( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'or' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'X' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'U' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'R' q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being 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
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being non empty set st ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'or' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'X' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'U' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'R' q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being 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
b1 c= D ) & ( for a being set st a in b2 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p '&' q in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p 'or' q in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
'X' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p 'U' q in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p 'R' q in b2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being 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
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines LTL_WFF MODELC_2:def 9 :
for b1 being non empty set holds
( b1 = LTL_WFF iff ( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'or' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'X' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'U' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'R' q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being 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
b1 c= D ) ) );

definition
let IT be FinSequence of NAT ;
attr IT is LTL-formula-like means :Def10: :: MODELC_2:def 10
IT is Element of LTL_WFF ;
end;

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

registration
existence
ex b1 being FinSequence of NAT st b1 is LTL-formula-like
proof end;
end;

definition end;

theorem Th1: :: MODELC_2:1
for a being set holds
( a is LTL-formula iff a in LTL_WFF )
proof end;

registration
let n be Nat;
coherence by Def9;
end;

registration
let H be LTL-formula;
coherence
proof end;
coherence
proof end;
let G be LTL-formula;
coherence
proof end;
coherence
proof end;
coherence
proof end;
coherence
proof end;
end;

definition
let H be LTL-formula;
attr H is atomic means :: MODELC_2:def 11
ex n being Nat st H = atom. n;
attr H is negative means :: MODELC_2:def 12
ex H1 being LTL-formula st H = 'not' H1;
attr H is conjunctive means :: MODELC_2:def 13
ex F, G being LTL-formula st H = F '&' G;
attr H is disjunctive means :: MODELC_2:def 14
ex F, G being LTL-formula st H = F 'or' G;
attr H is next means :: MODELC_2:def 15
ex H1 being LTL-formula st H = 'X' H1;
attr H is Until means :: MODELC_2:def 16
ex F, G being LTL-formula st H = F 'U' G;
attr H is Release means :: MODELC_2:def 17
ex F, G being LTL-formula st H = F 'R' G;
end;

:: deftheorem defines atomic MODELC_2:def 11 :
for H being LTL-formula holds
( H is atomic iff ex n being Nat st H = atom. n );

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

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

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

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

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

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

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

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

by FINSEQ_1:41;

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

by FINSEQ_1:41;

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;

theorem Th3: :: MODELC_2:3
for H being LTL-formula holds 1 <= len H
proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm15: for G, G1, H, H1 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 ) ;
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
( ( H is negative implies ex b1 being LTL-formula st 'not' b1 = H ) & ( not H is negative implies ex b1 being LTL-formula st 'X' b1 = H ) )
by A1;
uniqueness
for b1, b2 being LTL-formula holds
( ( H is negative & 'not' b1 = H & 'not' b2 = H implies b1 = b2 ) & ( not H is negative & 'X' b1 = H & 'X' b2 = H implies b1 = b2 ) )
by FINSEQ_1:33;
consistency
for b1 being LTL-formula holds verum
;
end;

:: 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 b2 being LTL-formula holds
( ( H is negative implies ( b2 = the_argument_of H iff 'not' b2 = H ) ) & ( not H is negative implies ( b2 = the_argument_of H iff 'X' b2 = H ) ) );

definition
let H be LTL-formula;
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
( ( H is conjunctive implies ex b1, H1 being LTL-formula st b1 '&' H1 = H ) & ( H is disjunctive implies ex b1, H1 being LTL-formula st b1 'or' H1 = H ) & ( H is Until implies ex b1, H1 being LTL-formula st b1 'U' H1 = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b1, H1 being LTL-formula st b1 'R' H1 = H ) )
by A1;
uniqueness
for b1, b2 being LTL-formula holds
( ( H is conjunctive & ex H1 being LTL-formula st b1 '&' H1 = H & ex H1 being LTL-formula st b2 '&' H1 = H implies b1 = b2 ) & ( H is disjunctive & ex H1 being LTL-formula st b1 'or' H1 = H & ex H1 being LTL-formula st b2 'or' H1 = H implies b1 = b2 ) & ( H is Until & ex H1 being LTL-formula st b1 'U' H1 = H & ex H1 being LTL-formula st b2 'U' H1 = H implies b1 = b2 ) & ( not H is conjunctive & not H is disjunctive & not H is Until & ex H1 being LTL-formula st b1 'R' H1 = H & ex H1 being LTL-formula st b2 'R' H1 = H implies b1 = b2 ) )
by ;
consistency
for b1 being LTL-formula holds
( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st b1 '&' H1 = H iff ex H1 being LTL-formula st b1 'or' H1 = H ) ) & ( H is conjunctive & H is Until implies ( ex H1 being LTL-formula st b1 '&' H1 = H iff ex H1 being LTL-formula st b1 'U' H1 = H ) ) & ( H is disjunctive & H is Until implies ( ex H1 being LTL-formula st b1 'or' H1 = H iff ex H1 being LTL-formula st b1 'U' H1 = H ) ) )
by ;
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
( ( H is conjunctive implies ex b1, H1 being LTL-formula st H1 '&' b1 = H ) & ( H is disjunctive implies ex b1, H1 being LTL-formula st H1 'or' b1 = H ) & ( H is Until implies ex b1, H1 being LTL-formula st H1 'U' b1 = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b1, H1 being LTL-formula st H1 'R' b1 = H ) )
by A1;
uniqueness
for b1, b2 being LTL-formula holds
( ( H is conjunctive & ex H1 being LTL-formula st H1 '&' b1 = H & ex H1 being LTL-formula st H1 '&' b2 = H implies b1 = b2 ) & ( H is disjunctive & ex H1 being LTL-formula st H1 'or' b1 = H & ex H1 being LTL-formula st H1 'or' b2 = H implies b1 = b2 ) & ( H is Until & ex H1 being LTL-formula st H1 'U' b1 = H & ex H1 being LTL-formula st H1 'U' b2 = H implies b1 = b2 ) & ( not H is conjunctive & not H is disjunctive & not H is Until & ex H1 being LTL-formula st H1 'R' b1 = H & ex H1 being LTL-formula st H1 'R' b2 = H implies b1 = b2 ) )
by ;
consistency
for b1 being LTL-formula holds
( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st H1 '&' b1 = H iff ex H1 being LTL-formula st H1 'or' b1 = H ) ) & ( H is conjunctive & H is Until implies ( ex H1 being LTL-formula st H1 '&' b1 = H iff ex H1 being LTL-formula st H1 'U' b1 = H ) ) & ( H is disjunctive & H is Until implies ( ex H1 being LTL-formula st H1 'or' b1 = H iff ex H1 being LTL-formula st H1 'U' b1 = H ) ) )
by ;
end;

:: 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 b2 being LTL-formula holds
( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being LTL-formula st b2 '&' H1 = H ) ) & ( H is disjunctive implies ( b2 = the_left_argument_of H iff ex H1 being LTL-formula st b2 'or' H1 = H ) ) & ( H is Until implies ( b2 = the_left_argument_of H iff ex H1 being LTL-formula st b2 'U' H1 = H ) ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ( b2 = the_left_argument_of H iff ex H1 being LTL-formula st b2 'R' H1 = H ) ) );

:: 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 b2 being LTL-formula holds
( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being LTL-formula st H1 '&' b2 = H ) ) & ( H is disjunctive implies ( b2 = the_right_argument_of H iff ex H1 being LTL-formula st H1 'or' b2 = H ) ) & ( H is Until implies ( b2 = the_right_argument_of H iff ex H1 being LTL-formula st H1 'U' b2 = H ) ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ( b2 = the_right_argument_of H iff ex H1 being LTL-formula st H1 'R' b2 = H ) ) );

theorem :: MODELC_2:4
for H being LTL-formula st H is negative holds
H = 'not' () by Def18;

theorem Th5: :: MODELC_2:5
for H being LTL-formula st H is next holds
H = 'X' ()
proof end;

theorem Th6: :: MODELC_2:6
for H being LTL-formula st H is conjunctive holds
H = '&'
proof end;

theorem Th7: :: MODELC_2:7
for H being LTL-formula st H is disjunctive holds
H = 'or'
proof end;

theorem Th8: :: MODELC_2:8
for H being LTL-formula st H is Until holds
H = 'U'
proof end;

theorem Th9: :: MODELC_2:9
for H being LTL-formula st H is Release holds
H = 'R'
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 () < 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 < len H & len < len H )
proof end;

::
:: The Immediate Constituents of LTL-formulae
::
definition
let H, F be LTL-formula;
pred H is_immediate_constituent_of F means :: MODELC_2:def 21
( 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 ) );
end;

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

theorem Th12: :: MODELC_2:12
for F, G being LTL-formula holds
( () . 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 Th13: :: MODELC_2:13
for F, H being LTL-formula holds
( H is_immediate_constituent_of 'not' F iff H = F )
proof end;

theorem Th14: :: MODELC_2:14
for F, H being LTL-formula holds
( H is_immediate_constituent_of 'X' F iff H = F )
proof end;

theorem Th15: :: MODELC_2:15
for F, G, H being LTL-formula holds
( H is_immediate_constituent_of F '&' G iff ( H = F or H = G ) )
proof end;

theorem Th16: :: MODELC_2:16
for F, G, H being LTL-formula holds
( H is_immediate_constituent_of F 'or' G iff ( H = F or H = G ) )
proof end;

theorem Th17: :: MODELC_2:17
for F, G, H being LTL-formula holds
( H is_immediate_constituent_of F 'U' G iff ( H = F or H = G ) )
proof end;

theorem Th18: :: MODELC_2:18
for F, G, H being LTL-formula holds
( H is_immediate_constituent_of F 'R' G iff ( H = F or H = G ) )
proof end;

theorem :: MODELC_2:19
for F, H being LTL-formula st F is atomic holds
not H is_immediate_constituent_of F
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 )
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 )
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 ) )
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 ) )
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 ) )
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 ) )
proof end;

theorem :: MODELC_2:26
for F, H 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 ) ;

definition
let H, F be LTL-formula;
pred H is_subformula_of F means :: 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
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;
end;

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

theorem :: MODELC_2:27
for H being LTL-formula holds H is_subformula_of H ;

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;

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

theorem Th28: :: MODELC_2:28
for F, H being LTL-formula st H is_immediate_constituent_of F holds
len H < len F
proof end;

theorem Th29: :: MODELC_2:29
for F, H being LTL-formula st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
proof end;

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

theorem Th32: :: MODELC_2:32
for F, H being LTL-formula st H is_proper_subformula_of F holds
len H < len F
proof end;

theorem :: MODELC_2:33
for F, H being LTL-formula st H is_proper_subformula_of F holds
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
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
proof end;

theorem :: MODELC_2:36
for G, H being LTL-formula st G is_subformula_of H & H is_subformula_of G holds
G = H
proof end;

theorem Th37: :: MODELC_2:37
for F, G 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
proof end;

theorem Th38: :: MODELC_2:38
for F, G 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
proof end;

theorem :: MODELC_2:39
for F, H being LTL-formula st F is_proper_subformula_of 'not' H holds
F is_subformula_of H
proof end;

theorem :: MODELC_2:40
for F, H being LTL-formula st F is_proper_subformula_of 'X' H holds
F is_subformula_of H
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 )
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 )
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 )
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 )
proof end;

::
:: The Set of Subformulae of LTL-formulae
::
definition
let H be LTL-formula;
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
ex b1 being set st
for a being set holds
( a in b1 iff ex F being LTL-formula st
( F = a & F is_subformula_of H ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex F being LTL-formula st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in b2 iff ex F being LTL-formula st
( F = a & F is_subformula_of H ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines Subformulae MODELC_2:def 24 :
for H being LTL-formula
for b2 being set holds
( b2 = Subformulae H iff for a being set holds
( a in b2 iff ex F being LTL-formula st
( F = a & F is_subformula_of H ) ) );

theorem Th45: :: MODELC_2:45
for G, H being LTL-formula holds
( G in Subformulae H iff G is_subformula_of H )
proof end;

registration
let H be LTL-formula;
cluster Subformulae H -> non empty ;
coherence
not Subformulae H is empty
by Th45;
end;

theorem :: MODELC_2:46
for F, H being LTL-formula st F is_subformula_of H holds
Subformulae F c= Subformulae H
proof end;

theorem :: MODELC_2:47
for a being set
for H being LTL-formula st a is Subset of () holds
a is Subset of LTL_WFF
proof end;

scheme :: MODELC_2:sch 1
LTLInd{ P1[ LTL-formula] } :
for H being LTL-formula holds P1[H]
provided
A1: for H being LTL-formula st H is atomic holds
P1[H] and
A2: for H being LTL-formula st ( H is negative or H is next ) & P1[ the_argument_of H] holds
P1[H] and
A3: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds
P1[H]
proof end;

scheme :: MODELC_2:sch 2
LTLCompInd{ P1[ LTL-formula] } :
for H being LTL-formula holds P1[H]
provided
A1: for H being LTL-formula st ( for F being LTL-formula st F is_proper_subformula_of H holds
P1[F] ) holds
P1[H]
proof end;

::***************************************************
::**
::** definition of LTL model structure.
::**
::****************************************************
definition
let x be object ;
func CastLTL x -> LTL-formula equals :Def25: :: MODELC_2:def 25
x if x in LTL_WFF
otherwise atom. 0;
correctness
coherence
( ( x in LTL_WFF implies x is LTL-formula ) & ( not x in LTL_WFF implies atom. 0 is LTL-formula ) )
;
consistency
for b1 being LTL-formula holds verum
;
by Th1;
end;

:: deftheorem Def25 defines CastLTL MODELC_2:def 25 :
for x being object holds
( ( x in LTL_WFF implies CastLTL x = x ) & ( not x in LTL_WFF implies CastLTL x = atom. 0 ) );

definition
attr c1 is strict ;
struct LTLModelStr -> OrthoLattStr ;
aggr LTLModelStr(# carrier, BasicAssign, L_meet, L_join, Compl, NEXT, UNTIL, RELEASE #) -> LTLModelStr ;
sel BasicAssign c1 -> Subset of the carrier of c1;
sel NEXT c1 -> UnOp of the carrier of c1;
sel UNTIL c1 -> BinOp of the carrier of c1;
sel RELEASE c1 -> BinOp of the carrier of c1;
end;

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

:: Preparation to define semantics for LTL-language
:: definition of evaluate function of LTL
definition
func atomic_LTL -> Subset of LTL_WFF equals :: MODELC_2:def 26
{ x where x is LTL-formula : x is atomic } ;
correctness
coherence
{ x where x is LTL-formula : x is atomic } is Subset of LTL_WFF
;
proof end;
end;

:: deftheorem defines atomic_LTL MODELC_2:def 26 :
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;
pred f is-Evaluation-for Kai means :: 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 . ()) ) & ( H is conjunctive implies f . H = the L_meet of V . ((),()) ) & ( H is disjunctive implies f . H = the L_join of V . ((),()) ) & ( H is next implies f . H = the NEXT of V . (f . ()) ) & ( H is Until implies f . H = the UNTIL of V . ((),()) ) & ( H is Release implies f . H = the RELEASE of V . ((),()) ) );
end;

:: deftheorem 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 . ()) ) & ( H is conjunctive implies f . H = the L_meet of V . ((),()) ) & ( H is disjunctive implies f . H = the L_join of V . ((),()) ) & ( H is next implies f . H = the NEXT of V . (f . ()) ) & ( H is Until implies f . H = the UNTIL of V . ((),()) ) & ( H is Release implies f . H = the RELEASE of V . ((),()) ) ) );

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;
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 . ()) ) & ( H is conjunctive implies f . H = the L_meet of V . ((),()) ) & ( H is disjunctive implies f . H = the L_join of V . ((),()) ) & ( H is next implies f . H = the NEXT of V . (f . ()) ) & ( H is Until implies f . H = the UNTIL of V . ((),()) ) & ( H is Release implies f . H = the RELEASE of V . ((),()) ) );
end;

:: 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 . ()) ) & ( H is conjunctive implies f . H = the L_meet of V . ((),()) ) & ( H is disjunctive implies f . H = the L_join of V . ((),()) ) & ( H is next implies f . H = the NEXT of V . (f . ()) ) & ( H is Until implies f . H = the UNTIL of V . ((),()) ) & ( H is Release implies f . H = the RELEASE of V . ((),()) ) ) );

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;
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 . ()) if ( len H = n + 1 & H is negative )
the L_meet of V . ((),()) if ( len H = n + 1 & H is conjunctive )
the L_join of V . ((),()) if ( len H = n + 1 & H is disjunctive )
the NEXT of V . (h . ()) if ( len H = n + 1 & H is next )
the UNTIL of V . ((),()) if ( len H = n + 1 & H is Until )
the RELEASE of V . ((),()) if ( len H = n + 1 & H is Release )
h . H if len H < n + 1
otherwise {} ;
coherence
( ( len H > n + 1 implies f . H is set ) & ( len H = n + 1 & H is atomic implies Kai . H is set ) & ( len H = n + 1 & H is negative implies the Compl of V . (h . ()) is set ) & ( len H = n + 1 & H is conjunctive implies the L_meet of V . ((),()) is set ) & ( len H = n + 1 & H is disjunctive implies the L_join of V . ((),()) is set ) & ( len H = n + 1 & H is next implies the NEXT of V . (h . ()) is set ) & ( len H = n + 1 & H is Until implies the UNTIL of V . ((),()) is set ) & ( len H = n + 1 & H is Release implies the RELEASE of V . ((),()) 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 b1 being set holds
( ( len H > n + 1 & len H = n + 1 & H is atomic implies ( b1 = f . H iff b1 = Kai . H ) ) & ( len H > n + 1 & len H = n + 1 & H is negative implies ( b1 = f . H iff b1 = the Compl of V . (h . ()) ) ) & ( len H > n + 1 & len H = n + 1 & H is conjunctive implies ( b1 = f . H iff b1 = the L_meet of V . ((),()) ) ) & ( len H > n + 1 & len H = n + 1 & H is disjunctive implies ( b1 = f . H iff b1 = the L_join of V . ((),()) ) ) & ( len H > n + 1 & len H = n + 1 & H is next implies ( b1 = f . H iff b1 = the NEXT of V . (h . ()) ) ) & ( len H > n + 1 & len H = n + 1 & H is Until implies ( b1 = f . H iff b1 = the UNTIL of V . ((),()) ) ) & ( len H > n + 1 & len H = n + 1 & H is Release implies ( b1 = f . H iff b1 = the RELEASE of V . ((),()) ) ) & ( len H > n + 1 & len H < n + 1 implies ( b1 = f . H iff b1 = h . H ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is negative implies ( b1 = Kai . H iff b1 = the Compl of V . (h . ()) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is conjunctive implies ( b1 = Kai . H iff b1 = the L_meet of V . ((),()) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is disjunctive implies ( b1 = Kai . H iff b1 = the L_join of V . ((),()) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is next implies ( b1 = Kai . H iff b1 = the NEXT of V . (h . ()) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is Until implies ( b1 = Kai . H iff b1 = the UNTIL of V . ((),()) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is Release implies ( b1 = Kai . H iff b1 = the RELEASE of V . ((),()) ) ) & ( len H = n + 1 & H is atomic & len H < n + 1 implies ( b1 = Kai . H iff b1 = h . H ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is conjunctive implies ( b1 = the Compl of V . (h . ()) iff b1 = the L_meet of V . ((),()) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is disjunctive implies ( b1 = the Compl of V . (h . ()) iff b1 = the L_join of V . ((),()) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is next implies ( b1 = the Compl of V . (h . ()) iff b1 = the NEXT of V . (h . ()) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Until implies ( b1 = the Compl of V . (h . ()) iff b1 = the UNTIL of V . ((),()) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Release implies ( b1 = the Compl of V . (h . ()) iff b1 = the RELEASE of V . ((),()) ) ) & ( len H = n + 1 & H is negative & len H < n + 1 implies ( b1 = the Compl of V . (h . ()) iff b1 = h . H ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is disjunctive implies ( b1 = the L_meet of V . ((),()) iff b1 = the L_join of V . ((),()) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is next implies ( b1 = the L_meet of V . ((),()) iff b1 = the NEXT of V . (h . ()) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Until implies ( b1 = the L_meet of V . ((),()) iff b1 = the UNTIL of V . ((),()) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Release implies ( b1 = the L_meet of V . ((),()) iff b1 = the RELEASE of V . ((),()) ) ) & ( len H = n + 1 & H is conjunctive & len H < n + 1 implies ( b1 = the L_meet of V . ((),()) iff b1 = h . H ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is next implies ( b1 = the L_join of V . ((),()) iff b1 = the NEXT of V . (h . ()) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Until implies ( b1 = the L_join of V . ((),()) iff b1 = the UNTIL of V . ((),()) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Release implies ( b1 = the L_join of V . ((),()) iff b1 = the RELEASE of V . ((),()) ) ) & ( len H = n + 1 & H is disjunctive & len H < n + 1 implies ( b1 = the L_join of V . ((),()) iff b1 = h . H ) ) & ( len H = n + 1 & H is next & len H = n + 1 & H is Until implies ( b1 = the NEXT of V . (h . ()) iff b1 = the UNTIL of V . ((),()) ) ) & ( len H = n + 1 & H is next & len H = n + 1 & H is Release implies ( b1 = the NEXT of V . (h . ()) iff b1 = the RELEASE of V . ((),()) ) ) & ( len H = n + 1 & H is next & len H < n + 1 implies ( b1 = the NEXT of V . (h . ()) iff b1 = h . H ) ) & ( len H = n + 1 & H is Until & len H = n + 1 & H is Release implies ( b1 = the UNTIL of V . ((),()) iff b1 = the RELEASE of V . ((),()) ) ) & ( len H = n + 1 & H is Until & len H < n + 1 implies ( b1 = the UNTIL of V . ((),()) iff b1 = h . H ) ) & ( len H = n + 1 & H is Release & len H < n + 1 implies ( b1 = the RELEASE of V . ((),()) iff b1 = h . H ) ) )
by ;
end;

:: 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 . ()) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet of V . ((),()) ) & ( len H = n + 1 & H is disjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_join of V . ((),()) ) & ( len H = n + 1 & H is next implies GraftEval (V,Kai,f,h,n,H) = the NEXT of V . (h . ()) ) & ( len H = n + 1 & H is Until implies GraftEval (V,Kai,f,h,n,H) = the UNTIL of V . ((),()) ) & ( len H = n + 1 & H is Release implies GraftEval (V,Kai,f,h,n,H) = the RELEASE of V . ((),()) ) & ( 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) = {} ) );

definition
let C be LTLModelStr ;
attr C is with_basic means :Def30: :: MODELC_2:def 30
not the BasicAssign of C is empty ;
end;

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

definition
func TrivialLTLModel -> LTLModelStr equals :: MODELC_2:def 31
LTLModelStr(# ,(),op2,op2,op1,op1,op2,op2 #);
coherence
LTLModelStr(# ,(),op2,op2,op1,op1,op2,op2 #) is LTLModelStr
;
end;

:: deftheorem defines TrivialLTLModel MODELC_2:def 31 :
TrivialLTLModel = LTLModelStr(# ,(),op2,op2,op1,op1,op2,op2 #);

registration
coherence ;
end;

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

registration
existence
ex b1 being non empty LTLModelStr st b1 is with_basic
proof end;
end;

definition end;

registration
let C be LTLModel;
cluster the BasicAssign of C -> non empty ;
coherence
not the BasicAssign of C is empty
by Def30;
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

by Th3;

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

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

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

definition
let V be LTLModel;
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
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 b1 being Function of LTL_WFF, the carrier of V holds verum
;
by FUNCT_2:66;
end;

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

definition
let V be LTLModel;
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
ex b1 being non empty set st
for p being set holds
( p in b1 iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) )
proof end;
uniqueness
for b1, b2 being non empty set st ( for p being set holds
( p in b1 iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) & ( for p being set holds
( p in b2 iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) holds
b1 = b2
proof end;
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 b3 being non empty set holds
( b3 = EvalFamily (V,Kai) iff for p being set holds
( p in b3 iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) );

Lm27: 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
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
proof end;

definition
let V be LTLModel;
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 b1 being Assign of V ex f being Function of LTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b1 = f . H )
proof end;
uniqueness
for b1, b2 being Assign of V st ex f being Function of LTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b1 = f . H ) & ex f being Function of LTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b2 = f . H ) holds
b1 = b2
by Th49;
end;

:: 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 b4 being Assign of V holds
( b4 = Evaluate (H,Kai) iff ex f being Function of LTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b4 = f . H ) );

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;

definition
let V be LTLModel;
let f be Assign of V;
func 'X' f -> Assign of V equals :: MODELC_2:def 36
the NEXT of V . f;
correctness
coherence
the NEXT of V . f is Assign of V
;
;
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;

definition
let V be LTLModel;
let f, g be Assign of V;
func f 'U' g -> Assign of V equals :: MODELC_2:def 37
the UNTIL of V . (f,g);
correctness
coherence
the UNTIL of V . (f,g) is Assign of V
;
;
func f 'R' g -> Assign of V equals :: MODELC_2:def 38
the RELEASE of V . (f,g);
correctness
coherence
the RELEASE of V . (f,g) is Assign of V
;
;
end;

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

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

::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 ((),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))
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))
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))
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))
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))
proof end;

::definition of concrete object of LTL model
definition
let S be non empty set ;
func Inf_seq S -> non empty set equals :: MODELC_2:def 39
Funcs (NAT,S);
correctness
coherence
Funcs (NAT,S) is non empty set
;
;
end;

:: deftheorem defines Inf_seq MODELC_2:def 39 :
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;
func CastSeq t -> Element of Inf_seq S equals :: MODELC_2:def 40
t;
correctness
coherence
t is Element of Inf_seq S
;
by FUNCT_2:8;
end;

:: deftheorem defines CastSeq MODELC_2:def 40 :
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 object ;
assume A1: t is Element of Inf_seq S ;
func CastSeq (t,S) -> sequence of S equals :Def41: :: MODELC_2:def 41
t;
correctness
coherence
t is sequence of S
;
by ;
end;

:: deftheorem Def41 defines CastSeq MODELC_2:def 41 :
for S being non empty set
for t being object 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;
func Shift (t,k,S) -> Element of Inf_seq S equals :: MODELC_2:def 42
CastSeq ((CastSeq (t,S)) ^\ k);
correctness
coherence
CastSeq ((CastSeq (t,S)) ^\ k) is Element of Inf_seq S
;
;
end;

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

definition
let S be non empty set ;
let t be Element of Inf_seq S;
let k be Nat;
func Shift (t,k) -> Element of Inf_seq S equals :: MODELC_2:def 43
Shift (t,k,S);
correctness
coherence
Shift (t,k,S) is Element of Inf_seq S
;
;
end;

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

Lm28: for S being non empty set
for seq being Element of Inf_seq S holds Shift (seq,0) = seq

proof end;

Lm29: 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 object ;
func Not_0 (f,S) -> Element of ModelSP () means :Def44: :: MODELC_2:def 44
for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid (f,())) . t)) = TRUE iff (Fid (it,())) . t = TRUE );
existence
ex b1 being Element of ModelSP () st
for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid (f,())) . t)) = TRUE iff (Fid (b1,())) . t = TRUE )
proof end;
uniqueness
for b1, b2 being Element of ModelSP () st ( for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid (f,())) . t)) = TRUE iff (Fid (b1,())) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid (f,())) . t)) = TRUE iff (Fid (b2,())) . t = TRUE ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def44 defines Not_0 MODELC_2:def 44 :
for S being non empty set
for f being object
for b3 being Element of ModelSP () holds
( b3 = Not_0 (f,S) iff for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid (f,())) . t)) = TRUE iff (Fid (b3,())) . t = TRUE ) );

Lm30: for S being non empty set
for o1, o2 being UnOp of (ModelSP ()) st ( for f being object st f in ModelSP () holds
o1 . f = Not_0 (f,S) ) & ( for f being object st f in ModelSP () holds
o2 . f = Not_0 (f,S) ) holds
o1 = o2

proof end;

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

:: deftheorem Def45 defines Not_ MODELC_2:def 45 :
for S being non empty set
for b2 being UnOp of (ModelSP ()) holds
( b2 = Not_ S iff for f being object st f in ModelSP () holds
b2 . f = Not_0 (f,S) );

:: definition of next_ unary operation of Model Space.
definition
let S be non empty set ;
let f be Function of (),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
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 b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def46 defines Next_univ MODELC_2:def 46 :
for S being non empty set
for f being Function of (),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 object ;
func Next_0 (f,S) -> Element of ModelSP () means :Def47: :: MODELC_2:def 47
for t being set st t in Inf_seq S holds
( Next_univ (t,(Fid (f,()))) = TRUE iff (Fid (it,())) . t = TRUE );
existence
ex b1 being Element of ModelSP () st
for t being set st t in Inf_seq S holds
( Next_univ (t,(Fid (f,()))) = TRUE iff (Fid (b1,())) . t = TRUE )
proof end;
uniqueness
for b1, b2 being Element of ModelSP () st ( for t being set st t in Inf_seq S holds
( Next_univ (t,(Fid (f,()))) = TRUE iff (Fid (b1,())) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( Next_univ (t,(Fid (f,()))) = TRUE iff (Fid (b2,())) . t = TRUE ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def47 defines Next_0 MODELC_2:def 47 :
for S being non empty set
for f being object
for b3 being Element of ModelSP () holds
( b3 = Next_0 (f,S) iff for t being set st t in Inf_seq S holds
( Next_univ (t,(Fid (f,()))) = TRUE iff (Fid (b3,())) . t = TRUE ) );

Lm31: for S being non empty set
for o1, o2 being UnOp of (ModelSP ()) st ( for f being object st f in ModelSP () holds
o1 . f = Next_0 (f,S) ) & ( for f being object st f in ModelSP () holds
o2 . f = Next_0 (f,S) ) holds
o1 = o2

proof end;

definition
let S be non empty set ;
func Next_ S -> UnOp of (ModelSP ()) means :Def48: :: MODELC_2:def 48
for f being object st f in ModelSP () holds
it . f = Next_0 (f,S);
existence
ex b1 being UnOp of (ModelSP ()) st
for f being object st f in ModelSP () holds
b1 . f = Next_0 (f,S)
proof end;
uniqueness
for b1, b2 being UnOp of (ModelSP ()) st ( for f being object st f in ModelSP () holds
b1 . f = Next_0 (f,S) ) & ( for f being object st f in ModelSP () holds
b2 . f = Next_0 (f,S) ) holds
b1 = b2
by Lm31;
end;

:: deftheorem Def48 defines Next_ MODELC_2:def 48 :
for S being non empty set
for b2 being UnOp of (ModelSP ()) holds
( b2 = Next_ S iff for f being object st f in ModelSP () holds
b2 . f = Next_0 (f,S) );

:: definition of And_ Binary Operation of Model Space.
definition
let S be non empty set ;
let f, g be set ;
func And_0 (f,g,S) -> Element of ModelSP () means :Def49: :: MODELC_2:def 49
for t being set st t in Inf_seq S holds
( (Castboolean ((Fid (f,())) . t)) '&' (Castboolean ((Fid (g,())) . t)) = TRUE iff (Fid (it,())) . t = TRUE );
existence
ex b1 being Element of ModelSP () st
for t being set st t in Inf_seq S holds
( (Castboolean ((Fid (f,())) . t)) '&' (Castboolean ((Fid (g,())) . t)) = TRUE iff (Fid (b1,())) . t = TRUE )
proof end;
uniqueness
for b1, b2 being Element of ModelSP () st ( for t being set st t in Inf_seq S holds
( (Castboolean ((Fid (f,())) . t)) '&' (Castboolean ((Fid (g,())) . t)) = TRUE iff (Fid (b1,())) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( (Castboolean ((Fid (f,())) . t)) '&' (Castboolean ((Fid (g,())) . t)) = TRUE iff (Fid (b2,())) . t = TRUE ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def49 defines And_0 MODELC_2:def 49 :
for S being non empty set
for f, g being set
for b4 being Element of ModelSP () holds
( b4 = And_0 (f,g,S) iff for t being set st t in Inf_seq S holds
( (Castboolean ((Fid (f,())) . t)) '&' (Castboolean ((Fid (g,())) . t)) = TRUE iff (Fid (b4,())) . t = TRUE ) );

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

proof end;

definition
let S be non empty set ;
func And_ S -> BinOp of (ModelSP ()) means :Def50: :: MODELC_2:def 50
for f, g being set st f in ModelSP () & g in ModelSP () holds
it . (f,g) = And_0 (f,g,S);
existence
ex b1 being BinOp of (ModelSP ()) st
for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = And_0 (f,g,S)
proof end;
uniqueness
for b1, b2 being BinOp of (ModelSP ()) st ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = And_0 (f,g,S) ) holds
b1 = b2
by Lm32;
end;

:: deftheorem Def50 defines And_ MODELC_2:def 50 :
for S being non empty set
for b2 being BinOp of (ModelSP ()) holds
( b2 = And_ S iff for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = And_0 (f,g,S) );

:: definition of Until_ Binary Operation of Model Space.
definition
let S be non empty set ;
let f, g be Function of (),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
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 b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def51 defines Until_univ MODELC_2:def 51 :
for S being non empty set
for f, g being Function of (),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 ;
func Until_0 (f,g,S) -> Element of ModelSP () means :Def52: :: MODELC_2:def 52
for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,())),(Fid (g,())),S) = TRUE iff (Fid (it,())) . t = TRUE );
existence
ex b1 being Element of ModelSP () st
for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,())),(Fid (g,())),S) = TRUE iff (Fid (b1,())) . t = TRUE )
proof end;
uniqueness
for b1, b2 being Element of ModelSP () st ( for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,())),(Fid (g,())),S) = TRUE iff (Fid (b1,())) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,())),(Fid (g,())),S) = TRUE iff (Fid (b2,())) . t = TRUE ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def52 defines Until_0 MODELC_2:def 52 :
for S being non empty set
for f, g being set
for b4 being Element of ModelSP () holds
( b4 = Until_0 (f,g,S) iff for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,())),(Fid (g,())),S) = TRUE iff (Fid (b4,())) . t = TRUE ) );

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

proof end;

definition
let S be non empty set ;
func Until_ S -> BinOp of (ModelSP ()) means :Def53: :: MODELC_2:def 53
for f, g being set st f in ModelSP () & g in ModelSP () holds
it . (f,g) = Until_0 (f,g,S);
existence
ex b1 being BinOp of (ModelSP ()) st
for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = Until_0 (f,g,S)
proof end;
uniqueness
for b1, b2 being BinOp of (ModelSP ()) st ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = Until_0 (f,g,S) ) & ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = Until_0 (f,g,S) ) holds
b1 = b2
by Lm33;
end;

:: deftheorem Def53 defines Until_ MODELC_2:def 53 :
for S being non empty set
for b2 being BinOp of (ModelSP ()) holds
( b2 = Until_ S iff for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = Until_0 (f,g,S) );

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

proof end;

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

proof end;

definition
let S be non empty set ;
func Or_ S -> BinOp of (ModelSP ()) means :Def54: :: MODELC_2:def 54
for f, g being set st f in ModelSP () & g in ModelSP () holds
it . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g)));
existence
ex b1 being BinOp of (ModelSP ()) st
for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g)))
proof end;
uniqueness
for b1, b2 being BinOp of (ModelSP ()) st ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) & ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds
b1 = b2
by Lm34;
func Release_ S -> BinOp of (ModelSP ()) means :Def55: :: MODELC_2:def 55
for f, g being set st f in ModelSP () & g in ModelSP () holds
it . (f,g) = (Not_ S) . (() . (((Not_ S) . f),((Not_ S) . g)));
existence
ex b1 being BinOp of (ModelSP ()) st
for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = (Not_ S) . (() . (((Not_ S) . f),((Not_ S) . g)))
proof end;
uniqueness
for b1, b2 being BinOp of (ModelSP ()) st ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b1 . (f,g) = (Not_ S) . (() . (((Not_ S) . f),((Not_ S) . g))) ) & ( for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = (Not_ S) . (() . (((Not_ S) . f),((Not_ S) . g))) ) holds
b1 = b2
by Lm35;
end;

:: deftheorem Def54 defines Or_ MODELC_2:def 54 :
for S being non empty set
for b2 being BinOp of (ModelSP ()) holds
( b2 = Or_ S iff for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) );

:: deftheorem Def55 defines Release_ MODELC_2:def 55 :
for S being non empty set
for b2 being BinOp of (ModelSP ()) holds
( b2 = Release_ S iff for f, g being set st f in ModelSP () & g in ModelSP () holds
b2 . (f,g) = (Not_ S) . (() . (((Not_ S) . f),((Not_ S) . g))) );

:: definition of concrete object of LTL model by ModelSP
definition
let S be non empty set ;
let BASSIGN be non empty Subset of (ModelSP ());
func Inf_seqModel (S,BASSIGN) -> LTLModelStr equals :: MODELC_2:def 56
LTLModelStr(# (ModelSP ()),BASSIGN,(And_ S),(Or_ S),(Not_ S),(),(),() #);
coherence
LTLModelStr(# (ModelSP ()),BASSIGN,(And_ S),(Or_ S),(Not_ S),(),(),() #) is LTLModelStr
;
end;

:: deftheorem defines Inf_seqModel MODELC_2:def 56 :
for S being non empty set
for BASSIGN being non empty Subset of (ModelSP ()) holds Inf_seqModel (S,BASSIGN) = LTLModelStr(# (ModelSP ()),BASSIGN,(And_ S),(Or_ S),(Not_ S),(),(),() #);

registration
let S be non empty set ;
let BASSIGN be non empty Subset of (ModelSP ());
cluster Inf_seqModel (S,BASSIGN) -> non empty strict with_basic ;
coherence
( Inf_seqModel (S,BASSIGN) is with_basic & Inf_seqModel (S,BASSIGN) is strict & not Inf_seqModel (S,BASSIGN) is empty )
;
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 ());
let t be Element of Inf_seq S;
let f be Assign of (Inf_seqModel (S,BASSIGN));
pred t |= f means :: MODELC_2:def 57
(Fid (f,())) . t = TRUE ;
end;

:: deftheorem defines |= MODELC_2:def 57 :
for S being non empty set
for BASSIGN being non empty Subset of (ModelSP ())
for t being Element of Inf_seq S
for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f iff (Fid (f,())) . t = TRUE );

notation
let S be non empty set ;
let BASSIGN be non empty Subset of (ModelSP ());
let t be Element of Inf_seq S;
let f be Assign of (Inf_seqModel (S,BASSIGN));
antonym t |/= f for t |= f;
end;

theorem :: MODELC_2:56
for S being non empty set
for BASSIGN being non empty Subset of (ModelSP ())
for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( f 'or' g = 'not' (() '&' ()) & f 'R' g = 'not' (() 'U' ()) ) by ;

theorem Th57: :: MODELC_2:57
for S being non empty set
for BASSIGN being non empty Subset of (ModelSP ())
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 ())
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 ())
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 ())
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 ())
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 ())
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
correctness
coherence
bool atomic_LTL is non empty set
;
;
end;

:: deftheorem defines AtomicFamily MODELC_2:def 58 :

definition
let a, t be object ;
func AtomicFunc (a,t) -> Element of BOOLEAN equals :Def59: :: MODELC_2:def 59
TRUE if ( t in Inf_seq AtomicFamily & a in () . 0 )
otherwise FALSE ;
correctness
coherence
( ( t in Inf_seq AtomicFamily & a in () . 0 implies TRUE is Element of BOOLEAN ) & ( ( not t in Inf_seq AtomicFamily or not a in () . 0 ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def59 defines AtomicFunc MODELC_2:def 59 :
for a, t being object holds
( ( t in Inf_seq AtomicFamily & a in () . 0 implies AtomicFunc (a,t) = TRUE ) & ( ( not t in Inf_seq AtomicFamily or not a in () . 0 ) implies AtomicFunc (a,t) = FALSE ) );

Lm36: 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 object ;
func AtomicAsgn a -> Element of ModelSP means :Def60: :: MODELC_2:def 60
for t being set st t in Inf_seq AtomicFamily holds
(Fid (it,)) . t = AtomicFunc (a,t);
existence
ex b1 being Element of ModelSP st
for t being set st t in Inf_seq AtomicFamily holds
(Fid (b1,)) . t = AtomicFunc (a,t)
proof end;
uniqueness
for b1, b2 being Element of ModelSP st ( for t being set st t in Inf_seq AtomicFamily holds
(Fid (b1,)) . t = AtomicFunc (a,t) ) & ( for t being set st t in Inf_seq AtomicFamily holds
(Fid (b2,)) . t = AtomicFunc (a,t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def60 defines AtomicAsgn MODELC_2:def 60 :
for a being object
for b2 being Element of ModelSP holds
( b2 = AtomicAsgn a iff for t being set st t in Inf_seq AtomicFamily holds
(Fid (b2,)) . t = AtomicFunc (a,t) );

definition
func AtomicBasicAsgn -> non empty Subset of equals :: MODELC_2:def 61
{ x where x is Element of ModelSP : ex a being set st x = AtomicAsgn a } ;
correctness
coherence
{ x where x is Element of ModelSP : ex a being set st x = AtomicAsgn a } is non empty Subset of
;
proof end;
end;

:: deftheorem defines AtomicBasicAsgn MODELC_2:def 61 :
AtomicBasicAsgn = { x where x is Element of ModelSP : ex a being set st x = AtomicAsgn a } ;

definition
func AtomicKai -> Function of atomic_LTL, the BasicAssign of means :Def62: :: MODELC_2:def 62
for a being set st a in atomic_LTL holds
it . a = AtomicAsgn a;
existence
ex b1 being Function of atomic_LTL, the BasicAssign of st
for a being set st a in atomic_LTL holds
b1 . a = AtomicAsgn a
proof end;
uniqueness
for b1, b2 being Function of atomic_LTL, the BasicAssign of st ( for a being set st a in atomic_LTL holds
b1 . a = AtomicAsgn a ) & ( for a being set st a in atomic_LTL holds
b2 . a = AtomicAsgn a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def62 defines AtomicKai MODELC_2:def 62 :
for b1 being Function of atomic_LTL, the BasicAssign of holds
( b1 = AtomicKai iff for a being set st a in atomic_LTL holds
b1 . a = AtomicAsgn a );

definition
let r be Element of Inf_seq AtomicFamily;
let H be LTL-formula;
pred r |= H means :Def63: :: MODELC_2:def 63
r |= Evaluate (H,AtomicKai);
end;

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

notation
let r be Element of Inf_seq AtomicFamily;
let H be LTL-formula;
antonym r |/= H for r |= H;
end;

definition
let r be Element of Inf_seq AtomicFamily;
let W be Subset of LTL_WFF;
pred r |= W means :: MODELC_2:def 64
for H being LTL-formula st H in W holds
r |= H;
end;

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

notation
let r be Element of Inf_seq AtomicFamily;
let W be Subset of LTL_WFF;
antonym r |/= W for r |= W;
end;

definition
let W be Subset of LTL_WFF;
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
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;
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 )
}
;

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

theorem Th74: :: MODELC_2:74
for H being LTL-formula
for r being Element of Inf_seq AtomicFamily holds
( r |= 'X' () 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))) )
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))) )
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 )
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 ;

theorem :: MODELC_2:79
for S being non empty set
for t being Element of Inf_seq S holds Shift (t,0) = t by Lm28;

theorem :: MODELC_2:80
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)) by Lm29;

theorem :: MODELC_2:81
for S being non empty set
for seq being sequence of S holds CastSeq ((CastSeq seq),S) = seq by Def41;

theorem :: MODELC_2:82
for S being non empty set
for seq being Element of Inf_seq S holds CastSeq (CastSeq (seq,S)) = seq by Def41;

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