:: Model Checking, Part II :: by Kazuhisa Ishida :: :: Received April 21, 2008 :: Copyright (c) 2008-2012 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 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 set holds ( ( x is Nat implies CastNat x = x ) & ( x is not Nat implies CastNat x = 0 ) ); Lm1: for m, n, k being Nat st m < n & n <= k + 1 holds m <= k proofend; :: 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 ; 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 <*0*> ^ p; coherence <*0*> ^ p is FinSequence of NAT ; let q be FinSequence of NAT ; funcp '&' q -> FinSequence of NAT equals :: MODELC_2:def 4 (<*1*> ^ p) ^ q; coherence (<*1*> ^ p) ^ q is FinSequence of NAT ; funcp '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 = <*0*> ^ 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 ; funcp 'U' q -> FinSequence of NAT equals :: MODELC_2:def 7 (<*4*> ^ p) ^ q; coherence (<*4*> ^ p) ^ q is FinSequence of NAT ; funcp '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) proofend; :: 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 ) ) proofend; 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 proofend; 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 ; attrIT 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 cluster Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like LTL-formula-like for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st b1 is LTL-formula-like proofend; 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 ) proofend; registration let n be Nat; cluster atom. n -> LTL-formula-like ; coherence atom. n is LTL-formula-like proofend; end; registration let H be LTL-formula; cluster 'not' H -> LTL-formula-like ; coherence 'not' H is LTL-formula-like proofend; cluster 'X' H -> LTL-formula-like ; coherence 'X' H is LTL-formula-like proofend; let G be LTL-formula; clusterH '&' G -> LTL-formula-like ; coherence H '&' G is LTL-formula-like proofend; clusterH 'or' G -> LTL-formula-like ; coherence H 'or' G is LTL-formula-like proofend; clusterH 'U' G -> LTL-formula-like ; coherence H 'U' G is LTL-formula-like proofend; clusterH 'R' G -> LTL-formula-like ; coherence H 'R' G is LTL-formula-like proofend; end; definition let H be LTL-formula; attrH is atomic means :Def11: :: MODELC_2:def 11 ex n being Nat st H = atom. n; attrH is negative means :Def12: :: MODELC_2:def 12 ex H1 being LTL-formula st H = 'not' H1; attrH is conjunctive means :Def13: :: MODELC_2:def 13 ex F, G being LTL-formula st H = F '&' G; attrH is disjunctive means :Def14: :: MODELC_2:def 14 ex F, G being LTL-formula st H = F 'or' G; attrH is next means :Def15: :: MODELC_2:def 15 ex H1 being LTL-formula st H = 'X' H1; attrH is Until means :Def16: :: MODELC_2:def 16 ex F, G being LTL-formula st H = F 'U' G; attrH 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_:_ for H being LTL-formula holds ( H is atomic iff ex n being Nat st H = atom. n ); :: deftheorem Def12 defines negative MODELC_2:def_12_:_ for H being LTL-formula holds ( H is negative iff ex H1 being LTL-formula st H = 'not' H1 ); :: deftheorem Def13 defines conjunctive MODELC_2:def_13_:_ for H being LTL-formula holds ( H is conjunctive iff ex F, G being LTL-formula st H = F '&' G ); :: deftheorem Def14 defines disjunctive MODELC_2:def_14_:_ for H being LTL-formula holds ( H is disjunctive iff ex F, G being LTL-formula st H = F 'or' G ); :: deftheorem Def15 defines next MODELC_2:def_15_:_ for H being LTL-formula holds ( H is next iff ex H1 being LTL-formula st H = 'X' H1 ); :: deftheorem Def16 defines Until MODELC_2:def_16_:_ for H being LTL-formula holds ( H is Until iff ex F, G being LTL-formula st H = F 'U' G ); :: deftheorem Def17 defines Release MODELC_2:def_17_:_ for H being LTL-formula holds ( H is Release iff ex F, G being LTL-formula st H = F 'R' G ); 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 ) proofend; Lm3: for H being LTL-formula st H is negative holds H . 1 = 0 proofend; Lm4: for H being LTL-formula st H is conjunctive holds H . 1 = 1 proofend; Lm5: for H being LTL-formula st H is disjunctive holds H . 1 = 2 proofend; Lm6: for H being LTL-formula st H is next holds H . 1 = 3 proofend; Lm7: for H being LTL-formula st H is Until holds H . 1 = 4 proofend; Lm8: for H being LTL-formula st H is Release holds H . 1 = 5 proofend; 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 ) proofend; 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 ) ) proofend; theorem Th3: :: MODELC_2:3 for H being LTL-formula holds 1 <= len H proofend; Lm11: for H, F being LTL-formula for sq being FinSequence st H = F ^ sq holds H = F proofend; Lm12: for H, G, H1, G1 being LTL-formula st H '&' G = H1 '&' G1 holds ( H = H1 & G = G1 ) proofend; Lm13: for H, G, H1, G1 being LTL-formula st H 'or' G = H1 'or' G1 holds ( H = H1 & G = G1 ) proofend; Lm14: for H, G, H1, G1 being LTL-formula st H 'U' G = H1 'U' G1 holds ( H = H1 & G = G1 ) proofend; Lm15: for H, G, H1, G1 being LTL-formula st H 'R' G = H1 'R' G1 holds ( H = H1 & G = G1 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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, Def12, Def15; 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, Def13, Def14, Def16, Def17; 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 Lm12, Lm13, Lm14, Lm15; 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 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 ( ( 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 ) ) proofend; 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 Lm12, Lm13, Lm14, Lm15; 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 Lm18, Lm20; 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' (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) proofend; 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) proofend; 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) proofend; 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) proofend; 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) proofend; 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 ) proofend; 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 ) proofend; :: :: The Immediate Constituents of LTL-formulae :: definition let H, F be LTL-formula; predH 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_:_ for H, F being LTL-formula holds ( H is_immediate_constituent_of F iff ( F = 'not' H or F = 'X' H or ex H1 being LTL-formula st ( F = H '&' H1 or F = H1 '&' H or F = H 'or' H1 or F = H1 'or' H or F = H 'U' H1 or F = H1 'U' H or F = H 'R' H1 or F = H1 'R' H ) ) ); theorem Th12: :: MODELC_2:12 for F, G being LTL-formula holds ( ('not' F) . 1 = 0 & (F '&' G) . 1 = 1 & (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 ) proofend; theorem Th13: :: MODELC_2:13 for H, F being LTL-formula holds ( H is_immediate_constituent_of 'not' F iff H = F ) proofend; theorem Th14: :: MODELC_2:14 for H, F being LTL-formula holds ( H is_immediate_constituent_of 'X' F iff H = F ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; theorem Th19: :: MODELC_2:19 for F, H being LTL-formula st F is atomic holds not H is_immediate_constituent_of F proofend; 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 ) proofend; 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 ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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; predH 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 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 ) ) ) proofend; end; :: deftheorem Def22 defines is_subformula_of MODELC_2:def_22_:_ for H, F being LTL-formula holds ( H is_subformula_of F iff ex n being Nat ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds ex H1, F1 being LTL-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) ); theorem :: MODELC_2:27 for H being LTL-formula holds H is_subformula_of H ; definition let H, F be LTL-formula; predH is_proper_subformula_of F means :Def23: :: MODELC_2:def 23 ( H is_subformula_of F & H <> F ); irreflexivity for H being LTL-formula holds ( not H is_subformula_of H or not H <> H ) ; end; :: deftheorem Def23 defines is_proper_subformula_of MODELC_2:def_23_:_ for H, F being LTL-formula holds ( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) ); theorem Th28: :: MODELC_2:28 for H, F being LTL-formula st H is_immediate_constituent_of F holds len H < len F proofend; 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 proofend; 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 proofend; 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 ) proofend; theorem Th32: :: MODELC_2:32 for H, F being LTL-formula st H is_proper_subformula_of F holds len H < len F proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: MODELC_2:36 for G, H being LTL-formula st G is_subformula_of H & H is_subformula_of G holds G = H proofend; 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 proofend; 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 proofend; theorem :: MODELC_2:39 for F, H being LTL-formula st F is_proper_subformula_of 'not' H holds F is_subformula_of H proofend; theorem :: MODELC_2:40 for F, H being LTL-formula st F is_proper_subformula_of 'X' H holds F is_subformula_of H proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; :: :: 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 ) ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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] proofend; 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] proofend; ::*************************************************** ::** ::** definition of LTL model structure. ::** ::**************************************************** 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 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 set holds ( ( x in LTL_WFF implies CastLTL x = x ) & ( not x in LTL_WFF implies CastLTL x = atom. 0 ) ); definition attrc1 is strict ; struct LTLModelStr -> OrthoLattStr ; aggrLTLModelStr(# 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; proofend; 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; predf 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_:_ for V being LTLModelStr for Kai being Function of atomic_LTL, the BasicAssign of V for f being Function of LTL_WFF, the carrier of V holds ( f is-Evaluation-for Kai iff for H being LTL-formula holds ( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) ); definition let V be LTLModelStr ; let Kai be Function of atomic_LTL, the BasicAssign of V; let f be Function of LTL_WFF, the carrier of V; let n be Nat; predf 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_:_ for V being LTLModelStr for Kai being Function of atomic_LTL, the BasicAssign of V for f being Function of LTL_WFF, the carrier of V for n being Nat holds ( f is-PreEvaluation-for n,Kai iff for H being LTL-formula st len H <= n holds ( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) ); definition let V be LTLModelStr ; let Kai be Function of atomic_LTL, the BasicAssign of V; let f, h be Function of LTL_WFF, the carrier of V; let n be Nat; let H be LTL-formula; 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 ( ( len H > n + 1 implies f . H is set ) & ( len H = n + 1 & H is atomic implies Kai . H is set ) & ( len H = n + 1 & H is negative implies the Compl of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is conjunctive implies the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is disjunctive implies the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is next implies the NEXT of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is Until implies the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is Release implies the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H < n + 1 implies h . H is set ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & not len H < n + 1 implies {} is set ) ) ; consistency for b1 being set holds ( ( len H > n + 1 & len H = n + 1 & H is atomic implies ( b1 = f . H iff b1 = Kai . H ) ) & ( len H > n + 1 & len H = n + 1 & H is negative implies ( b1 = f . H iff b1 = the Compl of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is conjunctive implies ( b1 = f . H iff b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H = n + 1 & H is disjunctive implies ( b1 = f . H iff b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H = n + 1 & H is next implies ( b1 = f . H iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is Until implies ( b1 = f . H iff b1 = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H = n + 1 & H is Release implies ( b1 = f . H iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H < n + 1 implies ( b1 = f . H iff b1 = h . H ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is negative implies ( b1 = Kai . H iff b1 = the Compl of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is conjunctive implies ( b1 = Kai . H iff b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is disjunctive implies ( b1 = Kai . H iff b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is next implies ( b1 = Kai . H iff b1 = the NEXT of V . (h . (the_argument_of 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 . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is Release implies ( b1 = Kai . H iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H < n + 1 implies ( b1 = Kai . H iff b1 = h . H ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is conjunctive implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is disjunctive implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is next implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Until implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Release implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H < n + 1 implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is disjunctive implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is next implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Until implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Release implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is conjunctive & len H < n + 1 implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = h . H ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is next implies ( b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Until implies ( b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Release implies ( b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is disjunctive & len H < n + 1 implies ( b1 = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) 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 . (the_argument_of H)) iff b1 = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is next & len H = n + 1 & H is Release implies ( b1 = the NEXT of V . (h . (the_argument_of H)) iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is next & len H < n + 1 implies ( b1 = the NEXT of V . (h . (the_argument_of 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 . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is Until & len H < n + 1 implies ( b1 = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = h . H ) ) & ( len H = n + 1 & H is Release & len H < n + 1 implies ( b1 = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = h . H ) ) ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21; 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 . (the_argument_of H)) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is disjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is next implies GraftEval (V,Kai,f,h,n,H) = the NEXT of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is Until implies GraftEval (V,Kai,f,h,n,H) = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is Release implies GraftEval (V,Kai,f,h,n,H) = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = h . H ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) ); definition let C be LTLModelStr ; attrC 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(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #); coherence LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #) is LTLModelStr ; end; :: deftheorem defines TrivialLTLModel MODELC_2:def_31_:_ TrivialLTLModel = LTLModelStr(# 1,([#] 1),op2,op2,op1,op1,op2,op2 #); registration cluster TrivialLTLModel -> non empty strict with_basic ; coherence ( TrivialLTLModel is with_basic & TrivialLTLModel is strict & not TrivialLTLModel is empty ) proofend; end; registration cluster non empty for LTLModelStr ; existence not for b1 being LTLModelStr holds b1 is empty proofend; end; registration cluster non empty with_basic for LTLModelStr ; existence ex b1 being non empty LTLModelStr st b1 is with_basic proofend; end; definition mode LTLModel is non empty with_basic LTLModelStr ; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ; proofend; 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) ) ) proofend; 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 proofend; 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) ) ) ); 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) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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; funcf '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; ; funcf '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 (('not' H),Kai) = 'not' (Evaluate (H,Kai)) proofend; 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)) proofend; 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)) proofend; 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)) proofend; 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)) proofend; 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)) proofend; ::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 set ; 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 A1, FUNCT_2:66; end; :: deftheorem Def41 defines CastSeq MODELC_2:def_41_:_ for S being non empty set for t being set st t is Element of Inf_seq S holds CastSeq (t,S) = t; 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); Lm29: for S being non empty set for seq being Element of Inf_seq S holds Shift (seq,0) = seq proofend; 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)) proofend; :: definition of Not_ unary operation of Model Space. definition let S be non empty set ; let f be set ; func Not_0 (f,S) -> Element of ModelSP (Inf_seq S) means :Def44: :: MODELC_2:def 44 for t being set st t in Inf_seq S holds ( 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE ); existence ex b1 being Element of ModelSP (Inf_seq S) st for t being set st t in Inf_seq S holds ( 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds ( 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds ( 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE iff (Fid (b2,(Inf_seq S))) . t = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def44 defines Not_0 MODELC_2:def_44_:_ for S being non empty set for f being set for b3 being Element of ModelSP (Inf_seq S) holds ( b3 = Not_0 (f,S) iff for t being set st t in Inf_seq S holds ( 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE iff (Fid (b3,(Inf_seq S))) . t = TRUE ) ); Lm31: for S being non empty set for o1, o2 being UnOp of (ModelSP (Inf_seq S)) st ( for f being set st f in ModelSP (Inf_seq S) holds o1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP (Inf_seq S) holds o2 . f = Not_0 (f,S) ) holds o1 = o2 proofend; definition let S be non empty set ; func Not_ S -> UnOp of (ModelSP (Inf_seq S)) means :Def45: :: MODELC_2:def 45 for f being set st f in ModelSP (Inf_seq S) holds it . f = Not_0 (f,S); existence ex b1 being UnOp of (ModelSP (Inf_seq S)) st for f being set st f in ModelSP (Inf_seq S) holds b1 . f = Not_0 (f,S) proofend; uniqueness for b1, b2 being UnOp of (ModelSP (Inf_seq S)) st ( for f being set st f in ModelSP (Inf_seq S) holds b1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP (Inf_seq S) holds b2 . f = Not_0 (f,S) ) holds b1 = b2 by Lm31; end; :: deftheorem Def45 defines Not_ MODELC_2:def_45_:_ for S being non empty set for b2 being UnOp of (ModelSP (Inf_seq S)) holds ( b2 = Not_ S iff for f being set st f in ModelSP (Inf_seq S) 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 (Inf_seq S),BOOLEAN; let t be set ; func Next_univ (t,f) -> Element of BOOLEAN equals :Def46: :: MODELC_2:def 46 TRUE if ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE ) otherwise FALSE ; correctness 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 (Inf_seq S),BOOLEAN for t being set holds ( ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE implies Next_univ (t,f) = TRUE ) & ( ( not t is Element of Inf_seq S or not f . (Shift (t,1,S)) = TRUE ) implies Next_univ (t,f) = FALSE ) ); definition let S be non empty set ; let f be set ; func Next_0 (f,S) -> Element of ModelSP (Inf_seq S) means :Def47: :: MODELC_2:def 47 for t being set st t in Inf_seq S holds ( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE ); existence ex b1 being Element of ModelSP (Inf_seq S) st for t being set st t in Inf_seq S holds ( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds ( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds ( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b2,(Inf_seq S))) . t = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def47 defines Next_0 MODELC_2:def_47_:_ for S being non empty set for f being set for b3 being Element of ModelSP (Inf_seq S) holds ( b3 = Next_0 (f,S) iff for t being set st t in Inf_seq S holds ( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b3,(Inf_seq S))) . t = TRUE ) ); Lm32: for S being non empty set for o1, o2 being UnOp of (ModelSP (Inf_seq S)) st ( for f being set st f in ModelSP (Inf_seq S) holds o1 . f = Next_0 (f,S) ) & ( for f being set st f in ModelSP (Inf_seq S) holds o2 . f = Next_0 (f,S) ) holds o1 = o2 proofend; definition let S be non empty set ; func Next_ S -> UnOp of (ModelSP (Inf_seq S)) means :Def48: :: MODELC_2:def 48 for f being set st f in ModelSP (Inf_seq S) holds it . f = Next_0 (f,S); existence ex b1 being UnOp of (ModelSP (Inf_seq S)) st for f being set st f in ModelSP (Inf_seq S) holds b1 . f = Next_0 (f,S) proofend; uniqueness for b1, b2 being UnOp of (ModelSP (Inf_seq S)) st ( for f being set st f in ModelSP (Inf_seq S) holds b1 . f = Next_0 (f,S) ) & ( for f being set st f in ModelSP (Inf_seq S) holds b2 . f = Next_0 (f,S) ) holds b1 = b2 by Lm32; end; :: deftheorem Def48 defines Next_ MODELC_2:def_48_:_ for S being non empty set for b2 being UnOp of (ModelSP (Inf_seq S)) holds ( b2 = Next_ S iff for f being set st f in ModelSP (Inf_seq S) 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 (Inf_seq S) means :Def49: :: MODELC_2:def 49 for t being set st t in Inf_seq S holds ( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE ); existence ex b1 being Element of ModelSP (Inf_seq S) st for t being set st t in Inf_seq S holds ( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds ( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds ( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b2,(Inf_seq S))) . t = TRUE ) ) holds b1 = b2 proofend; 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 (Inf_seq S) holds ( b4 = And_0 (f,g,S) iff for t being set st t in Inf_seq S holds ( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b4,(Inf_seq S))) . t = TRUE ) ); Lm33: for S being non empty set for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o2 . (f,g) = And_0 (f,g,S) ) holds o1 = o2 proofend; definition let S be non empty set ; func And_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def50: :: MODELC_2:def 50 for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds it . (f,g) = And_0 (f,g,S); existence ex b1 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 b1 . (f,g) = And_0 (f,g,S) proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (f,g) = And_0 (f,g,S) ) holds b1 = b2 by Lm33; end; :: deftheorem Def50 defines And_ MODELC_2:def_50_:_ for S being non empty set for b2 being BinOp of (ModelSP (Inf_seq S)) holds ( b2 = And_ S iff for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) 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 (Inf_seq S),BOOLEAN; let t be set ; func Until_univ (t,f,g,S) -> Element of BOOLEAN equals :Def51: :: MODELC_2:def 51 TRUE if ( t is Element of Inf_seq S & ex m being Nat st ( ( for j being Nat st j < m holds f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) ) otherwise FALSE ; correctness 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 (Inf_seq S),BOOLEAN for t being set holds ( ( t is Element of Inf_seq S & ex m being Nat st ( ( for j being Nat st j < m holds f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) implies Until_univ (t,f,g,S) = TRUE ) & ( ( not t is Element of Inf_seq S or for m being Nat holds ( ex j being Nat st ( j < m & not f . (Shift (t,j,S)) = TRUE ) or not g . (Shift (t,m,S)) = TRUE ) ) implies Until_univ (t,f,g,S) = FALSE ) ); definition let S be non empty set ; let f, g be set ; func Until_0 (f,g,S) -> Element of ModelSP (Inf_seq S) means :Def52: :: MODELC_2:def 52 for t being set st t in Inf_seq S holds ( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (it,(Inf_seq S))) . t = TRUE ); existence ex b1 being Element of ModelSP (Inf_seq S) st for t being set st t in Inf_seq S holds ( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds ( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b1,(Inf_seq S))) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds ( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b2,(Inf_seq S))) . t = TRUE ) ) holds b1 = b2 proofend; 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 (Inf_seq S) holds ( b4 = Until_0 (f,g,S) iff for t being set st t in Inf_seq S holds ( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b4,(Inf_seq S))) . t = TRUE ) ); Lm34: for S being non empty set for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o1 . (f,g) = Until_0 (f,g,S) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o2 . (f,g) = Until_0 (f,g,S) ) holds o1 = o2 proofend; definition let S be non empty set ; func Until_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def53: :: MODELC_2:def 53 for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds it . (f,g) = Until_0 (f,g,S); existence ex b1 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 b1 . (f,g) = Until_0 (f,g,S) proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (f,g) = Until_0 (f,g,S) ) holds b1 = b2 by Lm34; end; :: deftheorem Def53 defines Until_ MODELC_2:def_53_:_ for S being non empty set for b2 being BinOp of (ModelSP (Inf_seq S)) holds ( b2 = Until_ S iff for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds b2 . (f,g) = Until_0 (f,g,S) ); Lm35: for S being non empty set for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o1 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o2 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds o1 = o2 proofend; Lm36: for S being non empty set for o1, o2 being BinOp of (ModelSP (Inf_seq S)) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o1 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds o2 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds o1 = o2 proofend; definition let S be non empty set ; func Or_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def54: :: MODELC_2:def 54 for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds it . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))); existence ex b1 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 b1 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (f,g) = (Not_ S) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds b1 = b2 by Lm35; func Release_ S -> BinOp of (ModelSP (Inf_seq S)) means :Def55: :: MODELC_2:def 55 for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds it . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))); existence ex b1 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 b1 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds b1 = b2 by Lm36; end; :: deftheorem Def54 defines Or_ MODELC_2:def_54_:_ for S being non empty set for b2 being BinOp of (ModelSP (Inf_seq S)) holds ( b2 = Or_ S iff for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) 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 (Inf_seq S)) holds ( b2 = Release_ S iff for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds b2 . (f,g) = (Not_ S) . ((Until_ 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 (Inf_seq S)); func Inf_seqModel (S,BASSIGN) -> LTLModelStr equals :: MODELC_2:def 56 LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #); coherence LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #) 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 (Inf_seq S)) holds Inf_seqModel (S,BASSIGN) = LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #); registration let S be non empty set ; let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); 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 ) proofend; end; :: definition of correctness of Assign of Inf_seqModel(S,BASSIGN) definition let S be non empty set ; let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); let t be Element of Inf_seq S; let f be Assign of (Inf_seqModel (S,BASSIGN)); predt |= f means :Def57: :: MODELC_2:def 57 (Fid (f,(Inf_seq S))) . t = TRUE ; end; :: deftheorem Def57 defines |= MODELC_2:def_57_:_ for S being non empty set for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) for t being Element of Inf_seq S for f being Assign of (Inf_seqModel (S,BASSIGN)) holds ( t |= f iff (Fid (f,(Inf_seq S))) . t = TRUE ); 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 Def54, Def55; 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 ) proofend; 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 ) ) proofend; 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 ) proofend; theorem Th60: :: MODELC_2:60 for S being non empty set for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) for t being Element of Inf_seq S for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds ( t |= f 'U' g iff ex m being Nat st ( ( for j being Nat st j < m holds Shift (t,j) |= f ) & Shift (t,m) |= g ) ) proofend; theorem Th61: :: MODELC_2:61 for S being non empty set for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) for t being Element of Inf_seq S for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds ( t |= f 'or' g iff ( t |= f or t |= g ) ) proofend; theorem Th62: :: MODELC_2:62 for S being non empty set for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) for t being Element of Inf_seq S for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds ( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds Shift (t,j) |= 'not' f ) holds Shift (t,m) |= g ) proofend; :: definition of correctness of LTL-formula & its basic properties. definition func AtomicFamily -> non empty set equals :: MODELC_2:def 58 bool atomic_LTL; correctness coherence bool atomic_LTL is non empty set ; ; end; :: deftheorem defines AtomicFamily MODELC_2:def_58_:_ AtomicFamily = bool atomic_LTL; definition let a, t be set ; func AtomicFunc (a,t) -> Element of BOOLEAN equals :Def59: :: MODELC_2:def 59 TRUE if ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 ) otherwise FALSE ; correctness coherence ( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies TRUE is Element of BOOLEAN ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def59 defines AtomicFunc MODELC_2:def_59_:_ for a, t being set holds ( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies AtomicFunc (a,t) = TRUE ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies AtomicFunc (a,t) = FALSE ) ); Lm37: for S being non empty set for f1, f2 being set st f1 in ModelSP S & f2 in ModelSP S & Fid (f1,S) = Fid (f2,S) holds f1 = f2 proofend; definition let a be set ; func AtomicAsgn a -> Element of ModelSP (Inf_seq AtomicFamily) means :Def60: :: MODELC_2:def 60 for t being set st t in Inf_seq AtomicFamily holds (Fid (it,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t); existence ex b1 being Element of ModelSP (Inf_seq AtomicFamily) st for t being set st t in Inf_seq AtomicFamily holds (Fid (b1,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) proofend; uniqueness for b1, b2 being Element of ModelSP (Inf_seq AtomicFamily) st ( for t being set st t in Inf_seq AtomicFamily holds (Fid (b1,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ) & ( for t being set st t in Inf_seq AtomicFamily holds (Fid (b2,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ) holds b1 = b2 proofend; end; :: deftheorem Def60 defines AtomicAsgn MODELC_2:def_60_:_ for a being set for b2 being Element of ModelSP (Inf_seq AtomicFamily) holds ( b2 = AtomicAsgn a iff for t being set st t in Inf_seq AtomicFamily holds (Fid (b2,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ); definition func AtomicBasicAsgn -> non empty Subset of (ModelSP (Inf_seq AtomicFamily)) equals :: MODELC_2:def 61 { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ; correctness coherence { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } is non empty Subset of (ModelSP (Inf_seq AtomicFamily)); proofend; end; :: deftheorem defines AtomicBasicAsgn MODELC_2:def_61_:_ AtomicBasicAsgn = { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ; definition func AtomicKai -> Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) means :Def62: :: MODELC_2:def 62 for a being set st a in atomic_LTL holds it . a = AtomicAsgn a; existence ex b1 being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) st for a being set st a in atomic_LTL holds b1 . a = AtomicAsgn a proofend; uniqueness for b1, b2 being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) 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 proofend; end; :: deftheorem Def62 defines AtomicKai MODELC_2:def_62_:_ for b1 being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) 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; predr |= 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; predr |= W means :Def64: :: MODELC_2:def 64 for H being LTL-formula st H in W holds r |= H; end; :: deftheorem Def64 defines |= MODELC_2:def_64_:_ for r being Element of Inf_seq AtomicFamily for W being Subset of LTL_WFF holds ( r |= W iff for H being LTL-formula st H in W holds r |= H ); 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; proofend; 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 (CastSeq (r,AtomicFamily)) . 0 ) proofend; 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 ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) ) proofend; 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 ) proofend; 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) ) proofend; 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) ) proofend; 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)) ) proofend; 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) ) proofend; 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))) ) proofend; 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))) ) proofend; 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 ) proofend; :: theorems for external articles theorem :: MODELC_2:78 for H being LTL-formula holds ( ( H is atomic implies ( not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is negative implies ( not H is atomic & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is conjunctive implies ( not H is atomic & not H is negative & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is disjunctive implies ( not H is atomic & not H is negative & not H is conjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is next implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is Until & not H is Release ) ) & ( H is Until implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Release ) ) & ( H is Release implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until ) ) ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21; 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 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 proofend;