MODELC_2: Model Checking, Part II

:: Model Checking, Part II
:: by Kazuhisa Ishida
::
:: Received April 21, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

begin

definition

let x be set ;
func CastNat x -> Nat equals :Def1: :: MODELC_2:def 1
x if x is Nat
otherwise 0 ;
correctness ;

end;

:: deftheorem Def1 defines CastNat MODELC_2:def 1 :

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

proof end;

definition

let n be Nat;
func atom. n -> FinSequence of NAT equals :: MODELC_2:def 2
<*(6 + n)*>;
coherence ;

end;

:: deftheorem defines atom. MODELC_2:def 2 :

definition

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

end;

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

:: deftheorem defines '&' MODELC_2:def 4 :

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

definition

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

end;

:: deftheorem defines 'X' MODELC_2:def 6 :

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

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

Lm2: for n being Nat
for p, q being FinSequence of NAT holds len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q)

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines LTL_WFF MODELC_2:def 9 :

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 :

registration

cluster Relation-like NAT -valued Function-like V54() FinSequence-like FinSubsequence-like LTL-formula-like FinSequence of NAT ;
existence

proof end;

end;

definition

mode LTL-formula is LTL-formula-like FinSequence of NAT ;

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;
cluster atom. n -> LTL-formula-like ;
coherence

proof end;

end;

registration

let H be LTL-formula;
cluster 'not' H -> LTL-formula-like ;
coherence

proof end;

cluster 'X' H -> LTL-formula-like ;
coherence

proof end;

let G be LTL-formula;
cluster H '&' G -> LTL-formula-like ;
coherence

proof end;

cluster H 'or' G -> LTL-formula-like ;
coherence

proof end;

cluster H 'U' G -> LTL-formula-like ;
coherence

proof end;

cluster H 'R' G -> LTL-formula-like ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def11 defines atomic MODELC_2:def 11 :

:: deftheorem Def12 defines negative MODELC_2:def 12 :

:: deftheorem Def13 defines conjunctive MODELC_2:def 13 :

:: deftheorem Def14 defines disjunctive MODELC_2:def 14 :

:: deftheorem Def15 defines next MODELC_2:def 15 :

:: deftheorem Def16 defines Until MODELC_2:def 16 :

:: deftheorem Def17 defines Release MODELC_2:def 17 :

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

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;

theorem Th3: :: MODELC_2:3

for H being LTL-formula holds 1 <= len H

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 ) ;
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 by A1, Def12, Def15;
uniqueness by FINSEQ_1:46;
consistency ;

end;

:: deftheorem Def18 defines the_argument_of MODELC_2:def 18 :

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 by A1, Def13, Def14, Def16, Def17;
uniqueness by Lm12, Lm13, Lm14, Lm15;
consistency by Lm17, Lm18;
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

proof end;

uniqueness by Lm12, Lm13, Lm14, Lm15;
consistency by Lm18, Lm20;

end;

:: deftheorem Def19 defines the_left_argument_of MODELC_2:def 19 :

:: deftheorem Def20 defines the_right_argument_of MODELC_2:def 20 :

theorem :: MODELC_2:4

for H being LTL-formula st H is negative holds
H = 'not' (the_argument_of H) by Def18;

theorem Th5: :: MODELC_2:5

for H being LTL-formula st H is next holds
H = 'X' (the_argument_of H)

proof end;

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)

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)

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)

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)

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 )

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 )

proof end;

definition

let H, F be LTL-formula;
pred H is_immediate_constituent_of F means :Def21: :: 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 Def21 defines is_immediate_constituent_of MODELC_2:def 21 :

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 )

proof end;

theorem Th13: :: MODELC_2:13

for H, F being LTL-formula holds
( H is_immediate_constituent_of 'not' F iff H = F )

proof end;

theorem Th14: :: MODELC_2:14

for H, F being LTL-formula holds
( H is_immediate_constituent_of 'X' F iff H = F )

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

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

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

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

proof end;

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

definition

let H, F be LTL-formula;
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

proof end;

end;

:: deftheorem Def22 defines is_subformula_of MODELC_2:def 22 :

