:: Weak Completeness Theorem for Propositional Linear Time Temporal Logic :: by Mariusz Giero :: :: Received May 7, 2012 :: Copyright (c) 2012-2018 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, ORDINAL1, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, HILBERT2, ZFMISC_1, ZF_MODEL, GLIB_000, FINSET_1, ABCMIZ_0, HENMODEL, PRE_POLY, RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1, UNIALG_2, TREES_1, TREES_2, TREES_4, SETFAM_1, NECKLA_3, MEMBER_1, AOFA_I00, FINSEQ_4, FINSEQ_2, RFINSEQ2, TREES_9, INT_1, VECTSP_1, LTLAXIO1, LTLAXIO2, LTLAXIO3, LTLAXIO4, GOEDCPUC, XCMPLX_0; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, RELAT_1, FUNCT_1, 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, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, HILBERT2, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, MATROID0, RLAFFIN3, LTLAXIO1, LTLAXIO2, LTLAXIO3; 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, LTLAXIO3; registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1, JORDAN23, FINSEQ_2, CARD_1, TREES_9, TREES_2, XTUPLE_0, LTLAXIO1, LTLAXIO3; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions TARSKI, XBOOLE_0, FINSEQ_2, FINSET_1, LTLAXIO1; equalities XBOOLEAN, FINSEQ_1, TREES_2, LTLAXIO1, LTLAXIO2, LTLAXIO3; expansions TARSKI, XBOOLE_0, LTLAXIO1, LTLAXIO3; theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, NAT_D, XBOOLEAN, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, HILBERT2, XREAL_0, FINSEQ_4, RFINSEQ, RELAT_1, FINSEQ_5, FUNCT_1, FINSEQ_3, FINSEQ_6, XBOOLE_1, PRE_POLY, STIRL2_1, RLAFFIN3, HILBERT1, RFINSEQ2, NUMBERS, PARTFUN2, TREES_9, TREES_1, TREES_2, LTLAXIO1, LTLAXIO2, LTLAXIO3; schemes NAT_1, FUNCT_2, HILBERT2, RECDEF_1, FRAENKEL, FINSEQ_4, FINSEQ_2, TREES_9, TREES_2; begin reserve A,B,p,q,r for Element of LTLB_WFF, M for LTLModel, j,k,n for Element of NAT, i for Nat, X for Subset of LTLB_WFF, F for finite Subset of LTLB_WFF, f for FinSequence of LTLB_WFF, g for Function of LTLB_WFF,BOOLEAN, x,y,z for set, P,Q,R for PNPair; set l = LTLB_WFF,pairs = [:l**,l**:]; deffunc alt(FinSequence of l) = 'not'((con nega $1)/.(len con nega $1)); deffunc kon(FinSequence of l) = ((con $1)/.(len con $1)); definition let X be finite set; redefine mode Enumeration of X -> one-to-one FinSequence of X; coherence proof let E be Enumeration of X; rng E = X by RLAFFIN3:def 1; hence E is one-to-one FinSequence of X by FINSEQ_1:def 4; end; end; definition let E be set,F be finite Subset of E; redefine mode Enumeration of F -> one-to-one FinSequence of E; coherence proof let f be Enumeration of F; rng f = F by RLAFFIN3:def 1; hence thesis by FINSEQ_1:def 4; end; end; registration let D be set; cluster non empty finite for FinSequenceSet of D; existence proof {<*> D} is FinSequenceSet of D proof let a be object; thus a in {<*> D} implies a is FinSequence of D by TARSKI:def 1; end; hence thesis; end; end; theorem Th1: for X be set,G be non empty finite FinSequenceSet of X holds ex A be FinSequence st A in G & for B be FinSequence st B in G holds len B <= len A proof let X be set,G be non empty finite FinSequenceSet of X; set g = the Enumeration of G; deffunc F1(Nat)= len (g/.$1); consider f be FinSequence of NAT such that A1: len f = len g & for n be Nat st n in dom f holds f.n = F1(n) from FINSEQ_2:sch 1; rng f c= REAL by NUMBERS:19; then reconsider f1 = f as FinSequence of REAL by FINSEQ_1:def 4; set m = max_p f1, A = g/.m; A2: g <> {} by RLAFFIN3:def 1,RELAT_1:38; for B be FinSequence st B in G holds len B <= len A proof let B be FinSequence; set m1 = B .. g; m in dom f by A2,A1,RFINSEQ2:def 1; then A3: len A = f1.m by A1; assume B in G; then A4: B in rng g by RLAFFIN3:def 1; then A5: m1 in dom g by FINSEQ_4:20; then A6: m1 in dom f by A1,FINSEQ_3:29; g/.m1 = g.m1 by A5,PARTFUN1:def 6 .= B by FINSEQ_4:19,A4; then len B = f1.m1 by A6,A1; hence len B <= len A by A6,RFINSEQ2:def 1, A2,A1,A3; end; hence thesis; end; definition let T be DecoratedTree; let n; let t be Node of T; redefine func t | n -> Node of T; correctness proof set tn = t|n; ex p be FinSequence st t = tn^p by FINSEQ_1:80; hence tn is Node of T by TREES_1:21; end; end; theorem Th2: p is FinSequence of NAT proof l c= NAT* by HILBERT1:def 5; then p in NAT*; hence thesis by FINSEQ_1:def 11; end; notation let A; synonym A is s-until for A is conjunctive; end; definition let A; assume A1:A is s-until; func rarg A -> Element of LTLB_WFF means :Def1: ex p st p 'U' it = A; existence proof ex p,q st p 'U' q = A by A1,HILBERT2:def 6; hence thesis; end; uniqueness by HILBERT2:19; end; definition let A; attr A is satisfiable means ex M,n st (SAT M).[n,A] = 1; end; theorem Th3: {} LTLB_WFF |= A iff not 'not' A is satisfiable proof hereby assume A1: {}l |= A; assume 'not' A is satisfiable; then consider M,n such that A2: (SAT M).[n,'not' A] = 1; A3: M |= {}l; (SAT M).[n,A] = 0 by A2,LTLAXIO1:5; hence contradiction by A3,A1,LTLAXIO1:def 12; end; assume A4: not 'not' A is satisfiable; assume not {}l |= A; then consider M such that M |= {}l and A5: not M |= A; consider n such that A6: not (SAT M).[n,A] = 1 by A5; (SAT M).[n,'not' A] = 1 by A6,XBOOLEAN:def 3,LTLAXIO1:5; hence contradiction by A4; end; theorem Th4: TVERUM '&&' A is satisfiable implies A is satisfiable proof assume TVERUM '&&' A is satisfiable; then consider M,n such that A1: (SAT M).[n,TVERUM '&&' A] = 1; (SAT M).[n,A] = 1 by LTLAXIO1:7,A1; hence A is satisfiable; end; theorem Th5: for i being Element of NAT holds (SAT M).[i,p 'U' q] = 1 iff ex j st j > i & (SAT M).[j,q] = 1 & for k st i < k & k < j holds (SAT M).[k,p] = 1 proof let i be Element of NAT; set s = SAT M; hereby assume s.[i,p 'U' q] = 1; then consider j being Element of NAT such that A1: 0 < j & s.[i+j,q] = 1 and A2: for k st 1 <= k & k < j holds s.[(i + k),p] = 1 by LTLAXIO1:def 11; set m = i+j; now let k; assume that A3: i < k and A4: k < m; reconsider k1 = k-i as Element of NAT by A3,NAT_1:21; i + (-i) < k + (-i) by A3,XREAL_1:8; then A5: 1 <= k1 by NAT_1:25; k + (-i) < m + (-i) by A4,XREAL_1:8; then s.[i+k1,p] = 1 by A5,A2; hence s.[k,p] = 1; end; hence ex j st j > i & s.[j,q] = 1 & for k st i < k & k < j holds s.[k,p] = 1 by A1,NAT_1:16; end; given j such that A6: j > i and A7: s.[j,q] = 1 and A8: for k st i < k & k < j holds s.[k,p] = 1; reconsider n = j - i as Element of NAT by A6,NAT_1:21; A9: now let k; assume 1 <= k & k < n; then k+i < n+i & i < i+ k by XREAL_1:8,NAT_1:16; hence s.[i+k,p] = 1 by A8; end; j + (-i) > i + (-i) & s.[i+n,q] = 1 by A6,XREAL_1:8, A7; hence s.[i,p 'U' q] = 1 by A9,LTLAXIO1:def 11; end; theorem Th6: (SAT M).[n,(con f)/.(len con f)] = 1 iff for i st i in dom f holds (SAT M).[n,f/.i] = 1 proof set s = SAT M; defpred P[Nat] means for f st len f = $1 holds s.[n,kon(f)] = 1 iff (for i st i in dom f holds s.[n,f/.i] = 1); A1: now let k be Nat; assume A2: P[k]; thus P[k + 1] proof let f; A3: 1 <= k+1 by NAT_1:11; set fk = f|k; assume A4: len f = k+1; A5: dom fk c= dom f by RELAT_1:60; per cases; suppose A6: k > 0; then A7: 1 <= k by NAT_1:25; A8: kon(f) = (con f)/.(k+1) by LTLAXIO2:def 2,A4 .= ((con f) /. k) '&&' (f /. (k + 1)) by LTLAXIO2:7,A7, NAT_1:16,A4; A9: k < len f by NAT_1:16,A4; then A10: len fk = k by FINSEQ_1:59; A11: (con f)/.k = (con (f | k))/.k by A7,A9,LTLAXIO2:13 .= kon(fk) by A10,LTLAXIO2:def 2,A6; hereby assume A12: s.[n,kon(f)] = 1; then A13: s.[n,kon(fk)] = 1 by A8,LTLAXIO1:7,A11; let i; assume A14: i in dom f; then A15: 1 <= i by FINSEQ_3:25; A16: i <= len f by A14,FINSEQ_3:25; per cases by A16,XXREAL_0:1; suppose i < len f; then i <= k by A4,NAT_1:13; then A17: i in dom fk by A10,FINSEQ_3:25,A15; then s.[n,fk/.i] = 1 by A2,A10,A13; hence s.[n,f/.i] = 1 by FINSEQ_4:70,A17; end; suppose i = len f; hence s.[n,f/.i] = 1 by A4, A12,A8,LTLAXIO1:7; end; end; assume A18: for i st i in dom f holds s.[n,f/.i] = 1; now let i; assume A19: i in dom fk; then s.[n,f/.i] = 1 by A5,A18; hence s.[n,fk/.i] = 1 by FINSEQ_4:70,A19; end; then A20: s.[n,((con f) /. k)] = 1 by A2,A10,A11; s.[n,(f /. (k + 1))] = 1 by A18, FINSEQ_3:25,A4,A3; hence s.[n,kon(f)] = 1 by LTLAXIO1:7,A20,A8; end; suppose A21: k = 0; then A22: kon(f) = (con f)/.1 by A4,LTLAXIO2:def 2 .= f/.1 by LTLAXIO2:6,A4; hereby assume A23: s.[n,kon(f)] = 1; let i; assume i in dom f; then 1 <= i & i <= len f by FINSEQ_3:25; hence s.[n,f/.i] = 1 by NAT_1:25, A21,A4, A23, A22; end; assume for i st i in dom f holds s.[n,f/.i] = 1; hence s.[n,kon(f)] = 1 by A21,A4,FINSEQ_3:25,A22; end; end; end; A24: P[0] proof let f; assume len f = 0; then f = {}; hence thesis by LTLAXIO1:6,LTLAXIO2:10; end; for k being Nat holds P[k] from NAT_1:sch 2(A24,A1); then P[len f]; hence thesis; end; theorem Th7: ([<*> LTLB_WFF,<*A*>])^ = TVERUM '&&' 'not' A proof nega <*A*> = <*'not' A*> & [<*> l,<*A*>]`1 = <*> l by LTLAXIO2:14; hence thesis by LTLAXIO2:10, LTLAXIO2:11; end; theorem Th8: for P be complete PNPair st untn(A,B) in rng P holds A in rng P & B in rng P & A 'U' B in rng P proof let P be complete PNPair; assume A1: untn(A,B) in rng P; tau rng P = rng P by LTLAXIO3:def 11; hence A in rng P & B in rng P & A 'U' B in rng P by A1,LTLAXIO3:22; end; theorem Th9: rng P c= union Subt rng P proof let x be object; assume A1: x in rng P; then reconsider x1 = x as Element of l; A2: x in tau1.x1 & tau1.x1 c= Sub.x1 by LTLAXIO3:6, LTLAXIO3:25; Sub.x1 in Subt rng P by A1; hence thesis by A2,TARSKI:def 4; end; begin definition let F be Subset of [:LTLB_WFF**,LTLB_WFF**:]; func F^ -> Subset of LTLB_WFF equals {P^ where P is Element of [:LTLB_WFF**,LTLB_WFF**:]: P in F}; coherence proof set b = {P^ where P is Element of [:l**,l**:]: P in F}; b c= l proof let x be object; assume x in b; then ex P be PNPair st x = P^ & P in F; hence thesis; end; hence thesis; end; end; registration let F be non empty Subset of [:LTLB_WFF**,LTLB_WFF**:]; cluster F^ -> non empty; coherence proof consider x being object such that A1: x in F by XBOOLE_0:def 1; reconsider x1 = x as PNPair by A1; x1^ in F^ by A1; hence thesis; end; end; registration let F be finite Subset of [:LTLB_WFF**,LTLB_WFF**:]; cluster F^ -> finite; coherence proof set f = the Enumeration of F; deffunc d(Nat) = (f/.$1)^; consider g be FinSequence of l such that A1: len g = len f & for j be Nat st j in dom g holds g.j = d(j) from FINSEQ_2:sch 1; F^c= rng g proof let x be object; assume x in F^; then consider P such that A2: P^ = x and A3: P in F; A4: P in rng f by RLAFFIN3:def 1,A3; then A5: P .. f in dom f by FINSEQ_4:20; then A6: f/.(P .. f) = f.(P .. f) by PARTFUN1:def 6 .= P by FINSEQ_4:19,A4; A7: P .. f in dom g by A5, A1,FINSEQ_3:29; then g.(P .. f) in rng g by FUNCT_1:3; hence thesis by A1,A7,A6,A2; end; hence F^ is finite; end; end; theorem Th10: for F,G be Subset of [:LTLB_WFF**,LTLB_WFF**:] holds (F \/ G)^ = F^ \/ G^ proof let F,G be Subset of [:l**,l**:]; hereby let x be object; assume x in (F \/ G)^; then consider P such that A1: x = P^ and A2: P in F \/ G; P in F or P in G by A2,XBOOLE_0:def 3; then x in F^ or x in G^ by A1; hence x in F^ \/ G^ by XBOOLE_0:def 3; end; let x be object; assume A3: x in F^ \/ G^; per cases by A3,XBOOLE_0:def 3; suppose x in F^; then consider P such that A4: x = P^ and A5: P in F; P in F \/ G by A5,XBOOLE_0:def 3; hence x in (F \/ G)^ by A4; end; suppose x in G^; then consider P such that A6: x = P^ and A7: P in G; P in F \/ G by A7,XBOOLE_0:def 3; hence x in (F \/ G)^ by A6; end; end; theorem Th11: {[<*>LTLB_WFF,<*>LTLB_WFF]}^ = {TVERUM '&&' TVERUM} proof set Q = [<*>l,<*>l],t = TVERUM; hereby let x be object; assume x in {Q}^; then consider P such that A1: x = P^ and A2: P in {Q}; P^ = t '&&' t by A2,TARSKI:def 1,LTLAXIO3:27; hence x in {t '&&' t} by A1,TARSKI:def 1; end; let x be object; assume x in {t '&&' t}; then A3: x = t '&&' t by TARSKI:def 1; Q in {Q} by TARSKI:def 1; hence x in {Q}^ by LTLAXIO3:27,A3; end; definition let F be finite Subset of LTLB_WFF; func comp F -> non empty finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals {Q where Q is PNPair: rng Q = tau F & rng Q`1 misses rng Q`2}; coherence proof set c = {Q where Q is PNPair: rng Q = tau F & rng Q`1 misses rng Q`2}, tf = tau F, f = the Enumeration of tf, x = [f,<*>l]; A1: c c= [:tf**,tf**:] proof let x be object; assume x in c; then consider Q such that A2: x = Q and A3: rng Q = tau F and rng Q`1 misses rng Q`2; consider y,z being object such that A4: y in l** & z in l** and A5: Q = [y,z] by ZFMISC_1:def 2; reconsider y,z as one-to-one FinSequence of l by A4,LTLAXIO3:def 2; rng y = rng Q`1 by A5; then reconsider y as one-to-one FinSequence of tf by XBOOLE_1:7,A3,FINSEQ_1: def 4; rng z = rng Q`2 by A5; then reconsider z as one-to-one FinSequence of tf by XBOOLE_1:7,A3,FINSEQ_1: def 4; y in tf** & z in tf** by LTLAXIO3:def 2; hence thesis by ZFMISC_1:def 2,A5,A2; end; rng x`2 = {}; then A6: rng x`1 misses rng x`2; rng x = tf \/ rng <*>l by RLAFFIN3:def 1 .= tf; then x in c by A6; hence c is non empty finite Subset of [:l**,l**:] by A1,XBOOLE_1:1; end; end; registration let F be finite Subset of LTLB_WFF; cluster -> complete for Element of (comp F); coherence proof let x be Element of comp F; x in comp F; then ex Q st Q = x & rng Q = tau F & rng Q`1 misses rng Q`2; then tau rng x = rng x by LTLAXIO3:17; hence x is complete; end; end; theorem Th12: comp {}LTLB_WFF = {[<*>LTLB_WFF,<*>LTLB_WFF]} proof hereby let x be object; assume x in comp {}l; then consider Q such that A1: Q = x and A2: rng Q = tau {}l and rng (Q `1) misses rng (Q `2); rng Q`1 = {}l by A2; then A3: Q`1 = <*>l by RELAT_1:41; rng Q`2 = {}l by A2; then A4: Q`2 = <*>l by RELAT_1:41; ex z,y be object st z in l** & y in l** & Q = [z,y] by ZFMISC_1:def 2; then x = [<*>l,<*>l] by A1,A3,A4; hence x in {[<*>l,<*>l]} by TARSKI:def 1; end; let x be object; set Q = [<*>l,<*>l]; assume x in {Q}; then A5: x = Q by TARSKI:def 1; A6: rng Q`1 misses rng Q`2; rng Q = tau {}l; hence x in comp {}l by A6,A5; end; definition let P,Q; pred Q is_completion_of P means rng P`1 c= rng Q`1 & rng P`2 c= rng Q`2 & tau rng P = rng Q; end; theorem Th13: Q is_completion_of P implies Q is complete by LTLAXIO3:17; definition let P; func comp P -> finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals {Q where Q is consistent PNPair: Q is_completion_of P}; coherence proof set c = {Q where Q is consistent PNPair: Q is_completion_of P}, F = tau rng P; A1: c c= [:F**,F**:] proof let x be object; assume x in c; then consider Q be consistent PNPair such that A2: x = Q and A3: Q is_completion_of P; consider y,z being object such that A4: y in l** & z in l** and A5: Q=[y,z] by ZFMISC_1:def 2; reconsider y,z as one-to-one FinSequence of l by A4,LTLAXIO3:def 2; A6: F = rng Q by A3 .= rng y \/ rng z by A5; then z is one-to-one FinSequence of F by XBOOLE_1:7,FINSEQ_1:def 4; then A7: z in F** by LTLAXIO3:def 2; y is one-to-one FinSequence of F by A6, XBOOLE_1:7,FINSEQ_1:def 4; then y in F** by LTLAXIO3:def 2; hence x in [:F**,F**:] by A7,ZFMISC_1:def 2,A5,A2; end; c c= [:l**,l**:] proof let x be object; assume x in c; then ex Q be consistent PNPair st x = Q & Q is_completion_of P; hence x in [:l**,l**:]; end; hence thesis by A1; end; end; registration let P be consistent PNPair; cluster comp P -> non empty; coherence proof consider Q be consistent PNPair such that A1: rng P`1 c= rng Q`1 & rng P`2 c= rng Q`2 & tau rng P = rng Q by LTLAXIO3:34; Q is_completion_of P by A1; then Q in {R where R is consistent PNPair: R is_completion_of P}; hence thesis; end; end; registration let P be consistent PNPair; cluster -> consistent for Element of comp P; coherence proof let x be Element of comp P; x in comp P; then ex Q be consistent PNPair st x = Q & Q is_completion_of P; hence x is consistent; end; end; definition let X be Subset of [:LTLB_WFF**,LTLB_WFF**:]; func comp X -> Subset of [:LTLB_WFF**,LTLB_WFF**:] equals union {comp P where P is Element of [:LTLB_WFF**,LTLB_WFF**:]: P in X}; coherence proof set a = {comp P where P is Element of pairs : P in X}; a c= bool pairs proof let x be object; assume x in a; then ex P st x = comp P & P in X; hence thesis; end; then reconsider a1 = a as Subset-Family of pairs; union a1 is Subset of pairs; hence union a is Subset of pairs; end; end; registration let X be finite Subset of [:LTLB_WFF**,LTLB_WFF**:]; cluster comp X -> finite; coherence proof deffunc F(PNPair) = comp $1; set a = {F(P) where P is Element of pairs : P in X}; A1: a is finite-membered proof let x; assume x in a; then ex P st x = F(P) & P in X; hence x is finite; end; A2: a c= bool pairs proof let x be object; assume x in a; then ex P st x = comp P & P in X; hence thesis; end; A3: X is finite; a is finite from FRAENKEL:sch 21(A3);then reconsider a1 = a as finite finite-membered Subset-Family of pairs by A2,A1; union a1 is finite; hence thesis; end; end; theorem Th14: for X be non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):] st Q in X holds comp Q c= comp X proof let X be non empty Subset of pairs; assume Q in X; then A1: comp Q in {comp T where T is PNPair: T in X}; let x be object; assume x in comp Q; hence thesis by A1,TARSKI:def 4; end; theorem Th15: for F be non empty finite Subset of LTLB_WFF ex p st p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} proof let F be non empty finite Subset of l; set G = {A where A is Element of l: A in tau F & A is conditional}; A1: G c= tau F proof let x be object; assume x in G; then ex A st A = x & A in tau F & A is conditional; hence thesis; end; A2: G is FinSequenceSet of NAT proof let x be object; assume x in G; then ex A st A = x & A in tau F & A is conditional; hence thesis by Th2; end; per cases; suppose A3: G = {}; A4: F is without_implication proof assume not F is without_implication; then consider p such that A5: p in F & p is conditional; F c= tau F by LTLAXIO3:16; then p in G by A5; hence contradiction by A3; end; consider p be object such that A6: p in F by XBOOLE_0:def 1; reconsider p as Element of l by A6; set Fp = (tau F) \ {p}; Fp c= tau F by XBOOLE_1:36; then A7: Fp c= F by LTLAXIO3:18,A4; A8: tau Fp c= Fp proof let x be object; assume x in tau Fp; then consider A such that A9: A in Fp and A10: x in tau1.A by LTLAXIO3:def 5; x in {A} by A7,A9,A4,A10,LTLAXIO3:5; hence thesis by TARSKI:def 1,A9; end; Fp c= tau Fp & p in tau F by LTLAXIO3:16, A4,A6,LTLAXIO3:18; hence thesis by A8,XBOOLE_0:def 10; end; suppose G <> {}; then reconsider G as non empty finite FinSequenceSet of NAT by A2,A1; consider A be FinSequence such that A11: A in G and A12: for B be FinSequence st B in G holds len B <= len A by Th1; set Fp = (tau F) \ {A}; A13: Fp c= tau F by XBOOLE_1:36; A14: tau Fp c= Fp proof let x be object; assume x in tau Fp; then consider p such that A15: p in Fp and A16: x in tau1.p by LTLAXIO3:def 5; A17: not p in {A} by XBOOLE_0:def 5,A15; then A18: p <> A by TARSKI:def 1; x <> A proof per cases; suppose p is conditional; then p in G by A15,A13; then A19: len A >= len p by A12; per cases; suppose x = p; hence thesis by A17,TARSKI:def 1; end; suppose x <> p; hence thesis by LTLAXIO3:11,A16,A19; end; end; suppose not p is conditional; then x in {p} by LTLAXIO3:5,A16; hence thesis by TARSKI:def 1,A18; end; end; then A20: not x in {A} by TARSKI:def 1; tau1.p c= tau F by LTLAXIO3:23, A15,A13; hence thesis by A20,XBOOLE_0:def 5,A16; reconsider x1 = x as Element of l by A16; end; Fp c= tau Fp & ex q st q = A & q in tau F & q is conditional by LTLAXIO3: 16, A11; hence thesis by A14,XBOOLE_0:def 10; end; end; theorem Th16: for F be finite Subset of LTLB_WFF,f be FinSequence of LTLB_WFF st rng f = (comp F)^ holds {}LTLB_WFF |- 'not' ((con nega f)/.(len con nega f)) proof let F be finite Subset of l,f be FinSequence of l; defpred P[Nat] means for F be finite Subset of l st card tau F = $1 holds (for f be FinSequence of l st rng f = (comp F)^ holds {}l |- alt(f)); assume A1: rng f = (comp F)^; A2: card tau F = card tau F; A3: now let k be Nat; assume A4: P[k]; thus P[k+1] proof let G be finite Subset of l; assume A5: card tau G = k+1; then reconsider H = G as non empty finite Subset of l; let g be FinSequence of l; consider A such that A6: A in tau H and A7: tau ((tau H) \ {A}) = (tau H) \ {A} by Th15; set Fp = tau H \ {A}; consider ff be FinSequence such that A8: rng ff = comp Fp and ff is one-to-one by FINSEQ_4:58; reconsider ff as FinSequence of [:l**,l**:] by A8,FINSEQ_1:def 4; deffunc form1(Nat) = [((ff/.$1)`1)^^<*A*>,((ff/.$1)`2)]^; deffunc form2(Nat) = [((ff/.$1)`1),((ff/.$1)`2)^^<*A*>]^; consider ff1 be FinSequence of l such that A9: len ff1 = len ff & for i be Nat st i in dom ff1 holds ff1/.i = form1(i) from FINSEQ_4:sch 2; consider ff2 be FinSequence of l such that A10: len ff2 = len ff & for i be Nat st i in dom ff2 holds ff2/.i = form2(i) from FINSEQ_4:sch 2; set fl = ff1^ff2; A11: now let i be Nat; set Q = ff/.i; assume i in dom ff1 or i in dom ff2; then i in dom ff by A9,A10,FINSEQ_3:29; then Q in comp Fp by PARTFUN2:2,A8; then ex R st R = Q & rng R = tau Fp & rng R`1 misses rng R`2; hence rng Q = tau Fp & rng Q`1 misses rng Q`2; end; tau Fp misses {A} by XBOOLE_1:79, A7; then A12: tau Fp misses rng <*A*> by FINSEQ_1:38; A13: now let i be Nat; set Q = ff/.i; assume i in dom ff1; then A14: rng Q misses rng <*A*> by A12,A11; hence rng Q`1 misses rng <*A*> by XBOOLE_1:7,XBOOLE_1:63; thus rng Q`2 misses rng <*A*> by XBOOLE_1:7,A14,XBOOLE_1:63; end; A15: now let i be Nat; set Q = ff/.i; assume i in dom ff2; then A16: rng Q misses rng <*A*> by A12,A11; hence rng Q`2 misses rng <*A*> by XBOOLE_1:7,XBOOLE_1:63; thus rng Q`1 misses rng <*A*> by XBOOLE_1:7,A16,XBOOLE_1:63; end; A17: rng fl c= (comp G)^ proof let x be object; assume x in rng fl; then A18: x in rng ff1 \/ rng ff2 by FINSEQ_1:31; per cases by A18,XBOOLE_0:def 3; suppose A19: x in rng ff1; set i = x .. ff1,Q = ff/.i,P1 = [(Q`1)^^<*A*>,(Q`2)]; A20: i in dom ff1 by A19,FINSEQ_4:20; then A21: rng Q`1 misses rng <*A*> by A13; rng Q`2 misses rng <*A*> by A13,A20; then A22: rng P1`2 misses {A} by FINSEQ_1:38; A23: rng P1`1 = rng ((Q`1)^<*A*>) by LTLAXIO3:def 3,A21 .= rng Q`1 \/ rng <*A*> by FINSEQ_1:31 .= rng Q`1 \/ {A} by FINSEQ_1:38; rng Q`1 misses rng Q`2 by A11,A20; then A24: rng P1`1 misses rng P1`2 by XBOOLE_1:70,A22,A23; rng P1 = {A} \/ rng Q by XBOOLE_1:4,A23 .= {A} \/ tau Fp by A11,A20 .= tau G by XBOOLE_1:45, ZFMISC_1:31,A6,A7; then A25: P1 in comp G by A24; x = ff1/.i by FINSEQ_5:38,A19 .= P1^ by A9, A19,FINSEQ_4:20; hence x in (comp G)^ by A25; end; suppose A26: x in rng ff2; set i = x .. ff2,Q = ff/.i,P1 = [(Q`1),(Q`2)^^<*A*>]; A27: i in dom ff2 by A26,FINSEQ_4:20; then A28: rng Q`2 misses rng <*A*> by A15; rng Q`1 misses rng <*A*> by A15,A27; then A29: rng P1`1 misses {A} by FINSEQ_1:38; A30: rng P1`2 = rng ((Q`2)^<*A*>) by LTLAXIO3:def 3,A28 .= rng Q`2 \/ rng <*A*> by FINSEQ_1:31 .= rng Q`2 \/ {A} by FINSEQ_1:38; rng Q`2 misses rng Q`1 by A11,A27; then A31: rng P1`1 misses rng P1`2 by XBOOLE_1:70,A29,A30; rng P1 = {A} \/ rng Q by XBOOLE_1:4,A30 .= {A} \/ tau Fp by A11,A27 .= tau G by XBOOLE_1:45, ZFMISC_1:31,A6,A7; then A32: P1 in comp G by A31; x = ff2/.i by FINSEQ_5:38,A26 .= P1^ by A10, A26,FINSEQ_4:20; hence x in (comp G)^ by A32; end; end; assume A33: rng g = (comp G)^; alt(fl) => (alt(g)) is ctaut proof let h be Function of l,BOOLEAN; set v = VAL h; A34: v.alt(g) = 1 or v.alt(g) = 0 by XBOOLEAN:def 3; A35: now assume that A36: v.alt(fl) = 1 and A37: v.alt(g) = 0; per cases; suppose len fl = 0; then len nega fl = 0 by LTLAXIO2:def 4; then con nega fl = <*TVERUM*> by LTLAXIO2:def 2; then alt(fl) = 'not' (<*TVERUM*>/.1) by FINSEQ_1:39 .= 'not' TVERUM by FINSEQ_4:16; then v.alt(fl) = v.TVERUM => v.TFALSUM by LTLAXIO1:def 15 .= TRUE => v.TFALSUM by LTLAXIO2:4; hence contradiction by A36,LTLAXIO1:def 15; end; suppose len fl > 0; v.kon(nega fl) => v.TFALSUM = 1 by A36,LTLAXIO1:def 15; then v.kon(nega fl) => FALSE = 1 by LTLAXIO1:def 15; then consider i be Nat such that A38: i in dom nega fl and A39: not v.((nega fl)/.i) = 1 by LTLAXIO2:19; reconsider i1 = i as Element of NAT by ORDINAL1:def 12; len fl = len nega fl by LTLAXIO2:def 4; then A40: i1 in dom fl by FINSEQ_3:29,A38; then A41: not v.('not' (fl/.i1)) = 1 by LTLAXIO2:8,A39; set j = (fl/.i1) .. g; v.kon(nega g) => v.TFALSUM = 0 by A37,LTLAXIO1:def 15; then A42: v.kon(nega g) => FALSE = 0 by LTLAXIO1:def 15; A43: fl/.i1 in rng fl by PARTFUN2:2,A40; then A44: j in dom g by A17,A33,FINSEQ_4:20; then j <= len g by FINSEQ_3:25; then A45: j <= len nega g by LTLAXIO2:def 4; 1 <= j by A44,FINSEQ_3:25; then A46: j in dom nega g by A45,FINSEQ_3:25; (nega g)/.j = 'not' (g/.j) by LTLAXIO2:8,A44 .= 'not' (fl/.i1) by FINSEQ_5:38, A43,A17,A33; hence contradiction by A42,A46,LTLAXIO2:19, A41; end; end; thus v.(alt(fl) => alt(g)) = v.alt(fl) => v.alt(g) by LTLAXIO1:def 15 .= 1 by A35,A34, XBOOLEAN:def 3; end; then alt(fl) => alt(g) in LTL_axioms by LTLAXIO1:def 17; then A47: {}l |- alt(fl) => alt(g) by LTLAXIO1:42; deffunc dash(Nat)= (ff/.$1)^; consider fk be FinSequence of l such that A48: len fk = len ff & for i be Nat st i in dom fk holds fk/.i = dash(i) from FINSEQ_4:sch 2; A49: now let g; set v = VAL g; assume v.alt(fk) = 1; then v.kon(nega fk) => v.TFALSUM = 1 by LTLAXIO1:def 15; then v.kon(nega fk) => FALSE = 1 by LTLAXIO1:def 15; then consider i be Nat such that A50: i in dom nega fk and A51: not v.((nega fk)/.i) = 1 by LTLAXIO2:19; reconsider i1 = i as Element of NAT by ORDINAL1:def 12; A52: 1 <= i1 by FINSEQ_3:25,A50; i1 <= len nega fk by FINSEQ_3:25,A50; then A53: i1 <= len fk by LTLAXIO2:def 4; (nega fk)/.i = (nega fk).i1 by A50,PARTFUN1:def 6 .= 'not' (fk/.i1) by LTLAXIO2:def 4,A53,A52; then A54: v.((nega fk)/.i) = v.(fk/.i1) => v.TFALSUM by LTLAXIO1:def 15 .= v.(fk/.i1) => FALSE by LTLAXIO1:def 15; A55: v.(fk/.i1) = v.((ff/.i1)^) by A53,FINSEQ_3:25,A52,A48 .= v.(kon((ff/.i1)`1)) '&' v.kon(nega ((ff/.i1)`2)) by LTLAXIO1:31; now dom nega ff1 c= dom ((nega ff1)^(nega ff2)) by FINSEQ_1:26; then A56: dom nega ff1 c= dom nega fl by LTLAXIO2:16; assume v.alt(fl) = 0; then v.kon(nega fl) => v.TFALSUM = 0 by LTLAXIO1:def 15; then A57: v.kon(nega fl) => FALSE = 0 by LTLAXIO1:def 15; per cases by XBOOLEAN:def 3; suppose A58: v.A = 1; i1 <= len nega ff1 by A9,A48,A53,LTLAXIO2:def 4; then A59: i in dom nega ff1 by A52,FINSEQ_3:25; set a = ((ff/.i1)`1)^^<*A*>, b = (ff/.i1)`2; i1 in dom ff1 by A52, A9,A48,A53,FINSEQ_3:25; then rng ((ff/.i1)`1) misses rng <*A*> by A13; then A60: a = ((ff/.i1)`1)^<*A*> by LTLAXIO3:def 3; A61: (nega fl)/.i1 = ((nega ff1)^(nega ff2))/.i by LTLAXIO2:16 .= (nega ff1)/.i by FINSEQ_4:68,A59 .= (nega ff1).i1 by PARTFUN1:def 6,A59 .= 'not' (ff1/.i1) by LTLAXIO2:def 4, A52, A9,A48,A53; A62: 1 = v.((nega fl)/.i1) by A57, A59,A56,LTLAXIO2:19 .= v.(ff1/.i1) => v.TFALSUM by LTLAXIO1:def 15,A61 .= v.(ff1/.i1) => FALSE by LTLAXIO1:def 15; v.(ff1/.i1) = v.([a,b]^) by A9, A52,A48,A53,FINSEQ_3:25 .= v.kon(a) '&' v.kon(nega b) by LTLAXIO1:31 .= v.kon((ff/.i1)`1) '&' v.kon(<*A*>) '&' v.kon(nega b) by LTLAXIO2:17,A60 .= v.kon((ff/.i1)`1) '&' v.A '&' v.kon(nega b) by LTLAXIO2:11 .= 1 by A54, A51,XBOOLEAN:def 3,A58,A55; hence contradiction by A62; end; suppose A63: v.A = 0; set b = ((ff/.i1)`2)^^<*A*>, a = (ff/.i1)`1; i1 in dom ff2 by A52, A53, A10,A48,FINSEQ_3:25;then rng ((ff/.i1)`2) misses rng <*A*> by A15;then A64: nega (((ff/.i1)`2)^<*A*>) = (nega (((ff/.i1)`2)))^(nega (<*A*>)) & b = ((ff /.i1)`2)^<*A*> by LTLAXIO2:16,LTLAXIO3:def 3; nega <*A*> = <*'not' A*> by LTLAXIO2:14; then v.kon(nega <*A*>) = v.('not' A) by LTLAXIO2:11 .= v.A => v.TFALSUM by LTLAXIO1:def 15 .= 1 by A63;then A65: v.kon(nega b) = v.kon((nega ((ff/.i1)`2))) '&' TRUE by A64,LTLAXIO2:17; reconsider j = len ff1 + i1 as Element of NAT; A66: j = len nega ff1 + i1 by LTLAXIO2:def 4; i1 <= len nega ff2 by A53, A10,A48,LTLAXIO2:def 4; then A67: i1 in dom nega ff2 by FINSEQ_3:25, A52; A68: j in dom fl by FINSEQ_1:28, A52, A53, A10,A48,FINSEQ_3:25; then j <= len fl by FINSEQ_3:25; then A69: j <= len nega fl by LTLAXIO2:def 4; A70: (nega fl)/.j = ((nega ff1)^(nega ff2))/.j by LTLAXIO2:16 .= (nega ff2)/.i1 by FINSEQ_4:69,A67,A66 .= (nega ff2).i1 by PARTFUN1:def 6,A67 .= 'not' (ff2/.i1) by LTLAXIO2:def 4, A52, A53, A10,A48; 1 <= j by A68,FINSEQ_3:25; then j in dom nega fl by A69,FINSEQ_3:25; then A71: 1 = v.((nega fl)/.j) by A57,LTLAXIO2:19 .= v.(ff2/.i1) => v.TFALSUM by LTLAXIO1:def 15,A70 .= v.(ff2/.i1) => FALSE by LTLAXIO1:def 15; v.(ff2/.i1) = v.([a,b]^) by A10, A52, A53,A48,FINSEQ_3:25 .= v.kon(a) '&' v.kon(nega b) by LTLAXIO1:31 .= 1 by A54, A51,XBOOLEAN:def 3,A55,A65; hence contradiction by A71; end; end; hence v.alt(fl) = 1 by XBOOLEAN:def 3; end; alt(fk) => (alt(fl)) is ctaut proof let g; set v = VAL g; now assume v.(alt(fk) => (alt(fl))) = 0; then A72: v.alt(fk) => v.alt(fl) = 0 by LTLAXIO1:def 15; v.alt(fl) = 1 or v.alt(fl) = 0 by XBOOLEAN:def 3; hence contradiction by A72,A49; end; hence v.(alt(fk) => (alt(fl))) = 1 by XBOOLEAN:def 3; end; then alt(fk) => (alt(fl)) in LTL_axioms by LTLAXIO1:def 17; then A73: {}l |- alt(fk) => (alt(fl)) by LTLAXIO1:42; A74: rng fk = (comp Fp)^ proof hereby let x be object; assume A75: x in rng fk; then reconsider x1 = x as Element of l; set i = x1 .. fk; i in dom fk by A75,FINSEQ_4:20; then i in dom ff by A48,FINSEQ_3:29; then A76: ff/.i in comp Fp by A8,PARTFUN2:2; x1 = fk/.i by A75,FINSEQ_5:38 .= (ff/.i)^ by A48, A75,FINSEQ_4:20; hence x in (comp Fp)^ by A76; end; let x be object; assume x in (comp Fp)^; then consider P1 be PNPair such that A77: x = P1^ and A78: P1 in comp Fp; set i = P1 .. ff; i in dom ff by FINSEQ_4:20, A8,A78; then A79: i in dom fk by FINSEQ_3:29,A48; then fk/.i = (ff/.i)^ by A48 .= x by A77,FINSEQ_5:38, A8,A78; hence x in rng fk by PARTFUN2:2,A79; end; card tau Fp = k by STIRL2_1:55,A6,A7,A5; then {}l |- alt(fk) by A74,A4; then {}l |- alt(fl) by A73,LTLAXIO1:43; hence {}l |- alt(g) by A47,LTLAXIO1:43; end; end; A80: P[0] proof let F be finite Subset of l; assume card tau F = 0; then A81: F = {}l; let f be FinSequence of l; assume A82: rng f = (comp F)^; then A83: f/.1 in rng f by FINSEQ_6:42,RELAT_1:38; A84: 1 in dom f by A82,FINSEQ_3:32; alt(f) is ctaut proof let g; set v = VAL g; v.(f/.1) = v.(TVERUM '&&' TVERUM) by TARSKI:def 1,Th11,A82,Th12,A81,A83 .= v.TVERUM '&' v.TVERUM by LTLAXIO1:31 .= 1 by LTLAXIO2:4; hence v.alt(f) = 1 by XBOOLEAN:def 3,LTLAXIO2:20,A84; end; then alt(f) in LTL_axioms by LTLAXIO1:def 17; hence {}l |- alt(f) by LTLAXIO1:42; end; for k be Nat holds P[k] from NAT_1:sch 2(A80,A3); hence {}l |- alt(f) by A2,A1; end; theorem Th17: for P be consistent PNPair,f be FinSequence of LTLB_WFF st rng f = (comp P)^ holds {}LTLB_WFF |- P^ => 'not' ((con nega f)/.(len con nega f)) proof let P be consistent PNPair,f be FinSequence of l; set c = comp rng P; defpred P1a[PNPair] means rng P`1 c= rng $1`1 & rng P`2 c= rng $1`2; defpred P1[PNPair] means $1 is consistent & P1a[$1]; defpred P2[PNPair] means not rng P`1 misses rng $1`2 or not rng P`2 misses rng $1`1; set c1 = {Pg where Pg is Element of c: P1[Pg]},c2 = c \ c1; A1: c1 c= c from FRAENKEL:sch 10; A2: c1 = comp P proof hereby let x be object; assume x in c1; then consider Pg be Element of c such that A3: Pg = x and A4: P1[Pg]; reconsider Pg as consistent PNPair by A4; Pg in c;then ex Q st Q = Pg & rng Q = tau rng P & rng (Q `1) misses rng (Q `2); then Pg is_completion_of P by A4; hence x in comp P by A3; end; let x be object; assume x in comp P; then consider Q be consistent PNPair such that A5: Q = x and A6: Q is_completion_of P; rng Q`1 misses rng Q `2 & rng Q = tau rng P by LTLAXIO3:30,A6; then Q in c; then reconsider Q as Element of c; P1[Q] by A6; hence x in c1 by A5; end; reconsider c1 as finite Subset of [:l**,l**:] by A1,XBOOLE_1:1; A7: c = c1 \/ c2 by XBOOLE_1:45,A1; consider f2 be FinSequence such that A8: rng f2 = c2^ and f2 is one-to-one by FINSEQ_4:58; reconsider f2 as FinSequence of l by A8,FINSEQ_1:def 4; set r = kon(nega (f^f2)),s = kon(nega f),t = kon(nega f2); assume A9: rng f = (comp P)^; A10: now let x be PNPair; assume A11: x in c2; then reconsider x1 = x as Element of c by XBOOLE_0:def 5; assume P1[x]; then x1 in c1; hence contradiction by A11,XBOOLE_0:def 5; end; A12: now let pi be PNPair; assume A13: pi in c2; then pi in comp rng P by XBOOLE_0:def 5;then A14: ex Q st Q = pi & rng Q = tau rng P & rng Q`1 misses rng Q`2; per cases by A10,A13; suppose A15: pi is Inconsistent; 'not' (pi^) => (P^ => 'not' (pi^)) is ctaut by LTLAXIO2:33;then 'not' (pi^) => (P^ => 'not' (pi^)) in LTL_axioms by LTLAXIO1:def 17; then A16: {}l |- 'not' (pi^) => (P^ => 'not' (pi^)) by LTLAXIO1:42; {}l |- 'not' (pi^) by A15; hence {}l |- P^ => 'not' (pi^) by A16,LTLAXIO1:43; end; suppose A17: not P1a[pi]; A18: now per cases by A17; suppose not rng P`1 c= rng pi`1; then consider x being object such that A19: x in rng P`1 and A20: not x in rng pi`1; rng P`1 c= rng P by XBOOLE_1:7; then rng P c= tau rng P & x in rng P by LTLAXIO3:16,A19; then x in rng pi`2 by A14,XBOOLE_0:def 3,A20; then x in rng P`1 /\ rng pi`2 by XBOOLE_0:def 4,A19; hence P2[pi] by XBOOLE_0:def 7; end; suppose not rng P`2 c= rng pi`2; then consider x being object such that A21: x in rng P`2 and A22: not x in rng pi`2; rng P`2 c= rng P by XBOOLE_1:7; then rng P c= tau rng P & x in rng P by LTLAXIO3:16,A21; then x in rng pi`1 by A14,XBOOLE_0:def 3,A22; then x in rng P`2 /\ rng pi`1 by XBOOLE_0:def 4,A21; hence P2[pi] by XBOOLE_0:def 7; end; end; A23: now per cases by A18; suppose A24: not rng P`1 misses rng pi`2; set Q1 = [P`1,pi`2],p = kon(Q1`1),q = kon(nega Q1`2); not rng Q1`1 misses rng Q1`2 by A24; then Q1 is Inconsistent by LTLAXIO3:30; then A25: {}l |- 'not' (Q1^); A26: 'not' (kon(P`1) '&&' kon(nega pi`2)) => 'not' (P^ '&&' (pi^)) is ctaut by LTLAXIO2:42; 'not' (Q1^) => 'not' (P^ '&&' (pi^)) in LTL_axioms by A26,LTLAXIO1:def 17;then {}l |- 'not' (Q1^) => 'not' (P^ '&&' (pi^)) by LTLAXIO1:42; hence {}l |- 'not' (P^ '&&' (pi^)) by LTLAXIO1:43,A25; end; suppose A27: not rng P`2 misses rng pi`1; set Q2 = [pi`1,P`2],p = kon(Q2`1),q = kon(nega Q2`2); not rng Q2`2 misses rng Q2`1 by A27; then Q2 is Inconsistent by LTLAXIO3:30; then A28: {}l |- 'not' (Q2^); A29: 'not' (kon(pi`1) '&&' kon(nega P`2)) => 'not' (P^ '&&' (pi^)) is ctaut by LTLAXIO2:41; 'not' (Q2^) => 'not' (P^ '&&' (pi^)) in LTL_axioms by A29,LTLAXIO1:def 17;then {}l |- 'not' (Q2^) => 'not' (P^ '&&' (pi^)) by LTLAXIO1:42; hence {}l |- 'not' (P^ '&&' (pi^)) by LTLAXIO1:43,A28; end; end; 'not' (P^ '&&' (pi^)) => (P^ => 'not' (pi^)) is ctaut by LTLAXIO2:37; then 'not' (P^ '&&' (pi^)) => (P^ => 'not' (pi^)) in LTL_axioms by LTLAXIO1:def 17;then {}l |- 'not' (P^ '&&' (pi^)) => (P^ => 'not' (pi^)) by LTLAXIO1:42; hence {}l |- P^ => 'not' (pi^) by LTLAXIO1:43,A23; end; end; A30: for p st p in c2^ holds {}l |- P^ => 'not' p proof let p; assume p in c2^; then ex Q st p = Q^ & Q in c2; hence {}l |- P^ => 'not' p by A12; end; A31: now per cases; suppose A32: len f2 = 0; P^ => TVERUM is ctaut proof let g; set v = VAL g; thus v.(P^ => TVERUM) = v.(P^) => v.TVERUM by LTLAXIO1:def 15 .= v.(P^) => TRUE by LTLAXIO2:4 .= 1; end; then A33: P^ => TVERUM in LTL_axioms by LTLAXIO1:def 17; len nega f2 = 0 by A32,LTLAXIO2:def 4; then nega f2 = {}; hence {}l |- P^ => t by A33,LTLAXIO1:42,LTLAXIO2:10; end; suppose A34: len f2 > 0; set t1 = con nega f2; A35: len nega f2 > 0 by A34,LTLAXIO2:def 4; then reconsider lt1 = len t1 as non zero Nat by LTLAXIO2:def 2; defpred P3[Nat] means $1 <= len t1 implies{}l |- P^ => (t1/.$1); A36: now let k be non zero Nat such that A37: P3[k]; thus P3[k+1] proof set a = t1/.k,b = (nega f2)/.(k+1); reconsider k1 = k as non empty Element of NAT by ORDINAL1:def 12; assume A38: k+1 <= len t1; P^ => a => (P^ => b => (P^ => (a '&&' b))) is ctaut by LTLAXIO2:40; then P^ => a => (P^ => b => (P^ => (a '&&' b))) in LTL_axioms by LTLAXIO1:def 17; then {}l |- P^ => a => (P^ => b => (P^ => (a '&&' b))) by LTLAXIO1:42;then A39: {}l |- P^ => b => (P^ => (a '&&' b)) by LTLAXIO1:43,A38,NAT_1:13,A37; A40: k+1 <= len nega f2 by A38,LTLAXIO2:def 2,A35; then k+1 <= len f2 by LTLAXIO2:def 4; then A41: k1+1 in dom f2 by NAT_1:12,FINSEQ_3:25; then {}l |- P^ => 'not' f2/.(k+1) by PARTFUN2:2,A8,A30; then {}l |- P^ => b by LTLAXIO2:8,A41; then 1 <= k1 & {}l |- P^ => (a '&&' b) by NAT_1:25,A39,LTLAXIO1:43; hence {}l |- P^ => (t1/.(k+1)) by LTLAXIO2:7, NAT_1:13,A40; end; end; A42: P3[1] proof assume 1 <= len t1; 1 <= len f2 by A34,NAT_1:25; then A43: 1 in dom f2 by FINSEQ_3:25; t1/.1 = (nega f2)/.1 by A35,LTLAXIO2:6 .= 'not' f2/.1 by LTLAXIO2:8,A43; hence thesis by PARTFUN2:2,A43,A8,A30; end; for k being non zero Nat holds P3[k] from NAT_1:sch 10(A42, A36 ); then {}l |- P^ => (t1/.lt1); hence {}l |- P^ => t; end; end; A44: nega (f^f2) = (nega f) ^ (nega f2) by LTLAXIO2:16; now let g; set v = VAL g; A45: v.r = FALSE or v.r = TRUE by XBOOLEAN:def 3; A46: v.r = v.s '&' v.t by LTLAXIO2:17,A44; thus v.('not' r => ('not' (s '&&' t))) = v.('not' r) => v.('not' (s '&&' t)) by LTLAXIO1:def 15 .= v.r => v.TFALSUM => (v.('not' (s '&&' t))) by LTLAXIO1:def 15 .= v.r => FALSE => (v.('not' (s '&&' t))) by LTLAXIO1:def 15 .= v.r => FALSE => (v.(s '&&' t) => v.TFALSUM) by LTLAXIO1:def 15 .= v.r => FALSE => (v.(s '&&' t) => FALSE) by LTLAXIO1:def 15 .= 1 by A45,A46,LTLAXIO1:31; end; then 'not' r => ('not' (s '&&' t)) is ctaut;then 'not' r => ('not' (s '&&' t)) in LTL_axioms by LTLAXIO1:def 17; then A47: {}l |- 'not' r => ('not' (s '&&' t)) by LTLAXIO1:42; 'not' (s '&&' t) => (P^ => t => (P^ => 'not' s)) is ctaut by LTLAXIO2:39; then 'not' (s '&&' t) => (P^ => t => (P^ => 'not' s)) in LTL_axioms by LTLAXIO1: def 17; then A48: {}l |- 'not' (s '&&' t) => (P^ => t => (P^ => 'not' s)) by LTLAXIO1: 42; rng (f^f2) = rng f \/ rng f2 by FINSEQ_1:31 .= c^ by A7,Th10, A9,A2,A8; then {}l |- 'not' r by Th16; then {}l |- 'not' (s '&&' t) by A47,LTLAXIO1:43; then {}l |- P^ => t => (P^ => 'not' s) by A48,LTLAXIO1:43; hence {}l |- P^ => 'not' s by LTLAXIO1:43,A31; end; begin definition let X; func untn X -> Subset of LTLB_WFF equals {untn(A,B) where A is Element of LTLB_WFF,B is Element of LTLB_WFF: A 'U' B in X}; coherence proof set c = {untn(A,B) where A is Element of l,B is Element of l: A 'U' B in X}; c c= l proof let x be object; assume x in c; then ex A,B be Element of l st x = untn(A,B) & A 'U' B in X; hence x in l; end; hence thesis; end; end; registration let X be finite Subset of LTLB_WFF; cluster untn X -> finite; coherence proof defpred P[Element of l,Element of l] means ex p,q st $1 = p 'U' q & $2 = untn(p,q); set c = {A where A is Element of l: ex B st P[B,A] & B in X}; A1: untn X = c proof hereby let x be object; assume x in untn X; then ex A,B st x = untn(A,B) & A 'U' B in X; hence x in c; end; let x be object; assume x in c; then ex A st x = A & ex B be Element of l st P[B,A] & B in X; hence x in untn X; end; A2: now let w be Element of l, x,y be Element of l; assume that A3: P[w,x] and A4: P[w,y]; consider p,q such that A5: w = p 'U' q and A6: x = untn(p,q) by A3; consider A,B such that A7: w = A 'U' B and A8: y = untn(A,B) by A4; p = A by A5,A7,HILBERT2:19; hence x = y by A5,A7,HILBERT2:19,A6,A8; end; A9: X is finite; c is finite from FRAENKEL:sch 28(A9,A2); hence thesis by A1; end; end; definition let P; func untn P -> non empty finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals {Q where Q is PNPair: rng Q`1 = untn rng P`1 & rng Q`2 = untn rng P`2}; coherence proof defpred P[PNPair] means rng $1`1 = untn rng P`1 & rng $1`2 = untn rng P`2; set s = untn rng P`1 \/ untn rng P`2; consider f be FinSequence such that A1: rng f = untn rng P`1 and A2: f is one-to-one by FINSEQ_4:58; reconsider f as one-to-one FinSequence of l by A1,A2,FINSEQ_1:def 4; consider g be FinSequence such that A3: rng g = untn rng P`2 and A4: g is one-to-one by FINSEQ_4:58; reconsider g as one-to-one FinSequence of l by A3,A4,FINSEQ_1:def 4; A5: rng [f,g]`1 = untn rng P`1 by A1; A6: {A where A is PNPair: P[A]} c= [:s**,s**:] proof let x be object; assume x in {A where A is PNPair: P[A]}; then consider Q such that A7: x = Q and A8: rng Q`1 = untn rng P`1 and A9: rng Q`2 = untn rng P`2; consider y,z being object such that A10: y in l** & z in l** and A11: Q = [y,z] by ZFMISC_1:def 2; reconsider y,z as one-to-one FinSequence of l by A10,LTLAXIO3:def 2; rng Q`1 c= s by A8,XBOOLE_1:7; then A12: rng y c= s by A11; rng Q`2 c= s by A9,XBOOLE_1:7; then A13: rng z c= s by A11; reconsider y as one-to-one FinSequence of s by A12,FINSEQ_1:def 4; reconsider z as one-to-one FinSequence of s by A13,FINSEQ_1:def 4; y in s** & z in s** by LTLAXIO3:def 2; hence thesis by ZFMISC_1:def 2,A11,A7; end; rng [f,g]`2 = untn rng P`2 by A3; then A14: [f,g] in {A where A is PNPair: P[A]} by A5; {A where A is PNPair: P[A]} c= [:l**,l**:] from FRAENKEL:sch 10; hence thesis by A14, A6; end; end; theorem Th18: for Q be Element of untn P holds {}LTLB_WFF |- P^ => 'X'(Q^) proof let Q be Element of untn P; set p = 'X' kon(Q`1), q = 'X' kon(nega Q`2); Q in untn P;then A1: ex Q1 be PNPair st Q=Q1 & rng Q1`1 = untn rng P`1 & rng Q1`2 = untn rng P `2; now let i be Nat; assume A2: i in dom nex nega Q`2; A3: len nex nega Q`2 = len nega Q`2 by LTLAXIO2:def 5; then len nex nega Q`2 = len Q`2 by LTLAXIO2:def 4; then A4: i in dom Q`2 by FINSEQ_3:29,A2; then Q`2/.i in untn rng P`2 by PARTFUN2:2,A1; then consider A,B such that A5: Q`2/.i = untn(A,B) and A6: A 'U' B in rng P`2; i in dom nega Q`2 by A3,A2,FINSEQ_3:29; then A7: (nex nega Q`2)/.i = 'X' ((nega Q`2)/.i) by LTLAXIO2:9 .= 'X' ('not' (Q`2/.i)) by LTLAXIO2:8,A4; {}l |- 'not' (A 'U' B) => ('X' 'not' untn(A,B)) & {}l |- P^ => 'not' (A 'U' B) by LTLAXIO2:63, LTLAXIO3:29,A6; hence {}l |- P^ => (nex nega Q`2)/.i by A7,LTLAXIO1:47, A5; end; then {}l |- kon(nex nega Q`2) => q & {}l |- P^ => kon(nex nega Q`2) by LTLAXIO2:60,LTLAXIO2:56; then A8: {}l |- P^ => q by LTLAXIO1:47; now let i be Nat; assume A9: i in dom nex Q`1; len Q`1 = len nex Q`1 by LTLAXIO2:def 5; then A10: i in dom Q`1 by A9,FINSEQ_3:29; then Q`1/.i in untn rng P`1 by PARTFUN2:2,A1; then consider A,B such that A11: Q`1/.i = untn(A,B) and A12: A 'U' B in rng P`1; A13: {}l |- P^ => (A 'U' B) by LTLAXIO3:28,A12; (A 'U' B) => (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) in LTL_axioms by LTLAXIO1:def 17;then A14: {}l |- (A 'U' B) => (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) by LTLAXIO1:42; {}l |- (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) => 'X' untn(A,B) by LTLAXIO2:61; then A15: {}l |- (A 'U' B) => 'X' untn(A,B) by LTLAXIO1:47,A14; (nex Q`1)/.i = 'X' untn(A,B) by A11,LTLAXIO2:9,A10; hence {}l |- P^ => (nex Q`1)/.i by A15,LTLAXIO1:47,A13; end;then {}l |- kon(nex Q`1) => p & {}l |- P^ => kon(nex Q`1) by LTLAXIO2:60,56; then A16: {}l |- P^ => p by LTLAXIO1:47; P^ => p => ((P^ => q) => (P^ => (p '&&' q))) is ctaut by LTLAXIO2:40; then P^ => p => ((P^ => q) => (P^ => (p '&&' q))) in LTL_axioms by LTLAXIO1:def 17;then {}l |- P^ => p => ((P^ => q) => (P^ => (p '&&' q))) by LTLAXIO1:42; then {}l |- ((P^ => q) => (P^ => (p '&&' q))) by LTLAXIO1:43,A16; then A17: {}l |- P^ => (p '&&' q) by LTLAXIO1:43,A8; {}l |- (('X' (kon(Q`1))) '&&' ('X' (kon(nega Q`2)))) => ('X' (Q^)) by LTLAXIO1:53; hence {}l |- P^ => 'X'(Q^) by LTLAXIO1:47,A17; end; registration let P be consistent PNPair; cluster -> consistent for Element of untn P; coherence proof let Q be Element of untn P; assume not Q is consistent; then A1: {}l |- 'X' 'not' (Q^) by LTLAXIO1:44; {}l |- P^ => 'X'(Q^) by Th18; then A2: {}l |- (('not' 'X' (Q^)) => 'not' (P^)) by LTLAXIO1:52; ('X' 'not' (Q^)) => ('not' 'X' (Q^)) in LTL_axioms by LTLAXIO1:def 17; then {}l |- ('X' 'not' (Q^)) => ('not' 'X' (Q^)) by LTLAXIO1:42; then {}l |- 'not' 'X' (Q^) by A1,LTLAXIO1:43; hence contradiction by A2,LTLAXIO1:43,LTLAXIO3:def 10; end; end; definition let P; func compn P -> finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals {Q where Q is Element of [:LTLB_WFF**,LTLB_WFF**:]: Q in comp untn P}; coherence proof defpred P1[PNPair] means $1 in comp untn P; deffunc F1(PNPair) = $1; A1: comp untn P is finite; A2: {F1(Q) where Q is Element of pairs: Q in comp untn P} is finite from FRAENKEL: sch 21(A1); {Q where Q is PNPair: P1[Q]} c= [:l**,l**:] from FRAENKEL:sch 10; hence thesis by A2; end; end; registration let P be consistent PNPair; cluster compn P -> non empty; coherence proof consider x being object such that A1: x in untn P by XBOOLE_0:def 1; reconsider x as consistent PNPair by A1; consider y being object such that A2: y in comp x by XBOOLE_0:def 1; reconsider y as PNPair by A2; comp x in {comp Q where Q is Element of pairs: Q in untn P} by A1; then y in comp untn P by A2,TARSKI:def 4; then y in {Q where Q is PNPair: Q in comp untn P}; hence thesis; end; end; registration let P be consistent PNPair; cluster -> consistent for Element of compn P; coherence proof let Q be Element of compn P; Q in compn P; then consider R be PNPair such that A1: R = Q and A2: R in comp untn P; consider x such that A3: R in x and A4: x in {comp S where S is Element of pairs: S in untn P} by TARSKI:def 4,A2; consider S be PNPair such that A5: x = comp S and A6: S in untn P by A4; reconsider S as Element of untn P by A6; reconsider R as Element of comp S by A3,A5; R is consistent; hence Q is consistent by A1; end; end; theorem Th19: Q in compn P & R in untn P implies Q is_completion_of R proof assume that A1: Q in compn P and A2: R in untn P; consider Q1 be PNPair such that A3: Q1 = Q and A4: Q1 in comp untn P by A1; A5: ex R1 be PNPair st R1 = R & rng R1`1 = untn rng P`1 & rng R1 `2 = untn rng P`2 by A2; consider x such that A6: Q1 in x and A7: x in {comp S where S is PNPair:S in untn P} by A4,TARSKI:def 4; consider S be PNPair such that A8: x = comp S and A9: S in untn P by A7; consider Q2 be consistent PNPair such that A10: Q2 = Q1 and A11: Q2 is_completion_of S by A6,A8; A12: ex S1 be PNPair st S1 = S & rng S1`1 = untn rng P`1 & rng S1`2 = untn rng P`2 by A9; tau rng S = rng Q2 by A11; then A13: tau rng R = rng Q by A3,A10,A12,A5; rng R`1 c= rng Q`1 & rng R`2 c= rng Q`2 by A11,A3,A10,A12, A5; hence Q is_completion_of R by A13; end; theorem Th20: Q in compn P implies Q is complete proof assume A1: Q in compn P; then consider Q1 be PNPair such that Q1 = Q and A2: Q1 in comp untn P; consider x such that Q1 in x and A3: x in {comp R where R is PNPair : R in untn P} by A2,TARSKI:def 4; ex R be PNPair st x = comp R & R in untn P by A3; hence Q is complete by Th19,A1,Th13; end; registration let P be consistent PNPair; cluster -> complete for Element of compn P; coherence by Th20; end; theorem Th21: A 'U' B in rng P`2 & Q in compn P implies untn(A,B) in rng Q`2 proof assume that A1: A 'U' B in rng P`2 and A2: Q in compn P; consider Q1 be Element of pairs such that Q = Q1 and A3: Q1 in comp untn P by A2; consider x such that Q1 in x and A4: x in {(comp R) where R is Element of pairs : R in untn P} by TARSKI:def 4,A3; consider R be PNPair such that x = comp R and A5: R in untn P by A4; ex R1 be PNPair st R1 = R & rng R1`1 = untn rng P`1 & rng R1`2 = untn rng P`2 by A5; then A6: untn(A,B) in rng (R`2) by A1; Q is_completion_of R by A5,A2,Th19; then rng (R`2) c= rng (Q`2); hence untn(A,B) in rng Q`2 by A6; end; theorem Th22: A 'U' B in rng P`1 & Q in compn P implies untn(A,B) in rng Q`1 proof assume that A1: A 'U' B in rng P`1 and A2: Q in compn P; consider Q1 be Element of pairs such that Q = Q1 and A3: Q1 in comp untn P by A2; consider x such that Q1 in x and A4: x in {(comp R) where R is Element of pairs : R in untn P} by TARSKI:def 4,A3; consider R be PNPair such that x = comp R and A5: R in untn P by A4; ex R1 be PNPair st R1 = R&rng (R1`1) = untn rng (P`1) & rng (R1`2) = untn rng (P`2) by A5; then A6: untn(A,B) in rng (R`1) by A1; Q is_completion_of R by A5,A2,Th19; then rng (R`1) c= rng (Q`1); hence untn(A,B) in rng Q`1 by A6; end; theorem Th23: R in compn Q & rng Q c= union Subt rng P implies rng R c= union Subt rng P proof assume that A1: R in compn Q and A2: rng Q c= union Subt rng P; consider R1 be PNPair such that A3: R1 = R and A4: R1 in comp untn Q by A1; consider z such that A5: R1 in z and A6: z in {comp S where S is PNPair: S in untn Q} by A4,TARSKI:def 4; consider T be PNPair such that A7: z = comp T and A8: T in untn Q by A6; A9: ex T1 be PNPair st T1 = T & rng T1 `1 = untn rng Q`1 & rng T1`2 = untn rng Q`2 by A8; let x be object; assume A10: x in rng R; ex R2 be consistent PNPair st R2=R1 & R2 is_completion_of T by A7, A5; then x in tau rng T by A3,A10; then consider p such that A11: p in rng T and A12: x in tau1.p by LTLAXIO3:def 5; per cases by XBOOLE_0:def 3, A9,A11; suppose p in untn rng Q`1; then consider A,B such that A13: p = untn(A,B) and A14: A 'U' B in rng (Q`1); set aub = A 'U' B; rng (Q`1) c= rng Q by XBOOLE_1:7; then aub in rng Q by A14; then consider y such that A15: aub in y and A16: y in Subt rng P by A2,TARSKI:def 4; consider q be Element of l such that A17: y = Sub.q and q in rng P by A16; tau1.untn(A,B) c= tau1.untn(A,B) \/ (Sub.A \/ Sub.B) by XBOOLE_1:7;then tau1.untn(A,B) c= tau1.untn(A,B) \/ Sub.A \/ Sub.B by XBOOLE_1:4; then tau1.untn(A,B) c= Sub.aub by LTLAXIO3:def 6; then x in Sub.q by A17,A15,LTLAXIO3:26, A13,A12; hence x in union Subt rng P by A17,A16,TARSKI:def 4; end; suppose p in untn rng Q`2; then consider A,B such that A18: p = untn(A,B) and A19: A 'U' B in rng (Q`2); set aub = A 'U' B; rng (Q`2) c= rng Q by XBOOLE_1:7; then aub in rng Q by A19; then consider y such that A20: aub in y and A21: y in Subt rng P by A2,TARSKI:def 4; consider q be Element of l such that A22: y = Sub.q and q in rng P by A21; tau1.untn(A,B) c= tau1.untn(A,B) \/ (Sub.A \/ Sub.B) by XBOOLE_1:7; then tau1.untn(A,B) c= tau1.untn(A,B) \/ Sub.A \/ Sub.B by XBOOLE_1:4; then tau1.untn(A,B) c= Sub.aub by LTLAXIO3:def 6; then x in Sub.q by A22,A20,LTLAXIO3:26, A18,A12; hence x in union Subt rng P by A22,A21,TARSKI:def 4; end; end; theorem Th24: for P be consistent complete PNPair,Q be Element of compn P st A 'U' B in rng P`2 holds B in rng Q`2 & (A in rng Q`2 or A 'U' B in rng Q`2) proof let P be consistent complete PNPair,Q be Element of compn P; set aub = A 'U' B,nb = 'not' B, na = 'not' A,au = A '&&' aub; ('not' untn(A,B)) => (nb '&&' 'not' au) is ctaut by LTLAXIO2:36;then ('not' untn(A,B)) => (nb '&&' 'not' au) in LTL_axioms by LTLAXIO1:def 17; then A1: {}l |- ('not' untn(A,B)) => (nb '&&' 'not' au) by LTLAXIO1:42; assume aub in rng P`2; then A2: untn(A,B) in rng Q`2 by Th21; then A3: untn(A,B) in rng Q by XBOOLE_0:def 3; then A4: A in rng Q by Th8; {}l |- Q^ => 'not' untn(A,B) by LTLAXIO3:29,A2; then A5: {}l |- Q^ => (nb '&&' 'not' au) by A1,LTLAXIO1:47; (nb '&&' 'not' au) => nb is ctaut by LTLAXIO2:27; then (nb '&&' 'not' au) => nb in LTL_axioms by LTLAXIO1:def 17; then {}l |- (nb '&&' 'not' au) => nb by LTLAXIO1:42; then A6: {}l |- Q^ => nb by LTLAXIO1:47,A5; (nb '&&' 'not' au) => ('not' au) is ctaut by LTLAXIO2:28;then (nb '&&' 'not' au) => ('not' au) in LTL_axioms by LTLAXIO1:def 17; then {}l |- (nb '&&' 'not' au) => ('not' au) by LTLAXIO1:42; then A7: {}l |- Q^ => ('not' au) by LTLAXIO1:47,A5; A8: B in rng Q by A3,Th8; A9: aub in rng Q by A3,Th8; assume A10: not B in rng Q`2 or not (A in rng Q`2 or aub in rng Q`2); per cases by A10; suppose not B in rng Q`2; then B in rng Q`1 by A8,XBOOLE_0:def 3; then {}l |- Q^ => B by LTLAXIO3:28; then {}l |- Q^ => (B '&&' nb) by LTLAXIO2:52,A6; then {}l |- 'not' (Q^) by LTLAXIO2:55; hence contradiction by LTLAXIO3:def 10; end; suppose A11: not A in rng Q`2 & not aub in rng Q`2; then A in rng Q`1 by XBOOLE_0:def 3,A4; then A12: {}l |- Q^ => A by LTLAXIO3:28; aub in rng Q`1 by A11,XBOOLE_0:def 3,A9; then {}l |- Q^ => aub by LTLAXIO3:28; then {}l |- Q^ => au by A12,LTLAXIO2:52; then {}l |- Q^ => (au '&&' ('not' au)) by LTLAXIO2:52,A7; then {}l |- 'not' (Q^) by LTLAXIO2:55; hence contradiction by LTLAXIO3:def 10; end; end; theorem Th25: for P be consistent complete PNPair,Q be Element of compn P st A 'U' B in rng P`1 holds (B in rng Q`1 or A in rng Q`1 & A 'U' B in rng Q`1) proof let P be consistent complete PNPair,Q be Element of compn P; set aub = A 'U' B,nb = 'not' B, na = 'not' A,nu = 'not' aub; assume aub in rng P`1; then A1: untn(A,B) in rng Q`1 by Th22; then A2: untn(A,B) in rng Q by XBOOLE_0:def 3; then A3: A in rng Q by Th8; A4: aub in rng Q by A2,Th8; A5: {}l |- Q^ => untn(A,B) by LTLAXIO3:28,A1; Q^ => untn(A,B) => (Q^ => (na '&&' nb) => ('not' (Q^))) is ctaut by LTLAXIO2: 50;then Q^ => untn(A,B) => (Q^ => (na '&&' nb) => ('not' (Q^))) in LTL_axioms by LTLAXIO1:def 17;then {}l |- Q^ => untn(A,B) => (Q^ => (na '&&' nb) => ('not' (Q^))) by LTLAXIO1:42; then A6: {}l |- Q^ => (na '&&' nb) => ('not' (Q^)) by LTLAXIO1:43,A5; Q^ => untn(A,B) => (Q^ => (nb '&&' nu) => ('not' (Q^))) is ctaut by LTLAXIO2:51;then Q^ => untn(A,B) => (Q^ => (nb '&&' nu) => ('not' (Q^))) in LTL_axioms by LTLAXIO1:def 17;then {}l |- Q^ => untn(A,B) => (Q^ => (nb '&&' nu) => ('not' (Q^))) by LTLAXIO1:42; then A7: {}l |- Q^ => (nb '&&' nu) => ('not' (Q^)) by LTLAXIO1:43,A5; assume that A8: not B in rng Q`1 and A9: not A in rng Q`1 or not aub in rng Q`1; B in rng Q by A2,Th8; then B in rng Q`2 by A8,XBOOLE_0:def 3; then A10: {}l |- Q^ => nb by LTLAXIO3:29; per cases by A9; suppose not A in rng Q`1; then A in rng Q`2 by A3,XBOOLE_0:def 3; then {}l |- Q^ => na by LTLAXIO3:29; then {}l |- Q^ => (na '&&' nb) by LTLAXIO2:52,A10; hence contradiction by LTLAXIO1:43,A6,LTLAXIO3:def 10; end; suppose not aub in rng Q`1; then aub in rng Q`2 by XBOOLE_0:def 3,A4; then {}l |- Q^ => nu by LTLAXIO3:29; then {}l |- Q^ => (nb '&&' nu) by LTLAXIO2:52,A10; hence contradiction by LTLAXIO1:43,A7,LTLAXIO3:def 10; end; end; begin definition let P; mode pnptree of P -> finite-branching DecoratedTree of [:LTLB_WFF**,LTLB_WFF**:] means :Def11: it.{} = P & for t being Element of dom it for w being Element of [:LTLB_WFF**,LTLB_WFF**:] st w = it.t holds succ (it,t) = the Enumeration of compn w; correctness proof deffunc F3(Element of pairs) = the Enumeration of compn $1; ex T being finite-branching DecoratedTree of pairs st T . {} = P & for t being Element of dom T for w being Element of pairs st w = T . t holds succ (T,t) = F3(w) from TREES_9:sch 2; hence thesis; end; end; reserve T for pnptree of P,t for Node of T; definition let P,T,t; redefine func T|t -> pnptree of T.t; correctness proof set k = T|t; A1: dom k = (dom T) | t by TREES_2:def 10; A2: now let u be Element of dom k; reconsider tu = t^u as Element of dom T by A1,TREES_1:def 6; let w be Element of pairs; assume w = k.u; then A3: w = T.(t^u) by A1,TREES_2:def 10; thus succ (k,u) = succ(T,tu) by TREES_9:31 .= the Enumeration of compn w by Def11,A3; end; k.{} = T.t by TREES_9:35; hence thesis by A2,Def11; end; end; theorem Th26: for n being Nat st t^<*n*> in dom T holds T.(t^<*n*>) in compn (T.t) proof let n be Nat; set tn = t^<*n*>; assume A1: t^<*n*> in dom T; dom (succ (T,t)) = dom (t succ) by TREES_9:38;then A2: (succ (T,t)).(n+1) in rng succ (T,t) by TREES_9:39,A1,FUNCT_1:3; A3: succ (T,t) = the Enumeration of compn (T.t) by Def11; T.tn = (succ (T,t)).(n+1) by A1,TREES_9:40; hence T.tn in compn (T.t) by A3,A2,RLAFFIN3:def 1; end; theorem Th27: Q in rng T implies rng Q c= union Subt rng P proof deffunc F(PNPair) = {Sub.A where A is Element of l: A in rng $1}; defpred P1[set] means for Q st Q = T.$1 & $1 in dom T holds rng Q c= union Subt rng P; assume Q in rng T; then consider x being object such that A1: x in dom T and A2: T.x = Q by FUNCT_1:def 3; reconsider x as Element of dom T by A1; A3: now let t be Element of dom T,n be Nat; assume that A4: P1[t] and t^<*n*> in dom T; A5: rng (T.t) c= union Subt rng P by A4; thus P1[t^<*n*>] proof let Q; assume Q = T.(t^<*n*>) & t^<*n*> in dom T; then Q in compn (T.t) by Th26; hence rng Q c= union Subt rng P by Th23,A5; end; end; A6: P1[{}] proof let Q; assume that A7: Q = T.{} and {} in dom T; Q = P by A7,Def11; hence thesis by Th9; end; for t be Element of dom T holds P1[t] from TREES_2:sch 1(A6,A3 ); then rng (T.x) c= union Subt rng P; hence thesis by A2; end; registration let P,T; cluster rng T -> non empty finite; coherence proof set a = union Subt rng P; {} in dom T by TREES_1:22; hence rng T is non empty by FUNCT_1:3; rng T c= [:a**,a**:] proof let x be object; assume A1: x in rng T; then reconsider x1 = x as PNPair; A2: rng x1 c= a by Th27,A1; rng x1`1 c= rng x1 by XBOOLE_1:7;then x1`1 is one-to-one FinSequence of a by XBOOLE_1:1,A2,FINSEQ_1:def 4; then A3: x1`1 in a** by LTLAXIO3:def 2; rng x1`2 c= rng x1 by XBOOLE_1:7;then x1`2 is one-to-one FinSequence of a by XBOOLE_1:1,A2,FINSEQ_1:def 4; then A4: x1`2 in a** by LTLAXIO3:def 2; consider y,z being object such that A5: y in l** & z in l** and A6: x1=[y,z] by ZFMISC_1:def 2; reconsider y,z as one-to-one FinSequence of l by A5,LTLAXIO3:def 2; thus thesis by A3,A4,ZFMISC_1:def 2,A6; end; hence thesis; end; end; registration let P be consistent PNPair; let T be pnptree of P; cluster -> consistent for Element of rng T; coherence proof let y be Element of rng T; defpred P1[set] means for Q st Q = T.$1 & $1 in dom T holds Q is consistent; A1: ex x being object st x in dom T & T.x = y by FUNCT_1:def 3; A2: now let t be Element of dom T,n be Nat; assume that A3: P1[t] and t^<*n*> in dom T; reconsider pQ = T.t as consistent PNPair by A3; thus P1[t^<*n*>] proof let Q; assume Q = T.(t^<*n*>) & t^<*n*> in dom T; then reconsider Q1 = Q as Element of compn pQ by Th26; Q1 is consistent; hence thesis; end; end; A4: P1[{}] by Def11; for t be Element of dom T holds P1[t] from TREES_2:sch 1(A4, A2); hence thesis by A1; end; end; registration let P be consistent complete PNPair; let T be pnptree of P; cluster -> complete for Element of rng T; coherence proof let y be Element of rng T; defpred P1[set] means for Q st Q = T.$1 & $1 in dom T holds Q is complete; A1: ex x being object st x in dom T & T.x = y by FUNCT_1:def 3; A2: now let t be Element of dom T,n be Nat; assume that A3: P1[t] and t^<*n*> in dom T; reconsider Tt = T.t as Element of rng T by FUNCT_1:def 3; reconsider pQ = Tt as consistent complete PNPair by A3; thus P1[t^<*n*>] proof let Q; assume Q = T.(t^<*n*>) & t^<*n*> in dom T; then reconsider Q1 = Q as Element of compn pQ by Th26; Q1 is consistent; hence thesis; end; end; A4: P1[{}] by Def11; for t be Element of dom T holds P1[t] from TREES_2:sch 1(A4, A2); hence thesis by A1; end; end; registration let P be consistent complete PNPair,T be pnptree of P,t be Node of T; cluster T.t -> consistent complete for PNPair; coherence proof reconsider Tt = T.t as Element of rng T by FUNCT_1:3; Tt is consistent; hence thesis; end; end; registration let P be consistent PNPair,T be pnptree of P; let t be Element of dom T; cluster succ t -> non empty; coherence proof reconsider w = T.t as Element of rng T by FUNCT_1:def 3; reconsider w as consistent PNPair; succ (T,t) = the Enumeration of compn w by Def11; then rng succ (T,t) = compn w by RLAFFIN3:def 1; then consider y being object such that A1: y in rng succ (T,t) by XBOOLE_0:def 1; ex x being Element of dom T st y = T.x & x in succ t by TREES_9:42,A1; hence thesis; end; end; definition let P,T; func rngr T -> finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals {T.t where t is Node of T: t <> {}}; correctness proof set r = {T.t where t is Node of T: t <> {}}; r c= rng T proof let x be object; assume x in r; then ex t be Node of T st x = T.t & t <> {}; hence thesis by FUNCT_1:3; end; hence thesis by XBOOLE_1:1; end; end; registration let P be consistent PNPair, T be pnptree of P; cluster rngr T -> non empty; coherence proof reconsider e = {} as Element of dom T by TREES_1:22; consider x being object such that A1: x in succ e by XBOOLE_0:def 1; reconsider x as Element of dom T by A1; ex n being Nat st x = e^<*n*> & e^<*n*> in dom T by A1; then T.x in rngr T; hence thesis; end; end; theorem Th28: R in rng T & Q in untn R implies comp Q c= rngr T proof assume that A1: R in rng T and A2: Q in untn R; let S be object; assume A3: S in comp Q; comp Q c= comp untn R by Th14,A2; then A4: S in compn R by A3; consider t be object such that A5: t in dom T and A6: T.t = R by FUNCT_1:def 3,A1; reconsider t as Element of dom T by A5; succ (T,t) = the Enumeration of compn R by Def11,A6; then S in rng succ (T,t) by RLAFFIN3:def 1,A4; then consider t1 be Element of dom T such that A7: S = T.t1 and A8: t1 in succ t by TREES_9:42; ex n being Nat st t1 = t^<*n*> & t^<*n*> in dom T by A8; hence S in rngr T by A7; end; theorem Th29: for P be consistent complete PNPair,T be pnptree of P, f be FinSequence of LTLB_WFF st rng f = (rngr T)^ holds {}LTLB_WFF |- ('not' ((con nega f)/.(len con nega f))) => ('X' ('not' ((con nega f)/.(len con nega f)))) proof let P be consistent complete PNPair,T be pnptree of P,f be FinSequence of l; assume A1: rng f = (rngr T)^; A2: now let R be Element of rng T; consider Q be object such that A3: Q in untn R by XBOOLE_0:def 1; reconsider Q as Element of untn R by A3; consider g be FinSequence such that A4: rng g = (comp Q)^ and g is one-to-one by FINSEQ_4:58; reconsider g as FinSequence of l by A4,FINSEQ_1:def 4; A5: {}l |- R^ => 'X' (Q^) by Th18; reconsider Q as consistent PNPair; now let j be Nat; assume j in dom g; then g/.j in (comp Q)^ by PARTFUN2:2,A4; then consider S being PNPair such that A6: g/.j = S^ and A7: S in comp Q; comp Q c= rngr T by Th28; then S^ in (rngr T)^ by A7; then consider k such that A8: k in dom f and A9: f/.k = g/.j by A6,A1,PARTFUN2:2; f/.k => alt(f) is ctaut by LTLAXIO2:29,A8; then f/.k => alt(f) in LTL_axioms by LTLAXIO1:def 17; hence {}l |- (g/.j) => alt(f) by LTLAXIO1:42,A9; end; then A10: {}l |- alt(g) => alt(f) by LTLAXIO2:57; ('X' (Q^ => alt(f))) => (('X' (Q^)) => ('X' alt(f))) in LTL_axioms by LTLAXIO1:def 17;then A11: {}l |- ('X' (Q^ => alt(f))) => (('X' (Q^)) => ('X' alt(f))) by LTLAXIO1:42; {}l |- Q^ => alt(g) by Th17,A4; then {}l |- 'X' (Q^ => alt(f)) by A10,LTLAXIO1:47,LTLAXIO1:44; then {}l |- ('X' (Q^)) => ('X' alt(f)) by A11,LTLAXIO1:43; hence {}l |- R^ => ('X' alt(f)) by LTLAXIO1:47,A5; end; now let i be Nat; assume i in dom f; then f/.i in (rngr T)^ by PARTFUN2:2,A1; then consider R such that A12: f/.i = R^ and A13: R in rngr T; ex t be Node of T st R = T.t & t <> {} by A13; then R in rng T by FUNCT_1:3; hence {}l |- (f/.i) => ('X' alt(f)) by A2,A12; end; hence {}l |- alt(f) => ('X' alt(f)) by LTLAXIO2:57; end; begin definition let P be consistent PNPair; let T be pnptree of P; mode path of T -> sequence of dom T means :Def13: it.0 = {} & for k be Nat holds it.(k+1) in succ (it.k); existence proof set F1 = dom T; reconsider F2 = {} as Element of F1 by TREES_1:22; defpred P1[Nat,Element of F1,Element of F1] means $3 in succ $2; A1: now let n be Nat; let x be Element of F1; consider y being object such that A2: y in succ x by XBOOLE_0:def 1; reconsider y as Element of F1 by A2; thus ex y being Element of F1 st P1[n,x,y] by A2; end; consider f being sequence of F1 such that A3: f.0 = F2 & for n being Nat holds P1[n,f.n qua Element of F1, f.(n + 1) qua Element of F1] from RECDEF_1:sch 2(A1); thus thesis by A3; end; end; definition let P be consistent complete PNPair,T be pnptree of P,t be path of T,i; redefine func t.i -> Node of T; coherence proof t.i is Element of dom T;hence thesis;end; end; theorem Th30: for P be consistent complete PNPair,T be pnptree of P,t be path of T st A 'U' B in rng (T.(t.i))`2 holds for j st j > i holds (B in rng (T.(t.j))`2 or ex k st i < k & k < j & A in rng (T.(t.k))`2) proof set aub = A 'U' B; let P be consistent complete PNPair,T be pnptree of P,t be path of T; assume A1: aub in rng (T.(t.i))`2; given j such that A2: j > i and A3: not B in rng (T.(t.j))`2and A4: for k st i < k & k < j holds not A in rng (T.(t.k))`2; A5: j >= i+1 by A2,NAT_1:13; per cases by A5,XXREAL_0:1; suppose j = i+1; then t.j in succ (t.i) by Def13; then ex n being Nat st t.j = (t.i)^<*n*> & (t.i)^<*n*> in dom T; then T.(t.j) in compn T.(t.i) by Th26; hence contradiction by Th24,A1,A3; end; suppose A6: j > i+1; i+1 >= 1 by NAT_1:11; then reconsider j1 = j - 1 as Element of NAT by XXREAL_0:2,A6,NAT_1:21; defpred P[Nat] means i < $1 & $1 < j implies aub in rng (T.(t.$1))`2; j = j1 + 1; then t.j in succ (t.j1) by Def13; then ex n being Nat st t.j = (t.j1)^<*n*> & (t.j1)^<*n*> in dom T; then A7: (T.(t.j)) in compn T.(t.j1) by Th26; A8: now let k be Nat; set k1 = k + 1; assume A9: P[k]; thus P[k1] proof assume that A10: i < k1 and A11: k1 < j; A12: i <= k by NAT_1:13,A10; per cases by A12,XXREAL_0:1; suppose A13: i < k; set Pk1 = T.(t.k1); t.k1 in succ (t.k) by Def13; then ex n being Nat st t.k1 = (t.k)^<*n*> & (t.k)^<*n*> in dom T; then Pk1 in compn T.(t.k) by Th26;then A in rng Pk1`2 or aub in rng Pk1`2 by Th24,A11,NAT_1:16,XXREAL_0:2,A13,A9; hence aub in rng (T.(t.k1))`2 by A4,A10,A11; end; suppose A14: i = k; set Pk1 = T.(t.k1); t.k1 in succ (t.i) by A14,Def13; then ex n being Nat st t.k1 = (t.i)^<*n*> & (t.i)^<*n*> in dom T; then Pk1 in compn T.(t.i) by Th26; then A in rng Pk1`2 or aub in rng Pk1`2 by Th24,A1; hence aub in rng (T.(t.k1))`2 by A4,A10,A11; end; end; end; A15: j + (-1) < j & j+(-1) > i+1+(-1) by XREAL_1:30, A6,XREAL_1:8; A16: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A16,A8); then aub in rng (T.(t.j1))`2 by A15; hence contradiction by Th24,A7,A3; end; end; theorem Th31: for P be consistent complete PNPair,T be pnptree of P st A 'U' B in rng P`1 & (for Q be Element of rngr T holds not B in rng Q`1) holds for Q be Element of rngr T holds B in rng Q`2 & A 'U' B in rng Q`1 proof set aub = A 'U' B; let P be consistent complete PNPair,T be pnptree of P; assume that A1: aub in rng P`1 and A2: for Q be Element of rngr T holds not B in rng Q`1; defpred P[set] means for t be Element of dom T st t = $1 & t <> 0 holds B in rng (T.t)`2 & aub in rng (T.t)`1; A3: now let t be Element of dom T,n be Nat; assume that A4: P[t] and t^<*n*> in dom T; thus P[t^<*n*>] proof let u be Element of dom T; assume that A5: u = t^<*n*> and u <> 0; A6: T.u in rngr T by A5; per cases; suppose t = 0; then T.t = P by Def11; then reconsider Tu = T.u as Element of compn P by Th26,A5; untn(A,B) in rng Tu`1 & rng Tu`1 c= rng Tu by Th22,A1, XBOOLE_1:7; then A7: B in rng Tu by Th8; not B in rng Tu`1 by A2,A6; hence B in rng (T.u)`2 & aub in rng (T.u)`1 by Th25,A1,A7,XBOOLE_0: def 3; end; suppose A8: not t = 0; reconsider Tu = T.u as Element of compn T.t by Th26,A5; rng Tu`1 c= rng Tu & untn(A,B) in rng Tu`1 by XBOOLE_1:7,A8,A4,Th22; then A9: B in rng Tu by Th8; A10: aub in rng (T.t)`1 by A8,A4; not B in rng Tu`1 by A2,A6; hence B in rng (T.u)`2 & aub in rng (T.u)`1 by A10,A9,Th25,XBOOLE_0:def 3; end; end; end; let Q be Element of rngr T; Q in rngr T; then A11: ex t be Element of dom T st Q = T.t & t <> 0; A12: P[{}]; for t be Element of dom T holds P[t] from TREES_2:sch 1(A12,A3 ); hence B in rng Q`2 & A 'U' B in rng Q`1 by A11; end; theorem Th32: for P be consistent complete PNPair,T be pnptree of P st A 'U' B in rng P`1 ex R be Element of rngr T st B in rng R`1 proof let P be consistent complete PNPair,T be pnptree of P; set nb = 'not' B,gnb = 'G' nb,xgnb = 'X' gnb,aub = A 'U' B; set f = the Enumeration of (rngr T)^; set xaf = 'X' alt(f); A1: rng f = (rngr T)^ by RLAFFIN3:def 1; {} in dom T by TREES_1:22;then T.{} in rng T by FUNCT_1:3;then A2: P in rng T by Def11; reconsider f as FinSequence of l; assume A3: aub in rng P`1; assume A4: for R be Element of rngr T holds not B in rng R`1; now let i be Nat; assume i in dom f; then f/.i in (rngr T)^ by PARTFUN2:2,A1; then consider R such that A5: f/.i = R^ and A6: R in rngr T; B in rng R`2 by Th31,A3,A4,A6; hence {}l |- (f/.i) => nb by LTLAXIO3:29,A5; end;then A7: {}l |- alt(f) => nb by LTLAXIO2:57; ('X' (alt(f) => gnb)) => (xaf => xgnb) in LTL_axioms by LTLAXIO1:def 17; then A8: {}l |- ('X' (alt(f) => gnb)) => (xaf => xgnb) by LTLAXIO1:42; {}l |- alt(f) => xaf by Th29,A1;then {}l |- 'X' (alt(f) => gnb) by LTLAXIO1:45,A7,LTLAXIO1:44;then A9: {}l |- xaf => xgnb by A8,LTLAXIO1:43; consider R be object such that A10: R in untn P by XBOOLE_0:def 1; reconsider R as Element of untn P by A10; set xr = 'X' (R^); set g = the Enumeration of (comp R)^; reconsider g as FinSequence of l; A11: rng g = (comp R)^ by RLAFFIN3:def 1; (rngr T)^ = (comp R \/ rngr T)^ by Th28,XBOOLE_1:12,A2 .= (comp R)^ \/ (rngr T)^ by Th10; then alt(g) => alt(f) is ctaut by XBOOLE_1:7,A11,A1 ,LTLAXIO2:30; then alt(g) => alt(f) in LTL_axioms by LTLAXIO1:def 17; then A12: {}l |- alt(g) => alt(f) by LTLAXIO1:42; A13: {}l |- P^ => xr by Th18; ('X' (R^ => alt(f))) => (xr => xaf) in LTL_axioms by LTLAXIO1:def 17; then A14: {}l |- ('X' (R^ => alt(f))) => (xr => xaf) by LTLAXIO1:42; {}l |- R^ => alt(g) by A11,Th17; then {}l |- 'X' (R^ => alt(f)) by A12,LTLAXIO1:47,LTLAXIO1:44; then {}l |- xr => xaf by LTLAXIO1:43,A14;then {}l |- P^ => xaf by LTLAXIO1:47,A13;then A15: {}l |- P^ => xgnb by LTLAXIO1:47,A9; A16: {}l |- P^ => aub by LTLAXIO3:28,A3; aub => ('X' ('F' B)) in LTL_axioms by LTLAXIO1:def 17;then A17: {}l |- aub => ('X' ('F' B)) by LTLAXIO1:42; ('X' ('F' B)) => ('not' xgnb) in LTL_axioms by LTLAXIO1:def 17; then {}l |- ('X' ('F' B)) => ('not' xgnb) by LTLAXIO1:42; then {}l |- aub => ('not' xgnb) by A17,LTLAXIO1:47; then {}l |- P^ => ('not' xgnb) by LTLAXIO1:47,A16; then {}l |- P^ => (xgnb '&&' ('not' xgnb)) by A15,LTLAXIO2:52; then {}l |- 'not' (P^) by LTLAXIO2:55; hence contradiction by LTLAXIO3:def 10; end; definition let P be consistent PNPair,T be pnptree of P; let t be path of T; attr t is complete means :Def14: for i st A 'U' B in rng (T.(t.i))`1 ex j st j > i & B in rng (T.(t.j))`1 & for k st i < k & k < j holds A in rng (T.(t.k))`1; end; registration let P be consistent complete PNPair,T be pnptree of P; cluster complete for path of T; existence proof set YN = {rng R where R is Element of pairs: R in rng T}; A1: rng T is finite; A2: YN is finite from FRAENKEL:sch 21(A1); YN is finite-membered proof let x;assume x in YN;then consider R be Element of pairs such that A3: x = rng R & R in rng T; thus x is finite by A3; end;then reconsider YN as finite finite-membered set by A2; now let x;assume x in YN;then consider R be Element of pairs such that A4: x = rng R & R in rng T; thus x c= l by A4; end;then reconsider Tforms = union YN as finite Subset of l by ZFMISC_1:76; defpred P1[Element of l] means $1 in Tforms & $1 is s-until; set uns = {p where p is Element of l: P1[p]}; A5: uns c= l from FRAENKEL:sch 10; uns c= Tforms proof let x be object; assume x in uns; then ex p st p = x & P1[p]; hence x in Tforms; end; then reconsider uns as finite Subset of l by A5; reconsider e = 0 as Element of dom T by TREES_1:22; set f = the Function of NAT,dom T; set m = card uns; consider g be FinSequence such that A6: rng g = uns and A7: g is one-to-one by FINSEQ_4:58; reconsider g as one-to-one FinSequence of l by A6,A7,FINSEQ_1:def 4; defpred P[Nat,Element of dom T,Element of dom T] means (not g.(($1 mod m)+1) in rng (T.$2)`1 implies $3 in succ $2) & (g.(($1 mod m)+1) in rng (T.$2)`1 implies $2 is_a_proper_prefix_of $3 & rarg (g/.(($1 mod m)+1)) in rng (T.$3)`1); A8: card g = m by A6,PRE_POLY:19; A9: now let n be Nat; let x be Node of T; A10: ex t be object st t in succ x by XBOOLE_0:def 1; set gk = g.((n mod m)+1); per cases; suppose not gk in rng (T.x)`1; hence ex y being Node of T st P[n,x,y] by A10; end; suppose A11: gk in rng (T.x)`1; A12: 1 <= (n mod m)+1 by NAT_1:25; per cases; suppose uns = {}; then dom g = {} by A6,RELAT_1:42; then A13: gk = 0 by FUNCT_1:def 2; len <*>l = 0; hence ex y being Node of T st P[n,x,y] by HILBERT2:10, A13,A11; end; suppose uns <> {}; then (n mod m)+1 <= m by NAT_D:1,NAT_1:13; then A14: (n mod m)+1 in dom g by A8,FINSEQ_3:25,A12; then gk in uns by FUNCT_1:3,A6; then consider puq be Element of l such that A15: gk = puq and puq in Tforms and A16: puq is s-until; consider p,q such that A17: gk = p 'U' q by A15,A16,HILBERT2:def 6; consider R being Element of rngr (T|x) such that A18: q in rng R`1 by A11,Th32,A17; R in rngr (T|x); then consider t be Node of (T|x) such that A19: R = (T|x).t and A20: t <> 0; t in dom (T|x); then A21: t in (dom T)|x by TREES_2:def 10; then reconsider y = x^t as Node of T by TREES_1:def 6; A22: x is_a_proper_prefix_of y by TREES_1:10,A20; g/.((n mod m)+1) = puq by A15,PARTFUN1:def 6,A14; then A23: rarg g/.((n mod m)+1) = q by Def1, A15,A16,A17; (T.y)`1 = R`1 by A19,TREES_2:def 10,A21; hence ex y being Node of T st P[n,x,y] by A18,A23, A11,A22; end; end; end; consider p being sequence of dom T such that A24: p.0 = e & for n being Nat holds P[n,p.n qua Element of dom T,p.(n+1) qua Element of dom T] from RECDEF_1:sch 2(A9); defpred Q[Nat] means $1 <= len (p.$1 qua Node of T); A25: now let k be Nat; defpred P3[Nat] means ex t be FinSequence st (p.$1 qua Node of T)^t = (p.($1+1) qua Node of T) & t <> {}; reconsider pk = p.k,pk1 = p.(k+1) as Node of T; A26: P[k,pk,pk1] by A24; per cases; suppose not g.((k mod m)+1) in rng (T.pk)`1; then ex n being Nat st pk1 = pk^<*n*> & pk^<*n*> in dom T by A26; hence P3[k]; end; suppose g.((k mod m)+1) in rng (T.pk)`1; then A27: pk is_a_proper_prefix_of pk1 by A24; then consider r being FinSequence such that A28: pk1 = pk ^ r by TREES_1:1; r <> 0 by FINSEQ_1:34, A27,A28; hence P3[k] by A28; end; end; A29: now let k be Nat; assume A30: Q[k]; reconsider pk = p.k,pk1 = p.(k+1) as Node of T; consider t be FinSequence such that A31: pk1 = pk^t and A32: t <> {} by A25; len t >= 1 by A32,NAT_1:25; then len pk + len t >= k+1 by A30,XREAL_1:7; hence Q[k + 1] by A31,FINSEQ_1:22; end; defpred P4[Nat] means for i st i <= $1 holds p.i c= p.$1; deffunc F3(Element of NAT) = (p.$1 qua Node of T)|$1; consider f be sequence of dom T such that A33: for n holds f.n = F3(n) from FUNCT_2:sch 4; A34: now let k be Nat; reconsider pk=p.k,pk1=p.(k+1)as Node of T; assume A35: P4[k]; thus P4[k+1] proof let i; A36: now assume i < k+1; then i <= k by NAT_1:13; then A37: p.i c= p.k by A35; ex t be FinSequence st pk^t = pk1 & t <> 0 by A25; then pk c= pk1 by FINSEQ_6:10; hence p.i c= p.(k+1) by A37; end; assume i <= k+1; hence thesis by A36,XXREAL_0:1; end; end; A38: Q[0]; A39: for n being Nat holds Q[n] from NAT_1:sch 2(A38,A29); A40: P4[0]; A41: for j being Nat holds P4[j] from NAT_1:sch 2(A40,A34); A42: now let k be Nat; reconsider k1 = k as Element of NAT by ORDINAL1:def 12; reconsider fk = f.k,fk1=f.(k+1) as Element of dom T; reconsider pk = p.k,pk1=p.(k+1) as Node of T; k+1<= len pk1 by A39; then A43: len (pk1|(k+1)) = k+1 by FINSEQ_1:59; k1<=len pk by A39; then len (pk|k) = k by FINSEQ_1:59; then A44: len fk = k by A33; A45: k1 < k1+1 by NAT_1:13; then pk c= pk1 by A41; then pk|k c= pk1|(k+1) by RELAT_1:77, A45,FINSEQ_1:5; then f.k1 c= pk1|(k+1) by A33; then fk is_a_prefix_of fk1 by A33; then consider r being FinSequence such that A46: fk1 = fk ^ r by TREES_1:1; rng r c= rng fk1 by FINSEQ_1:30,A46; then reconsider r as FinSequence of NAT by XBOOLE_1:1,FINSEQ_1:def 4; len fk1 = len fk + len r by FINSEQ_1:22,A46; then k+1 = k + len r by A43,A33,A44; then Z: r = <*r.1*> by FINSEQ_5:14; then 1 <= len r by FINSEQ_1:39; then 1 in dom r by FINSEQ_3:25; then r.1 = r/.1 by PARTFUN1:def 6; hence f.(k+1) in succ (f.k) by A46,Z; end; f.0 = F3(0) by A33 .= 0 by A24; then reconsider f as path of T by A42,Def13; A47: now let n; reconsider pn = p.n as Node of T; reconsider pln = p.(len pn) as Node of T; pn c= pln by A39,A41; then Seg len pn c= dom pn & ex t be FinSequence st pln = pn^t by FINSEQ_1: def 3,TREES_1:1; then pln|(len pn) = pn|len pn by FINSEQ_6:11 .= pn by FINSEQ_1:58; hence F3(len (p.n qua Node of T)) = p.n; end; f is complete proof let A,B,i; set aub = A 'U' B; assume A48: aub in rng (T.(f.i))`1; defpred P2[Nat] means $1 > i implies not B in rng (T.(f.$1))`1 & aub in rng (T.(f.$1))`1 & A in rng (T.(f.$1))`1; assume A49: for j st j > i holds (not B in rng (T.(f.j))`1 or ex k st i < k & k < j & not A in rng (T.(f.k))`1 ); A50: now let k be Nat; assume A51: for n being Nat st n < k holds P2[n]; thus P2[k] proof reconsider k1 = k as Element of NAT by ORDINAL1:def 12; set fk = T.(f.k1); assume A52: k > i; then k1 >= 1 by NAT_1:25; then reconsider kk = k1-1 as Element of NAT by NAT_1:21; set fkk = T.(f.kk); A53: kk+1 = k; then A54: kk >=i by NAT_1:13,A52; per cases by A54,XXREAL_0:1; suppose A55: kk = i; per cases by A49, A52; suppose A56: not B in rng fk`1; f.k in succ (f.kk) by Def13,A53;then ex n being Nat st f.k = (f.kk)^<*n*> & (f.kk)^<*n*> in dom T; then reconsider fk as Element of compn fkk by Th26; B in rng fk`1 or A in rng fk`1 & aub in rng fk`1 by Th25,A55,A48; hence thesis by A56; end; suppose ex m be Element of NAT st i < m&m < k1& not A in rng (T.(f.m))`1; hence thesis by NAT_1:13,A55,A53; end; end; suppose A57: kk > i; per cases by A49, A52; suppose A58: not B in rng fk`1; f.k in succ (f.kk) by Def13,A53;then ex n being Nat st f.k = (f.kk)^<*n*> & (f.kk)^<*n*> in dom T; then reconsider fk as Element of compn fkk by Th26; kk < k by XREAL_1:146; then aub in rng fkk`1 by A51,A57;then B in rng fk`1 or A in rng fk`1 & aub in rng fk`1 by Th25; hence thesis by A58; end; suppose ex m be Element of NAT st i < m&m < k1& not A in rng (T.(f.m))`1; hence thesis by A51; end; end; end; end; A59: for j be Nat holds P2[j] from NAT_1:sch 4(A50); T.(f.i) in rng T by FUNCT_1:3;then rng (T.(f.i)) in YN & rng (T.(f.i))`1 c= rng (T.(f.i)) by XBOOLE_1:7; then (aub is s-until)& aub in Tforms by HILBERT2:def 6,A48,TARSKI:def 4; then A60: aub in uns; then consider n be object such that A61: n in dom g and A62: g.n = aub by A6,FUNCT_1:def 3; reconsider n as Element of NAT by A61; reconsider k = n - 1 as Element of NAT by A61,FINSEQ_3:25, NAT_1:21; k+1 <= len g by FINSEQ_3:25, A61; then A63: k < card g by NAT_1:13; set mnk = m*(i+1)+k; i+1 > i & m >=1 by NAT_1:13, A60,NAT_1:25; then (i+1)*m > i*1 by XREAL_1:97; then A64: m*(i+1)+k > i by XREAL_1:40; then A65: mnk+1 > i by NAT_1:13; A66: (mnk mod m)+1 = (k mod m)+1 by NAT_D:21 .= k+1 by NAT_D:24, A63, A8; reconsider t = p.mnk,t1 = p.(mnk+1) as Node of T; mnk <= len t by A39; then A67: len t > i by A64,XXREAL_0:2; A68: aub is s-until by HILBERT2:def 6; mnk+1 <= len t1 by A39; then A69: len t1 > i by A65,XXREAL_0:2; A70: t1 = F3(len t1) by A47 .= f.(len t1) by A33; t = F3(len t) by A47 .= f.(len t) by A33; then g.(k+1) in rng (T.t)`1 by A67,A59, A62; then A71: rarg (g/.((mnk mod m)+1)) in rng (T.t1)`1 by A66,A24; rarg (g/.((mnk mod m)+1)) = rarg aub by A62, A61,PARTFUN1:def 6,A66 .= B by Def1,A68; hence contradiction by A69,A59, A71,A70; end; hence thesis; end; end; registration let P be consistent PNPair; cluster P^ -> satisfiable; coherence proof consider Q be object such that A1: Q in comp P by XBOOLE_0:def 1; consider Pg be consistent PNPair such that Pg = Q and A2: Pg is_completion_of P by A1; A3: rng P`1 c= rng Pg`1 by A2; A4: rng P`2 c= rng Pg`2 by A2; reconsider Pg as consistent complete PNPair by A2,Th13; set T = the pnptree of Pg; set t = the complete path of T; defpred P[Element of NAT,Element of bool props] means $2 = {p where p is Element of l: p is simple & p in rng (T.(t.$1))`1}; A5: now let x be Element of NAT; set y = {p where p is Element of l: p is simple & p in rng (T.(t.x))`1}; y c= props proof let z be object; assume z in y; then consider p be Element of l such that A6: p = z and A7: p is simple and p in rng (T.(t.x))`1; ex n st p = prop n by A7,HILBERT2:def 8; hence z in props by LTLAXIO1:def 10,A6; end; then reconsider y as Element of bool props; P[x,y]; hence ex y being Element of bool props st P[x,y]; end; consider M being sequence of bool props such that A8: for n being Element of NAT holds P[n,M.n qua Element of bool props] from FUNCT_2:sch 3(A5); set s = SAT M; defpred P1[Element of l] means for i be Element of NAT st $1 in rng (T.(t.i)) holds (s.[i,$1] = 1 iff $1 in rng (T.(t.i))`1); A9: now let i be Element of NAT,p; assume A10: p is simple; then A11:ex n st p = prop n by HILBERT2:def 8; A12: M.i = {q where q is Element of l: q is simple & q in rng (T.(t.i))`1} by A8; hereby assume s.[i,p] = 1; then p in M.i by A11,LTLAXIO1:def 11;then ex q be Element of l st p = q &( q is simple)& q in rng (T.(t .i))`1 by A12; hence p in rng (T.(t.i))`1; end; assume p in rng (T.(t.i))`1; then p in M.i by A12,A10; hence s.[i,p] = 1 by LTLAXIO1:def 11,A11; end; A13: now let n; prop n is simple by HILBERT2:def 8; hence P1[prop n] by A9; end; A14: now let r,q; set ruq = r 'U' q; assume that A15: P1[r] and A16: P1[q]; thus P1[ruq] proof let i be Element of NAT; defpred P2[Nat] means not (SAT M).[$1,q] = 1; set Q = T.(t.i); defpred P3[Element of NAT] means ex k st i < k & k < $1 & not (SAT M).[k,r] = 1; assume A17: ruq in rng Q; hereby assume A18: s.[i,ruq] = 1; assume not r 'U' q in rng (T.(t.i))`1;then A19: r 'U' q in rng (T.(t.i))`2 by A17,XBOOLE_0:def 3; consider j such that A20: j > i & s.[j,q] = 1 & for k st i < k & k < j holds s.[k,r] = 1 by A18,Th5; per cases by Th30,A19,A20; suppose q in rng (T.(t.j))`2;then not q in rng (T.(t.j))`1 & q in rng (T.(t.j)) by LTLAXIO3:30,XBOOLE_0:3,XBOOLE_0:def 3; hence contradiction by A16,A20; end; suppose ex k st i < k & k < j & r in rng (T.(t.k))`2;then consider k such that A21: i < k & k < j and A22: r in rng (T.(t.k))`2; not r in rng (T.(t.k))`1 & r in rng (T.(t.k)) by LTLAXIO3:30,A22,XBOOLE_0:3,XBOOLE_0 : def 3;then not s.[k,r] = 1 by A15; hence contradiction by A21,A20; end; end; assume ruq in rng Q`1; then consider j such that A23: j > i and A24: q in rng (T.(t.j))`1 and A25: for k st i < k & k < j holds r in rng (T.(t.k))`1 by Def14; A26: now let k; assume i < k & k < j; then A27: r in rng (T.(t.k))`1 by A25; then r in rng (T.(t.k)) by XBOOLE_0:def 3; hence s.[k,r] = 1 by A15,A27; end; q in rng (T.(t.j)) by A24,XBOOLE_0:def 3; then s.[j,q] = 1 by A24,A16; hence s.[i,ruq] = 1 by A26,Th5,A23; end; thus P1[r => q] proof let i be Element of NAT; set Q = T.(t.i); assume A28: r => q in rng Q; A29: tau rng Q = rng Q by LTLAXIO3:def 11; then A30: r in rng Q by A28,LTLAXIO3:19; A31: q in rng Q by A28,LTLAXIO3:19,A29; A32: s.[i,r] = 1 or s.[i,r] = 0 by XBOOLEAN:def 3; hereby assume s.[i,r=>q] = 1; then s.[i,r] => s.[i,q] = 1 by LTLAXIO1:def 11; then not r in rng Q`1 or q in rng Q`1 by A32,A15,A16, A30,A31; then r in rng Q`2 or q in rng Q`1 by A30,XBOOLE_0:def 3; hence r => q in rng Q`1 by LTLAXIO3:33,A28,A30,A31; end; assume r => q in rng Q`1; then r in rng Q`2 or q in rng Q`1 by LTLAXIO3:33,A28,A30, A31; then not r in rng Q`1 or q in rng Q`1 by XBOOLE_0:3, LTLAXIO3:30; then s.[i,r] => s.[i,q] = 1 by A15,A16,A30,A31,A32; hence s.[i,r=>q] = 1 by LTLAXIO1:def 11; end; end; A33: P1[TFALSUM] by LTLAXIO3:32,LTLAXIO1:def 11; A34: for A holds P1[A] from HILBERT2:sch 2(A33,A13,A14); A35: T.(t.0) = T.{} by Def13 .= Pg by Def11; now let i; set nA = (nega P`2)/.i,A = (P`2)/.i; assume A36: i in dom nega P`2; len nega P`2 = len P`2 by LTLAXIO2:def 4; then A37: i in dom P`2 by A36,FINSEQ_3:29; then (P`2).i in rng P`2 by FUNCT_1:3; then A in rng P`2 by PARTFUN1:def 6,A37;then A38: A in rng Pg`2 & not A in rng Pg`1 by A4, LTLAXIO3:30,XBOOLE_0:3; rng Pg`2 c= rng Pg by XBOOLE_1:7; then A39: not s.[0,A] = 1 by A38,A35,A34; thus s.[0,nA] = s.[0,'not' A] by LTLAXIO2:8,A37 .= 1 by A39,XBOOLEAN:def 3,LTLAXIO1:5; end; then A40: s.[0,kon(nega (P`2))] = 1 by Th6; now let i; set A = (P`1)/.i; assume i in dom P`1; then A in rng P`1 by PARTFUN2:2; then rng Pg`1 c= rng Pg & A in rng Pg`1 by XBOOLE_1:7, A3; hence s.[0,A] = 1 by A35,A34; end; then s.[0,kon(P`1)] = 1 by Th6; then s.[0,P^] = 1 by A40,LTLAXIO1:7; hence P^ is satisfiable; end; end; ::$N Completeness theorem for Propositional Linear Temporal Logic theorem F |= A implies F |- A proof A1: now let p; set PN = [<*> l,<*p*>],tv = TVERUM; assume {}l |= p; then not tv '&&' 'not' p is satisfiable by Th3,Th4; then not PN^ is satisfiable by Th7; then PN is Inconsistent; then {} l |- 'not' (PN^); then A2: {} l |- 'not' (tv '&&' 'not' p) by Th7; ('not' (tv '&&' 'not' p)) => p is ctaut by LTLAXIO2:38; then ('not' (tv '&&' 'not' p)) => p in LTL_axioms by LTLAXIO1:def 17; then {}l |- ('not' (tv '&&' 'not' p)) => p by LTLAXIO1:42; hence {}l |- p by LTLAXIO1:43,A2; end; assume A3: F |= A; now consider f be FinSequence such that A4: rng f = F and f is one-to-one by FINSEQ_4:58; reconsider f as FinSequence of l by A4,FINSEQ_1:def 4; assume A5: not F is empty; then A6: 1 <= len f by RELAT_1:38,A4,FINSEQ_1:20; then 1 <= len impg(f,A) by LTLAXIO2:def 3; then A7: impg(f,A)/.1 = impg(f,A).1 by FINSEQ_4:15; defpred P[Nat] means 1 <= $1 & $1 <= len f implies rng (f /^ $1) |= impg(f,A)/.$1; a8: 1 in dom f by A6,FINSEQ_3:25; rng (f|1) = rng <*f.1*> by FINSEQ_5:20, RELAT_1:38,A4,A5 .= rng <*f/.1*> by a8,PARTFUN1:def 6; then A8: rng (f /^ 1) \/ {f/.1} = rng (f|1) \/ rng (f /^ 1) by FINSEQ_1:38 .= rng ((f|1) ^ (f /^ 1)) by FINSEQ_1:31 .= rng f by RFINSEQ:8; A9: len impg(f,A) = len f by A6,LTLAXIO2:def 3; A10: now let i; A11: i in NAT by ORDINAL1:def 12; assume A12: P[i]; thus P[i + 1] proof assume that A13: 1 <= i+1 and A14: i+1 <= len f; per cases by NAT_1:25; suppose A15: i = 0; ('G' f/.1) => A = impg(f,A).1 by LTLAXIO2:def 3,A6 .= impg(f,A)/.1 by FINSEQ_4:15,A9,A6; hence rng (f /^ (i+1)) |= impg(f,A)/.(i+1) by A8,A4,A3,LTLAXIO1:30,A15; end; suppose A16: 1 <= i; i+1 in dom f by FINSEQ_3:25,A13,A14;then rng (<*f/.(i+1)*>^(f /^ (i+1))) |= impg(f,A)/.i by A12,A16,NAT_1:13,A14,FINSEQ_5:31;then rng <*f/.(i+1)*> \/ rng (f /^ (i+1)) |= impg(f,A)/.i by FINSEQ_1:31;then A17: rng (f /^ (i+1)) \/ {f/.(i+1)} |= impg(f,A)/.i by FINSEQ_1:38; A18: i < len f by NAT_1:13,A14; impg(f,A)/.(i+1) = impg(f,A).(i+1) by FINSEQ_4:15,A13,A14,A9 .= ('G' f/.(i+1)) => impg(f,A)/.i by LTLAXIO2:def 3,A16,A18,A11; hence rng (f /^ (i+1)) |= impg(f,A)/.(i+1) by A17,LTLAXIO1:30; end; end; end; A19: P[0]; for i holds P[i] from NAT_1:sch 2(A19,A10); then rng (f /^ (len f)) |= impg(f,A)/.(len f) by A6; then {} l |= impg(f,A)/.(len f) by RFINSEQ:27,RELAT_1:38; then A20: {} l |- impg(f,A)/.(len f) by A1; defpred P[Nat] means $1 < len f implies rng (f /^ (len f -' $1)) |- impg(f,A)/.(len f -' $1); A21: now let i; assume A22: P[i]; thus P[i+1] proof set j = len f -' (i+1); assume A23: i + 1 < len f; then A24: i + 1 + (- (i +1)) < len f + (-(i + 1)) by XREAL_1:8; then A25: j = len f - (i+1) by XREAL_0:def 2; then A26: 1 <= j by NAT_1:25, A24; i < len f by A23,NAT_1:12; then len f + (-i) > i + (-i) by XREAL_1:8; then A27: len f - i > 0; A28: j + 1 = len f - (i + 1) + 1 by XREAL_0:def 2, A24 .= len f -' i by XREAL_0:def 2,A27; A29: len f + (-i) <= len f by XREAL_1:32; then j + 1 <= len f by A25; then A30: j < len f by NAT_1:16,XXREAL_0:2; j + 1 <= len impg(f,A) by A29,A25,LTLAXIO2:def 3;then impg(f,A)/.(len f -' i) = impg(f,A).(j + 1) by A28,FINSEQ_4:15, NAT_1:11 .= ('G' (f/.(j + 1))) => impg(f,A)/.j by LTLAXIO2:def 3,A26, A30; then (rng (f /^ (len f -' i))) \/ {f/.(j + 1)} |- impg(f,A)/.j by LTLAXIO1:59,A22,NAT_1:12,A23;then (rng <*f/.(j + 1)*>) \/ rng (f /^ (len f -' i)) |- impg(f,A)/.j by FINSEQ_1:38;then A31: rng (<*f/.(j + 1)*>^(f /^ (len f -' i))) |- impg(f,A)/.j by FINSEQ_1:31; j + 1 in dom f by FINSEQ_3:25, NAT_1:11, A29,A25; hence rng (f /^ j) |- impg(f,A)/.j by A31,FINSEQ_5:31, A28; end; end; 1 + (-1) <= len f + (-1) by XREAL_1:6,FINSEQ_1:20,RELAT_1:38,A4,A5; then len f -' 1 = len f - 1 by XREAL_0:def 2; then reconsider i = len f -1 as Element of NAT; A32: len f + (- 1) < len f by XREAL_1:37; len f - 0 >= 1 by RELAT_1:38,A4,A5,FINSEQ_1:20; then len f -' 0 = len f by XREAL_0:def 2; then A33: P[0] by A20, RELAT_1:38,RFINSEQ:27; A34: for i holds P[i] from NAT_1:sch 2(A33,A21); len f -' i = len f - i by XREAL_0:def 2 .= 1; then rng (f /^ 1) |- impg(f,A)/.1 by A34,A32; then rng (f /^ 1) |- ('G' f/.1) => A by LTLAXIO2:def 3,A7, A6; hence F |- A by A4,A8,LTLAXIO1:59; end; hence F |- A by A1,A3; end;