:: 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