:: The Properties of Sets of Temporal Logic Subformulas
:: by Mariusz Giero
::
:: Received May 7, 2012
:: Copyright (c) 2012-2026 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, 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,
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 **); :: redefines ** (LTLAXIO3, definition)
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:63;
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; :: redefines `1 (XTUPLE_0, definition)
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; :: redefines `2 (XTUPLE_0, definition)
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; :: redefines [ (TARSKI, definition)
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;