theorem :: MODELC_2:27

for H being LTL-formula holds H is_subformula_of H ;

definition

let H, F be LTL-formula;
pred H is_proper_subformula_of F means :Def23: :: MODELC_2:def 23
( H is_subformula_of F & H <> F );
irreflexivity ;

end;

:: deftheorem Def23 defines is_proper_subformula_of MODELC_2:def 23 :

theorem Th28: :: MODELC_2:28

for H, F being LTL-formula st H is_immediate_constituent_of F holds
len H < len F

proof end;

theorem Th29: :: MODELC_2:29

for H, F 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 H, F being LTL-formula st H is_proper_subformula_of F holds
len H < len F

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

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

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

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines Subformulae MODELC_2:def 24 :

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 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 (Subformulae H) holds
a is Subset of LTL_WFF

proof end;

scheme :: MODELC_2:sch 1
LTLInd{ P₁[ LTL-formula] } :

for H being LTL-formula holds P₁[H]

provided

A1: for H being LTL-formula st H is atomic holds
P₁[H] and
A2: for H being LTL-formula st ( H is negative or H is next ) & P₁[ the_argument_of H] holds
P₁[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₁[ the_left_argument_of H] & P₁[ the_right_argument_of H] holds
P₁[H]

proof end;

scheme :: MODELC_2:sch 2
LTLCompInd{ P₁[ LTL-formula] } :

for H being LTL-formula holds P₁[H]

provided

A1: for H being LTL-formula st ( for F being LTL-formula st F is_proper_subformula_of H holds
P₁[F] ) holds
P₁[H]

proof end;

definition

let x be set ;
func CastLTL x -> LTL-formula equals :Def25: :: MODELC_2:def 25
x if x in LTL_WFF
otherwise atom. 0;
correctness by Th1;

end;

:: deftheorem Def25 defines CastLTL MODELC_2:def 25 :

definition

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

end;

definition

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

end;

definition

func atomic_LTL -> Subset of LTL_WFF equals :: MODELC_2:def 26
{ x where x is LTL-formula : x is atomic } ;
correctness

proof end;

end;

:: deftheorem defines atomic_LTL MODELC_2:def 26 :

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

end;

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

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

end;

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

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 . (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 ;
consistency by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21;

end;

:: deftheorem Def29 defines GraftEval MODELC_2:def 29 :

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 :

definition

func TrivialLTLModel -> LTLModelStr equals :: MODELC_2:def 31
LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #);
coherence ;

end;

:: deftheorem defines TrivialLTLModel MODELC_2:def 31 :

registration

cluster TrivialLTLModel -> non empty strict with_basic ;
coherence

proof end;

end;

registration

cluster non empty LTLModelStr ;
existence

proof end;

end;

registration

cluster non empty with_basic LTLModelStr ;
existence

proof end;

end;

definition

mode LTLModel is non empty with_basic LTLModelStr ;

end;

registration

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

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

proof end;

end;

:: deftheorem defines EvalSet MODELC_2:def 32 :

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 by FUNCT_2:121;

end;

:: deftheorem Def33 defines CastEval MODELC_2:def 33 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def34 defines EvalFamily MODELC_2:def 34 :

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

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

proof end;

uniqueness by Th49;

end;

:: deftheorem Def35 defines Evaluate MODELC_2:def 35 :

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

canceled;
canceled;
canceled;
let V be LTLModel;
let f be Assign of V;
func 'X' f -> Assign of V equals :: MODELC_2:def 39
the NEXT of V . f;
correctness ;

end;

:: deftheorem MODELC_2:def 36 :

:: deftheorem MODELC_2:def 37 :

:: deftheorem MODELC_2:def 38 :

:: deftheorem defines 'X' MODELC_2:def 39 :

definition

let V be LTLModel;
let f, g be Assign of V;
func f 'U' g -> Assign of V equals :: MODELC_2:def 40
the UNTIL of V . (f,g);
correctness ;
func f 'R' g -> Assign of V equals :: MODELC_2:def 41
the RELEASE of V . (f,g);
correctness ;

end;

:: deftheorem defines 'U' MODELC_2:def 40 :

:: deftheorem defines 'R' MODELC_2:def 41 :

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

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

let S be non empty set ;
func Inf_seq S -> non empty set equals :: MODELC_2:def 42
Funcs (NAT,S);
correctness ;

end;

:: deftheorem defines Inf_seq MODELC_2:def 42 :

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 43
t;
correctness by FUNCT_2:11;

end;

:: deftheorem defines CastSeq MODELC_2:def 43 :

definition

let S be non empty set ;
let t be set ;
assume A1: t is Element of Inf_seq S ;
func CastSeq (t,S) -> sequence of S equals :Def44: :: MODELC_2:def 44
t;
correctness by A1, FUNCT_2:121;

end;

:: deftheorem Def44 defines CastSeq MODELC_2:def 44 :

definition

let S be non empty set ;
let t be sequence of S;
let k be Nat;
func Shift (t,k) -> sequence of S means :Def45: :: MODELC_2:def 45
for n being Nat holds it . n = t . (n + k);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def45 defines Shift MODELC_2:def 45 :

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 46
CastSeq (Shift ((CastSeq (t,S)),k));
correctness ;

end;

:: deftheorem defines Shift MODELC_2:def 46 :

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 47
Shift (t,k,S);
correctness ;

end;

:: deftheorem defines Shift MODELC_2:def 47 :

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

let S be non empty set ;
let f be set ;
func Not_0 (f,S) -> Element of ModelSP (Inf_seq S) means :Def48: :: MODELC_2:def 48
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def48 defines Not_0 MODELC_2:def 48 :

Lm31: for S being non empty set ex o being UnOp of (ModelSP (Inf_seq S)) st
for f being set st f in ModelSP (Inf_seq S) holds
o . f = Not_0 (f,S)

proof end;

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 = 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 ;
func Not_ S -> UnOp of (ModelSP (Inf_seq S)) means :Def49: :: MODELC_2:def 49
for f being set st f in ModelSP (Inf_seq S) holds
it . f = Not_0 (f,S);
existence by Lm31;
uniqueness by Lm32;

end;

:: deftheorem Def49 defines Not_ MODELC_2:def 49 :

definition

let S be non empty set ;
let f be Function of (Inf_seq S),BOOLEAN;
let t be set ;
func Next_univ (t,f) -> Element of BOOLEAN equals :Def50: :: MODELC_2:def 50
TRUE if ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE )
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def50 defines Next_univ MODELC_2:def 50 :

definition

let S be non empty set ;
let f be set ;
func Next_0 (f,S) -> Element of ModelSP (Inf_seq S) means :Def51: :: MODELC_2:def 51
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def51 defines Next_0 MODELC_2:def 51 :

Lm33: for S being non empty set ex o being UnOp of (ModelSP (Inf_seq S)) st
for f being set st f in ModelSP (Inf_seq S) holds
o . f = Next_0 (f,S)

proof end;

Lm34: 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 ;
func Next_ S -> UnOp of (ModelSP (Inf_seq S)) means :Def52: :: MODELC_2:def 52
for f being set st f in ModelSP (Inf_seq S) holds
it . f = Next_0 (f,S);
existence by Lm33;
uniqueness by Lm34;

end;

:: deftheorem Def52 defines Next_ MODELC_2:def 52 :

definition

let S be non empty set ;
let f, g be set ;
func And_0 (f,g,S) -> Element of ModelSP (Inf_seq S) means :Def53: :: MODELC_2:def 53
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def53 defines And_0 MODELC_2:def 53 :

Lm35: for S being non empty set ex o 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
o . (f,g) = And_0 (f,g,S)

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) = 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 ;
func And_ 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) = And_0 (f,g,S);
existence by Lm35;
uniqueness by Lm36;

