:: The Axiomatization of Propositional Linear Time Temporal Logic
:: by Mariusz Giero
::
:: Received November 20, 2010
:: Copyright (c) 2010-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI,
RELAT_1, XBOOLE_0, FUNCT_1, QC_LANG1, XBOOLEAN, HILBERT1, MODELC_2,
CQC_THE1, NAT_1, XXREAL_0, LTLAXIO1, ARYTM_1, ZF_LANG, PARTFUN1,
MARGREL1, FUNCT_2, HILBERT2, ZFMISC_1, FUNCOP_1, ZF_MODEL, PBOOLE,
GLIB_000;
notations TARSKI, XBOOLE_0, ZFMISC_1, DOMAIN_1, SUBSET_1, RELAT_1, PARTFUN1,
NUMBERS, XCMPLX_0, ORDINAL1, NAT_1, XXREAL_0, NAT_D, FUNCT_1, FUNCT_2,
BINOP_1, FINSEQ_1, FUNCOP_1, HILBERT1, HILBERT2, PBOOLE, XBOOLEAN,
MARGREL1, AOFA_I00;
constructors NAT_D, RELSET_1, AOFA_I00, HILBERT2, DOMAIN_1;
registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN,
RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, FUNCT_2, HILBERT1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI;
equalities XBOOLEAN, MARGREL1;
expansions TARSKI;
theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, NAT_D, XBOOLEAN,
FUNCT_2, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, FUNCOP_1, HILBERT2,
BINOP_1, XREAL_0;
schemes NAT_1, XBOOLE_0, FUNCT_2, FINSEQ_1, BINOP_1, HILBERT2;
begin :: Preliminaries
Lm1:
for X be set,f be FinSequence of X,i be Nat st 1<=i & i<=len f holds f.i=f/.i
proof
let X be set,f be FinSequence of X,i be Nat;
assume 1<=i & i<=len f;
then i in Seg len f by FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
hence thesis by PARTFUN1:def 6;
end;
reserve a,b,c for boolean object;
theorem Th1:
(a=>(b '&' c))=>(a=>b)=1
proof
A1: b=0 or b=1 by XBOOLEAN:def 3;
a=0 or a=1 by XBOOLEAN:def 3;
hence (a=>(b '&' c))=>(a=>b)=1 by A1;
end;
theorem Th2:
(a=>(b=>c))=>((a '&' b)=>c)=1
proof
A1: a=0 or a=1 by XBOOLEAN:def 3;
A2: b=0 or b=1 by XBOOLEAN:def 3;
c =0 or c =1 by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem Th3:
((a '&' b)=>c)=>(a=>(b=>c))=1
proof
A1: a=0 or a=1 by XBOOLEAN:def 3;
A2: b=0 or b=1 by XBOOLEAN:def 3;
c =0 or c =1 by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
begin :: The Language. Basic Operators. Further Operators as Abbreviations
notation
synonym LTLB_WFF for HP-WFF;
end;
reserve p,q,r,s,A,B,C for Element of LTLB_WFF,
F,G,X,Y for Subset of LTLB_WFF,
i,j,k,n for Element of NAT,
f,f1,f2,g for FinSequence of LTLB_WFF;
notation
synonym TFALSUM for VERUM;
end;
notation let p,q;
synonym p 'U' q for p '&' q;
end;
theorem Th4:
for A holds A=TFALSUM or
ex n st A=prop n or ex p,q st A=p=>q or ex p,q st A=p 'U' q
proof
let A;
A=VERUM or A is simple or A is conjunctive or A is conditional by HILBERT2:9;
hence thesis by HILBERT2:def 6,def 7,def 8;
end;
definition let p;
func 'not' p -> Element of LTLB_WFF equals
p => TFALSUM;
correctness;
func 'X' p -> Element of LTLB_WFF equals
TFALSUM 'U' p;
correctness;
end;
definition
func TVERUM -> Element of LTLB_WFF equals
'not' TFALSUM;
correctness;
end;
definition let p,q;
func p '&&' q -> Element of LTLB_WFF equals
'not' (p=>('not' q));
correctness;
end;
definition let p,q;
func p 'or' q -> Element of LTLB_WFF equals
'not'(('not' p)'&&'('not' q));
correctness;
end;
definition let p;
func 'G' p -> Element of LTLB_WFF equals
'not'(('not' p)'or'(TVERUM 'U'('not' p)));
correctness;
end;
definition let p;
func 'F' p -> Element of LTLB_WFF equals
'not'('G'('not' p));
correctness;
end;
definition let p,q;
func p 'Uw' q -> Element of LTLB_WFF equals
q 'or'(p '&&'(p 'U' q));
correctness;
end;
definition let p,q;
func p 'R' q -> Element of LTLB_WFF equals
'not'(('not' p)'Uw'('not' q));
correctness;
end;
begin :: The Semantics
definition
func props -> Subset of LTLB_WFF means
for x be set holds x in it iff ex n be Element of NAT st x=prop n;
existence
proof
defpred P1[object] means
ex n be Element of NAT st$1=prop n;
consider X being set such that
A1: for x being object holds(x in X iff x in LTLB_WFF & P1[x])
from XBOOLE_0:
sch 1;
X c=LTLB_WFF
by A1;
then reconsider X as Subset of LTLB_WFF;
take X;
thus for x being set holds (x in X iff ex n be Element of NAT st x=prop n)
by A1;
end;
uniqueness
proof
let A,B be Subset of LTLB_WFF such that
A2: for x be set holds x in A iff ex n be Element of NAT st x=prop n and
A3: for x be set holds x in B iff ex n be Element of NAT st x=prop n;
A4: B c=A
proof
let x be object;
assume x in B;
then consider n be Element of NAT such that
A5: x=prop n by A3;
thus x in A by A2,A5;
end;
A c=B
proof
let x be object;
assume x in A;
then consider n be Element of NAT such that
A6: x=prop n by A2;
thus x in B by A3,A6;
end;
hence A=B by A4,XBOOLE_0:def 10;
end;
end;
definition
mode LTLModel is sequence of bool props;
end;
reserve M for LTLModel;
definition let M be LTLModel;
func SAT M -> Function of[:NAT,LTLB_WFF:],BOOLEAN means :Def11:
for n holds it.[n,TFALSUM]=0 &
(for k holds it.[n,prop k]=1 iff prop k in M.n) &
for p,q holds it.[n,p=>q]=it.[n,p]=>it.[n,q] &
(it.[n,p 'U' q]=1 iff ex i st 0*s4.n)
& (not($3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN) implies $5=NAT-->
FALSE);
defpred C[Element of LTLB_WFF,Element of LTLB_WFF,set,set,set] means
($3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN implies ex s3,s4,s5
be sequence of BOOLEAN st s3=$3 & s4=$4 & s5=$5 & for n holds(s5.n=1 iff (ex i
st 0**FALSE);
defpred P1[Element of NAT,Function] means
for n holds($2.n=1 iff prop$1 in M.n);
A1: for p,q for a,b being set ex d being set st C[p,q,a,b,d]
proof
let p,q;
let a,b be set;
per cases;
suppose a is sequence of BOOLEAN & b is sequence of BOOLEAN;
then reconsider a1=a,b1=b as sequence of BOOLEAN;
defpred PP[Element of NAT,Element of BOOLEAN] means
$2=1 iff (ex i st 0**s41.n by A22;
consider s3,s4,s5 be sequence of BOOLEAN such that
A28: s3=a and
A29: s4=b and
A30: s5=c and
A31: for n holds s5.n=s3.n=>s4.n by A21,A23;
now let x be object;
assume x in NAT;
then reconsider x1=x as Element of NAT;
thus s5.x=s31.x1=>s4.x1 by A28,A31,A24
.=s51.x by A29,A25,A27;
end;
hence c =d by A30,A26,FUNCT_2:12;
end;
suppose not(a is sequence of BOOLEAN & b is sequence of BOOLEAN);
hence c =d by A21,A22;
end;
end;
deffunc P(Element of NAT)=f1.$1;
A32: for p,q for a,b being set ex d being set st I[p,q,a,b,d]
proof
let p,q;
let a,b be set;
per cases;
suppose a is sequence of BOOLEAN & b is sequence of BOOLEAN;
then reconsider a1=a,b1=b as sequence of BOOLEAN;
deffunc F3(Element of NAT)='not'(a1.$1'&' 'not' b1.$1);
consider d be sequence of BOOLEAN such that
A33: for n holds d.n=F3(n) from FUNCT_2:sch 4;
for n holds d.n=a1.n=>b1.n by A33;
hence thesis;
end;
suppose not(a is sequence of BOOLEAN & b is sequence of BOOLEAN);
hence thesis;
end;
end;
consider sat being ManySortedSet of LTLB_WFF such that
A34: sat.TFALSUM=NAT-->FALSE & (for n holds sat.(prop n)=P(n)) & for p,q
holds C[p,q,sat.p,sat.q,sat.(p 'U' q)] & I[p,q,sat.p,sat.q,sat.(p=>q)] from
HILBERT2:sch 3(A1,A32,A4,A20);
A35: now
A36: now let A,B;
A37: I[A,B,sat.A,sat.B,sat.(A=>B)] by A34;
per cases;
suppose sat.A is sequence of BOOLEAN & sat.B is sequence of BOOLEAN;
then consider s3,s4,s5 be sequence of BOOLEAN such that
s3=sat.A and
s4=sat.B and
A38: s5=sat.(A=>B) and
for n holds s5.n=s3.n=>s4.n by A34;
thus sat.(A=>B) in FNB by A38,FUNCT_2:8;
end;
suppose not(sat.A is sequence of BOOLEAN & sat.B is sequence of BOOLEAN);
thus sat.(A=>B) in FNB by A37,FUNCT_2:8;
end;
end;
A39: now let A,B;
A40: C[A,B,sat.A,sat.B,sat.(A 'U' B)] by A34;
per cases;
suppose sat.A is sequence of BOOLEAN & sat.B is sequence of BOOLEAN;
then consider s3,s4,s5 be sequence of BOOLEAN such that
s3=sat.A and
s4=sat.B and
A41: s5=sat.(A 'U' B) and
for n holds(s5.n=1 iff ex i st 0**q;
hence sat.x in FNB by A36;
end;
end;
dom sat=LTLB_WFF by PARTFUN1:def 2;
then reconsider sat as Function of LTLB_WFF,Funcs(NAT,BOOLEAN) by A35,
FUNCT_2:3;
deffunc satpom(Element of NAT,Element of LTLB_WFF)=(sat.$2).$1;
consider sat2 be Function of[:NAT,LTLB_WFF:],BOOLEAN such that
A43: for n,A holds sat2.(n,A)=satpom(n,A) from BINOP_1:sch 4;
A44: now let A,n;
thus sat2.[n,A]=sat2.(n,A) by BINOP_1:def 1
.=(sat.A).n by A43;
end;
A45: now let k,n;
sat2.[n,prop k]=(sat.(prop k)).n by A44
.=(f1.k).n by A34;
hence sat2.[n,prop k]=1 iff prop k in M.n by A19;
end;
A46: now let p,q,n;
reconsider satp=sat.p,satq=sat.q as sequence of BOOLEAN by FUNCT_2:66;
consider s31,s41,s51 be sequence of BOOLEAN such that
A47: s31=satp and
A48: s41=satq and
A49: s51=sat.(p 'U' q) and
A50: for n holds(s51.n=1 iff ex i st 0**q) & for n holds s5.n=s3.n=>s4.n by A34;
thus sat2.[n,p=>q]=(sat.(p=>q)).n by A44
.=((sat.p).n)=>s4.n by A51,A53
.=sat2.[n,p]=>(sat.q).n by A44,A52
.=sat2.[n,p]=>sat2.[n,q] by A44;
thus sat2.[n,p 'U' q]=1 iff ex i st 0**q]=v1.[n,p]=>v1.[n,q]
& (v1.[n,p 'U' q]=1 iff ex i st 0**q]=v2.[n,p]=>v2.[n,q]
& (v2.[n,p 'U' q]=1 iff ex i st 0**q]
proof
let p,q;
assume that
A71: P1[p] and
A72: P1[q];
thus P1[p 'U' q]
proof
let n;
per cases;
suppose A73: ex i st 0**q]
proof
let n be Element of NAT;
thus v1.[n,p=>q]=v1.[n,p]=>v1.[n,q] by A65
.=v2.[n,p]=>v1.[n,q] by A71
.=v2.[n,p]=>v2.[n,q] by A72
.=v2.[n,p=>q] by A66;
end;
end;
now let n be Element of NAT;
thus v1.[n,TFALSUM]=0 by A65
.=v2.[n,TFALSUM] by A66;
end;
then A83: P1[TFALSUM];
A84: for A holds P1[A] from HILBERT2:sch 2(A83,A67,A70);
A85: for x be Element of[:NAT,LTLB_WFF:] st x in dom v1 holds v1.x=v2.x
proof
let x be Element of[:NAT,LTLB_WFF:];
consider y,z be object such that
A86: y in NAT and
A87: z in LTLB_WFF and
A88: x=[y,z] by ZFMISC_1:def 2;
reconsider y1=y as Element of NAT by A86;
assume x in dom v1;
thus v1.x=v2.x by A84,A86,A87,A88;
reconsider z1=z as Element of LTLB_WFF by A87;
end;
dom v1=[:NAT,LTLB_WFF:] by FUNCT_2:def 1
.=dom v2 by FUNCT_2:def 1;
hence thesis by A85,PARTFUN1:5;
end;
end;
end;
theorem Th5:
(SAT M).[n,'not' A]=1 iff (SAT M).[n,A]=0
proof
hereby assume(SAT M).[n,'not' A]=1;
then A1: (SAT M).[n,A]=>(SAT M).[n,TFALSUM]=1 by Def11;
(SAT M).[n,A]=1 or(SAT M).[n,A]=0 by XBOOLEAN:def 3;
hence (SAT M).[n,A]=0 by A1,Def11;
end;
assume A2: (SAT M).[n,A]=0;
thus(SAT M).[n,'not' A]=(SAT M).[n,A]=>(SAT M).[n,TFALSUM] by Def11
.=1 by A2;
end;
theorem Th6:
(SAT M).[n,TVERUM]=1
proof
assume not(SAT M).[n,TVERUM]=1;
then not(SAT M).[n,TFALSUM]=0 by Th5;
hence contradiction by Def11;
end;
theorem Th7:
(SAT M).[n,A '&&' B]=1 iff (SAT M).[n,A]=1 & (SAT M).[n,B]=1
proof
hereby assume(SAT M).[n,A '&&' B]=1;
then (SAT M).[n,A=>(B=>TFALSUM)]=>(SAT M).[n,TFALSUM]=1 by Def11;
then (SAT M).[n,A=>(B=>TFALSUM)]=>FALSE=1 by Def11;
then ((SAT M).[n,A]=>(SAT M).[n,B=>TFALSUM])=0 by Def11;
then (SAT M).[n,A]=>((SAT M).[n,B]=>(SAT M).[n,TFALSUM])=0 by Def11;
then A1: (SAT M).[n,A]=>((SAT M).[n,B]=>FALSE)=0 by Def11;
(SAT M).[n,A]=0 or(SAT M).[n,A]=1 by XBOOLEAN:def 3;
hence (SAT M).[n,A]=1 & (SAT M).[n,B]=1 by A1;
end;
assume that
A2: (SAT M).[n,A]=1 and
A3: (SAT M).[n,B]=1;
(SAT M).[n,B]=>(SAT M).[n,TFALSUM]=0 by A3,Def11;
then (SAT M).[n,A]=>(SAT M).[n,B=>TFALSUM]=0 by A2,Def11;
then (SAT M).[n,A=>(B=>TFALSUM)]=0 by Def11;
then (SAT M).[n,A=>(B=>TFALSUM)]=>(SAT M).[n,TFALSUM]=1;
hence (SAT M).[n,A '&&' B]=1 by Def11;
end;
theorem Th8:
(SAT M).[n,A 'or' B]=1 iff ((SAT M).[n,A]=1 or(SAT M).[n,B]=1)
proof
hereby assume(SAT M).[n,A 'or' B]=1;
then A1: (SAT M).[n,('not' A)'&&'('not' B)]=0 by Th5;
per cases by A1,Th7;
suppose not(SAT M).[n,('not' A)]=1;
hence (SAT M).[n,A]=1 or(SAT M).[n,B]=1 by XBOOLEAN:def 3,Th5;
end;
suppose not(SAT M).[n,('not' B)]=1;
hence (SAT M).[n,A]=1 or(SAT M).[n,B]=1 by XBOOLEAN:def 3,Th5;
end;
end;
assume A2: (SAT M).[n,A]=1 or(SAT M).[n,B]=1;
per cases by A2;
suppose(SAT M).[n,A]=1;
then not(SAT M).[n,'not' A]=1 by Th5;
then not(SAT M).[n,('not' A)'&&'('not' B)]=1 by Th7;
hence thesis by Th5,XBOOLEAN:def 3;
end;
suppose(SAT M).[n,B]=1;
then not(SAT M).[n,'not' B]=1 by Th5;
then not(SAT M).[n,('not' A)'&&'('not' B)]=1 by Th7;
hence thesis by Th5,XBOOLEAN:def 3;
end;
end;
theorem Th9:
(SAT M).[n,'X' A]=(SAT M).[n+1,A]
proof
set f=TFALSUM,sm=SAT M;
per cases by XBOOLEAN:def 3;
suppose A1: (SAT M).[n,f 'U' A]=1;
then consider i such that
A2: 0**(SAT M).[n,TFALSUM] by
Def11
.=(SAT M).[n+1,B]=>(SAT M).[n,TFALSUM] by Th9
.=(SAT M).[n+1,B]=>FALSE by Def11
.=(SAT M).[n+1,B]=>(SAT M).[n+1,TFALSUM] by Def11
.=(SAT M).[n+1,B=>TFALSUM] by Def11
.=(SAT M).[n,'X'('not' B)] by Th9;
end;
theorem Th15:
(SAT M).[n,('not'('X' B))=>('X'('not' B))]=1
proof
A1: (SAT M).[n,('not'('X' B))]=0 or(SAT M).[n,('not'('X' B))]=1 by
XBOOLEAN:def 3;
thus(SAT M).[n,('not'('X' B))=>('X'('not' B))]=(SAT M).[n,('not'('X' B))]=>(
SAT M).[n,('X'('not' B))] by Def11
.=1 by A1,Th14;
end;
theorem Th16:
(SAT M).[n,('X'('not' B))=>('not'('X' B))]=1
proof
A1: (SAT M).[n,('not'('X' B))]=0 or(SAT M).[n,('not'('X' B))]=1 by
XBOOLEAN:def 3;
thus(SAT M).[n,('X'('not' B))=>('not'('X' B))]=(SAT M).[n,('X'('not' B))]=>(
SAT M).[n,('not'('X' B))] by Def11
.=1 by A1,Th14;
end;
theorem Th17:
(SAT M).[n,('X'(B=>C))=>(('X' B)=>('X' C))]=1
proof
A1: (SAT M).[n+1,B]=0 or(SAT M).[n+1,B]=1 by XBOOLEAN:def 3;
A2: (SAT M).[n+1,C]=0 or(SAT M).[n+1,C]=1 by XBOOLEAN:def 3;
thus(SAT M).[n,('X'(B=>C))=>(('X' B)=>('X' C))]=(SAT M).[n,'X'(B=>C)]=>(SAT M
).[n,('X' B)=>('X' C)] by Def11
.=(SAT M).[n+1,B=>C]=>(SAT M).[n,('X' B)=>('X' C)] by Th9
.=(SAT M).[n+1,B=>C]=>((SAT M).[n,'X' B]=>(SAT M).[n,'X' C]) by Def11
.=(SAT M).[n+1,B=>C]=>((SAT M).[n+1,B]=>(SAT M).[n,'X' C]) by Th9
.=(SAT M).[n+1,B=>C]=>((SAT M).[n+1,B]=>(SAT M).[n+1,C]) by Th9
.=1 by A1,A2,Def11;
end;
theorem Th18:
(SAT M).[n,('G' B)=>(B '&&'('X'('G' B)))]=1
proof
A1: (SAT M).[n,('G' B)=>(B '&&'('X'('G' B)))]=(SAT M).[n,('G' B)]=>(SAT M).[n
,B '&&'('X'('G' B))] by Def11;
per cases by XBOOLEAN:def 3;
suppose(SAT M).[n,('G' B)]=0;
hence thesis by A1;
end;
suppose A2: (SAT M).[n,('G' B)]=1;
now let i be Element of NAT;
(SAT M).[n+(i+1),B]=1 by A2,Th10;
hence (SAT M).[n+1+i,B]=1;
end;
then (SAT M).[n+1,'G' B]=1 by Th10;
then A3: (SAT M).[n,'X'('G' B)]=1 by Th9;
(SAT M).[n+0,B]=1 by A2,Th10;
then (SAT M).[n,B '&&'('X'('G' B))]=1 by A3,Th7;
hence thesis by A1;
end;
end;
theorem Th19:
(SAT M).[n,(B 'U' C)=>(('X' C)'or'('X'(B '&&'(B 'U' C))))]=1
proof
set sm=SAT M;
A1: now assume that
A2: sm.[n,(('X' C)'or'('X'(B '&&'(B 'U' C))))]=0 and
A3: sm.[n,(B 'U' C)]=1;
consider i such that
A4: 0**1;
A10: now let j;
assume that
A11: 1<=j and
A12: j1+(-1) by A9,XREAL_1:8;
n+i=n+1+(i-1)
.=n+1+(i-' 1) by A15,XREAL_0:def 2;
hence contradiction by A5,A6,A9,A15,A10,A14,Def11;
end;
end;
sm.[n,(('X' C)'or'('X'(B '&&'(B 'U' C))))]=0 or sm.[n,(('X' C)'or'('X'(B
'&&'(B 'U' C))))]=1 by XBOOLEAN:def 3;
then sm.[n,(B 'U' C)]=>sm.[n,(('X' C)'or'('X'(B '&&'(B 'U' C))))]=1 by A1,
XBOOLEAN:def 3;
hence thesis by Def11;
end;
theorem Th20:
(SAT M).[n,(('X' C)'or'('X'(B '&&'(B 'U' C))))=>(B 'U' C)]=1
proof
set sm=SAT M;
A1: now assume that
A2: sm.[n,(('X' C)'or'('X'(B '&&'(B 'U' C))))]=1 and
A3: sm.[n,(B 'U' C)]=0;
per cases by A2,Th8;
suppose A4: sm.[n,'X' C]=1;
A5: for j st 1<=j & j<1 holds sm.[n+j,B]=1;
sm.[n+1,C]=1 by A4,Th9;
hence contradiction by A3,A5,Def11;
end;
suppose sm.[n,'X'(B '&&'(B 'U' C))]=1;
then A6: sm.[n+1,B '&&'(B 'U' C)]=1 by Th9;
then sm.[n+1,B 'U' C]=1 by Th7;
then consider i such that
i>0 and
A7: sm.[n+1+i,C]=1 and
A8: for j st 1<=j & j**0;
then j-' 1>0 by XREAL_0:def 2;
then A13: 1<=j-' 1 by NAT_1:25;
A14: n+j+1-1=n+1+(j-1)
.=n+1+(j-' 1) by A12,XREAL_0:def 2;
j+(-1)**sm.[n,(B 'U' C)]=1 by A1,
XBOOLEAN:def 3;
hence thesis by Def11;
end;
theorem Th21:
(SAT M).[n,(B 'U' C)=>('X'('F' C))]=1
proof
set sm=SAT M;
A1: now assume that
A2: sm.[n,B 'U' C]=1 and
A3: sm.[n,'X'('F' C)]=0;
consider i such that
A4: 0**=1+(-1) by A4,NAT_1:25,XREAL_1:6;
then A6: n+1+(i-' 1)=n+1+(i-1) by XREAL_0:def 2
.=n+i;
sm.[n+1,'F' C]=0 by A3,Th9;
hence contradiction by A5,A6,Th11;
end;
sm.[n,B 'U' C]=0 or sm.[n,B 'U' C]=1 by XBOOLEAN:def 3;
then sm.[n,B 'U' C]=>sm.[n,'X'('F' C)]=1 by A1,XBOOLEAN:def 3;
hence thesis by Def11;
end;
begin :: Validity. Consequence. Some Facts about the Semantical Notions
definition let M,p;
pred M|=p means :Def12:
for n be Element of NAT holds(SAT M).[n,p]=1;
end;
definition let M,F;
pred M|=F means
for p st p in F holds M|=p;
end;
definition let F,p;
pred F|=p means
for M holds(M|=F implies M|=p);
end;
theorem Th22:
M|=F & M|=G iff M|=F\/G
proof
hereby assume A1: M|=F & M|=G;
thus M|=F\/G
proof
let p;
assume p in F\/G;
then p in F or p in G by XBOOLE_0:def 3;
hence M|=p by A1;
end;
end;
assume A2: M|=F\/G;
thus M|=F
proof
let p;
assume p in F;
then p in F\/G by XBOOLE_0:def 3;
hence M|=p by A2;
end;
thus M|=G
proof
let p;
assume p in G;
then p in F\/G by XBOOLE_0:def 3;
hence M|=p by A2;
end;
end;
theorem Th23:
M|=A iff M |= {A}
proof
thus M|=A implies M |= {A} by TARSKI:def 1;
A in {A} by TARSKI:def 1;
hence thesis;
end;
theorem Th24:
F|=A & F|=A=>B implies F|=B
proof
assume that
A1: F|=A and
A2: F|=A=>B;
let M;
assume A3: M|=F;
let n be Element of NAT;
(SAT M).[n,A=>B]=1 by Def12,A2,A3;
then A4: (SAT M).[n,A]=>(SAT M).[n,B]=1 by Def11;
(SAT M).[n,A]=1 by Def12,A1,A3;
hence (SAT M).[n,B]=1 by A4;
end;
theorem Th25:
F|=A implies F|='X' A
proof
assume A1: F|=A;
let M;
assume A2: M|=F;
let n be Element of NAT;
thus(SAT M).[n,'X' A]=(SAT M).[n+1,A] by Th9
.=1 by A2,Def12,A1;
end;
theorem
F|=A implies F|='G' A
proof
assume A1: F|=A;
let M;
assume A2: M|=F;
let n be Element of NAT;
for i be Element of NAT holds(SAT M).[n+i,A]=1 by Def12,A1,A2;
hence (SAT M).[n,'G' A]=1 by Th10;
end;
theorem Th27:
F|=A=>B & F|=A=>('X' A) implies F|=A=>('G' B)
proof
assume that
A1: F|=A=>B and
A2: F|=A=>('X' A);
let M;
assume A3: M|=F;
let n be Element of NAT;
defpred P1[Nat] means
(SAT M).[n+$1,A]=1;
per cases by XBOOLEAN:def 3;
suppose A4: (SAT M).[n,A]=1;
A5: for k being Nat st P1[k] holds P1[k+1]
proof
let k be Nat such that
A6: P1[k];
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
(SAT M).[n+kk,A=>('X' A)]=1 by A2,A3,Def12;
then (SAT M).[n+kk,A]=>(SAT M).[n+kk,'X' A]=1 by Def11;
then (SAT M).[n+kk+1,A]=1 by A6,Th9;
hence P1[k+1];
end;
A7: P1[0] by A4;
A8: for i be Nat holds P1[i] from NAT_1:sch 2(A7,A5);
now let i be Element of NAT;
(SAT M).[n+i,A=>B]=1 by A3,A1,Def12;
then A9: (SAT M).[n+i,A]=>(SAT M).[n+i,B]=1 by Def11;
(SAT M).[n+i,A]=1 by A8;
hence (SAT M).[n+i,B]=1 by A9;
end;
then (SAT M).[n,'G' B]=1 by Th10;
then (SAT M).[n,A]=>(SAT M).[n,'G' B]=1;
hence (SAT M).[n,A=>('G' B)]=1 by Def11;
end;
suppose(SAT M).[n,A]=0;
then (SAT M).[n,A]=>(SAT M).[n,'G' B]=1;
hence (SAT M).[n,A=>('G' B)]=1 by Def11;
end;
end;
theorem Th28:
(SAT(M^\i)).[j,A]=(SAT M).[i+j,A]
proof
defpred P1[Element of LTLB_WFF] means
for k holds(SAT(M^\i)).[k,$1]=(SAT M).[i+k,$1];
A1: for n being Element of NAT holds P1[prop n]
proof
let n,k;
per cases;
suppose A2: prop n in (M^\i).k;
then A3: prop n in M.(i+k) by NAT_1:def 3;
thus(SAT(M^\i)).[k,prop n]=1 by A2,Def11
.=(SAT M).[i+k,prop n] by A3,Def11;
end;
suppose A4: not prop n in (M^\i).k;
then not prop n in M.(i+k) by NAT_1:def 3;
then A5: not(SAT M).[i+k,prop n]=1 by Def11;
not(SAT(M^\i)).[k,prop n]=1 by A4,Def11;
hence (SAT(M^\i)).[k,prop n]=0 by XBOOLEAN:def 3
.=(SAT M).[i+k,prop n] by A5,XBOOLEAN:def 3;
end;
end;
A6: for r,s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r=>s]
proof
let r,s being Element of LTLB_WFF;
assume that
A7: P1[r] and
A8: P1[s];
thus P1[r 'U' s]
proof
let k;
A9: (SAT(M^\i)).[k,r 'U' s]=1 iff (SAT M).[i+k,r 'U' s]=1
proof
hereby assume(SAT(M^\i)).[k,r 'U' s]=1;
then consider m be Element of NAT such that
A10: 0s]
proof
let k be Element of NAT;
thus(SAT(M^\i)).[k,r=>s]=(SAT(M^\i)).[k,r]=>(SAT(M^\i)).[k,s] by Def11
.=(SAT M).[i+k,r]=>(SAT(M^\i)).[k,s] by A7
.=(SAT M).[i+k,r]=>(SAT M).[i+k,s] by A8
.=(SAT M).[i+k,r=>s] by Def11;
end;
end;
now let k;
thus(SAT(M^\i)).[k,TFALSUM]=0 by Def11
.=(SAT M).[i+k,TFALSUM] by Def11;
end;
then A18: P1[TFALSUM];
for r being Element of LTLB_WFF holds P1[r] from HILBERT2:sch 2(A18,A1,A6);
hence (SAT(M^\i)).[j,A]=(SAT M).[i+j,A];
end;
theorem Th29:
M|=F implies M^\i|=F
proof
assume A1: M|=F;
thus M^\i|=F
proof
let p;
assume A2: p in F;
thus M^\i|=p
proof
let n;
(SAT M).[i+n,p]=1 by A2,A1,Def12;
hence (SAT(M^\i)).[n,p]=1 by Th28;
end;
end;
end;
theorem
F\/{A}|=B iff F|=('G' A)=>B
proof
hereby assume A1: F\/{A}|=B;
thus F|=('G' A)=>B
proof
let M;
assume A2: M|=F;
thus M|=('G' A)=>B
proof
let n;
per cases by XBOOLEAN:def 3;
suppose A3: (SAT M).[n,'G' A]=0;
thus(SAT M).[n,('G' A)=>B]=(SAT M).[n,'G' A]=>(SAT M).[n,B] by Def11
.=1 by A3;
end;
suppose A4: (SAT M).[n,'G' A]=1;
now let j;
(SAT M).[n+j,A]=1 by A4,Th10;
hence (SAT(M^\n)).[j,A]=1 by Th28;
end;
then A5: M^\n|={A} by Th23,Def12;
M^\n|=F by A2,Th29;
then M^\n|=F\/{A} by A5,Th22;
then (SAT(M^\n)).[0,B]=1 by Def12,A1;
then A6: (SAT M).[n+0,B]=1 by Th28;
thus(SAT M).[n,('G' A)=>B]=(SAT M).[n,'G' A]=>(SAT M).[n,B] by Def11
.=1 by A6;
end;
end;
end;
end;
assume A7: F|=('G' A)=>B;
let M;
assume A8: M|=F\/{A};
let i;
M|={A} by A8,Th22;
then for j holds(SAT M).[i+j,A]=1 by Def12,Th23;
then A9: (SAT M).[i,'G' A]=1 by Th10;
M|=F by A8,Th22;
then (SAT M).[i,('G' A)=>B]=1 by Def12,A7;
then (SAT M).[i,('G' A)]=>(SAT M).[i,B]=1 by Def11;
hence (SAT M).[i,B]=1 by A9;
end;
definition let f be Function of LTLB_WFF,BOOLEAN;
func VAL f -> Function of LTLB_WFF,BOOLEAN means :Def15:
it.TFALSUM=0 & it.(prop n)=f.(prop n) &
it.(A=>B)=it.A=>it.B & it.(A 'U' B)=f.(A 'U' B);
existence
proof
defpred P3[Element of LTLB_WFF,Element of LTLB_WFF,set,set,set] means
($3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex a,b,c be
Element of BOOLEAN st a=$3 & b=$4 & c =$5 & c =a=>b) & (not$3 is Element of
BOOLEAN or not$4 is Element of BOOLEAN implies $5={});
defpred P1[Element of LTLB_WFF,Element of LTLB_WFF,set,set,set] means
$5=f.($1'U'$2);
deffunc F2(Element of NAT)=f.(prop$1);
A1: for A,B for x,y be set ex z be set st P3[A,B,x,y,z]
proof
let A,B;
let x,y be set;
per cases;
suppose that
A2: x is Element of BOOLEAN and
A3: y is Element of BOOLEAN;
reconsider b=y as Element of BOOLEAN by A3;
reconsider a=x as Element of BOOLEAN by A2;
per cases by XBOOLEAN:def 3;
suppose A4: a=0;
set c =TRUE;
c =a=>b by A4;
hence thesis;
end;
suppose A5: a=1;
per cases by XBOOLEAN:def 3;
suppose A6: b=0;
set c =FALSE;
c =a=>b by A5,A6;
hence thesis;
end;
suppose A7: b=1;
set c =TRUE;
c =a=>b by A7;
hence thesis;
end;
end;
end;
suppose not x is Element of BOOLEAN or not y is Element of BOOLEAN;
hence thesis;
end;
end;
A8: 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;
A9: 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;
A10: for A,B for x,y be set ex z be set st P1[A,B,x,y,z];
consider val being ManySortedSet of LTLB_WFF such that
A11: val.TFALSUM=0 & (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(A10,A1,A8,A9);
A12: now A13: now let A,B;
per cases;
suppose val.A is Element of BOOLEAN & val.B is Element of BOOLEAN;
then consider a,b,c be Element of BOOLEAN such that
a=val.A and
b=val.B and
A14: c =val.(A=>B) and
c =a=>b by A11;
thus val.(A=>B) in BOOLEAN by A14;
end;
suppose not(val.A is Element of BOOLEAN & val.B is Element of BOOLEAN);
then val.(A=>B)=FALSE by A11;
hence val.(A=>B) in BOOLEAN;
end;
end;
let x be object;
assume x in LTLB_WFF;
then reconsider x1=x as Element of LTLB_WFF;
A15: now let n;
val.(prop n)=f.(prop n) by A11;
hence val.(prop n) in BOOLEAN;
end;
A16: now let A,B;
val.(A 'U' B)=f.(A 'U' B) by A11;
hence val.(A 'U' B) in BOOLEAN;
end;
per cases by Th4;
suppose x1=TFALSUM;
hence val.x in BOOLEAN by A11,TARSKI:def 2;
end;
suppose ex n be Element of NAT st x1=prop n;
hence val.x in BOOLEAN by A15;
end;
suppose ex p,q st x1=p 'U' q;
hence val.x in BOOLEAN by A16;
end;
suppose ex p,q st x1=p=>q;
hence val.x in BOOLEAN by A13;
end;
end;
dom val=LTLB_WFF by PARTFUN1:def 2;
then reconsider val as Function of LTLB_WFF,BOOLEAN by A12,FUNCT_2:3;
take val;
now let A,B;
P3[A,B,val.A,val.B,val.(A=>B)] by A11;
hence val.(A=>B)=val.A=>val.B;
end;
hence thesis by A11;
end;
uniqueness
proof
let v1,v2 be Function of LTLB_WFF,BOOLEAN;
assume A17: v1.TFALSUM=0 & v1.(prop n)=f.(prop n) & v1.(A=>B)=v1.A=>v1.B & v1
.(A 'U' B)=f.(A 'U' B);
assume A18: v2.TFALSUM=0 & v2.(prop n)=f.(prop n) & v2.(A=>B)=v2.A=>v2.B & v2
.(A 'U' B)=f.(A 'U' B);
thus v1=v2
proof
defpred P1[Element of LTLB_WFF] means
v1.$1=v2.$1;
A19: for n holds P1[prop n]
proof
let n;
v1.(prop n)=f.(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)=f.(r 'U' s) by A17
.=v2.(r 'U' s) by A18;
v1.(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 LTLB_WFF holds P1[x] from HILBERT2:sch 2(A23,A19,A20);
then A24: for x be Element of LTLB_WFF st x in dom v1 holds P1[x];
dom v1=LTLB_WFF by FUNCT_2:def 1
.=dom v2 by FUNCT_2:def 1;
hence thesis by A24,PARTFUN1:5;
end;
end;
end;
theorem Th31:
for f be Function of LTLB_WFF,BOOLEAN,p,q holds
(VAL f).(p '&&' q)=(VAL f).p'&'(VAL f).q
proof
let f be Function of LTLB_WFF,BOOLEAN,p,q;
A1: (VAL f).p=0 or(VAL f).p=1 by XBOOLEAN:def 3;
A2: (VAL f).q=0 or(VAL f).q=1 by XBOOLEAN:def 3;
thus(VAL f).(p '&&' q)=(VAL f).(p=>(q=>TFALSUM))=>(VAL f).(TFALSUM) by Def15
.=((VAL f).p=>(VAL f).(q=>TFALSUM))=>(VAL f).(TFALSUM) by Def15
.=((VAL f).p=>((VAL f).q=>(VAL f).(TFALSUM)))=>(VAL f).(TFALSUM) by Def15
.=((VAL f)/.p=>((VAL f).q=>FALSE))=>(VAL f).(TFALSUM) by Def15
.=(VAL f).p '&'(VAL f).q by A1,A2,Def15;
end;
theorem Th32:
for f be Function of LTLB_WFF,BOOLEAN st
(for B be object st B in LTLB_WFF holds f.B=(SAT M).[n,B]) holds
(VAL f).A=(SAT M).[n,A]
proof
let f be Function of LTLB_WFF,BOOLEAN;
defpred P1[Element of LTLB_WFF] means (VAL f).$1=(SAT M).[n,$1];
assume A1: for B be object st B in LTLB_WFF holds f.B=(SAT M).[n,B];
A2: for k holds P1[prop k]
proof
let k;
(SAT M).[n,prop k]=f.(prop k) by A1
.=(VAL f).(prop k) by Def15;
hence thesis;
end;
A3: for r,s st P1[r] & P1[s] holds P1[r 'U' s] & P1[r=>s]
proof
let r,s;
assume A4: (P1[r]) & P1[s];
(VAL f).(r 'U' s)=f.(r 'U' s) by Def15
.=(SAT M).[n,r 'U' s] by A1;
hence P1[r 'U' s];
(SAT M).[n,r=>s]=(SAT M).[n,r]=>(SAT M).[n,s] by Def11
.=(VAL f).(r=>s) by A4,Def15;
hence P1[r=>s];
end;
(SAT M).[n,TFALSUM]=0 by Def11
.=(VAL f).TFALSUM by Def15;
then A5: P1[TFALSUM];
for r holds P1[r] from HILBERT2:sch 2(A5,A2,A3);
hence (VAL f).A=(SAT M).[n,A];
end;
definition let p;
attr p is LTL_TAUT_OF_PL means
for f be Function of LTLB_WFF,BOOLEAN holds(VAL f).p=1;
end;
theorem Th33:
A is LTL_TAUT_OF_PL implies F|=A
proof
assume A1: A is LTL_TAUT_OF_PL;
let M be LTLModel;
assume M|=F;
let n;
defpred P[object,object] means
$2=(SAT M).[n,$1];
A2: for x be object st x in LTLB_WFF
ex y be object st y in BOOLEAN & P[x,y]
proof
let x be object;
set y=(SAT M).[n,x];
assume x in LTLB_WFF;
then reconsider x1=x as Element of LTLB_WFF;
take y;
(SAT M).[n,x1] in BOOLEAN;
hence y in BOOLEAN & P[x,y];
end;
consider f be Function of LTLB_WFF,BOOLEAN such that
A3: for B be object st B in LTLB_WFF holds P[B,f.B]
from FUNCT_2:sch 1(A2);
thus(SAT M).[n,A]=(VAL f).A by A3,Th32
.=1 by A1;
end;
begin :: Axioms. Derivation Rules. Derivability. Soundness Theorem for LTL
definition let D be set;
attr D is with_LTL_axioms means :Def17:
for p,q holds (p is LTL_TAUT_OF_PL implies p in D) &
('not'('X' p))=>('X'('not' p)) in D &
('X'('not' p))=>('not'('X' p)) in D &
('X'(p=>q))=>(('X' p)=>('X' q)) in D &
('G' p)=>(p '&&'('X'('G' p))) in D &
(p 'U' q)=>(('X' q)'or'('X'(p '&&'(p 'U' q)))) in D &
(('X' q)'or'('X'(p '&&'(p 'U' q))))=>(p 'U' q) in D &
(p 'U' q)=>('X'('F' q)) in D;
end;
definition
func LTL_axioms -> Subset of LTLB_WFF means :Def18:
it is with_LTL_axioms &
for D be Subset of LTLB_WFF st D is with_LTL_axioms holds it c=D;
existence
proof
defpred S1[object] means
for D being set st D is with_LTL_axioms holds$1 in D;
consider D0 being set such that
A1: for x being object
holds(x in D0 iff x in LTLB_WFF & S1[x]) from XBOOLE_0:
sch 1;
D0 c=LTLB_WFF
by A1;
then reconsider D0 as Subset of LTLB_WFF;
take D0;
thus D0 is with_LTL_axioms
proof
let p,q be Element of LTLB_WFF;
thus p is LTL_TAUT_OF_PL implies p in D0
proof
assume p is LTL_TAUT_OF_PL;
then for D being set st D is with_LTL_axioms holds p in D;
hence thesis by A1;
end;
for D being set st D is with_LTL_axioms holds('not'('X' p))=>('X'('not' p))
in D;
hence ('not'('X' p))=>('X'('not' p)) in D0 by A1;
for D being set st D is with_LTL_axioms holds('X'('not' p))=>('not'('X' p))
in D;
hence ('X'('not' p))=>('not'('X' p)) in D0 by A1;
for D being set st D is with_LTL_axioms holds('X'(p=>q))=>(('X' p)=>('X' q))
in D;
hence ('X'(p=>q))=>(('X' p)=>('X' q)) in D0 by A1;
for D being set st D is with_LTL_axioms holds('G' p)=>(p '&&'('X'('G' p)))
in D;
hence ('G' p)=>(p '&&'('X'('G' p))) in D0 by A1;
for D being set st D is with_LTL_axioms holds(p 'U' q)=>(('X' q)'or'('X'(p
'&&'(p 'U' q)))) in D;
hence (p 'U' q)=>(('X' q)'or'('X'(p '&&'(p 'U' q)))) in D0 by A1;
for D being set st D is with_LTL_axioms holds(('X' q)'or'('X'(p '&&'(p 'U'
q))))=>(p 'U' q) in D;
hence (('X' q)'or'('X'(p '&&'(p 'U' q))))=>(p 'U' q) in D0 by A1;
for D being set st D is with_LTL_axioms holds(p 'U' q)=>('X'('F' q)) in D;
hence (p 'U' q)=>('X'('F' q)) in D0 by A1;
end;
let D be Subset of LTLB_WFF;
assume A2: D is with_LTL_axioms;
let x be object;
assume x in D0;
hence x in D by A1,A2;
end;
uniqueness
proof
let D1,D2 be Subset of LTLB_WFF;
assume(D1 is with_LTL_axioms) & (for D be Subset of LTLB_WFF st D is
with_LTL_axioms holds D1 c=D) & D2 is with_LTL_axioms & for D be Subset of
LTLB_WFF st D is with_LTL_axioms holds D2 c=D;
then D1 c=D2 & D2 c=D1;
hence D1=D2 by XBOOLE_0:def 10;
end;
end;
registration
cluster LTL_axioms -> with_LTL_axioms;
coherence by Def18;
end;
theorem Th34:
p=>(q=>p) in LTL_axioms
proof
p=>(q=>p) is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN;
A1: (VAL f).p=0 or(VAL f).p=1 by XBOOLEAN:def 3;
thus(VAL f).(p=>(q=>p))=(VAL f).p=>(VAL f).(q=>p) by Def15
.=(VAL f).p=>((VAL f).q=>(VAL f).p) by Def15
.=1 by A1;
end;
hence p=>(q=>p) in LTL_axioms by Def17;
end;
theorem Th35:
(p=>(q=>r))=>((p=>q)=>(p=>r)) in LTL_axioms
proof
(p=>(q=>r))=>((p=>q)=>(p=>r)) is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN;
A1: (VAL f).p=0 or(VAL f).p=1 by XBOOLEAN:def 3;
A2: (VAL f).q=0 or(VAL f).q=1 by XBOOLEAN:def 3;
A3: (VAL f).r=0 or(VAL f).r=1 by XBOOLEAN:def 3;
thus(VAL f).((p=>(q=>r))=>((p=>q)=>(p=>r)))=(VAL f).(p=>(q=>r))=>(VAL f).((p
=>q)=>(p=>r)) by Def15
.=((VAL f).p=>(VAL f).(q=>r))=>(VAL f).((p=>q)=>(p=>r)) by Def15
.=((VAL f).p=>((VAL f).q=>(VAL f).r))=>(VAL f).((p=>q)=>(p=>r)) by Def15
.=((VAL f).p=>((VAL f).q=>(VAL f).r))=>((VAL f).(p=>q)=>(VAL f).(p=>r)) by
Def15
.=((VAL f).p=>((VAL f).q=>(VAL f).r))=>(((VAL f).p=>(VAL f).q)=>(VAL f).(p
=>r)) by Def15
.=1 by A1,A2,A3,Def15;
end;
hence (p=>(q=>r))=>((p=>q)=>(p=>r)) in LTL_axioms by Def17;
end;
definition let p,q;
pred p NEX_rule q means
q='X' p;
let r;
pred p,q MP_rule r means
q=p=>r;
pred p,q IND_rule r means
ex A,B st p=A=>B & q=A=>('X' A) & r=A=>('G' B);
end;
registration
cluster LTL_axioms -> non empty;
coherence by Def17;
end;
definition let A;
attr A is axltl1 means :Def22:
ex B st A=('not'('X' B))=>('X'('not' B));
attr A is axltl1a means :Def23:
ex B st A=('X'('not' B))=>('not'('X' B));
attr A is axltl2 means :Def24:
ex B,C st A=('X'(B=>C))=>(('X' B)=>('X' C));
attr A is axltl3 means :Def25:
ex B st A=('G' B)=>(B '&&'('X'('G' B)));
attr A is axltl4 means :Def26:
ex B,C st A=(B 'U' C)=>(('X' C)'or'('X'(B '&&'(B 'U' C))));
attr A is axltl5 means :Def27:
ex B,C st A=(('X' C)'or'('X'(B '&&'(B 'U' C))))=>(B 'U' C);
attr A is axltl6 means :Def28:
ex B,C st A=(B 'U' C)=>('X'('F' C));
end;
theorem Th36:
for A be Element of LTL_axioms holds
(A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or
A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6)
proof
defpred P1[Element of LTL_axioms] means
$1 is LTL_TAUT_OF_PL or$1 is axltl1 or$1 is axltl1a or$1 is axltl2 or$1 is
axltl3 or$1 is axltl4 or$1 is axltl5 or$1 is axltl6;
set X={p where p is Element of LTL_axioms:P1[p]};
X c=LTLB_WFF
proof
let x be object;
assume x in X;
then ex p be Element of LTL_axioms st x=p & P1[p];
hence x in LTLB_WFF;
end;
then reconsider X as Subset of LTLB_WFF;
let A be Element of LTL_axioms;
X is with_LTL_axioms
proof
let p,q;
thus p is LTL_TAUT_OF_PL implies p in X
proof
assume A1: p is LTL_TAUT_OF_PL;
then reconsider p1=p as Element of LTL_axioms by Def17;
P1[p1] by A1;
hence thesis;
end;
thus('not'('X' p))=>('X'('not' p)) in X
proof
reconsider pp=('not'('X' p))=>('X'('not' p)) as Element of LTL_axioms by
Def17;
P1[pp] by Def22;
hence thesis;
end;
thus('X'('not' p))=>('not'('X' p)) in X
proof
reconsider pp=('X'('not' p))=>('not'('X' p)) as Element of LTL_axioms by
Def17;
P1[pp] by Def23;
hence thesis;
end;
thus('X'(p=>q))=>(('X' p)=>('X' q)) in X
proof
reconsider pp=('X'(p=>q))=>(('X' p)=>('X' q)) as Element of LTL_axioms by
Def17;
P1[pp] by Def24;
hence thesis;
end;
thus('G' p)=>(p '&&'('X'('G' p))) in X
proof
reconsider pp=('G' p)=>(p '&&'('X'('G' p))) as Element of LTL_axioms by
Def17;
P1[pp] by Def25;
hence thesis;
end;
thus(p 'U' q)=>(('X' q)'or'('X'(p '&&'(p 'U' q)))) in X
proof
reconsider pp=(p 'U' q)=>(('X' q)'or'('X'(p '&&'(p 'U' q)))) as Element
of LTL_axioms by Def17;
P1[pp] by Def26;
hence thesis;
end;
thus(('X' q)'or'('X'(p '&&'(p 'U' q))))=>(p 'U' q) in X
proof
reconsider pp=(('X' q)'or'('X'(p '&&'(p 'U' q))))=>(p 'U' q) as Element
of LTL_axioms by Def17;
P1[pp] by Def27;
hence thesis;
end;
thus(p 'U' q)=>('X'('F' q)) in X
proof
reconsider pp=(p 'U' q)=>('X'('F' q)) as Element of LTL_axioms by Def17;
P1[pp] by Def28;
hence thesis;
end;
end;
then A in LTL_axioms & LTL_axioms c=X by Def18;
then A in X;
then ex p be Element of LTL_axioms st A=p & P1[p];
hence P1[A];
end;
theorem Th37:
A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or
A is axltl4 or A is axltl5 or A is axltl6 implies F|=A
proof
assume A1: A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is
axltl4 or A is axltl5 or A is axltl6;
let M;
assume M|=F;
let n be Element of NAT;
per cases by A1;
suppose A is axltl1;
then consider B be Element of LTLB_WFF such that
A2: A=('not'('X' B))=>('X'('not' B));
thus thesis by A2,Th15;
end;
suppose A is axltl1a;
then consider B be Element of LTLB_WFF such that
A3: A=('X'('not' B))=>('not'('X' B));
thus thesis by A3,Th16;
end;
suppose A is axltl2;
then consider B,C be Element of LTLB_WFF such that
A4: A=('X'(B=>C))=>(('X' B)=>('X' C));
thus thesis by A4,Th17;
end;
suppose A is axltl3;
then consider B be Element of LTLB_WFF such that
A5: A=('G' B)=>(B '&&'('X'('G' B)));
thus thesis by A5,Th18;
end;
suppose A is axltl4;
then consider B,C such that
A6: A=(B 'U' C)=>(('X' C)'or'('X'(B '&&'(B 'U' C))));
thus thesis by A6,Th19;
end;
suppose A is axltl5;
then consider B,C such that
A7: A=(('X' C)'or'('X'(B '&&'(B 'U' C))))=>(B 'U' C);
thus thesis by A7,Th20;
end;
suppose A is axltl6;
then consider B,C such that
A8: A=(B 'U' C)=>('X'('F' C));
thus thesis by A8,Th21;
end;
end;
definition let i be Nat,f,X;
pred prc f,X,i means :Def29:
f.i in LTL_axioms or f.i in X or
(ex j,k be Nat st 1<=j & j** & 1<=len f1 &
for i be Nat st 1<=i & i<=len f1 holds prc f1,X,i) &
prc f,X,len f implies (for i be Nat st 1<=i & i<=len f holds prc f,X,i) &
X|-p
proof
assume that
A1: f=f1^<*p*> and
1<=len f1 and
A2: for i be Nat st 1<=i & i<=len f1 holds prc f1,X,i;
A3: len f=(len f1+len<*p*>) by A1,FINSEQ_1:22
.=len f1+1 by FINSEQ_1:39;
assume A4: prc f,X,len f;
A5: 0+len f1<=len f by A3,NAT_1:12;
A6: now let i be Nat;
assume that
A7: 1<=i and
A8: i<=len f;
A9: i) by A1,FINSEQ_1:22
.=f.(len f1+1) by FINSEQ_1:39
.=p by A1,FINSEQ_1:42;
hence X|-p by A3,XREAL_1:31,A6;
end;
theorem
F|-A implies F|=A
proof
assume F|-A;
then consider f such that
A1: f.len f=A and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,F,i;
defpred P[Nat] means
1<=$1 & $1<=len f implies F|=f/.$1;
A4: for i being Nat st for j being Nat st j**f/.i by A15;
hence F|=f/.i by A5,A10,A11,A16,Th24;
end;
suppose f/.j,f/.k IND_rule f/.i;
then consider A,B such that
A17: f/.j=A=>B and
A18: f/.k=A=>('X' A) & f/.i=A=>('G' B);
F|=A=>B by A5,A10,A11,A16,A17;
hence F|=f/.i by A15,A18,Th27;
end;
end;
suppose ex j be Nat st 1<=j & j**q implies X|-q
proof
assume X|-p;
then consider f such that
A1: f.len f=p and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,X,i;
set j=len f;
assume X|-p=>q;
then consider f1 such that
A4: f1.len f1=p=>q and
A5: 1<=len f1 and
A6: for i be Nat st 1<=i & i<=len f1 holds prc f1,X,i;
A7: 1<=len f+len f1 by A2,NAT_1:12;
set g=f^f1^<*q*>;
A8: g=f^(f1^<*q*>) by FINSEQ_1:32;
A9: for i be Nat st 1<=i & i<=len f1 holds g.(len f+i)=f1.i
proof
let i be Nat;
assume that
A10: 1<=i and
A11: i<=len f1;
len(f1^<*q*>)=len f1+len<*q*> by FINSEQ_1:22
.=len f1+1 by FINSEQ_1:39;
then i<=len(f1^<*q*>) by A11,NAT_1:12;
hence g.(len f+i)=(f1^<*q*>).i by A8,A10,FINSEQ_1:65
.=f1.i by A10,A11,FINSEQ_1:64;
end;
A12: len g=len(f^f1)+len<*q*> by FINSEQ_1:22
.=len(f^f1)+1 by FINSEQ_1:39;
then A13: len g=len f+len f1+1 by FINSEQ_1:22;
then len g=len f+(len f1+1);
then A14: jq by A4,A5,A9;
then g/.j,g/.k MP_rule g/.len g by A15,A17;
then A19: len(f^f1)=len f+len f1 & prc g,X,len g by A2,A14,A16,A18,
FINSEQ_1:22;
for i be Nat st 1<=i & i<=len(f^f1) holds prc f^f1,X,i by A2,A3,A5,A6,Th39;
hence X|-q by A7,A19,Th40;
end;
theorem Th44:
X|-p implies X|-'X' p
proof
assume X|-p;
then consider f such that
A1: f.len f=p and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,X,i;
set g=f^<*('X' p)*>;
A4: len g=len f+len<*('X' p)*> by FINSEQ_1:22
.=len f+1 by FINSEQ_1:39;
then A5: len fq & X|-p=>('X' p) implies X|-p=>('G' q)
proof
assume that
A1: X|-p=>q and
A2: X|-p=>('X' p);
consider f such that
A3: f.len f=p=>q and
A4: 1<=len f and
A5: for i be Nat st 1<=i & i<=len f holds prc f,X,i by A1;
consider g such that
A6: g.len g=p=>('X' p) and
A7: 1<=len g and
A8: for i be Nat st 1<=i & i<=len g holds prc g,X,i by A2;
A9: for i be Nat st 1<=i & i<=len(f^g) holds prc f^g,X,i by A4,A5,A7,A8,Th39;
set h=f^g^<*p=>('G' q)*>;
A10: h=f^(g^<*p=>('G' q)*>) by FINSEQ_1:32;
A11: len(f^g)=len f+len g by FINSEQ_1:22;
then A12: 1<=len(f^g) by A4,NAT_1:12;
A13: len h=len(f^g)+len<*p=>('G' q)*> by FINSEQ_1:22
.=len(f^g)+1 by FINSEQ_1:39;
then 1<=len h by A4,A11,NAT_1:16;
then A14: h/.len h=h.len h by Lm1
.=p=>('G' q) by A13,FINSEQ_1:42;
len h=len f+(len g+1) by A11,A13;
then A15: len fq by A3,A4,A10,FINSEQ_1:64;
A17: len(f^g)('X' p) by A6,A7,FINSEQ_1:65;
then h/.len f,h/.len(f^g)IND_rule h/.len h by A16,A14;
then prc h,X,len h by A4,A12,A15,A17;
hence X|-p=>('G' q) by A12,A9,Th40;
end;
theorem Th46:
X|-r=>(p '&&' q) implies X|-r=>p & X|-r=>q
proof
assume A1: X|-r=>(p '&&' q);
set A=(r=>(p '&&' q))=>(r=>p);
A is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN;
thus(VAL f).A=(VAL f).(r=>(p '&&' q))=>(VAL f).(r=>p) by Def15
.=(VAL f).r=>(VAL f).(p '&&' q)=>(VAL f).(r=>p) by Def15
.=(VAL f).r=>((VAL f).p '&'(VAL f).q)=>(VAL f).(r=>p) by Th31
.=(VAL f).r=>((VAL f).p '&'(VAL f).q)=>((VAL f).r=>(VAL f).p) by Def15
.=1 by Th1;
end;
then A in LTL_axioms by Def17;
then X|-A by Th42;
hence X|-r=>p by A1,Th43;
set A=(r=>(p '&&' q))=>(r=>q);
A is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN;
thus(VAL f).A=(VAL f).(r=>(p '&&' q))=>(VAL f).(r=>q) by Def15
.=(VAL f).r=>(VAL f).(p '&&' q)=>(VAL f).(r=>q) by Def15
.=(VAL f).r=>((VAL f).p '&'(VAL f).q)=>(VAL f).(r=>q) by Th31
.=(VAL f).r=>((VAL f).p '&'(VAL f).q)=>((VAL f).r=>(VAL f).q) by Def15
.=1 by Th1;
end;
then A in LTL_axioms by Def17;
then X|-A by Th42;
hence X|-r=>q by A1,Th43;
end;
theorem Th47:
X|-p=>q & X|-q=>r implies X|-p=>r
proof
assume that
A1: X|-p=>q and
A2: X|-q=>r;
set A=(p=>q)=>((q=>r)=>(p=>r));
now let f be Function of LTLB_WFF,BOOLEAN;
thus(VAL f).A=(VAL f).(p=>q)=>(VAL f).((q=>r)=>(p=>r)) by Def15
.=((VAL f).p=>(VAL f).q)=>(VAL f).((q=>r)=>(p=>r)) by Def15
.=((VAL f).p=>(VAL f).q)=>((VAL f).(q=>r)=>(VAL f).(p=>r)) by Def15
.=((VAL f).p=>(VAL f).q)=>((VAL f).q=>(VAL f).r=>(VAL f).(p=>r)) by Def15
.=((VAL f).p=>(VAL f).q)=>((VAL f).q=>(VAL f).r=>((VAL f).p=>(VAL f).r))
by Def15
.=1 by XBOOLEAN:106;
end;
then (p=>q)=>((q=>r)=>(p=>r)) is LTL_TAUT_OF_PL;
then (p=>q)=>((q=>r)=>(p=>r)) in LTL_axioms by Def17;
then X|-(p=>q)=>((q=>r)=>(p=>r)) by Th42;
then X|-(q=>r)=>(p=>r) by A1,Th43;
hence X|-p=>r by A2,Th43;
end;
theorem Th48:
X|-p=>(q=>r) implies X|-(p '&&' q)=>r
proof
set A=(p=>(q=>r))=>((p '&&' q)=>r);
now let f be Function of LTLB_WFF,BOOLEAN;
thus(VAL f).A=(VAL f).(p=>(q=>r))=>(VAL f).((p '&&' q)=>r) by Def15
.=((VAL f).p=>(VAL f).(q=>r))=>(VAL f).((p '&&' q)=>r) by Def15
.=(VAL f).p=>((VAL f).q=>(VAL f).r)=>(VAL f).((p '&&' q)=>r) by Def15
.=(VAL f).p=>((VAL f).q=>(VAL f).r)=>((VAL f).(p '&&' q)=>(VAL f).r) by
Def15
.=(VAL f).p=>((VAL f).q=>(VAL f).r)=>((VAL f).p '&'(VAL f).q=>(VAL f).r)
by Th31
.=1 by Th2;
end;
then A is LTL_TAUT_OF_PL;
then A in LTL_axioms by Def17;
then A1: X|-A by Th42;
assume X|-p=>(q=>r);
hence X|-(p '&&' q)=>r by A1,Th43;
end;
theorem Th49:
X|-(p '&&' q)=>r implies X|-p=>(q=>r)
proof
set A=((p '&&' q)=>r)=>(p=>(q=>r));
now let f be Function of LTLB_WFF,BOOLEAN;
thus(VAL f).A=(VAL f).((p '&&' q)=>r)=>(VAL f).(p=>(q=>r)) by Def15
.=((VAL f).(p '&&' q)=>(VAL f).r)=>(VAL f).(p=>(q=>r)) by Def15
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>(VAL f).(p=>(q=>r)) by Th31
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>((VAL f).p=>(VAL f).(q=>r)) by
Def15
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>((VAL f).p=>((VAL f).q=>(VAL f).r)
) by Def15
.=1 by Th3;
end;
then A is LTL_TAUT_OF_PL;
then A in LTL_axioms by Def17;
then A1: X|-A by Th42;
assume X|-(p '&&' q)=>r;
hence X|-p=>(q=>r) by A1,Th43;
end;
theorem Th50:
X|-(p '&&' q)=>r & X|-p=>s implies X|-(p '&&' q)=>(s '&&' r)
proof
assume that
A1: X|-(p '&&' q)=>r and
A2: X|-p=>s;
set A=((p '&&' q)=>r)=>((p=>s)=>((p '&&' q)=>(s '&&' r)));
now let f be Function of LTLB_WFF,BOOLEAN;
A3: (VAL f).p=0 or(VAL f).p=1 by XBOOLEAN:def 3;
A4: (VAL f).q=0 or(VAL f).q=1 by XBOOLEAN:def 3;
A5: (VAL f).s=0 or(VAL f).s=1 by XBOOLEAN:def 3;
A6: (VAL f).r=0 or(VAL f).r=1 by XBOOLEAN:def 3;
thus(VAL f).A=(VAL f).((p '&&' q)=>r)=>(VAL f).((p=>s)=>((p '&&' q)=>(s '&&'
r))) by Def15
.=((VAL f).(p '&&' q)=>(VAL f).r)=>(VAL f).((p=>s)=>((p '&&' q)=>(s '&&' r)
)) by Def15
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>(VAL f).((p=>s)=>((p '&&' q)=>(s
'&&' r))) by Th31
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>((VAL f).(p=>s)=>(VAL f).((p '&&'
q)=>(s '&&' r))) by Def15
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>(((VAL f).p=>(VAL f).s)=>(VAL f).(
(p '&&' q)=>(s '&&' r))) by Def15
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>(((VAL f).p=>(VAL f).s)=>((VAL f).
(p '&&' q)=>(VAL f).(s '&&' r))) by Def15
.=(((VAL f).p '&'(VAL f).q)=>(VAL f).r)=>(((VAL f).p=>(VAL f).s)=>(((VAL f)
.p '&'(VAL f).q)=>(VAL f).(s '&&' r))) by Th31
.=1 by A3,A4,A6,A5,Th31;
end;
then A is LTL_TAUT_OF_PL;
then A in LTL_axioms by Def17;
then X|-A by Th42;
then X|-((p=>s)=>((p '&&' q)=>(s '&&' r))) by A1,Th43;
hence thesis by A2,Th43;
end;
theorem Th51:
X|-p=>(q=>r) & X|-r=>s implies X|-p=>(q=>s)
proof
assume that
A1: X|-p=>(q=>r) and
A2: X|-r=>s;
set A=(p=>(q=>r))=>((r=>s)=>(p=>(q=>s)));
now let f be Function of LTLB_WFF,BOOLEAN;
A3: (VAL f).p=0 or(VAL f).p=1 by XBOOLEAN:def 3;
A4: (VAL f).r=0 or(VAL f).r=1 by XBOOLEAN:def 3;
set B=(VAL f).(p=>(q=>r)),C=(VAL f).(r=>s),D=(VAL f).(p=>(q=>s));
A5: (VAL f).q=0 or(VAL f).q=1 by XBOOLEAN:def 3;
A6: (VAL f).s=0 or(VAL f).s=1 by XBOOLEAN:def 3;
A7: (VAL f).(p=>(q=>s))=(VAL f).p=>(VAL f).(q=>s) by Def15
.=(VAL f).p=>((VAL f).q=>(VAL f).s) by Def15;
A8: (VAL f).(p=>(q=>r))=(VAL f).p=>(VAL f).(q=>r) by Def15
.=(VAL f).p=>((VAL f).q=>(VAL f).r) by Def15;
thus(VAL f).A=B=>(VAL f).((r=>s)=>(p=>(q=>s))) by Def15
.=B=>(C=>D) by Def15
.=1 by A3,A5,A4,A6,A8,A7,Def15;
end;
then A is LTL_TAUT_OF_PL;
then A in LTL_axioms by Def17;
then X|-A by Th42;
then X|-((r=>s)=>(p=>(q=>s))) by A1,Th43;
hence X|-p=>(q=>s) by A2,Th43;
end;
theorem Th52:
X|-p=>q implies X|-('not' q)=>('not' p)
proof
set A=(p=>q)=>(('not' q)=>('not' p));
now let f be Function of LTLB_WFF,BOOLEAN;
A1: (VAL f).p=0 or(VAL f).p=1 by XBOOLEAN:def 3;
A2: (VAL f).q=0 or(VAL f).q=1 by XBOOLEAN:def 3;
thus(VAL f).A=(VAL f).(p=>q)=>(VAL f).(('not' q)=>('not' p)) by Def15
.=((VAL f).p=>(VAL f).q)=>(VAL f).(('not' q)=>('not' p)) by Def15
.=((VAL f).p=>(VAL f).q)=>((VAL f).(q=>TFALSUM)=>(VAL f).(p=>TFALSUM)) by
Def15
.=((VAL f).p=>(VAL f).q)=>(((VAL f).q=>(VAL f).TFALSUM)=>((VAL f).(p=>
TFALSUM))) by Def15
.=((VAL f).p=>(VAL f).q)=>(((VAL f).q=>FALSE)=>((VAL f).(p=>TFALSUM))) by
Def15
.=((VAL f).p=>(VAL f).q)=>(((VAL f).q=>FALSE)=>(((VAL f).p=>(VAL f).TFALSUM
))) by Def15
.=1 by A1,A2;
end;
then A is LTL_TAUT_OF_PL;
then A in LTL_axioms by Def17;
then A3: X|-A by Th42;
assume X|-p=>q;
hence thesis by A3,Th43;
end;
theorem Th53:
X|-(('X' p)'&&'('X' q))=>('X'(p '&&' q))
proof
set Xp='X' p,nq='not' q,nXq='not' 'X' q,Xnq='X' 'not' q;
Xnq=>nXq in LTL_axioms by Def17;
then A1: X|-Xnq=>nXq by Th42;
('not'('X'(p=>nq)))=>('X'('not'(p=>nq))) in LTL_axioms by Def17;
then A2: X|-('not'('X'(p=>nq)))=>('X'('not'(p=>nq))) by Th42;
('X'(p=>nq))=>(Xp=>Xnq) in LTL_axioms by Def17;
then X|-('X'(p=>nq))=>(Xp=>Xnq) by Th42;
then X|-('X'(p=>nq))=>(Xp=>nXq) by A1,Th51;
then X|-('not'(Xp=>nXq))=>('not'('X'(p=>nq))) by Th52;
hence thesis by A2,Th47;
end;
theorem Th54:
F|-p implies F|-'G' p
proof
assume A1: F|-p;
p=>(p=>p) in LTL_axioms by Th34;
then F|-p=>(p=>p) by Th42;
then A2: F|-p=>p by A1,Th43;
('X' p)=>(p=>('X' p)) in LTL_axioms by Th34;
then A3: F|-('X' p)=>(p=>('X' p)) by Th42;
F|-'X' p by A1,Th44;
then F|-p=>('X' p) by A3,Th43;
then F|-p=>('G' p) by A2,Th45;
hence F|-'G' p by A1,Th43;
end;
theorem Th55:
p=>q in F implies F\/{p}|-'G' q
proof
p in {p} by TARSKI:def 1;
then p in F\/{p} by XBOOLE_0:def 3;
then A1: F\/{p}|-p by Th42;
assume p=>q in F;
then p=>q in F\/{p} by XBOOLE_0:def 3;
then F\/{p}|-p=>q by Th42;
then F\/{p}|-q by A1,Th43;
hence F\/{p}|-'G' q by Th54;
end;
theorem Th56:
F|-q implies F\/{p}|-q
proof
assume F|-q;
then consider f such that
A1: f.len f=q & 1<=len f and
A2: for i be Nat st 1<=i & i<=len f holds prc f,F,i;
now let i be Nat;
assume 1<=i & i<=len f;
then f.i in LTL_axioms or f.i in F or ex j,k be Nat st 1<=j & j**q
proof
set G=F\/{p};
assume G|-q;
then consider f such that
A1: f.len f=q and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,G,i;
defpred P[Nat] means
1<=$1 & $1<=len f implies F|-('G' p)=>f/.$1;
A4: for i being Nat st for j being Nat st j**(('G' p)=>t) in LTL_axioms by Th34;
then A9: F|-t=>(('G' p)=>t) by Th42;
f/.i in LTL_axioms by A6,A7,A8,Lm1;
then F|-t by Th42;
hence thesis by A9,Th43;
end;
suppose A10: f.i in G;
per cases by A10,XBOOLE_0:def 3;
suppose A11: f.i in F;
set t=f/.i;
t=>(('G' p)=>t) in LTL_axioms by Th34;
then A12: F|-t=>(('G' p)=>t) by Th42;
f/.i in F by A6,A7,A11,Lm1;
then F|-t by Th42;
hence thesis by A12,Th43;
end;
suppose A13: f.i in {p};
('G' p)=>(p '&&'('X'('G' p))) in LTL_axioms by Def17;
then A14: F|-('G' p)=>(p '&&'('X'('G' p))) by Th42;
f.i=p by A13,TARSKI:def 1;
then f/.i=p by A6,A7,Lm1;
hence thesis by A14,Th46;
end;
end;
suppose ex j,k be Nat st 1<=j & j**f/.j by A5,A15,A16;
k<=len f by A7,A18,XXREAL_0:2;
then A21: F|-('G' p)=>f/.k by A5,A17,A18;
per cases by A19;
suppose A22: f/.j,f/.k MP_rule f/.i;
set t3=(('G' p)=>(f/.j=>f/.i))=>((('G' p)=>f/.j)=>(('G' p)=>f/.i));
t3 in LTL_axioms by Th35;
then A23: F|-t3 by Th42;
F|-('G' p)=>(f/.j=>f/.i) by A21,A22;
then F|-((('G' p)=>f/.j)=>(('G' p)=>f/.i)) by A23,Th43;
hence F|-('G' p)=>f/.i by A20,Th43;
end;
suppose f/.j,f/.k IND_rule f/.i;
then consider A,B such that
A24: f/.j=A=>B and
A25: f/.k=A=>('X' A) and
A26: f/.i=A=>('G' B);
set Gp='G' p,XGp='X' 'G' p,XA='X' A,Xq='X' q,GB='G' B;
Gp=>(p '&&' XGp) in LTL_axioms by Def17;
then F|-Gp=>(p '&&' XGp) by Th42;
then A27: F|-Gp=>XGp by Th46;
F|-(Gp '&&' A)=>XA by A21,A25,Th48;
then A28: F|-(Gp '&&' A)=>(XGp '&&' XA) by A27,Th50;
F|-(XGp '&&' XA)=>('X'(Gp '&&' A)) by Th53;
then A29: F|-(Gp '&&' A)=>('X'(Gp '&&' A)) by A28,Th47;
F|-(Gp '&&' A)=>B by A20,A24,Th48;
then F|-(Gp '&&' A)=>GB by A29,Th45;
hence thesis by A26,Th49;
end;
end;
suppose A30: ex j be Nat st 1<=j & j**(p '&&'('X'('G' p))) in LTL_axioms by Def17;
then F|-('G' p)=>(p '&&'('X'('G' p))) by Th42;
then A31: F|-('G' p)=>('X'('G' p)) by Th46;
consider j be Nat,q,r such that
A32: 1<=j and
A33: j**f/.j))=>(('X'('G' p))=>'X' f/.j) in LTL_axioms by Def17;
then A35: F|-('X'(('G' p)=>f/.j))=>(('X'('G' p))=>'X' f/.j) by Th42;
j<=len f by A7,A33,XXREAL_0:2;
then F|-'X'(('G' p)=>f/.j) by A5,A32,A33,Th44;
then A36: F|-('X'('G' p))=>'X' f/.j by A35,Th43;
f/.i='X' f/.j by A34;
hence thesis by A36,A31,Th47;
end;
end;
end;
A37: for i be Nat holds P[i] from NAT_1:sch 4(A4);
q=f/.len f by A1,A2,Lm1;
hence F|-('G' p)=>q by A2,A37;
end;
theorem
F|-p=>q implies F\/{p}|-q
proof
p in {p} by TARSKI:def 1;
then p in F\/{p} by XBOOLE_0:def 3;
then A1: F\/{p}|-p by Th42;
assume F|-p=>q;
then F\/{p}|-p=>q by Th56;
hence F\/{p}|-q by A1,Th43;
end;
theorem
F|-('G' p)=>q implies F\/{p}|-q
proof
p in {p} by TARSKI:def 1;
then p in F\/{p} by XBOOLE_0:def 3;
then F\/{p}|-p by Th42;
then A1: F\/{p}|-'G' p by Th54;
assume F|-('G' p)=>q;
then F\/{p}|-('G' p)=>q by Th56;
hence F\/{p}|-q by A1,Th43;
end;
theorem
F|-('G'(p=>q))=>(('G' p)=>('G' q))
proof
reconsider G=F\/{p=>q}\/{p} as Subset of LTLB_WFF;
p=>q in {p=>q} by TARSKI:def 1;
then p=>q in F\/{p=>q} by XBOOLE_0:def 3;
then G|-'G' q by Th55;
then F\/{p=>q}|-('G' p)=>('G' q) by Th57;
hence thesis by Th57;
end;
*