:: The Properties of Sets of Temporal Logic Subformulas :: by Mariusz Giero :: :: Received May 7, 2012 :: Copyright (c) 2012-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, FUNCT_1, XBOOLEAN, MODELC_2, CQC_THE1, NAT_1, XXREAL_0, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, FUNCT_2, HILBERT2, ZFMISC_1, FUNCOP_1, ZF_MODEL, PBOOLE, GLIB_000, FINSET_1, ABCMIZ_0, HENMODEL, PRE_POLY, RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1, UNIALG_2, MEMBER_1, FINSEQ_5, LTLAXIO1, LTLAXIO2, LTLAXIO3, XCMPLX_0; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, RELSET_1, PARTFUN1, DOMAIN_1, NUMBERS, XCMPLX_0, NAT_1, XXREAL_0, TREES_1, TREES_2, TREES_4, TREES_9, XREAL_0, NAT_D, FUNCT_2, FINSET_1, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, HILBERT2, PBOOLE, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, MATROID0, LTLAXIO1, LTLAXIO2; constructors XXREAL_0, NAT_D, RELSET_1, AOFA_I00, HILBERT2, FINSET_1, RFINSEQ, DOMAIN_1, AFINSQ_2, REAL_1, STRUCT_0, FUNCOP_1, XREAL_0, MATROID0, LEXBFS, MCART_1, CARD_1, RLAFFIN3, FINSEQ_4, FINSEQ_5, FINSEQ_2, RFINSEQ2, BINOP_2, ENUMSET1, SETFAM_1, TREES_9, TREES_2, TREES_4, AFINSQ_1, LTLAXIO1, LTLAXIO2, XTUPLE_0; registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1, LTLAXIO1, JORDAN23, CARD_1, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions TARSKI, XBOOLE_0, FINSET_1, LTLAXIO1; equalities XBOOLEAN, FINSEQ_1, XBOOLE_0, FINSEQ_5, LTLAXIO1, LTLAXIO2, CARD_1, ORDINAL1; expansions TARSKI, XBOOLE_0, LTLAXIO1; theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, XBOOLEAN, FUNCT_2, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, FUNCOP_1, HILBERT2, XREAL_0, FINSEQ_4, RFINSEQ, FINSEQ_5, CARD_1, FUNCT_1, FINSEQ_3, FINSEQ_6, FINSEQ_2, XBOOLE_1, FINSET_1, PRE_POLY, CARD_2, LTLAXIO1, LTLAXIO2; schemes NAT_1, XBOOLE_0, HILBERT2, RECDEF_1, FRAENKEL; begin reserve A,B,p,q,r,s for Element of LTLB_WFF, n for Element of NAT, X for Subset of LTLB_WFF, g for Function of LTLB_WFF,BOOLEAN, x,y for set; set l = LTLB_WFF; deffunc alt(FinSequence of l) = 'not'((con nega \$1)/.(len con nega \$1)); deffunc kon(FinSequence of l) = ((con \$1)/.(len con \$1)); theorem Th1: for X be non empty set,t be FinSequence of X,k be Nat st k+1 <= len t holds t/^k = <*t.(k+1)*>^(t/^(k+1)) proof let X be non empty set,t be FinSequence of X,k be Nat; A1: k+1-'1 = k+1-1 by XREAL_0:def 2 .= k; assume k+1 <= len t;then t = (t|(k+1-'1)) ^ <*t.(k+1)*> ^ (t/^(k+1)) by NAT_1:11,FINSEQ_5:84 .= (t|k) ^ (<*t.(k+1)*> ^ (t/^(k+1))) by A1,FINSEQ_1:32; then (t|k)^(t/^k) = (t|k) ^ (<*t.(k+1)*> ^ (t/^(k+1))) by RFINSEQ:8; hence t/^k = <*t.(k+1)*>^(t/^(k+1)) by FINSEQ_1:33; end; theorem Th2: NAT --> {} is LTLModel proof set M = NAT --> {}; A1: now let x be object; assume x in NAT; then A2: M.x = {} by FUNCOP_1:7; {} c= props; hence M.x in bool props by A2; end; dom M = NAT by FUNCOP_1:13; hence thesis by A1,FUNCT_2:3; end; definition let X; attr X is without_implication means for p st p in X holds not p is conditional; end; definition let D be set; func D** -> set means :Def2: for x holds (x in it iff x is one-to-one FinSequence of D); existence proof defpred S2[object] means \$1 is one-to-one FinSequence of D; consider X being set such that A1: for x being object holds ( x in X iff x in bool [:NAT,D:] & S2[x] ) from XBOOLE_0:sch 1; take X; let x be set; thus x in X implies x is one-to-one FinSequence of D by A1; assume x is one-to-one FinSequence of D; then reconsider p = x as one-to-one FinSequence of D; p c= [:NAT,D:]; hence x in X by A1; end; uniqueness proof let D1, D2 be set; assume that A2: for x being set holds ( x in D1 iff x is one-to-one FinSequence of D) and A3: for x being set holds ( x in D2 iff x is one-to-one FinSequence of D); now let x be object; thus x in D1 implies x in D2 proof assume x in D1; then x is one-to-one FinSequence of D by A2; hence x in D2 by A3; end; assume x in D2; then x is one-to-one FinSequence of D by A3; hence x in D1 by A2; end; hence D1 = D2 by TARSKI:2; end; end; registration let D be set; cluster D** -> non empty; coherence proof the one-to-one FinSequence of D in D** by Def2; hence thesis; end; end; registration let D be finite set; cluster D** -> finite; coherence proof set seg =Seg card D; A1: D** c= PFuncs(seg,D) proof let x be object; assume x in D**; then reconsider f = x as one-to-one FinSequence of D by Def2; A2: dom f c= seg proof let x be object; assume A3: x in dom f; then reconsider x1 = x as Nat; A4: x in Seg len f by A3, FINSEQ_1:def 3; then A5: 1 <= x1 by FINSEQ_1:1; x1 <= len f by A4,FINSEQ_1:1; then A6: x1 <= card (rng f) by FINSEQ_4:62; Segm card (rng f) c= Segm card D by CARD_1:11; then card (rng f) <= card D by NAT_1:39; then x1 <= card D by XXREAL_0:2,A6; hence thesis by A5; end; rng f c= D; hence thesis by A2,PARTFUN1:def 3; end; PFuncs(seg,D) is finite by PRE_POLY:17; hence thesis by A1; end; end; theorem Th3: for D1, D2 being set st D1 c= D2 holds D1 ** c= D2 ** proof let D1, D2 be set; assume A1: D1 c= D2; let x be object; assume x in D1 **; then reconsider p = x as one-to-one FinSequence of D1 by Def2; rng p c= D2 by A1; then x is one-to-one FinSequence of D2 by FINSEQ_1:def 4; hence x in D2 ** by Def2; end; definition let a1 be set; let a2 be Subset of a1; redefine func a2 ** -> non empty Subset of (a1 **); coherence by Th3; end; theorem Th4: for F, G being one-to-one FinSequence st rng F misses rng G holds F ^ G is one-to-one proof let F, G be one-to-one FinSequence; assume A1: rng F misses rng G; reconsider FG = F ^ G as Function of (dom (F ^ G)),(rng (F ^ G)) by FUNCT_2:1; A2: FG is onto by FUNCT_2:def 3; card (dom (F ^ G)) = card Seg ((len F) + (len G)) by FINSEQ_1:def 7 .= (len F) + (len G) by FINSEQ_1:57 .= card (rng F) + (len G) by FINSEQ_4:62 .= card (rng F) + card (rng G) by FINSEQ_4:62 .= card ((rng F) \/ (rng G)) by A1,CARD_2:40 .= card (rng (F ^ G)) by FINSEQ_1:31; hence F ^ G is one-to-one by A2,FINSEQ_4:64; end; definition let X be set; let f,g be one-to-one FinSequence of X; assume A1: rng f misses rng g; func f ^^ g -> one-to-one FinSequence of X equals :Def3: f^g; coherence by Th4,A1; end; begin definition func tau1 -> Function of LTLB_WFF,bool LTLB_WFF means :Def4: it.TFALSUM={TFALSUM} & it.(prop n)={prop n} & it.(A=>B)={A => B} \/ it.A \/ it.B & it.(A 'U' B)={A 'U' B}; existence proof set bltl = bool l; defpred P1[Element of l,Element of l,set,set,set] means \$5={\$1'U'\$2}; deffunc F2(Element of NAT)={prop \$1}; defpred P3[Element of l,Element of l,set,set,set] means (\$3 is Element of bltl & \$4 is Element of bltl implies ex a,b,c be Element of bltl st a=\$3 & b=\$4 & c =\$5 & c = {\$1 => \$2} \/ \$3 \/ \$4) & (not\$3 is Element of bltl or not\$4 is Element of bltl implies \$5={} l); A1: for A,B for x,y be set ex z be set st P3[A,B,x,y,z] proof let A,B,x,y; per cases; suppose that A2: x is Element of bltl and A3: y is Element of bltl; reconsider b=y as Element of bltl by A3; reconsider a=x as Element of bltl by A2; consider z be set such that A4: z = {A => B} \/ a \/ b; take z; thus thesis by A4; end; suppose not x is Element of bltl or not y is Element of bltl; hence thesis; end; end; A5: for A,B for x,y be set ex z be set st P1[A,B,x,y,z]; A6: for p,q for a,b,c,d be set st P1[p,q,a,b,c] & P1[p,q,a,b,d] holds c =d; A7: for p,q for a,b,c,d be set st P3[p,q,a,b,c] & P3[p,q,a,b,d] holds c =d; consider val being ManySortedSet of l such that A8: val.TFALSUM={TFALSUM} & (for n holds val.(prop n)=F2(n)) & for p,q holds P1[p,q,val.p,val.q,val.(p 'U' q)] & P3[p,q,val.p,val.q,val.(p=>q)] from HILBERT2:sch 3(A5,A1,A6,A7); A9: now A10: now let A,B; A11: P3[A,B,val.A,val.B,val.(A=>B)] by A8; per cases; suppose val.A is Element of bltl & val.B is Element of bltl; thus val.(A=>B) in bltl by A11; end; suppose not(val.A is Element of bltl & val.B is Element of bltl); then val.(A=>B)={} l by A8; hence val.(A=>B) in bltl; end; end; let x be object; assume x in l; then reconsider x1=x as Element of l; A12: now let n; val.(prop n)={prop n} by A8; hence val.(prop n) in bltl; end; A13: now let A,B; val.(A 'U' B)={A 'U' B} by A8; hence val.(A 'U' B) in bltl; end; per cases by LTLAXIO1:4; suppose x1=TFALSUM; hence val.x in bltl by A8; end; suppose ex n be Element of NAT st x1=prop n; hence val.x in bltl by A12; end; suppose ex p,q st x1=p 'U' q; hence val.x in bltl by A13; end; suppose ex p,q st x1=p=>q; hence val.x in bltl by A10; end; end; dom val=l by PARTFUN1:def 2; then reconsider val as Function of l,bltl by A9,FUNCT_2:3; take val; now let A,B; P3[A,B,val.A,val.B,val.(A=>B)] by A8; hence val.(A=>B)={A => B} \/ val.A \/ val.B; end; hence thesis by A8; end; uniqueness proof set bltl = bool l; let v1,v2 be Function of l,bltl; assume A14: v1.TFALSUM={TFALSUM} & v1.(prop n)={prop n} & v1.(A=>B)= {A => B} \/ v1.A \/ v1.B & v1.(A 'U' B)={A 'U' B}; assume A15: v2.TFALSUM={TFALSUM} & v2.(prop n)={prop n} & v2.(A=>B)={A => B} \/ v2.A \/ v2.B & v2.(A 'U' B)={A 'U' B}; thus v1=v2 proof defpred P1[Element of l] means v1.\$1=v2.\$1; A16: for n holds P1[prop n] proof let n; v1.(prop n)={prop n} by A14 .=v2.(prop n) by A15; hence P1[prop n]; end; A17: for r,s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r=>s] proof let r,s; assume A18: ( P1[r])& P1[s]; A19: v1.(r 'U' s)={r 'U' s} by A14 .=v2.(r 'U' s) by A15; v1.(r=>s)={r=>s} \/ v1.r \/ v1.s by A14 .=v2.(r=>s) by A15,A18; hence thesis by A19; end; A20: P1[TFALSUM] by A14,A15; for x be Element of l holds P1[x] from HILBERT2:sch 2(A20,A16, A17); then A21: for x be Element of l st x in dom v1 holds P1[x]; dom v1=l by FUNCT_2:def 1 .=dom v2 by FUNCT_2:def 1; hence thesis by A21,PARTFUN1:5; end; end; end; theorem Th5: not A is conditional implies tau1.A = {A} proof assume not A is conditional; then A is conjunctive or A is simple or A = TFALSUM by HILBERT2:9; then ex r, s st A = r 'U' s or ex n st A = prop n or A = TFALSUM by HILBERT2:def 8,HILBERT2:def 6; hence thesis by Def4; end; theorem Th6: p in tau1.p proof defpred P1[Element of l] means \$1 in tau1.\$1; A1: for n holds P1[ prop n] proof let n; tau1.(prop n) = {prop n} by Def4; hence thesis by TARSKI:def 1; end; A2: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that P1[r] and P1[s]; tau1.(r 'U' s) = {r 'U' s} by Def4; hence P1[r 'U' s] by TARSKI:def 1; tau1.(r => s) = {r => s} \/ tau1.r \/ tau1.s by Def4;then {r => s} c= {r => s} \/ tau1.r & {r => s} \/ tau1.r c= tau1.(r => s) by XBOOLE_1:7; hence P1[r => s] by ZFMISC_1:31; end; tau1.TFALSUM = {TFALSUM} by Def4; then A3: P1[TFALSUM] by TARSKI:def 1; for p holds P1[p] from HILBERT2:sch 2(A3,A1,A2); hence thesis; end; registration let p; cluster tau1.p -> non empty finite; coherence proof thus tau1.p is non empty by Th6; defpred P1[Element of l] means tau1.\$1 is finite; A1: for n holds P1[ prop n] proof let n; tau1.(prop n) = {prop n} by Def4; hence thesis; end; A2: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume A3: P1[r] & P1[s]; tau1.(r 'U' s) = {r 'U' s} by Def4; hence P1[r 'U' s]; tau1.(r => s) = {r => s} \/ tau1.r \/ tau1.s by Def4; hence P1[r => s] by A3; end; A4: P1[TFALSUM] by Def4; for p holds P1[p] from HILBERT2:sch 2(A4,A1,A2); hence tau1.p is finite; end; end; theorem Th7: p => q in tau1.r implies p in tau1.r & q in tau1.r proof defpred P1[Element of l] means p => q in tau1.\$1 implies p in tau1.\$1 & q in tau1.\$1; A1: for n holds P1[ prop n] proof let n; set pr = prop n; assume p => q in tau1.pr; then p => q in {pr} by Def4; then p => q = pr by TARSKI:def 1; hence p in tau1.pr & q in tau1.pr by HILBERT2:26; end; A2: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that A3: P1[r] and A4: P1[s]; thus P1[r 'U' s] proof set f = r 'U' s; assume p => q in tau1.f; then p => q in {f} by Def4; then p => q = f by TARSKI:def 1; hence p in tau1.f & q in tau1.f by HILBERT2:22; end; thus P1[r => s] proof set f = r => s; A5: tau1.f = {f} \/ tau1.r \/ tau1.s by Def4; then A6: tau1.s c= tau1.f by XBOOLE_1:7; tau1.r c= {f} \/ tau1.r & {f} \/ tau1.r c= tau1.f by XBOOLE_1:7,A5; then A7: tau1.r c= tau1.f; assume A8: p => q in tau1.f; per cases by A8,A5,XBOOLE_0:def 3; suppose A9: p => q in {f} \/ tau1.r; per cases by A9,XBOOLE_0:def 3; suppose p => q in {f}; then A10: p => q = f by TARSKI:def 1; then A11: p = r by HILBERT2:20; r in tau1.r by Th6; hence p in tau1.f by A11,A7; A12: q = s by A10,HILBERT2:20; s in tau1.s by Th6; hence q in tau1.f by A12,A6; end; suppose p => q in tau1.r; hence p in tau1.f & q in tau1.f by A3,A7; end; end; suppose p => q in tau1.s; hence p in tau1.f & q in tau1.f by A4,A6; end; end; end; A13: P1[TFALSUM] proof set f = TFALSUM; assume p => q in tau1.f; then p => q in {f} by Def4; then p => q = f by TARSKI:def 1; hence p in tau1.f & q in tau1.f by HILBERT2:25; end; for p holds P1[p] from HILBERT2:sch 2(A13,A1,A2); hence thesis; end; theorem Th8: p in tau1.q implies tau1.p c= tau1.q proof defpred P1[Element of l] means \$1 in tau1.q implies tau1.\$1 c= tau1.q; A1: for n holds P1[ prop n] proof let n; set pr = prop n; assume A2: pr in tau1.q; let x be object; assume x in tau1.pr; then x in {pr} by Def4; hence x in tau1.q by TARSKI:def 1,A2; end; A3: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that A4: P1[r] and A5: P1[s]; thus P1[r 'U' s] proof set f = r 'U' s; assume A6: f in tau1.q; let x be object; assume x in tau1.f; then x in {f} by Def4; hence x in tau1.q by TARSKI:def 1,A6; end; thus P1[r => s] proof set f = r => s; assume A7: f in tau1.q; then {f} c= tau1.q by ZFMISC_1:31; then {f} \/ tau1.r c= tau1.q by XBOOLE_1:8, A7,Th7,A4;then A8: {f} \/ tau1.r \/ tau1.s c= tau1.q by XBOOLE_1:8, A7,Th7, A5; let x be object; assume x in tau1.f; then x in {f} \/ tau1.r \/ tau1.s by Def4; hence x in tau1.q by A8; end; end; A9: P1[TFALSUM] proof set f = TFALSUM; assume A10: f in tau1.q; let x be object; assume x in tau1.f; then x in {f} by Def4; hence x in tau1.q by TARSKI:def 1,A10; end; for p holds P1[p] from HILBERT2:sch 2(A9,A1,A3); hence thesis; end; theorem Th9: p 'U' q in tau1.('not' A) implies p 'U' q in tau1.A proof set a = p 'U' q,na = 'not' A,f = TFALSUM; A1: a <> A => f by HILBERT2:22; assume a in tau1.na; then a in {A => f} \/ tau1.A \/ tau1.f by Def4; then A2: a in {A => f} \/ tau1.A or a in tau1.f by XBOOLE_0:def 3; a <> f by HILBERT2:23; then not a in {f} by TARSKI:def 1; then a in {A => f} or a in tau1.A by A2,Def4,XBOOLE_0:def 3; hence thesis by A1,TARSKI:def 1; end; theorem Th10: p 'U' q in tau1.(A '&&' B)implies(p 'U' q in tau1.A or p 'U' q in tau1.B) proof set a = p 'U' q,nb = 'not' B; assume a in tau1.(A '&&' B); then a in tau1.(A => nb) by Th9; then a in {A => nb} \/ tau1.A \/ tau1.nb by Def4; then A1: a in {A => nb} \/ (tau1.A \/ tau1.nb) by XBOOLE_1:4; a <> A => nb by HILBERT2:22; then not a in {A => nb} by TARSKI:def 1; then a in tau1.A \/ tau1.nb by A1,XBOOLE_0:def 3; then a in tau1.A or a in tau1.nb by XBOOLE_0:def 3; hence thesis by Th9; end; theorem p in tau1.q & p <> q implies len p < len q proof defpred P1[Element of l] means p in tau1.\$1 & p <> \$1 implies len p < len \$1; A1: for n holds P1[ prop n] proof let n; tau1.(prop n) = {prop n} by Def4; hence thesis by TARSKI:def 1; end; A2: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that A3: P1[r] and A4: P1[s]; set u = r => s; tau1.(r 'U' s) = {r 'U' s} by Def4; hence P1[r 'U' s] by TARSKI:def 1; thus P1[u] proof assume that A5: p in tau1.u and A6: p <> u; tau1.u = {u} \/ tau1.r \/ tau1.s by Def4; then p in {u} \/ (tau1.r \/ tau1.s) by XBOOLE_1:4,A5; then A7: p in {u} or p in tau1.r \/ tau1.s by XBOOLE_0:def 3; per cases by A7,TARSKI:def 1,A6,XBOOLE_0:def 3; suppose p in tau1.r; hence thesis by HILBERT2:16,XXREAL_0:2,A3; end; suppose p in tau1.s; hence thesis by HILBERT2:16,XXREAL_0:2,A4; end; end; end; tau1.TFALSUM = {TFALSUM} by Def4; then A8: P1[TFALSUM] by TARSKI:def 1; for p holds P1[p] from HILBERT2:sch 2(A8,A1,A2); hence thesis; end; theorem Th12: tau1.p c= tau1.('not' p) proof set np = 'not' p,f=TFALSUM; A1: tau1.p c= {np} \/ tau1.p by XBOOLE_1:7; {np} \/ tau1.p c= {np} \/ tau1.p \/ tau1.f & tau1.np = {np} \/ tau1.p \/ tau1.f by XBOOLE_1:7, Def4; hence thesis by A1; end; theorem Th13: tau1.q c= tau1.(p '&&' q) proof set pq = p '&&' q,np = 'not' p,nq = 'not' q; A1: tau1.(p => nq) c= tau1.('not' (p => nq)) by Th12; tau1.(p => nq) = {p => nq} \/ tau1.p \/ tau1.nq by Def4; then A2: tau1.nq c= tau1.(p => nq) by XBOOLE_1:7; tau1.q c= tau1.nq by Th12; then tau1.q c= tau1.(p => nq) by A2; hence thesis by A1; end; theorem Th14: tau1.q c= tau1.(p 'or' q) proof set pq = p 'or' q,np = 'not' p,nq = 'not' q,npq = np '&&' nq; tau1.nq c= tau1.npq & tau1.q c= tau1.nq by Th13, Th12; then A1: tau1.q c= tau1.npq; tau1.npq c= tau1.pq by Th12; hence thesis by A1; end; definition let X; func tau X -> Subset of LTLB_WFF means :Def5: x in it iff ex A st A in X & x in tau1.A; existence proof set t = {tau1.p where p is Element of l: p in X}; union t c= l proof let x be object; assume x in union t; then consider y such that A1: x in y and A2: y in t by TARSKI:def 4; ex p be Element of l st y = tau1.p & p in X by A2; hence x in l by A1; end; then reconsider ut = union t as Subset of l; x in ut iff ex A st A in X & x in tau1.A proof hereby assume x in ut; then consider y such that A3: x in y and A4: y in t by TARSKI:def 4; ex p st y = tau1.p & p in X by A4; hence ex A st A in X & x in tau1.A by A3; end; given A such that A5: A in X and A6: x in tau1.A; tau1.A in t by A5; hence x in ut by TARSKI:def 4,A6; end; hence thesis; end; uniqueness proof let Y,Z be Subset of l such that A7: x in Y iff ex A st A in X & x in tau1.A and A8: x in Z iff ex A st A in X & x in tau1.A; thus Y c= Z proof let x be object; assume x in Y; then ex A st A in X & x in tau1.A by A7; hence thesis by A8; end; thus Z c= Y proof let x be object; assume x in Z; then ex A st A in X & x in tau1.A by A8; hence thesis by A7; end; end; end; theorem Th15: tau X = union {tau1.p where p is Element of LTLB_WFF: p in X} proof set A = {tau1.p where p is Element of l: p in X}; hereby let x be object; assume x in tau X; then consider p such that A1: p in X and A2: x in tau1.p by Def5; tau1.p in A by A1; hence x in union A by TARSKI:def 4,A2; end; let x be object; assume x in union A; then consider y such that A3: x in y and A4: y in A by TARSKI:def 4; A5: ex p st y = tau1.p & p in X by A4; then reconsider x1 = x as Element of l by A3; thus x in tau X by A5,A3,Def5; end; theorem Th16: X c= tau X proof let x be object; defpred P1[Element of l] means \$1 in X implies \$1 in tau X; assume A1: x in X; then reconsider x1 = x as Element of l; A2: for n holds P1[ prop n] proof let n; set pr = prop n; pr in {pr} by TARSKI:def 1; then A3: pr in tau1.pr by Def4; assume pr in X; hence thesis by A3,Def5; end; A4: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that P1[r] and P1[s]; thus P1[r 'U' s] proof set f = r 'U' s; f in {f} by TARSKI:def 1; then A5: f in tau1.f by Def4; assume f in X; hence thesis by A5,Def5; end; thus P1[r => s] proof set f = r => s; tau1.f = {f} \/ tau1.r \/ tau1.s by Def4 .= {f} \/ (tau1.r \/ tau1.s) by XBOOLE_1:4; then A6: f in {f} & {f} c= tau1.f by TARSKI:def 1,XBOOLE_1:7; assume f in X; hence thesis by A6,Def5; end; end; A7: P1[TFALSUM] proof set f = TFALSUM; f in {f} by TARSKI:def 1; then A8: f in tau1.f by Def4; assume f in X; hence thesis by A8,Def5; end; for p holds P1[p] from HILBERT2:sch 2(A7,A2,A4); hence x in tau X by A1; end; registration let X be empty Subset of LTLB_WFF; cluster tau X -> empty; coherence proof assume tau X is non empty; then consider x being object such that A1: x in tau X; ex p st p in X & x in tau1.p by A1,Def5; hence contradiction; end; end; registration let X be finite Subset of LTLB_WFF; cluster tau X -> finite; coherence proof set A = {tau1.p where p is Element of l: p in X}; deffunc F(Element of l) = tau1.\$1; A1: for x st x in A holds x is finite proof let x; assume x in A; then ex p st x = tau1.p & p in X; hence thesis; end; set B = {F(p) where p is Element of l: p in X}; A2: X is finite; A3: B is finite from FRAENKEL:sch 21(A2); tau X = union A by Th15; hence tau X is finite by A3,FINSET_1:7,A1; end; end; registration let X be non empty Subset of LTLB_WFF; cluster tau X -> non empty; coherence proof X c= tau X by Th16; hence thesis; end; end; theorem tau tau X = tau X proof thus tau tau X c= tau X proof let x be object; assume x in tau tau X; then consider p such that A1: p in tau X and A2: x in tau1.p by Def5; consider q such that A3: q in X and A4: p in tau1.q by A1,Def5; tau1.p c= tau1.q by A4,Th8; hence x in tau X by A2,A3,Def5; end; thus tau X c= tau tau X by Th16; end; theorem X is without_implication implies tau X = X proof assume A1: X is without_implication; A2: tau X c= X proof let x be object; assume x in tau X; then consider p such that A3: p in X and A4: x in tau1.p by Def5; x in {p} by A3,A1,Th5,A4; hence thesis by A3,TARSKI:def 1; end; X c= tau X by Th16; hence thesis by A2; end; theorem Th19: p => q in tau X implies p in tau X & q in tau X proof set t = {tau1.r where r is Element of l: r in X}; assume p => q in tau X; then consider B such that A1: B in X and A2: p => q in tau1.B by Def5; A3: tau1.B in t by A1; p in tau1.B by Th7,A2; then A4: p in union t by A3,TARSKI:def 4; q in tau1.B by Th7,A2; then q in union t by TARSKI:def 4,A3; hence thesis by A4,Th15; end; theorem Th20: p '&&' q in tau X implies p in tau X & q in tau X proof assume p '&&' q in tau X; then A1: p => (q => TFALSUM) in tau X by Th19; then 'not' q in tau X by Th19; hence thesis by A1,Th19; end; theorem Th21: p 'or' q in tau X implies p in tau X & q in tau X proof assume p 'or' q in tau X; then (('not' p) '&&' ('not' q)) in tau X by Th19; then 'not' p in tau X & 'not' q in tau X by Th20; hence thesis by Th19; end; theorem untn(p,q) in tau X implies p in tau X & q in tau X & p 'U' q in tau X proof assume A1: untn(p,q) in tau X; then p '&&' (p 'U' q) in tau X by Th21; hence thesis by A1,Th21,Th20; end; theorem p in tau X implies tau1.p c= tau X proof assume p in tau X; then consider B such that A1: B in X and A2: p in tau1.B by Def5; A3: tau1.B c= tau X by Def5,A1; tau1.p c= tau1.B by A2,Th8; hence thesis by A3; end; begin definition func Sub -> Function of LTLB_WFF,bool LTLB_WFF means :Def6: it.TFALSUM={TFALSUM} & it.(prop n)={prop n} & it.(A=>B)={A => B} \/ it.A \/ it.B & it.(A 'U' B)= tau1.untn (A,B) \/ it.A \/ it.B; existence proof set bltl = bool l; deffunc F2(Element of NAT)={prop \$1}; defpred P3[Element of l,Element of l,set,set,set] means (\$3 is Element of bltl & \$4 is Element of bltl implies ex a,b,c be Element of bltl st a=\$3 & b=\$4 & c =\$5 & c = {\$1 => \$2} \/ \$3 \/ \$4) & (not\$3 is Element of bltl or not\$4 is Element of bltl implies \$5={} l); defpred P1[Element of l,Element of l,set,set,set] means (\$3 is Element of bltl & \$4 is Element of bltl implies ex a,b,c be Element of bltl st a=\$3 & b=\$4 & c =\$5 & c = tau1.untn(\$1,\$2) \/ \$3 \/ \$4)& (not\$3 is Element of bltl or not\$4 is Element of bltl implies \$5={} l); A1: for A,B for x,y be set ex z be set st P3[A,B,x,y,z] proof let A,B,x,y; per cases; suppose that A2: x is Element of bltl and A3: y is Element of bltl; reconsider b=y as Element of bltl by A3; reconsider a=x as Element of bltl by A2; consider z be set such that A4: z = {A => B} \/ a \/ b; take z; thus thesis by A4; end; suppose not x is Element of bltl or not y is Element of bltl; hence thesis; end; end; A5: for A,B for x,y be set ex z be set st P1[A,B,x,y,z] proof let A,B,x,y; per cases; suppose that A6: x is Element of bltl and A7: y is Element of bltl; reconsider b=y as Element of bltl by A7; reconsider a=x as Element of bltl by A6; consider z be set such that A8: z = tau1.untn(A,B) \/ a \/ b; take z; thus thesis by A8; end; suppose not x is Element of bltl or not y is Element of bltl; hence thesis; end; end; A9: for p,q for a,b,c,d be set st P1[p,q,a,b,c] & P1[p,q,a,b,d] holds c = d; A10: for p,q for a,b,c,d be set st P3[p,q,a,b,c] & P3[p,q,a,b,d] holds c = d; consider val being ManySortedSet of l such that A11: val.TFALSUM={TFALSUM} & (for n holds val.(prop n)=F2(n)) & for p,q holds P1[p,q,val.p,val.q,val.(p 'U' q)] & P3[p,q,val.p,val.q,val.(p=>q)] from HILBERT2:sch 3(A5,A1,A9,A10); A12: now A13: now let A,B; P3[A,B,val.A,val.B,val.(A=>B)] by A11; hence val.(A=>B) in bltl; end; A14: now let A,B; P1[A,B,val.A,val.B,val.(A 'U' B)] by A11; hence val.(A 'U' B) in bltl; end; let x be object; assume x in l; then reconsider x1=x as Element of l; A15: now let n; val.(prop n)={prop n} by A11; hence val.(prop n) in bltl; end; per cases by LTLAXIO1:4; suppose x1=TFALSUM; hence val.x in bltl by A11; end; suppose ex n be Element of NAT st x1=prop n; hence val.x in bltl by A15; end; suppose ex p,q st x1=p 'U' q; hence val.x in bltl by A14; end; suppose ex p,q st x1=p=>q; hence val.x in bltl by A13; end; end; dom val=l by PARTFUN1:def 2; then reconsider val as Function of l,bltl by A12,FUNCT_2:3; A16: now let A,B; P3[A,B,val.A,val.B,val.(A=>B)] by A11; hence val.(A=>B)={A => B} \/ val.A \/ val.B; end; take val; now let A,B; P1[A,B,val.A,val.B,val.(A 'U' B)] by A11; hence val.(A 'U' B)=tau1.untn(A,B) \/ val.A \/ val.B; end; hence thesis by A16,A11; end; uniqueness proof set bltl = bool LTLB_WFF; let v1,v2 be Function of l,bltl; assume A17: v1.TFALSUM={TFALSUM} & v1.(prop n)={prop n} & v1.(A=>B)= {A => B} \/ v1.A \/ v1.B & v1.(A 'U' B)= tau1.untn(A,B) \/ v1.A \/ v1.B; assume A18: v2.TFALSUM={TFALSUM} & v2.(prop n)={prop n} & v2.(A=>B)={A => B} \/ v2.A \/ v2.B & v2.(A 'U' B)= tau1.untn(A,B) \/ v2.A \/ v2.B; thus v1=v2 proof defpred P1[Element of l] means v1.\$1=v2.\$1; A19: for n holds P1[prop n] proof let n; v1.(prop n)={prop n} by A17 .=v2.(prop n) by A18; hence P1[prop n]; end; A20: for r,s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r=>s] proof let r,s; assume A21: ( P1[r])& P1[s]; A22: v1.(r 'U' s)=tau1.untn(r,s) \/ v1.r \/ v1.s by A17 .=v2.(r 'U' s) by A18,A21; v1.(r=>s)={r=>s} \/ v1.r \/ v1.s by A17 .=v2.(r=>s) by A18,A21; hence thesis by A22; end; A23: P1[TFALSUM] by A17,A18; for x be Element of l holds P1[x] from HILBERT2:sch 2(A23,A19, A20); then A24: for x be Element of l st x in dom v1 holds P1[x]; dom v1=l by FUNCT_2:def 1 .=dom v2 by FUNCT_2:def 1; hence thesis by A24,PARTFUN1:5; end; end; end; theorem Th24: p 'U' q in Sub.(p 'U' q) proof set puq = p 'U' q; A1: tau1.puq c= tau1.(p '&&' puq) by Th13; puq in {puq} by TARSKI:def 1; then A2: puq in tau1.puq by Def4; tau1.untn(p,q) \/ Sub.p c= tau1.untn(p,q) \/ Sub.p \/ Sub.q by XBOOLE_1:7; then tau1.untn(p,q) c= tau1.untn(p,q) \/ Sub.p & tau1.untn(p,q) \/ Sub.p c= Sub.( puq) by XBOOLE_1:7,Def6; then A3: tau1.untn(p,q) c= Sub.(puq); tau1.(p '&&' puq) c= tau1.untn(p,q) by Th14; then tau1.(p '&&' puq) c= Sub.(puq) by A3; then tau1.puq c= Sub.(puq) by A1; hence thesis by A2; end; theorem Th25: tau1.p c= Sub.p proof defpred P1[Element of l] means tau1.\$1 c= Sub.\$1; set f = TFALSUM; A1: for n holds P1[ prop n] proof let n; set pr = prop n; tau1.pr = {pr} by Def4 .= Sub.pr by Def6; hence thesis; end; A2: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that A3: P1[r]and A4: P1[s]; thus P1[r 'U' s] proof set f = r 'U' s; {f} c= Sub.f by Th24,ZFMISC_1:31; hence thesis by Def4; end; thus P1[r => s] proof set f = r => s; A5: Sub.f = {f} \/ Sub.r \/ Sub.s by Def6; {f} \/ tau1.r c= {f} \/ Sub.r & tau1.f = {f} \/ tau1.r \/ tau1.s by XBOOLE_1: 13,A3, Def4; hence thesis by A5,A4,XBOOLE_1:13; end; end; tau1.f = {f} by Def4 .= Sub.f by Def6; then A6: P1[f]; for p holds P1[p] from HILBERT2:sch 2(A6,A1,A2); hence thesis; end; registration let p; cluster Sub.p -> non empty finite; coherence proof tau1.p c= Sub.p by Th25; hence Sub.p is non empty; defpred P1[Element of l] means Sub.\$1 is finite; A1: for n holds P1[ prop n] proof let n; Sub.(prop n) = {prop n} by Def6; hence thesis; end; A2: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume A3: ( P1[r])& P1[s]; Sub.(r 'U' s) = tau1.untn(r,s) \/ Sub.r \/ Sub.s by Def6; hence P1[r 'U' s] by A3; Sub.(r => s) = {r => s} \/ Sub.r \/ Sub.s by Def6; hence P1[r => s] by A3; end; A4: P1[TFALSUM] by Def6; for p holds P1[p] from HILBERT2:sch 2(A4,A1,A2); hence Sub.p is finite; end; end; theorem p in Sub.(A 'U' B) implies (A 'U' B in Sub.q implies p in Sub.q) proof set aub = A 'U' B,f = TFALSUM; defpred P1[Element of l] means aub in Sub.\$1 implies p in Sub.\$1; A1: for n holds P1[ prop n] proof let n; set pr = prop n; assume aub in Sub.pr; then aub in {pr} by Def6; then aub = pr by TARSKI:def 1; hence thesis by HILBERT2:24; end; assume A2: p in Sub.aub; A3: for r, s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r => s] proof let r,s; assume that A4: P1[r] and A5: P1[s]; thus P1[r 'U' s] proof set f = r 'U' s; A6: tau1.r c= Sub.r by Th25; A7: Sub. f = tau1.untn(r,s) \/ Sub.r \/ Sub.s by Def6; then A8: Sub.s c= Sub.f by XBOOLE_1:7; Sub.r c= tau1.untn(r,s) \/ Sub.r & tau1.untn(r,s) \/ Sub.r c= Sub.f by XBOOLE_1:7, A7; then A9: Sub.r c= Sub.f; assume aub in Sub.f; then A10: aub in tau1.untn(r,s) \/ Sub.r \/ Sub.s by Def6; A11: tau1.s c= Sub.s by Th25; per cases by A10,XBOOLE_0:def 3; suppose A12: aub in tau1.untn(r,s) \/ Sub.r; per cases by A12,XBOOLE_0:def 3; suppose aub in tau1.untn(r,s);then aub in tau1.(('not' s) '&&' ('not' (r '&&' f))) by Th9;then aub in tau1.('not' s) or aub in tau1.('not' (r '&&' f)) by Th10; then A13: aub in tau1.s or aub in tau1.(r '&&' f) by Th9; per cases by A13,Th10; suppose A14: aub in tau1.r or aub in tau1.s; per cases by A14; suppose aub in tau1.r; hence p in Sub.f by A6,A4,A9; end; suppose aub in tau1.s; hence p in Sub.f by A11,A5,A8; end; end; suppose aub in tau1.f; then aub in {f} by Def4; hence p in Sub.f by TARSKI:def 1,A2; end; end; suppose aub in Sub.r; hence p in Sub.f by A4,A9; end; end; suppose aub in Sub.s; hence p in Sub.f by A5,A8; end; end; thus P1[r => s] proof set f = r => s; A15: Sub.f = {f} \/ Sub.r \/ Sub.s by Def6; then A16: Sub.s c= Sub.f by XBOOLE_1:7; Sub.r c= {f} \/ Sub.r & {f} \/ Sub.r c= Sub.f by XBOOLE_1:7, A15; then A17: Sub.r c= Sub.f; assume aub in Sub.f; then A18: aub in {f} \/ Sub.r \/ Sub.s by Def6; per cases by A18,XBOOLE_0:def 3; suppose A19: aub in {f} \/ Sub.r; per cases by A19,XBOOLE_0:def 3; suppose aub in {f}; then aub = f by TARSKI:def 1; hence p in Sub.f by HILBERT2:22; end; suppose aub in Sub.r; hence p in Sub.f by A4,A17; end; end; suppose aub in Sub.s; hence p in Sub.f by A5,A16; end; end; end; A20: P1[f] proof assume aub in Sub.f; then aub in {f} by Def6; then aub = f by TARSKI:def 1; hence thesis by HILBERT2:23; end; for p holds P1[p] from HILBERT2:sch 2(A20,A1,A3); hence thesis; end; definition let X; func Subt X -> Subset of bool LTLB_WFF equals {Sub.A where A is Element of LTLB_WFF: A in X}; correctness proof set s = {Sub.A where A is Element of l: A in X}; s c= bool l proof let x be object; assume x in s; then ex A st x = Sub.A & A in X; hence x in bool l; end; hence thesis; end; end; registration let X be finite Subset of LTLB_WFF; cluster Subt X -> finite finite-membered; coherence proof deffunc F(Element of l) = Sub.\$1; A1: X is finite; {F(A) where A is Element of l: A in X} is finite from FRAENKEL:sch 21(A1); hence Subt X is finite; let x;assume x in Subt X; then ex A st x = Sub.A & A in X; hence x is finite; end; end; begin definition mode PNPair is Element of [:LTLB_WFF**,LTLB_WFF**:]; end; set pairs = [:l**,l**:]; reserve P,Q,P1,R for PNPair; definition let P; redefine func P`1 -> one-to-one FinSequence of LTLB_WFF; coherence proof consider x, y being object such that x in l** and y in l** and A1: P = [x,y] by ZFMISC_1:def 2; P`1 = [x,y]`1 by A1 .= x; hence thesis by Def2; end; redefine func P`2 -> one-to-one FinSequence of LTLB_WFF; coherence proof consider x, y being object such that x in l** and y in l** and A2: P = [x,y] by ZFMISC_1:def 2; P`2 = [x,y]`2 by A2 .= y; hence thesis by Def2; end; end; definition let P; func rng P -> finite Subset of LTLB_WFF equals rng P`1 \/ rng P`2; correctness; end; definition let fp,fm be one-to-one FinSequence of LTLB_WFF; redefine func [fp,fm] -> PNPair; coherence proof fp in l** & fm in l** by Def2; hence [fp,fm] is PNPair by ZFMISC_1:def 2; end; end; definition let P; func P^ -> Element of LTLB_WFF equals (con (P`1))/.len (con (P`1)) '&&' (con nega (P`2))/.len (con nega (P`2)); correctness; end; theorem Th27: [<*>LTLB_WFF,<*>LTLB_WFF]^ = TVERUM '&&' TVERUM proof len <*>l = 0; then len nega <*>l = 0 by LTLAXIO2:def 4; then nega <*>l = 0; hence [<*>l,<*>l]^ = TVERUM '&&' TVERUM by LTLAXIO2:10; end; theorem Th28: A in rng P`1 implies {} LTLB_WFF |- (P^) => A proof set fp = P`1,fm = P`2,nfm = nega fm; assume A in rng fp; then consider i being Nat such that A1: i in dom fp and A2: fp . i = A by FINSEQ_2:10; (P^) => A is ctaut proof let g; set v = VAL g,r = v.kon(fp|(i -' 1)),s = v.kon(fp/^i); A3: v.A = 1 or v.A = 0 by XBOOLEAN:def 3; thus v.((P^) => A) = v.(P^) => v.A by LTLAXIO1:def 15 .= (v.kon(fp) '&' v.kon(nfm)) => v.A by LTLAXIO1:31 .= (r '&' v.(fp/.i) '&' s '&' v.kon(nfm)) => v.A by LTLAXIO2:18, A1 .= ((r '&' v.A '&' s) '&' v.kon(nfm)) => v.A by PARTFUN1:def 6, A1, A2 .= 1 by A3; end; then (P^) => A in LTL_axioms by LTLAXIO1:def 17; hence {} l |- (P^) => A by LTLAXIO1:42; end; theorem Th29: A in rng P`2 implies {} LTLB_WFF |- (P^) => 'not' A proof set fp = P`1,fm = P`2,nfm = nega fm; assume A in rng fm; then consider i being Nat such that A1: i in dom fm and A2: fm . i = A by FINSEQ_2:10; reconsider i as Element of NAT by ORDINAL1:def 12; i <= len fm by A1,FINSEQ_3:25; then A3: i <= len nfm by LTLAXIO2:def 4; 1 <= i by A1,FINSEQ_3:25; then A4: i in dom nfm by A3,FINSEQ_3:25; (P^) => 'not' A is ctaut proof let g; set v = VAL g,p = v.kon(fp),q = v.kon(nfm), r = v.kon(nfm|(i -' 1)), s = v.kon(nfm/^i); A5: v.('not' A) = 1 or v.('not' A) = 0 by XBOOLEAN:def 3; A6: q = r '&' v.(nfm/.i) '&' s by LTLAXIO2:18,A4 .= r '&' v.('not' (fm/.i)) '&' s by LTLAXIO2:8,A1 .= r '&' v.('not' A) '&' s by PARTFUN1:def 6,A1,A2; thus v.((P^) => ('not' A)) = v.(P^) => v.('not' A) by LTLAXIO1:def 15 .= (p '&' q) => v.('not' A) by LTLAXIO1:31 .= 1 by A5,A6; end; then (P^) => 'not' A in LTL_axioms by LTLAXIO1:def 17; hence {} l |- (P^) => ('not' A) by LTLAXIO1:42; end; definition let P; attr P is Inconsistent means :Def10: {} LTLB_WFF |- 'not' (P^); end; notation let P; antonym P is consistent for P is Inconsistent; end; definition let P; attr P is complete means tau rng P = rng P; end; registration cluster [<*> LTLB_WFF,<*> LTLB_WFF] -> consistent for PNPair; coherence proof let P; assume A1: P = [<*>l,<*>l]; not {} l |= 'not' (P^) proof reconsider M = NAT --> {} as LTLModel by Th2; set s = SAT M; take M; thus M |= {} l; s.[0,'not' (P^)] <> 1 proof assume s.[0,'not' (P^)] = 1; then s.[0,P^] = 0 by LTLAXIO1:5; then s.[0,TVERUM] <> 1 by LTLAXIO1:7, A1,Th27; hence contradiction by LTLAXIO1:6; end; hence not M |= 'not' (P^); end; hence P is consistent by LTLAXIO1:41; end; end; registration cluster [<*> LTLB_WFF,<*> LTLB_WFF] -> complete for PNPair; coherence proof let P; assume A1: P = [<*>l,<*>l]; then A2: rng P`1 = {}; rng P`2 = {} by A1; then tau rng P = rng P by A2; hence P is complete; end; end; registration cluster consistent complete for PNPair; existence proof set p = [<*>l,<*>l]; take p; thus thesis; end; end; registration let P be consistent PNPair; cluster [P`1,P`2] -> consistent for PNPair; coherence proof let a be PNPair; assume a = [P`1,P`2];then A1: a`1 = P`1 & a`2 = P`2; not {}l |- 'not' (P^) by Def10; then not {}l |- 'not' (a^) by A1; hence a is consistent; end; end; begin theorem for P be consistent PNPair holds rng P`1 misses rng P`2 proof let P be consistent PNPair; assume not rng P`1 misses rng P`2; then not rng P`1 /\ rng P`2 = {}; then consider x being object such that A1: x in rng P`1 /\ rng P`2 by XBOOLE_0:def 1; x in rng P`1 by XBOOLE_0:def 4,A1; then consider n1 be object such that A2: n1 in dom P`1 and A3: P`1.n1 = x by FUNCT_1:def 3; x in rng P`2 by XBOOLE_0:def 4,A1; then consider n2 be object such that A4: n2 in dom P`2 and A5: P`2.n2 = x by FUNCT_1:def 3; reconsider n1,n2 as Element of NAT by A2,A4; x = P`2/.n2 by PARTFUN1:def 6,A4,A5; then reconsider x as Element of l; A6: 1<=n2 by FINSEQ_3:25,A4; A7: n2 <= len P`2 by FINSEQ_3:25,A4; 'not' (P^) is ctaut proof let g; set nP2 = nega P`2,v = VAL g; A8: v.x = TRUE or v.x = FALSE by XBOOLEAN:def 3; A9: v.(P`1/.n1) = v.x by PARTFUN1:def 6,A2,A3; n2 <= len nP2 by A7,LTLAXIO2:def 4; then A10: n2 in dom nP2 by FINSEQ_3:25,A6; A11: v.(nP2/.n2) = v.('not' ((P`2)/.n2)) by LTLAXIO2:8,A4 .= v.('not' x) by A4,A5,PARTFUN1:def 6 .= v.x => v.TFALSUM by LTLAXIO1:def 15 .= v.x => FALSE by LTLAXIO1:def 15; A12: v.(P^) = v.kon(P`1) '&' v.kon(nega P`2) by LTLAXIO1:31 .= v.kon(P`1|(n1-'1)) '&' v.(P`1/.n1) '&' v.kon(P`1/^n1)'&'v.kon(nP2) by LTLAXIO2:18,A2 .= v.kon(P`1|(n1-'1)) '&' v.(P`1/.n1) '&' v.kon(P`1/^n1) '&' (v.kon(nP2|(n2-'1)) '&' v.(nP2/.n2) '&' v.kon(nP2/^n2)) by LTLAXIO2:18,A10 .= 0 by A8,A11,A9; thus v.('not' (P^)) = v.(P^) => v.TFALSUM by LTLAXIO1:def 15 .= 1 by A12; end; then 'not' (P^) in LTL_axioms by LTLAXIO1:def 17; then {} l |- 'not' (P^) by LTLAXIO1:42; hence contradiction by Def10; end; theorem Th31: for P be consistent PNPair st not A in rng P holds ([(P`1)^^<*A*>,P`2] is consistent or [P`1,(P`2)^^<*A*>] is consistent) proof let P be consistent PNPair; set fpa = P`1^^<*A*>,fma = P`2^^<*A*>,Pl = [fpa,P`2],Pr = [P`1,fma], np = 'not' (P^),npl = 'not' (Pl^),npr = 'not' (Pr^),na= <*'not' A*>; assume A1: not A in rng P; then not A in rng P`1 by XBOOLE_0:def 3; then rng P`1 misses {A} by ZFMISC_1:50; then rng P`1 misses rng <*A*> by FINSEQ_1:39; then A2: fpa = P`1^<*A*> by Def3; not A in rng P`2 by A1,XBOOLE_0:def 3; then rng P`2 misses {A} by ZFMISC_1:50; then rng P`2 misses rng <*A*> by FINSEQ_1:39; then fma = P`2^<*A*> by Def3; then A3: nega fma = (nega P`2)^<*'not' A*> by LTLAXIO2:15; npl => (npr => np) is ctaut proof let g; set v = VAL g,vf = v.TFALSUM; A4: vf = 0 by LTLAXIO1:def 15; set p = (v.(P^) '&' v.A) => vf,q = ((v.(P^) '&' (v.A => vf)) => vf); A5: v.A = 1 or v.A = 0 by XBOOLEAN:def 3; A6: v.(Pr^) = v.kon(P`1) '&' v.kon(nega fma) by LTLAXIO1:31 .= v.kon(P`1) '&' (v.kon(nega P`2) '&' v.kon(na)) by LTLAXIO2:17,A3 .= v.kon(P`1) '&' v.kon(nega P`2) '&' v.kon(na) .= v.(P^) '&' v.kon(na) by LTLAXIO1:31 .= v.(P^) '&' v.('not' A) by LTLAXIO2:11 .= v.(P^) '&' (v.A => vf) by LTLAXIO1:def 15; A7: v.(Pl^) = v.kon(fpa) '&' v.kon(nega P`2) by LTLAXIO1:31 .= v.kon(P`1) '&' v.kon(<*A*>) '&' v.kon(nega P`2) by LTLAXIO2:17,A2 .= v.kon(P`1) '&' v.A '&' v.kon(nega P`2) by LTLAXIO2:11 .= v.kon(P`1) '&' v.kon(nega P`2) '&' v.A .= v.(P^) '&' v.A by LTLAXIO1:31; A8: v.(P^) = 1 or v.(P^) = 0 by XBOOLEAN:def 3; thus v.(npl => (npr => np)) = v.npl => v.(npr => np) by LTLAXIO1:def 15 .= v.npl => (v.npr => v.np) by LTLAXIO1:def 15 .= p => (v.npr => v.np) by A7,LTLAXIO1:def 15 .= p => (q => v.np) by A6,LTLAXIO1:def 15 .= 1 by A8,A5,A4,LTLAXIO1:def 15; end; then npl => (npr => np) in LTL_axioms by LTLAXIO1:def 17; then A9: {} l |- npl => (npr => np) by LTLAXIO1:42; assume that A10: Pl is Inconsistent and A11: Pr is Inconsistent; {} l |- npl by A10; then A12: {} l |- (npr => np) by A9,LTLAXIO1:43; {} l |- npr by A11; hence contradiction by A12,Def10,LTLAXIO1:43; end; theorem for P be consistent PNPair holds not TFALSUM in rng P`1 proof let P be consistent PNPair; assume TFALSUM in rng P`1; then {}l |- 'not' (P^) by Th28; hence contradiction by Def10; end; theorem for P be consistent PNPair st A in rng P & B in rng P & A => B in rng P holds (A => B in rng P`1 iff (A in rng P`2 or B in rng P`1)) proof let P be consistent PNPair; assume that A1: A in rng P and A2: B in rng P and A3: A => B in rng P; set p = P^,pa = p => A, pna = p => 'not' A,pb = p => B,pnb = p => 'not' B, pab = p => (A => B),pnab = p => 'not' (A => B), np = 'not' p; hereby pa => (pnb => (pab => np)) is ctaut proof let g; set v = VAL g,vf = v.TFALSUM; A4: v.A = 1 or v.A = 0 by XBOOLEAN:def 3; A5: v.B = 1 or v.B = 0 by XBOOLEAN:def 3; A6: v.p = 1 or v.p = 0 by XBOOLEAN:def 3; A7: vf = 0 & v.pa = v.p => v.A by LTLAXIO1:def 15; A8: v.pab = v.p => v.(A => B) by LTLAXIO1:def 15 .= v.p => (v.A => v.B) by LTLAXIO1:def 15; A9: v.pnb = v.p => v.('not' B) by LTLAXIO1:def 15 .= v.p => (v.B => vf) by LTLAXIO1:def 15; thus v.(pa => (pnb => (pab => np))) = v.pa => v.(pnb => (pab => np)) by LTLAXIO1: def 15 .= v.pa => (v.pnb => v.(pab => np)) by LTLAXIO1:def 15 .= v.pa => (v.pnb => (v.pab => v.np)) by LTLAXIO1:def 15 .= 1 by A4,A5,A6,A7,A8, LTLAXIO1:def 15,A9; end; then pa => (pnb => (pab => np)) in LTL_axioms by LTLAXIO1:def 17; then A10: {} l |- pa => (pnb => (pab => np)) by LTLAXIO1:42; assume A => B in rng P`1; then A11: {} l |- pab by Th28; assume that A12: not A in rng P`2 and A13: not B in rng P`1; B in rng P`2 by A13,A2,XBOOLE_0:def 3; then A14: {} l |- pnb by Th29; A in rng P`1 by A12,A1,XBOOLE_0:def 3; then {} l |- pa by Th28; then {} l |- pnb => (pab => np) by A10,LTLAXIO1:43; then {} l |- pab => np by LTLAXIO1:43,A14; hence contradiction by LTLAXIO1:43,A11,Def10; end; assume A15: A in rng P`2 or B in rng P`1; assume not A => B in rng P`1; then A => B in rng P`2 by XBOOLE_0:def 3,A3; then A16: {} l |- pnab by Th29; per cases by A15; suppose A17: A in rng P`2; pna => (pnab => np) is ctaut proof let g; set v = VAL g,vf = v.TFALSUM; A18: vf = 0 by LTLAXIO1:def 15; A19: v.A = 1 or v.A = 0 by XBOOLEAN:def 3; A20: v.p = 1 or v.p = 0 by XBOOLEAN:def 3; A21: v.pna = v.p => v.('not' A) by LTLAXIO1:def 15 .= v.p => (v.A => vf) by LTLAXIO1:def 15; A22: v.pnab = v.p => v.('not' (A => B)) by LTLAXIO1:def 15 .= v.p => (v.(A => B) => vf) by LTLAXIO1:def 15 .= v.p => (v.A => v.B => vf) by LTLAXIO1:def 15; thus v.(pna => (pnab => np)) = v.pna => v.(pnab => np) by LTLAXIO1:def 15 .= v.pna => (v.pnab => v.np) by LTLAXIO1:def 15 .= 1 by A19,A20,A18,LTLAXIO1:def 15,A21,A22; end; then pna => (pnab => np) in LTL_axioms by LTLAXIO1:def 17; then A23: {} l |- pna => (pnab => np) by LTLAXIO1:42; {} l |- pna by A17,Th29; then {} l |- pnab => np by A23,LTLAXIO1:43; hence contradiction by LTLAXIO1:43,A16,Def10; end; suppose A24: B in rng P`1; pb => (pnab => np) is ctaut proof let g; set v = VAL g,vf = v.TFALSUM; A25: v.B = 1 or v.B = 0 by XBOOLEAN:def 3; A26: v.p = 1 or v.p = 0 by XBOOLEAN:def 3; A27: vf = 0 & v.pb = v.p => v.B by LTLAXIO1:def 15; A28: v.pnab = v.p => v.('not' (A => B)) by LTLAXIO1:def 15 .= v.p => (v.(A => B) => vf) by LTLAXIO1:def 15 .= v.p => (v.A => v.B => vf) by LTLAXIO1:def 15; thus v.(pb => (pnab => np)) = v.pb => v.(pnab => np) by LTLAXIO1:def 15 .= v.pb => (v.pnab => v.np) by LTLAXIO1:def 15 .= 1 by A25,A26,A27,LTLAXIO1:def 15,A28; end; then pb => (pnab => np) in LTL_axioms by LTLAXIO1:def 17; then A29: {} l |- pb => (pnab => np) by LTLAXIO1:42; {} l |- pb by A24,Th28; then {} l |- pnab => np by A29,LTLAXIO1:43; hence contradiction by LTLAXIO1:43,A16,Def10; end; end; theorem for P be consistent PNPair ex P1 be consistent PNPair st rng (P`1) c= rng (P1`1) & rng (P`2) c= rng (P1`2) & tau rng P = rng P1 proof let P be consistent PNPair; set tfp = tau rng P \ rng P; consider t be FinSequence such that A1: rng t = tfp and A2: t is one-to-one by FINSEQ_4:58; reconsider t as one-to-one FinSequence of l by FINSEQ_1:def 4,A1,A2; defpred Pr[Nat,Element of [:l**,l**:],Element of [:l**,l**:]] means \$2 is consistent implies ( ([(\$2`1)^^<*t/.\$1*>,\$2`2] is consistent implies \$3 = [(\$2`1)^^<*t/.\$1*>,\$2`2]) & (not [(\$2`1)^^<*t/.\$1*>,\$2`2] is consistent implies \$3 = [\$2`1,(\$2`2)^^<*t/.\$1*>]) ); A3: now let n be Nat; assume that 1 <= n and n <= len t + 1-1; let x being Element of [:l**,l**:]; [(x`1)^^<*t/.n*>,(x`2)] is consistent or not [(x`1)^^<*t/.n*>,(x`2)] is consistent; hence ex y being Element of [:l**,l**:] st Pr[n,x,y]; end; consider pn be FinSequence of [:l**,l**:] such that A4: len pn = len t + 1 & (pn/.1 = P or len t + 1 = 0) & for n being Nat st 1 <= n & n <= len t + 1 - 1 holds Pr[n,pn/.n,pn/.(n + 1)] from RECDEF_1:sch 18(A3); defpred Pr1[Nat] means \$1 <= len pn implies (\$1 <= len t implies rng (pn/.\$1) misses (rng <*t/.\$1*> \/ rng (t/^\$1))) & pn/.\$1 is consistent & rng P c= rng (pn/.\$1); A5: for k being non zero Nat st Pr1[k] holds Pr1[k + 1] proof let k being non zero Nat; reconsider k1 = k as Element of NAT by ORDINAL1:def 12; A6: 1 <= k by NAT_1:25; A7: k+1 > k by NAT_1:13; assume A8: Pr1[k]; A9: 1 <= k+1 by NAT_1:25; thus Pr1[k + 1] proof t/.k1 in {t/.k1} by TARSKI:def 1; then A10: t/.k1 in rng <*t/.k1*> by FINSEQ_1:39; assume A11: k+1 <= len pn; then reconsider P1 = pn/.k1 as consistent PNPair by NAT_1:13,A8; set pp = [(P1`1)^^<*t/.k1*>,P1`2],pp2 = [P1`1,(P1`2)^^<*t/.k1*>]; A12: rng P1 misses rng (t/^k1) by XBOOLE_1:7,XBOOLE_1:63, A8, A4, A11,XREAL_1: 6,NAT_1:13; rng P1 misses rng <*t/.k1*> by XBOOLE_1:63, XBOOLE_1:7, A8, A4,A11,XREAL_1:6,NAT_1:13; then A13: rng P1`2 misses rng <*t/.k1*> by XBOOLE_1:7,XBOOLE_1:63; A14: rng P1 misses rng <*t/.k1*> by XBOOLE_1:7,XBOOLE_1:63, A8, A4, A11,XREAL_1: 6,NAT_1:13; then A15: rng P1`1 misses rng <*t/.k1*> by XBOOLE_1:7,XBOOLE_1:63; rng P1 /\ rng <*t/.k1*> = {} by A14; then A16: not t/.k1 in rng (P1) by A10,XBOOLE_0:def 4; A17: k+1+(-1) <= len t + 1+(-1) by A4,A11,XREAL_1:6; then A18: k in dom t by FINSEQ_3:25,A6; A19: Pr[k1,P1,pn/.(k1 + 1)] by A4,A6, A17; set r1 = [((P1`1)^^<*t/.k1*>),pp`2],r2 = [pp2`1,(P1`2)^^<*t/.k1*>]; per cases; suppose A20: pp is consistent;then A21: rng (pn/.(k+1)) = rng r1`1 \/ rng r1`2 by A19 .= rng ((P1`1)^<*t/.k1*>) \/ rng P1`2 by Def3,A15 .= rng P1`1 \/ rng <*t/.k1*> \/ rng P1`2 by FINSEQ_1:31 .= rng P1 \/ rng <*t/.k1*> by XBOOLE_1:4; thus k+1 <= len t implies rng (pn/.(k+1)) misses rng <*t/.(k+1)*> \/ rng (t/^(k+1)) proof assume A22: k+1 <= len t; then <*t.(k+1)*> ^(t/^(k+1)) = t/^k by Th1;then rng <*t.(k+1)*> \/ rng (t/^(k+1)) = rng (t/^k) by FINSEQ_1:31; then A23: rng (t/^(k+1)) c= rng (t/^k) by XBOOLE_1:7; k+1 in dom t by FINSEQ_3:25,A22,A9;then {t/.(k+1)} c= rng (t/^k) by FINSEQ_6:58,A7,ZFMISC_1:31; then rng <*t/.(k+1)*> c= rng (t/^k) by FINSEQ_1:39;then A24: rng (t/^(k+1)) \/ rng <*t/.(k+1)*> c= rng (t/^k) \/ rng (t/^k) by XBOOLE_1:13,A23; k1 in Seg k1 by A6; then t.k1 in rng (t|(Seg k)) by FUNCT_1:50,A18; then t/.k1 in rng (t|k) by PARTFUN1:def 6,A18; then {t/.k1} c= rng (t|k) by ZFMISC_1:31; then rng <*t/.k1*> c= rng (t|k) by FINSEQ_1:39;then A25: rng <*t/.k1*> misses (rng <*t/.(k+1)*> \/ rng (t/^(k+1))) by FINSEQ_5:34,XBOOLE_1:64,A24; rng (pn/.(k+1)) /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1))) = (rng P1 /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1)))) \/ (rng <*t /.k1*> /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1)))) by XBOOLE_1:23,A21 .= {} \/ (rng <*t/.k1*> /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1)))) by A24,XBOOLE_1:63,A12,XBOOLE_0:def 7 .= {} by A25; hence rng (pn/.(k+1)) misses rng <*t/.(k+1)*> \/ rng (t/^(k+1)); end; thus pn/.(k+1) is consistent by A4,A6, A17,A20; rng (pn/.k) c= rng (pn/.(k+1)) by XBOOLE_1:7,A21; hence rng P c= rng (pn/.(k+1)) by A8, A11,NAT_1:13; end; suppose not pp is consistent;then A26: rng (pn/.(k+1)) = rng r2`1 \/ rng r2`2 by A19 .= rng (P1`1) \/ rng ((P1`2)^<*t/.k1*>) by Def3,A13 .= rng (P1`1) \/ (rng (P1`2) \/ rng <*t/.k1*>) by FINSEQ_1:31 .= rng (P1) \/ rng <*t/.k1*> by XBOOLE_1:4; thus k+1 <= len t implies rng (pn/.(k+1)) misses rng <*t/.(k+1)*> \/ rng (t/^(k+1)) proof assume A27: k+1 <= len t; then <*t.(k+1)*> ^(t/^(k+1)) = t/^k by Th1;then rng <*t.(k+1)*> \/ rng (t/^(k+1)) = rng (t/^k) by FINSEQ_1:31; then A28: rng (t/^(k+1)) c= rng (t/^k) by XBOOLE_1:7; k+1 in dom t by FINSEQ_3:25,A27,A9; then {t/.(k+1)} c= rng (t/^k) by FINSEQ_6:58,A7,ZFMISC_1:31; then rng <*t/.(k+1)*> c= rng (t/^k) by FINSEQ_1:39;then A29: rng (t/^(k+1)) \/ rng <*t/.(k+1)*> c= rng (t/^k) \/ rng (t/^k) by XBOOLE_1:13,A28; k1 in Seg k1 by A6; then t.k1 in rng (t|(Seg k)) by FUNCT_1:50,A18; then t/.k1 in rng (t|k) by PARTFUN1:def 6,A18; then {t/.k1} c= rng (t|k) by ZFMISC_1:31; then rng <*t/.k1*> c= rng (t|k) by FINSEQ_1:39;then A30: rng <*t/.k1*> misses (rng <*t/.(k+1)*> \/ rng (t/^(k+1))) by FINSEQ_5:34,XBOOLE_1:64,A29; rng (pn/.(k+1)) /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1))) = (rng P1 /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1)))) \/ (rng <*t /.k1*> /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1)))) by XBOOLE_1:23,A26 .= {} \/ (rng <*t/.k1*> /\ (rng <*t/.(k+1)*> \/ rng (t/^(k+1)))) by A29,XBOOLE_1:63,A12,XBOOLE_0:def 7 .= {} by A30; hence rng (pn/.(k+1)) misses rng <*t/.(k+1)*> \/ rng (t/^(k+1)); end; thus pn/.(k+1) is consistent by A19, Th31,A16; rng (pn/.k) c= rng (pn/.(k+1)) by XBOOLE_1:7,A26; hence rng P c= rng (pn/.(k+1)) by A8, A11,NAT_1:13; end; end; end; reconsider lpn = len pn as non zero Nat by A4; A31: Pr1[1] proof assume 1 <= len pn; thus 1 <= len t implies rng (pn/.1) misses (rng <*t/.1*> \/ rng (t/^1)) proof assume 1 <= len t; then A32: t <> {}; rng <*t/.1*> \/ rng (t/^1) = rng (<*t/.1*>^(t/^1)) by FINSEQ_1:31 .= rng (t:- (t/.1)) by FINSEQ_6:43,A32 .= rng t by FINSEQ_6:44,A32; hence thesis by A4, XBOOLE_1:79,A1; end; thus pn/.1 is consistent by A4; thus rng P c= rng (pn/.1) by A4; end; A33: for k be non zero Nat holds Pr1[k] from NAT_1:sch 10(A31, A5); then pn/.lpn is consistent; then reconsider P2 = pn/.len pn as consistent PNPair; set i2 = len pn -' 1,P3 = pn/.lpn; A34: len pn -' i2 = len pn -' (len pn - 1) by A4,XREAL_0:def 2 .= len pn - (len pn - 1) by XREAL_0:def 2 .= 1; defpred Pr6[Nat] means \$1 < len pn implies rng ((pn/.(len pn -' \$1))`1) c= rng P2`1 & rng ((pn/.(len pn -' \$1))`2) c= rng P2`2; A35: now let n; assume that A36: 1 <= n and A37: n <= len t; n <= len pn by A37,NAT_1:13,A4; then rng (pn/.n) misses (rng <*t/.n*> \/ rng (t/^n)) by A33, A36, A37; then A38: rng (pn/.n) misses rng <*t/.n*> by XBOOLE_1:7,XBOOLE_1:63; hence rng (pn/.n)`1 misses rng <*t/.n*> by XBOOLE_1:7,XBOOLE_1:63; thus rng (pn/.n)`2 misses rng <*t/.n*> by XBOOLE_1:7,XBOOLE_1:63, A38; end; A39: now let n be Nat; set k = len pn -' (n+1); assume A40: Pr6[n]; thus Pr6[n+1] proof assume A41: n+1 < len pn; then A42: n+1 + (-1) < len pn by XREAL_1:36; then A43: n + (-n) < len pn + (-n) by XREAL_1:8; A44: n+1 + (-(n+1)) < len pn + (-(n+1)) by A41,XREAL_1:8; then A45: k = len pn - (n+1) by XREAL_0:def 2 .= len t - n by A4; A46: len pn - (n+1) > 0 by A44; then len pn -' (n+1) > 0 by XREAL_0:def 2; then A47: 1 <= k by NAT_1:25; reconsider k as non zero Element of NAT by XREAL_0:def 2,A46; set P1 = pn/.k; A48: len t >= len t + (-n) by XREAL_1:32; then A49: rng P1`2 misses rng <*t/.k*> by A35,A47,A45; A50: rng P1`1 misses rng <*t/.k*> by A35,A47, A48,A45; A51: k+1 = len pn - (n+1) + 1 by XREAL_0:def 2 .= len pn - n .= len pn -' n by XREAL_0:def 2, A43; k < len pn by A4,NAT_1:13, A48,A45; then A52: pn/.k is consistent PNPair by A33; per cases; suppose [(P1`1)^^<*t/.k*>,P1`2] is consistent;then A53: pn/.(k+1) = [(P1`1)^^<*t/.k*>,P1`2] by A47, A48,A45, A4,A52;then rng ((P1`1)^^<*t/.k*>) c= rng P2`1 by A40, A42, A51; then rng ((P1`1)^<*t/.k*>) c= rng P2`1 by A50,Def3; then A54: rng P1`1 \/ rng <*t/.k*> c= rng P2`1 by FINSEQ_1:31; rng P1`1 c= rng (P1`1) \/ rng <*t/.k*> by XBOOLE_1:7; hence thesis by A40, A42, A51,A53,A54; end; suppose not [(P1`1)^^<*t/.k*>,P1`2] is consistent;then A55: pn/.(k+1) = [P1`1,(P1`2)^^<*t/.k*>] by A47, A48,A45,A4,A52;then rng ((P1`2)^^<*t/.k*>) c= rng P2`2 by A40, A42, A51; then rng ((P1`2)^<*t/.k*>) c= rng P2`2 by A49,Def3; then A56: rng P1`2 \/ rng <*t/.k*> c= rng P2`2 by FINSEQ_1:31; rng P1`2 c= rng P1`2 \/ rng <*t/.k*> by XBOOLE_1:7; hence thesis by A56, A55, A40, A42, A51; end; end; end; A57: Pr6[0] proof assume 0 < len pn; then len pn - 0 > 0; hence thesis by XREAL_0:def 2; end; A58: for n being Nat holds Pr6[n] from NAT_1:sch 2(A57,A39); then A59: len pn + (-1) < len pn & Pr6[i2] by XREAL_1:30; A60: tau rng P c= rng P2 proof let x be object; assume x in tau rng P; then A61: x in tfp \/ rng P by XBOOLE_1:45, Th16; per cases by A61,XBOOLE_0:def 3; suppose x in tfp; then consider i being Nat such that A62: i in dom t and A63: t.i = x by A1,FINSEQ_2:10; reconsider i1 = i as Element of NAT by ORDINAL1:def 12; set P5 = pn/.i1; A64: i <= len t + 1-1 by FINSEQ_3:25,A62; then A65: i < len pn by A4,NAT_1:13; reconsider ii = len pn -' (i+1) as Element of NAT; set P3 = pn/.(len pn -' ii); (-1)*(i+1) < (-1)*0 by XREAL_1:69; then A66: len pn + (-(i+1)) < len pn by XREAL_1:30; A67: 1 <= i by FINSEQ_3:25,A62; then A68: Pr[i1,pn/.i1,pn/.(i1+1)] by A64,A4; A69: i <= len t by FINSEQ_3:25,A62; then A70: rng P5`1 misses rng <*t/.i*> by A35,A67; A71: rng P5`2 misses rng <*t/.i*> by A35,A67,A69; i+1 <= len pn by XREAL_1:6,A69,A4; then i+1 + (-(i+1)) <= len pn + (-(i+1)) by XREAL_1:6; then A72: ii = len pn - (i+1) by XREAL_0:def 2;then A73: len pn -' ii = len pn - (len pn - (i+1)) by XREAL_0:def 2 .= i + 1; Pr6[len pn -' (i+1)] by A58; then A74: rng P3 c= rng P2 by A66,A72,XBOOLE_1:13; per cases; suppose A75: [(P5`1)^^<*t/.i*>,P5`2] is consistent; rng <*t/.i*> c= rng P5`1 \/ rng <*t/.i*> by XBOOLE_1:7; then rng <*t/.i*> c= rng ((P5`1)^<*t/.i*>) by FINSEQ_1:31; then rng <*t/.i*> c= rng ((P5`1)^<*t/.i*>) \/ rng P5`2 by XBOOLE_1:10;then rng <*t/.i*> c= rng ((P5`1)^^<*t/.i*>) \/ rng P5`2 by A70,Def3;then rng <*t/.i*> c= rng P3`1 \/ rng P5`2 by A73, A75, A33,A65,A67,A68;then rng <*t/.i*> c= rng P3 by A75, A33,A65,A67,A68,A73; then A76: rng <*t/.i*> c= rng P2 by A74; t/.i in {t/.i} by TARSKI:def 1; then t/.i in rng <*t/.i*> by FINSEQ_1:38; then t/.i in rng P2 by A76; hence x in rng P2 by A62,A63,PARTFUN1:def 6; end; suppose A77: not [(P5`1)^^<*t/.i*>,P5`2] is consistent; mg:P3 = [P5`1,(P5`2)^^<*t/.i*>] by A77,A33,A65,A67,A68,A73; rng <*t/.i*> c= rng P5`2 \/ rng <*t/.i*> by XBOOLE_1:7; then rng <*t/.i*> c= rng ((P5`2)^<*t/.i*>) by FINSEQ_1:31; then rng <*t/.i*> c= rng P5`1 \/ rng ((P5`2)^<*t/.i*>) by XBOOLE_1:10;then rng <*t/.i*> c= rng P5`1 \/ rng ((P5`2)^^<*t/.i*>) by A71,Def3;then rng <*t/.i*> c= rng P5`1 \/ rng P3`2 by mg;then rng <*t/.i*> c= rng P3 by mg; then A78: rng <*t/.i*> c= rng P2 by A74; t/.i in {t/.i} by TARSKI:def 1; then t/.i in rng <*t/.i*> by FINSEQ_1:38; then t/.i in rng P2 by A78; hence x in rng P2 by A62,A63,PARTFUN1:def 6; end; end; suppose A79: x in rng P; rng P c= rng (pn/.len pn) by A33,A4; hence x in rng P2 by A79; end; end; defpred Pr4[Nat] means \$1 <= len pn implies rng ((pn/.\$1)`1) \/ rng ((pn/.\$1)`2) c= tau rng P; A80: tfp c= tau rng P by XBOOLE_1:36; A81: for k being non zero Nat st Pr4[k] holds Pr4[k + 1] proof let k being non zero Nat; reconsider k1 = k as Element of NAT by ORDINAL1:def 12; A82: 1 <= k by NAT_1:25; assume A83: Pr4[k]; thus Pr4[k + 1] proof set P1 = pn/.k1; set P4 = pn/.k; assume A84: k+1 <= len pn; then A85: k+1+(-1) <= len t + 1 +(-1) by A4,XREAL_1:6; then A86: rng P1`2 misses rng <*t/.k*> by A35,A82; A87: rng P1`1 misses rng <*t/.k*> by A35,A82, A85; k < len pn by A84,NAT_1:13; then A88: pn/.k1 is consistent by A33; A89: {t/.k1} c= tau(rng P) proof let x be object; A90: k1 in dom t by FINSEQ_3:25,A82, A85; then t.k1 in rng t by FUNCT_1:3; then A91: t/.k1 in rng t by PARTFUN1:def 6,A90; assume x in {t/.k1}; then x in rng t by A91,TARSKI:def 1; hence thesis by A1,A80; end; per cases; suppose A92: [(P1`1)^^<*t/.k1*>,P1`2] is consistent; set P3 = pn/.(k1+1); A93: pn/.(k1+1) = [(P1`1)^^<*t/.k1*>,P1`2] by A92, A85,A4,A82,A88; then A94: rng P3`2 = rng P4`2; rng P3`1 = rng ((P1`1)^^<*t/.k1*>) by A93 .= rng ((P1`1)^<*t/.k1*>) by A87,Def3 .= rng P1`1 \/ rng <*t/.k1*> by FINSEQ_1:31 .= rng P4`1 \/ {t/.k1} by FINSEQ_1:38; then rng P3 = rng P4 \/ {t/.k1} by XBOOLE_1:4,A94; hence thesis by XBOOLE_1:8,A89, A83, A84,NAT_1:13; end; suppose A95: not [(P1`1)^^<*t/.k1*>,P1`2] is consistent; set P3 = pn/.(k1+1); A96: pn/.(k1+1) = [(P1`1),(P1`2)^^<*t/.k1*>] by A95, A85,A4,A82,A88; then A97: rng P3`1 = rng P4`1; rng P3`2 = rng ((P1`2)^^<*t/.k1*>) by A96 .= rng ((P1`2)^<*t/.k1*>) by Def3,A86 .= rng P1`2 \/ rng <*t/.k1*> by FINSEQ_1:31 .= rng P4`2 \/ {t/.k1} by FINSEQ_1:38; then rng P3 = rng P4 \/ {t/.k1} by A97,XBOOLE_1:4; hence thesis by XBOOLE_1:8,A89, A83, A84,NAT_1:13; end; end; end; A98: Pr4[1] by Th16,A4; for k be non zero Nat holds Pr4[k] from NAT_1:sch 10(A98, A81); then rng P3 c= tau rng P; hence thesis by A34,A4,A59,XREAL_0:def 2,A60,XBOOLE_0:def 10; end;