:: Model Checking, Part {I} :: by Kazuhisa Ishida :: :: Received November 14, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin Lm1: for m, n, k being Nat st m < n & n <= k + 1 holds m <= k proofend; definition let x, S be set ; let a be Element of S; func k_id (x,S,a) -> Element of S equals :Def1: :: MODELC_1:def 1 x if x in S otherwise a; correctness coherence ( ( x in S implies x is Element of S ) & ( not x in S implies a is Element of S ) ); consistency for b1 being Element of S holds verum; ; end; :: deftheorem Def1 defines k_id MODELC_1:def_1_:_ for x, S being set for a being Element of S holds ( ( x in S implies k_id (x,S,a) = x ) & ( not x in S implies k_id (x,S,a) = a ) ); definition let x be set ; func k_nat x -> Element of NAT equals :Def2: :: MODELC_1:def 2 x if x in NAT otherwise 0 ; correctness coherence ( ( x in NAT implies x is Element of NAT ) & ( not x in NAT implies 0 is Element of NAT ) ); consistency for b1 being Element of NAT holds verum; ; end; :: deftheorem Def2 defines k_nat MODELC_1:def_2_:_ for x being set holds ( ( x in NAT implies k_nat x = x ) & ( not x in NAT implies k_nat x = 0 ) ); definition let f be Function; let x, a be set ; func UnivF (x,f,a) -> set equals :Def3: :: MODELC_1:def 3 f . x if x in dom f otherwise a; correctness coherence ( ( x in dom f implies f . x is set ) & ( not x in dom f implies a is set ) ); consistency for b1 being set holds verum; ; end; :: deftheorem Def3 defines UnivF MODELC_1:def_3_:_ for f being Function for x, a being set holds ( ( x in dom f implies UnivF (x,f,a) = f . x ) & ( not x in dom f implies UnivF (x,f,a) = a ) ); definition let a be set ; func Castboolean a -> boolean set equals :Def4: :: MODELC_1:def 4 a if a is boolean set otherwise FALSE ; correctness coherence ( ( a is boolean set implies a is boolean set ) & ( a is not boolean set implies FALSE is boolean set ) ); consistency for b1 being boolean set holds verum; ; end; :: deftheorem Def4 defines Castboolean MODELC_1:def_4_:_ for a being set holds ( ( a is boolean set implies Castboolean a = a ) & ( a is not boolean set implies Castboolean a = FALSE ) ); definition let X, a be set ; func CastBool (a,X) -> Subset of X equals :Def5: :: MODELC_1:def 5 a if a c= X otherwise {} ; correctness coherence ( ( a c= X implies a is Subset of X ) & ( not a c= X implies {} is Subset of X ) ); consistency for b1 being Subset of X holds verum; by XBOOLE_1:2; end; :: deftheorem Def5 defines CastBool MODELC_1:def_5_:_ for X, a being set holds ( ( a c= X implies CastBool (a,X) = a ) & ( not a c= X implies CastBool (a,X) = {} ) ); :: The operations to make CTL-formulae definition let n be Element of NAT ; func atom. n -> FinSequence of NAT equals :: MODELC_1:def 6 <*(5 + n)*>; coherence <*(5 + n)*> is FinSequence of NAT ; end; :: deftheorem defines atom. MODELC_1:def_6_:_ for n being Element of NAT holds atom. n = <*(5 + n)*>; definition let p be FinSequence of NAT ; func 'not' p -> FinSequence of NAT equals :: MODELC_1:def 7 <*0*> ^ p; coherence <*0*> ^ p is FinSequence of NAT ; let q be FinSequence of NAT ; funcp '&' q -> FinSequence of NAT equals :: MODELC_1:def 8 (<*1*> ^ p) ^ q; coherence (<*1*> ^ p) ^ q is FinSequence of NAT ; end; :: deftheorem defines 'not' MODELC_1:def_7_:_ for p being FinSequence of NAT holds 'not' p = <*0*> ^ p; :: deftheorem defines '&' MODELC_1:def_8_:_ for p, q being FinSequence of NAT holds p '&' q = (<*1*> ^ p) ^ q; definition let p be FinSequence of NAT ; func EX p -> FinSequence of NAT equals :: MODELC_1:def 9 <*2*> ^ p; coherence <*2*> ^ p is FinSequence of NAT ; func EG p -> FinSequence of NAT equals :: MODELC_1:def 10 <*3*> ^ p; coherence <*3*> ^ p is FinSequence of NAT ; let q be FinSequence of NAT ; funcp EU q -> FinSequence of NAT equals :: MODELC_1:def 11 (<*4*> ^ p) ^ q; coherence (<*4*> ^ p) ^ q is FinSequence of NAT ; end; :: deftheorem defines EX MODELC_1:def_9_:_ for p being FinSequence of NAT holds EX p = <*2*> ^ p; :: deftheorem defines EG MODELC_1:def_10_:_ for p being FinSequence of NAT holds EG p = <*3*> ^ p; :: deftheorem defines EU MODELC_1:def_11_:_ for p, q being FinSequence of NAT holds p EU q = (<*4*> ^ p) ^ q; Lm2: for n being Element of NAT for p, q being FinSequence of NAT holds len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q) proofend; :: The set of all well formed formulae of CTL-language definition func CTL_WFF -> non empty set means :Def12: :: MODELC_1:def 12 ( ( for a being set st a in it holds a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in it ) & ( for p being FinSequence of NAT st p in it holds 'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds p '&' q in it ) & ( for p being FinSequence of NAT st p in it holds EX p in it ) & ( for p being FinSequence of NAT st p in it holds EG p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds p EU q in it ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds EX p in D ) & ( for p being FinSequence of NAT st p in D holds EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p EU q in D ) holds it c= D ) ); existence ex b1 being non empty set st ( ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for n being Element of 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 being FinSequence of NAT st p in b1 holds EX p in b1 ) & ( for p being FinSequence of NAT st p in b1 holds EG p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p EU 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 Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds EX p in D ) & ( for p being FinSequence of NAT st p in D holds EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p EU q in D ) holds 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 Element of 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 being FinSequence of NAT st p in b1 holds EX p in b1 ) & ( for p being FinSequence of NAT st p in b1 holds EG p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p EU 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 Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds EX p in D ) & ( for p being FinSequence of NAT st p in D holds EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p EU q in D ) holds b1 c= D ) & ( for a being set st a in b2 holds a is FinSequence of NAT ) & ( for n being Element of 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 being FinSequence of NAT st p in b2 holds EX p in b2 ) & ( for p being FinSequence of NAT st p in b2 holds EG p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds p EU 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 Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds EX p in D ) & ( for p being FinSequence of NAT st p in D holds EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p EU q in D ) holds b2 c= D ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines CTL_WFF MODELC_1:def_12_:_ for b1 being non empty set holds ( b1 = CTL_WFF iff ( ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for n being Element of 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 being FinSequence of NAT st p in b1 holds EX p in b1 ) & ( for p being FinSequence of NAT st p in b1 holds EG p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p EU 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 Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds EX p in D ) & ( for p being FinSequence of NAT st p in D holds EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p EU q in D ) holds b1 c= D ) ) ); definition let IT be FinSequence of NAT ; attrIT is CTL-formula-like means :Def13: :: MODELC_1:def 13 IT is Element of CTL_WFF ; end; :: deftheorem Def13 defines CTL-formula-like MODELC_1:def_13_:_ for IT being FinSequence of NAT holds ( IT is CTL-formula-like iff IT is Element of CTL_WFF ); registration cluster Relation-like NAT -defined NAT -valued Function-like FinSequence-like CTL-formula-like for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st b1 is CTL-formula-like proofend; end; definition mode CTL-formula is CTL-formula-like FinSequence of NAT ; end; theorem Th1: :: MODELC_1:1 for a being set holds ( a is CTL-formula iff a in CTL_WFF ) proofend; registration let n be Element of NAT ; cluster atom. n -> CTL-formula-like ; coherence atom. n is CTL-formula-like proofend; end; registration let H be CTL-formula; cluster 'not' H -> CTL-formula-like ; coherence 'not' H is CTL-formula-like proofend; cluster EX H -> CTL-formula-like ; coherence EX H is CTL-formula-like proofend; cluster EG H -> CTL-formula-like ; coherence EG H is CTL-formula-like proofend; let G be CTL-formula; clusterH '&' G -> CTL-formula-like ; coherence H '&' G is CTL-formula-like proofend; clusterH EU G -> CTL-formula-like ; coherence H EU G is CTL-formula-like proofend; end; definition let H be CTL-formula; attrH is atomic means :Def14: :: MODELC_1:def 14 ex n being Element of NAT st H = atom. n; attrH is negative means :Def15: :: MODELC_1:def 15 ex H1 being CTL-formula st H = 'not' H1; attrH is conjunctive means :Def16: :: MODELC_1:def 16 ex F, G being CTL-formula st H = F '&' G; attrH is ExistNext means :Def17: :: MODELC_1:def 17 ex H1 being CTL-formula st H = EX H1; attrH is ExistGlobal means :Def18: :: MODELC_1:def 18 ex H1 being CTL-formula st H = EG H1; attrH is ExistUntill means :Def19: :: MODELC_1:def 19 ex F, G being CTL-formula st H = F EU G; end; :: deftheorem Def14 defines atomic MODELC_1:def_14_:_ for H being CTL-formula holds ( H is atomic iff ex n being Element of NAT st H = atom. n ); :: deftheorem Def15 defines negative MODELC_1:def_15_:_ for H being CTL-formula holds ( H is negative iff ex H1 being CTL-formula st H = 'not' H1 ); :: deftheorem Def16 defines conjunctive MODELC_1:def_16_:_ for H being CTL-formula holds ( H is conjunctive iff ex F, G being CTL-formula st H = F '&' G ); :: deftheorem Def17 defines ExistNext MODELC_1:def_17_:_ for H being CTL-formula holds ( H is ExistNext iff ex H1 being CTL-formula st H = EX H1 ); :: deftheorem Def18 defines ExistGlobal MODELC_1:def_18_:_ for H being CTL-formula holds ( H is ExistGlobal iff ex H1 being CTL-formula st H = EG H1 ); :: deftheorem Def19 defines ExistUntill MODELC_1:def_19_:_ for H being CTL-formula holds ( H is ExistUntill iff ex F, G being CTL-formula st H = F EU G ); definition let F, G be CTL-formula; funcF 'or' G -> CTL-formula equals :: MODELC_1:def 20 'not' (('not' F) '&' ('not' G)); coherence 'not' (('not' F) '&' ('not' G)) is CTL-formula ; end; :: deftheorem defines 'or' MODELC_1:def_20_:_ for F, G being CTL-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G)); theorem Th2: :: MODELC_1:2 for H being CTL-formula holds ( H is atomic or H is negative or H is conjunctive or H is ExistNext or H is ExistGlobal or H is ExistUntill ) proofend; Lm3: for H being CTL-formula st H is negative holds H . 1 = 0 proofend; Lm4: for H being CTL-formula st H is conjunctive holds H . 1 = 1 proofend; Lm5: for H being CTL-formula st H is ExistNext holds H . 1 = 2 proofend; Lm6: for H being CTL-formula st H is ExistGlobal holds H . 1 = 3 proofend; Lm7: for H being CTL-formula st H is ExistUntill holds H . 1 = 4 proofend; Lm8: for H being CTL-formula st H is atomic holds ( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 ) proofend; Lm9: for H being CTL-formula holds ( ( H is atomic & H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 ) or ( H is negative & H . 1 = 0 ) or ( H is conjunctive & H . 1 = 1 ) or ( H is ExistNext & H . 1 = 2 ) or ( H is ExistGlobal & H . 1 = 3 ) or ( H is ExistUntill & H . 1 = 4 ) ) proofend; Lm10: for H being CTL-formula holds 1 <= len H proofend; Lm11: for H, F being CTL-formula for sq being FinSequence st H = F ^ sq holds H = F proofend; Lm12: for H, G, H1, G1 being CTL-formula st H '&' G = H1 '&' G1 holds ( H = H1 & G = G1 ) proofend; Lm13: for H, G, H1, G1 being CTL-formula st H EU G = H1 EU G1 holds ( H = H1 & G = G1 ) proofend; Lm14: for H being CTL-formula st H is atomic holds ( not H is negative & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill ) proofend; Lm15: for H being CTL-formula st H is negative holds ( not H is atomic & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill ) proofend; Lm16: for H being CTL-formula st H is conjunctive holds ( not H is atomic & not H is negative & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill ) proofend; Lm17: for H being CTL-formula st H is ExistNext holds ( not H is atomic & not H is conjunctive & not H is negative & not H is ExistGlobal & not H is ExistUntill ) proofend; Lm18: for H being CTL-formula st H is ExistGlobal holds ( not H is atomic & not H is conjunctive & not H is negative & not H is ExistNext & not H is ExistUntill ) proofend; definition let H be CTL-formula; assume A1: ( H is negative or H is ExistNext or H is ExistGlobal ) ; func the_argument_of H -> CTL-formula means :Def21: :: MODELC_1:def 21 'not' it = H if H is negative EX it = H if H is ExistNext otherwise EG it = H; existence ( ( H is negative implies ex b1 being CTL-formula st 'not' b1 = H ) & ( H is ExistNext implies ex b1 being CTL-formula st EX b1 = H ) & ( not H is negative & not H is ExistNext implies ex b1 being CTL-formula st EG b1 = H ) ) by A1, Def15, Def17, Def18; uniqueness for b1, b2 being CTL-formula holds ( ( H is negative & 'not' b1 = H & 'not' b2 = H implies b1 = b2 ) & ( H is ExistNext & EX b1 = H & EX b2 = H implies b1 = b2 ) & ( not H is negative & not H is ExistNext & EG b1 = H & EG b2 = H implies b1 = b2 ) ) by FINSEQ_1:33; consistency for b1 being CTL-formula st H is negative & H is ExistNext holds ( 'not' b1 = H iff EX b1 = H ) by Lm15; end; :: deftheorem Def21 defines the_argument_of MODELC_1:def_21_:_ for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds for b2 being CTL-formula holds ( ( H is negative implies ( b2 = the_argument_of H iff 'not' b2 = H ) ) & ( H is ExistNext implies ( b2 = the_argument_of H iff EX b2 = H ) ) & ( not H is negative & not H is ExistNext implies ( b2 = the_argument_of H iff EG b2 = H ) ) ); definition let H be CTL-formula; assume A1: ( H is conjunctive or H is ExistUntill ) ; func the_left_argument_of H -> CTL-formula means :Def22: :: MODELC_1:def 22 ex H1 being CTL-formula st it '&' H1 = H if H is conjunctive otherwise ex H1 being CTL-formula st it EU H1 = H; existence ( ( H is conjunctive implies ex b1, H1 being CTL-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being CTL-formula st b1 EU H1 = H ) ) by A1, Def16, Def19; uniqueness for b1, b2 being CTL-formula holds ( ( H is conjunctive & ex H1 being CTL-formula st b1 '&' H1 = H & ex H1 being CTL-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being CTL-formula st b1 EU H1 = H & ex H1 being CTL-formula st b2 EU H1 = H implies b1 = b2 ) ) by Lm12, Lm13; consistency for b1 being CTL-formula holds verum ; func the_right_argument_of H -> CTL-formula means :Def23: :: MODELC_1:def 23 ex H1 being CTL-formula st H1 '&' it = H if H is conjunctive otherwise ex H1 being CTL-formula st H1 EU it = H; existence ( ( H is conjunctive implies ex b1, H1 being CTL-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being CTL-formula st H1 EU b1 = H ) ) proofend; uniqueness for b1, b2 being CTL-formula holds ( ( H is conjunctive & ex H1 being CTL-formula st H1 '&' b1 = H & ex H1 being CTL-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being CTL-formula st H1 EU b1 = H & ex H1 being CTL-formula st H1 EU b2 = H implies b1 = b2 ) ) by Lm12, Lm13; consistency for b1 being CTL-formula holds verum ; end; :: deftheorem Def22 defines the_left_argument_of MODELC_1:def_22_:_ for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds for b2 being CTL-formula holds ( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being CTL-formula st b2 '&' H1 = H ) ) & ( not H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being CTL-formula st b2 EU H1 = H ) ) ); :: deftheorem Def23 defines the_right_argument_of MODELC_1:def_23_:_ for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds for b2 being CTL-formula holds ( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being CTL-formula st H1 '&' b2 = H ) ) & ( not H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being CTL-formula st H1 EU b2 = H ) ) ); Lm19: for H being CTL-formula st H is ExistGlobal holds H = EG (the_argument_of H) proofend; Lm20: for H being CTL-formula st H is conjunctive holds H = (the_left_argument_of H) '&' (the_right_argument_of H) proofend; Lm21: for H being CTL-formula st H is ExistUntill holds H = (the_left_argument_of H) EU (the_right_argument_of H) proofend; Lm22: for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds len (the_argument_of H) < len H proofend; Lm23: for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds ( len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) proofend; definition let x be set ; func CastCTLformula x -> CTL-formula equals :Def24: :: MODELC_1:def 24 x if x in CTL_WFF otherwise atom. 0; correctness coherence ( ( x in CTL_WFF implies x is CTL-formula ) & ( not x in CTL_WFF implies atom. 0 is CTL-formula ) ); consistency for b1 being CTL-formula holds verum; by Th1; end; :: deftheorem Def24 defines CastCTLformula MODELC_1:def_24_:_ for x being set holds ( ( x in CTL_WFF implies CastCTLformula x = x ) & ( not x in CTL_WFF implies CastCTLformula x = atom. 0 ) ); ::*************************************************** ::** ::** definition of Kripke structure & CTL model structure. ::** ::**************************************************** definition let Prop be set ; attrc2 is strict ; struct KripkeStr over Prop -> RelStr ; aggrKripkeStr(# carrier, Starts, InternalRel, Label #) -> KripkeStr over Prop; sel Starts c2 -> Subset of the carrier of c2; sel Label c2 -> Function of the carrier of c2,(bool Prop); end; definition attrc1 is strict ; struct CTLModelStr -> ComplULattStr ; aggrCTLModelStr(# carrier, BasicAssign, L_meet, Compl, EneXt, EGlobal, EUntill #) -> CTLModelStr ; sel BasicAssign c1 -> Subset of the carrier of c1; sel EneXt c1 -> UnOp of the carrier of c1; sel EGlobal c1 -> UnOp of the carrier of c1; sel EUntill c1 -> BinOp of the carrier of c1; end; definition let V be CTLModelStr ; mode Assign of V is Element of the carrier of V; end; :: Preparation to define semantics for CTL-language :: definition of evaluate function of CTL definition func atomic_WFF -> Subset of CTL_WFF equals :: MODELC_1:def 25 { x where x is CTL-formula : x is atomic } ; correctness coherence { x where x is CTL-formula : x is atomic } is Subset of CTL_WFF; proofend; end; :: deftheorem defines atomic_WFF MODELC_1:def_25_:_ atomic_WFF = { x where x is CTL-formula : x is atomic } ; definition let V be CTLModelStr ; let Kai be Function of atomic_WFF, the BasicAssign of V; let f be Function of CTL_WFF, the carrier of V; predf is-Evaluation-for Kai means :Def26: :: MODELC_1:def 26 for H being CTL-formula holds ( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ); end; :: deftheorem Def26 defines is-Evaluation-for MODELC_1:def_26_:_ for V being CTLModelStr for Kai being Function of atomic_WFF, the BasicAssign of V for f being Function of CTL_WFF, the carrier of V holds ( f is-Evaluation-for Kai iff for H being CTL-formula holds ( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) ); definition let V be CTLModelStr ; let Kai be Function of atomic_WFF, the BasicAssign of V; let f be Function of CTL_WFF, the carrier of V; let n be Element of NAT ; predf is-PreEvaluation-for n,Kai means :Def27: :: MODELC_1:def 27 for H being CTL-formula st len H <= n holds ( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ); end; :: deftheorem Def27 defines is-PreEvaluation-for MODELC_1:def_27_:_ for V being CTLModelStr for Kai being Function of atomic_WFF, the BasicAssign of V for f being Function of CTL_WFF, the carrier of V for n being Element of NAT holds ( f is-PreEvaluation-for n,Kai iff for H being CTL-formula st len H <= n holds ( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) ) ); definition let V be CTLModelStr ; let Kai be Function of atomic_WFF, the BasicAssign of V; let f, h be Function of CTL_WFF, the carrier of V; let n be Element of NAT ; let H be CTL-formula; func GraftEval (V,Kai,f,h,n,H) -> set equals :Def28: :: MODELC_1:def 28 f . H if len H > n + 1 Kai . H if ( len H = n + 1 & H is atomic ) the Compl of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is negative ) the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is conjunctive ) the EneXt of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is ExistNext ) the EGlobal of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is ExistGlobal ) the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is ExistUntill ) h . H if len H < n + 1 otherwise {} ; coherence ( ( len H > n + 1 implies f . H is set ) & ( len H = n + 1 & H is atomic implies Kai . H is set ) & ( len H = n + 1 & H is negative implies the Compl of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is conjunctive implies the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H = n + 1 & H is ExistNext implies the EneXt of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is ExistGlobal implies the EGlobal of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is ExistUntill implies the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) is set ) & ( len H < n + 1 implies h . H is set ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is ExistNext ) & ( not len H = n + 1 or not H is ExistGlobal ) & ( not len H = n + 1 or not H is ExistUntill ) & not len H < n + 1 implies {} is set ) ) ; consistency for 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 ExistNext implies ( b1 = f . H iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistGlobal implies ( b1 = f . H iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is ExistUntill implies ( b1 = f . H iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H > n + 1 & len H < n + 1 implies ( 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 ExistNext implies ( b1 = Kai . H iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistGlobal implies ( b1 = Kai . H iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is ExistUntill implies ( b1 = Kai . H iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is atomic & len H < n + 1 implies ( 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 ExistNext implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistGlobal implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is ExistUntill implies ( b1 = the Compl of V . (h . (the_argument_of H)) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is negative & len H < n + 1 implies ( 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 ExistNext implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the EneXt of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistGlobal implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is ExistUntill implies ( b1 = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is conjunctive & len H < n + 1 implies ( 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 ExistNext & len H = n + 1 & H is ExistGlobal implies ( b1 = the EneXt of V . (h . (the_argument_of H)) iff b1 = the EGlobal of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is ExistNext & len H = n + 1 & H is ExistUntill implies ( b1 = the EneXt of V . (h . (the_argument_of H)) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is ExistNext & len H < n + 1 implies ( b1 = the EneXt of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is ExistGlobal & len H = n + 1 & H is ExistUntill implies ( b1 = the EGlobal of V . (h . (the_argument_of H)) iff b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) ) & ( len H = n + 1 & H is ExistGlobal & len H < n + 1 implies ( b1 = the EGlobal of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is ExistUntill & len H < n + 1 implies ( b1 = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = h . H ) ) ) by Lm14, Lm15, Lm16, Lm17, Lm18; end; :: deftheorem Def28 defines GraftEval MODELC_1:def_28_:_ for V being CTLModelStr for Kai being Function of atomic_WFF, the BasicAssign of V for f, h being Function of CTL_WFF, the carrier of V for n being Element of NAT for H being CTL-formula holds ( ( len H > n + 1 implies GraftEval (V,Kai,f,h,n,H) = f . H ) & ( len H = n + 1 & H is atomic implies GraftEval (V,Kai,f,h,n,H) = Kai . H ) & ( len H = n + 1 & H is negative implies GraftEval (V,Kai,f,h,n,H) = the Compl of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is ExistNext implies GraftEval (V,Kai,f,h,n,H) = the EneXt of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistGlobal implies GraftEval (V,Kai,f,h,n,H) = the EGlobal of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistUntill implies GraftEval (V,Kai,f,h,n,H) = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = h . H ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is ExistNext ) & ( not len H = n + 1 or not H is ExistGlobal ) & ( not len H = n + 1 or not H is ExistUntill ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) ); definition let C be CTLModelStr ; attrC is with_basic means :Def29: :: MODELC_1:def 29 not the BasicAssign of C is empty ; end; :: deftheorem Def29 defines with_basic MODELC_1:def_29_:_ for C being CTLModelStr holds ( C is with_basic iff not the BasicAssign of C is empty ); definition func TrivialCTLModel -> CTLModelStr equals :: MODELC_1:def 30 CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #); coherence CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #) is CTLModelStr ; end; :: deftheorem defines TrivialCTLModel MODELC_1:def_30_:_ TrivialCTLModel = CTLModelStr(# 1,([#] 1),op2,op1,op1,op1,op2 #); registration cluster TrivialCTLModel -> non empty strict with_basic ; coherence ( TrivialCTLModel is with_basic & TrivialCTLModel is strict & not TrivialCTLModel is empty ) proofend; end; registration cluster non empty for CTLModelStr ; existence not for b1 being CTLModelStr holds b1 is empty proofend; end; registration cluster non empty with_basic for CTLModelStr ; existence ex b1 being non empty CTLModelStr st b1 is with_basic proofend; end; definition mode CTLModel is non empty with_basic CTLModelStr ; end; registration let C be CTLModel; cluster the BasicAssign of C -> non empty ; coherence not the BasicAssign of C is empty by Def29; end; Lm24: for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for f being Function of CTL_WFF, the carrier of V holds f is-PreEvaluation-for 0 ,Kai proofend; Lm25: for n being Element of NAT for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds f is-PreEvaluation-for n,Kai proofend; Lm26: for n being Element of NAT for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for f being Function of CTL_WFF, the carrier of V st f is-Evaluation-for Kai holds f is-PreEvaluation-for n,Kai proofend; Lm27: for n being Element of NAT for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for f1, f2 being Function of CTL_WFF, the carrier of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds for H being CTL-formula st len H <= n holds f1 . H = f2 . H proofend; Lm28: for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for n being Element of NAT ex f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai proofend; Lm29: for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for f being Function of CTL_WFF, the carrier of V st ( for n being Element of NAT holds f is-PreEvaluation-for n,Kai ) holds f is-Evaluation-for Kai proofend; definition let V be CTLModel; let Kai be Function of atomic_WFF, the BasicAssign of V; let n be Element of NAT ; func EvalSet (V,Kai,n) -> non empty set equals :: MODELC_1:def 31 { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ; correctness coherence { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } is non empty set ; proofend; end; :: deftheorem defines EvalSet MODELC_1:def_31_:_ for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for n being Element of NAT holds EvalSet (V,Kai,n) = { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ; definition let V be CTLModel; let v0 be Element of the carrier of V; let x be set ; func CastEval (V,x,v0) -> Function of CTL_WFF, the carrier of V equals :Def32: :: MODELC_1:def 32 x if x in Funcs (CTL_WFF, the carrier of V) otherwise CTL_WFF --> v0; correctness coherence ( ( x in Funcs (CTL_WFF, the carrier of V) implies x is Function of CTL_WFF, the carrier of V ) & ( not x in Funcs (CTL_WFF, the carrier of V) implies CTL_WFF --> v0 is Function of CTL_WFF, the carrier of V ) ); consistency for b1 being Function of CTL_WFF, the carrier of V holds verum; by FUNCT_2:66; end; :: deftheorem Def32 defines CastEval MODELC_1:def_32_:_ for V being CTLModel for v0 being Element of the carrier of V for x being set holds ( ( x in Funcs (CTL_WFF, the carrier of V) implies CastEval (V,x,v0) = x ) & ( not x in Funcs (CTL_WFF, the carrier of V) implies CastEval (V,x,v0) = CTL_WFF --> v0 ) ); definition let V be CTLModel; let Kai be Function of atomic_WFF, the BasicAssign of V; func EvalFamily (V,Kai) -> non empty set means :Def33: :: MODELC_1:def 33 for p being set holds ( p in it iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ); existence ex b1 being non empty set st for p being set holds ( p in b1 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of 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 (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) ) & ( for p being set holds ( p in b2 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def33 defines EvalFamily MODELC_1:def_33_:_ for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for b3 being non empty set holds ( b3 = EvalFamily (V,Kai) iff for p being set holds ( p in b3 iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) ); Lm30: for n being Element of NAT for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai) proofend; theorem Th3: :: MODELC_1:3 for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V ex f being Function of CTL_WFF, the carrier of V st f is-Evaluation-for Kai proofend; theorem Th4: :: MODELC_1:4 for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for f1, f2 being Function of CTL_WFF, the carrier of V st f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai holds f1 = f2 proofend; definition let V be CTLModel; let Kai be Function of atomic_WFF, the BasicAssign of V; let H be CTL-formula; func Evaluate (H,Kai) -> Assign of V means :Def34: :: MODELC_1:def 34 ex f being Function of CTL_WFF, the carrier of V st ( f is-Evaluation-for Kai & it = f . H ); existence ex b1 being Assign of V ex f being Function of CTL_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 CTL_WFF, the carrier of V st ( f is-Evaluation-for Kai & b1 = f . H ) & ex f being Function of CTL_WFF, the carrier of V st ( f is-Evaluation-for Kai & b2 = f . H ) holds b1 = b2 by Th4; end; :: deftheorem Def34 defines Evaluate MODELC_1:def_34_:_ for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V for H being CTL-formula for b4 being Assign of V holds ( b4 = Evaluate (H,Kai) iff ex f being Function of CTL_WFF, the carrier of V st ( f is-Evaluation-for Kai & b4 = f . H ) ); notation let V be CTLModel; let f be Assign of V; synonym 'not' f for f ` ; let g be Assign of V; synonym f '&' g for f "/\" g; end; definition let V be CTLModel; let f be Assign of V; func EX f -> Assign of V equals :: MODELC_1:def 35 the EneXt of V . f; correctness coherence the EneXt of V . f is Assign of V; ; func EG f -> Assign of V equals :: MODELC_1:def 36 the EGlobal of V . f; correctness coherence the EGlobal of V . f is Assign of V; ; end; :: deftheorem defines EX MODELC_1:def_35_:_ for V being CTLModel for f being Assign of V holds EX f = the EneXt of V . f; :: deftheorem defines EG MODELC_1:def_36_:_ for V being CTLModel for f being Assign of V holds EG f = the EGlobal of V . f; definition let V be CTLModel; let f, g be Assign of V; funcf EU g -> Assign of V equals :: MODELC_1:def 37 the EUntill of V . (f,g); correctness coherence the EUntill of V . (f,g) is Assign of V; ; funcf 'or' g -> Assign of V equals :: MODELC_1:def 38 'not' (('not' f) '&' ('not' g)); correctness coherence 'not' (('not' f) '&' ('not' g)) is Assign of V; ; end; :: deftheorem defines EU MODELC_1:def_37_:_ for V being CTLModel for f, g being Assign of V holds f EU g = the EUntill of V . (f,g); :: deftheorem defines 'or' MODELC_1:def_38_:_ for V being CTLModel for f, g being Assign of V holds f 'or' g = 'not' (('not' f) '&' ('not' g)); ::Some properties of evaluate function of CTL theorem Th5: :: MODELC_1:5 for H being CTL-formula for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai)) proofend; theorem Th6: :: MODELC_1:6 for H1, H2 being CTL-formula for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 '&' H2),Kai) = (Evaluate (H1,Kai)) '&' (Evaluate (H2,Kai)) proofend; theorem Th7: :: MODELC_1:7 for H being CTL-formula for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EX H),Kai) = EX (Evaluate (H,Kai)) proofend; theorem Th8: :: MODELC_1:8 for H being CTL-formula for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai)) proofend; theorem Th9: :: MODELC_1:9 for H1, H2 being CTL-formula for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai)) proofend; theorem Th10: :: MODELC_1:10 for H1, H2 being CTL-formula for V being CTLModel for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai)) proofend; notation let f be Function; let n be Nat; synonym f |** n for iter (f,n); end; definition let S be set ; let f be Function of S,S; let n be Nat; :: original:|** redefine funcf |** n -> Function of S,S; coherence f |** n is Function of S,S proofend; end; Lm31: for S being set for R being Relation of S,S st R is total holds for x being set st x in S holds ex y being set st ( y in S & [x,y] in R ) proofend; Lm32: for S being set for R being Relation of S,S st ( for x being set st x in S holds ex y being set st ( y in S & [x,y] in R ) ) holds R is total proofend; Lm33: for S being non empty set for R being total Relation of S,S for s being Element of S holds not R .: {s} is empty proofend; scheme :: MODELC_1:sch 1 ExistPath{ F1() -> non empty set , F2() -> total Relation of F1(),F1(), F3() -> Element of F1(), F4( Element of F1()) -> set } : ex f being Function of NAT,F1() st ( f . 0 = F3() & ( for n being Element of NAT holds ( [(f . n),(f . (n + 1))] in F2() & f . (n + 1) in F4((f . n)) ) ) ) provided A1: for s being Element of F1() holds (Im (F2(),s)) /\ F4(s) is non empty Subset of F1() proofend; Lm34: for S being non empty set for R being total Relation of S,S for s0 being Element of S ex f being Function of NAT,S st ( f . 0 = s0 & ( for n being Element of NAT holds [(f . n),(f . (n + 1))] in R ) ) proofend; :: definition of infinity path definition let S be non empty set ; let R be total Relation of S,S; mode inf_path of R -> Function of NAT,S means :Def39: :: MODELC_1:def 39 for n being Element of NAT holds [(it . n),(it . (n + 1))] in R; existence ex b1 being Function of NAT,S st for n being Element of NAT holds [(b1 . n),(b1 . (n + 1))] in R proofend; end; :: deftheorem Def39 defines inf_path MODELC_1:def_39_:_ for S being non empty set for R being total Relation of S,S for b3 being Function of NAT,S holds ( b3 is inf_path of R iff for n being Element of NAT holds [(b3 . n),(b3 . (n + 1))] in R ); ::definition of concrete object of CTL model definition let S be non empty set ; func ModelSP S -> set equals :: MODELC_1:def 40 Funcs (S,BOOLEAN); correctness coherence Funcs (S,BOOLEAN) is set ; ; end; :: deftheorem defines ModelSP MODELC_1:def_40_:_ for S being non empty set holds ModelSP S = Funcs (S,BOOLEAN); registration let S be non empty set ; cluster ModelSP S -> non empty ; coherence not ModelSP S is empty ; end; :: definition Fid:ModelSP(S) -> Function of S,BOOLEAN definition let S be non empty set ; let f be set ; func Fid (f,S) -> Function of S,BOOLEAN equals :Def41: :: MODELC_1:def 41 f if f in ModelSP S otherwise S --> FALSE; correctness coherence ( ( f in ModelSP S implies f is Function of S,BOOLEAN ) & ( not f in ModelSP S implies S --> FALSE is Function of S,BOOLEAN ) ); consistency for b1 being Function of S,BOOLEAN holds verum; by FUNCT_2:66; end; :: deftheorem Def41 defines Fid MODELC_1:def_41_:_ for S being non empty set for f being set holds ( ( f in ModelSP S implies Fid (f,S) = f ) & ( not f in ModelSP S implies Fid (f,S) = S --> FALSE ) ); Lm35: for S being non empty set for s being Element of S for f being set st (Fid (f,S)) . s <> TRUE holds (Fid (f,S)) . s = FALSE by TARSKI:def_2; scheme :: MODELC_1:sch 2 Func1EX{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3( set , Function of F1(),BOOLEAN) -> boolean set } : ex g being set st ( g in ModelSP F1() & ( for s being set st s in F1() holds ( F3(s,F2()) = TRUE iff (Fid (g,F1())) . s = TRUE ) ) ) proofend; scheme :: MODELC_1:sch 3 Func1Unique{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3( set , Function of F1(),BOOLEAN) -> boolean set } : for g1, g2 being set st g1 in ModelSP F1() & ( for s being set st s in F1() holds ( F3(s,F2()) = TRUE iff (Fid (g1,F1())) . s = TRUE ) ) & g2 in ModelSP F1() & ( for s being set st s in F1() holds ( F3(s,F2()) = TRUE iff (Fid (g2,F1())) . s = TRUE ) ) holds g1 = g2 proofend; scheme :: MODELC_1:sch 4 UnOpEX{ F1() -> non empty set , F2( set ) -> Element of F1() } : ex o being UnOp of F1() st for f being set st f in F1() holds o . f = F2(f) proofend; scheme :: MODELC_1:sch 5 UnOpUnique{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2() } : for o1, o2 being UnOp of F2() st ( for f being set st f in F2() holds o1 . f = F3(f) ) & ( for f being set st f in F2() holds o2 . f = F3(f) ) holds o1 = o2 proofend; scheme :: MODELC_1:sch 6 Func2EX{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3() -> Function of F1(),BOOLEAN, F4( set , Function of F1(),BOOLEAN, Function of F1(),BOOLEAN) -> boolean set } : ex h being set st ( h in ModelSP F1() & ( for s being set st s in F1() holds ( F4(s,F2(),F3()) = TRUE iff (Fid (h,F1())) . s = TRUE ) ) ) proofend; scheme :: MODELC_1:sch 7 Func2Unique{ F1() -> non empty set , F2() -> Function of F1(),BOOLEAN, F3() -> Function of F1(),BOOLEAN, F4( set , Function of F1(),BOOLEAN, Function of F1(),BOOLEAN) -> boolean set } : for h1, h2 being set st h1 in ModelSP F1() & ( for s being set st s in F1() holds ( F4(s,F2(),F3()) = TRUE iff (Fid (h1,F1())) . s = TRUE ) ) & h2 in ModelSP F1() & ( for s being set st s in F1() holds ( F4(s,F2(),F3()) = TRUE iff (Fid (h2,F1())) . s = TRUE ) ) holds h1 = h2 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 S means :Def42: :: MODELC_1:def 42 for s being set st s in S holds ( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (it,S)) . s = TRUE ); existence ex b1 being Element of ModelSP S st for s being set st s in S holds ( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds ( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds ( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def42 defines Not_0 MODELC_1:def_42_:_ for S being non empty set for f being set for b3 being Element of ModelSP S holds ( b3 = Not_0 (f,S) iff for s being set st s in S holds ( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b3,S)) . s = TRUE ) ); Lm36: for S being non empty set for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds o1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP S holds o2 . f = Not_0 (f,S) ) holds o1 = o2 proofend; definition let S be non empty set ; func Not_ S -> UnOp of (ModelSP S) means :Def43: :: MODELC_1:def 43 for f being set st f in ModelSP S holds it . f = Not_0 (f,S); existence ex b1 being UnOp of (ModelSP S) st for f being set st f in ModelSP S holds b1 . f = Not_0 (f,S) proofend; uniqueness for b1, b2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds b1 . f = Not_0 (f,S) ) & ( for f being set st f in ModelSP S holds b2 . f = Not_0 (f,S) ) holds b1 = b2 by Lm36; end; :: deftheorem Def43 defines Not_ MODELC_1:def_43_:_ for S being non empty set for b2 being UnOp of (ModelSP S) holds ( b2 = Not_ S iff for f being set st f in ModelSP S holds b2 . f = Not_0 (f,S) ); :: definition of EneXt_ unary operation of Model Space. definition let S be non empty set ; let R be total Relation of S,S; let f be Function of S,BOOLEAN; let x be set ; func EneXt_univ (x,f,R) -> Element of BOOLEAN equals :Def44: :: MODELC_1:def 44 TRUE if ( x in S & ex pai being inf_path of R st ( pai . 0 = x & f . (pai . 1) = TRUE ) ) otherwise FALSE ; correctness coherence ( ( x in S & ex pai being inf_path of R st ( pai . 0 = x & f . (pai . 1) = TRUE ) implies TRUE is Element of BOOLEAN ) & ( ( not x in S or for pai being inf_path of R holds ( not pai . 0 = x or not f . (pai . 1) = TRUE ) ) implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def44 defines EneXt_univ MODELC_1:def_44_:_ for S being non empty set for R being total Relation of S,S for f being Function of S,BOOLEAN for x being set holds ( ( x in S & ex pai being inf_path of R st ( pai . 0 = x & f . (pai . 1) = TRUE ) implies EneXt_univ (x,f,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds ( not pai . 0 = x or not f . (pai . 1) = TRUE ) ) implies EneXt_univ (x,f,R) = FALSE ) ); definition let S be non empty set ; let R be total Relation of S,S; let f be set ; func EneXt_0 (f,R) -> Element of ModelSP S means :Def45: :: MODELC_1:def 45 for s being set st s in S holds ( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE ); existence ex b1 being Element of ModelSP S st for s being set st s in S holds ( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds ( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds ( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def45 defines EneXt_0 MODELC_1:def_45_:_ for S being non empty set for R being total Relation of S,S for f being set for b4 being Element of ModelSP S holds ( b4 = EneXt_0 (f,R) iff for s being set st s in S holds ( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b4,S)) . s = TRUE ) ); Lm37: for S being non empty set for R being total Relation of S,S for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds o1 . f = EneXt_0 (f,R) ) & ( for f being set st f in ModelSP S holds o2 . f = EneXt_0 (f,R) ) holds o1 = o2 proofend; definition let S be non empty set ; let R be total Relation of S,S; func EneXt_ R -> UnOp of (ModelSP S) means :Def46: :: MODELC_1:def 46 for f being set st f in ModelSP S holds it . f = EneXt_0 (f,R); existence ex b1 being UnOp of (ModelSP S) st for f being set st f in ModelSP S holds b1 . f = EneXt_0 (f,R) proofend; uniqueness for b1, b2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds b1 . f = EneXt_0 (f,R) ) & ( for f being set st f in ModelSP S holds b2 . f = EneXt_0 (f,R) ) holds b1 = b2 by Lm37; end; :: deftheorem Def46 defines EneXt_ MODELC_1:def_46_:_ for S being non empty set for R being total Relation of S,S for b3 being UnOp of (ModelSP S) holds ( b3 = EneXt_ R iff for f being set st f in ModelSP S holds b3 . f = EneXt_0 (f,R) ); :: definition of EGlobal_ unary operation of Model Space. definition let S be non empty set ; let R be total Relation of S,S; let f be Function of S,BOOLEAN; let x be set ; func EGlobal_univ (x,f,R) -> Element of BOOLEAN equals :Def47: :: MODELC_1:def 47 TRUE if ( x in S & ex pai being inf_path of R st ( pai . 0 = x & ( for n being Element of NAT holds f . (pai . n) = TRUE ) ) ) otherwise FALSE ; correctness coherence ( ( x in S & ex pai being inf_path of R st ( pai . 0 = x & ( for n being Element of NAT holds f . (pai . n) = TRUE ) ) implies TRUE is Element of BOOLEAN ) & ( ( not x in S or for pai being inf_path of R holds ( not pai . 0 = x or ex n being Element of NAT st not f . (pai . n) = TRUE ) ) implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def47 defines EGlobal_univ MODELC_1:def_47_:_ for S being non empty set for R being total Relation of S,S for f being Function of S,BOOLEAN for x being set holds ( ( x in S & ex pai being inf_path of R st ( pai . 0 = x & ( for n being Element of NAT holds f . (pai . n) = TRUE ) ) implies EGlobal_univ (x,f,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds ( not pai . 0 = x or ex n being Element of NAT st not f . (pai . n) = TRUE ) ) implies EGlobal_univ (x,f,R) = FALSE ) ); definition let S be non empty set ; let R be total Relation of S,S; let f be set ; func EGlobal_0 (f,R) -> Element of ModelSP S means :Def48: :: MODELC_1:def 48 for s being set st s in S holds ( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE ); existence ex b1 being Element of ModelSP S st for s being set st s in S holds ( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds ( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds ( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def48 defines EGlobal_0 MODELC_1:def_48_:_ for S being non empty set for R being total Relation of S,S for f being set for b4 being Element of ModelSP S holds ( b4 = EGlobal_0 (f,R) iff for s being set st s in S holds ( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b4,S)) . s = TRUE ) ); Lm38: for S being non empty set for R being total Relation of S,S for o1, o2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds o1 . f = EGlobal_0 (f,R) ) & ( for f being set st f in ModelSP S holds o2 . f = EGlobal_0 (f,R) ) holds o1 = o2 proofend; definition let S be non empty set ; let R be total Relation of S,S; func EGlobal_ R -> UnOp of (ModelSP S) means :Def49: :: MODELC_1:def 49 for f being set st f in ModelSP S holds it . f = EGlobal_0 (f,R); existence ex b1 being UnOp of (ModelSP S) st for f being set st f in ModelSP S holds b1 . f = EGlobal_0 (f,R) proofend; uniqueness for b1, b2 being UnOp of (ModelSP S) st ( for f being set st f in ModelSP S holds b1 . f = EGlobal_0 (f,R) ) & ( for f being set st f in ModelSP S holds b2 . f = EGlobal_0 (f,R) ) holds b1 = b2 by Lm38; end; :: deftheorem Def49 defines EGlobal_ MODELC_1:def_49_:_ for S being non empty set for R being total Relation of S,S for b3 being UnOp of (ModelSP S) holds ( b3 = EGlobal_ R iff for f being set st f in ModelSP S holds b3 . f = EGlobal_0 (f,R) ); :: 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 S means :Def50: :: MODELC_1:def 50 for s being set st s in S holds ( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (it,S)) . s = TRUE ); existence ex b1 being Element of ModelSP S st for s being set st s in S holds ( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds ( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds ( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def50 defines And_0 MODELC_1:def_50_:_ for S being non empty set for f, g being set for b4 being Element of ModelSP S holds ( b4 = And_0 (f,g,S) iff for s being set st s in S holds ( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b4,S)) . s = TRUE ) ); Lm39: for S being non empty set for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds o1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds o2 . (f,g) = And_0 (f,g,S) ) holds o1 = o2 proofend; definition let S be non empty set ; func And_ S -> BinOp of (ModelSP S) means :Def51: :: MODELC_1:def 51 for f, g being set st f in ModelSP S & g in ModelSP S holds it . (f,g) = And_0 (f,g,S); existence ex b1 being BinOp of (ModelSP S) st for f, g being set st f in ModelSP S & g in ModelSP S holds b1 . (f,g) = And_0 (f,g,S) proofend; uniqueness for b1, b2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds b1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds b2 . (f,g) = And_0 (f,g,S) ) holds b1 = b2 by Lm39; end; :: deftheorem Def51 defines And_ MODELC_1:def_51_:_ for S being non empty set for b2 being BinOp of (ModelSP S) holds ( b2 = And_ S iff for f, g being set st f in ModelSP S & g in ModelSP S holds b2 . (f,g) = And_0 (f,g,S) ); :: definition of EUntill_ Binary Operation of Model Space. definition let S be non empty set ; let R be total Relation of S,S; let f, g be Function of S,BOOLEAN; let x be set ; func EUntill_univ (x,f,g,R) -> Element of BOOLEAN equals :Def52: :: MODELC_1:def 52 TRUE if ( x in S & ex pai being inf_path of R st ( pai . 0 = x & ex m being Element of NAT st ( ( for j being Element of NAT st j < m holds f . (pai . j) = TRUE ) & g . (pai . m) = TRUE ) ) ) otherwise FALSE ; correctness coherence ( ( x in S & ex pai being inf_path of R st ( pai . 0 = x & ex m being Element of NAT st ( ( for j being Element of NAT st j < m holds f . (pai . j) = TRUE ) & g . (pai . m) = TRUE ) ) implies TRUE is Element of BOOLEAN ) & ( ( not x in S or for pai being inf_path of R holds ( not pai . 0 = x or for m being Element of NAT holds ( ex j being Element of NAT st ( j < m & not f . (pai . j) = TRUE ) or not g . (pai . m) = TRUE ) ) ) implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def52 defines EUntill_univ MODELC_1:def_52_:_ for S being non empty set for R being total Relation of S,S for f, g being Function of S,BOOLEAN for x being set holds ( ( x in S & ex pai being inf_path of R st ( pai . 0 = x & ex m being Element of NAT st ( ( for j being Element of NAT st j < m holds f . (pai . j) = TRUE ) & g . (pai . m) = TRUE ) ) implies EUntill_univ (x,f,g,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds ( not pai . 0 = x or for m being Element of NAT holds ( ex j being Element of NAT st ( j < m & not f . (pai . j) = TRUE ) or not g . (pai . m) = TRUE ) ) ) implies EUntill_univ (x,f,g,R) = FALSE ) ); definition let S be non empty set ; let R be total Relation of S,S; let f, g be set ; func EUntill_0 (f,g,R) -> Element of ModelSP S means :Def53: :: MODELC_1:def 53 for s being set st s in S holds ( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE ); existence ex b1 being Element of ModelSP S st for s being set st s in S holds ( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) proofend; uniqueness for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds ( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds ( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds b1 = b2 proofend; end; :: deftheorem Def53 defines EUntill_0 MODELC_1:def_53_:_ for S being non empty set for R being total Relation of S,S for f, g being set for b5 being Element of ModelSP S holds ( b5 = EUntill_0 (f,g,R) iff for s being set st s in S holds ( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b5,S)) . s = TRUE ) ); Lm40: for S being non empty set for R being total Relation of S,S for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds o2 . (f,g) = EUntill_0 (f,g,R) ) holds o1 = o2 proofend; definition let S be non empty set ; let R be total Relation of S,S; func EUntill_ R -> BinOp of (ModelSP S) means :Def54: :: MODELC_1:def 54 for f, g being set st f in ModelSP S & g in ModelSP S holds it . (f,g) = EUntill_0 (f,g,R); existence ex b1 being BinOp of (ModelSP S) st for f, g being set st f in ModelSP S & g in ModelSP S holds b1 . (f,g) = EUntill_0 (f,g,R) proofend; uniqueness for b1, b2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds b1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds b2 . (f,g) = EUntill_0 (f,g,R) ) holds b1 = b2 by Lm40; end; :: deftheorem Def54 defines EUntill_ MODELC_1:def_54_:_ for S being non empty set for R being total Relation of S,S for b3 being BinOp of (ModelSP S) holds ( b3 = EUntill_ R iff for f, g being set st f in ModelSP S & g in ModelSP S holds b3 . (f,g) = EUntill_0 (f,g,R) ); :: definition of concrete object of CTL model by ModelSP definition let S be non empty set ; let X be non empty Subset of (ModelSP S); let s be set ; func F_LABEL (s,X) -> Subset of X means :Def55: :: MODELC_1:def 55 for x being set holds ( x in it iff ( x in X & ex f being Function of S,BOOLEAN st ( f = x & f . s = TRUE ) ) ); existence ex b1 being Subset of X st for x being set holds ( x in b1 iff ( x in X & ex f being Function of S,BOOLEAN st ( f = x & f . s = TRUE ) ) ) proofend; uniqueness for b1, b2 being Subset of X st ( for x being set holds ( x in b1 iff ( x in X & ex f being Function of S,BOOLEAN st ( f = x & f . s = TRUE ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in X & ex f being Function of S,BOOLEAN st ( f = x & f . s = TRUE ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def55 defines F_LABEL MODELC_1:def_55_:_ for S being non empty set for X being non empty Subset of (ModelSP S) for s being set for b4 being Subset of X holds ( b4 = F_LABEL (s,X) iff for x being set holds ( x in b4 iff ( x in X & ex f being Function of S,BOOLEAN st ( f = x & f . s = TRUE ) ) ) ); definition let S be non empty set ; let X be non empty Subset of (ModelSP S); func Label_ X -> Function of S,(bool X) means :Def56: :: MODELC_1:def 56 for x being set st x in S holds it . x = F_LABEL (x,X); existence ex b1 being Function of S,(bool X) st for x being set st x in S holds b1 . x = F_LABEL (x,X) proofend; uniqueness for b1, b2 being Function of S,(bool X) st ( for x being set st x in S holds b1 . x = F_LABEL (x,X) ) & ( for x being set st x in S holds b2 . x = F_LABEL (x,X) ) holds b1 = b2 proofend; end; :: deftheorem Def56 defines Label_ MODELC_1:def_56_:_ for S being non empty set for X being non empty Subset of (ModelSP S) for b3 being Function of S,(bool X) holds ( b3 = Label_ X iff for x being set st x in S holds b3 . x = F_LABEL (x,X) ); definition let S be non empty set ; let S0 be Subset of S; let R be total Relation of S,S; let Prop be non empty Subset of (ModelSP S); func KModel (R,S0,Prop) -> KripkeStr over Prop equals :: MODELC_1:def 57 KripkeStr(# S,S0,R,(Label_ Prop) #); coherence KripkeStr(# S,S0,R,(Label_ Prop) #) is KripkeStr over Prop ; end; :: deftheorem defines KModel MODELC_1:def_57_:_ for S being non empty set for S0 being Subset of S for R being total Relation of S,S for Prop being non empty Subset of (ModelSP S) holds KModel (R,S0,Prop) = KripkeStr(# S,S0,R,(Label_ Prop) #); registration let S be non empty set ; let S0 be Subset of S; let R be total Relation of S,S; let Prop be non empty Subset of (ModelSP S); cluster the carrier of (KModel (R,S0,Prop)) -> non empty ; coherence not the carrier of (KModel (R,S0,Prop)) is empty ; end; registration let S be non empty set ; let S0 be Subset of S; let R be total Relation of S,S; let Prop be non empty Subset of (ModelSP S); cluster ModelSP the carrier of (KModel (R,S0,Prop)) -> non empty for Subset of (Funcs ( the carrier of (KModel (R,S0,Prop)),BOOLEAN)); coherence for b1 being Subset of (Funcs ( the carrier of (KModel (R,S0,Prop)),BOOLEAN)) st b1 = ModelSP the carrier of (KModel (R,S0,Prop)) holds not b1 is empty ; end; definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); func BASSModel (R,BASSIGN) -> CTLModelStr equals :: MODELC_1:def 58 CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #); coherence CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #) is CTLModelStr ; end; :: deftheorem defines BASSModel MODELC_1:def_58_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) holds BASSModel (R,BASSIGN) = CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #); registration let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); cluster BASSModel (R,BASSIGN) -> non empty with_basic ; coherence ( BASSModel (R,BASSIGN) is with_basic & not BASSModel (R,BASSIGN) is empty ) proofend; end; :: definition of correctness of Assign of BASSModel(R,BASSIGN) definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let s be Element of S; let f be Assign of (BASSModel (R,BASSIGN)); preds |= f means :Def59: :: MODELC_1:def 59 (Fid (f,S)) . s = TRUE ; end; :: deftheorem Def59 defines |= MODELC_1:def_59_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for s being Element of S for f being Assign of (BASSModel (R,BASSIGN)) holds ( s |= f iff (Fid (f,S)) . s = TRUE ); notation let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let s be Element of S; let f be Assign of (BASSModel (R,BASSIGN)); antonym s |/= f for s |= f; end; theorem Th11: :: MODELC_1:11 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds ( s |= a iff a in (Label_ BASSIGN) . s ) proofend; theorem Th12: :: MODELC_1:12 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds ( s |= 'not' f iff s |/= f ) proofend; theorem Th13: :: MODELC_1:13 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds ( s |= f '&' g iff ( s |= f & s |= g ) ) proofend; theorem Th14: :: MODELC_1:14 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds ( s |= EX f iff ex pai being inf_path of R st ( pai . 0 = s & pai . 1 |= f ) ) proofend; theorem Th15: :: MODELC_1:15 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds ( s |= EG f iff ex pai being inf_path of R st ( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) ) proofend; theorem Th16: :: MODELC_1:16 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds ( s |= f EU g iff ex pai being inf_path of R st ( pai . 0 = s & ex m being Element of NAT st ( ( for j being Element of NAT st j < m holds pai . j |= f ) & pai . m |= g ) ) ) proofend; theorem Th17: :: MODELC_1:17 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds ( s |= f 'or' g iff ( s |= f or s |= g ) ) proofend; :: definition of correctness of CTL-formula & its basic properties. definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); let s be Element of S; let H be CTL-formula; preds,kai |= H means :Def60: :: MODELC_1:def 60 s |= Evaluate (H,kai); end; :: deftheorem Def60 defines |= MODELC_1:def_60_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) for s being Element of S for H being CTL-formula holds ( s,kai |= H iff s |= Evaluate (H,kai) ); notation let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); let s be Element of S; let H be CTL-formula; antonym s,kai |/= H for s,kai |= H; end; theorem :: MODELC_1:18 for H being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) st H is atomic holds ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s ) proofend; theorem :: MODELC_1:19 for H being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds ( s,kai |= 'not' H iff s,kai |/= H ) proofend; theorem :: MODELC_1:20 for H1, H2 being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds ( s,kai |= H1 '&' H2 iff ( s,kai |= H1 & s,kai |= H2 ) ) proofend; theorem :: MODELC_1:21 for H1, H2 being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds ( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) ) proofend; theorem :: MODELC_1:22 for H being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds ( s,kai |= EX H iff ex pai being inf_path of R st ( pai . 0 = s & pai . 1,kai |= H ) ) proofend; theorem :: MODELC_1:23 for H being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds ( s,kai |= EG H iff ex pai being inf_path of R st ( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) ) proofend; theorem :: MODELC_1:24 for H1, H2 being CTL-formula for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds ( s,kai |= H1 EU H2 iff ex pai being inf_path of R st ( pai . 0 = s & ex m being Element of NAT st ( ( for j being Element of NAT st j < m holds pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) ) proofend; ::Some basic theorems for external Mizar files. theorem Th25: :: MODELC_1:25 for S being non empty set for R being total Relation of S,S for s0 being Element of S ex pai being inf_path of R st pai . 0 = s0 proofend; theorem :: MODELC_1:26 for S being non empty set for R being Relation of S,S holds ( R is total iff for x being set st x in S holds ex y being set st ( y in S & [x,y] in R ) ) by Lm31, Lm32; ::************* :: ::Verification of the basic algorithm :: for Model checking based on CTL. :: ::the basic algorithm is solver to get :: {s where s is Element of S: s,kai|=H} :: ::************* definition let S be non empty set ; let R be total Relation of S,S; let s0 be Element of S; let pai be inf_path of R; let n be set ; func PrePath (n,s0,pai) -> Element of S equals :Def61: :: MODELC_1:def 61 s0 if n = 0 otherwise pai . (k_nat ((k_nat n) - 1)); correctness coherence ( ( n = 0 implies s0 is Element of S ) & ( not n = 0 implies pai . (k_nat ((k_nat n) - 1)) is Element of S ) ); consistency for b1 being Element of S holds verum; ; end; :: deftheorem Def61 defines PrePath MODELC_1:def_61_:_ for S being non empty set for R being total Relation of S,S for s0 being Element of S for pai being inf_path of R for n being set holds ( ( n = 0 implies PrePath (n,s0,pai) = s0 ) & ( not n = 0 implies PrePath (n,s0,pai) = pai . (k_nat ((k_nat n) - 1)) ) ); theorem Th27: :: MODELC_1:27 for S being non empty set for R being total Relation of S,S for s0, s1 being Element of S st [s0,s1] in R holds ex pai being inf_path of R st ( pai . 0 = s0 & pai . 1 = s1 ) proofend; theorem Th28: :: MODELC_1:28 for S being non empty set for R being total Relation of S,S for s being Element of S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds ( s |= EX f iff ex s1 being Element of S st ( [s,s1] in R & s1 |= f ) ) proofend; :: definition of predecessor definition let S be non empty set ; let R be total Relation of S,S; let H be Subset of S; func Pred (H,R) -> Subset of S equals :: MODELC_1:def 62 { s where s is Element of S : ex t being Element of S st ( t in H & [s,t] in R ) } ; coherence { s where s is Element of S : ex t being Element of S st ( t in H & [s,t] in R ) } is Subset of S proofend; end; :: deftheorem defines Pred MODELC_1:def_62_:_ for S being non empty set for R being total Relation of S,S for H being Subset of S holds Pred (H,R) = { s where s is Element of S : ex t being Element of S st ( t in H & [s,t] in R ) } ; :: definition of SIGMA definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f be Assign of (BASSModel (R,BASSIGN)); func SIGMA f -> Subset of S equals :: MODELC_1:def 63 { s where s is Element of S : s |= f } ; correctness coherence { s where s is Element of S : s |= f } is Subset of S; proofend; end; :: deftheorem defines SIGMA MODELC_1:def_63_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : s |= f } ; Lm41: for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE } proofend; Lm42: for X being non empty set for f, g being Function of X,BOOLEAN st { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } holds f = g proofend; Lm43: for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds f = g proofend; :: SIGMA is one to one. theorem :: MODELC_1:29 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) st SIGMA f = SIGMA g holds f = g proofend; :: definition of Tau (inverse of SIGMA). definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let T be Subset of S; func Tau (T,R,BASSIGN) -> Assign of (BASSModel (R,BASSIGN)) means :Def64: :: MODELC_1:def 64 for s being set st s in S holds (Fid (it,S)) . s = (chi (T,S)) . s; existence ex b1 being Assign of (BASSModel (R,BASSIGN)) st for s being set st s in S holds (Fid (b1,S)) . s = (chi (T,S)) . s proofend; uniqueness for b1, b2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being set st s in S holds (Fid (b1,S)) . s = (chi (T,S)) . s ) & ( for s being set st s in S holds (Fid (b2,S)) . s = (chi (T,S)) . s ) holds b1 = b2 proofend; end; :: deftheorem Def64 defines Tau MODELC_1:def_64_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for T being Subset of S for b5 being Assign of (BASSModel (R,BASSIGN)) holds ( b5 = Tau (T,R,BASSIGN) iff for s being set st s in S holds (Fid (b5,S)) . s = (chi (T,S)) . s ); :: Tau is one to one. theorem :: MODELC_1:30 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for T1, T2 being Subset of S st Tau (T1,R,BASSIGN) = Tau (T2,R,BASSIGN) holds T1 = T2 proofend; :: Tau is on to. theorem Th31: :: MODELC_1:31 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds Tau ((SIGMA f),R,BASSIGN) = f proofend; :: SIGMA is on to. theorem Th32: :: MODELC_1:32 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for T being Subset of S holds SIGMA (Tau (T,R,BASSIGN)) = T proofend; :: SIGMA is homomorphism . theorem Th33: :: MODELC_1:33 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds ( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) ) proofend; :: Tau is monotonic. theorem Th34: :: MODELC_1:34 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for G1, G2 being Subset of S st G1 c= G2 holds for s being Element of S st s |= Tau (G1,R,BASSIGN) holds s |= Tau (G2,R,BASSIGN) proofend; :: SIGMA is monotonic. theorem Th35: :: MODELC_1:35 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f1, f2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= f1 holds s |= f2 ) holds SIGMA f1 c= SIGMA f2 proofend; :: theorems for translation :: problem of :: (1)find status s st s |= EG(f) :: (2)find status s st s |= f EU g :: to "find fixpoint of some function of bool S -> bool S". :: definition Fax(f,*):carrier ->carrier definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f, g be Assign of (BASSModel (R,BASSIGN)); func Fax (f,g) -> Assign of (BASSModel (R,BASSIGN)) equals :: MODELC_1:def 65 f '&' (EX g); correctness coherence f '&' (EX g) is Assign of (BASSModel (R,BASSIGN)); ; end; :: deftheorem defines Fax MODELC_1:def_65_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds Fax (f,g) = f '&' (EX g); :: Fax(f,*) is monotonic. theorem Th36: :: MODELC_1:36 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g1, g2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= g1 holds s |= g2 ) holds for s being Element of S st s |= Fax (f,g1) holds s |= Fax (f,g2) proofend; ::commutative :: Fax(f,*) :: Assigns ------> Assigns :: | | :: SIGMA | | Tau :: v v :: bool S -------> bool S :: SigFaxTau(f,*) :: definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f be Assign of (BASSModel (R,BASSIGN)); let G be Subset of S; func SigFaxTau (f,G,R,BASSIGN) -> Subset of S equals :: MODELC_1:def 66 SIGMA (Fax (f,(Tau (G,R,BASSIGN)))); coherence SIGMA (Fax (f,(Tau (G,R,BASSIGN)))) is Subset of S ; end; :: deftheorem defines SigFaxTau MODELC_1:def_66_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) for G being Subset of S holds SigFaxTau (f,G,R,BASSIGN) = SIGMA (Fax (f,(Tau (G,R,BASSIGN)))); :: SigFaxTau(f,*) is monotonic. theorem Th37: :: MODELC_1:37 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) for G1, G2 being Subset of S st G1 c= G2 holds SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN) proofend; :: Some tools to treat path. definition let S be non empty set ; let R be total Relation of S,S; let pai be inf_path of R; let k be Element of NAT ; func PathShift (pai,k) -> inf_path of R means :Def67: :: MODELC_1:def 67 for n being Element of NAT holds it . n = pai . (n + k); existence ex b1 being inf_path of R st for n being Element of NAT holds b1 . n = pai . (n + k) proofend; uniqueness for b1, b2 being inf_path of R st ( for n being Element of NAT holds b1 . n = pai . (n + k) ) & ( for n being Element of NAT holds b2 . n = pai . (n + k) ) holds b1 = b2 proofend; end; :: deftheorem Def67 defines PathShift MODELC_1:def_67_:_ for S being non empty set for R being total Relation of S,S for pai being inf_path of R for k being Element of NAT for b5 being inf_path of R holds ( b5 = PathShift (pai,k) iff for n being Element of NAT holds b5 . n = pai . (n + k) ); definition let S be non empty set ; let R be total Relation of S,S; let pai1, pai2 be inf_path of R; let n, k be Element of NAT ; func PathChange (pai1,pai2,k,n) -> set equals :Def68: :: MODELC_1:def 68 pai1 . n if n < k otherwise pai2 . (n - k); correctness coherence ( ( n < k implies pai1 . n is set ) & ( not n < k implies pai2 . (n - k) is set ) ); consistency for b1 being set holds verum; ; end; :: deftheorem Def68 defines PathChange MODELC_1:def_68_:_ for S being non empty set for R being total Relation of S,S for pai1, pai2 being inf_path of R for n, k being Element of NAT holds ( ( n < k implies PathChange (pai1,pai2,k,n) = pai1 . n ) & ( not n < k implies PathChange (pai1,pai2,k,n) = pai2 . (n - k) ) ); definition let S be non empty set ; let R be total Relation of S,S; let pai1, pai2 be inf_path of R; let k be Element of NAT ; func PathConc (pai1,pai2,k) -> Function of NAT,S means :Def69: :: MODELC_1:def 69 for n being Element of NAT holds it . n = PathChange (pai1,pai2,k,n); existence ex b1 being Function of NAT,S st for n being Element of NAT holds b1 . n = PathChange (pai1,pai2,k,n) proofend; uniqueness for b1, b2 being Function of NAT,S st ( for n being Element of NAT holds b1 . n = PathChange (pai1,pai2,k,n) ) & ( for n being Element of NAT holds b2 . n = PathChange (pai1,pai2,k,n) ) holds b1 = b2 proofend; end; :: deftheorem Def69 defines PathConc MODELC_1:def_69_:_ for S being non empty set for R being total Relation of S,S for pai1, pai2 being inf_path of R for k being Element of NAT for b6 being Function of NAT,S holds ( b6 = PathConc (pai1,pai2,k) iff for n being Element of NAT holds b6 . n = PathChange (pai1,pai2,k,n) ); theorem Th38: :: MODELC_1:38 for S being non empty set for R being total Relation of S,S for pai1, pai2 being inf_path of R for k being Element of NAT st pai1 . k = pai2 . 0 holds PathConc (pai1,pai2,k) is inf_path of R proofend; :: EG(f) is fixpoint of Fax(f,*). theorem Th39: :: MODELC_1:39 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) for s being Element of S holds ( s |= EG f iff s |= Fax (f,(EG f)) ) proofend; :: Existence path for fixpoint of Fax(f,*). theorem Th40: :: MODELC_1:40 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for g being Assign of (BASSModel (R,BASSIGN)) for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds s |= EX g ) holds ex pai being inf_path of R st ( pai . 0 = s0 & ( for n being Element of NAT holds pai . n |= g ) ) proofend; :: EG(f) is the maximum fixpoint of Fax(f,*) theorem Th41: :: MODELC_1:41 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds ( s |= g iff s |= Fax (f,g) ) ) holds for s being Element of S st s |= g holds s |= EG f proofend; :: definition of TransEG(f)::translated function for EG(f) definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f be Assign of (BASSModel (R,BASSIGN)); func TransEG f -> V226() Function of (bool S),(bool S) means :Def70: :: MODELC_1:def 70 for G being Subset of S holds it . G = SigFaxTau (f,G,R,BASSIGN); existence ex b1 being V226() Function of (bool S),(bool S) st for G being Subset of S holds b1 . G = SigFaxTau (f,G,R,BASSIGN) proofend; uniqueness for b1, b2 being V226() Function of (bool S),(bool S) st ( for G being Subset of S holds b1 . G = SigFaxTau (f,G,R,BASSIGN) ) & ( for G being Subset of S holds b2 . G = SigFaxTau (f,G,R,BASSIGN) ) holds b1 = b2 proofend; end; :: deftheorem Def70 defines TransEG MODELC_1:def_70_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) for b5 being V226() Function of (bool S),(bool S) holds ( b5 = TransEG f iff for G being Subset of S holds b5 . G = SigFaxTau (f,G,R,BASSIGN) ); :: fixpoint of TransEG(f) theorem Th42: :: MODELC_1:42 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds ( ( for s being Element of S holds ( s |= g iff s |= Fax (f,g) ) ) iff SIGMA g is_a_fixpoint_of TransEG f ) proofend; theorem :: MODELC_1:43 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EG f) = gfp (S,(TransEG f)) proofend; :: definition Foax(g,f,*):carrier ->carrier definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f, g, h be Assign of (BASSModel (R,BASSIGN)); func Foax (g,f,h) -> Assign of (BASSModel (R,BASSIGN)) equals :: MODELC_1:def 71 g 'or' (Fax (f,h)); coherence g 'or' (Fax (f,h)) is Assign of (BASSModel (R,BASSIGN)) ; end; :: deftheorem defines Foax MODELC_1:def_71_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g, h being Assign of (BASSModel (R,BASSIGN)) holds Foax (g,f,h) = g 'or' (Fax (f,h)); :: Foax(g,f,*) is monotonic. theorem Th44: :: MODELC_1:44 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g, h1, h2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= h1 holds s |= h2 ) holds for s being Element of S st s |= Foax (g,f,h1) holds s |= Foax (g,f,h2) proofend; ::commutative :: Foax(g,f,*) :: Assigns ------> Assigns :: | | :: SIGMA | | Tau :: v v :: bool S -------> bool S :: SigFoaxTau(g,f,*) :: definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f, g be Assign of (BASSModel (R,BASSIGN)); let H be Subset of S; func SigFoaxTau (g,f,H,R,BASSIGN) -> Subset of S equals :: MODELC_1:def 72 SIGMA (Foax (g,f,(Tau (H,R,BASSIGN)))); coherence SIGMA (Foax (g,f,(Tau (H,R,BASSIGN)))) is Subset of S ; end; :: deftheorem defines SigFoaxTau MODELC_1:def_72_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) for H being Subset of S holds SigFoaxTau (g,f,H,R,BASSIGN) = SIGMA (Foax (g,f,(Tau (H,R,BASSIGN)))); :: SigFoaxTau(g,f,*) is monotonic. theorem Th45: :: MODELC_1:45 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) for H1, H2 being Subset of S st H1 c= H2 holds SigFoaxTau (g,f,H1,R,BASSIGN) c= SigFoaxTau (g,f,H2,R,BASSIGN) proofend; :: f EU g is fixpoint of Foax(g,f,*). theorem Th46: :: MODELC_1:46 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) for s being Element of S holds ( s |= f EU g iff s |= Foax (g,f,(f EU g)) ) proofend; :: f EU g is the minimum fixpoint of Foax(g,f,*) theorem Th47: :: MODELC_1:47 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds ( s |= h iff s |= Foax (g,f,h) ) ) holds for s being Element of S st s |= f EU g holds s |= h proofend; :: definition of TransEU(f,g)::translated function for f EU g definition let S be non empty set ; let R be total Relation of S,S; let BASSIGN be non empty Subset of (ModelSP S); let f, g be Assign of (BASSModel (R,BASSIGN)); func TransEU (f,g) -> V226() Function of (bool S),(bool S) means :Def73: :: MODELC_1:def 73 for H being Subset of S holds it . H = SigFoaxTau (g,f,H,R,BASSIGN); existence ex b1 being V226() Function of (bool S),(bool S) st for H being Subset of S holds b1 . H = SigFoaxTau (g,f,H,R,BASSIGN) proofend; uniqueness for b1, b2 being V226() Function of (bool S),(bool S) st ( for H being Subset of S holds b1 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) & ( for H being Subset of S holds b2 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) holds b1 = b2 proofend; end; :: deftheorem Def73 defines TransEU MODELC_1:def_73_:_ for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) for b6 being V226() Function of (bool S),(bool S) holds ( b6 = TransEU (f,g) iff for H being Subset of S holds b6 . H = SigFoaxTau (g,f,H,R,BASSIGN) ); :: fixpoint of TransEU(f,g) theorem Th48: :: MODELC_1:48 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g, h being Assign of (BASSModel (R,BASSIGN)) holds ( ( for s being Element of S holds ( s |= h iff s |= Foax (g,f,h) ) ) iff SIGMA h is_a_fixpoint_of TransEU (f,g) ) proofend; theorem :: MODELC_1:49 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (f EU g) = lfp (S,(TransEU (f,g))) proofend; :: Solver for EX and TransEG,TransEU theorem Th50: :: MODELC_1:50 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EX f) = Pred ((SIGMA f),R) proofend; theorem :: MODELC_1:51 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f being Assign of (BASSModel (R,BASSIGN)) for X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R)) proofend; theorem :: MODELC_1:52 for S being non empty set for R being total Relation of S,S for BASSIGN being non empty Subset of (ModelSP S) for f, g being Assign of (BASSModel (R,BASSIGN)) for X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R))) proofend;