end;

:: deftheorem Def54 defines And_ MODELC_2:def 54 :

definition

let S be non empty set ;
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 :Def55: :: MODELC_2:def 55
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 ;

end;

:: deftheorem Def55 defines Until_univ MODELC_2:def 55 :

definition

let S be non empty set ;
let f, g be set ;
func Until_0 (f,g,S) -> Element of ModelSP (Inf_seq S) means :Def56: :: MODELC_2:def 56
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def56 defines Until_0 MODELC_2:def 56 :

Lm37: for S being non empty set ex o 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
o . (f,g) = Until_0 (f,g,S)

proof end;

Lm38: 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 ;
func Until_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def57: :: MODELC_2:def 57
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 by Lm37;
uniqueness by Lm38;

end;

:: deftheorem Def57 defines Until_ MODELC_2:def 57 :

Lm39: for S being non empty set ex o 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
o . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g)))

proof end;

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

Lm41: for S being non empty set ex o 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
o . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g)))

proof end;

Lm42: 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 ;
func Or_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def58: :: MODELC_2:def 58
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 by Lm39;
uniqueness by Lm40;
func Release_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def59: :: MODELC_2:def 59
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 by Lm41;
uniqueness by Lm42;

end;

:: deftheorem Def58 defines Or_ MODELC_2:def 58 :

