:: The Properties of Sets of Temporal Logic Subformulas :: by Mariusz Giero :: :: Received May 7, 2012 :: Copyright (c) 2012-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, FUNCT_1, XBOOLEAN, MODELC_2, CQC_THE1, NAT_1, XXREAL_0, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, FUNCT_2, HILBERT2, ZFMISC_1, FUNCOP_1, ZF_MODEL, PBOOLE, GLIB_000, FINSET_1, ABCMIZ_0, HENMODEL, PRE_POLY, RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1, UNIALG_2, MEMBER_1, FINSEQ_5, LTLAXIO1, LTLAXIO2, LTLAXIO3, XCMPLX_0; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, RELSET_1, PARTFUN1, DOMAIN_1, NUMBERS, XCMPLX_0, NAT_1, XXREAL_0, TREES_1, TREES_2, TREES_4, TREES_9, XREAL_0, NAT_D, FUNCT_2, FINSET_1, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, HILBERT2, PBOOLE, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, MATROID0, LTLAXIO1, LTLAXIO2; constructors XXREAL_0, NAT_D, RELSET_1, AOFA_I00, HILBERT2, FINSET_1, RFINSEQ, DOMAIN_1, AFINSQ_2, REAL_1, STRUCT_0, FUNCOP_1, XREAL_0, MATROID0, LEXBFS, MCART_1, CARD_1, RLAFFIN3, FINSEQ_4, FINSEQ_5, FINSEQ_2, RFINSEQ2, BINOP_2, ENUMSET1, SETFAM_1, TREES_9, TREES_2, TREES_4, AFINSQ_1, LTLAXIO1, LTLAXIO2, XTUPLE_0; registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1, LTLAXIO1, JORDAN23, CARD_1, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin reserve A,B,p,q,r,s for Element of LTLB_WFF, n for Element of NAT, X for Subset of LTLB_WFF, g for Function of LTLB_WFF,BOOLEAN, x,y for set; theorem :: LTLAXIO3:1 for X be non empty set,t be FinSequence of X,k be Nat st k+1 <= len t holds t/^k = <*t.(k+1)*>^(t/^(k+1)); theorem :: LTLAXIO3:2 NAT --> {} is LTLModel; definition let X; attr X is without_implication means :: LTLAXIO3:def 1 for p st p in X holds not p is conditional; end; definition let D be set; func D** -> set means :: LTLAXIO3:def 2 for x holds (x in it iff x is one-to-one FinSequence of D); end; registration let D be set; cluster D** -> non empty; end; registration let D be finite set; cluster D** -> finite; end; theorem :: LTLAXIO3:3 for D1, D2 being set st D1 c= D2 holds D1 ** c= D2 **; definition let a1 be set; let a2 be Subset of a1; redefine func a2 ** -> non empty Subset of (a1 **); end; theorem :: LTLAXIO3:4 for F, G being one-to-one FinSequence st rng F misses rng G holds F ^ G is one-to-one; definition let X be set; let f,g be one-to-one FinSequence of X; assume rng f misses rng g; func f ^^ g -> one-to-one FinSequence of X equals :: LTLAXIO3:def 3 f^g; end; begin definition func tau1 -> Function of LTLB_WFF,bool LTLB_WFF means :: LTLAXIO3:def 4 it.TFALSUM={TFALSUM} & it.(prop n)={prop n} & it.(A=>B)={A => B} \/ it.A \/ it.B & it.(A 'U' B)={A 'U' B}; end; theorem :: LTLAXIO3:5 not A is conditional implies tau1.A = {A}; theorem :: LTLAXIO3:6 p in tau1.p; registration let p; cluster tau1.p -> non empty finite; end; theorem :: LTLAXIO3:7 p => q in tau1.r implies p in tau1.r & q in tau1.r; theorem :: LTLAXIO3:8 p in tau1.q implies tau1.p c= tau1.q; theorem :: LTLAXIO3:9 p 'U' q in tau1.('not' A) implies p 'U' q in tau1.A; theorem :: LTLAXIO3:10 p 'U' q in tau1.(A '&&' B)implies(p 'U' q in tau1.A or p 'U' q in tau1.B); theorem :: LTLAXIO3:11 p in tau1.q & p <> q implies len p < len q; theorem :: LTLAXIO3:12 tau1.p c= tau1.('not' p); theorem :: LTLAXIO3:13 tau1.q c= tau1.(p '&&' q); theorem :: LTLAXIO3:14 tau1.q c= tau1.(p 'or' q); definition let X; func tau X -> Subset of LTLB_WFF means :: LTLAXIO3:def 5 x in it iff ex A st A in X & x in tau1.A; end; theorem :: LTLAXIO3:15 tau X = union {tau1.p where p is Element of LTLB_WFF: p in X}; theorem :: LTLAXIO3:16 X c= tau X; registration let X be empty Subset of LTLB_WFF; cluster tau X -> empty; end; registration let X be finite Subset of LTLB_WFF; cluster tau X -> finite; end; registration let X be non empty Subset of LTLB_WFF; cluster tau X -> non empty; end; theorem :: LTLAXIO3:17 tau tau X = tau X; theorem :: LTLAXIO3:18 X is without_implication implies tau X = X; theorem :: LTLAXIO3:19 p => q in tau X implies p in tau X & q in tau X; theorem :: LTLAXIO3:20 p '&&' q in tau X implies p in tau X & q in tau X; theorem :: LTLAXIO3:21 p 'or' q in tau X implies p in tau X & q in tau X; theorem :: LTLAXIO3:22 untn(p,q) in tau X implies p in tau X & q in tau X & p 'U' q in tau X; theorem :: LTLAXIO3:23 p in tau X implies tau1.p c= tau X; begin definition func Sub -> Function of LTLB_WFF,bool LTLB_WFF means :: LTLAXIO3:def 6 it.TFALSUM={TFALSUM} & it.(prop n)={prop n} & it.(A=>B)={A => B} \/ it.A \/ it.B & it.(A 'U' B)= tau1.untn (A,B) \/ it.A \/ it.B; end; theorem :: LTLAXIO3:24 p 'U' q in Sub.(p 'U' q); theorem :: LTLAXIO3:25 tau1.p c= Sub.p; registration let p; cluster Sub.p -> non empty finite; end; theorem :: LTLAXIO3:26 p in Sub.(A 'U' B) implies (A 'U' B in Sub.q implies p in Sub.q); definition let X; func Subt X -> Subset of bool LTLB_WFF equals :: LTLAXIO3:def 7 {Sub.A where A is Element of LTLB_WFF: A in X}; end; registration let X be finite Subset of LTLB_WFF; cluster Subt X -> finite finite-membered; end; begin definition mode PNPair is Element of [:LTLB_WFF**,LTLB_WFF**:]; end; reserve P,Q,P1,R for PNPair; definition let P; redefine func P`1 -> one-to-one FinSequence of LTLB_WFF; redefine func P`2 -> one-to-one FinSequence of LTLB_WFF; end; definition let P; func rng P -> finite Subset of LTLB_WFF equals :: LTLAXIO3:def 8 rng P`1 \/ rng P`2; end; definition let fp,fm be one-to-one FinSequence of LTLB_WFF; redefine func [fp,fm] -> PNPair; end; definition let P; func P^ -> Element of LTLB_WFF equals :: LTLAXIO3:def 9 (con (P`1))/.len (con (P`1)) '&&' (con nega (P`2))/.len (con nega (P`2)); end; theorem :: LTLAXIO3:27 [<*>LTLB_WFF,<*>LTLB_WFF]^ = TVERUM '&&' TVERUM; theorem :: LTLAXIO3:28 A in rng P`1 implies {} LTLB_WFF |- (P^) => A; theorem :: LTLAXIO3:29 A in rng P`2 implies {} LTLB_WFF |- (P^) => 'not' A; definition let P; attr P is Inconsistent means :: LTLAXIO3:def 10 {} LTLB_WFF |- 'not' (P^); end; notation let P; antonym P is consistent for P is Inconsistent; end; definition let P; attr P is complete means :: LTLAXIO3:def 11 tau rng P = rng P; end; registration cluster [<*> LTLB_WFF,<*> LTLB_WFF] -> consistent for PNPair; end; registration cluster [<*> LTLB_WFF,<*> LTLB_WFF] -> complete for PNPair; end; registration cluster consistent complete for PNPair; end; registration let P be consistent PNPair; cluster [P`1,P`2] -> consistent for PNPair; end; begin theorem :: LTLAXIO3:30 for P be consistent PNPair holds rng P`1 misses rng P`2; theorem :: LTLAXIO3:31 for P be consistent PNPair st not A in rng P holds ([(P`1)^^<*A*>,P`2] is consistent or [P`1,(P`2)^^<*A*>] is consistent); theorem :: LTLAXIO3:32 for P be consistent PNPair holds not TFALSUM in rng P`1; theorem :: LTLAXIO3:33 for P be consistent PNPair st A in rng P & B in rng P & A => B in rng P holds (A => B in rng P`1 iff (A in rng P`2 or B in rng P`1)); theorem :: LTLAXIO3:34 for P be consistent PNPair ex P1 be consistent PNPair st rng (P`1) c= rng (P1`1) & rng (P`2) c= rng (P1`2) & tau rng P = rng P1;