:: Model Checking, Part {III}
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received August 19, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies MODELC_3, SUBSTUT1, MODELC_2, MODELC_1, BOOLE, FUNCT_1, ARYTM_1,
RELAT_1, FINSEQ_1, ORDERS_1, ZF_LANG, ZF_MODEL, FSM_1, FSM_2, NORMSP_1,
FINSET_1, RELOC, SERIES_1, SEQ_1, RLVECT_1, CARD_1, ARYTM_3, ARYTM,
INT_1, CAT_3, TARSKI, SQUARE_1, ALG_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, CARD_1,
NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, NAT_1, RELAT_1, FUNCT_1,
BINOP_1, RELSET_1, FINSEQ_1, ORDERS_1, FUNCOP_1, MARGREL1, FUNCT_2,
INT_1, SEQ_1, SERIES_1, PARTFUN1, MODELC_1, MODELC_2, RFINSEQ2;
constructors BINOP_1, FUNCT_3, XXREAL_0, NAT_1, MARGREL1, ABIAN, ZF_LANG,
KNASTER, MODELC_1, MODELC_2, FINSEQ_1, SERIES_1, FINSEQ_4, FUNCOP_1,
REAL_1, SEQ_2, SEQM_3, NEWTON, PREPOWER, POWER, ORDINAL3, ARYTM_1,
ARYTM_0, FUNCT_4, FUNCT_7, XCMPLX_0, XREAL_0, RFINSEQ2, NUMBERS,
VALUED_1, SEQ_1, VALUED_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCT_2, FUNCOP_1, ARYTM_3, XXREAL_0, XREAL_0, NAT_1, INT_1, ORDERS_1,
XBOOLEAN, MARGREL1, KNASTER, FINSET_1, CARD_5, MODELC_1, MODELC_2,
FINSEQ_1, RELSET_1, NUMBERS, VALUED_0, VALUED_1, SERIES_1, MEMBERED,
SEQM_3, NEWTON, CARD_1, ARYTM_2, XCMPLX_0, REAL_1;
requirements REAL, NUMERALS, ARITHM, SUBSET, BOOLE;
definitions RELAT_1, TARSKI, BINOP_1, MARGREL1, XBOOLEAN, MODELC_1, MODELC_2,
SERIES_1, FINSEQ_4, NAT_1, SUBSET_1;
theorems RELSET_1, XBOOLE_0, ZFMISC_1, XBOOLE_1, TARSKI, FUNCT_1, FUNCT_2,
FUNCT_7, WELLORD2, NAT_1, INT_1, ENUMSET1, XREAL_1, FINSEQ_1, ORDERS_1,
XXREAL_0, MODELC_1, MODELC_2, ORDINAL1, SUBSET_1, FINSEQ_4, SERIES_1,
CARD_1, CARD_2, SERIES_2, FINSET_1, RFINSEQ2, FINSEQ_3, SUBSET;
schemes NAT_1, FUNCT_2, MODELC_2, TARSKI, FUNCT_1, FINSEQ_1, RECDEF_1;
begin
reserve k,k1,n,n1,m,m1,m0,m01,h,i,i1,j,j1 for Nat,
a,b,x,y,X,X1,X2,X3,X4,Y,Z for set,
D,D1,D2,S for non empty set;
reserve L,L',L1,L2 for FinSequence;
reserve F,F1,G,G1,H for LTL-formula;
reserve W,W1,W2 for Subset of Subformulae H;
reserve v for LTL-formula;
reserve r,r1,r2 for real number;
LemSUM01:
a in (X1 \/ X2) \/ X3 iff (a in X1) or (a in X2) or (a in X3)
proof
a in (X1 \/ X2) \/ X3 iff
(a in (X1 \/ X2)) or (a in X3) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
LemSUM02:
a in (X1 \ X2) \/ (X3\ X4) iff
(a in X1 & not a in X2) or (a in X3 & not a in X4)
proof
a in (X1 \ X2) \/ (X3 \ X4) iff
(a in X1 \ X2) or (a in X3 \ X4) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 5;
end;
LemFinSeq01:
(<* H *>).1 = H & (rng <* H *> = {H})
proof
set p = <* H *>;
dom p = {1} & p.1= H by FINSEQ_1:4,def 8;
hence thesis by FUNCT_1:14;
end;
LemReal01:
for r1,r2 being real number holds
r1<=r2 implies [\ r1 /] <= [\ r2 /]
proof
let r1,r2 be real number;
r1<=r2 implies [\ r1 /] <= [\ r2 /]
proof
assume B1:r1<=r2;
now assume [\ r2 /] < [\ r1 /];
then B2:[\ r2 /] +1 <= [\ r1 /] by INT_1:20;
[\ r1 /] <= r1 by INT_1:def 4;
then [\ r2 /] +1 <= r1 by B2,XXREAL_0:2;
hence contradiction by B1,INT_1:52,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis;
end;
LemReal02:
for r1,r2 being real number holds
r1<=r2-1 implies [\ r1 /] <= [\ r2 /]-1
proof
let r1,r2 be real number;
r1<=r2-1 implies [\ r1 /] <= [\ r2 /]-1
proof
assume r1<=r2-1;
then r1+1<=r2-1 +1 by XREAL_1:8;
then [\ r1+1 /] <= [\ r2 /] by LemReal01;
then [\ r1 /] +1 <= [\ r2 /] by INT_1:51;
then [\ r1 /]+1 -1 <= [\ r2 /] -1 by XREAL_1:11;
hence thesis;
end;
hence thesis;
end;
Lem1006:n=0 or 1<=n
proof
n=0 or 0<0+n;
hence thesis by NAT_1:19;
end;
Lem101:
(H is negative or H is next) implies the_argument_of H is_subformula_of H
proof
set G = the_argument_of H;
assume (H is negative or H is next);
then G is_immediate_constituent_of H by MODELC_2:20,21;
then G is_proper_subformula_of H by MODELC_2:29;
hence thesis by MODELC_2:def 23;
end;
Lem102:
(H is conjunctive or H is disjunctive or H is Until or H is Release)
implies the_left_argument_of H is_subformula_of H
& the_right_argument_of H is_subformula_of H
proof
set G1 = the_left_argument_of H;
set G2 = the_right_argument_of H;
assume (H is conjunctive or H is disjunctive or H is Until
or H is Release);
then (G1 is_immediate_constituent_of H)
& (G2 is_immediate_constituent_of H)
by MODELC_2:22,23,24,25;
then (G1 is_proper_subformula_of H)
& (G2 is_proper_subformula_of H) by MODELC_2:29;
hence thesis by MODELC_2:def 23;
end;
Lem104:
F is_subformula_of H implies {F} is Subset of Subformulae H
proof
set E = Subformulae H;
assume F is_subformula_of H;
then F in E by MODELC_2:45;
hence thesis by SUBSET_1:63;
end;
Lem106:
F is_subformula_of H & G is_subformula_of H
implies {F,G} is Subset of Subformulae H
proof
set E = Subformulae H;
assume F is_subformula_of H & G is_subformula_of H;
then F in E & G in E by MODELC_2:45;
hence thesis by SUBSET_1:56;
end;
Lem107:
H is disjunctive or H is conjunctive or
H is Until or H is Release
implies {the_left_argument_of H,the_right_argument_of H }
is Subset of Subformulae H
proof
assume H is disjunctive or H is conjunctive or
H is Until or H is Release;
then the_left_argument_of H is_subformula_of H
& the_right_argument_of H is_subformula_of H by Lem102;
hence thesis by Lem106;
end;
Lem108:
H is disjunctive or H is conjunctive or
H is Until or H is Release
implies ({the_left_argument_of H} is Subset of Subformulae H) &
({the_right_argument_of H} is Subset of Subformulae H)
proof
assume H is disjunctive or H is conjunctive or
H is Until or H is Release;
then the_left_argument_of H is_subformula_of H
& the_right_argument_of H is_subformula_of H by Lem102;
hence thesis by Lem104;
end;
Lem109:
{H} is Subset of Subformulae H by Lem104,MODELC_2:27;
Lem110:
H is negative or H is next
implies ({the_argument_of H} is Subset of Subformulae H)
proof
assume H is negative or H is next;
then the_argument_of H is_subformula_of H by Lem101;
hence thesis by Lem104;
end;
definition let F;
redefine func Subformulae F -> Subset of LTL_WFF;
coherence
proof
set E = Subformulae F;
E is Subset of E by SUBSET:3;
hence thesis by MODELC_2:47;
end;
end;
:: definition of basic operations to build an automaton for LTL.
definition let H;
func LTLNew1 H -> Subset of Subformulae H equals
:Def203:
{the_left_argument_of H,the_right_argument_of H } if H is conjunctive,
{the_left_argument_of H } if H is disjunctive,
{} if H is next,
{the_left_argument_of H } if H is Until,
{the_right_argument_of H } if H is Release
otherwise {};
correctness by Lem107,Lem108,MODELC_2:78,SUBSET_1:4;
func LTLNew2 H -> Subset of Subformulae H equals
:Def204:
{} if H is conjunctive,
{the_right_argument_of H } if H is disjunctive,
{} if H is next,
{the_right_argument_of H } if H is Until,
{the_left_argument_of H,the_right_argument_of H } if H is Release
otherwise {};
correctness by Lem107,Lem108,MODELC_2:78,SUBSET_1:4;
func LTLNext H -> Subset of Subformulae H equals
:Def205:
{} if H is conjunctive,
{} if H is disjunctive,
{the_argument_of H} if H is next,
{H} if H is Until,
{H} if H is Release
otherwise {};
correctness by Lem109,Lem110,MODELC_2:78,SUBSET_1:4;
end;
definition let v;
struct LTLnode over v
(#LTLold,LTLnew,LTLnext -> Subset of Subformulae v #);
end;
definition let v; let N be LTLnode over v; let H;
assume A1:H in the LTLnew of N;
func SuccNode1(H,N) -> strict LTLnode over v means
:Def206: the LTLold of it =(the LTLold of N) \/ {H} &
the LTLnew of it = ((the LTLnew of N) \ {H})
\/ (LTLNew1 H \ the LTLold of N) &
the LTLnext of it = (the LTLnext of N) \/ LTLNext H;
existence
proof
set Old= (the LTLold of N) \/ {H};
set NewA= (the LTLnew of N) \ {H};
set NewB=LTLNew1 H \ the LTLold of N;
set NewC = NewA \/ NewB;
set NextD = (the LTLnext of N) \/ LTLNext H;
{H} c= Subformulae v by A1,ZFMISC_1:37;
then reconsider Old as Subset of Subformulae v by XBOOLE_1:8;
consider F such that A9:H=F and A10: F is_subformula_of v
by A1,MODELC_2:def 24;
A11:Subformulae H c= Subformulae v by A9,A10,MODELC_2:46;
then NewB c= Subformulae v by XBOOLE_1:1;
then reconsider NewC as Subset of Subformulae v by XBOOLE_1:8;
LTLNext H c= Subformulae v by A11,XBOOLE_1:1;
then reconsider NextD as Subset of Subformulae v by XBOOLE_1:8;
set IT = LTLnode(#Old,NewC,NextD#);
take IT;
thus thesis;
end;
uniqueness;
end;
definition let v; let N be LTLnode over v; let H;
assume A1:(H in the LTLnew of N) &
(H is disjunctive or H is Until or H is Release);
func SuccNode2(H,N) -> strict LTLnode over v means
:Def207: the LTLold of it =(the LTLold of N) \/ {H} &
the LTLnew of it = ((the LTLnew of N) \ {H})
\/ (LTLNew2 H \ the LTLold of N) &
the LTLnext of it = the LTLnext of N;
existence
proof
set Old= (the LTLold of N) \/ {H};
set NewA= (the LTLnew of N) \ {H};
set NewB=LTLNew2 H \ the LTLold of N;
set NewC = NewA \/ NewB;
set NextD = the LTLnext of N;
{H} c= Subformulae v by A1,ZFMISC_1:37;
then reconsider Old as Subset of Subformulae v by XBOOLE_1:8;
consider F such that A9:H=F and A10: F is_subformula_of v
by A1,MODELC_2:def 24;
Subformulae H c= Subformulae v by A9,A10,MODELC_2:46;
then NewB c= Subformulae v by XBOOLE_1:1;
then reconsider NewC as Subset of Subformulae v by XBOOLE_1:8;
set IT = LTLnode(#Old,NewC,NextD#);
take IT;
thus thesis;
end;
uniqueness;
end;
definition let v; let N1,N2 be LTLnode over v; let H;
pred N2 is_succ_of N1,H means
:DefSucc01:H in the LTLnew of N1 &
(N2 = SuccNode1(H,N1) or
(H is disjunctive or H is Until or H is Release) &
N2=SuccNode2(H,N1));
end;
definition let v; let N1,N2 be LTLnode over v;
pred N2 is_succ1_of N1 means
:Def208:ex H st H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
pred N2 is_succ2_of N1 means
:Def209:ex H st H in the LTLnew of N1 &
(H is disjunctive or H is Until or H is Release) &
N2=SuccNode2(H,N1);
end;
definition let v; let N1,N2 be LTLnode over v;
pred N2 is_succ_of N1 means
:Def210:N2 is_succ1_of N1 or N2 is_succ2_of N1;
end;
definition let v; let N be LTLnode over v;
attr N is failure means
ex H,F st H is atomic & F = 'not' H
& H in the LTLold of N & F in the LTLold of N;
end;
definition let v; let N be LTLnode over v;
attr N is elementary means
:Defelementary:the LTLnew of N = {};
end;
definition let v; let N be LTLnode over v;
attr N is final means
N is elementary & the LTLnext of N = {};
end;
definition let v;
func {}v -> Subset of Subformulae v equals
{};
correctness by SUBSET_1:4;
end;
definition let v;
func Seed v -> Subset of Subformulae v equals
{v};
correctness by Lem104,MODELC_2:27;
end;
registration let v;
cluster elementary strict LTLnode over v;
existence
proof
set X = LTLnode(# {}v,{}v,{}v #);
take X;
thus thesis by Defelementary;
end;
end;
definition let v;
func FinalNode v -> elementary strict LTLnode over v equals
LTLnode(# {}v,{}v,{}v #);
correctness by Defelementary;
end;
definition let x, v;
func CastNode(x,v) -> strict LTLnode over v equals :defCastNode01:
x if x is strict LTLnode over v
otherwise LTLnode(# {}v,{}v,{}v #);
correctness;
end;
definition let v;
func init v -> elementary strict LTLnode over v equals
LTLnode(# {}v,{}v,Seed v #);
correctness by Defelementary;
end;
definition let v; let N be LTLnode over v;
func 'X' N -> strict LTLnode over v equals
LTLnode(# {}v,the LTLnext of N,{}v #);
correctness;
end;
:: Some properties of basic operations to build an automaton for LTL.
reserve N,N1,N2,N3,N10,N20,M,M1,M2 for strict LTLnode over v;
reserve w for Element of Inf_seq(AtomicFamily);
definition let v, L;
pred L is_Finseq_for v means :DefFinseq:
for k st 1 <= k & k < len(L) holds
ex N,M st N = L.k & M=L.(k+1) & M is_succ_of N;
end;
lemFinseq01:
L is_Finseq_for v & 1<= m & m<=len(L)
implies ex L1,L2 st L2 is_Finseq_for v &
L = L1^L2 & L2.1=L.m &1<=len(L2) &
len(L2) =len(L)-(m-1) &
L2.(len(L2)) = L.(len(L))
proof
assume that A1:L is_Finseq_for v and A2:1<= m & m<=len(L);
set m1=m-1;
m-m<=len(L)-m by A2,XREAL_1:11;
then A201:0+1<=(len(L)-m)+1 by XREAL_1:8;
reconsider m1 as Nat by A2,NAT_1:21;
set L1=L|Seg m1;
reconsider L1 as FinSequence by FINSEQ_1:19;
a4: m-1<=len(L)-0 by A2,XREAL_1:15;
then A4:len(L1) = m1 by FINSEQ_1:21;
consider L2 being FinSequence such that A5: L = L1^L2 by FINSEQ_1:101;
len(L)=len(L1)+len(L2) by A5,FINSEQ_1:35;
then A601:len(L2) = len(L)-len(L1) .= len(L)-m1 by a4,FINSEQ_1:21;
then len(L2) in dom L2 by A201,FINSEQ_3:27;
then A7:L2.(len(L2)) =L.(len(L1)+len(L2)) by A5,FINSEQ_1:def 7
.= L.(len(L)) by A5,FINSEQ_1:35;
1 in dom L2 by A601,A201,FINSEQ_3:27;
then A9:L2.1 = L.(len(L1) + 1) by A5,FINSEQ_1:def 7
.= L.(m1+1) by a4,FINSEQ_1:21 .=L.m;
for k st 1 <= k & k < len(L2) holds
ex N,M st N = L2.k & M=L2.(k+1) & M is_succ_of N
proof
let k such that B1:1 <= k & k < len(L2);
set km1=k+m1;
B101:1+0<= k+m1 by B1,XREAL_1:9;
km1 <(len(L)-m1) +m1 by A601,B1,XREAL_1:8;
then consider N,M such that B2: N = L.km1 & M=L.(km1+1) &
M is_succ_of N by A1,DefFinseq,B101;
B201:k in dom L2 by B1,FINSEQ_3:27;
B3:N = L2.k by A4,A5,B201,B2,FINSEQ_1:def 7;
set k1=k+1;
1<=k1 & k1<=len(L2) by B1,NAT_1:13;
then B301:k1 in dom L2 by FINSEQ_3:27;
M = L.(m1+k1) by B2
.= L2.(k1) by A4,A5,B301,FINSEQ_1:def 7;
hence thesis by B2,B3;
end;
then L2 is_Finseq_for v by DefFinseq;
hence thesis by A5,A601,A201,A7,A9;
end;
definition let v, N1,N2;
pred N2 is_next_of N1 means
:Def215:N1 is elementary & N2 is elementary &
ex L st 1<=len(L) & L is_Finseq_for v &
L.1 = 'X' N1 & L.(len(L)) = N2;
end;
definition let v; let W be Subset of Subformulae v;
func CastLTL(W) -> Subset of LTL_WFF equals
W;
correctness by MODELC_2:47;
end;
definition let v, N;
func *N -> Subset of LTL_WFF equals
((the LTLold of N) \/ (the LTLnew of N))
\/ 'X' CastLTL(the LTLnext of N);
correctness
proof
set S1= the LTLold of N;
set S2= the LTLnew of N;
set S3= CastLTL(the LTLnext of N);
A1:S1 is Subset of LTL_WFF by MODELC_2:47;
S2 is Subset of LTL_WFF by MODELC_2:47;
then A2:S1 \/ S2 c= LTL_WFF by A1,XBOOLE_1:8;
reconsider S3 as Subset of LTL_WFF;
thus thesis by A2,XBOOLE_1:8;
end;
end;
LemSUM04:
(H in the LTLnew of N) & (H is atomic or H is negative)
implies *N = *SuccNode1(H,N)
proof
set N1 = SuccNode1(H,N);
assume A1:(H in the LTLnew of N) & (H is atomic or H is negative);
A3:(not H is conjunctive) & (not H is disjunctive) &
(not H is next) & (not H is Until) & (not H is Release)
by A1,MODELC_2:78;
then A4:LTLNew1 H ={} by Def203;
A5:LTLNext H = {} by A3,Def205;
set N1O = the LTLold of N1;
set N1N = the LTLnew of N1;
set N1X = the LTLnext of N1;
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
A6:N1O = NO \/ {H} &
N1N = (NN \ {H}) \/ (LTLNew1 H \ NO) &
N1X = NX \/ LTLNext H by A1,Def206;
N1O \/ N1N = NO \/ NN
proof
B1:a in N1O \/ N1N implies a in NO \/ NN
proof
assume C1:a in N1O \/ N1N;
a in N1O implies a in NO or a in {H}
by A6,XBOOLE_0:def 3;
then C2:a in N1O implies a in NO or a in NN by A1,TARSKI:def 1;
a in N1N implies a in NN & not a in {H} by A6,A4,XBOOLE_0:def 5;
hence thesis by C1,C2,XBOOLE_0:def 3;
end;
a in NO \/ NN implies a in N1O \/ N1N
proof
assume C1:a in NO \/ NN;
C2:a in NO implies a in N1O by A6,XBOOLE_0:def 3;
a in NN implies (not a in {H} & a in NN) or
(a in {H} & a in NN);
then a in NN implies (a in NN \ {H}) or (a in NO \/{H} )
by XBOOLE_0:def 3,def 5;
hence thesis by A6,A4,C1,C2,XBOOLE_0:def 3;
end;
hence thesis by B1,TARSKI:2;
end;
hence thesis by A6,A5;
end;
LemSUM06:
(H in the LTLnew of N) & (H is conjunctive or H is next ) implies
(w |= *N iff w |= *SuccNode1(H,N))
proof
assume that A1: (H in the LTLnew of N) and
A2: (H is conjunctive or H is next);
set SN=SuccNode1(H,N);
set SNO = the LTLold of SN;
set SNN = the LTLnew of SN;
set SNX = the LTLnext of SN;
set XSNX = 'X' CastLTL(SNX);
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
set XNX = 'X' CastLTL(NX);
A3:H in *N by LemSUM01,A1;
A4:w |= *N implies w |= *SN
proof
assume B1:w |= *N;
then B2:w |= H by A3,MODELC_2:def 66;
for F being LTL-formula st F in *SN holds w|= F
proof
let F be LTL-formula such that C1: F in *SN;
now per cases by C1,LemSUM01;
suppose F in SNO;
then D1:F in NO \/ {H} by A1,Def206;
now per cases by D1,XBOOLE_0:def 3;
suppose F in NO;
then F in *N by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
suppose F in {H};
then F in *N by A3,TARSKI:def 1;
hence thesis by B1,MODELC_2:def 66;
end;
end;
hence thesis;
end;
suppose F in SNN;
then D1:F in (NN \ {H})\/ (LTLNew1 H \ NO) by A1,Def206;
now per cases by D1,LemSUM02;
suppose F in NN;
then F in (NO \/ NN) \/ XNX by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
suppose D2: F in (LTLNew1 H);
now per cases by A2;
suppose E1:H is conjunctive;
then F in {the_left_argument_of H,
the_right_argument_of H } by D2,Def203;
then E2:F = the_left_argument_of H or
F = the_right_argument_of H by TARSKI:def 2;
H =(the_left_argument_of H) '&'
(the_right_argument_of H) by E1,MODELC_2:6;
hence thesis by B2,E2,MODELC_2:65;
end;
suppose H is next;
hence thesis by D2,Def203;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose C1:F in XSNX;
set SN1 = CastLTL(SNX);
D0:SN1 = NX \/ LTLNext H by A1,Def206;
consider G such that D1:F=G and
D2:ex G1 st (G1 in SN1 & G ='X' G1) by C1;
consider G1 such that D3:G1 in SN1 and
D4:G ='X' G1 by D2;
now per cases by D0,D3,XBOOLE_0:def 3;
suppose G1 in NX;
then F in XNX by D1,D4;
then F in (NO \/ NN) \/ XNX by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
suppose E2:G1 in LTLNext H;
now per cases by A2;
suppose E21:H is next;
then G1 in {the_argument_of H} by E2,Def205;
then G1 = the_argument_of H by TARSKI:def 1;
hence thesis by B2,E21,D1,D4,MODELC_2:5;
end;
suppose H is conjunctive;
hence thesis by E2,Def205;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by MODELC_2:def 66;
end;
w |= *SN implies w |= *N
proof
assume B1:w |= *SN;
for F being LTL-formula st F in *N holds w|= F
proof
let F be LTL-formula such that C1: F in *N;
now per cases by C1,LemSUM01;
suppose F in NO;
then F in NO \/ {H} by XBOOLE_0:def 3;
then F in SNO by Def206,A1;
then F in *SN by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
suppose C3:F in NN;
now per cases;
suppose F=H;
then F in {H} by TARSKI:def 1;
then F in NO \/ {H} by XBOOLE_0:def 3;
then F in SNO by Def206,A1;
then F in *SN by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
suppose not(F=H);
then not F in {H} by TARSKI:def 1;
then F in NN \ {H} by C3,XBOOLE_0:def 5;
then F in (NN \ {H}) \/(LTLNew1 H \ NO) by XBOOLE_0:def 3;
then F in SNN by Def206,A1;
then F in *SN by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
end;
hence thesis;
end;
suppose C3:F in XNX;
set N1 = CastLTL(NX);
set SN11= (NX) \/ LTLNext H;
SNX = SN11 by A1,Def206;
then reconsider SN11 as Subset of Subformulae v;
set SN1 =CastLTL(SN11);
consider G such that D1:F=G and
D2:ex G1 st (G1 in N1 &
G ='X' G1) by C3;
consider G1 such that D3:G1 in N1 and
D4:G ='X' G1 by D2;
G1 in SN11 by D3,XBOOLE_0:def 3;
then F in 'X' SN1 by D1,D4;
then F in XSNX by Def206,A1;
then F in *SN by LemSUM01;
hence thesis by B1,MODELC_2:def 66;
end;
end;
hence thesis;
end;
hence thesis by MODELC_2:def 66;
end;
hence thesis by A4;
end;
theorem
H in the LTLnew of N &
(H is atomic or H is negative or H is conjunctive or H is next ) implies
(w |= *N iff w |= *SuccNode1(H,N))
by LemSUM04,LemSUM06;
Lem203:
(H in the LTLnew of N) & (H is disjunctive) implies
(w |= *N iff (w |= *SuccNode1(H,N) or w |= *SuccNode2(H,N)))
proof
assume that A1: (H in the LTLnew of N) and
A2: (H is disjunctive);
set SN1=SuccNode1(H,N);
set SN1O = the LTLold of SN1;
set SN1N = the LTLnew of SN1;
set SN1X = the LTLnext of SN1;
set XSN1X = 'X' CastLTL(SN1X);
set SN2=SuccNode2(H,N);
set SN2O = the LTLold of SN2;
set SN2N = the LTLnew of SN2;
set SN2X = the LTLnext of SN2;
set XSN2X = 'X' CastLTL(SN2X);
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
set XNX = 'X' CastLTL(NX);
A3:H in *N by LemSUM01,A1;
set H1 = the_left_argument_of H;
set H2 = the_right_argument_of H;
H = H1 'or' H2 by A2,MODELC_2:7;
then A4:w|= H iff w|= H1 or w|= H2 by MODELC_2:66;
A5:LTLNew1 H = {H1} by A2,Def203;
A6:LTLNew2 H = {H2} by A2,Def204;
A7:LTLNext H = {} by A2,Def205;
A8:SN1O = NO \/ {H} by A1,Def206;
A9:SN1N = (NN \ {H}) \/ ({H1} \ NO) by A1,Def206,A5;
A10:SN1X = NX \/ {} by A1,Def206,A7 .= NX;
A11:SN2O = NO \/ {H} by A1,A2,Def207;
A12:SN2N = (NN \ {H}) \/ ({H2} \ NO) by A1,A2,Def207,A6;
A13:SN2X = NX by A1,A2,Def207;
Alem1:F in *SN1 implies (F in *N) or (F=H1)
proof
assume B1:F in *SN1;
now per cases by B1,LemSUM01;
suppose F in SN1O;
then (F in NO) or (F in {H}) by A8,XBOOLE_0:def 3;
hence thesis by LemSUM01,A3,TARSKI:def 1;
end;
suppose F in SN1N;
then (F in (NN \ {H})) or (F in ({H1} \ NO)) by A9,XBOOLE_0:def 3;
then (F in NN) or (F in {H1}) by XBOOLE_0:def 5;
hence thesis by LemSUM01,TARSKI:def 1;
end;
suppose F in XSN1X;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(SN1X) &
G ='X' G1);
consider G1 such that C3:G1 in SN1X and
C4:G ='X' G1 by C2;
F in XNX by C1,C4,C3,A10;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
Alem2:F in *SN2 implies (F in *N) or (F=H2)
proof
assume B1:F in *SN2;
now per cases by B1,LemSUM01;
suppose F in SN2O;
then (F in NO) or (F in {H}) by A11,XBOOLE_0:def 3;
hence thesis by LemSUM01,A3,TARSKI:def 1;
end;
suppose F in SN2N;
then (F in (NN \ {H})) or (F in ({H2} \ NO)) by A12,XBOOLE_0:def 3;
then (F in NN) or (F in {H2}) by XBOOLE_0:def 5;
hence thesis by LemSUM01,TARSKI:def 1;
end;
suppose F in XSN2X;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(SN2X) &
G ='X' G1);
consider G1 such that C3:G1 in SN2X and
C4:G ='X' G1 by C2;
F in XNX by C1,C4,C3,A13;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
Alem3:F in *N implies (F in *SN1) & (F in *SN2)
proof
assume B1:F in *N;
now per cases by B1,LemSUM01;
suppose F in NO;
then (F in SN1O) & (F in SN2O) by A8,A11,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
suppose C2:F in NN;
now per cases;
suppose F=H;
then F in {H} by TARSKI:def 1;
then (F in SN1O) & (F in SN2O) by A8,A11,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
suppose not (F=H);
then not (F in {H}) by TARSKI:def 1;
then F in (NN \ {H}) by C2,XBOOLE_0:def 5;
then (F in SN1N) & (F in SN2N) by A9,A12,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
suppose F in XNX;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(NX) & G ='X' G1);
consider G1 such that C3:G1 in NX and
C4:G ='X' G1 by C2;
(F in XSN1X) & (F in XSN2X) by C1,C4,C3,A10,A13;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
A17:w |= *N implies (w |= *SN1 or w |= *SN2)
proof
assume B1:w |= *N;
now per cases by B1,A3,A4,MODELC_2:def 66;
suppose B3:w|= H1;
F in *SN1 implies w|= F
proof
assume F in *SN1;
then (F in *N) or (F=H1) by Alem1;
hence thesis by B1,B3,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
suppose B4:w|= H2;
F in *SN2 implies w|= F
proof
assume F in *SN2;
then (F in *N) or (F=H2) by Alem2;
hence thesis by B1,B4,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
end;
hence thesis;
end;
(w |= *SN1 or w |= *SN2) implies w |= *N
proof
assume B1:w |= *SN1 or w |= *SN2;
F in *N implies w |= F
proof
assume F in *N;
then C1:(F in *SN1) & (F in *SN2) by Alem3;
now per cases by B1;
suppose w |= *SN1;
hence thesis by C1,MODELC_2:def 66;
end;
suppose w |= *SN2;
hence thesis by C1,MODELC_2:def 66;
end;
end;
hence thesis;
end;
hence thesis by MODELC_2:def 66;
end;
hence thesis by A17;
end;
Lem204:
(H in the LTLnew of N) & (H is Until) implies
(w |= *N iff (w |= *SuccNode1(H,N) or w |= *SuccNode2(H,N)))
proof
assume that A1: (H in the LTLnew of N) and
A2: (H is Until);
set SN1=SuccNode1(H,N);
set SN1O = the LTLold of SN1;
set SN1N = the LTLnew of SN1;
set SN1X = the LTLnext of SN1;
set XSN1X = 'X' CastLTL(SN1X);
set SN2=SuccNode2(H,N);
set SN2O = the LTLold of SN2;
set SN2N = the LTLnew of SN2;
set SN2X = the LTLnext of SN2;
set XSN2X = 'X' CastLTL(SN2X);
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
set XNX = 'X' CastLTL(NX);
A3:H in *N by LemSUM01,A1;
set H1 = the_left_argument_of H;
set H2 = the_right_argument_of H;
H = H1 'U' H2 by A2,MODELC_2:8;
then w|= H iff w|=H2 'or' (H1 '&' ('X' H)) by MODELC_2:75;
then A4:w|= H iff w|=H2 or w |= (H1 '&' ('X' H)) by MODELC_2:66;
A5:LTLNew1 H = {H1} by A2,Def203;
A6:LTLNew2 H = {H2} by A2,Def204;
A7:LTLNext H = {H} by A2,Def205;
A8:SN1O = NO \/ {H} by A1,Def206;
A9:SN1N = (NN \ {H}) \/ ({H1} \ NO) by A1,Def206,A5;
A10:SN1X = NX \/ {H} by A1,Def206,A7;
A11:SN2O = NO \/ {H} by A1,A2,Def207;
A12:SN2N = (NN \ {H}) \/ ({H2} \ NO) by A1,A2,Def207,A6;
A13:SN2X = NX by A1,A2,Def207;
Alem1:F in *SN1 implies (F in *N) or (F=H1) or (F='X' H)
proof
assume B1:F in *SN1;
now per cases by B1,LemSUM01;
suppose F in SN1O;
then (F in NO) or (F in {H}) by A8,XBOOLE_0:def 3;
hence thesis by LemSUM01,A3,TARSKI:def 1;
end;
suppose F in SN1N;
then (F in (NN \ {H})) or (F in ({H1} \ NO)) by A9,XBOOLE_0:def 3;
then (F in NN) or (F in {H1}) by XBOOLE_0:def 5;
hence thesis by LemSUM01,TARSKI:def 1;
end;
suppose F in XSN1X;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(SN1X) & G ='X' G1);
consider G1 such that C3:G1 in SN1X and
C4:G ='X' G1 by C2;
C5:G1 in NX or G1 in {H} by C3,A10,XBOOLE_0:def 3;
now per cases by C5,TARSKI:def 1;
suppose G1 in NX;
then F in XNX by C1,C4;
hence thesis by LemSUM01;
end;
suppose G1=H;
hence thesis by C1,C4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Alem2:F in *SN2 implies (F in *N) or (F=H2)
proof
assume B1:F in *SN2;
now per cases by B1,LemSUM01;
suppose F in SN2O;
then (F in NO) or (F in {H}) by A11,XBOOLE_0:def 3;
hence thesis by LemSUM01,A3,TARSKI:def 1;
end;
suppose F in SN2N;
then (F in (NN \ {H})) or (F in ({H2} \ NO)) by A12,XBOOLE_0:def 3;
then (F in NN) or (F in {H2}) by XBOOLE_0:def 5;
hence thesis by LemSUM01,TARSKI:def 1;
end;
suppose F in XSN2X;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(SN2X) &
G ='X' G1);
consider G1 such that C3:G1 in SN2X and
C4:G ='X' G1 by C2;
F in XNX by C1,C4,C3,A13;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
Alem3:F in *N implies (F in *SN1) & (F in *SN2)
proof
assume B1:F in *N;
now per cases by B1,LemSUM01;
suppose F in NO;
then (F in SN1O) & (F in SN2O) by A8,A11,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
suppose C2:F in NN;
now per cases;
suppose F=H;
then F in {H} by TARSKI:def 1;
then (F in SN1O) & (F in SN2O) by A8,A11,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
suppose F <> H;
then not F in {H} by TARSKI:def 1;
then F in (NN \ {H}) by C2,XBOOLE_0:def 5;
then (F in SN1N) & (F in SN2N) by A9,A12,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
suppose F in XNX;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(NX) &
G ='X' G1);
consider G1 such that C3:G1 in NX and
C4:G ='X' G1 by C2;
C5:G1 in SN1X by C3,A10,XBOOLE_0:def 3;
(F in XSN1X) & (F in XSN2X) by C1,C4,C3,C5,A13;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
A17:w |= *N implies (w |= *SN1 or w |= *SN2)
proof
assume B1:w |= *N;
now per cases by A3,A4,B1,MODELC_2:65,def 66;
suppose B3:(w|=H1 & w|='X' H);
F in *SN1 implies w|= F
proof
assume F in *SN1;
then (F in *N) or (F=H1) or (F='X' H) by Alem1;
hence thesis by B1,B3,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
suppose B4:w|= H2;
F in *SN2 implies w|= F
proof
assume F in *SN2;
then (F in *N) or (F=H2) by Alem2;
hence thesis by B1,B4,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
end;
hence thesis;
end;
(w |= *SN1 or w |= *SN2) implies w |= *N
proof
assume B1:w |= *SN1 or w |= *SN2;
F in *N implies w |= F
proof
assume F in *N;
then C1:(F in *SN1) & (F in *SN2) by Alem3;
now per cases by B1;
suppose w |= *SN1;
hence thesis by C1,MODELC_2:def 66;
end;
suppose w |= *SN2;
hence thesis by C1,MODELC_2:def 66;
end;
end;
hence thesis;
end;
hence thesis by MODELC_2:def 66;
end;
hence thesis by A17;
end;
Lem205:
(H in the LTLnew of N) & (H is Release) implies
(w |= *N iff (w |= *SuccNode1(H,N) or w |= *SuccNode2(H,N)))
proof
assume that A1: (H in the LTLnew of N) and
A2: (H is Release);
set SN1=SuccNode1(H,N);
set SN1O = the LTLold of SN1;
set SN1N = the LTLnew of SN1;
set SN1X = the LTLnext of SN1;
set XSN1X = 'X' CastLTL(SN1X);
set SN2=SuccNode2(H,N);
set SN2O = the LTLold of SN2;
set SN2N = the LTLnew of SN2;
set SN2X = the LTLnext of SN2;
set XSN2X = 'X' CastLTL(SN2X);
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
set XNX = 'X' CastLTL(NX);
A3:H in *N by LemSUM01,A1;
set H1 = the_left_argument_of H;
set H2 = the_right_argument_of H;
H = H1 'R' H2 by A2,MODELC_2:9;
then w|= H iff w|=(H1 '&' H2) 'or' (H2 '&' ('X' (H)))
by MODELC_2:76;
then A4:w|= H iff (w|=(H1 '&' H2)) or (w |= (H2 '&' ('X' H)))
by MODELC_2:66;
A5:LTLNew1 H = {H2} by A2,Def203;
A6:LTLNew2 H = {H1,H2} by A2,Def204;
A7:LTLNext H = {H} by A2,Def205;
A8:SN1O = NO \/ {H} by A1,Def206;
A9:SN1N = (NN \ {H}) \/ ({H2} \ NO) by A1,Def206,A5;
A10:SN1X = NX \/ {H} by A1,Def206,A7;
A11:SN2O = NO \/ {H} by A1,A2,Def207;
A12:SN2N = (NN \ {H}) \/ ({H1,H2} \ NO) by A1,A2,Def207,A6;
A13:SN2X = NX by A1,A2,Def207;
Alem1:F in *SN1 implies (F in *N) or (F=H2) or (F='X' H)
proof
assume B1:F in *SN1;
now per cases by B1,LemSUM01;
suppose F in SN1O;
then (F in NO) or (F in {H}) by A8,XBOOLE_0:def 3;
hence thesis by LemSUM01,A3,TARSKI:def 1;
end;
suppose F in SN1N;
then (F in (NN \ {H})) or (F in ({H2} \ NO)) by A9,XBOOLE_0:def 3;
then (F in NN) or (F in {H2}) by XBOOLE_0:def 5;
hence thesis by LemSUM01,TARSKI:def 1;
end;
suppose F in XSN1X;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(SN1X) &
G ='X' G1);
consider G1 such that C3:G1 in SN1X and
C4:G ='X' G1 by C2;
C6:G1 in NX or G1 in {H} by C3,A10,XBOOLE_0:def 3;
now per cases by C6,TARSKI:def 1;
suppose G1 in NX;
then F in XNX by C1,C4;
hence thesis by LemSUM01;
end;
suppose G1=H;
hence thesis by C1,C4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Alem2:F in *SN2 implies (F in *N) or (F=H1) or (F=H2)
proof
assume B1:F in *SN2;
now per cases by B1,LemSUM01;
suppose F in SN2O;
then (F in NO) or (F in {H}) by A11,XBOOLE_0:def 3;
hence thesis by LemSUM01,A3,TARSKI:def 1;
end;
suppose F in SN2N;
then (F in (NN \ {H})) or (F in ({H1,H2} \ NO)) by A12,XBOOLE_0:def 3;
then (F in NN) or (F in {H1,H2}) by XBOOLE_0:def 5;
hence thesis by LemSUM01,TARSKI:def 2;
end;
suppose F in XSN2X;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(SN2X) &
G ='X' G1);
consider G1 such that C3:G1 in SN2X and
C4:G ='X' G1 by C2;
F in XNX by C1,C4,C3,A13;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
Alem3:F in *N implies (F in *SN1) & (F in *SN2)
proof
assume B1:F in *N;
now per cases by B1,LemSUM01;
suppose F in NO;
then (F in SN1O) & (F in SN2O) by A8,A11,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
suppose C2:F in NN;
now per cases;
suppose F=H;
then F in {H} by TARSKI:def 1;
then (F in SN1O) & (F in SN2O) by A8,A11,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
suppose not (F=H);
then not (F in {H}) by TARSKI:def 1;
then F in (NN \ {H}) by C2,XBOOLE_0:def 5;
then (F in SN1N) & (F in SN2N) by A9,A12,XBOOLE_0:def 3;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
suppose F in XNX;
then consider G such that C1:F=G and
C2:ex G1 st (G1 in CastLTL(NX) &
G ='X' G1);
consider G1 such that C3:G1 in NX and
C4:G ='X' G1 by C2;
C5:G1 in SN1X by C3,A10,XBOOLE_0:def 3;
(F in XSN1X) & (F in XSN2X) by C1,C4,C3,C5,A13;
hence thesis by LemSUM01;
end;
end;
hence thesis;
end;
A17:w |= *N implies
(w |= *SN1 or w |= *SN2)
proof
assume B1:w |= *N;
now per cases by A3,A4,B1,MODELC_2:65,def 66;
suppose B3:(w|=H2 & w|='X' H);
F in *SN1 implies w|= F
proof
assume F in *SN1;
then (F in *N) or (F=H2) or (F='X' H) by Alem1;
hence thesis by B1,B3,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
suppose B4:w|=H1 & w|=H2;
F in *SN2 implies w|= F
proof
assume F in *SN2;
then (F in *N) or (F=H1) or (F=H2) by Alem2;
hence thesis by B1,B4,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
end;
hence thesis;
end;
(w |= *SN1 or w |= *SN2)
implies w |= *N
proof
assume B1:w |= *SN1 or w |= *SN2;
F in *N implies w |= F
proof
assume F in *N;
then C1:(F in *SN1) & (F in *SN2) by Alem3;
now per cases by B1;
suppose w |= *SN1;
hence thesis by C1,MODELC_2:def 66;
end;
suppose w |= *SN2;
hence thesis by C1,MODELC_2:def 66;
end;
end;
hence thesis;
end;
hence thesis by MODELC_2:def 66;
end;
hence thesis by A17;
end;
theorem
(H in the LTLnew of N) &
(H is disjunctive or H is Until or H is Release) implies
(w |= *N iff (w |= *SuccNode1(H,N) or w |= *SuccNode2(H,N)))
by Lem203,Lem204,Lem205;
LemSubformulae01:
(H is negative or H is next) implies
Subformulae H = (Subformulae the_argument_of H) \/ {H}
proof
assume A0:H is negative or H is next;
set H1 = the_argument_of H;
H1 is_immediate_constituent_of H by A0,MODELC_2:20,21;
then H1 is_proper_subformula_of H by MODELC_2:29;
then H1 is_subformula_of H by MODELC_2:def 23;
then A1:Subformulae H1 c= Subformulae H by MODELC_2:46;
H is_subformula_of H by MODELC_2:27;
then H in Subformulae H by MODELC_2:45;
then {H} c= Subformulae H by ZFMISC_1:37;
then A2:Subformulae H1 \/ {H} c= Subformulae H by A1,XBOOLE_1:8;
x in Subformulae H iff x in Subformulae H1 \/ {H}
proof
x in Subformulae H implies x in Subformulae H1 \/ {H}
proof
assume x in Subformulae H;
then consider F such that
B1: F = x and
B2: F is_subformula_of H by MODELC_2:def 24;
now per cases;
suppose F = H;
then F in {H} by TARSKI:def 1;
hence thesis by B1,XBOOLE_0:def 3;
end;
suppose F <> H;
then F is_proper_subformula_of H by B2,MODELC_2:def 23;
then F is_subformula_of H1 by A0,MODELC_2:37;
then F in Subformulae H1 by MODELC_2:45;
hence thesis by B1,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence thesis by A2;
end;
hence thesis by TARSKI:2;
end;
LemSubformulae02:
(H is conjunctive or H is disjunctive or H is Until or H is Release)
implies
Subformulae H = ((Subformulae the_left_argument_of H) \/
(Subformulae the_right_argument_of H) ) \/ {H}
proof
assume A0:H is conjunctive or H is disjunctive or
H is Until or H is Release;
set H1 = the_left_argument_of H;
set H2 = the_right_argument_of H;
set SUBF = (Subformulae the_left_argument_of H) \/
(Subformulae the_right_argument_of H);
H1 is_immediate_constituent_of H by A0,MODELC_2:22,23,24,25;
then H1 is_proper_subformula_of H by MODELC_2:29;
then H1 is_subformula_of H by MODELC_2:def 23;
then A1:Subformulae H1 c= Subformulae H by MODELC_2:46;
H2 is_immediate_constituent_of H by A0,MODELC_2:22,23,24,25;
then H2 is_proper_subformula_of H by MODELC_2:29;
then H2 is_subformula_of H by MODELC_2:def 23;
then Subformulae H2 c= Subformulae H by MODELC_2:46;
then A2: SUBF c= Subformulae H by A1,XBOOLE_1:8;
H is_subformula_of H by MODELC_2:27;
then H in Subformulae H by MODELC_2:def 24;
then {H} c= Subformulae H by ZFMISC_1:37;
then A3:SUBF \/ {H} c= Subformulae H by A2,XBOOLE_1:8;
x in Subformulae H iff x in SUBF \/ {H}
proof
x in Subformulae H implies x in SUBF \/ {H}
proof
assume x in Subformulae H;
then consider F such that
B1: F = x and
B2: F is_subformula_of H by MODELC_2:def 24;
now per cases;
suppose F = H;
then F in {H} by TARSKI:def 1;
hence thesis by B1,XBOOLE_0:def 3;
end;
suppose F <> H;
then F is_proper_subformula_of H by B2,MODELC_2:def 23;
then F is_subformula_of H1 or F is_subformula_of H2
by A0,MODELC_2:38;
then F in Subformulae H1 or F in Subformulae H2 by MODELC_2:45;
then F in SUBF by XBOOLE_0:def 3;
hence thesis by B1,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
LemSubformulae03:
H is atomic implies Subformulae H ={H}
proof
assume H is atomic;
then consider n such that
A01: H = atom.n by MODELC_2:def 11;
A02:len H =1 by A01,FINSEQ_1:57;
A1:x in {H} implies x in Subformulae H
proof
assume x in {H};
then B1:x = H by TARSKI:def 1;
H is_subformula_of H by MODELC_2:27;
hence thesis by B1,MODELC_2:45;
end;
x in Subformulae H implies x in {H}
proof
assume x in Subformulae H;
then consider G such that B1:G = x and
B2:G is_subformula_of H by MODELC_2:def 24;
G = H
proof
now assume G <> H;
then G is_proper_subformula_of H by B2,MODELC_2:def 23;
then len G < 1 by A02,MODELC_2:32;
hence contradiction by MODELC_2:3;
end;
hence thesis;
end;
hence thesis by B1,TARSKI:def 1;
end;
hence thesis by A1,TARSKI:2;
end;
LemSubformulae04:
not {} in W
proof
assume {} in W;
then consider F such that B1: F = {} & F is_subformula_of H
by MODELC_2:def 24;
thus contradiction by B1,CARD_1:47,MODELC_2:3;
end;
theorem Th207:
ex L st Subformulae H = rng L
proof
defpred P[LTL-formula] means ex L st Subformulae $1 = rng L;
A1:for H st H is atomic holds P[H]
proof
let H such that B1:H is atomic;
set L =<* H *>;
take L;
rng L = {H} by LemFinSeq01 .= Subformulae H by B1,LemSubformulae03;
hence thesis;
end;
A2:for H st (H is negative or H is next) & P[the_argument_of H]
holds P[H]
proof
let H such that B1:(H is negative or H is next) and
B2:P[the_argument_of H];
consider L1 such that B3:Subformulae the_argument_of H = rng L1 by B2;
set L = L1 ^ <* H *>;
take L;
rng L = rng L1 \/ rng <* H *> by FINSEQ_1:44
.= Subformulae the_argument_of H \/ {H} by B3,LemFinSeq01
.= Subformulae H by LemSubformulae01,B1;
hence thesis;
end;
A3:for H st (H is conjunctive or H is disjunctive or
H is Until or H is Release ) &
P[the_left_argument_of H] & P[the_right_argument_of H] holds P[H]
proof
let H such that B1:(H is conjunctive or H is disjunctive or
H is Until or H is Release ) and
B2:P[the_left_argument_of H] and
B3:P[the_right_argument_of H];
consider L1 such that
B4:Subformulae the_left_argument_of H = rng L1 by B2;
consider L2 such that
B5:Subformulae the_right_argument_of H = rng L2 by B3;
set L = (L1 ^ L2) ^ <* H *>;
take L;
B6:rng(L1 ^ L2) = Subformulae the_left_argument_of H
\/ Subformulae the_right_argument_of H
by B4,B5,FINSEQ_1:44;
rng L = rng (L1 ^ L2) \/ rng <* H *> by FINSEQ_1:44
.= (Subformulae the_left_argument_of H
\/ Subformulae the_right_argument_of H) \/ {H}
by B6,LemFinSeq01
.= Subformulae H by LemSubformulae02,B1;
hence thesis;
end;
for H holds P[H] from MODELC_2:sch 1(A1,A2,A3);
hence thesis;
end;
registration let H;
cluster Subformulae H -> finite;
correctness
proof
consider L such that A1:Subformulae H = rng L by Th207;
thus thesis by A1;
end;
end;
definition let H, W, L, x;
func Length_fun(L,W,x) -> Nat equals
:DefPartialfun:
len CastLTL(L.x) if L.x in W
otherwise 0;
correctness;
end;
definition let H, W, L;
func Partial_seq(L,W) -> Real_Sequence means
:DefPartialseq:
for k holds (L.k in W implies it.k = len CastLTL(L.k)) &
(not (L.k in W) implies it.k=0 );
existence
proof
deffunc F(set) = Length_fun(L,W,$1);
A1:for x st x in NAT holds F(x) in REAL
proof
let x such that x in NAT;
F(x) in NAT by ORDINAL1:def 13;
hence thesis;
end;
consider IT being Function of NAT,REAL such that
A2: for x st x in NAT holds IT.x = F(x)
from FUNCT_2:sch 2 (A1);
take IT;
for k holds (L.k in W implies IT.k = len CastLTL(L.k)) &
(not (L.k in W ) implies IT.k=0 )
proof
let k;
B0:k in NAT by ORDINAL1:def 13;
B1: L.k in W implies IT.k = len CastLTL(L.k)
proof
assume C1:L.k in W;
IT.k = Length_fun(L,W,k) by A2,B0;
hence thesis by C1,DefPartialfun;
end;
not (L.k in W) implies IT.k=0
proof
assume C1:not (L.k in W);
IT.k = Length_fun(L,W,k) by A2,B0;
hence thesis by C1,DefPartialfun;
end;
hence thesis by B1;
end;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Real_Sequence;
(for k holds (L.k in W implies R1.k = len CastLTL(L.k)) &
(not (L.k in W ) implies R1.k=0 ) ) &
(for k holds (L.k in W implies R2.k = len CastLTL(L.k)) &
(not (L.k in W ) implies R2.k=0 ) ) implies R1 = R2
proof
assume that
B1:(for k holds (L.k in W implies R1.k = len CastLTL(L.k)) &
(not (L.k in W ) implies R1.k=0 ) ) and
B2:(for k holds (L.k in W implies R2.k = len CastLTL(L.k)) &
(not (L.k in W ) implies R2.k=0 ) );
for x st x in NAT holds R1.x = R2.x
proof
let x such that A1: x in NAT;
reconsider x as Nat by A1;
now per cases;
suppose C1:L.x in W;
then R1.x = len CastLTL(L.x) by B1;
hence thesis by C1,B2;
end;
suppose C2:not (L.x in W);
then R1.x=0 by B1;
hence thesis by C2,B2;
end;
end;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
hence thesis;
end;
end;
reserve R,R1,R2 for Real_Sequence;
definition let H, W, L;
func len(L,W) -> Real equals
Sum(Partial_seq(L,W), len L);
correctness;
end;
lemlen02:
(for i st i<=n holds R1.i = R2.i) implies Sum(R1, n) = Sum(R2, n)
proof
A0:CastNat(n)=n by MODELC_2:def 1;
defpred P[Nat] means
(for i st i<=$1 holds R1.i = R2.i) implies
Sum(R1, CastNat($1)) = Sum(R2, CastNat($1));
A1:P[0]
proof
assume B1:for i st i<=0 holds R1.i = R2.i;
Sum(R1,CastNat(0))
= Sum(R1,0) by MODELC_2:def 1
.= R1.0 by SERIES_1:def 1
.= R2.0 by B1
.= Sum(R2,0) by SERIES_1:def 1;
hence thesis by MODELC_2:def 1;
end;
A2:for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that B1:P[k];
P[k+1]
proof
assume C1:for i st i<=k+1 holds R1.i = R2.i;
set m=k+1;
C2:CastNat(k)=k by MODELC_2:def 1;
C4:for i st i<=k holds R1.i = R2.i
proof
let i such that D1: i<= k;
k<=k+1 by NAT_1:11;
hence thesis by D1,C1,XXREAL_0:2;
end;
C5:R1.m = R2.m by C1;
reconsider k as Element of NAT by ORDINAL1:def 13;
Sum(R1, CastNat(m))
= Sum(R1, m) by MODELC_2:def 1
.= Sum(R2, k) + R2.m
by C4,B1,C2,C5,SERIES_1:def 1
.= Sum(R2, m) by SERIES_1:def 1;
hence thesis by MODELC_2:def 1;
end;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A1,A2);
hence thesis by A0;
end;
lemlen03:
(for i st ( i<=n) & not (i=j) holds R1.i = R2.i) & (j<=n)
implies Sum(R1, n) - R1.j = Sum(R2, n) - R2.j
proof
A0:CastNat(n)=n by MODELC_2:def 1;
defpred P[Nat] means
(for i st i<=$1 & not (i=j) holds R1.i = R2.i)
& (j<=$1)
implies
Sum(R1, CastNat($1)) - R1.j= Sum(R2, CastNat($1))- R2.j;
A1:P[0]
proof
assume that
for i st i<=0 & not (i=j) holds R1.i = R2.i and
B2: j<=0;
B3:j=0 by B2;
b6: Sum(R1,CastNat(0)) = Sum(R1,0) by MODELC_2:def 1
.= R1.0 by SERIES_1:def 1;
Sum(R2,CastNat(0)) = Sum(R2,0) by MODELC_2:def 1
.= R2.0 by SERIES_1:def 1;
hence thesis by b6,B3;
end;
A2:for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that B1:P[k];
P[k+1]
proof
assume that
C1:for i st i<=k+1 & not (i = j) holds R1.i = R2.i and
C2:j <= k+1;
set m=k+1;
C4:CastNat(k)=k by MODELC_2:def 1;
reconsider k as Element of NAT by ORDINAL1:def 13;
now per cases by C2,NAT_1:8;
suppose C7:j <= k;
D3:j < m by C7,NAT_1:13;
Sum(R1, CastNat(m)) - R1.j
= Sum(R1, m) - R1.j by MODELC_2:def 1
.= (Sum(R1, k) + R1.m) - R1.j by SERIES_1:def 1
.= (Sum(R1, k)- R1.j) + R1.m
.= (Sum(R2, k)- R2.j) + R2.m
by C7,C1,B1,C4,D3,NAT_1:12
.= (Sum(R2, k) + R2.m) - R2.j
.= Sum(R2, m) - R2.j by SERIES_1:def 1;
hence thesis by MODELC_2:def 1;
end;
suppose D1:j = k+1;
D2:for i st i<=k holds R1.i = R2.i
proof
let i such that E1: i<=k;
i < j by D1,E1,NAT_1:13;
hence thesis by C1,E1,NAT_1:12;
end;
Sum(R1, CastNat(m)) - R1.j
= Sum(R1, m) - R1.j by MODELC_2:def 1
.= (Sum(R1, k) + R1.m) - R1.j by SERIES_1:def 1
.= (Sum(R2, k) + R2.m) - R2.j by D1,D2,lemlen02
.= Sum(R2, m) - R2.j by SERIES_1:def 1;
hence thesis by MODELC_2:def 1;
end;
end;
hence thesis;
end;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A1,A2);
hence thesis by A0;
end;
theorem Thlen00:
len(L,{}H) = 0
proof
set s = Partial_seq(L,{}H);
A2:for n being Element of NAT holds s.n = 0*n+0 by DefPartialseq;
for n holds Partial_Sums(s).n = 0
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 13;
B1:s.0 = 0 by DefPartialseq;
Partial_Sums(s).n = (n+1)*(s.0 + s.n)/2 by A2,SERIES_2:42
.= (n+1)*(0+0)/2 by B1,DefPartialseq;
hence thesis;
end;
hence thesis;
end;
theorem Thlen01:
not F in W implies len(L,W \ {F}) = len(L,W)
proof
assume A1:not (F in W);
A2: x in W \ {F} implies x in W by XBOOLE_0:def 5;
x in W implies x in W \ {F}
proof
assume B1:x in W;
not x in {F} by A1,B1,TARSKI:def 1;
hence thesis by B1,XBOOLE_0:def 5;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Thlen02:
(rng L = Subformulae H & L is one-to-one) & F in W implies
len(L,W\{F}) = len(L,W) - len F
proof
assume that A1:(rng L = Subformulae H & L is one-to-one) and
A2:F in W;
set n = len L;
consider x such that A3: x in dom L and
A4: L.x = F by A1,A2,FUNCT_1:def 5;
x in Seg n by A3,FINSEQ_1:def 3;
then x in { k where k is Element of NAT:
1 <= k & k <= n } by FINSEQ_1:def 1;
then consider k being Element of NAT such that
A5:x=k & 1<=k & k <= n;
reconsider k as Nat;
L.k in {F} by A4,A5,TARSKI:def 1;
then A7:not (L.k in W\{F}) by XBOOLE_0:def 5;
set R1 = Partial_seq(L,W);
set R2= Partial_seq(L,W\{F});
A801:F in LTL_WFF by MODELC_2:1;
A8:R1.k = len CastLTL(L.k) by A4,A5,A2,DefPartialseq
.= len F by A801,A4,A5,MODELC_2:def 25;
A9:R2.k= 0 by A7,DefPartialseq;
for i st (i<=n) & not (i=k) holds R1.i = R2.i
proof
let i such that B1:(i<=n) & not (i=k);
now per cases;
suppose not (i in dom L);
then B401:L.i = {} by FUNCT_1:def 4;
then B4:not (L.i in W) by LemSubformulae04;
not (L.i in W\{F}) by B401,LemSubformulae04;
then R2.i = 0 by DefPartialseq
.= R1.i by B4,DefPartialseq;
hence thesis;
end;
suppose i in dom L;
then not (L.i = F) by A1,A3,A4,A5,B1,FUNCT_1:def 8;
then B6:not (L.i in {F}) by TARSKI:def 1;
now per cases;
suppose C1:L.i in W;
then L.i in W\{F} by B6,XBOOLE_0:def 5;
then R2.i = len CastLTL(L.i) by DefPartialseq
.= R1.i by C1,DefPartialseq;
hence thesis;
end;
suppose C2:not (L.i in W);
then not (L.i in W\{F}) by XBOOLE_0:def 5;
then R2.i = 0 by DefPartialseq
.= R1.i by C2,DefPartialseq;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then Sum(R1, n) - R1.k = Sum(R2, n) - R2.k by A5,lemlen03;
hence thesis by A8,A9;
end;
theorem Thlen03:
(rng L = Subformulae H & L is one-to-one) & (not F in W) & W1 = W \/ {F}
implies len(L,W1) = len(L,W) + len F
proof
assume that A1:(rng L = Subformulae H & L is one-to-one) and
A2:not F in W and
A3:W1 = W \/ {F};
F in {F} by TARSKI:def 1;
then A4:F in W1 by A3,XBOOLE_0:def 3;
W1\{F} = W
proof
B1: x in W1\{F} implies x in W
proof
assume x in W1\{F};
then x in W1 & not x in {F} by XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 3;
end;
x in W implies x in W1\{F}
proof
assume C1:x in W;
then C2:not (x in {F}) by A2,TARSKI:def 1;
x in W1 by C1,A3,XBOOLE_0:def 3;
hence thesis by C2,XBOOLE_0:def 5;
end;
hence thesis by B1,TARSKI:2;
end;
then len(L,W) = len(L,W1) - len F by Thlen02,A1,A4;
hence thesis;
end;
theorem Thlen04:
(rng L1 = Subformulae H & L1 is one-to-one) &
(rng L2 = Subformulae H & L2 is one-to-one) implies
len(L1,W) = len(L2,W)
proof
defpred P[Nat] means
for W1 st card W1 <=$1 holds
(rng L1 = Subformulae H & L1 is one-to-one) &
(rng L2 = Subformulae H & L2 is one-to-one)
implies
len(L1,W1) = len(L2,W1);
A1:P[0]
proof
let W1 such that B1:card W1 <=0;
B2:W1 = {} H by B1;
then len(L1,W1) = 0 by Thlen00;
hence thesis by B2,Thlen00;
end;
A2:for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that B0:P[k];
P[k+1]
proof
let W1 such that B1: card W1 <=k+1;
(rng L1 = Subformulae H & L1 is one-to-one) &
(rng L2 = Subformulae H & L2 is one-to-one)
implies len(L1,W1) = len(L2,W1)
proof
assume that
C1:(rng L1 = Subformulae H & L1 is one-to-one) &
(rng L2 = Subformulae H & L2 is one-to-one);
now per cases by B1,NAT_1:8;
suppose card W1 <=k;
hence thesis by B0,C1;
end;
suppose E1:card W1 = k+1; then
W1 <> {};
then consider F being set
such that E2:F in W1 by XBOOLE_0:def 1;
F in Subformulae H by E2;
then reconsider F as LTL-formula by MODELC_2:1;
{F} c= W1 by E2,ZFMISC_1:37;
then E3:card (W1 \ {F}) = card W1 - card {F} by CARD_2:63
.= card W1 - 1 by CARD_1:50
.= k by E1;
E4:len(L1,W1) = (len(L1,W1) - len F) + len F
.= len(L1,W1\{F}) + len F by C1,E2,Thlen02;
len(L2,W1) = (len(L2,W1) - len F) + len F
.= len(L2,W1\{F}) + len F by C1,E2,Thlen02
.= len(L1,W1\{F}) + len F by E3,B0,C1;
hence thesis by E4;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A3:for k being Nat holds P[k] from NAT_1:sch 2 (A1,A2);
set k = card W;
P[k] by A3;
hence thesis;
end;
definition let H, W;
func len(W) -> Real means
:Deflen02:
ex L st rng L = Subformulae H & L is one-to-one & it = len(L,W);
existence
proof
consider L such that A1: rng L = Subformulae H & L is one-to-one
by FINSEQ_4:73;
set IT = len(L,W);
take IT;
thus thesis by A1;
end;
uniqueness by Thlen04;
end;
theorem
not (F in W) implies len(W\{F}) = len(W)
proof
assume A1:not F in W;
consider L such that A2: rng L = Subformulae H & L is one-to-one
by FINSEQ_4:73;
len(W\{F}) = len(L,W\{F}) by Deflen02,A2
.= len(L,W) by Thlen01,A1;
hence thesis by Deflen02,A2;
end;
theorem Thlen07:
F in W implies len(W\{F}) = len(W) - len F
proof
assume A1:F in W;
consider L such that A2: rng L = Subformulae H & L is one-to-one
by FINSEQ_4:73;
len(W\{F}) = len(L,W\{F}) by Deflen02,A2
.= len(L,W) - len F by Thlen02,A1,A2;
hence thesis by Deflen02,A2;
end;
theorem Thlen08:
(not F in W) & (W1 = W \/ {F}) implies
len(W1) = len(W) + len F
proof
assume A1:(not F in W) & (W1 = W \/ {F});
consider L such that A2: rng L = Subformulae H & L is one-to-one
by FINSEQ_4:73;
len(W1) = len(L,W1) by Deflen02,A2
.= len(L,W) + len F by Thlen03,A1,A2;
hence thesis by Deflen02,A2;
end;
theorem Thlen09:
W1 = W \/ {F} implies len(W1) <= len(W) + len F
proof
assume A1:W1 = W \/ {F};
now per cases;
suppose F in W;
then {F} c= W by ZFMISC_1:37;
then W1 = W by A1,XBOOLE_1:12;
hence thesis by XREAL_1:33;
end;
suppose not F in W;
hence thesis by Thlen08,A1;
end;
end;
hence thesis;
end;
theorem Thlen10:
len({}H ) = 0
proof
consider L such that A1: rng L = Subformulae H & L is one-to-one
by FINSEQ_4:73;
len({}H) = len(L,{}H) by Deflen02,A1;
hence thesis by Thlen00;
end;
theorem Thlen11:
W = {F} implies len(W) = len F
proof
assume A1:W = {F};
then A2:F in W by TARSKI:def 1;
A3: W\{F}={}H
proof
now assume ex x st x in W\{F};
then consider x such that B1:x in W\{F};
(x in W) & not (x in {F}) by B1,XBOOLE_0:def 5;
hence contradiction by A1;
end;
hence thesis by XBOOLE_0:def 1;
end;
len(W) = (len(W) - len F) + len F
.= len(W\{F}) + len F by A2,Thlen07
.= 0 + len F by Thlen10,A3;
hence thesis;
end;
lemlen05:W c= W1 implies
W = W1 or ex x st x in W1 & W c= W1\{x}
proof
assume A1:W c= W1;
not (W = W1) implies (ex x st x in W1 & W c= W1\{x})
proof
assume not (W = W1);
then consider x such that
B1: not (x in W implies x in W1) or
not (x in W1 implies x in W) by TARSKI:2;
take x;
W \ {x} = W
proof
C1:y in W \ {x} implies y in W by XBOOLE_0:def 5;
y in W implies y in W \ {x}
proof
assume y in W;
then y in W & not (y in {x}) by A1,B1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by C1,TARSKI:2;
end;
hence thesis by A1,B1,XBOOLE_1:33;
end;
hence thesis;
end;
theorem Thlen12:
W c= W1 implies len(W) <= len(W1)
proof
defpred P[Nat] means
for W1 st card W1 <=$1 holds
W c= W1 implies len(W) <= len(W1);
A1:P[0]
proof
let W1 such that B1: card W1 <=0;
W1 = {} H by B1;
hence thesis;
end;
A2:for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that B1: P[k];
P[k+1]
proof
let W1 such that B2: card W1 <=k+1;
W c= W1 implies len(W) <= len(W1)
proof
assume C1:W c= W1;
now per cases by C1,lemlen05;
suppose W = W1;
hence thesis;
end;
suppose ex x st x in W1 & W c= W1\{x};
then consider x such that D1: x in W1 & W c= W1\{x};
x in Subformulae H by D1;
then reconsider x as LTL-formula by MODELC_2:1;
set X = {x};
X c= W1 by D1,ZFMISC_1:37;
then card (W1\X) = card W1 - card X by CARD_2:63
.= card W1 - 1 by CARD_1:50;
then card (W1\X) +1 <= k+1 by B2;
then card (W1\X) <= k by XREAL_1:8;
then len(W) <= len(W1\X) by B1,D1;
then D3:len(W) <= len(W1) - len x by D1,Thlen07;
len(W1) - len x <= len(W1) by XREAL_1:45;
hence thesis by D3,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A3:for k being Nat holds P[k] from NAT_1:sch 2 (A1,A2);
set k = card W1;
P[k] by A3;
hence thesis;
end;
theorem Thlen1201:
len(W)<1 implies W = {}H
proof
assume A1:len(W)<1;
now assume W <> {}H;
then consider x such that B1:x in W by XBOOLE_0:def 1;
x in Subformulae H by B1;
then reconsider x as LTL-formula by MODELC_2:1;
set X = {x};
B2:X c= W by B1,ZFMISC_1:37;
x is_subformula_of H by B1,MODELC_2:45;
then reconsider X as Subset of Subformulae H by Lem104;
len(X) = len x by Thlen11;
then B3:len(X) >=1 by MODELC_2:3;
len(X) <= len(W) by B2,Thlen12;
hence contradiction by B3,A1,XXREAL_0:2;
end;
hence thesis;
end;
theorem Thlen1203:
len(W) >= 0
proof
now per cases;
suppose W = {}H;
hence thesis by Thlen10;
end;
suppose W <> {}H;
hence thesis by Thlen1201;
end;
end;
hence thesis;
end;
theorem Thlen13:
W = W1 \/ W2 implies len(W) <= len(W1) + len(W2)
proof
defpred P[Nat] means
for W,W1,W2 st card W1 <=$1 holds
(W = W1 \/ W2 implies len(W) <= len(W1) + len(W2));
A1:P[0]
proof
let W,W1,W2 such that B1: card W1 <=0;
B2:W1 = {} H by B1;
then len(W1) = 0 by Thlen10;
hence thesis by B2;
end;
A2:for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that B1: P[k];
P[k+1]
proof
let W,W1,W2 such that B2: card W1 <=k+1;
W = W1 \/ W2 implies len(W) <= len(W1) + len(W2)
proof
assume C1: W = W1 \/ W2;
now per cases by B2,NAT_1:8;
suppose card W1 <=k;
hence thesis by B1,C1;
end;
suppose card W1 = k+1; then
W1 <> {};
then consider x such that D1: x in W1 by XBOOLE_0:def 1;
x in Subformulae H by D1;
then reconsider x as LTL-formula by MODELC_2:1;
set X = {x};
set Y = W1\X;
set Z = Y \/ W2;
D4:X c= W1 by D1,ZFMISC_1:37;
then card (Y) = card W1 - card X by CARD_2:63
.= card W1 - 1 by CARD_1:50;
then card (Y) + 1 = card W1;
then card (Y) <= k by B2,XREAL_1:8;
then Z = Y \/ W2 implies
len(Z) <= len(Y) + len(W2) by B1;
then len(Z) <= len(W1) - len x + len(W2) by D1,Thlen07;
then len(Z) <= (len(W1) + len(W2)) - len x;
then D5:len(Z) + len x <= len(W1) + len(W2) by XREAL_1:21;
Z \/ X = (Y \/ X) \/ W2 by XBOOLE_1:4
.= W1 \/ W2 by D4,XBOOLE_1:45;
then len(W) <= len(Z) + len x by C1,Thlen09;
hence thesis by D5,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A3:for k being Nat holds P[k] from NAT_1:sch 2 (A1,A2);
set k = card W1;
P[k] by A3;
hence thesis;
end;
definition let v, H;
assume A1:H in Subformulae v;
func LTLNew1(H,v) -> Subset of Subformulae v equals
:defLTLNew101: LTLNew1 H;
correctness
proof
consider F such that A3:H=F and A4: F is_subformula_of v
by A1,MODELC_2:def 24;
Subformulae H c= Subformulae v by A3,A4,MODELC_2:46;
hence thesis by XBOOLE_1:1;
end;
func LTLNew2(H,v) -> Subset of Subformulae v equals
:defLTLNew201: LTLNew2 H;
correctness
proof
consider F such that A3:H=F and A4: F is_subformula_of v
by A1,MODELC_2:def 24;
Subformulae H c= Subformulae v by A3,A4,MODELC_2:46;
hence thesis by XBOOLE_1:1;
end;
end;
lemlen05:
H in Subformulae v implies len(LTLNew1(H,v)) <= len(H) -1
proof
assume A1:H in Subformulae v;
set New = LTLNew1(H,v);
A01:New = LTLNew1 H by A1,defLTLNew101;
set Left = {the_left_argument_of H};
set Right = {the_right_argument_of H};
consider F such that A2:H=F and A3: F is_subformula_of v
by A1,MODELC_2:def 24;
A4:Subformulae H c= Subformulae v by A2,A3,MODELC_2:46;
now per cases;
suppose A5:H is conjunctive;
Left is Subset of Subformulae H by A5,Lem108;
then reconsider Left as Subset of Subformulae v by A4,XBOOLE_1:1;
Right is Subset of Subformulae H by A5,Lem108;
then reconsider Right as Subset of Subformulae v by A4,XBOOLE_1:1;
B1:len(Left) = len(the_left_argument_of H) by Thlen11;
B2:len(Right) = len(the_right_argument_of H) by Thlen11;
B3:len(H) = 1+len(the_left_argument_of H) +
len(the_right_argument_of H) by A5,MODELC_2:11;
New = {the_left_argument_of H,the_right_argument_of H }
by A01,A5,Def203;
then New = Left \/ Right by ENUMSET1:41;
then len(New) <= len(Left) + len(Right) by Thlen13;
hence thesis by B1,B2,B3;
end;
suppose A6:H is disjunctive or H is Until;
B2:len(H) = 1+len(the_left_argument_of H) +
len(the_right_argument_of H) by A6,MODELC_2:11;
New = Left by A01,A6,Def203;
then len(New) = len(the_left_argument_of H) by Thlen11;
then len(New) +0 <= len(the_left_argument_of H) +
len(the_right_argument_of H) by XREAL_1:9;
hence thesis by B2;
end;
suppose A7:H is next;
1<=len(H) by MODELC_2:3;
then B1:1-1 <= len(H)-1 by XREAL_1:11;
New = {} v by A01,A7,Def203;
hence thesis by B1,Thlen10;
end;
suppose A8:H is Release;
B2:len(H) = 1+len(the_left_argument_of H) +
len(the_right_argument_of H) by A8,MODELC_2:11;
New = Right by A01,A8,Def203;
then len(New) = len(the_right_argument_of H) by Thlen11;
then len(New)+0 <= len(the_left_argument_of H) +
len(the_right_argument_of H) by XREAL_1:9;
hence thesis by B2;
end;
suppose A9:not (H is conjunctive or H is disjunctive or H is next or
H is Until or H is Release);
1<=len(H) by MODELC_2:3;
then B1:1-1 <= len(H)-1 by XREAL_1:11;
New = {} v by A01,A9,Def203;
hence thesis by Thlen10,B1;
end;
end;
hence thesis;
end;
lemlen06:
H in Subformulae v implies len(LTLNew2(H,v)) <= len(H) -1
proof
assume A1:H in Subformulae v;
set New = LTLNew2(H,v);
A01:New = LTLNew2 H by A1,defLTLNew201;
set Left = {the_left_argument_of H};
set Right = {the_right_argument_of H};
consider F such that A2:H=F and A3: F is_subformula_of v
by A1,MODELC_2:def 24;
A4:Subformulae H c= Subformulae v by A2,A3,MODELC_2:46;
now per cases;
suppose A5:H is Release;
Left is Subset of Subformulae H by A5,Lem108;
then reconsider Left as Subset of Subformulae v by A4,XBOOLE_1:1;
Right is Subset of Subformulae H by A5,Lem108;
then reconsider Right as Subset of Subformulae v by A4,XBOOLE_1:1;
B1:len(Left) = len(the_left_argument_of H) by Thlen11;
B2:len(Right) = len(the_right_argument_of H) by Thlen11;
B3:len(H) = 1+len(the_left_argument_of H) +
len(the_right_argument_of H) by A5,MODELC_2:11;
New = {the_left_argument_of H,the_right_argument_of H }
by A01,A5,Def204;
then New = Left \/ Right by ENUMSET1:41;
then len(New) <= len(Left) + len(Right) by Thlen13;
hence thesis by B1,B2,B3;
end;
suppose A6: H is disjunctive or H is Until;
B2:len(H) = 1+len(the_left_argument_of H) +
len(the_right_argument_of H) by A6,MODELC_2:11;
New = Right by A01,A6,Def204;
then len(New) = len(the_right_argument_of H) by Thlen11;
then len(New)+0 <= len(the_left_argument_of H) +
len(the_right_argument_of H) by XREAL_1:9;
hence thesis by B2;
end;
suppose A7:H is conjunctive or H is next;
1<=len(H) by MODELC_2:3;
then B1:1-1 <= len(H)-1 by XREAL_1:11;
New = {} v by A01,A7,Def204;
hence thesis by B1,Thlen10;
end;
suppose A8:not (H is conjunctive or H is disjunctive or H is next or
H is Until or H is Release);
1<=len(H) by MODELC_2:3;
then B1:1-1 <= len(H)-1 by XREAL_1:11;
New = {} v by A01,A8,Def204;
hence thesis by B1,Thlen10;
end;
end;
hence thesis;
end;
theorem Thlen15:
N2 is_succ1_of N1 implies
len(the LTLnew of N2) <= len(the LTLnew of N1) - 1
proof
set NN1 = the LTLnew of N1;
set NN2 = the LTLnew of N2;
assume N2 is_succ1_of N1;
then consider H such that A1:H in NN1 and
A2:N2 = SuccNode1(H,N1) by Def208;
set New1= LTLNew1(H,v);
set M1 = NN1 \ {H};
set M2 = New1 \ the LTLold of N1;
reconsider NN1 as Subset of Subformulae v;
reconsider M1 as Subset of Subformulae v;
reconsider M2 as Subset of Subformulae v;
New1 = LTLNew1 H by A1,defLTLNew101;
then A3:NN2 = M1 \/ M2 by A1,A2,Def206;
A4:len(M1) = len(NN1)-len(H) by A1,Thlen07;
A5:len(New1) <= len(H) -1 by A1,lemlen05;
len(M2) <= len(New1) by Thlen12,XBOOLE_1:36;
then len(M2) <= len(H) -1 by A5,XXREAL_0:2;
then A6:len(M1) + len(M2) <= len(M1) + (len(H) -1) by XREAL_1:8;
len(NN2)<=len(M1) + len(M2) by A3,Thlen13;
hence thesis by A6,A4,XXREAL_0:2;
end;
theorem Thlen16:
N2 is_succ2_of N1 implies
len(the LTLnew of N2) <= len(the LTLnew of N1) - 1
proof
set NN1 = the LTLnew of N1;
set NN2 = the LTLnew of N2;
assume N2 is_succ2_of N1;
then consider H such that
A1:H in NN1 and
A101:(H is disjunctive or H is Until or H is Release) and
A2:N2 = SuccNode2(H,N1) by Def209;
set New2= LTLNew2(H,v);
set M1 = NN1 \ {H};
set M2 = New2 \ the LTLold of N1;
reconsider NN1 as Subset of Subformulae v;
reconsider M1 as Subset of Subformulae v;
reconsider M2 as Subset of Subformulae v;
New2 = LTLNew2 H by A1,defLTLNew201;
then A3:NN2 = M1 \/ M2 by A1,A101,A2,Def207;
A4:len(M1) = len(NN1)-len(H) by A1,Thlen07;
A5:len(New2) <= len(H) -1 by A1,lemlen06;
len(M2) <= len(New2) by Thlen12,XBOOLE_1:36;
then len(M2) <= len(H) -1 by A5,XXREAL_0:2;
then A6:len(M1) + len(M2) <= len(M1) + (len(H) -1) by XREAL_1:8;
len(NN2)<=len(M1) + len(M2) by A3,Thlen13;
hence thesis by A6,A4,XXREAL_0:2;
end;
definition let v, N;
func len(N) -> Nat equals
[\ len(the LTLnew of N) /];
correctness
proof
len(the LTLnew of N) >= 0 by Thlen1203;
hence thesis by INT_1:80;
end;
end;
theorem Thlen17:
N2 is_succ_of N1 implies len(N2) <= len(N1) - 1
proof
set r1 = len(the LTLnew of N1);
set r2 = len(the LTLnew of N2);
assume N2 is_succ_of N1;
then N2 is_succ1_of N1 or N2 is_succ2_of N1 by Def210;
then r2 <= r1-1 by Thlen15,Thlen16;
hence thesis by LemReal02;
end;
theorem Thlen18:
len(N)<=0 implies the LTLnew of N = {}v
proof
A1: len(the LTLnew of N) -1 < [\ len(the LTLnew of N) /] by INT_1:def 4;
assume len(N)<=0;
then len(the LTLnew of N) -1 +1 <0+1 by A1,XREAL_1:10;
hence thesis by Thlen1201;
end;
theorem Thlen19:
len(N)>0 implies the LTLnew of N <> {}v
proof
assume A1:len(N) >0;
now assume the LTLnew of N = {}v;
then len (the LTLnew of N) = 0 by Thlen10;
hence contradiction by A1,INT_1:47;
end;
hence thesis;
end;
theorem
ex n,L,M st 1 <= n & len L = n & L.1 = N & L.n = M &
the LTLnew of M = {}v &
L is_Finseq_for v
proof
defpred P[Nat] means
for N holds
len(N)<=$1 implies
ex n,L,M st 1 <= n & len L = n & L.1 = N & L.n = M &
the LTLnew of M = {}v &
L is_Finseq_for v;
A1:P[0]
proof
let N;
len(N)<=0 implies
ex n,L,M st 1 <= n & len L = n & L.1 = N & L.n = M &
the LTLnew of M = {}v &
L is_Finseq_for v
proof
assume B1:len(N)<=0;
set M = N;
set n = 1;
set L = <*M*>;
B3:for k st 1 <= k & k < len L holds
ex N1,N2 st L.k = N1 & L.(k + 1) = N2 &
N2 is_succ_of N1 by FINSEQ_1:56;
take n;
take L;
take M;
thus thesis by B1,Thlen18,B3,DefFinseq,FINSEQ_1:57;
end;
hence thesis;
end;
A2:for l being Nat st P[l] holds P[l + 1]
proof
let l be Nat such that B1: P[l];
P[l+1]
proof
let N;
len(N)<=l+1 implies
ex n,L,M st 1 <= n & len L = n & L.1 = N & L.n = M &
the LTLnew of M = {}v &
L is_Finseq_for v
proof
assume C0:len(N)<=l+1;
ex n,L,M st 1 <= n & len L = n & L.1 = N & L.n = M &
the LTLnew of M = {}v &
L is_Finseq_for v
proof
set NewN=the LTLnew of N;
now per cases by C0,NAT_1:8;
suppose len(N)<=l;
hence thesis by B1;
end;
suppose C2:len(N)=l+1;
then NewN <> {}v by Thlen19;
then consider x such that D1:x in NewN by XBOOLE_0:def 1;
x in Subformulae v by D1;
then reconsider x as LTL-formula by MODELC_2:1;
set M1 = SuccNode1(x,N);
M1 is_succ1_of N by D1,Def208;
then D2:M1 is_succ_of N by Def210;
then len(M1)<=len(N)-1 by Thlen17;
then consider n,L,M such that
D3: 1 <= n & len L = n & L.1 = M1 & L.n = M &
the LTLnew of M = {}v &
L is_Finseq_for v by C2,B1;
set n1=n+1;
D301:1^L;
D5:len L1 = len <*N*> + len L by FINSEQ_1:35
.= n1 by D3,FINSEQ_1:56;
D6:L1.1= N by FINSEQ_1:58;
len <*N*> =1 by FINSEQ_1:56;
then D7:L1.n1 = L.(n1 - 1) by D301,D5,FINSEQ_1:37
.= M by D3;
L1 is_Finseq_for v
proof
let k such that E1:1 <= k and E2: k < len(L1);
E3:k+1<=len(L1) by E2,NAT_1:13;
ex N1,N2 st L1.k = N1 & L1.(k + 1) = N2 &
N2 is_succ_of N1
proof
set N1 = L1.k;
set N2 = L1.(k+1);
now per cases;
suppose k<=1;
then E101:k=1 by E1,XXREAL_0:1;
reconsider N1 as strict LTLnode over v
by E101,FINSEQ_1:58;
E104:len <*N*> =1 by FINSEQ_1:56;
E105:N2 = L.(2-1) by E104,E101,E3,FINSEQ_1:37
.= M1 by D3;
then reconsider N2 as strict LTLnode over v;
take N1,N2;
thus thesis by E101,E105,D2,FINSEQ_1:58;
end;
suppose E200:1< k;
then E201:len <*N*> < k by FINSEQ_1:56;
k<=k+1 by NAT_1:11;
then E202:len <*N*> ) by E2,E201,FINSEQ_1:37
.= L.km1 by FINSEQ_1:56;
E206:N2= L.(k+1 - len <*N*>) by E3,E202,FINSEQ_1:37
.= L.(k+1 -1) by FINSEQ_1:56
.= L.(km1+1);
consider N10,N20 such that
E207: L.km1 = N10 & L.(km1 + 1) = N20 &
N20 is_succ_of N10 by E203,E204,D3,DefFinseq;
reconsider N1 as strict LTLnode over v by E205,E207;
reconsider N2 as strict LTLnode over v by E206,E207;
take N1,N2;
thus thesis by E205,E206,E207;
end;
end;::**case
hence thesis;
end;
hence thesis;
end;::**for
hence thesis by D5,D6,D7,D3,NAT_1:11;
end;::**suppose C2:len(N)=l+1;
end;::**case
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;::**for
A3:for k being Nat holds P[k] from NAT_1:sch 2 (A1,A2);
set k = len(N);
reconsider k as Nat;
P[k] by A3;
hence thesis;
end;
theorem ThSucc01:
N2 is_succ_of N1 implies
the LTLold of N1 c= the LTLold of N2 &
the LTLnext of N1 c= the LTLnext of N2
proof
assume A1:N2 is_succ_of N1;
now per cases by A1,Def210;
suppose N2 is_succ1_of N1;
then consider H such that
B1:H in the LTLnew of N1 and
B2:N2 = SuccNode1(H,N1) by Def208;
the LTLold of N2 =(the LTLold of N1) \/ {H} &
the LTLnext of N2 = (the LTLnext of N1) \/ LTLNext H
by B1,B2,Def206;
hence thesis by XBOOLE_1:7;
end;
suppose N2 is_succ2_of N1;
then consider H such that
B1:H in the LTLnew of N1 and
B2:(H is disjunctive or H is Until or H is Release) and
B3:N2 = SuccNode2(H,N1) by Def209;
the LTLold of N2 =(the LTLold of N1) \/ {H} &
the LTLnext of N2 = the LTLnext of N1
by B1,B2,B3,Def207;
hence thesis by XBOOLE_1:7;
end;
end;
hence thesis;
end;
theorem ThSucc02:
L is_Finseq_for v & m<= len(L) & L1 = L|Seg m
implies L1 is_Finseq_for v
proof
assume that A1:L is_Finseq_for v and
A2:m<= len(L) and
A3:L1 = L|Seg m;
reconsider L1 as FinSequence;
A4:len(L1) = m & dom L1 = Seg m by A2,A3,FINSEQ_1:21;
for k st 1 <= k & k < len(L1) holds
ex N1,N2 st N1 = L1.k & N2=L1.(k+1) & N2 is_succ_of N1
proof
let k such that B1:1 <= k & k < len(L1);
k < len(L) by B1,A4,A2,XXREAL_0:2;
then consider N1,N2 such that
B3: N1 = L.k & N2=L.(k+1) & N2 is_succ_of N1 by B1,A1,DefFinseq;
k in dom L1 by B1,A4,FINSEQ_1:3;
then B4:L1.k=L.k by A3,FUNCT_1:70;
1<= k+1 & k+1<=m by B1,A4,NAT_1:13;
then k+1 in dom L1 by A4,FINSEQ_1:3;
then L1.(k+1)=L.(k+1) by A3,FUNCT_1:70;
hence thesis by B4,B3;
end;
hence thesis by DefFinseq;
end;
theorem ThSucc03:
L is_Finseq_for v &
not (F in the LTLold of CastNode(L.1,v)) &
(1< n & n <= len(L) & F in the LTLold of CastNode(L.n,v) )
implies ex m st 1<= m & m=1;
L1.n = L.n & L1.1=L.1 by D9,D6;
then E3:len(CastNode(L.n,v)) <= len(CastNode(L.1,v)) -n+1
by B1,D1,D3,ThSucc02,D9,D5;
len(CastNode(L.k,v)) <= len(CastNode(L.n,v)) -1
by ThSucc11,D1,D3,D9,Thlen17;
then len(CastNode(L.k,v)) + 1 <= len(CastNode(L.n,v))-1 +1
by XREAL_1:8;
then len(CastNode(L.k,v)) + 1 <= (len(CastNode(L.1,v)) -n)+1
by E3,XXREAL_0:2;
hence thesis by D9,XREAL_1:8;
end;
suppose k=n+1 & n=0;
hence thesis;
end;
end;::**cases
hence thesis;
end;
hence thesis;
end;
P[n+1]
proof
let L,j such that C1:len(L)<=n+1;
L is_Finseq_for v & 1<= j & j<=len(L)
implies len(CastNode(L.j,v)) <= len(CastNode(L.1,v)) -j+1
proof
now per cases by C1,NAT_1:8;
suppose len(L)<=n;
hence thesis by B1;
end;
suppose len(L) =n+1;
hence thesis by B2;
end;
end;::**cases
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
reserve s,s0,s1,s2,t,t0,t1,t2 for elementary strict LTLnode over v;
theorem ThNext01:
s2 is_next_of s1 implies the LTLnext of s1 c= the LTLold of s2
proof
assume s2 is_next_of s1;
then consider L such that A1: 1<=len(L) & L is_Finseq_for v and
A2: L.1 = 'X' s1 & L.(len(L)) = s2 by Def215;
set N1 = 'X' s1;
set n = len(L);
A3:CastNode(L.1,v) = N1 by defCastNode01,A2;
A4:CastNode(L.n,v) = s2 by defCastNode01,A2;
A5:the LTLnew of s2 = {} v by Defelementary;
the LTLnext of s1 c= the LTLold of s2
proof
let x; assume B1:x in the LTLnext of s1;
x in Subformulae v by B1;
then reconsider x as LTL-formula by MODELC_2:1;
1 non empty set means
:defLTLNodes:
x in it iff ex N being strict LTLnode over v st x=N;
existence
proof
set T= bool Subformulae v;
set Y = [: T,T,T :];
defpred P[set, set] means
$1 in Y &
ex y1,y2,y3 being Subset of Subformulae v,
N being strict LTLnode over v
st $1 = [[y1,y2],y3] & $2 = N &
the LTLold of N = y1 & the LTLnew of N = y2 &
the LTLnext of N = y3;
A1:for x,y,z being set st P[x,y] & P[x,z] holds y = z
proof
let x,y,z being set such that B1:P[x,y] and B2: P[x,z];
consider y1,y2,y3 being Subset of Subformulae v,
N1 being strict LTLnode over v
such that B3:x = [[y1,y2],y3] & y = N1 &
the LTLold of N1 = y1 & the LTLnew of N1 = y2 &
the LTLnext of N1 = y3 by B1;
consider z1,z2,z3 being Subset of Subformulae v,
N2 being strict LTLnode over v
such that B4:x = [[z1,z2],z3] & z = N2 &
the LTLold of N2 = z1 & the LTLnew of N2 = z2 &
the LTLnext of N2 = z3 by B2;
[y1,y2]= [z1,z2] & y3=z3 by B3,B4,ZFMISC_1:33;
then y1=z1 & y2=z2 & y3=z3 by ZFMISC_1:33;
hence thesis by B3,B4;
end;
consider IT being set
such that A2:for x holds x in IT iff ex y st y in Y & P[y,x]
from TARSKI:sch 1(A1);
IT is non empty
proof
set e = {}v;
set x = LTLnode(# e,e,e #);
set y = [[e,e], e];
[e,e] in [: T,T :] by ZFMISC_1:def 2;
then [[e,e],e] in [: [: T,T :], T :] by ZFMISC_1:def 2;
then P[y,x] by ZFMISC_1:def 3;
hence thesis by A2;
end;
then reconsider IT as non empty set;
take IT;
A3:x in IT implies ex N being strict LTLnode over v st x=N
proof
assume x in IT;
then consider y such that B1:y in Y & P[y,x] by A2;
consider y1,y2,y3 being Subset of Subformulae v,
N being strict LTLnode over v
such that B2:y = [[y1,y2],y3] & x = N &
the LTLold of N = y1 & the LTLnew of N = y2 &
the LTLnext of N = y3 by B1;
thus thesis by B2;
end;
(ex N being strict LTLnode over v st x=N) implies x in IT
proof
assume ex N being strict LTLnode over v st x=N;
then consider N being strict LTLnode over v
such that B1:x = N;
set y1 = the LTLold of N;
set y2 = the LTLnew of N;
set y3 = the LTLnext of N;
set y = [[y1,y2],y3];
[y1,y2] in [: T,T :] by ZFMISC_1:def 2;
then [[y1,y2],y3] in [: [: T,T :], T :] by ZFMISC_1:def 2;
then y in Y by ZFMISC_1:def 3;
hence thesis by B1,A2;
end;
hence thesis by A3;
end;
uniqueness
proof
let X,Y being non empty set;
(for x holds x in X iff ex N being strict LTLnode over v st x=N) &
(for x holds x in Y iff ex N being strict LTLnode over v st x=N)
implies X = Y
proof
assume that
A1:(for x holds x in X iff ex N being strict LTLnode over v st x=N) &
(for x holds x in Y iff ex N being strict LTLnode over v st x=N);
for x holds x in X iff x in Y
proof
let x;
x in X iff ex N being strict LTLnode over v st x=N by A1;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
hence thesis;
end;
end;
registration
let v;
cluster LTLNodes(v) -> finite;
correctness
proof
set LN = LTLNodes(v);
set X = bool Subformulae v;
set Y = [:X,X,X:];
deffunc F(set)
= [ [the LTLold of CastNode($1,v),
the LTLnew of CastNode($1,v) ],
the LTLnext of CastNode($1,v) ];
A1:for x st x in LN holds F(x) in Y
proof
let x;
assume x in LN;
then consider N being strict LTLnode over v
such that B1: x=N by defLTLNodes;
set N1 = the LTLold of CastNode(x,v);
set N2 = the LTLnew of CastNode(x,v);
set N3 = the LTLnext of CastNode(x,v);
set M1 = [N1,N2];
set X1 = [:X,X:];
B1p:F(x) = [M1,N3] & Y =[:X1,X:] by ZFMISC_1:def 3;
reconsider x as strict LTLnode over v by B1;
M1 in X1 by ZFMISC_1:106;
hence thesis by B1p,ZFMISC_1:106;
end;
ex f being Function of LN,Y st for x st x in LN holds f.x = F(x)
from FUNCT_2:sch 2(A1);
then consider f being Function of LN,Y such that
A2:for x st x in LN holds f.x = F(x);
A3p:dom f = LN & rng f c=Y by FUNCT_2:def 1;
for x1,x2 be set st x1 in LN & x2 in LN & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be set;
assume that B1:x1 in LN & x2 in LN & f.x1 = f.x2;
consider Nx1 being strict LTLnode over v
such that B2: x1=Nx1 by B1,defLTLNodes;
set Nx11 = the LTLold of CastNode(x1,v);
set Nx12 = the LTLnew of CastNode(x1,v);
set Nx13 = the LTLnext of CastNode(x1,v);
set Mx1 = [Nx11,Nx12];
reconsider x1 as strict LTLnode over v by B2;
B3:Nx11 = the LTLold of x1 & Nx12 = the LTLnew of x1 &
Nx13 = the LTLnext of x1 by defCastNode01;
B4:f.x1 = [Mx1,Nx13] by A2,B1;
consider Nx2 being strict LTLnode over v
such that B5: x2=Nx2 by B1,defLTLNodes;
set Nx21 = the LTLold of CastNode(x2,v);
set Nx22 = the LTLnew of CastNode(x2,v);
set Nx23 = the LTLnext of CastNode(x2,v);
set Mx2 = [Nx21,Nx22];
reconsider x2 as strict LTLnode over v by B5;
B6:Nx21 = the LTLold of x2 & Nx22 = the LTLnew of x2 &
Nx23 = the LTLnext of x2 by defCastNode01;
B7:f.x2 = [Mx2,Nx23] by A2,B1;
Mx1 =Mx2 & Nx13 = Nx23 by B1,B4,B7,ZFMISC_1:33;
then Nx11 = Nx21 & Nx12 = Nx22 & Nx13 = Nx23 by ZFMISC_1:33;
hence thesis by B3,B6;
end;
then A4:f is one-to-one by FUNCT_2:25;
rng f is finite;
then dom (f") is finite by A4,FUNCT_1:55;
then rng (f") is finite by FINSET_1:26;
hence thesis by A4,A3p,FUNCT_1:55;
end;
end;
definition
let v;
func LTLStates(v) -> non empty set equals
{x where x is Element of LTLNodes(v):
x is elementary strict LTLnode over v};
coherence
proof
set IT = {x where x is Element of LTLNodes(v):
x is elementary strict LTLnode over v};
init v is Element of LTLNodes(v) by defLTLNodes;
then init v in IT;
hence thesis;
end;
end;
registration
let v;
cluster LTLStates(v) -> finite;
correctness
proof
LTLStates(v) c= LTLNodes(v)
proof
LTLStates(v) c= LTLNodes(v)
proof
let a; assume a in LTLStates(v);
then consider x being Element of LTLNodes(v)
such that C1: a=x & x is elementary strict LTLnode over v;
thus a in LTLNodes(v) by C1;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem
init v is Element of LTLStates(v)
proof
init v is Element of LTLNodes(v) by defLTLNodes;
then init v in LTLStates(v);
hence thesis;
end;
theorem ThLTLStates02:
s is Element of LTLStates(v)
proof
s is Element of LTLNodes(v) by defLTLNodes;
then s in LTLStates(v);
hence thesis;
end;
theorem ThLTLStates03:
x is Element of LTLStates(v) iff ex s st s=x
proof
x is Element of LTLStates(v) implies ex s st s=x
proof
assume x is Element of LTLStates(v);
then x in LTLStates(v);
then consider y be Element of LTLNodes(v) such that
B1: y=x and
B2:y is elementary strict LTLnode over v;
reconsider y as elementary strict LTLnode over v by B2;
take y;
thus thesis by B1;
end;
hence thesis by ThLTLStates02;
end;
lemExistMin:X<>{} & X c= Seg n implies
ex k st 1<=k & k<=n & k in X &
for i st 1<=i & i{} & X c= Seg $1 holds
ex k st 1<=k & k<=$1 & k in X &
for i st 1<=i & i{} & Y c= Seg m1 & not m1 in Y implies Y c= Seg m
proof
assume that D1:Y<>{} & Y c= Seg m1 & not m1 in Y;
Y c= Seg m
proof
let x; assume E1:x in Y;
then x in Seg m1 by D1;
then x in { j where j is Element of NAT
:1 <= j & j <= m1 } by FINSEQ_1:def 1;
then consider j being Element of NAT such that
E2:x=j & 1 <= j & j <= m1;
j {} & X c= Seg m1 holds
ex k st 1<=k & k<=m1 & k in X &
for i st 1<=i & i{} & X c= Seg m1;
now per cases;
suppose not m1 in X;
then X c= Seg m by C1,B2;
then consider k such that
D1:1<=k & k<= m & k in X &
for i st 1<=i & i {};
then X1 c= Seg m by B2,D1,D2;
then consider k such that
E1:1<=k & k<=m & k in X1 &
for i st 1<=i & i=1 holds (F 'U' G in the LTLold of CastNode(q.i,v)) &
(F in the LTLold of CastNode(q.i,v)) &
not ( G in the LTLold of CastNode(q.i,v)))
or
(ex j st j>=1 & ( G in the LTLold of CastNode(q.j,v)) &
(for i st 1<=i & i=1 holds (F 'U' G in the LTLold of Node(i)) &
(F in the LTLold of Node(i)) &
not ( G in the LTLold of Node(i)))
implies
(ex j st j>=1 & ( G in the LTLold of Node(j)) &
(for i st 1<=i & i=1 holds
(F 'U' G in the LTLold of Node(i)) &
(F in the LTLold of Node(i)) &
not ( G in the LTLold of Node(i)));
then consider k such that
B1:k>=1 and
B2:not (F 'U' G in the LTLold of Node(k)
& F in the LTLold of Node(k) ) or
(G in the LTLold of Node(k));
set k1=k+1;
B3:ex m st 1<=m & m<=k & G in the LTLold of Node(m)
proof
now per cases by B2;
suppose C1:not (F 'U' G in the LTLold of Node(k)
& F in the LTLold of Node(k) );
now assume C100:not ex m st 1<=m & m<=k &
G in the LTLold of Node(m);
C2:for m st 1<=m & m=1 & ( G in the LTLold of Node(j))
proof
consider m being Element of NAT such that
C1:j = m & 1<=m & m<=k & G in the LTLold of Node(m) by B7;
thus thesis by C1;
end;
for i st 1<=i & i=1 holds
(H in the LTLold of CastNode(q.i,v)) &
(the_left_argument_of H in the LTLold of CastNode(q.i,v)) &
not (the_right_argument_of H in the LTLold of CastNode(q.i,v)))
or
(ex j st j>=1 &
(the_right_argument_of H in the LTLold of CastNode(q.j,v)) &
(for i st 1<=i & i {} &
the LTLnew of N in BOOL Subformulae v
proof
set x = the LTLnew of N;
assume N is non elementary;
then x <> {} by Defelementary;
hence thesis by ORDERS_1:6;
end;
registration let v;
cluster union BOOL Subformulae v -> non empty;
correctness by ThBOOL01;
cluster BOOL Subformulae v -> non empty;
correctness;
end;
theorem
ex f being Choice_Function of BOOL Subformulae v st
f is Function of BOOL Subformulae v,Subformulae v
proof
set Y = Subformulae v;
set X = BOOL Y;
A0:not {} in X by ORDERS_1:4;
A1:union X = Y by ThBOOL01;
for x st x in X holds x <> {} by ORDERS_1:4;
then consider Choice being Function such that
A4:dom Choice = X &
for x st x in X holds Choice.x in x by WELLORD2:28;
A6:for x st x in X holds Choice.x in Y
proof
let x such that B1:x in X;
x is non empty by B1,ORDERS_1:4;
then B2:x is Subset of Y by B1,ORDERS_1:6;
Choice.x in x by B1,A4;
hence thesis by B2;
end;
then Choice is Function of X,Y by A4,FUNCT_2:5;
then reconsider Choice as Choice_Function of X
by A0,A1,A4,ORDERS_1:def 1;
take Choice;
thus thesis by A6,A4,FUNCT_2:5;
end;
reserve U for Choice_Function of BOOL Subformulae v;
definition
let v;
let U;
let N;
assume A1:N is non elementary;
func chosen_formula(U,N) -> LTL-formula equals
:Defchosenformula:U.(the LTLnew of N);
correctness
proof
set x = the LTLnew of N;
set a = U.x;
x in BOOL Subformulae v by A1,ThBOOL02;
then U.x in union BOOL Subformulae v by FUNCT_2:7;
then a in Subformulae v by ThBOOL01;
then consider F such that B1:F = a & F is_subformula_of v
by MODELC_2:def 24;
thus thesis by B1;
end;
end;
theorem Thchoice:
N is non elementary implies chosen_formula(U,N) in the LTLnew of N
proof
assume A1:not N is elementary;
set x = the LTLnew of N;
set X = BOOL Subformulae v;
X is non empty & not {} in X & x in X by A1,ThBOOL02,ORDERS_1:4;
then U.x in x by ORDERS_1:def 1;
hence thesis by Defchosenformula,A1;
end;
definition
let w;
let v;
let U;
let N;
func chosen_succ(w,v,U,N) -> strict LTLnode over v equals
:Defchosensucc:
SuccNode1(chosen_formula(U,N),N)
if (not chosen_formula(U,N) is Until &
w |= *SuccNode1(chosen_formula(U,N),N))
or
(chosen_formula(U,N) is Until &
w |/= the_right_argument_of chosen_formula(U,N))
otherwise SuccNode2(chosen_formula(U,N),N);
correctness;
end;
theorem Thchosensucc01:
w|=*N & N is non elementary implies
w|=*chosen_succ(w,v,U,N) &
chosen_succ(w,v,U,N) is_succ_of N
proof
assume A1:w|=*N & N is non elementary;
set SN = chosen_succ(w,v,U,N);
set H = chosen_formula(U,N);
set H2 = the_right_argument_of H;
A2:H in the LTLnew of N by A1,Thchoice;
now per cases;
suppose A3:(not H is Until & w |= *SuccNode1(H,N)) or
(H is Until & w |/= H2);
then B1:SN = SuccNode1(H,N) by Defchosensucc;
then Bp1:SN is_succ1_of N by A2,Def208;
w|=*SN
proof
now per cases by A3;
suppose (not H is Until & w |= *SuccNode1(H,N));
hence thesis by Defchosensucc;
end;
suppose C1:(H is Until & w |/= H2);
set N2 = SuccNode2(H,N);
D1:w |= *SN or w |= *N2 by A1,A2,B1,C1,Lem204;
now assume E1:not w |= *SN;
E2:the LTLold of N2 =(the LTLold of N) \/ {H} &
the LTLnew of N2 = ((the LTLnew of N) \ {H})
\/ (LTLNew2 H \ the LTLold of N)
by A2,C1,Def207;
LTLNew2 H = {H2} by C1,Def204;
then H2 in LTLNew2 H by TARSKI:def 1;
then not H2 in the LTLold of N implies
H2 in (LTLNew2 H \ the LTLold of N) by XBOOLE_0:def 5;
then E3:not H2 in the LTLold of N implies
H2 in the LTLnew of N2 by E2,XBOOLE_0:def 3;
H2 in the LTLold of N implies H2 in the LTLold of N2
by E2,XBOOLE_0:def 3;
then H2 in *N2 by LemSUM01,E3;
hence contradiction by E1,D1,C1,MODELC_2:def 66;
end;
hence thesis;
end;
end;::**cases
hence thesis;
end;
hence thesis by Bp1,Def210;
end;
suppose A4:not ((not H is Until & w |= *SuccNode1(H,N)) or
(H is Until & w |/= H2));
then B1:SN = SuccNode2(H,N) by Defchosensucc;
set N1 = SuccNode1(H,N);
w|=*SN & SN is_succ_of N
proof
now per cases by A4;
suppose B3:H is Until & w |= H2;
then Cp1:SN is_succ2_of N by A2,B1,Def209;
C1:LTLNew2 H = {H2} by B3,Def204;
set SNO = the LTLold of SN;
set SNN = the LTLnew of SN;
set SNX = the LTLnext of SN;
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
C2:SNO =NO \/ {H} &
SNN = (NN \ {H}) \/ ({H2} \ NO) &
SNX = NX by A2,B1,B3,Def207,C1;
{H} c= NN by A2,ZFMISC_1:37;
then C4:SNO c= NO \/ NN by C2,XBOOLE_1:9;
(NN \ {H} c= NN) & ({H2} \ NO c= {H2}) by XBOOLE_1:36;
then C5:SNN c= NN \/ {H2} by C2,XBOOLE_1:13;
G in *SN implies w|=G
proof
assume D1:G in *SN;
now per cases by D1,LemSUM01;
suppose G in SNO;
then G in *N by C4,XBOOLE_0:def 3;
hence thesis by A1,MODELC_2:def 66;
end;
suppose G in SNN;
then G in NN or G in {H2} by C5,XBOOLE_0:def 3;
then G in *N or G = H2 by LemSUM01,TARSKI:def 1;
hence thesis by A1,B3,MODELC_2:def 66;
end;
suppose G in 'X' CastLTL(SNX);
then G in *N by C2,LemSUM01;
hence thesis by A1,MODELC_2:def 66;
end;
end;::**cases
hence thesis;
end;
hence thesis by Cp1,Def210,MODELC_2:def 66;
end;
suppose B4:not w |=*N1;
now per cases by MODELC_2:2;
suppose (H is atomic or H is negative or
H is conjunctive or H is next);
hence thesis by A1,A2,LemSUM04,LemSUM06,B4;
end;
suppose C2:(H is disjunctive or H is Until or H is Release);
then SN is_succ2_of N by A2,B1,Def209;
hence thesis by Def210,A1,A2,B1,C2,Lem203,Lem204,Lem205,B4;
end;
end;::**cases
hence thesis;
end;
end;::**cases
hence thesis;
end;
hence thesis;
end;
end;::**cases;
hence thesis;
end;
theorem
w|=*N & N is non elementary implies
( chosen_formula(U,N) is Until &
w |= the_right_argument_of chosen_formula(U,N)
implies
(the_right_argument_of chosen_formula(U,N)
in the LTLnew of chosen_succ(w,v,U,N) or
the_right_argument_of chosen_formula(U,N)
in the LTLold of N ) &
(chosen_formula(U,N)
in the LTLold of chosen_succ(w,v,U,N)) )
proof
assume A1:w|=*N & N is non elementary;
set SN = chosen_succ(w,v,U,N);
set H = chosen_formula(U,N);
set H2 = the_right_argument_of H;
set SNO = the LTLold of SN;
set SNN = the LTLnew of SN;
set SNX = the LTLnext of SN;
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
A2:H in the LTLnew of N by A1,Thchoice;
H is Until & w |= H2 implies
(H2 in SNN or H2 in NO) & H in SNO
proof
assume B1:H is Until & w |= H2;
then B2:SN = SuccNode2(H,N) by Defchosensucc;
B3:LTLNew2 H = {H2} by B1,Def204;
B4:SNO =NO \/ {H} &
SNN = (NN \ {H}) \/ ({H2} \ NO) &
SNX = NX by A2,B1,B2,Def207,B3;
B5:H in {H} by TARSKI:def 1;
now per cases;
suppose H2 in NO;
hence H2 in SNN or H2 in NO;
end;
suppose B6:not H2 in NO;
H2 in {H2} by TARSKI:def 1;
then H2 in {H2} \ NO by B6,XBOOLE_0:def 5;
hence H2 in SNN or H2 in NO by B4,XBOOLE_0:def 3;
end;
end;::**cases
hence thesis by B5,B4,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem
w|=*N & N is non elementary implies
the LTLold of N c= the LTLold of chosen_succ(w,v,U,N) &
the LTLnext of N c= the LTLnext of chosen_succ(w,v,U,N)
proof
assume w|=*N & N is non elementary;
then chosen_succ(w,v,U,N) is_succ_of N by Thchosensucc01;
hence thesis by ThSucc01;
end;
definition
let w;
let v;
let U;
func choice_succ_func(w,v,U)
-> Function of LTLNodes(v),LTLNodes(v) means
:Defchoicesuccfunc:
for x st x in LTLNodes(v) holds
it.x = chosen_succ(w,v,U,CastNode(x,v));
existence
proof
deffunc F(set) = chosen_succ(w,v,U,CastNode($1,v));
A1:for x st x in LTLNodes(v) holds F(x) in LTLNodes(v)
by defLTLNodes;
consider IT being Function of LTLNodes(v),LTLNodes(v) such that
A2: for x st x in LTLNodes(v) holds IT.x = F(x)
from FUNCT_2:sch 2 (A1);
take IT;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 being Function of LTLNodes(v),LTLNodes(v) such that
A1:(for x st x in LTLNodes(v) holds
f1.x = chosen_succ(w,v,U,CastNode(x,v))) and
A2:(for x st x in LTLNodes(v) holds
f2.x = chosen_succ(w,v,U,CastNode(x,v)) );
for x st x in LTLNodes(v) holds f1.x = f2.x
proof
let x;
assume B1:x in LTLNodes(v);
f1.x = chosen_succ(w,v,U,CastNode(x,v)) by A1,B1
.= f2.x by A2,B1;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Thchoicesuccfunc01:
choice_succ_func(w,v,U) is_succ_homomorphism v,w
proof
set f = choice_succ_func(w,v,U);
for x st x in LTLNodes(v) & CastNode(x,v) is non elementary &
w |= *CastNode(x,v) holds
CastNode(f.x,v) is_succ_of CastNode(x,v) &
w |= *CastNode(f.x,v)
proof
let x such that A1:x in LTLNodes(v) &
CastNode(x,v) is non elementary &
w|=*CastNode(x,v);
set N = CastNode(x,v);
set SN = chosen_succ(w,v,U,N);
CastNode(f.x,v) = CastNode(SN,v) by A1,Defchoicesuccfunc
.= SN by defCastNode01;
hence thesis by A1,Thchosensucc01;
end;
hence thesis by defSuccHom;
end;
begin :: Definition of Negation inner most LTL.
definition let H;
attr H is neg-inner-most means
:DefNegIM:
for G being LTL-formula st G is_subformula_of H holds
G is negative implies the_argument_of G is atomic;
end;
registration
cluster neg-inner-most LTL-formula;
existence
proof
set a=atom.0;
A1:a is atomic by MODELC_2:def 11;
take a;
for G being LTL-formula st G is_subformula_of a holds
G is negative implies the_argument_of G is atomic
proof
let G being LTL-formula such that B1:G is_subformula_of a;
consider n,L such that B2: 1 <= n & len L = n & L.1 = G & L.n = a &
for k st 1 <= k & k < n
ex H1,G1 being LTL-formula st L.k = H1 & L.(k + 1) = G1 &
H1 is_immediate_constituent_of G1 by B1,MODELC_2:def 22;
B3:n=1
proof
set k = n-1;
reconsider k as Nat by B2,NAT_1:21;
now assume not (n=1);
then 1<1+k by B2,XXREAL_0:1;
then C0:1<=k by NAT_1:19;
k set,
Tran -> Relation of [:the carrier,W :], the carrier,
InitS -> Element of bool the carrier,
FinalS -> Subset of bool the carrier #);
end;
definition let W be non empty set, B be BuchiAutomaton over W;
let w be Element of Inf_seq(W);
pred w is-accepted-by B means
:DefBam01:
ex run be sequence of the carrier of B st
run.0 in the InitS of B
&
for i be Nat holds
[[run.i,CastSeq(w,W).i],run.(i+1)] in the Tran of B
&
for FSet be set st FSet in the FinalS of B holds
{k where k is Element of NAT:run.k in FSet} is infinite set;
end;
:: Preparation to define Buch Automaton for neg-inner-most LTL-formula v
:: after this, reserve v as neg-inner-most LTL-formula
reserve v for neg-inner-most LTL-formula;
reserve U for Choice_Function of BOOL Subformulae v;
reserve N,N1,N2,M,M1,M2 for strict LTLnode over v;
reserve s,s0,s1,s2 for elementary strict LTLnode over v;
definition
let v;
let N;
func atomic_LTL(N) -> Subset of LTL_WFF equals
{x where x is LTL-formula:x is atomic & x in the LTLold of N};
correctness
proof
set X = {x where x is LTL-formula:x is atomic & x in the LTLold of N};
X c= LTL_WFF
proof
let y;
assume y in X;
then ex x being LTL-formula st y=x & x is atomic &
x in the LTLold of N;
hence y in LTL_WFF by MODELC_2:1;
end;
hence thesis;
end;
func Neg_atomic_LTL(N) -> Subset of LTL_WFF equals
{x where x is LTL-formula:x is atomic & ('not' x) in the LTLold of N};
correctness
proof
set X = {x where x is LTL-formula:x is atomic &
('not' x) in the LTLold of N};
X c= LTL_WFF
proof
let y;
assume y in X;
then ex x being LTL-formula st y=x & x is atomic &
('not' x) in the LTLold of N;
hence y in LTL_WFF by MODELC_2:1;
end;
hence thesis;
end;
end;
definition
let v;
let N;
func Label_(N) -> set equals
{x where x is Subset of atomic_LTL:atomic_LTL(N) c= x &
Neg_atomic_LTL(N) misses x };
correctness;
end;
definition
let v;
func Tran_LTL(v) -> Relation of
[:LTLStates(v),AtomicFamily:], LTLStates(v) equals
{y where y is Element of [:LTLStates(v),AtomicFamily,LTLStates(v):]
: ex s,s1,x st y=[[s,x],s1] & s1 is_next_of s & x in Label_(s1)};
correctness
proof
set X = {y where y is Element of
[: LTLStates(v),AtomicFamily,LTLStates(v) :]
: ex s,s1,x st y=[[s,x],s1] & s1 is_next_of s &
x in Label_(s1)};
X c= [: LTLStates(v),AtomicFamily,LTLStates(v) :]
proof
let a;
assume a in X;
then consider y being Element of
[: LTLStates(v),AtomicFamily,LTLStates(v) :] such that
B1:a=y &
(ex s,s1,x st y=[[s,x],s1] & s1 is_next_of s & x in Label_(s1));
thus thesis by B1;
end;
then X c= [: [: LTLStates(v),AtomicFamily:],LTLStates(v) :]
by ZFMISC_1:def 3;
then reconsider X as Relation of
[:LTLStates(v),AtomicFamily:], LTLStates(v)
by RELSET_1:def 1;
X is Relation of [:LTLStates(v),AtomicFamily:], LTLStates(v);
hence thesis;
end;
func InitS_LTL(v) -> Element of bool LTLStates(v) equals
{init v};
correctness
proof
set y = init v;
reconsider y as elementary strict LTLnode over v;
A1:y is Element of LTLNodes(v) &
y is elementary strict LTLnode over v by defLTLNodes;
{y} c= LTLStates(v)
proof
let x;
assume x in {y};
then x = y by TARSKI:def 1;
hence thesis by A1;
end;
hence thesis;
end;
end;
definition
let v;
let F;
func FinalS_LTL(F,v) -> Element of bool LTLStates(v) equals
{x where x is Element of LTLStates(v):
not F in the LTLold of CastNode(x,v) or
the_right_argument_of F in the LTLold of CastNode(x,v) };
correctness
proof
set X ={x where x is Element of LTLStates(v):
not F in the LTLold of CastNode(x,v) or
the_right_argument_of F in the LTLold of CastNode(x,v) };
X c= LTLStates(v)
proof
let y be set;
assume y in X;
then ex x being Element of LTLStates(v) st
y = x &
(not F in the LTLold of CastNode(x,v) or
the_right_argument_of F in the LTLold of CastNode(x,v));
hence thesis;
end;
hence thesis;
end;
end;
definition
let v;
func FinalS_LTL(v) -> Subset of bool LTLStates(v) equals
{x where x is Element of bool LTLStates(v):
ex F st F is_subformula_of v & F is Until &
x= FinalS_LTL(F,v)};
correctness
proof
set X = {x where x is Element of bool LTLStates(v):
ex F st F is_subformula_of v & F is Until &
x= FinalS_LTL(F,v)};
X c= bool LTLStates(v)
proof
let y;
assume y in X;
then ex x being Element of bool LTLStates(v) st
y = x &
ex F st F is_subformula_of v & F is Until &
x= FinalS_LTL(F,v);
hence thesis;
end;
hence thesis;
end;
end;
definition
let v;
func BAutomaton(v) -> BuchiAutomaton over AtomicFamily equals
BuchiAutomaton (#
LTLStates(v),
Tran_LTL(v),
InitS_LTL(v),
FinalS_LTL(v) #);
correctness;
end;
::************
:: verification of the main theorem
::************
theorem thBA01:
w is-accepted-by BAutomaton(v) implies w |= v
proof
deffunc Gzai(Nat) = CastSeq(w,AtomicFamily).$1;
assume w is-accepted-by BAutomaton(v);
then consider run being sequence of LTLStates(v) such that
A1:run.0 in InitS_LTL(v) and
A2:for i holds
[[run.i,Gzai(i)],run.(i+1)] in Tran_LTL(v) and
A3:for FSet be set st FSet in FinalS_LTL(v) holds
{k where k is Element of NAT:run.k in FSet} is infinite set
by DefBam01;
deffunc Run(Nat) = CastNode(run.$1,v);
A4:Run(0) = CastNode(init v,v) by A1,TARSKI:def 1
.= init v by defCastNode01;
A5:for i holds
Run(i+1) is_next_of Run(i) & Gzai(i) in Label_(Run(i+1))
proof
let i;
set z= [[run.i,Gzai(i)],run.(i+1)];
z in Tran_LTL(v) by A2;
then consider y being Element of
[:LTLStates(v),AtomicFamily,LTLStates(v):] such that
B1:z = y & (ex s,s1,x st y=[[s,x],s1] &
s1 is_next_of s & x in Label_(s1));
consider s,s1,x such that B2: y=[[s,x],s1] & s1 is_next_of s &
x in Label_(s1) by B1;
B3:[s,x] = [run.i,Gzai(i)] & s1 = run.(i+1) by B1,B2,ZFMISC_1:33;
B4:Run(i) = CastNode(s,v) by B3,ZFMISC_1:33
.= s by defCastNode01;
Run(i+1) = CastNode(s1,v) by B1,B2,ZFMISC_1:33
.= s1 by defCastNode01;
hence thesis by B2,B3,B4,ZFMISC_1:33;
end;
A6:for i holds Run(i) = run.i
proof
let i;
reconsider i as Element of NAT by ORDINAL1:def 13;
run.i in LTLStates(v);
then consider x being Element of LTLNodes(v)
such that B1:run.i =x & x is elementary strict LTLnode over v;
thus thesis by defCastNode01,B1;
end;
A7:for FSet be set st FSet in FinalS_LTL(v) holds
{k where k is Element of NAT:Run(k) in FSet} is infinite
proof
let FSet be set;
assume B0:FSet in FinalS_LTL(v);
set X = {k where k is Element of NAT:run.k in FSet};
set Y = {k where k is Element of NAT:Run(k) in FSet};
X = Y
proof
C1:X c= Y
proof
let x;
assume x in X;
then consider k being Element of NAT
such that D1:x=k & run.k in FSet;
x=k & Run(k) in FSet by D1,A6;
hence thesis;
end;
Y c= X
proof
let x;
assume x in Y;
then consider k being Element of NAT
such that D1:x=k & Run(k) in FSet;
x=k & run.k in FSet by D1,A6;
hence thesis;
end;
hence thesis by C1,XBOOLE_0:def 10;
end;
hence thesis by A3,B0;
end;
set Run01=Run(0+1);
set Run00=Run(0);
A800:Run01 is_next_of Run00 by A5;
reconsider Run00 as elementary strict LTLnode over v by Def215,A800;
reconsider Run01 as elementary strict LTLnode over v by Def215,A800;
A801:the LTLnext of Run00 c= the LTLold of Run01 by ThNext01,A5;
defpred P[Nat] means
for i,F st F is_subformula_of v & len(F)<=$1 &
F in the LTLold of Run(i+1) holds Shift(w,i) |= F;
A9:P[0] by MODELC_2:3;
A10:for n st P[n] holds P[n + 1]
proof
let n;
assume B1:P[n];
B3:for i,F st F is_subformula_of v & len(F) = n+1 &
F in the LTLold of Run(i+1) holds Shift(w,i) |= F
proof
let i,F;
assume C1:F is_subformula_of v & len(F)= n+1 &
F in the LTLold of Run(i+1);
set zeta = Shift(w,i);
now per cases by C1,ThNegIM01,ThNegIM03;
suppose C3:F is Sub_atomic;
set Gi=Gzai(i);
Gi in Label_(Run(i+1)) by A5;
then consider X being Subset of atomic_LTL
such that D1:Gi = X &
atomic_LTL(Run(i+1)) c= X &
Neg_atomic_LTL(Run(i+1)) misses X;
D01:Neg_atomic_LTL(Run(i+1)) /\ X ={} by D1,XBOOLE_0:def 7;
set Gi'=Shift(CastSeq(w,AtomicFamily),i);
CastSeq(zeta,AtomicFamily) = Gi' by MODELC_2:81;
then D3:CastSeq(zeta,AtomicFamily).0
= CastSeq(w,AtomicFamily).(0+i) by MODELC_2:def 43
.= Gi;
now per cases by ThNegIM02,C3;
suppose D4:F is atomic;
then F in atomic_LTL(Run(i+1)) by C1;
hence thesis by D1,D3,D4,MODELC_2:63;
end;
suppose D5:F is negative & the_argument_of F is atomic;
set Fa= the_argument_of F;
E2:F = 'not' Fa by D5,MODELC_2:4;
then zeta |= F iff zeta |/= Fa by MODELC_2:64;
then E3:zeta |= F iff not (Fa in Gi) by D5,D3,MODELC_2:63;
Fa in Neg_atomic_LTL(Run(i+1)) by C1,E2,D5;
hence thesis by D1,D01,E3,XBOOLE_0:def 4;
end;
end;::**cases
hence thesis;
end;
suppose C4:F is conjunctive or F is disjunctive;
set h1 = the_left_argument_of F;
set h2 = the_right_argument_of F;
D1:h1 is_subformula_of F & h2 is_subformula_of F
by C4,MODELC_2:31;
len(h1) < n+1 & len(h2) < n+1 by C4,C1,MODELC_2:11;
then D2: len(h1) <= n & len(h2) <= n by NAT_1:13;
set Runi = Run(i);
set Runi1 = Run(i+1);
D301:Runi1 is_next_of Runi & F in the LTLold of Runi1
by A5,C1;
reconsider Runi as elementary strict LTLnode over v
by Def215,D301;
reconsider Runi1 as elementary strict LTLnode over v
by Def215,D301;
D3:Runi1 is_next_of Runi & F in the LTLold of Runi1 implies
(F is conjunctive implies
h1 in the LTLold of Runi1 &
h2 in the LTLold of Runi1) &
(F is disjunctive implies
h1 in the LTLold of Runi1 or
h2 in the LTLold of Runi1) by Thnext03;
zeta |= F
proof
now per cases by C4;
suppose D4:F is conjunctive;
then zeta |= h1 & zeta |= h2
by D1,D2,D3,A5,C1,B1,MODELC_2:35;
then zeta |= h1 '&' h2 by MODELC_2:65;
hence thesis by D4,MODELC_2:6;
end;
suppose D5:F is disjunctive;
then zeta |= h1 or zeta |= h2
by D1,D2,D3,A5,C1,B1,MODELC_2:35;
then zeta |= h1 'or' h2 by MODELC_2:66;
hence thesis by D5,MODELC_2:7;
end;
end;::**cases
hence thesis;
end;
hence thesis;
end;
suppose C6:F is next;
set h = the_argument_of F;
D1:h is_subformula_of F by C6,MODELC_2:30;
len(h) < n+1 by C6,C1,MODELC_2:10;
then D2: len(h) <= n by NAT_1:13;
set i1=i+1;
set Runi =Run(i);
set Runi1 = Run(i1);
set Runi2 = Run(i1+1);
D301:Runi1 is_next_of Runi & F in the LTLold of Runi1
by A5,C1;
D302:Runi2 is_next_of Runi1 by A5;
reconsider Runi as elementary strict LTLnode over v
by Def215,D301;
reconsider Runi1 as elementary strict LTLnode over v
by Def215,D301;
reconsider Runi2 as elementary strict LTLnode over v
by Def215,D302;
D3:Runi1 is_next_of Runi & F in the LTLold of Runi1 implies
(F is next implies h in the LTLnext of Runi1) by Thnext03;
the LTLnext of Runi1 c= the LTLold of Runi2
by ThNext01,A5;
then Shift(w,i1) |= h by D1,C1,D2,D3,A5,C6,B1,MODELC_2:35;
then Shift(zeta,1) |= h by MODELC_2:80;
then zeta |= 'X' h by MODELC_2:67;
hence thesis by C6,MODELC_2:5;
end;
suppose C7:F is Until;
set h1 = the_left_argument_of F;
set h2 = the_right_argument_of F;
D0:F = h1 'U' h2 by C7,MODELC_2:8;
D1:h1 is_subformula_of F & h2 is_subformula_of F
by C7,MODELC_2:31;
len(h1) < n+1 & len(h2) < n+1 by C7,C1,MODELC_2:11;
then D2: len(h1) <= n & len(h2) <= n by NAT_1:13;
deffunc Fun(set) = run.(CastNat($1)+i);
D3:for x st x in NAT holds Fun(x) in LTLStates(v)
proof
let x;
assume x in NAT;
set y = CastNat(x)+i;
reconsider y as Element of NAT by ORDINAL1:def 13;
Fun(x) = run.y;
hence thesis;
end;
consider runQ being Function of NAT,LTLStates(v)
such that D4: for x st x in NAT holds runQ.x = Fun(x)
from FUNCT_2:sch 2(D3);
reconsider runQ as sequence of LTLStates(v);
deffunc RunQ(Nat) = CastNode(runQ.$1,v);
D5:for m holds RunQ(m) = Run(m+i)
proof
let m;
reconsider m as Element of NAT by ORDINAL1:def 13;
RunQ(m) = CastNode(Fun(m),v) by D4
.= Run(m+i) by MODELC_2:def 1;
hence thesis;
end;
D6:for m holds RunQ(m+1) is_next_of RunQ(m)
proof
let m;
set m1 = m+i;
E1:RunQ(m) = Run(m1) by D5;
RunQ(m+1) = Run((m+1)+i) by D5 .= Run(m1+1);
hence thesis by A5,E1;
end;
D7:F in the LTLold of RunQ(1) by C1,D5;
set Fin = FinalS_LTL(F,v);
set FRun = {k where k is Element of NAT:Run(k) in Fin};
set FRunQ = {k where k is Element of NAT:RunQ(k) in Fin};
D9:Fin in FinalS_LTL(v) by C1,C7;
D10:FRunQ is infinite
proof
set FRun1 = {k where k is Element of NAT:k<=i & k in FRun};
set FRun2 = {k where k is Element of NAT:i 0;
then 0<0+k;
then 1<= k & k <=i by EA1,NAT_1:19;
then k in Seg i by FINSEQ_1:3;
hence x in Seg i \/ {0} by EA1,XBOOLE_0:def 3;
end;
end;::**cases
hence x in Seg i \/ {0};
end;
hence thesis by E1,D9,A7,E2;
end;
D11:(for m st m>=1 holds
F in the LTLold of RunQ(m) &
h1 in the LTLold of RunQ(m) &
not (h2 in the LTLold of RunQ(m))) implies FRunQ is finite
proof
assume E1:(for m st m>=1 holds
F in the LTLold of RunQ(m) &
h1 in the LTLold of RunQ(m) &
not (h2 in the LTLold of RunQ(m)));
now assume EA0:not (FRunQ c= {0});
consider x such that EA1:x in FRunQ & not x in {0}
by EA0,TARSKI:def 3;
consider k being Element of NAT
such that EA2:x = k & RunQ(k) in Fin by EA1;
k <> 0 by EA1,EA2,TARSKI:def 1;
then 0<0+k;
then EA3:1 <= k by NAT_1:19;
set RQk = RunQ(k);
consider y being Element of LTLStates(v)
such that EA4:RQk = y &
(not F in the LTLold of CastNode(y,v) or
h2 in the LTLold of CastNode(y,v)) by EA2;
reconsider y as strict LTLnode over v by EA4;
CastNode(y,v) = RunQ(k) by EA4,defCastNode01;
hence contradiction by E1,EA3,EA4;
end;::**now
hence thesis;
end;
consider j such that
D12:j>=1 & (h2 in the LTLold of RunQ(j)) &
(for m st 1<=m & m Nat means
:DefUsuccEndnum:
(for i st in2;
now per cases by C1,XXREAL_0:1;
suppose n1
elementary strict LTLnode over v equals
:Defchosennext:
CastNode
((choice_succ_func(w,v,U)
|**chosen_succ_end_num(w,v,U,'X' N)).('X' N)
,v) if 'X' N is non elementary
otherwise FinalNode v;
correctness
proof
set XN = 'X' N;
set f = choice_succ_func(w,v,U);
set n = chosen_succ_end_num(w,v,U,XN);
set nextnode =CastNode((f|**n).XN,v);
now per cases;
suppose XN is non elementary;
thus thesis by A1,DefUsuccEndnum;
end;
suppose XN is elementary;
hence thesis;
end;
end;::**cases
hence thesis;
end;
end;
theorem thChoicedNext01:
w |= * ('X' s) implies
chosen_next(w,v,U,s) is_next_of s &
w |= *chosen_next(w,v,U,s)
proof
set LN = LTLNodes(v);
set N = 'X' s;
A0:N in LN by defLTLNodes;
assume A1:w |= *N;
set f = choice_succ_func(w,v,U);
set n = chosen_succ_end_num(w,v,U,N);
set nextnode =CastNode((f|**n).N,v);
now per cases;
suppose B1:N is non elementary;
then C1:nextnode = chosen_next(w,v,U,s)
by Defchosennext,A1;
set n1=n+1;
C3:1<=n1 by NAT_1:11;
deffunc F(set) = CastNode((f|**CastNat(CastNat($1)-1)).N,v);
ex L st len L = n1 &
for k being Nat
st k in dom L holds L.k=F(k) from FINSEQ_1:sch 2;
then consider L such that
C4:len L = n1 and
C5:for k being Nat st k in dom L holds L.k=F(k);
C601:Seg n1 = dom L by C4,FINSEQ_1:def 3;
C6:for k st 1<=k & k<=n1 holds L.k = CastNode((f|**CastNat(k-1)).N,v)
proof
let k;
assume 1<=k & k<=n1;
then k in Seg n1 by FINSEQ_1:3;
then L.k=CastNode((f|**CastNat(CastNat(k)-1)).N,v) by C5,C601;
hence thesis by MODELC_2:def 1;
end;
C7:L.1 = CastNode((f|**CastNat(1-1)).N,v) by C3,C6
.= CastNode((f|**0).N,v) by MODELC_2:def 1
.= CastNode((id LN).N,v) by FUNCT_7:86
.= CastNode(N,v) by A0,FUNCT_1:35
.='X' s by defCastNode01;
C8:L.(len L) = CastNode((f|**CastNat(n1-1)).N,v) by C6,C3,C4
.= nextnode by MODELC_2:def 1;
for k st 1 <= k & k < len(L) holds
ex N1,M1 st N1 = L.k & M1=L.(k+1) & M1 is_succ_of N1
proof
let k;
assume D1:1<=k & k sequence of LTLStates(v) means
:Defchosenrun:
it.0 = init v &
for n holds
it.(n+1) = chosen_next(Shift(w,n),v,U,CastNode(it.n,v));
existence
proof
set LS = LTLStates(v);
deffunc G(set,set) =
chosen_next(Shift(w,CastNat($1)),v,U,CastNode($2,v));
(ex y being set st ex f being Function st
y = f.0 & dom f = NAT & f.0 = init v &
for n being Element of NAT holds f.(n+1) = G(n,f.n)) &
for y1,y2 being set st (ex f being Function st
y1 = f.0 & dom f = NAT & f.0 = init v &
for n being Element of NAT holds f.(n+1) = G(n,f.n)) &
(ex f being Function st
y2 = f.0 & dom f = NAT & f.0 = init v &
for n being Element of NAT holds f.(n+1) = G(n,f.n))
holds y1 = y2 from RECDEF_1:sch 12;
then consider y being set such that
A0:ex f being Function st
y = f.0 & dom f = NAT & f.0 = init v &
for n being Element of NAT holds f.(n+1) = G(n,f.n);
consider IT being Function such that
A01:dom IT = NAT & IT.0 =init v &
for n being Element of NAT holds IT.(n+1) = G(n,IT.n) by A0;
A1:for n being Nat holds IT.(n+1) = G(n,IT.n)
proof
let n being Nat;
reconsider n as Element of NAT by ORDINAL1:def 13;
IT.(n+1) = G(n,IT.n) by A01;
hence thesis;
end;
A2:for n being Nat holds
IT.(n+1) = chosen_next(Shift(w,n),v,U,CastNode(IT.n,v))
proof
let n;
IT.(n+1)
= chosen_next(Shift(w,CastNat(n)),v,U,CastNode(IT.n,v)) by A1;
hence thesis by MODELC_2:def 1;
end;
for x st x in NAT holds IT.x in LS
proof
let x;
assume x in NAT;
then reconsider x as Nat;
B0:x=0 or 0<0+x;
now per cases by B0,NAT_1:19;
suppose B1:x = 0;
set y = IT.x;
reconsider y as Element of LTLNodes(v) by A01,B1,defLTLNodes;
IT.x = y;
hence thesis by A01,B1;
end;
suppose B2:1<=x;
set y = IT.x;
set x1 = x-1;
reconsider x1 as Nat by B2,NAT_1:21;
C1:y = IT.(x1+1) .= G(x1,IT.x1) by A1;
then reconsider y as Element of LTLNodes(v) by defLTLNodes;
IT.x = y;
hence thesis by C1;
end;
end;::**cases
hence thesis;
end;
then reconsider IT as sequence of LS by A01,FUNCT_2:5;
take IT;
thus thesis by A01,A2;
end;
uniqueness
proof
set LS = LTLStates(v);
deffunc G1(Nat,set) =
chosen_next(Shift(w,$1),v,U,CastNode($2,v));
deffunc G(set,set) =
chosen_next(Shift(w,CastNat($1)),v,U,CastNode($2,v));
A1:for f,g being Function of NAT,LTLStates(v) st
(f.0 =init v & for n holds f.(n+1) = G(n,f.n)) &
(g.0 =init v & for n holds g.(n+1) = G(n,g.n)) holds f = g
proof
let f,g being Function of NAT,LS such that
B1:(f.0 =init v & for n being Nat holds f.(n+1) = G(n,f.n)) and
B2:(g.0 =init v & for n being Nat holds g.(n+1) = G(n,g.n));
B4: dom f = NAT & f.0 =init v &
for n being Nat holds f.(n+1) = G(n,f.n) by B1,FUNCT_2:def 1;
B5: dom g = NAT & g.0 =init v &
for n being Nat holds g.(n+1) = G(n,g.n) by B2,FUNCT_2:def 1;
defpred P[Nat] means f.$1= g.$1;
B601:P[0] by B1,B2;
B602:for k being Element of NAT st P[k] holds P[k + 1]
proof
let k be Element of NAT such that C1:P[k];
f.(k+1) = G(k,g.k) by B1,C1 .= g.(k+1) by B2;
hence thesis;
end;
for k being Element of NAT holds P[k] from NAT_1:sch 1(B601,B602);
then for x st x in dom f holds f.x = g.x;
hence thesis by B4,B5,FUNCT_1:9;
end;
for f,g being Function of NAT,LTLStates(v) st
(f.0 =init v & for n holds f.(n+1) = G1(n,f.n)) &
(g.0 =init v & for n holds g.(n+1) = G1(n,g.n)) holds f = g
proof
let f,g being Function of NAT,LS such that
B1:(f.0 =init v & for n holds f.(n+1) = G1(n,f.n)) and
B2:(g.0 =init v & for n holds g.(n+1) = G1(n,g.n));
B3:for n holds f.(n+1) = G(n,f.n)
proof
let n;
f.(n+1) = chosen_next(Shift(w,n),v,U,CastNode(f.n,v)) by B1;
hence thesis by MODELC_2:def 1;
end;
for n holds g.(n+1) = G(n,g.n)
proof
let n;
g.(n+1) = chosen_next(Shift(w,n),v,U,CastNode(g.n,v)) by B2;
hence thesis by MODELC_2:def 1;
end;
hence thesis by B1,B2,B3,A1;
end;
hence thesis;
end;
end;
LemBA01:
'X' CastLTL({} v)= {}
proof
now assume 'X' CastLTL({} v) <> {};
then consider y such that
B1:y in 'X' CastLTL({} v) by XBOOLE_0:def 1;
consider x being LTL-formula such that
y=x and
B3:ex u being LTL-formula st u in CastLTL({} v) & x='X' u by B1;
consider u being LTL-formula such that
B4: u in CastLTL({} v) & x='X' u by B3;
thus contradiction by B4;
end;::**now assume
hence thesis;
end;
theorem thBA02:
w |= * N implies Shift(w,1) |= * ('X' N)
proof
assume A0:w |= *N;
set XN = 'X' N;
A4:*XN = CastLTL(the LTLnext of N) by LemBA01;
w |='X' CastLTL(the LTLnext of N)
proof
for H be LTL-formula st H in 'X' CastLTL(the LTLnext of N) holds w|= H
proof
let H be LTL-formula;
assume H in 'X' CastLTL(the LTLnext of N);
then H in *N by LemSUM01;
hence thesis by A0,MODELC_2:def 66;
end;
hence thesis by MODELC_2:def 66;
end;
hence thesis by A4,MODELC_2:77;
end;
theorem
w |= 'X' v implies w |= * (init v)
proof
assume A1:w |= 'X' v;
set N = init v;
for H be LTL-formula st H in 'X' CastLTL(Seed v) holds w|= H
proof
let H being LTL-formula;
assume B1: H in 'X' CastLTL(Seed v);
consider x being LTL-formula such that
B2:H=x and
B3:ex u being LTL-formula st u in CastLTL(Seed v) & x='X' u by B1;
consider u being LTL-formula such that
B4: u in CastLTL(Seed v) & x='X' u by B3;
thus thesis by B4,B2,A1,TARSKI:def 1;
end;
hence thesis by MODELC_2:def 66;
end;
theorem thBA04:
w |= v iff w |= *('X' init v)
proof
set N = init v;
set M = 'X' N;
A2:*M = {v} by LemBA01;
A3:w |= v implies w |= *M
proof
assume w |= v;
then for H be LTL-formula st H in *M holds w|= H by A2,TARSKI:def 1;
hence thesis by MODELC_2:def 66;
end;
w |= *M implies w |= v
proof
assume B1:w |= *M;
v in *M by A2,TARSKI:def 1;
hence thesis by B1,MODELC_2:def 66;
end;
hence thesis by A3;
end;
theorem thBA05:
w |= v implies
for n holds
CastNode(chosen_run(w,v,U).(n+1),v) is_next_of
CastNode(chosen_run(w,v,U).n,v) &
Shift(w,n) |= * ('X' CastNode(chosen_run(w,v,U).n,v))
proof
set s = init v;
assume w |= v;
then A1:w |= *('X' s) by thBA04;
deffunc R(Nat) = CastNode(chosen_run(w,v,U).$1,v);
defpred P[Nat] means
R($1+1) is_next_of R($1) & Shift(w,$1) |= *('X' R($1));
A2:P[0]
proof
B0:CastNode(chosen_run(w,v,U).0,v)
= CastNode(s,v) by Defchosenrun
.= s by defCastNode01;
R(0+1) = CastNode(
chosen_next
(Shift(w,0),v,U,
CastNode(chosen_run(w,v,U).0,v)
),v) by Defchosenrun
.= CastNode(chosen_next(w,v,U,s),v)
by B0,MODELC_2:79
.= chosen_next(w,v,U,s)
by defCastNode01;
hence thesis by B0,thChoicedNext01,A1,MODELC_2:79;
end;
A3:for n st P[n] holds P[n+1]
proof
let n;
set n1 =n+1;
set w1 = Shift(w,n);
set w2 = Shift(w,n1);
B0:w2 = Shift(w1,1) by MODELC_2:80;
set s1=R(n);
set s2=R(n1);
set s3=R(n1+1);
s1 is elementary strict LTLnode over v
proof
now per cases;
suppose n = 0;
then s1 = CastNode(s,v) by Defchosenrun
.= s by defCastNode01;
hence thesis;
end;
suppose C1:0 1 by C800,B1,C10,C8,XXREAL_0:1;
H in the LTLold of nextnode &
H is Until & w0|=the_right_argument_of H
implies
the_right_argument_of H
in the LTLold of nextnode
proof
set H2 = the_right_argument_of H;
assume D1:H in the LTLold of nextnode &
H is Until &
w0|=H2;
D3:the LTLold of CastNode(L.1,v)
= {} v by defCastNode01,C800;
D4:the LTLold of CastNode(L.len(L),v)
= the LTLold of nextnode by defCastNode01,C8;
consider m such that
D501:1<= m & m G;
then not (H in {G}) by TARSKI:def 1;
hence contradiction by E5,E1,XBOOLE_0:def 3;
end;::now assume
hence thesis;
end;
D12: N2 = SuccNode2(H,N1) by D11,D1,Defchosensucc,D8;
D13:H in the LTLnew of N1 & H is Until by D1,D10,DefSucc01;
LTLNew2 H = {H2} by D1,Def204;
then D13p:the LTLnew of N2
= ((the LTLnew of N1) \ {H})
\/ ({H2} \ the LTLold of N1) by D12,D13,Def207;
D14:CastNode(L.(len(L)),v) = nextnode by C8,defCastNode01;
the LTLnew of nextnode = {} by C10,Defelementary;
then the LTLnew of CastNode(L.m1,v)
c= the LTLold of CastNode(L.(len(L)),v)
by D14,C9,D801,C4,ThSucc10;
then D16:the LTLnew of N2 c= the LTLold of nextnode
by D5p,D14,defCastNode01;
the LTLold of CastNode(L.m,v)
c= the LTLold of CastNode(L.len(L),v) by D501,C4,C9,ThSucc07;
then D17:the LTLold of N1
c= the LTLold of nextnode by D5p,D14,defCastNode01;
now per cases;
suppose H2 in the LTLold of N1;
hence thesis by D17;
end;
suppose D18:not (H2 in the LTLold of N1);
H2 in {H2} by TARSKI:def 1;
then H2 in {H2} \ the LTLold of N1 by D18,XBOOLE_0:def 5;
then H2 in the LTLnew of N2 by D13p,XBOOLE_0:def 3;
hence thesis by D16;
end;
end;::**cases
hence thesis;
end;
hence thesis by C0;
end;
suppose B2:N is elementary;
C1:the LTLnew of N = the LTLnew of FinalNode v by B2,Defelementary;
chosen_next(w0,v,U,s)= N by C1,A1,Defchosennext;
then s1 = CastNode(N,v) by Defchosenrun
.= N by defCastNode01;
hence thesis;
end;
end;::**cases
hence thesis;
end;
hence thesis;
end;
theorem thBA07:
w |= v implies w is-accepted-by BAutomaton(v)
proof
assume A0:w |= v;
set B = BAutomaton(v);
set LS = LTLStates(v);
set LT = Tran_LTL(v);
set IS = InitS_LTL(v);
set FS = FinalS_LTL(v);
ex run be sequence of LS st
run.0 in IS
&
for n holds
[[run.n,CastSeq(w,AtomicFamily).n],run.(n+1)] in LT
&
for FSet being set st FSet in FS holds
{k where k is Element of NAT:run.k in FSet} is infinite set
proof
consider chf being Choice_Function of BOOL Subformulae v;
deffunc R(set) = chosen_run(w,v,chf).k_nat($1);
A2:for x st x in NAT holds R(x) in LS;
ex run being Function of NAT,LS st for x st x in NAT holds run.x = R(x)
from FUNCT_2:sch 2(A2);
then consider run being sequence of LS such that
A3:for x st x in NAT holds run.x = R(x);
A4:for n holds run.n = chosen_run(w,v,chf).n
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 13;
run.n = R(n) by A3;
hence thesis by MODELC_1:def 2;
end;
deffunc Run(Nat) = CastNode(run.$1,v);
A501:for n holds
run.n is elementary strict LTLnode over v &
Run(n) is elementary strict LTLnode over v
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 13;
set Rn = Run(n);
run.n in LS;
then consider N being Element of LTLNodes(v) such that
B1:N = run.n &
N is elementary strict LTLnode over v;
reconsider N as elementary strict LTLnode over v by B1;
the LTLnew of Rn = the LTLnew of N by defCastNode01,B1
.= {} by Defelementary;
hence thesis by Defelementary,B1;
end;
A5:for n holds Run(n+1) is_next_of Run(n) &
Shift(w,n) |= * Run(n+1)
proof
let n;
set n1=n+1;
set w1 = Shift(w,n);
set Rn = Run(n);
reconsider Rn as elementary strict LTLnode over v by A501;
B101:run.n = chosen_run(w,v,chf).n by A4;
B1:Run(n) = CastNode(chosen_run(w,v,chf).n,v) by A4;
B2:Run(n1) = CastNode(chosen_run(w,v,chf).n1,v) by A4;
B3:Run(n+1) is_next_of Rn &
w1 |= * ('X' Rn) by A0,thBA05,B1,B2;
run.n1 = chosen_run(w,v,chf).n1 by A4
.= chosen_next(w1,v,chf,Rn) by Defchosenrun,B101;
then Run(n1) = chosen_next(w1,v,chf,Rn) by defCastNode01;
hence thesis by B3,thChoicedNext01;
end;
A6:for n,H holds
H in the LTLold of Run(n+1) &
H is Until &
Shift(w,n)|=the_right_argument_of H
implies
the_right_argument_of H in the LTLold of Run(n+1)
proof
let n;
let H;
set n1 =n+1;
Run(n1) = CastNode(chosen_run(w,v,chf).n1,v) by A4;
hence thesis by A0,thBA06;
end;
A7:run.0 in IS
proof
run.0 = chosen_run(w,v,chf).0 by A4
.= init v by Defchosenrun;
hence thesis by TARSKI:def 1;
end;
A8:for n holds
CastSeq(w,AtomicFamily).n in Label_(Run(n+1))
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 13;
set Rn = Run(n);
set Rn1 = Run(n+1);
set w1= Shift(w,n);
set X = CastSeq(w,AtomicFamily).n;
reconsider X as Subset of atomic_LTL;
B0:X = (CastSeq(w1,AtomicFamily)).0
proof
CastSeq(w1,AtomicFamily)
= Shift(CastSeq(w,AtomicFamily),n) by MODELC_2:81;
then CastSeq(w1,AtomicFamily).0
= CastSeq(w,AtomicFamily).(0+n) by MODELC_2:def 43;
hence thesis;
end;
B4:Rn1 is_next_of Rn & w1 |= * Rn1 by A5;
B5:atomic_LTL(Rn1) c= X
proof
atomic_LTL(Rn1) c= X
proof
let a; assume a in atomic_LTL(Rn1);
then consider x being LTL-formula such that
D1:x = a & x is atomic & x in the LTLold of Rn1;
x in * Rn1 by D1,LemSUM01;
then w1 |= x by B4,MODELC_2:def 66;
hence a in X by B0,D1,MODELC_2:63;
end;
hence thesis;
end;
Neg_atomic_LTL(Rn1) misses X
proof
now assume not Neg_atomic_LTL(Rn1) misses X;
then Neg_atomic_LTL(Rn1) /\ X <> {} by XBOOLE_0:def 7;
then consider a such that D1:a in Neg_atomic_LTL(Rn1) /\ X
by XBOOLE_0:def 1;
D2:a in Neg_atomic_LTL(Rn1) & a in X by D1,XBOOLE_0:def 4;
then consider x being LTL-formula such that
D3:x = a & x is atomic &
('not' x) in the LTLold of Rn1;
('not' x) in * Rn1 by D3,LemSUM01;
then w1 |= ('not' x) by B4,MODELC_2:def 66;
then w1 |/= x by MODELC_2:64;
hence contradiction by B0,D2,D3,MODELC_2:63;
end;::**now assume
hence thesis;
end;
hence thesis by B5;
end;
A9:for n holds
[[run.n,CastSeq(w,AtomicFamily).n],run.(n+1)] in LT
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 13;
set n1=n+1;
set r = run.n;
set r1 = run.n1;
set R = Run(n);
set R1 = Run(n1);
set gA = CastSeq(w,AtomicFamily).n;
set y = [[r, gA], r1];
[r, gA] in [: LS, AtomicFamily :] by ZFMISC_1:106;
then [[r, gA],r1] in [:[: LS, AtomicFamily :],LS:] by ZFMISC_1:106;
then B2:y is Element of [: LS, AtomicFamily, LS:] by ZFMISC_1:def 3;
reconsider r as elementary strict LTLnode over v by A501;
reconsider r1 as elementary strict LTLnode over v by A501;
reconsider R as elementary strict LTLnode over v by A501;
reconsider R1 as elementary strict LTLnode over v by A501;
B3:R = r by defCastNode01;
B4:R1 = r1 by defCastNode01;
R1 is_next_of R & gA in Label_(R1) by A5,A8;
hence thesis by B2,B3,B4;
end;
for FSet be set st FSet in FS holds
{k where k is Element of NAT:run.k in FSet} is infinite set
proof
let FSet be set;
assume FSet in FS;
then consider x being Element of bool LS such that
B1:FSet = x &
ex F st (F is_subformula_of v & F is Until &
x= FinalS_LTL(F,v));
consider F such that
B2:F is_subformula_of v & F is Until &
x= FinalS_LTL(F,v) by B1;
set F1 = the_left_argument_of F;
set F2 = the_right_argument_of F;
B301:F = F1 'U' F2 by B2,MODELC_2:8;
set FK = {k where k is Element of NAT:run.k in FSet};
now assume not (FK is infinite set);
then consider L such that C2: FK = rng L by FINSEQ_1:73;
ex m st for k st m<=k holds not k in FK
proof
D0:len L = 0 or 0< 0+len L;
now per cases by D0,NAT_1:19;
suppose D1: 1<=len L;
set LEN = len L;
FK c= REAL
proof
FK c= REAL
proof
let a; assume a in FK;
then consider k being Element of NAT
such that EA1:a=k & run.k in FSet;
thus a in REAL by EA1;
end;
hence thesis;
end;
then reconsider L as FinSequence of REAL by C2,FINSEQ_1:def 4;
set realMAX = max L;
set iMAX = [/ realMAX \];
set natMAX = iMAX +1;
0<=realMAX
proof
set b = L.LEN;
LEN in Seg (len L) by D1,FINSEQ_1:3;
then EA0:LEN in dom L by FINSEQ_1:def 3;
b in rng L by EA0,FUNCT_1:12;
then consider k being Element of NAT
such that EA2:k=b & run.k in FSet by C2;
thus thesis by D1,EA2,RFINSEQ2:1;
end;
then reconsider iMAX as Nat by INT_1:80;
iMAX +1 is Nat;
then reconsider natMAX as Nat;
for k st natMAX<=k holds not k in FK
proof
let k;
assume EA1:natMAX <= k;
now assume k in FK;
then consider i1 being set such that
EA2:i1 in dom L & k = L.i1 by C2,FUNCT_1:def 5;
reconsider i1 as Element of NAT by EA2;
i1 in Seg LEN by EA2,FINSEQ_1:def 3;
then 1<=i1 & i1<=LEN & k = L.i1 by EA2,FINSEQ_1:3;
then k <= realMAX by RFINSEQ2:1;
hence contradiction by EA1,INT_1:57,XXREAL_0:2;
end;::**now assume
hence thesis;
end;
hence thesis;
end;
suppose len L=0; then
L = {};
then for k st 0<=k holds not k in FK by C2;
hence thesis;
end;
end;::**cases
hence thesis;
end;
then consider m such that
C3:for k st m<=k holds not k in FK;
C4: for k st m<=k holds
F in the LTLold of Run(k) &
not F2 in the LTLold of Run(k)
proof
let k;
assume m<=k;
then D1:not k in FK by C3;
reconsider k as Element of NAT by ORDINAL1:def 13;
set r = run.k;
reconsider r as elementary strict LTLnode over v by A501;
now assume not (F in the LTLold of CastNode(r,v) &
not F2 in the LTLold of CastNode(r,v));
then r in FSet by B1,B2;
hence contradiction by D1;
end;::**now assume;
hence thesis;
end;
set m1=m+1;
m<=m1 by NAT_1:11;
then C5:F in the LTLold of Run(m1) &
not F2 in the LTLold of Run(m1) by C4;
C6:F in * Run(m1) by C5,LemSUM01;
set w1 = Shift(w,m);
w1 |= * Run(m1) by A5;
then w1 |= F by C6,MODELC_2:def 66;
then consider h such that
C8:(for j being Nat st j