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