:: deftheorem Def59 defines Release_ MODELC_2:def 59 :

definition

let S be non empty set ;
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S));
func Inf_seqModel (S,BASSIGN) -> LTLModelStr equals :: MODELC_2:def 60
LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #);
coherence ;

end;

:: deftheorem defines Inf_seqModel MODELC_2:def 60 :

registration

let S be non empty set ;
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S));
cluster Inf_seqModel (S,BASSIGN) -> non empty strict with_basic ;
coherence

proof end;

end;

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));
pred t |= f means :Def61: :: MODELC_2:def 61
(Fid (f,(Inf_seq S))) . t = TRUE ;

end;

:: deftheorem Def61 defines |= MODELC_2:def 61 :

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;

theorem :: MODELC_2:56

for S being non empty set
for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( f 'or' g = 'not' (('not' f) '&' ('not' g)) & f 'R' g = 'not' (('not' f) 'U' ('not' g)) ) by Def58, Def59;

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 )

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

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 )

proof end;

theorem Th60: :: MODELC_2:60

proof end;

theorem Th61: :: MODELC_2:61

proof end;

theorem Th62: :: MODELC_2:62

proof end;

definition

func AtomicFamily -> non empty set equals :: MODELC_2:def 62
bool atomic_LTL;
correctness ;

end;

:: deftheorem defines AtomicFamily MODELC_2:def 62 :

definition

let a, t be set ;
func AtomicFunc (a,t) -> Element of BOOLEAN equals :Def63: :: MODELC_2:def 63
TRUE if ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 )
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def63 defines AtomicFunc MODELC_2:def 63 :

Lm43: 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 ;
func AtomicAsgn a -> Element of ModelSP (Inf_seq AtomicFamily) means :Def64: :: MODELC_2:def 64
for t being set st t in Inf_seq AtomicFamily holds
(Fid (it,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def64 defines AtomicAsgn MODELC_2:def 64 :

definition

func AtomicBasicAsgn -> non empty Subset of (ModelSP (Inf_seq AtomicFamily)) equals :: MODELC_2:def 65
{ x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ;
correctness

proof end;

end;

:: deftheorem defines AtomicBasicAsgn MODELC_2:def 65 :

definition

func AtomicKai -> Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) means :Def66: :: MODELC_2:def 66
for a being set st a in atomic_LTL holds
it . a = AtomicAsgn a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def66 defines AtomicKai MODELC_2:def 66 :

definition

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

end;

:: deftheorem Def67 defines |= MODELC_2:def 67 :

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 :Def68: :: MODELC_2:def 68
for H being LTL-formula st H in W holds
r |= H;

end;

:: deftheorem Def68 defines |= MODELC_2:def 68 :

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 69
{ x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } ;
correctness

proof end;

end;

:: deftheorem defines 'X' MODELC_2:def 69 :

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 )

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

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;

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;

theorem :: MODELC_2:79

for S being non empty set
for t being Element of Inf_seq S holds Shift (t,0) = t by Lm29;

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

theorem :: MODELC_2:81

for S being non empty set
for seq being sequence of S holds CastSeq ((CastSeq seq),S) = seq by Def44;

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

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;