:: The Axiomatization of Propositional Linear Time Temporal Logic :: by Mariusz Giero :: :: Received November 20, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin Lm1: for X being set for f being FinSequence of X for i being Nat st 1 <= i & i <= len f holds f . i = f /. i proofend; theorem Th1: :: LTLAXIO1:1 for a, b, c being boolean number holds (a => (b '&' c)) => (a => b) = 1 proofend; theorem Th2: :: LTLAXIO1:2 for a, b, c being boolean number holds (a => (b => c)) => ((a '&' b) => c) = 1 proofend; theorem Th3: :: LTLAXIO1:3 for a, b, c being boolean number holds ((a '&' b) => c) => (a => (b => c)) = 1 proofend; begin notation synonym LTLB_WFF for HP-WFF ; end; notation synonym TFALSUM for VERUM ; end; notation let p, q be Element of LTLB_WFF ; synonym p 'Us' q for p '&' q; end; theorem Th4: :: LTLAXIO1:4 for A being Element of LTLB_WFF holds ( A = TFALSUM or ex n being Element of NAT st ( A = prop n or ex p, q being Element of LTLB_WFF st ( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'Us' q ) ) ) proofend; definition let p be Element of LTLB_WFF ; func 'not' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 1 p => TFALSUM; correctness coherence p => TFALSUM is Element of LTLB_WFF ; ; func 'X' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 2 TFALSUM 'Us' p; correctness coherence TFALSUM 'Us' p is Element of LTLB_WFF ; ; end; :: deftheorem defines 'not' LTLAXIO1:def_1_:_ for p being Element of LTLB_WFF holds 'not' p = p => TFALSUM; :: deftheorem defines 'X' LTLAXIO1:def_2_:_ for p being Element of LTLB_WFF holds 'X' p = TFALSUM 'Us' p; definition func TVERUM -> Element of LTLB_WFF equals :: LTLAXIO1:def 3 'not' TFALSUM; correctness coherence 'not' TFALSUM is Element of LTLB_WFF ; ; end; :: deftheorem defines TVERUM LTLAXIO1:def_3_:_ TVERUM = 'not' TFALSUM; definition let p, q be Element of LTLB_WFF ; funcp '&&' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 4 (p => (q => TFALSUM)) => TFALSUM; correctness coherence (p => (q => TFALSUM)) => TFALSUM is Element of LTLB_WFF ; ; end; :: deftheorem defines '&&' LTLAXIO1:def_4_:_ for p, q being Element of LTLB_WFF holds p '&&' q = (p => (q => TFALSUM)) => TFALSUM; definition let p, q be Element of LTLB_WFF ; funcp 'or' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 5 'not' (('not' p) '&&' ('not' q)); correctness coherence 'not' (('not' p) '&&' ('not' q)) is Element of LTLB_WFF ; ; end; :: deftheorem defines 'or' LTLAXIO1:def_5_:_ for p, q being Element of LTLB_WFF holds p 'or' q = 'not' (('not' p) '&&' ('not' q)); definition let p be Element of LTLB_WFF ; func 'G' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 6 'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p)))); correctness coherence 'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p)))) is Element of LTLB_WFF ; ; end; :: deftheorem defines 'G' LTLAXIO1:def_6_:_ for p being Element of LTLB_WFF holds 'G' p = 'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p)))); definition let p be Element of LTLB_WFF ; func 'F' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 7 'not' ('G' ('not' p)); correctness coherence 'not' ('G' ('not' p)) is Element of LTLB_WFF ; ; end; :: deftheorem defines 'F' LTLAXIO1:def_7_:_ for p being Element of LTLB_WFF holds 'F' p = 'not' ('G' ('not' p)); definition let p, q be Element of LTLB_WFF ; funcp 'U' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 8 q 'or' (p '&&' (p 'Us' q)); correctness coherence q 'or' (p '&&' (p 'Us' q)) is Element of LTLB_WFF ; ; end; :: deftheorem defines 'U' LTLAXIO1:def_8_:_ for p, q being Element of LTLB_WFF holds p 'U' q = q 'or' (p '&&' (p 'Us' q)); definition let p, q be Element of LTLB_WFF ; funcp 'R' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 9 'not' (('not' p) 'U' ('not' q)); correctness coherence 'not' (('not' p) 'U' ('not' q)) is Element of LTLB_WFF ; ; end; :: deftheorem defines 'R' LTLAXIO1:def_9_:_ for p, q being Element of LTLB_WFF holds p 'R' q = 'not' (('not' p) 'U' ('not' q)); begin definition func props -> Subset of LTLB_WFF means :: LTLAXIO1:def 10 for x being set holds ( x in it iff ex n being Element of NAT st x = prop n ); existence ex b1 being Subset of LTLB_WFF st for x being set holds ( x in b1 iff ex n being Element of NAT st x = prop n ) proofend; uniqueness for b1, b2 being Subset of LTLB_WFF st ( for x being set holds ( x in b1 iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds ( x in b2 iff ex n being Element of NAT st x = prop n ) ) holds b1 = b2 proofend; end; :: deftheorem defines props LTLAXIO1:def_10_:_ for b1 being Subset of LTLB_WFF holds ( b1 = props iff for x being set holds ( x in b1 iff ex n being Element of NAT st x = prop n ) ); definition mode LTLModel is sequence of (bool props); end; definition let M be LTLModel; func SAT M -> Function of [:NAT,LTLB_WFF:],BOOLEAN means :Def11: :: LTLAXIO1:def 11 for n being Element of NAT holds ( it . [n,TFALSUM] = 0 & ( for k being Element of NAT holds ( it . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds ( it . [n,(p => q)] = (it . [n,p]) => (it . [n,q]) & ( it . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st ( 0 < i & it . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds it . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st ( 0 < i & it . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds it . [(n + j),p] = 1 ) ) implies it . [n,(p 'Us' q)] = 1 ) ) ) ); existence ex b1 being Function of [:NAT,LTLB_WFF:],BOOLEAN st for n being Element of NAT holds ( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds ( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds ( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st ( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st ( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'Us' q)] = 1 ) ) ) ) proofend; uniqueness for b1, b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN st ( for n being Element of NAT holds ( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds ( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds ( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st ( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st ( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'Us' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds ( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds ( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds ( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st ( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st ( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'Us' q)] = 1 ) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines SAT LTLAXIO1:def_11_:_ for M being LTLModel for b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN holds ( b2 = SAT M iff for n being Element of NAT holds ( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds ( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds ( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st ( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st ( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'Us' q)] = 1 ) ) ) ) ); theorem Th5: :: LTLAXIO1:5 for A being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 ) proofend; theorem Th6: :: LTLAXIO1:6 for n being Element of NAT for M being LTLModel holds (SAT M) . [n,TVERUM] = 1 proofend; theorem Th7: :: LTLAXIO1:7 for A, B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) ) proofend; theorem Th8: :: LTLAXIO1:8 for A, B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) ) proofend; theorem Th9: :: LTLAXIO1:9 for A being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] proofend; theorem Th10: :: LTLAXIO1:10 for A being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 ) proofend; theorem Th11: :: LTLAXIO1:11 for A being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 ) proofend; theorem Th12: :: LTLAXIO1:12 for p, q being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st ( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds (SAT M) . [(n + j),p] = 1 ) ) ) proofend; theorem :: LTLAXIO1:13 for p, q being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds ( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st ( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds (SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) ) proofend; theorem Th14: :: LTLAXIO1:14 for B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))] proofend; theorem Th15: :: LTLAXIO1:15 for B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1 proofend; theorem Th16: :: LTLAXIO1:16 for B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1 proofend; theorem Th17: :: LTLAXIO1:17 for B, C being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1 proofend; theorem Th18: :: LTLAXIO1:18 for B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1 proofend; theorem Th19: :: LTLAXIO1:19 for B, C being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1 proofend; theorem Th20: :: LTLAXIO1:20 for C, B being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1 proofend; theorem Th21: :: LTLAXIO1:21 for B, C being Element of LTLB_WFF for n being Element of NAT for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1 proofend; begin definition let M be LTLModel; let p be Element of LTLB_WFF ; predM |= p means :Def12: :: LTLAXIO1:def 12 for n being Element of NAT holds (SAT M) . [n,p] = 1; end; :: deftheorem Def12 defines |= LTLAXIO1:def_12_:_ for M being LTLModel for p being Element of LTLB_WFF holds ( M |= p iff for n being Element of NAT holds (SAT M) . [n,p] = 1 ); definition let M be LTLModel; let F be Subset of LTLB_WFF; predM |= F means :Def13: :: LTLAXIO1:def 13 for p being Element of LTLB_WFF st p in F holds M |= p; end; :: deftheorem Def13 defines |= LTLAXIO1:def_13_:_ for M being LTLModel for F being Subset of LTLB_WFF holds ( M |= F iff for p being Element of LTLB_WFF st p in F holds M |= p ); definition let F be Subset of LTLB_WFF; let p be Element of LTLB_WFF ; predF |= p means :Def14: :: LTLAXIO1:def 14 for M being LTLModel st M |= F holds M |= p; end; :: deftheorem Def14 defines |= LTLAXIO1:def_14_:_ for F being Subset of LTLB_WFF for p being Element of LTLB_WFF holds ( F |= p iff for M being LTLModel st M |= F holds M |= p ); theorem Th22: :: LTLAXIO1:22 for F, G being Subset of LTLB_WFF for M being LTLModel holds ( ( M |= F & M |= G ) iff M |= F \/ G ) proofend; theorem Th23: :: LTLAXIO1:23 for A being Element of LTLB_WFF for M being LTLModel holds ( M |= A iff M |= {A} ) proofend; theorem Th24: :: LTLAXIO1:24 for A, B being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |= A & F |= A => B holds F |= B proofend; theorem Th25: :: LTLAXIO1:25 for A being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |= A holds F |= 'X' A proofend; theorem :: LTLAXIO1:26 for A being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |= A holds F |= 'G' A proofend; theorem Th27: :: LTLAXIO1:27 for A, B being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds F |= A => ('G' B) proofend; theorem Th28: :: LTLAXIO1:28 for A being Element of LTLB_WFF for i, j being Element of NAT for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A] proofend; theorem Th29: :: LTLAXIO1:29 for F being Subset of LTLB_WFF for i being Element of NAT for M being LTLModel st M |= F holds M ^\ i |= F proofend; theorem :: LTLAXIO1:30 for A, B being Element of LTLB_WFF for F being Subset of LTLB_WFF holds ( F \/ {A} |= B iff F |= ('G' A) => B ) proofend; definition let f be Function of LTLB_WFF,BOOLEAN; func VAL f -> Function of LTLB_WFF,BOOLEAN means :Def15: :: LTLAXIO1:def 15 for A, B being Element of LTLB_WFF for n being Element of NAT holds ( it . TFALSUM = 0 & it . (prop n) = f . (prop n) & it . (A => B) = (it . A) => (it . B) & it . (A 'Us' B) = f . (A 'Us' B) ); existence ex b1 being Function of LTLB_WFF,BOOLEAN st for A, B being Element of LTLB_WFF for n being Element of NAT holds ( b1 . TFALSUM = 0 & b1 . (prop n) = f . (prop n) & b1 . (A => B) = (b1 . A) => (b1 . B) & b1 . (A 'Us' B) = f . (A 'Us' B) ) proofend; uniqueness for b1, b2 being Function of LTLB_WFF,BOOLEAN st ( for A, B being Element of LTLB_WFF for n being Element of NAT holds ( b1 . TFALSUM = 0 & b1 . (prop n) = f . (prop n) & b1 . (A => B) = (b1 . A) => (b1 . B) & b1 . (A 'Us' B) = f . (A 'Us' B) ) ) & ( for A, B being Element of LTLB_WFF for n being Element of NAT holds ( b2 . TFALSUM = 0 & b2 . (prop n) = f . (prop n) & b2 . (A => B) = (b2 . A) => (b2 . B) & b2 . (A 'Us' B) = f . (A 'Us' B) ) ) holds b1 = b2 proofend; end; :: deftheorem Def15 defines VAL LTLAXIO1:def_15_:_ for f, b2 being Function of LTLB_WFF,BOOLEAN holds ( b2 = VAL f iff for A, B being Element of LTLB_WFF for n being Element of NAT holds ( b2 . TFALSUM = 0 & b2 . (prop n) = f . (prop n) & b2 . (A => B) = (b2 . A) => (b2 . B) & b2 . (A 'Us' B) = f . (A 'Us' B) ) ); theorem Th31: :: LTLAXIO1:31 for f being Function of LTLB_WFF,BOOLEAN for p, q being Element of LTLB_WFF holds (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q) proofend; theorem Th32: :: LTLAXIO1:32 for A being Element of LTLB_WFF for n being Element of NAT for M being LTLModel for f being Function of LTLB_WFF,BOOLEAN st ( for B being set st B in LTLB_WFF holds f . B = (SAT M) . [n,B] ) holds (VAL f) . A = (SAT M) . [n,A] proofend; definition let p be Element of LTLB_WFF ; attrp is LTL_TAUT_OF_PL means :Def16: :: LTLAXIO1:def 16 for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1; end; :: deftheorem Def16 defines LTL_TAUT_OF_PL LTLAXIO1:def_16_:_ for p being Element of LTLB_WFF holds ( p is LTL_TAUT_OF_PL iff for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1 ); theorem Th33: :: LTLAXIO1:33 for A being Element of LTLB_WFF for F being Subset of LTLB_WFF st A is LTL_TAUT_OF_PL holds F |= A proofend; begin definition let D be set ; attrD is with_LTL_axioms means :Def17: :: LTLAXIO1:def 17 for p, q being Element of LTLB_WFF holds ( ( p is LTL_TAUT_OF_PL implies p in D ) & ('not' ('X' p)) => ('X' ('not' p)) in D & ('X' ('not' p)) => ('not' ('X' p)) in D & ('X' (p => q)) => (('X' p) => ('X' q)) in D & ('G' p) => (p '&&' ('X' ('G' p))) in D & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D & (p 'Us' q) => ('X' ('F' q)) in D ); end; :: deftheorem Def17 defines with_LTL_axioms LTLAXIO1:def_17_:_ for D being set holds ( D is with_LTL_axioms iff for p, q being Element of LTLB_WFF holds ( ( p is LTL_TAUT_OF_PL implies p in D ) & ('not' ('X' p)) => ('X' ('not' p)) in D & ('X' ('not' p)) => ('not' ('X' p)) in D & ('X' (p => q)) => (('X' p) => ('X' q)) in D & ('G' p) => (p '&&' ('X' ('G' p))) in D & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D & (p 'Us' q) => ('X' ('F' q)) in D ) ); definition func LTL_axioms -> Subset of LTLB_WFF means :Def18: :: LTLAXIO1:def 18 ( it is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds it c= D ) ); existence ex b1 being Subset of LTLB_WFF st ( b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds b1 c= D ) ) proofend; uniqueness for b1, b2 being Subset of LTLB_WFF st b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds b1 c= D ) & b2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds b2 c= D ) holds b1 = b2 proofend; end; :: deftheorem Def18 defines LTL_axioms LTLAXIO1:def_18_:_ for b1 being Subset of LTLB_WFF holds ( b1 = LTL_axioms iff ( b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds b1 c= D ) ) ); registration cluster LTL_axioms -> with_LTL_axioms ; coherence LTL_axioms is with_LTL_axioms by Def18; end; theorem Th34: :: LTLAXIO1:34 for p, q being Element of LTLB_WFF holds p => (q => p) in LTL_axioms proofend; theorem Th35: :: LTLAXIO1:35 for p, q, r being Element of LTLB_WFF holds (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms proofend; definition let p, q be Element of LTLB_WFF ; predp NEX_rule q means :Def19: :: LTLAXIO1:def 19 q = 'X' p; let r be Element of LTLB_WFF ; predp,q MP_rule r means :Def20: :: LTLAXIO1:def 20 q = p => r; predp,q IND_rule r means :Def21: :: LTLAXIO1:def 21 ex A, B being Element of LTLB_WFF st ( p = A => B & q = A => ('X' A) & r = A => ('G' B) ); end; :: deftheorem Def19 defines NEX_rule LTLAXIO1:def_19_:_ for p, q being Element of LTLB_WFF holds ( p NEX_rule q iff q = 'X' p ); :: deftheorem Def20 defines MP_rule LTLAXIO1:def_20_:_ for p, q, r being Element of LTLB_WFF holds ( p,q MP_rule r iff q = p => r ); :: deftheorem Def21 defines IND_rule LTLAXIO1:def_21_:_ for p, q, r being Element of LTLB_WFF holds ( p,q IND_rule r iff ex A, B being Element of LTLB_WFF st ( p = A => B & q = A => ('X' A) & r = A => ('G' B) ) ); registration cluster LTL_axioms -> non empty ; coherence not LTL_axioms is empty by Def17; end; definition let A be Element of LTLB_WFF ; attrA is axltl1 means :Def22: :: LTLAXIO1:def 22 ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B)); attrA is axltl1a means :Def23: :: LTLAXIO1:def 23 ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B)); attrA is axltl2 means :Def24: :: LTLAXIO1:def 24 ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C)); attrA is axltl3 means :Def25: :: LTLAXIO1:def 25 ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B))); attrA is axltl4 means :Def26: :: LTLAXIO1:def 26 ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))); attrA is axltl5 means :Def27: :: LTLAXIO1:def 27 ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C); attrA is axltl6 means :Def28: :: LTLAXIO1:def 28 ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => ('X' ('F' C)); end; :: deftheorem Def22 defines axltl1 LTLAXIO1:def_22_:_ for A being Element of LTLB_WFF holds ( A is axltl1 iff ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B)) ); :: deftheorem Def23 defines axltl1a LTLAXIO1:def_23_:_ for A being Element of LTLB_WFF holds ( A is axltl1a iff ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B)) ); :: deftheorem Def24 defines axltl2 LTLAXIO1:def_24_:_ for A being Element of LTLB_WFF holds ( A is axltl2 iff ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C)) ); :: deftheorem Def25 defines axltl3 LTLAXIO1:def_25_:_ for A being Element of LTLB_WFF holds ( A is axltl3 iff ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B))) ); :: deftheorem Def26 defines axltl4 LTLAXIO1:def_26_:_ for A being Element of LTLB_WFF holds ( A is axltl4 iff ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) ); :: deftheorem Def27 defines axltl5 LTLAXIO1:def_27_:_ for A being Element of LTLB_WFF holds ( A is axltl5 iff ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C) ); :: deftheorem Def28 defines axltl6 LTLAXIO1:def_28_:_ for A being Element of LTLB_WFF holds ( A is axltl6 iff ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => ('X' ('F' C)) ); theorem Th36: :: LTLAXIO1:36 for A being Element of LTL_axioms holds ( A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) proofend; theorem Th37: :: LTLAXIO1:37 for A being Element of LTLB_WFF for F being Subset of LTLB_WFF st ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) holds F |= A proofend; definition let i be Nat; let f be FinSequence of LTLB_WFF ; let X be Subset of LTLB_WFF; pred prc f,X,i means :Def29: :: LTLAXIO1:def 29 ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st ( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st ( 1 <= j & j < i & f /. j NEX_rule f /. i ) ); end; :: deftheorem Def29 defines prc LTLAXIO1:def_29_:_ for i being Nat for f being FinSequence of LTLB_WFF for X being Subset of LTLB_WFF holds ( prc f,X,i iff ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st ( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st ( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) ); definition let X be Subset of LTLB_WFF; let p be Element of LTLB_WFF ; predX |- p means :Def30: :: LTLAXIO1:def 30 ex f being FinSequence of LTLB_WFF st ( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds prc f,X,i ) ); end; :: deftheorem Def30 defines |- LTLAXIO1:def_30_:_ for X being Subset of LTLB_WFF for p being Element of LTLB_WFF holds ( X |- p iff ex f being FinSequence of LTLB_WFF st ( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds prc f,X,i ) ) ); theorem Th38: :: LTLAXIO1:38 for X being Subset of LTLB_WFF for f, f2 being FinSequence of LTLB_WFF for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,X,i holds prc f2,X,i + n proofend; theorem Th39: :: LTLAXIO1:39 for X being Subset of LTLB_WFF for f2, f, f1 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds prc f1,X,i ) holds for i being Nat st 1 <= i & i <= len f2 holds prc f2,X,i proofend; theorem Th40: :: LTLAXIO1:40 for p being Element of LTLB_WFF for X being Subset of LTLB_WFF for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds prc f1,X,i ) & prc f,X, len f holds ( ( for i being Nat st 1 <= i & i <= len f holds prc f,X,i ) & X |- p ) proofend; theorem :: LTLAXIO1:41 for A being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |- A holds F |= A proofend; begin theorem Th42: :: LTLAXIO1:42 for p being Element of LTLB_WFF for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds X |- p proofend; theorem Th43: :: LTLAXIO1:43 for p, q being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p & X |- p => q holds X |- q proofend; theorem Th44: :: LTLAXIO1:44 for p being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p holds X |- 'X' p proofend; theorem Th45: :: LTLAXIO1:45 for p, q being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p => q & X |- p => ('X' p) holds X |- p => ('G' q) proofend; theorem Th46: :: LTLAXIO1:46 for r, p, q being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- r => (p '&&' q) holds ( X |- r => p & X |- r => q ) proofend; theorem Th47: :: LTLAXIO1:47 for p, q, r being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p => q & X |- q => r holds X |- p => r proofend; theorem Th48: :: LTLAXIO1:48 for p, q, r being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p => (q => r) holds X |- (p '&&' q) => r proofend; theorem Th49: :: LTLAXIO1:49 for p, q, r being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- (p '&&' q) => r holds X |- p => (q => r) proofend; theorem Th50: :: LTLAXIO1:50 for p, q, r, s being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- (p '&&' q) => r & X |- p => s holds X |- (p '&&' q) => (s '&&' r) proofend; theorem Th51: :: LTLAXIO1:51 for p, q, r, s being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p => (q => r) & X |- r => s holds X |- p => (q => s) proofend; theorem Th52: :: LTLAXIO1:52 for p, q being Element of LTLB_WFF for X being Subset of LTLB_WFF st X |- p => q holds X |- ('not' q) => ('not' p) proofend; theorem Th53: :: LTLAXIO1:53 for p, q being Element of LTLB_WFF for X being Subset of LTLB_WFF holds X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q)) proofend; theorem Th54: :: LTLAXIO1:54 for p being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |- p holds F |- 'G' p proofend; theorem Th55: :: LTLAXIO1:55 for p, q being Element of LTLB_WFF for F being Subset of LTLB_WFF st p => q in F holds F \/ {p} |- 'G' q proofend; theorem Th56: :: LTLAXIO1:56 for q, p being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |- q holds F \/ {p} |- q proofend; theorem Th57: :: LTLAXIO1:57 for p, q being Element of LTLB_WFF for F being Subset of LTLB_WFF st F \/ {p} |- q holds F |- ('G' p) => q proofend; theorem :: LTLAXIO1:58 for p, q being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |- p => q holds F \/ {p} |- q proofend; theorem :: LTLAXIO1:59 for p, q being Element of LTLB_WFF for F being Subset of LTLB_WFF st F |- ('G' p) => q holds F \/ {p} |- q proofend; theorem :: LTLAXIO1:60 for p, q being Element of LTLB_WFF for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q)) proofend;