:: Model Checking, Part {III}
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received August 19, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, MODELC_2, SUBSET_1, ZF_LANG,
FUNCT_1, RELAT_1, XXREAL_0, INT_1, ARYTM_3, ARYTM_1, CARD_1, STRUCT_0,
TARSKI, XBOOLEAN, LATTICES, CAT_3, ORDINAL4, ZF_MODEL, MODELC_1,
FINSET_1, SEQ_1, REAL_1, CARD_3, SERIES_1, ZFMISC_1, MSUALG_3, ORDERS_1,
SUBSTUT1, FSM_1, FSM_2, VALUED_1, MODELC_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, CARD_1,
NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, RELAT_1, FUNCT_1, RELSET_1,
FINSEQ_1, ORDERS_1, FUNCT_2, INT_1, NAT_1, SEQ_1, SERIES_1, PARTFUN1,
STRUCT_0, MODELC_1, MODELC_2, RFINSEQ2;
constructors KNASTER, MODELC_2, SERIES_1, REAL_1, NEWTON, RFINSEQ2, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0,
XREAL_0, NAT_1, INT_1, ORDERS_1, FINSET_1, MODELC_2, FINSEQ_1, NUMBERS,
VALUED_0, CARD_1, RELSET_1, FUNCT_2;
requirements REAL, NUMERALS, ARITHM, SUBSET, BOOLE;
definitions TARSKI;
equalities MODELC_2, SERIES_1;
expansions TARSKI, MODELC_2;
theorems XBOOLE_0, ZFMISC_1, XBOOLE_1, TARSKI, FUNCT_1, FUNCT_2, FUNCT_7,
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, XTUPLE_0, XREAL_0,
NUMBERS;
schemes NAT_1, FUNCT_2, MODELC_2, TARSKI, FUNCT_1, FINSEQ_1, RECDEF_1;
begin
reserve k,n,n1,m,m1,m0,h,i,j for Nat,
a,x,y,X,X1,X2,X3,X4,Y for set;
reserve 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;
Lm1: 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;
Lm2: 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;
Lm3: (<* H *>).1 = H & rng <* H *> = {H}
proof
set p = <* H *>;
dom p = {1} & p.1= H by FINSEQ_1:2,def 8;
hence thesis by FUNCT_1:4;
end;
Lm4: for r1,r2 being Real holds r1<=r2 implies [\ r1 /] <= [\ r2 /]
proof
let r1,r2 be Real;
r1<=r2 implies [\ r1 /] <= [\ r2 /]
proof
assume
A1: r1<=r2;
now
assume [\ r2 /] < [\ r1 /];
then
A2: [\ r2 /] +1 <= [\ r1 /] by INT_1:7;
[\ r1 /] <= r1 by INT_1:def 6;
then [\ r2 /] +1 <= r1 by A2,XXREAL_0:2;
hence contradiction by A1,INT_1:29,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis;
end;
Lm5: for r1,r2 being Real holds r1<=r2-1 implies [\ r1 /] <= [\ r2 /]-1
proof
let r1,r2 be Real;
r1<=r2-1 implies [\ r1 /] <= [\ r2 /]-1
proof
assume r1<=r2-1;
then r1+1<=r2-1 +1 by XREAL_1:6;
then [\ r1+1 /] <= [\ r2 /] by Lm4;
then [\ r1 /] +1 <= [\ r2 /] by INT_1:28;
then [\ r1 /]+1 -1 <= [\ r2 /] -1 by XREAL_1:9;
hence thesis;
end;
hence thesis;
end;
Lm6: n=0 or 1<=n
proof
n=0 or 0<0+n;
hence thesis by NAT_1:19;
end;
Lm7: (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;
end;
Lm8: (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
A1: H is conjunctive or H is disjunctive or H is Until or H is Release;
then G2 is_immediate_constituent_of H by MODELC_2:22,23,24,25;
then
A2: G2 is_proper_subformula_of H by MODELC_2:29;
G1 is_immediate_constituent_of H by A1,MODELC_2:22,23,24,25;
then G1 is_proper_subformula_of H by MODELC_2:29;
hence thesis by A2;
end;
Lm9: F is_subformula_of H implies {F} is Subset of Subformulae H
by MODELC_2:45,SUBSET_1:41;
Lm10: 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:34;
end;
Lm11: 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 Lm8;
hence thesis by Lm10;
end;
Lm12: 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 Lm8;
hence thesis by Lm9;
end;
Lm13: {H} is Subset of Subformulae H by Lm9;
Lm14: 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 Lm7;
hence thesis by Lm9;
end;
definition
let F;
redefine func Subformulae F -> Subset of LTL_WFF; :: redefines Subformulae (MODELC_2, definition)
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
:Def1:
{
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 Lm11,Lm12,MODELC_2:78,SUBSET_1:1;
func LTLNew2 H -> Subset of Subformulae H equals
:Def2:
{} 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 Lm11,Lm12,MODELC_2:78,SUBSET_1:1;
func LTLNext H -> Subset of Subformulae H equals
:Def3:
{} 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 Lm13,Lm14,MODELC_2:78,SUBSET_1:1;
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
:Def4:
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 NextD = (the LTLnext of N) \/ LTLNext H;
set NewB=LTLNew1 H \ the LTLold of N;
set NewA= (the LTLnew of N) \ {H};
set Old= (the LTLold of N) \/ {H};
set NewC = NewA \/ NewB;
{H} c= Subformulae v by A1,ZFMISC_1:31;
then reconsider Old as Subset of Subformulae v by XBOOLE_1:8;
ex F st H=F & F is_subformula_of v by A1,MODELC_2:def 24;
then
A2: Subformulae H c= Subformulae v by MODELC_2:46;
then NewB c= Subformulae v;
then reconsider NewC as Subset of Subformulae v by XBOOLE_1:8;
LTLNext H c= Subformulae v by A2;
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;
func SuccNode2(H,N) -> strict LTLnode over v means
:Def5:
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 NextD = the LTLnext of N;
set NewB=LTLNew2 H \ the LTLold of N;
set NewA= (the LTLnew of N) \ {H};
set Old= (the LTLold of N) \/ {H};
set NewC = NewA \/ NewB;
{H} c= Subformulae v by A1,ZFMISC_1:31;
then reconsider Old as Subset of Subformulae v by XBOOLE_1:8;
ex F st H=F & F is_subformula_of v by A1,MODELC_2:def 24;
then Subformulae H c= Subformulae v by MODELC_2:46;
then NewB c= Subformulae v;
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
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
ex H st H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
pred N2 is_succ2_of N1 means
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
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
:Def11:
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:1;
end;
definition
let v;
func Seed v -> Subset of Subformulae v equals
{v};
correctness by Lm9;
end;
registration
let v;
cluster elementary strict for LTLnode over v;
existence
proof
set X = LTLnode(# {}v,{}v,{}v #);
take X;
thus thesis;
end;
end;
definition
let v;
func FinalNode v -> elementary strict LTLnode over v equals
LTLnode(# {}v,{}v,{}v #);
correctness by Def11;
end;
definition
let x be object; let v;
func CastNode(x,v) -> strict LTLnode over v equals
:Def16:
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 Def11;
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,N10,N20,M for strict LTLnode over v;
reserve w for Element of Inf_seq(AtomicFamily);
definition
let v, L;
pred L is_Finseq_for v means
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;
Lm15: 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 and
A3: m<=len(L);
A4: m-1<=len(L)-0 by A3,XREAL_1:13;
set m1=m-1;
reconsider m1 as Nat by A2,NAT_1:21;
set L1=L|Seg m1;
reconsider L1 as FinSequence by FINSEQ_1:15;
consider L2 being FinSequence such that
A5: L = L1^L2 by FINSEQ_1:80;
len(L)=len(L1)+len(L2) by A5,FINSEQ_1:22;
then
A6: len(L2) = len(L)-len(L1) .= len(L)-m1 by A4,FINSEQ_1:17;
m-m<=len(L)-m by A3,XREAL_1:9;
then
A7: 0+1<=(len(L)-m)+1 by XREAL_1:6;
then 1 in dom L2 by A6,FINSEQ_3:25;
then
A8: L2.1 = L.(len(L1) + 1) by A5,FINSEQ_1:def 7
.= L.(m1+1) by A4,FINSEQ_1:17
.=L.m;
A9: len(L1) = m1 by A4,FINSEQ_1:17;
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
A10: 1 <= k & k < len(L2);
set k1=k+1;
1<=k1 & k1<=len(L2) by A10,NAT_1:13;
then
A11: k1 in dom L2 by FINSEQ_3:25;
set km1=k+m1;
1+0<= k+m1 & km1 <(len(L)-m1) +m1 by A6,A10,XREAL_1:6,7;
then consider N,M such that
A12: N = L.km1 and
A13: M=L.(km1+1) and
A14: M is_succ_of N by A1;
A15: M = L.(m1+k1) by A13
.= L2.(k1) by A9,A5,A11,FINSEQ_1:def 7;
k in dom L2 by A10,FINSEQ_3:25;
then N = L2.k by A9,A5,A12,FINSEQ_1:def 7;
hence thesis by A14,A15;
end;
then
A16: L2 is_Finseq_for v;
len(L2) in dom L2 by A7,A6,FINSEQ_3:25;
then L2.(len(L2)) =L.(len(L1)+len(L2)) by A5,FINSEQ_1:def 7
.= L.(len(L)) by A5,FINSEQ_1:22;
hence thesis by A7,A5,A6,A8,A16;
end;
definition
let v, N1,N2;
pred N2 is_next_of N1 means
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 S2= the LTLnew of N;
set S1= the LTLold of N;
S1 is Subset of LTL_WFF & S2 is Subset of LTL_WFF by MODELC_2:47;
then S1 \/ S2 c= LTL_WFF by XBOOLE_1:8;
hence thesis by XBOOLE_1:8;
end;
end;
Lm16: 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 that
A1: H in the LTLnew of N and
A2: H is atomic or H is negative;
A3: ( not H is next)& not H is Until by A2,MODELC_2:78;
set NX = the LTLnext of N;
set N1X = the LTLnext of N1;
A4: N1X = NX \/ LTLNext H by A1,Def4;
set NN = the LTLnew of N;
set N1N = the LTLnew of N1;
set NO = the LTLold of N;
set N1O = the LTLold of N1;
A5: N1O = NO \/ {H} by A1,Def4;
A6: not H is Release by A2,MODELC_2:78;
A7: ( not H is conjunctive)& not H is disjunctive by A2,MODELC_2:78;
then
A8: LTLNew1 H ={} by A3,A6,Def1;
A9: N1N = (NN \ {H}) \/ (LTLNew1 H \ NO) by A1,Def4;
A10: for a being object holds a in N1O \/ N1N implies a in NO \/ NN
proof let a be object;
assume
A11: a in N1O \/ N1N;
a in N1O implies a in NO or a in {H} by A5,XBOOLE_0:def 3;
then
A12: 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 A8,A9,XBOOLE_0:def 5;
hence thesis by A11,A12,XBOOLE_0:def 3;
end;
A13: for a being object holds a in NO \/ NN implies a in N1O \/ N1N
proof let a be object;
assume
A14: a in NO \/ NN;
a in NN implies not a in {H} & a in NN or a in {H} & a in NN;
then
A15: a in NN implies a in NN \ {H} or a in NO \/{H} by XBOOLE_0:def 3,def 5;
a in NO implies a in N1O by A5,XBOOLE_0:def 3;
hence thesis by A8,A5,A9,A14,A15,XBOOLE_0:def 3;
end;
LTLNext H = {} by A7,A3,A6,Def3;
hence thesis by A4,A10,A13,TARSKI:2;
end;
Lm17: 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 NX = the LTLnext of N;
set NN = the LTLnew of N;
set NO = the LTLold of N;
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 XNX = 'X' CastLTL(NX);
A3: H in *N by A1,Lm1;
A4: w |= *N implies w |= *SN
proof
assume
A5: w |= *N;
then
A6: w |= H by A3;
for F being LTL-formula st F in *SN holds w|= F
proof
let F be LTL-formula such that
A7: F in *SN;
now
per cases by A7,Lm1;
suppose
F in SNO;
then
A8: F in NO \/ {H} by A1,Def4;
now
per cases by A8,XBOOLE_0:def 3;
suppose
F in NO;
then F in *N by Lm1;
hence thesis by A5;
end;
suppose
F in {H};
then F in *N by A3,TARSKI:def 1;
hence thesis by A5;
end;
end;
hence thesis;
end;
suppose
F in SNN;
then
A9: F in (NN \ {H})\/ (LTLNew1 H \ NO) by A1,Def4;
now
per cases by A9,Lm2;
suppose
F in NN;
then F in (NO \/ NN) \/ XNX by Lm1;
hence thesis by A5;
end;
suppose
A10: F in (LTLNew1 H);
now
per cases by A2;
suppose
A11: H is conjunctive;
then
F in {the_left_argument_of H, the_right_argument_of H }
by A10,Def1;
then
A12: 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 A11,MODELC_2:6;
hence thesis by A6,A12,MODELC_2:65;
end;
suppose
H is next;
hence thesis by A10,Def1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A13: F in XSNX;
set SN1 = CastLTL(SNX);
consider G such that
A14: F=G and
A15: ex G1 st G1 in SN1 & G ='X' G1 by A13;
consider G1 such that
A16: G1 in SN1 and
A17: G ='X' G1 by A15;
A18: SN1 = NX \/ LTLNext H by A1,Def4;
now
per cases by A18,A16,XBOOLE_0:def 3;
suppose
G1 in NX;
then F in XNX by A14,A17;
then F in (NO \/ NN) \/ XNX by Lm1;
hence thesis by A5;
end;
suppose
A19: G1 in LTLNext H;
now
per cases by A2;
suppose
A20: H is next;
then G1 in {the_argument_of H} by A19,Def3;
then G1 = the_argument_of H by TARSKI:def 1;
hence thesis by A6,A14,A17,A20,MODELC_2:5;
end;
suppose
H is conjunctive;
hence thesis by A19,Def3;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
w |= *SN implies w |= *N
proof
assume
A21: w |= *SN;
for F being LTL-formula st F in *N holds w|= F
proof
let F be LTL-formula such that
A22: F in *N;
now
per cases by A22,Lm1;
suppose
F in NO;
then F in NO \/ {H} by XBOOLE_0:def 3;
then F in SNO by A1,Def4;
then F in *SN by Lm1;
hence thesis by A21;
end;
suppose
A23: 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 A1,Def4;
then F in *SN by Lm1;
hence thesis by A21;
end;
suppose
not F=H;
then not F in {H} by TARSKI:def 1;
then F in NN \ {H} by A23,XBOOLE_0:def 5;
then F in (NN \ {H}) \/(LTLNew1 H \ NO) by XBOOLE_0:def 3;
then F in SNN by A1,Def4;
then F in *SN by Lm1;
hence thesis by A21;
end;
end;
hence thesis;
end;
suppose
A24: F in XNX;
set SN11= (NX) \/ LTLNext H;
SNX = SN11 by A1,Def4;
then reconsider SN11 as Subset of Subformulae v;
set SN1 =CastLTL(SN11);
set N1 = CastLTL(NX);
consider G such that
A25: F=G and
A26: ex G1 st G1 in N1 & G ='X' G1 by A24;
consider G1 such that
A27: G1 in N1 and
A28: G ='X' G1 by A26;
G1 in SN11 by A27,XBOOLE_0:def 3;
then F in 'X' SN1 by A25,A28;
then F in XSNX by A1,Def4;
then F in *SN by Lm1;
hence thesis by A21;
end;
end;
hence thesis;
end;
hence thesis;
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 Lm16
,Lm17;
Lm18: 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 NN = the LTLnew of N;
set NO = the LTLold of N;
set SN2=SuccNode2(H,N);
set NX = the LTLnext of N;
set SN1=SuccNode1(H,N);
A3: H in *N by A1,Lm1;
set SN1X = the LTLnext of SN1;
LTLNext H = {} by A2,Def3;
then
A4: SN1X = NX \/ {} by A1,Def4
.= NX;
set H1 = the_left_argument_of H;
set XSN1X = 'X' CastLTL(SN1X);
set SN1N = the LTLnew of SN1;
set SN1O = the LTLold of SN1;
A5: SN1O = NO \/ {H} by A1,Def4;
LTLNew1 H = {H1} by A2,Def1;
then
A6: SN1N = (NN \ {H}) \/ ({H1} \ NO) by A1,Def4;
A7: F in *SN1 implies F in *N or F=H1
proof
assume
A8: F in *SN1;
now
per cases by A8,Lm1;
suppose
F in SN1O;
then F in NO or F in {H} by A5,XBOOLE_0:def 3;
hence thesis by A3,Lm1,TARSKI:def 1;
end;
suppose
F in SN1N;
then F in (NN \ {H}) or F in ({H1} \ NO) by A6,XBOOLE_0:def 3;
then F in NN or F in {H1} by XBOOLE_0:def 5;
hence thesis by Lm1,TARSKI:def 1;
end;
suppose
F in XSN1X;
hence thesis by A4,Lm1;
end;
end;
hence thesis;
end;
set XNX = 'X' CastLTL(NX);
set SN2X = the LTLnext of SN2;
set XSN2X = 'X' CastLTL(SN2X);
set SN2O = the LTLold of SN2;
A9: SN2O = NO \/ {H} by A1,Def5;
set H2 = the_right_argument_of H;
set SN2N = the LTLnew of SN2;
LTLNew2 H = {H2} by A2,Def2;
then
A10: SN2N = (NN \ {H}) \/ ({H2} \ NO) by A1,Def5;
A11: SN2X = NX by A1,Def5;
A12: F in *SN2 implies F in *N or F=H2
proof
assume
A13: F in *SN2;
now
per cases by A13,Lm1;
suppose
F in SN2O;
then F in NO or F in {H} by A9,XBOOLE_0:def 3;
hence thesis by A3,Lm1,TARSKI:def 1;
end;
suppose
F in SN2N;
then F in (NN \ {H}) or F in ({H2} \ NO) by A10,XBOOLE_0:def 3;
then F in NN or F in {H2} by XBOOLE_0:def 5;
hence thesis by Lm1,TARSKI:def 1;
end;
suppose
F in XSN2X;
hence thesis by A11,Lm1;
end;
end;
hence thesis;
end;
H = H1 'or' H2 by A2,MODELC_2:7;
then
A14: w|= H iff w|= H1 or w|= H2 by MODELC_2:66;
A15: w |= *N implies (w |= *SN1 or w |= *SN2)
proof
assume
A16: w |= *N;
now
per cases by A3,A14,A16;
suppose
A17: w|= H1;
F in *SN1 implies w|= F
by A7,A16,A17;
hence thesis;
end;
suppose
A18: w|= H2;
F in *SN2 implies w|= F
by A12,A16,A18;
hence thesis;
end;
end;
hence thesis;
end;
A19: F in *N implies F in *SN1 & F in *SN2
proof
assume
A20: F in *N;
now
per cases by A20,Lm1;
suppose
F in NO;
then F in SN1O & F in SN2O by A5,A9,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
suppose
A21: 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 A5,A9,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
suppose
not F=H;
then not F in {H} by TARSKI:def 1;
then F in (NN \ {H}) by A21,XBOOLE_0:def 5;
then F in SN1N & F in SN2N by A6,A10,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
end;
hence thesis;
end;
suppose
A22: F in XNX;
then F in XSN2X by A1,Def5;
hence thesis by A4,A22,Lm1;
end;
end;
hence thesis;
end;
(w |= *SN1 or w |= *SN2) implies w |= *N
proof
assume
A23: w |= *SN1 or w |= *SN2;
F in *N implies w |= F
proof
assume
A24: F in *N;
then
A25: F in *SN2 by A19;
A26: F in *SN1 by A19,A24;
now
per cases by A23;
suppose
w |= *SN1;
hence thesis by A26;
end;
suppose
w |= *SN2;
hence thesis by A25;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A15;
end;
Lm19: 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 NX = the LTLnext of N;
set SN1=SuccNode1(H,N);
A3: H in *N by A1,Lm1;
set SN1X = the LTLnext of SN1;
LTLNext H = {H} by A2,Def3;
then
A4: SN1X = NX \/ {H} by A1,Def4;
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SN2=SuccNode2(H,N);
set H2 = the_right_argument_of H;
set SN2N = the LTLnew of SN2;
LTLNew2 H = {H2} by A2,Def2;
then
A5: SN2N = (NN \ {H}) \/ ({H2} \ NO) by A1,Def5;
set H1 = the_left_argument_of H;
set XNX = 'X' CastLTL(NX);
set XSN1X = 'X' CastLTL(SN1X);
set SN1N = the LTLnew of SN1;
set SN1O = the LTLold of SN1;
A6: SN1O = NO \/ {H} by A1,Def4;
LTLNew1 H = {H1} by A2,Def1;
then
A7: SN1N = (NN \ {H}) \/ ({H1} \ NO) by A1,Def4;
A8: F in *SN1 implies F in *N or F=H1 or F='X' H
proof
assume
A9: F in *SN1;
now
per cases by A9,Lm1;
suppose
F in SN1O;
then F in NO or F in {H} by A6,XBOOLE_0:def 3;
hence thesis by A3,Lm1,TARSKI:def 1;
end;
suppose
F in SN1N;
then F in (NN \ {H}) or F in ({H1} \ NO) by A7,XBOOLE_0:def 3;
then F in NN or F in {H1} by XBOOLE_0:def 5;
hence thesis by Lm1,TARSKI:def 1;
end;
suppose
F in XSN1X;
then consider G such that
A10: F=G and
A11: ex G1 st G1 in CastLTL(SN1X) & G ='X' G1;
consider G1 such that
A12: G1 in SN1X and
A13: G ='X' G1 by A11;
A14: G1 in NX or G1 in {H} by A4,A12,XBOOLE_0:def 3;
now
per cases by A14,TARSKI:def 1;
suppose
G1 in NX;
then F in XNX by A10,A13;
hence thesis by Lm1;
end;
suppose
G1=H;
hence thesis by A10,A13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
set SN2X = the LTLnext of SN2;
set XSN2X = 'X' CastLTL(SN2X);
set SN2O = the LTLold of SN2;
A15: SN2O = NO \/ {H} by A1,Def5;
A16: SN2X = NX by A1,Def5;
A17: F in *SN2 implies F in *N or F=H2
proof
assume
A18: F in *SN2;
now
per cases by A18,Lm1;
suppose
F in SN2O;
then F in NO or F in {H} by A15,XBOOLE_0:def 3;
hence thesis by A3,Lm1,TARSKI:def 1;
end;
suppose
F in SN2N;
then F in (NN \ {H}) or F in ({H2} \ NO) by A5,XBOOLE_0:def 3;
then F in NN or F in {H2} by XBOOLE_0:def 5;
hence thesis by Lm1,TARSKI:def 1;
end;
suppose
F in XSN2X;
hence thesis by A16,Lm1;
end;
end;
hence thesis;
end;
H = H1 'U' H2 by A2,MODELC_2:8;
then w|= H iff w|=H2 'or' (H1 '&' ('X' H)) by MODELC_2:75;
then
A19: w|= H iff w|=H2 or w |= (H1 '&' ('X' H)) by MODELC_2:66;
A20: w |= *N implies (w |= *SN1 or w |= *SN2)
proof
assume
A21: w |= *N;
now
per cases by A3,A19,A21,MODELC_2:65;
suppose
A22: w|=H1 & w|='X' H;
F in *SN1 implies w|= F
by A8,A21,A22;
hence thesis;
end;
suppose
A23: w|= H2;
F in *SN2 implies w|= F
by A17,A21,A23;
hence thesis;
end;
end;
hence thesis;
end;
A24: F in *N implies F in *SN1 & F in *SN2
proof
assume
A25: F in *N;
now
per cases by A25,Lm1;
suppose
F in NO;
then F in SN1O & F in SN2O by A6,A15,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
suppose
A26: 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 A6,A15,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
suppose
F <> H;
then not F in {H} by TARSKI:def 1;
then F in (NN \ {H}) by A26,XBOOLE_0:def 5;
then F in SN1N & F in SN2N by A7,A5,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
end;
hence thesis;
end;
suppose
F in XNX;
then consider G such that
A27: F=G and
A28: ex G1 st G1 in CastLTL(NX) & G ='X' G1;
consider G1 such that
A29: G1 in NX and
A30: G ='X' G1 by A28;
G1 in SN1X by A4,A29,XBOOLE_0:def 3;
then
A31: F in XSN1X by A27,A30;
F in XSN2X by A16,A27,A29,A30;
hence thesis by A31,Lm1;
end;
end;
hence thesis;
end;
(w |= *SN1 or w |= *SN2) implies w |= *N
proof
assume
A32: w |= *SN1 or w |= *SN2;
F in *N implies w |= F
proof
assume
A33: F in *N;
then
A34: F in *SN2 by A24;
A35: F in *SN1 by A24,A33;
now
per cases by A32;
suppose
w |= *SN1;
hence thesis by A35;
end;
suppose
w |= *SN2;
hence thesis by A34;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A20;
end;
Lm20: 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 NX = the LTLnext of N;
set SN1=SuccNode1(H,N);
A3: H in *N by A1,Lm1;
set SN1X = the LTLnext of SN1;
LTLNext H = {H} by A2,Def3;
then
A4: SN1X = NX \/ {H} by A1,Def4;
set H2 = the_right_argument_of H;
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SN2=SuccNode2(H,N);
set H1 = the_left_argument_of H;
set SN2N = the LTLnew of SN2;
LTLNew2 H = {H1,H2} by A2,Def2;
then
A5: SN2N = (NN \ {H}) \/ ({H1,H2} \ NO) by A1,Def5;
set XNX = 'X' CastLTL(NX);
set XSN1X = 'X' CastLTL(SN1X);
set SN1N = the LTLnew of SN1;
set SN1O = the LTLold of SN1;
A6: SN1O = NO \/ {H} by A1,Def4;
LTLNew1 H = {H2} by A2,Def1;
then
A7: SN1N = (NN \ {H}) \/ ({H2} \ NO) by A1,Def4;
A8: F in *SN1 implies F in *N or F=H2 or F='X' H
proof
assume
A9: F in *SN1;
now
per cases by A9,Lm1;
suppose
F in SN1O;
then F in NO or F in {H} by A6,XBOOLE_0:def 3;
hence thesis by A3,Lm1,TARSKI:def 1;
end;
suppose
F in SN1N;
then F in (NN \ {H}) or F in ({H2} \ NO) by A7,XBOOLE_0:def 3;
then F in NN or F in {H2} by XBOOLE_0:def 5;
hence thesis by Lm1,TARSKI:def 1;
end;
suppose
F in XSN1X;
then consider G such that
A10: F=G and
A11: ex G1 st G1 in CastLTL(SN1X) & G ='X' G1;
consider G1 such that
A12: G1 in SN1X and
A13: G ='X' G1 by A11;
A14: G1 in NX or G1 in {H} by A4,A12,XBOOLE_0:def 3;
now
per cases by A14,TARSKI:def 1;
suppose
G1 in NX;
then F in XNX by A10,A13;
hence thesis by Lm1;
end;
suppose
G1=H;
hence thesis by A10,A13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
set SN2X = the LTLnext of SN2;
set XSN2X = 'X' CastLTL(SN2X);
set SN2O = the LTLold of SN2;
A15: SN2O = NO \/ {H} by A1,Def5;
A16: SN2X = NX by A1,Def5;
A17: F in *SN2 implies F in *N or F=H1 or F=H2
proof
assume
A18: F in *SN2;
now
per cases by A18,Lm1;
suppose
F in SN2O;
then F in NO or F in {H} by A15,XBOOLE_0:def 3;
hence thesis by A3,Lm1,TARSKI:def 1;
end;
suppose
F in SN2N;
then F in (NN \ {H}) or F in ({H1,H2} \ NO) by A5,XBOOLE_0:def 3;
then F in NN or F in {H1,H2} by XBOOLE_0:def 5;
hence thesis by Lm1,TARSKI:def 2;
end;
suppose
F in XSN2X;
hence thesis by A16,Lm1;
end;
end;
hence thesis;
end;
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
A19: w|= H iff w|=(H1 '&' H2) or w |= (H2 '&' ('X' H)) by MODELC_2:66;
A20: w |= *N implies (w |= *SN1 or w |= *SN2)
proof
assume
A21: w |= *N;
now
per cases by A3,A19,A21,MODELC_2:65;
suppose
A22: w|=H2 & w|='X' H;
F in *SN1 implies w|= F
by A8,A21,A22;
hence thesis;
end;
suppose
A23: w|=H1 & w|=H2;
F in *SN2 implies w|= F
by A17,A21,A23;
hence thesis;
end;
end;
hence thesis;
end;
A24: F in *N implies F in *SN1 & F in *SN2
proof
assume
A25: F in *N;
now
per cases by A25,Lm1;
suppose
F in NO;
then F in SN1O & F in SN2O by A6,A15,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
suppose
A26: 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 A6,A15,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
suppose
not F=H;
then not F in {H} by TARSKI:def 1;
then F in (NN \ {H}) by A26,XBOOLE_0:def 5;
then F in SN1N & F in SN2N by A7,A5,XBOOLE_0:def 3;
hence thesis by Lm1;
end;
end;
hence thesis;
end;
suppose
F in XNX;
then consider G such that
A27: F=G and
A28: ex G1 st G1 in CastLTL(NX) & G ='X' G1;
consider G1 such that
A29: G1 in NX and
A30: G ='X' G1 by A28;
G1 in SN1X by A4,A29,XBOOLE_0:def 3;
then
A31: F in XSN1X by A27,A30;
F in XSN2X by A16,A27,A29,A30;
hence thesis by A31,Lm1;
end;
end;
hence thesis;
end;
(w |= *SN1 or w |= *SN2) implies w |= *N
proof
assume
A32: w |= *SN1 or w |= *SN2;
F in *N implies w |= F
proof
assume
A33: F in *N;
then
A34: F in *SN2 by A24;
A35: F in *SN1 by A24,A33;
now
per cases by A32;
suppose
w |= *SN1;
hence thesis by A35;
end;
suppose
w |= *SN2;
hence thesis by A34;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A20;
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 Lm18
,Lm19,Lm20;
Lm21: (H is negative or H is next) implies Subformulae H = (Subformulae
the_argument_of H) \/ {H}
proof
set H1 = the_argument_of H;
H in Subformulae H by MODELC_2:45;
then
A1: {H} c= Subformulae H by ZFMISC_1:31;
assume
A2: H is negative or H is next;
then H1 is_immediate_constituent_of H by MODELC_2:20,21;
then H1 is_proper_subformula_of H by MODELC_2:29;
then H1 is_subformula_of H;
then Subformulae H1 c= Subformulae H by MODELC_2:46;
then
A3: Subformulae H1 \/ {H} c= Subformulae H by A1,XBOOLE_1:8;
for x being object holds x in Subformulae H iff x in Subformulae H1 \/ {H}
proof let x be object;
x in Subformulae H implies x in Subformulae H1 \/ {H}
proof
assume x in Subformulae H;
then consider F such that
A4: F = x and
A5: 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 A4,XBOOLE_0:def 3;
end;
suppose
F <> H;
then F is_proper_subformula_of H by A5;
then F is_subformula_of H1 by A2,MODELC_2:37;
then F in Subformulae H1 by MODELC_2:45;
hence thesis by A4,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
Lm22: (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
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);
H in Subformulae H by MODELC_2:def 24;
then
A1: {H} c= Subformulae H by ZFMISC_1:31;
assume
A2: H is conjunctive or H is disjunctive or H is Until or H is Release;
then H2 is_immediate_constituent_of H by MODELC_2:22,23,24,25;
then H2 is_proper_subformula_of H by MODELC_2:29;
then H2 is_subformula_of H;
then
A3: Subformulae H2 c= Subformulae H by MODELC_2:46;
H1 is_immediate_constituent_of H by A2,MODELC_2:22,23,24,25;
then H1 is_proper_subformula_of H by MODELC_2:29;
then H1 is_subformula_of H;
then Subformulae H1 c= Subformulae H by MODELC_2:46;
then SUBF c= Subformulae H by A3,XBOOLE_1:8;
then
A4: SUBF \/ {H} c= Subformulae H by A1,XBOOLE_1:8;
for x being object holds x in Subformulae H iff x in SUBF \/ {H}
proof let x be object;
x in Subformulae H implies x in SUBF \/ {H}
proof
assume x in Subformulae H;
then consider F such that
A5: F = x and
A6: 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 A5,XBOOLE_0:def 3;
end;
suppose
F <> H;
then F is_proper_subformula_of H by A6;
then F is_subformula_of H1 or F is_subformula_of H2 by A2,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 A5,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
Lm23: H is atomic implies Subformulae H ={H}
proof
assume H is atomic;
then ex n st H = atom.n;
then
A1: len H =1 by FINSEQ_1:40;
A2: for x being object holds x in Subformulae H implies x in {H}
proof let x be object;
assume x in Subformulae H;
then consider G such that
A3: G = x and
A4: G is_subformula_of H by MODELC_2:def 24;
now
assume G <> H;
then G is_proper_subformula_of H by A4;
then len G < 1 by A1,MODELC_2:32;
hence contradiction by MODELC_2:3;
end;
hence thesis by A3,TARSKI:def 1;
end;
for x being object holds x in {H} implies x in Subformulae H
proof let x be object;
assume x in {H};
then x = H by TARSKI:def 1;
hence thesis by MODELC_2:45;
end;
hence thesis by A2,TARSKI:2;
end;
Lm24: not {} in W
proof
assume {} in W;
then ex F st F = {} & F is_subformula_of H by MODELC_2:def 24;
hence contradiction by CARD_1:27,MODELC_2:3;
end;
theorem Th3:
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 negative or H is next) & P[the_argument_of H] holds P[H]
proof
let H such that
A2: H is negative or H is next and
A3: P[the_argument_of H];
consider L1 such that
A4: Subformulae the_argument_of H = rng L1 by A3;
set L = L1 ^ <* H *>;
take L;
rng L = rng L1 \/ rng <* H *> by FINSEQ_1:31
.= Subformulae the_argument_of H \/ {H} by A4,Lm3
.= Subformulae H by A2,Lm21;
hence thesis;
end;
A5: 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
A6: H is conjunctive or H is disjunctive or H is Until or H is Release and
A7: P[the_left_argument_of H] and
A8: P[the_right_argument_of H];
consider L1 such that
A9: Subformulae the_left_argument_of H = rng L1 by A7;
consider L2 such that
A10: Subformulae the_right_argument_of H = rng L2 by A8;
A11: rng(L1 ^ L2) = Subformulae the_left_argument_of H \/ Subformulae
the_right_argument_of H by A9,A10,FINSEQ_1:31;
set L = (L1 ^ L2) ^ <* H *>;
take L;
rng L = rng (L1 ^ L2) \/ rng <* H *> by FINSEQ_1:31
.= (Subformulae the_left_argument_of H \/ Subformulae
the_right_argument_of H) \/ {H} by A11,Lm3
.= Subformulae H by A6,Lm22;
hence thesis;
end;
A12: for H st H is atomic holds P[H]
proof
let H such that
A13: H is atomic;
set L =<* H *>;
take L;
rng L = {H} by Lm3
.= Subformulae H by A13,Lm23;
hence thesis;
end;
for H holds P[H] from MODELC_2:sch 1(A12,A1,A5);
hence thesis;
end;
registration
let H;
cluster Subformulae H -> finite;
correctness
proof
ex L st Subformulae H = rng L by Th3;
hence thesis;
end;
end;
definition
let H, W, L, x;
func Length_fun(L,W,x) -> Nat equals
:Def23:
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
:Def24:
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
by ORDINAL1:def 12,NUMBERS:19;
consider IT being sequence of REAL such that
A2: for x st x in NAT holds IT.x = F(x) from FUNCT_2:sch 11(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;
A3: k in NAT by ORDINAL1:def 12;
A4: not L.k in W implies IT.k=0
proof
assume
A5: not L.k in W;
IT.k = Length_fun(L,W,k) by A2,A3;
hence thesis by A5,Def23;
end;
L.k in W implies IT.k = len CastLTL(L.k)
proof
assume
A6: L.k in W;
IT.k = Length_fun(L,W,k) by A2,A3;
hence thesis by A6,Def23;
end;
hence thesis by A4;
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
A7: for k holds (L.k in W implies R1.k = len CastLTL(L.k)) & (not L
.k in W implies R1.k=0 ) and
A8: 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 being object st x in NAT holds R1.x = R2.x
proof
let x be object;
assume x in NAT;
then reconsider x as Nat;
now
per cases;
suppose
A9: L.x in W;
then R1.x = len CastLTL(L.x) by A7;
hence thesis by A8,A9;
end;
suppose
A10: not L.x in W;
then R1.x=0 by A7;
hence thesis by A8,A10;
end;
end;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
hence thesis;
end;
end;
reserve 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;
Lm25: (for i st i<=n holds R1.i = R2.i) implies Sum(R1, n) = Sum(R2, n)
proof
A1: 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));
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A3: P[k];
P[k+1]
proof
set m=k+1;
assume
A4: for i st i<=k+1 holds R1.i = R2.i;
then
A5: CastNat(k)=k & R1.m = R2.m by MODELC_2:def 1;
A6: for i st i<=k holds R1.i = R2.i
proof
A7: k<=k+1 by NAT_1:11;
let i;
assume i<= k;
hence thesis by A4,A7,XXREAL_0:2;
end;
reconsider k as Element of NAT by ORDINAL1:def 12;
Sum(R1, CastNat(m)) = Sum(R1, m) by MODELC_2:def 1
.= Sum(R2, k) + R2.m by A3,A6,A5,SERIES_1:def 1
.= Sum(R2, m) by SERIES_1:def 1;
hence thesis by MODELC_2:def 1;
end;
hence thesis;
end;
A8: P[0]
proof
assume
A9: 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 A9
.= Sum(R2,0) by SERIES_1:def 1;
hence thesis by MODELC_2:def 1;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A8,A2);
hence thesis by A1;
end;
Lm26: (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
A1: 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;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A3: P[k];
P[k+1]
proof
A4: CastNat(k)=k by MODELC_2:def 1;
set m=k+1;
assume that
A5: for i st i<=k+1 & not i = j holds R1.i = R2.i and
A6: j <= k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
now
per cases by A6,NAT_1:8;
suppose
A7: j <= k;
then
A8: j < m by 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 A3,A5,A4,A7,A8,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
A9: j = k+1;
A10: for i st i<=k holds R1.i = R2.i
proof
let i such that
A11: i<=k;
i < j by A9,A11,NAT_1:13;
hence thesis by A5,A11,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 A9,A10,Lm25
.= 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;
A12: P[0]
proof
A13: Sum(R2,CastNat(0)) = Sum(R2,0) by MODELC_2:def 1
.= R2.0 by SERIES_1:def 1;
assume that
for i st i<=0 & not i=j holds R1.i = R2.i and
A14: j<=0;
A15: Sum(R1,CastNat(0)) = Sum(R1,0) by MODELC_2:def 1
.= R1.0 by SERIES_1:def 1;
j=0 by A14;
hence thesis by A15,A13;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A12,A2);
hence thesis by A1;
end;
theorem Th4:
len(L,{}H) = 0
proof
set s = Partial_seq(L,{}H);
A1: for n being Nat holds s.n = 0*n+0 by Def24;
for n holds Partial_Sums(s).n = 0
proof
let n;
A2: s.0 = 0 by Def24;
Partial_Sums(s).n = (n+1)*(s.0 + s.n)/2 by A1,SERIES_2:42
.= (n+1)*(0+0)/2 by A2,Def24;
hence thesis;
end;
hence thesis;
end;
theorem Th5:
not F in W implies len(L,W \ {F}) = len(L,W)
proof
assume
A1: not F in W;
A2: for x being object holds x in W implies x in W \ {F}
proof let x be object;
assume
A3: x in W;
then not x in {F} by A1,TARSKI:def 1;
hence thesis by A3,XBOOLE_0:def 5;
end;
for x being object holds x in W \ {F} implies x in W by XBOOLE_0:def 5;
hence thesis by A2,TARSKI:2;
end;
theorem Th6:
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 and
A2: L is one-to-one and
A3: F in W;
consider x being object such that
A4: x in dom L and
A5: L.x = F by A1,A3,FUNCT_1:def 3;
set R2= Partial_seq(L,W\{F});
set R1 = Partial_seq(L,W);
set n = len L;
A6: F in LTL_WFF by MODELC_2:1;
x in Seg n by A4,FINSEQ_1:def 3;
then x in { k where k is Nat: 1 <= k & k <= n } by FINSEQ_1:def 1;
then consider k being Nat such that
A7: x=k and
1<=k and
A8: k <= n;
reconsider k as Nat;
L.k in {F} by A5,A7,TARSKI:def 1;
then not L.k in W\{F} by XBOOLE_0:def 5;
then
A9: R2.k= 0 by Def24;
for i st i<=n & not i=k holds R1.i = R2.i
proof
let i such that
i<=n and
A10: not i=k;
now
per cases;
suppose
not i in dom L;
then
A11: L.i = {} by FUNCT_1:def 2;
then
A12: not L.i in W by Lm24;
not L.i in W\{F} by A11,Lm24;
then R2.i = 0 by Def24
.= R1.i by A12,Def24;
hence thesis;
end;
suppose
i in dom L;
then not L.i = F by A2,A4,A5,A7,A10,FUNCT_1:def 4;
then
A13: not L.i in {F} by TARSKI:def 1;
now
per cases;
suppose
A14: L.i in W;
then L.i in W\{F} by A13,XBOOLE_0:def 5;
then R2.i = len CastLTL(L.i) by Def24
.= R1.i by A14,Def24;
hence thesis;
end;
suppose
A15: not L.i in W;
then not L.i in W\{F} by XBOOLE_0:def 5;
then R2.i = 0 by Def24
.= R1.i by A15,Def24;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A16: Sum(R1, n) - R1.k = Sum(R2, n) - R2.k by A8,Lm26;
R1.k = len CastLTL(L.k) by A3,A5,A7,Def24
.= len F by A5,A7,A6,MODELC_2:def 25;
hence thesis by A9,A16;
end;
theorem Th7:
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};
A4: for x being object holds x in W1\{F} implies x in W
proof let x be object;
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;
for x being object holds x in W implies x in W1\{F}
proof let x be object;
assume x in W;
then (not x in {F})& x in W1 by A2,A3,TARSKI:def 1,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 5;
end;
then
A5: W1\{F} = W by A4,TARSKI:2;
F in {F} by TARSKI:def 1;
then F in W1 by A3,XBOOLE_0:def 3;
then len(L,W) = len(L,W1) - len F by A1,A5,Th6;
hence thesis;
end;
theorem Th8:
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);
set k = card W;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A2: P[k];
P[k+1]
proof
let W1 such that
A3: 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
A4: rng L1 = Subformulae H & L1 is one-to-one and
A5: rng L2 = Subformulae H & L2 is one-to-one;
now
per cases by A3,NAT_1:8;
suppose
card W1 <=k;
hence thesis by A2,A4,A5;
end;
suppose
A6: card W1 = k+1;
then W1 <> {};
then consider F being object such that
A7: F in W1 by XBOOLE_0:def 1;
F in Subformulae H by A7;
then reconsider F as LTL-formula by MODELC_2:1;
{F} c= W1 by A7,ZFMISC_1:31;
then
A8: card (W1 \ {F}) = card W1 - card {F} by CARD_2:44
.= card W1 - 1 by CARD_1:30
.= k by A6;
A9: len(L1,W1) = (len(L1,W1) - len F) + len F
.= len(L1,W1\{F}) + len F by A4,A7,Th6;
len(L2,W1) = (len(L2,W1) - len F) + len F
.= len(L2,W1\{F}) + len F by A5,A7,Th6
.= len(L1,W1\{F}) + len F by A2,A4,A5,A8;
hence thesis by A9;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A10: P[0]
proof
let W1;
assume card W1 <=0;
then
A11: W1 = {} H;
then len(L1,W1) = 0 by Th4;
hence thesis by A11,Th4;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A10,A1);
then P[k];
hence thesis;
end;
definition
let H, W;
func len(W) -> Real means
:Def26:
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:58;
set IT = len(L,W);
take IT;
thus thesis by A1;
end;
uniqueness by Th8;
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:58;
len(W\{F}) = len(L,W\{F}) by A2,Def26
.= len(L,W) by A1,Th5;
hence thesis by A2,Def26;
end;
theorem Th10:
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:58;
len(W\{F}) = len(L,W\{F}) by A2,Def26
.= len(L,W) - len F by A1,A2,Th6;
hence thesis by A2,Def26;
end;
theorem Th11:
(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:58;
len(W1) = len(L,W1) by A2,Def26
.= len(L,W) + len F by A1,A2,Th7;
hence thesis by A2,Def26;
end;
theorem Th12:
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:31;
then W1 = W by A1,XBOOLE_1:12;
hence thesis by XREAL_1:31;
end;
suppose
not F in W;
hence thesis by A1,Th11;
end;
end;
hence thesis;
end;
theorem Th13:
len({}H ) = 0
proof
consider L such that
A1: rng L = Subformulae H & L is one-to-one by FINSEQ_4:58;
len({}H) = len(L,{}H) by A1,Def26;
hence thesis by Th4;
end;
theorem Th14:
W = {F} implies len(W) = len F
proof
assume
A1: W = {F};
then
A2: F in W by TARSKI:def 1;
now
assume ex x being object st x in W\{F};
then consider x such that
A3: x in W\{F};
x in W by A3,XBOOLE_0:def 5;
hence contradiction by A1,A3,XBOOLE_0:def 5;
end;
then
A4: W\{F}={}H by XBOOLE_0:def 1;
len(W) = (len(W) - len F) + len F .= len(W\{F}) + len F by A2,Th10
.= 0 + len F by A4,Th13;
hence thesis;
end;
theorem Th15:
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);
set k = card W1;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A2: P[k];
P[k+1]
proof
let W1 such that
A3: card W1 <=k+1;
W c= W1 implies len(W) <= len(W1)
proof
assume
A4: W c= W1;
now
per cases;
suppose
W = W1;
hence thesis;
end;
suppose
W <> W1;
then W c< W1 by A4,XBOOLE_0:def 8;
then consider x being object such that
A5: x in W1 and
A6: W c= W1\{x} by XBOOLE_0:8;
x in Subformulae H by A5;
then reconsider x as LTL-formula by MODELC_2:1;
set X = {x};
X c= W1 by A5,ZFMISC_1:31;
then card (W1\X) = card W1 - card X by CARD_2:44
.= card W1 - 1 by CARD_1:30;
then card (W1\X) +1 <= k+1 by A3;
then card (W1\X) <= k by XREAL_1:6;
then len(W) <= len(W1\X) by A2,A6;
then
A7: len(W) <= len(W1) - len x by A5,Th10;
len(W1) - len x <= len(W1) by XREAL_1:43;
hence thesis by A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A8: P[0]
proof
let W1;
assume card W1 <=0;
then W1 = {} H;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A8,A1);
then P[k];
hence thesis;
end;
theorem Th16:
len(W)<1 implies W = {}H
proof
assume
A1: len(W)<1;
now
assume W <> {}H;
then consider x being object such that
A2: x in W by XBOOLE_0:def 1;
x in Subformulae H by A2;
then reconsider x as LTL-formula by MODELC_2:1;
set X = {x};
A3: X c= W by A2,ZFMISC_1:31;
x is_subformula_of H by A2,MODELC_2:45;
then reconsider X as Subset of Subformulae H by Lm9;
len(X) = len x by Th14;
then
A4: len(X) >=1 by MODELC_2:3;
len(X) <= len(W) by A3,Th15;
hence contradiction by A1,A4,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th17:
len(W) >= 0
proof
now
per cases;
suppose
W = {}H;
hence thesis by Th13;
end;
suppose
W <> {}H;
hence thesis by Th16;
end;
end;
hence thesis;
end;
theorem Th18:
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));
set k = card W1;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A2: P[k];
P[k+1]
proof
let W,W1,W2 such that
A3: card W1 <=k+1;
W = W1 \/ W2 implies len(W) <= len(W1) + len(W2)
proof
assume
A4: W = W1 \/ W2;
now
per cases by A3,NAT_1:8;
suppose
card W1 <=k;
hence thesis by A2,A4;
end;
suppose
card W1 = k+1;
then W1 <> {};
then consider x being object such that
A5: x in W1 by XBOOLE_0:def 1;
x in Subformulae H by A5;
then reconsider x as LTL-formula by MODELC_2:1;
set X = {x};
set Y = W1\X;
set Z = Y \/ W2;
A6: X c= W1 by A5,ZFMISC_1:31;
then card (Y) = card W1 - card X by CARD_2:44
.= card W1 - 1 by CARD_1:30;
then card (Y) + 1 = card W1;
then card (Y) <= k by A3,XREAL_1:6;
then Z = Y \/ W2 implies len(Z) <= len(Y) + len(W2) by A2;
then len(Z) <= len(W1) - len x + len(W2) by A5,Th10;
then len(Z) <= (len(W1) + len(W2)) - len x;
then
A7: len(Z) + len x <= len(W1) + len(W2) by XREAL_1:19;
Z \/ X = (Y \/ X) \/ W2 by XBOOLE_1:4
.= W1 \/ W2 by A6,XBOOLE_1:45;
then len(W) <= len(Z) + len x by A4,Th12;
hence thesis by A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A8: P[0]
proof
let W,W1,W2;
assume card W1 <=0;
then
A9: W1 = {} H;
then len(W1) = 0 by Th13;
hence thesis by A9;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A8,A1);
then P[k];
hence thesis;
end;
definition
let v, H;
assume
A1: H in Subformulae v;
func LTLNew1(H,v) -> Subset of Subformulae v equals
:Def27:
LTLNew1 H;
correctness
proof
ex F st H=F & F is_subformula_of v by A1,MODELC_2:def 24;
then Subformulae H c= Subformulae v by MODELC_2:46;
hence thesis by XBOOLE_1:1;
end;
func LTLNew2(H,v) -> Subset of Subformulae v equals
:Def28:
LTLNew2 H;
correctness
proof
ex F st H=F & F is_subformula_of v by A1,MODELC_2:def 24;
then Subformulae H c= Subformulae v by MODELC_2:46;
hence thesis by XBOOLE_1:1;
end;
end;
Lm27: H in Subformulae v implies len(LTLNew1(H,v)) <= len(H) -1
proof
set New = LTLNew1(H,v);
set Left = {the_left_argument_of H};
set Right = {the_right_argument_of H};
assume
A1: H in Subformulae v;
then
A2: New = LTLNew1 H by Def27;
ex F st H=F & F is_subformula_of v by A1,MODELC_2:def 24;
then
A3: Subformulae H c= Subformulae v by MODELC_2:46;
now
per cases;
suppose
A4: H is conjunctive;
then Right is Subset of Subformulae H by Lm12;
then reconsider Right as Subset of Subformulae v by A3,XBOOLE_1:1;
Left is Subset of Subformulae H by A4,Lm12;
then reconsider Left as Subset of Subformulae v by A3,XBOOLE_1:1;
New = {the_left_argument_of H,the_right_argument_of H } by A2,A4,Def1;
then New = Left \/ Right by ENUMSET1:1;
then
A5: len(New) <= len(Left) + len(Right) by Th18;
A6: len(H) = 1+len(the_left_argument_of H) + len(the_right_argument_of H
) by A4,MODELC_2:11;
len(Left) = len(the_left_argument_of H) & len(Right) = len(
the_right_argument_of H) by Th14;
hence thesis by A6,A5;
end;
suppose
A7: H is disjunctive or H is Until;
then New = Left by A2,Def1;
then len(New) = len(the_left_argument_of H) by Th14;
then
A8: len(New) +0 <= len(the_left_argument_of H) + len(
the_right_argument_of H) by XREAL_1:7;
len(H) = 1+len(the_left_argument_of H) + len(the_right_argument_of H
) by A7,MODELC_2:11;
hence thesis by A8;
end;
suppose
A9: H is next;
1<=len(H) by MODELC_2:3;
then
A10: 1-1 <= len(H)-1 by XREAL_1:9;
New = {} v by A2,A9,Def1;
hence thesis by A10,Th13;
end;
suppose
A11: H is Release;
then New = Right by A2,Def1;
then len(New) = len(the_right_argument_of H) by Th14;
then
A12: len(New)+0 <= len(the_left_argument_of H) + len(
the_right_argument_of H) by XREAL_1:7;
len(H) = 1+len(the_left_argument_of H) + len(the_right_argument_of H
) by A11,MODELC_2:11;
hence thesis by A12;
end;
suppose
A13: 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
A14: 1-1 <= len(H)-1 by XREAL_1:9;
New = {} v by A2,A13,Def1;
hence thesis by A14,Th13;
end;
end;
hence thesis;
end;
Lm28: H in Subformulae v implies len(LTLNew2(H,v)) <= len(H) -1
proof
set New = LTLNew2(H,v);
set Left = {the_left_argument_of H};
set Right = {the_right_argument_of H};
assume
A1: H in Subformulae v;
then
A2: New = LTLNew2 H by Def28;
ex F st H=F & F is_subformula_of v by A1,MODELC_2:def 24;
then
A3: Subformulae H c= Subformulae v by MODELC_2:46;
now
per cases;
suppose
A4: H is Release;
then Right is Subset of Subformulae H by Lm12;
then reconsider Right as Subset of Subformulae v by A3,XBOOLE_1:1;
Left is Subset of Subformulae H by A4,Lm12;
then reconsider Left as Subset of Subformulae v by A3,XBOOLE_1:1;
New = {the_left_argument_of H,the_right_argument_of H } by A2,A4,Def2;
then New = Left \/ Right by ENUMSET1:1;
then
A5: len(New) <= len(Left) + len(Right) by Th18;
A6: len(H) = 1+len(the_left_argument_of H) + len(the_right_argument_of H
) by A4,MODELC_2:11;
len(Left) = len(the_left_argument_of H) & len(Right) = len(
the_right_argument_of H) by Th14;
hence thesis by A6,A5;
end;
suppose
A7: H is disjunctive or H is Until;
then New = Right by A2,Def2;
then len(New) = len(the_right_argument_of H) by Th14;
then
A8: len(New)+0 <= len(the_left_argument_of H) + len(
the_right_argument_of H) by XREAL_1:7;
len(H) = 1+len(the_left_argument_of H) + len(the_right_argument_of H
) by A7,MODELC_2:11;
hence thesis by A8;
end;
suppose
A9: H is conjunctive or H is next;
1<=len(H) by MODELC_2:3;
then
A10: 1-1 <= len(H)-1 by XREAL_1:9;
New = {} v by A2,A9,Def2;
hence thesis by A10,Th13;
end;
suppose
A11: 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
A12: 1-1 <= len(H)-1 by XREAL_1:9;
New = {} v by A2,A11,Def2;
hence thesis by A12,Th13;
end;
end;
hence thesis;
end;
theorem Th19:
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);
set M1 = NN1 \ {H};
set New1= LTLNew1(H,v);
set M2 = New1 \ the LTLold of N1;
reconsider M1 as Subset of Subformulae v;
reconsider M2 as Subset of Subformulae v;
New1 = LTLNew1 H by A1,Def27;
then NN2 = M1 \/ M2 by A1,A2,Def4;
then
A3: len(NN2)<=len(M1) + len(M2) by Th18;
reconsider NN1 as Subset of Subformulae v;
A4: len(M2) <= len(New1) by Th15,XBOOLE_1:36;
len(New1) <= len(H) -1 by A1,Lm27;
then len(M2) <= len(H) -1 by A4,XXREAL_0:2;
then
A5: len(M1) + len(M2) <= len(M1) + (len(H) -1) by XREAL_1:6;
len(M1) = len(NN1)-len(H) by A1,Th10;
hence thesis by A5,A3,XXREAL_0:2;
end;
theorem Th20:
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
H is disjunctive or H is Until or H is Release and
A2: N2 = SuccNode2(H,N1);
set M1 = NN1 \ {H};
set New2= LTLNew2(H,v);
set M2 = New2 \ the LTLold of N1;
reconsider M1 as Subset of Subformulae v;
reconsider M2 as Subset of Subformulae v;
New2 = LTLNew2 H by A1,Def28;
then NN2 = M1 \/ M2 by A1,A2,Def5;
then
A3: len(NN2)<=len(M1) + len(M2) by Th18;
reconsider NN1 as Subset of Subformulae v;
A4: len(M2) <= len(New2) by Th15,XBOOLE_1:36;
len(New2) <= len(H) -1 by A1,Lm28;
then len(M2) <= len(H) -1 by A4,XXREAL_0:2;
then
A5: len(M1) + len(M2) <= len(M1) + (len(H) -1) by XREAL_1:6;
len(M1) = len(NN1)-len(H) by A1,Th10;
hence thesis by A5,A3,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 Th17;
hence thesis by INT_1:53;
end;
end;
theorem Th21:
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;
then r2 <= r1-1 by Th19,Th20;
hence thesis by Lm5;
end;
theorem Th22:
len(N)<=0 implies the LTLnew of N = {}v
proof
assume
A1: len(N)<=0;
len(the LTLnew of N) -1 < [\ len(the LTLnew of N) /] by INT_1:def 6;
then len(the LTLnew of N) -1 +1 <0+1 by A1,XREAL_1:8;
hence thesis by Th16;
end;
theorem Th23:
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 Th13;
hence contradiction by A1;
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: for l being Nat st P[l] holds P[l + 1]
proof
let l be Nat such that
A2: 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
A3: 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 A3,NAT_1:8;
suppose
len(N)<=l;
hence thesis by A2;
end;
suppose
A4: len(N)=l+1;
then NewN <> {}v by Th23;
then consider x being object such that
A5: x in NewN by XBOOLE_0:def 1;
x in Subformulae v by A5;
then reconsider x as LTL-formula by MODELC_2:1;
set M1 = SuccNode1(x,N);
M1 is_succ1_of N by A5;
then
A6: M1 is_succ_of N;
then len(M1)<=len(N)-1 by Th21;
then consider n,L,M such that
A7: 1 <= n and
A8: len L = n and
A9: L.1 = M1 and
A10: L.n = M and
A11: the LTLnew of M = {}v and
A12: L is_Finseq_for v by A2,A4;
set L1 = <*N*>^L;
set n1=n+1;
A13: len L1 = len <*N*> + len L by FINSEQ_1:22
.= n1 by A8,FINSEQ_1:39;
A14: L1 is_Finseq_for v
proof
let k such that
A15: 1 <= k and
A16: k < len(L1);
A17: k+1<=len(L1) by A16,NAT_1:13;
ex N1,N2 st L1.k = N1 & L1.(k + 1) = N2 & N2 is_succ_of N1
proof
set N2 = L1.(k+1);
set N1 = L1.k;
now
per cases;
suppose
k<=1;
then
A18: k=1 by A15,XXREAL_0:1;
then reconsider N1 as strict LTLnode over v by
FINSEQ_1:41;
len <*N*> =1 by FINSEQ_1:39;
then
A19: N2 = L.(2-1) by A17,A18,FINSEQ_1:24
.= M1 by A9;
then reconsider N2 as strict LTLnode over v;
take N1,N2;
thus thesis by A6,A18,A19,FINSEQ_1:41;
end;
suppose
A20: 1< k;
set km1= k -1;
reconsider km1 as Nat by A20,NAT_1:20;
1<km1+1 by A20;
then
A21: 1<= km1 by NAT_1:13;
A22: len <*N*> < k by A20,FINSEQ_1:39;
then
A23: N1=L.(k - len <*N*>) by A16,FINSEQ_1:24
.= L.km1 by FINSEQ_1:39;
k<=k+1 by NAT_1:11;
then len <*N*> <k+1 by A22,XXREAL_0:2;
then
A24: N2= L.(k+1 - len <*N*>) by A17,FINSEQ_1:24
.= L.(k+1 -1) by FINSEQ_1:39
.= L.(km1+1);
A25: km1<n1-1 by A13,A16,XREAL_1:14;
then
A26: ex N10,N20 st L.km1 = N10 & L.(km1 + 1) = N20 & N20
is_succ_of N10 by A8,A12,A21;
then reconsider N1 as strict LTLnode over v by A23;
reconsider N2 as strict LTLnode over v by A24,A26;
take N1,N2;
thus thesis by A8,A12,A21,A25,A23,A24;
end;
end;
hence thesis;
end;
hence thesis;
end;
A27: len <*N*> =1 by FINSEQ_1:39;
A28: L1.1= N by FINSEQ_1:41;
1<n1 by A7,NAT_1:13;
then L1.n1 = L.(n1 - 1) by A13,A27,FINSEQ_1:24
.= M by A10;
hence thesis by A11,A13,A28,A14,NAT_1:11;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
set k = len(N);
reconsider k as Nat;
A29: 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
set n = 1;
set M = N;
assume
A30: len(N)<=0;
take n;
set L = <*M*>;
take L;
take M;
thus thesis by A30,Th22,FINSEQ_1:40;
end;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2 (A29,A1);
then P[k];
hence thesis;
end;
theorem Th25:
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;
suppose
N2 is_succ1_of N1;
then consider H such that
A2: H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
the LTLold of N2 =(the LTLold of N1) \/ {H} & the LTLnext of N2 = (
the LTLnext of N1) \/ LTLNext H by A2,Def4;
hence thesis by XBOOLE_1:7;
end;
suppose
N2 is_succ2_of N1;
then consider H such that
A3: H in the LTLnew of N1 and
H is disjunctive or H is Until or H is Release and
A4: N2 = SuccNode2(H,N1);
the LTLold of N2 =(the LTLold of N1) \/ {H} by A3,A4,Def5;
hence thesis by A3,A4,Def5,XBOOLE_1:7;
end;
end;
hence thesis;
end;
theorem Th26:
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 by A2,A3,FINSEQ_1:17;
A5: dom L1 = Seg m by A2,A3,FINSEQ_1:17;
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
A6: 1 <= k and
A7: k < len(L1);
k in dom L1 by A4,A5,A6,A7,FINSEQ_1:1;
then
A8: L1.k=L.k by A3,FUNCT_1:47;
1<= k+1 & k+1<=m by A4,A6,A7,NAT_1:13;
then k+1 in dom L1 by A5,FINSEQ_1:1;
then
A9: L1.(k+1)=L.(k+1) by A3,FUNCT_1:47;
k < len(L) by A2,A4,A7,XXREAL_0:2;
hence thesis by A1,A6,A8,A9;
end;
hence thesis;
end;
theorem Th27:
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<
n & not F in the LTLold of CastNode(L.m,v) & F in the LTLold of CastNode(L.(m+1
),v)
proof
assume
A1: 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);
defpred P[Nat] means for F1,n1,L1 st len(L1) <= $1 holds L1 is_Finseq_for v
& not (F1 in the LTLold of CastNode(L1.1,v)) & (1< n1 & n1 <= len(L1) & F1 in
the LTLold of CastNode(L1.n1,v) ) implies ex m st 1<= m & m<n1 & not(F1 in the
LTLold of CastNode(L1.m,v)) & F1 in the LTLold of CastNode(L1.(m+1),v);
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k such that
A3: P[k];
P[k + 1]
proof
let F1,n1,L1 such that
A4: len(L1) <= k+1;
now
per cases by A4,NAT_1:8;
suppose
len(L1)<=k;
hence thesis by A3;
end;
suppose
A5: len(L1)=k+1;
L1 is_Finseq_for v & not F1 in the LTLold of CastNode(L1.1,v) &
1< n1 & n1 <= len(L1) & F1 in the LTLold of CastNode(L1.n1,v) implies ex m st 1
<= m & m<n1 & not F1 in the LTLold of CastNode(L1.m,v) & F1 in the LTLold of
CastNode(L1.(m+1),v)
proof
assume that
A6: L1 is_Finseq_for v and
A7: not F1 in the LTLold of CastNode(L1.1,v) and
A8: 1< n1 and
A9: n1 <= len(L1) and
A10: F1 in the LTLold of CastNode(L1.n1,v);
now
per cases by A5,A9,NAT_1:8;
suppose
A11: n1<=k;
set L2=L1|Seg k;
reconsider L2 as FinSequence by FINSEQ_1:15;
A12: k+0 <= k+1 by XREAL_1:7;
then
A13: dom L2 = Seg k by A5,FINSEQ_1:17;
then n1 in dom L2 by A8,A11,FINSEQ_1:1;
then
A14: L2.n1 = L1.n1 by FUNCT_1:47;
1< k by A8,A11,XXREAL_0:2;
then 1 in dom L2 by A13,FINSEQ_1:1;
then
A15: not F1 in the LTLold of CastNode(L2.1,v) by A7,FUNCT_1:47;
len(L2) = k & L2 is_Finseq_for v by A5,A6,A12,Th26,FINSEQ_1:17;
then consider m such that
A16: 1<= m and
A17: m<n1 and
A18: ( not F1 in the LTLold of CastNode(L2.m,v))& F1 in
the LTLold of CastNode(L2.(m +1),v) by A3,A8,A10,A11,A15,A14;
m+1<=n1 by A17,NAT_1:13;
then
A19: m+1 <=k by A11,XXREAL_0:2;
1<= m+1 by A16,NAT_1:13;
then m+1 in dom L2 by A13,A19,FINSEQ_1:1;
then
A20: L2.(m+1) = L1.(m+1) by FUNCT_1:47;
m <=k by A11,A17,XXREAL_0:2;
then m in dom L2 by A13,A16,FINSEQ_1:1;
then L2.m = L1.m by FUNCT_1:47;
hence thesis by A16,A17,A18,A20;
end;
suppose
A21: n1=k+1;
then
A22: 1<= k by A8,NAT_1:13;
A23: k+0 < k+1 by XREAL_1:8;
now
per cases;
suppose
not F1 in the LTLold of CastNode(L1.k,v);
hence thesis by A10,A21,A23,A22;
end;
suppose
A24: F1 in the LTLold of CastNode(L1.k,v);
A25: 1<k
proof
set b=1-k;
set a=k-1;
A26: a+b=0 & 1-1<=k-1 by A22,XREAL_1:9;
now
assume k<=1;
then 1-1<=1-k by XREAL_1:10;
then a=0 by A26;
hence contradiction by A7,A24;
end;
hence thesis;
end;
set L2=L1|Seg k;
reconsider L2 as FinSequence by FINSEQ_1:15;
A27: k+0 <= k+1 by XREAL_1:7;
then
A28: dom L2 = Seg k by A5,FINSEQ_1:17;
then k in dom L2 by A22,FINSEQ_1:1;
then
A29: F1 in the LTLold of CastNode(L2.k,v) by A24,FUNCT_1:47;
1 in dom L2 by A22,A28,FINSEQ_1:1;
then
A30: not F1 in the LTLold of CastNode(L2.1,v) by A7,FUNCT_1:47;
len(L2) = k & L2 is_Finseq_for v by A5,A6,A27,Th26,
FINSEQ_1:17;
then consider m such that
A31: 1<= m and
A32: m<k and
A33: not F1 in the LTLold of CastNode(L2.m,v) and
A34: F1 in the LTLold of CastNode(L2.(m+1),v) by A3,A30,A29,A25;
m in dom L2 by A28,A31,A32,FINSEQ_1:1;
then
A35: not F1 in the LTLold of CastNode(L1.m,v) by A33,FUNCT_1:47;
1<= m+1 & m+1<=k by A31,A32,NAT_1:13;
then m+1 in dom L2 by A28,FINSEQ_1:1;
then
A36: L2.(m+1) = L1.(m+1) by FUNCT_1:47;
m<n1 by A21,A23,A32,XXREAL_0:2;
hence thesis by A31,A34,A35,A36;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
A37: P[0];
for k being Nat holds P[k] from NAT_1:sch 2 (A37,A2);
hence thesis by A1;
end;
theorem Th28:
N2 is_succ_of N1 & not F in the LTLold of N1 & F in the LTLold
of N2 implies N2 is_succ_of N1,F
proof
assume that
A1: N2 is_succ_of N1 and
A2: not F in the LTLold of N1 and
A3: F in the LTLold of N2;
now
per cases by A1;
suppose
N2 is_succ1_of N1;
then consider H such that
A4: H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
the LTLold of N2 =(the LTLold of N1) \/ {H} by A4,Def4;
then F in (the LTLold of N1) or F in {H} by A3,XBOOLE_0:def 3;
then F=H by A2,TARSKI:def 1;
hence thesis by A4;
end;
suppose
N2 is_succ2_of N1;
then consider H such that
A5: H in the LTLnew of N1 and
A6: H is disjunctive or H is Until or H is Release and
A7: N2=SuccNode2(H,N1);
the LTLold of N2 =(the LTLold of N1) \/ {H} by A5,A7,Def5;
then F in (the LTLold of N1) or F in {H} by A3,XBOOLE_0:def 3;
then F=H by A2,TARSKI:def 1;
hence thesis by A5,A6,A7;
end;
end;
hence thesis;
end;
theorem Th29:
L is_Finseq_for v & F in the LTLnew of CastNode(L.1,v) & 1< n &
n <= len(L) & not F in the LTLnew of CastNode(L.n,v) implies ex m st 1<= m & m<
n & F in the LTLnew of CastNode(L.m,v) & not F in the LTLnew of CastNode(L.(m+1
),v)
proof
assume
A1: L is_Finseq_for v & F in the LTLnew of CastNode(L.1,v) & 1< n & n <=
len (L) & not F in the LTLnew of CastNode(L.n,v);
defpred P[Nat] means for F1,n1,L1 st len(L1) <= $1 holds L1 is_Finseq_for v
& F1 in the LTLnew of CastNode(L1.1,v) & (1< n1 & n1 <= len(L1) & not (F1 in
the LTLnew of CastNode(L1.n1,v)) ) implies ex m st 1<= m & m<n1 & F1 in the
LTLnew of CastNode(L1.m,v) & not (F1 in the LTLnew of CastNode(L1.(m+1),v));
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k such that
A3: P[k];
P[k + 1]
proof
let F1,n1,L1 such that
A4: len(L1) <= k+1;
now
per cases by A4,NAT_1:8;
suppose
len(L1)<=k;
hence thesis by A3;
end;
suppose
A5: len(L1)=k+1;
L1 is_Finseq_for v & F1 in the LTLnew of CastNode(L1.1,v) & 1<
n1 & n1 <= len(L1) & not F1 in the LTLnew of CastNode(L1.n1,v) implies ex m st
1<= m & m<n1 & F1 in the LTLnew of CastNode(L1.m,v) & not F1 in the LTLnew of
CastNode(L1.(m+1),v)
proof
assume that
A6: L1 is_Finseq_for v and
A7: F1 in the LTLnew of CastNode(L1.1,v) and
A8: 1< n1 and
A9: n1 <= len(L1) and
A10: not F1 in the LTLnew of CastNode(L1.n1,v);
now
per cases by A5,A9,NAT_1:8;
suppose
A11: n1<=k;
set L2=L1|Seg k;
reconsider L2 as FinSequence by FINSEQ_1:15;
A12: k+0 <= k+1 by XREAL_1:7;
then
A13: dom L2 = Seg k by A5,FINSEQ_1:17;
then n1 in dom L2 by A8,A11,FINSEQ_1:1;
then
A14: L2.n1 = L1.n1 by FUNCT_1:47;
1< k by A8,A11,XXREAL_0:2;
then 1 in dom L2 by A13,FINSEQ_1:1;
then
A15: F1 in the LTLnew of CastNode(L2.1,v) by A7,FUNCT_1:47;
len(L2) = k & L2 is_Finseq_for v by A5,A6,A12,Th26,FINSEQ_1:17;
then consider m such that
A16: 1<= m and
A17: m<n1 and
A18: F1 in the LTLnew of CastNode(L2.m,v) & not F1 in the
LTLnew of CastNode(L2.(m+ 1),v) by A3,A8,A10,A11,A15,A14;
m+1<=n1 by A17,NAT_1:13;
then
A19: m+1 <=k by A11,XXREAL_0:2;
1<= m+1 by A16,NAT_1:13;
then m+1 in dom L2 by A13,A19,FINSEQ_1:1;
then
A20: L2.(m+1) = L1.(m+1) by FUNCT_1:47;
m <=k by A11,A17,XXREAL_0:2;
then m in dom L2 by A13,A16,FINSEQ_1:1;
then L2.m = L1.m by FUNCT_1:47;
hence thesis by A16,A17,A18,A20;
end;
suppose
A21: n1=k+1;
then
A22: 1<= k by A8,NAT_1:13;
A23: k+0 < k+1 by XREAL_1:8;
now
per cases;
suppose
F1 in the LTLnew of CastNode(L1.k,v);
hence thesis by A10,A21,A23,A22;
end;
suppose
A24: not F1 in the LTLnew of CastNode(L1.k,v);
A25: 1<k
proof
set b=1-k;
set a=k-1;
A26: a+b=0 & 1-1<=k-1 by A22,XREAL_1:9;
now
assume k<=1;
then 1-1<=1-k by XREAL_1:10;
then a=0 by A26;
hence contradiction by A7,A24;
end;
hence thesis;
end;
set L2=L1|Seg k;
reconsider L2 as FinSequence by FINSEQ_1:15;
A27: k+0 <= k+1 by XREAL_1:7;
then
A28: dom L2 = Seg k by A5,FINSEQ_1:17;
then k in dom L2 by A22,FINSEQ_1:1;
then
A29: not F1 in the LTLnew of CastNode(L2.k,v) by A24,FUNCT_1:47;
1 in dom L2 by A22,A28,FINSEQ_1:1;
then
A30: F1 in the LTLnew of CastNode(L2.1,v) by A7,FUNCT_1:47;
len(L2) = k & L2 is_Finseq_for v by A5,A6,A27,Th26,
FINSEQ_1:17;
then consider m such that
A31: 1<= m and
A32: m<k and
A33: F1 in the LTLnew of CastNode(L2.m,v) and
A34: not F1 in the LTLnew of CastNode(L2.(m+1),v) by A3,A30,A29
,A25;
m in dom L2 by A28,A31,A32,FINSEQ_1:1;
then
A35: F1 in the LTLnew of CastNode(L1.m,v) by A33,FUNCT_1:47;
1<= m+1 & m+1<=k by A31,A32,NAT_1:13;
then m+1 in dom L2 by A28,FINSEQ_1:1;
then
A36: L2.(m+1) = L1.(m+1) by FUNCT_1:47;
m<n1 by A21,A23,A32,XXREAL_0:2;
hence thesis by A31,A34,A35,A36;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
A37: P[0];
for k being Nat holds P[k] from NAT_1:sch 2 (A37,A2);
hence thesis by A1;
end;
theorem Th30:
N2 is_succ_of N1 & F in the LTLnew of N1 & not F in the LTLnew
of N2 implies N2 is_succ_of N1,F
proof
assume that
A1: N2 is_succ_of N1 and
A2: F in the LTLnew of N1 and
A3: not F in the LTLnew of N2;
now
per cases by A1;
suppose
N2 is_succ1_of N1;
then consider H such that
A4: H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
the LTLnew of N2 =((the LTLnew of N1) \ {H}) \/ (LTLNew1 H \ the
LTLold of N1) by A4,Def4;
then not F in (the LTLnew of N1)\ {H} by A3,XBOOLE_0:def 3;
then not F in the LTLnew of N1 or F in {H} by XBOOLE_0:def 5;
then F=H by A2,TARSKI:def 1;
hence thesis by A4;
end;
suppose
N2 is_succ2_of N1;
then consider H such that
A5: H in the LTLnew of N1 and
A6: H is disjunctive or H is Until or H is Release and
A7: N2=SuccNode2(H,N1);
the LTLnew of N2 =((the LTLnew of N1) \ {H}) \/ (LTLNew2 H \ the
LTLold of N1) by A5,A7,Def5;
then not F in (the LTLnew of N1)\ {H} by A3,XBOOLE_0:def 3;
then not F in the LTLnew of N1 or F in {H} by XBOOLE_0:def 5;
then F=H by A2,TARSKI:def 1;
hence thesis by A5,A6,A7;
end;
end;
hence thesis;
end;
theorem Th31:
L is_Finseq_for v & 1<= m & m<=n & n<= len(L) implies the LTLold
of CastNode(L.m,v) c= the LTLold of CastNode(L.n,v) & the LTLnext of CastNode(L
.m,v) c= the LTLnext of CastNode(L.n,v)
proof
assume
A1: L is_Finseq_for v & 1<= m & m<=n & n<= len(L);
defpred P[Nat] means for n1,m1,L1 st len(L1) <= $1 holds L1 is_Finseq_for v
& (1<= m1 & m1<=n1 & n1<= len(L1)) implies (the LTLold of CastNode(L1.m1,v) c=
the LTLold of CastNode(L1.n1,v)) & (the LTLnext of CastNode(L1.m1,v) c= the
LTLnext of CastNode(L1.n1,v));
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k such that
A3: P[k];
P[k + 1]
proof
let n1,m1,L1 such that
A4: len(L1) <= k+1;
now
per cases by A4,NAT_1:8;
suppose
len(L1)<=k;
hence thesis by A3;
end;
suppose
A5: len(L1)=k+1;
L1 is_Finseq_for v & 1<= m1 & m1<=n1 & n1<= len(L1) implies the
LTLold of CastNode(L1.m1,v) c= the LTLold of CastNode(L1.n1,v) & the LTLnext of
CastNode(L1.m1,v) c= the LTLnext of CastNode(L1.n1,v)
proof
assume that
A6: L1 is_Finseq_for v and
A7: 1<= m1 and
A8: m1<=n1 and
A9: n1<= len(L1);
A10: 1<=n1 by A7,A8,XXREAL_0:2;
now
per cases by A5,A9,NAT_1:8;
suppose
A11: n1<=k;
set L2=L1|Seg k;
reconsider L2 as FinSequence by FINSEQ_1:15;
A12: k+0 <= k+1 by XREAL_1:7;
then
A13: dom L2 = Seg k by A5,FINSEQ_1:17;
then n1 in dom L2 by A10,A11,FINSEQ_1:1;
then
A14: L2.n1 = L1.n1 by FUNCT_1:47;
m1<=k by A8,A11,XXREAL_0:2;
then m1 in dom L2 by A7,A13,FINSEQ_1:1;
then
A15: L2.m1 = L1.m1 by FUNCT_1:47;
len(L2) = k & L2 is_Finseq_for v by A5,A6,A12,Th26,FINSEQ_1:17;
hence thesis by A3,A7,A8,A11,A15,A14;
end;
suppose
A16: n1=k+1;
now
per cases by A8,XXREAL_0:1;
suppose
A17: m1<n1;
set L2=L1|Seg k;
reconsider L2 as FinSequence by FINSEQ_1:15;
A18: m1<=k by A16,A17,NAT_1:13;
A19: k+0 <= k+1 by XREAL_1:7;
then
A20: dom L2 = Seg k by A5,FINSEQ_1:17;
then m1 in dom L2 by A7,A18,FINSEQ_1:1;
then
A21: L2.m1 = L1.m1 by FUNCT_1:47;
A22: 1<= k by A7,A18,XXREAL_0:2;
then k in dom L2 by A20,FINSEQ_1:1;
then
A23: L2.k = L1.k by FUNCT_1:47;
len(L2) = k & L2 is_Finseq_for v by A5,A6,A19,Th26,
FINSEQ_1:17;
then
A24: the LTLold of CastNode(L1.m1,v) c= the LTLold of
CastNode(L1.k,v) & the LTLnext of CastNode(L1.m1,v) c= the LTLnext of CastNode(
L1.k,v) by A3,A7,A18,A21,A23;
k<len(L1) by A5,NAT_1:13;
then consider N1,N2 such that
A25: N1 = L1.k & N2=L1.(k+1) and
A26: N2 is_succ_of N1 by A6,A22;
A27: N1 = CastNode(N1,v) & N2 = CastNode(N2,v) by Def16;
the LTLold of N1 c= the LTLold of N2 & the LTLnext of
N1 c= the LTLnext of N2 by A26,Th25;
hence thesis by A16,A24,A25,A27;
end;
suppose
m1=n1;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
A28: P[0];
for k being Nat holds P[k] from NAT_1:sch 2 (A28,A2);
hence thesis by A1;
end;
theorem Th32:
N2 is_succ_of N1,F implies F in the LTLold of N2
proof
assume
A1: N2 is_succ_of N1,F;
now
per cases by A1;
suppose
F in the LTLnew of N1 & N2 = SuccNode1(F,N1);
then the LTLold of N2 =(the LTLold of N1) \/ {F} by Def4;
then
A2: {F} c= the LTLold of N2 by XBOOLE_1:7;
F in {F} by TARSKI:def 1;
hence thesis by A2;
end;
suppose
F in the LTLnew of N1 & (F is disjunctive or F is Until or F is
Release) & N2=SuccNode2(F,N1);
then the LTLold of N2 =(the LTLold of N1) \/ {F} by Def5;
then
A3: {F} c= the LTLold of N2 by XBOOLE_1:7;
F in {F} by TARSKI:def 1;
hence thesis by A3;
end;
end;
hence thesis;
end;
theorem Th33:
L is_Finseq_for v & 1<= len(L) & the LTLnew of CastNode(L.(len(L
)),v) = {} v implies the LTLnew of CastNode(L.1,v) c= the LTLold of CastNode(L.
(len(L)),v)
proof
assume that
A1: L is_Finseq_for v and
A2: 1<=len(L) and
A3: the LTLnew of CastNode(L.(len(L)),v) = {} v;
set n= len(L);
the LTLnew of CastNode(L.1,v) c= the LTLold of CastNode(L.n,v)
proof
let x be object;
assume
A4: x in the LTLnew of CastNode(L.1,v);
then x in Subformulae v;
then reconsider x as LTL-formula by MODELC_2:1;
1<n by A2,A3,A4,XXREAL_0:1;
then consider m such that
A5: 1<= m & m<n and
A6: x in the LTLnew of CastNode(L.m,v) & not x in the LTLnew of
CastNode(L.(m+1) ,v) by A1,A3,A4,Th29;
set m1 = m+1;
1<=m1 & m1<=n by A5,NAT_1:13;
then
A7: the LTLold of CastNode(L.m1,v) c= the LTLold of CastNode(L.n,v) by A1,Th31;
consider N1,N2 such that
A8: N1 = L.m and
A9: N2 = L.(m+1) and
A10: N2 is_succ_of N1 by A1,A5;
A11: N2 = CastNode(L.m1,v) by A9,Def16;
N1 = CastNode(L.m,v) by A8,Def16;
then x in the LTLold of N2 by A6,A10,A11,Th30,Th32;
hence thesis by A11,A7;
end;
hence thesis;
end;
theorem Th34:
L is_Finseq_for v & 1<= m & m<=len(L) & the LTLnew of CastNode(L
.(len(L)),v) = {} v implies the LTLnew of CastNode(L.m,v) c= the LTLold of
CastNode(L.(len(L)),v)
proof
assume that
A1: L is_Finseq_for v & 1<= m & m<=len(L) and
A2: the LTLnew of CastNode(L.(len(L)),v) = {} v;
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)) by A1,Lm15;
hence thesis by A2,Th33;
end;
theorem Th35:
L is_Finseq_for v & 1<= k & k<len(L) implies CastNode(L.(k+1),v)
is_succ_of CastNode(L.k,v)
proof
assume L is_Finseq_for v & 1<= k & k<len(L);
then consider N,M such that
A1: N = L.k and
A2: M=L.(k+1) & M is_succ_of N;
CastNode(L.k,v) = N by A1,Def16;
hence thesis by A2,Def16;
end;
theorem Th36:
L is_Finseq_for v & 1<= k & k<=len(L) implies len(CastNode(L.k,v
)) <= len(CastNode(L.1,v)) -k+1
proof
defpred P[Nat] means for L,j st len(L) <= $1 holds L is_Finseq_for v & 1<= j
& j<=len(L) implies len(CastNode(L.j,v)) <= len(CastNode(L.1,v)) -j+1;
A1: for n st P[n] holds P[n + 1]
proof
let n;
assume
A2: P[n];
A3: for L,k st len(L) = n+1 holds L is_Finseq_for v & 1<= k & k<=len(L)
implies len(CastNode(L.k,v)) <= len(CastNode(L.1,v)) -k+1
proof
let L,k such that
A4: len(L) = n+1;
L is_Finseq_for v & 1<= k & k<=len(L) implies len(CastNode(L.k,v))
<= len(CastNode(L.1,v)) -k+1
proof
set L1= L|Seg n;
assume that
A5: L is_Finseq_for v and
A6: 1<= k and
A7: k<=len(L);
reconsider L1 as FinSequence by FINSEQ_1:15;
A8: n<len(L) by A4,NAT_1:13;
then
A9: len(L1) = n by FINSEQ_1:17;
A10: dom L1 = Seg n by A8,FINSEQ_1:17;
A11: for m st 1<= m & m<=n holds L1.m = L.m
by A10,FINSEQ_1:1,FUNCT_1:47;
A12: not n=0 implies 0<0+n;
now
per cases by A4,A7,A12,NAT_1:8,19;
suppose
A13: k<=n;
then 1<=n by A6,XXREAL_0:2;
then
A14: L1.1=L.1 by A11;
L1.k = L.k by A6,A11,A13;
hence thesis by A2,A5,A6,A8,A9,A13,A14,Th26;
end;
suppose
A15: k=n+1 & n>=1;
then
len(CastNode(L.k,v)) <= len(CastNode(L.n,v)) -1 by A5,A8,Th21,Th35;
then
A16: len(CastNode(L.k,v)) + 1 <= len(CastNode(L.n,v))-1 +1 by XREAL_1:6;
L1.n = L.n & L1.1=L.1 by A11,A15;
then
len(CastNode(L.n,v)) <= len(CastNode(L.1,v)) -n+1 by A2,A5,A8,A9
,A15,Th26;
then len(CastNode(L.k,v)) + 1 <= (len(CastNode(L.1,v)) -n)+1 by A16
,XXREAL_0:2;
hence thesis by A15,XREAL_1:6;
end;
suppose
k=n+1 & n=0;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
P[n+1]
proof
let L,j such that
A17: 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 A17,NAT_1:8;
suppose
len(L)<=n;
hence thesis by A2;
end;
suppose
len(L) =n+1;
hence thesis by A3;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A18: P[0];
for n holds P[n] from NAT_1:sch 2(A18,A1);
hence thesis;
end;
reserve s,s0,s1,s2 for elementary strict LTLnode over v;
theorem Th37:
s2 is_next_of s1 implies the LTLnext of s1 c= the LTLold of s2
proof
set N1 = 'X' s1;
A1: the LTLnew of s2 = {} v by Def11;
assume s2 is_next_of s1;
then consider L such that
A2: 1<=len(L) and
A3: L is_Finseq_for v and
A4: L.1 = 'X' s1 and
A5: L.(len(L)) = s2;
set n = len(L);
A6: CastNode(L.n,v) = s2 by A5,Def16;
A7: CastNode(L.1,v) = N1 by A4,Def16;
the LTLnext of s1 c= the LTLold of s2
proof
let x be object;
assume
A8: x in the LTLnext of s1;
then x in Subformulae v;
then reconsider x as LTL-formula by MODELC_2:1;
1<n by A2,A4,A5,A1,A8,XXREAL_0:1;
then consider m such that
A9: 1<= m & m<n and
A10: x in the LTLnew of CastNode(L.m,v) & not x in the LTLnew of
CastNode(L.(m+1) ,v) by A3,A7,A6,A1,A8,Th29;
set m1 = m+1;
consider N1,N2 such that
A11: N1 = L.m and
A12: N2 = L.(m+1) and
A13: N2 is_succ_of N1 by A3,A9;
A14: N2 = CastNode(L.m1,v) by A12,Def16;
1<=m1 & m1<=n by A9,NAT_1:13;
then
A15: the LTLold of N2 c= the LTLold of CastNode(L.n,v) by A3,A14,Th31;
N1 = CastNode(L.m,v) by A11,Def16;
then x in the LTLold of N2 by A10,A13,A14,Th30,Th32;
hence thesis by A6,A15;
end;
hence thesis;
end;
theorem Th38:
s2 is_next_of s1 & F in the LTLold of s2 implies ex L,m st 1<=
len(L) & L is_Finseq_for v & L.1 = 'X' s1 & L.(len(L)) = s2 & 1 <= m & m <len(L
) & CastNode(L.(m+1),v) is_succ_of CastNode(L.m,v),F
proof
assume that
A1: s2 is_next_of s1 and
A2: F in the LTLold of s2;
set N1 = 'X' s1;
consider L such that
A3: 1<=len(L) and
A4: L is_Finseq_for v and
A5: L.1 = 'X' s1 & L.(len(L)) = s2 by A1;
set n = len(L);
A6: CastNode(L.1,v) = N1 & CastNode(L.n,v) = s2 by A5,Def16;
1<n by A2,A3,A5,XXREAL_0:1;
then consider m such that
A7: 1<= m & m<n and
A8: ( not F in the LTLold of CastNode(L.m,v))& F in the LTLold of
CastNode(L.(m+1) ,v) by A2,A4,A6,Th27;
set m1 = m+1;
consider N1,N2 such that
A9: N1 = L.m & N2 = L.(m+1) and
A10: N2 is_succ_of N1 by A4,A7;
N1 = CastNode(L.m,v) & N2 = CastNode(L.m1,v) by A9,Def16;
hence thesis by A3,A4,A5,A7,A8,A10,Th28;
end;
theorem Th39:
s2 is_next_of s1 & H is Release & H in the LTLold of s2 & not
the_left_argument_of H in the LTLold of s2 implies the_right_argument_of H in
the LTLold of s2 & H in the LTLnext of s2
proof
set F = the_left_argument_of H;
set G = the_right_argument_of H;
set N1 = 'X' s1;
assume that
A1: s2 is_next_of s1 and
A2: H is Release and
A3: H in the LTLold of s2 and
A4: not F in the LTLold of s2;
consider L,m such that
1<=len(L) and
A5: L is_Finseq_for v and
L.1 = N1 and
A6: L.(len(L)) = s2 and
A7: 1<= m & m <len(L) and
A8: CastNode(L.(m+1),v) is_succ_of CastNode(L.m,v),H by A1,A3,Th38;
set m1 = m+1;
set M2 = CastNode(L.m1,v);
set n = len(L);
A9: CastNode(L.n,v) = s2 by A6,Def16;
set M1 = CastNode(L.m,v);
A10: H in the LTLnew of M1 by A8;
A11: 1<=m1 & m1<=n by A7,NAT_1:13;
then
A12: the LTLnext of M2 c= the LTLnext of s2 by A5,A9,Th31;
the LTLnew of s2 = {} v by Def11;
then
A13: the LTLnew of M2 c= the LTLold of s2 by A5,A9,A11,Th34;
LTLNew2 H = {F,G} by A2,Def2;
then
A14: F in LTLNew2 H by TARSKI:def 2;
A15: now
the LTLold of M1 c= the LTLold of s2 by A5,A7,A9,Th31;
then not F in the LTLold of M1 by A4;
then F in LTLNew2 H \ the LTLold of M1 by A14,XBOOLE_0:def 5;
then
A16: F in ((the LTLnew of M1) \ {H}) \/ (LTLNew2 H \ the LTLold of M1) by
XBOOLE_0:def 3;
assume
A17: M2=SuccNode2(H,M1);
not F in the LTLnew of M2 by A4,A13;
hence contradiction by A10,A17,A16,Def5;
end;
LTLNew1 H = {G} by A2,Def1;
then
A18: G in LTLNew1 H by TARSKI:def 1;
A19: M2 = SuccNode1(H,M1) or (H is disjunctive or H is Until or H is Release
) & M2=SuccNode2(H,M1) by A8;
A20: the LTLold of M2 c= the LTLold of s2 by A5,A9,A11,Th31;
A21: G in the LTLold of s2
proof
now
per cases;
suppose
not G in the LTLold of M1;
then G in LTLNew1 H \ the LTLold of M1 by A18,XBOOLE_0:def 5;
then
G in ((the LTLnew of M1) \ {H}) \/ (LTLNew1 H \ the LTLold of M1)
by XBOOLE_0:def 3;
then G in the LTLnew of M2 by A10,A19,A15,Def4;
hence thesis by A13;
end;
suppose
G in the LTLold of M1;
then G in (the LTLold of M1) \/ {H} by XBOOLE_0:def 3;
then G in the LTLold of M2 by A10,A19,A15,Def4;
hence thesis by A20;
end;
end;
hence thesis;
end;
LTLNext H = {H} by A2,Def3;
then H in LTLNext H by TARSKI:def 1;
then H in (the LTLnext of M1) \/ LTLNext H by XBOOLE_0:def 3;
then H in the LTLnext of M2 by A10,A19,A15,Def4;
hence thesis by A12,A21;
end;
theorem Th40:
s2 is_next_of s1 & H is Release & H in the LTLnext of s1 implies
the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2
proof
set F = the_left_argument_of H;
set G = the_right_argument_of H;
set N1 = 'X' s1;
assume that
A1: s2 is_next_of s1 and
A2: H is Release and
A3: H in the LTLnext of s1;
A4: the LTLnext of s1 c= the LTLold of s2 by A1,Th37;
then consider L,m such that
1<=len(L) and
A5: L is_Finseq_for v and
L.1 = N1 and
A6: L.(len(L)) = s2 and
A7: 1<= m & m <len(L) and
A8: CastNode(L.(m+1),v) is_succ_of CastNode(L.m,v),H by A1,A3,Th38;
A9: the LTLnew of s2 = {} v by Def11;
set M1 = CastNode(L.m,v);
set m1 = m+1;
set M2 = CastNode(L.m1,v);
set n = len(L);
A10: CastNode(L.n,v) = s2 by A6,Def16;
1<=m1 & m1<=n by A7,NAT_1:13;
then
A11: the LTLnew of M2 c= the LTLold of s2 by A5,A10,A9,Th34;
LTLNew2 H = {F,G} by A2,Def2;
then
A12: G in LTLNew2 H by TARSKI:def 2;
LTLNew1 H = {G} by A2,Def1;
then
A13: G in LTLNew1 H by TARSKI:def 1;
A14: the LTLold of M1 c= the LTLold of s2 by A5,A7,A10,Th31;
G in the LTLold of s2
proof
now
per cases;
suppose
G in the LTLold of M1;
hence thesis by A14;
end;
suppose
A15: not G in the LTLold of M1;
now
per cases by A8;
suppose
A16: H in the LTLnew of M1 & M2 = SuccNode1(H,M1);
G in LTLNew1 H \ the LTLold of M1 by A13,A15,XBOOLE_0:def 5;
then
G in ((the LTLnew of M1) \ {H}) \/ (LTLNew1 H \ the LTLold of
M1) by XBOOLE_0:def 3;
then G in the LTLnew of M2 by A16,Def4;
hence thesis by A11;
end;
suppose
A17: H in the LTLnew of M1 & (H is disjunctive or H is Until or
H is Release) & M2=SuccNode2(H,M1);
G in LTLNew2 H \ the LTLold of M1 by A12,A15,XBOOLE_0:def 5;
then
G in ((the LTLnew of M1) \ {H}) \/ (LTLNew2 H \ the LTLold of
M1) by XBOOLE_0:def 3;
then G in the LTLnew of M2 by A17,Def5;
hence thesis by A11;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by A3,A4;
end;
theorem Th41:
s1 is_next_of s0 & H in the LTLold of s1 implies (H is
conjunctive implies the_left_argument_of H in the LTLold of s1 &
the_right_argument_of H in the LTLold of s1) & (H is disjunctive or H is Until
implies the_left_argument_of H in the LTLold of s1 or the_right_argument_of H
in the LTLold of s1) & (H is next implies the_argument_of H in the LTLnext of
s1 ) & (H is Release implies the_right_argument_of H in the LTLold of s1)
proof
assume that
A1: s1 is_next_of s0 and
A2: H in the LTLold of s1;
consider L such that
A3: 1<=len(L) and
A4: L is_Finseq_for v and
A5: L.1 = 'X' s0 and
A6: L.(len(L)) = s1 by A1;
A7: CastNode(L.1,v) = 'X' s0 by A5,Def16;
set n = len(L);
A8: CastNode(L.n,v) = s1 by A6,Def16;
1<n by A2,A3,A5,A6,XXREAL_0:1;
then consider m such that
A9: 1<= m & m<n and
A10: ( not H in the LTLold of CastNode(L.m,v))& H in the LTLold of
CastNode(L.(m+1) ,v) by A2,A4,A8,A7,Th27;
consider N1,N2 such that
A11: N1 = L.m and
A12: N2 = L.(m+1) and
A13: N2 is_succ_of N1 by A4,A9;
A14: CastNode(L.m,v) = N1 by A11,Def16;
then
A15: the LTLold of N1 c= the LTLold of s1 by A4,A8,A9,Th31;
set m1=m+1;
A16: m1<=n & 1<=m1 by A9,NAT_1:13;
A17: CastNode(L.(m+1),v) = N2 by A12,Def16;
then
A18: N2 is_succ_of N1,H by A10,A13,A14,Th28;
the LTLnew of CastNode(L.n,v) = {} v by A8,Def11;
then
A19: the LTLnew of N2 c= the LTLold of s1 by A4,A8,A17,A16,Th34;
A20: H is conjunctive implies the_left_argument_of H in the LTLold of s1 &
the_right_argument_of H in the LTLold of s1
proof
set G = the_right_argument_of H;
set F = the_left_argument_of H;
assume
A21: H is conjunctive;
then
A22: LTLNew1 H = {F,G} by Def1;
now
per cases by A18;
suppose
H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
then
the LTLnew of N2 = ((the LTLnew of N1) \ {H}) \/ (LTLNew1 H \ the
LTLold of N1) by Def4;
then
A23: (LTLNew1 H \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
A24: G in the LTLold of s1
proof
now
per cases;
suppose
G in the LTLold of N1;
hence thesis by A15;
end;
suppose
A25: not G in the LTLold of N1;
G in LTLNew1 H by A22,TARSKI:def 2;
then G in LTLNew1 H \ the LTLold of N1 by A25,XBOOLE_0:def 5;
then G in the LTLnew of N2 by A23;
hence thesis by A19;
end;
end;
hence thesis;
end;
F in the LTLold of s1
proof
now
per cases;
suppose
F in the LTLold of N1;
hence thesis by A15;
end;
suppose
A26: not F in the LTLold of N1;
F in LTLNew1 H by A22,TARSKI:def 2;
then F in LTLNew1 H \ the LTLold of N1 by A26,XBOOLE_0:def 5;
then F in the LTLnew of N2 by A23;
hence thesis by A19;
end;
end;
hence thesis;
end;
hence thesis by A24;
end;
suppose
H in the LTLnew of N1 & (H is disjunctive or H is Until or H
is Release) & N2=SuccNode2(H,N1);
hence thesis by A21,MODELC_2:78;
end;
end;
hence thesis;
end;
A27: H is Release implies the_right_argument_of H in the LTLold of s1
proof
set G = the_right_argument_of H;
set F = the_left_argument_of H;
assume
A28: H is Release;
then
A29: LTLNew2 H = {F,G} by Def2;
A30: LTLNew1 H = {G} by A28,Def1;
now
per cases by A18;
suppose
H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
then
the LTLnew of N2 = ((the LTLnew of N1) \ {H}) \/ (LTLNew1 H \ the
LTLold of N1) by Def4;
then
A31: (LTLNew1 H \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
G in the LTLold of s1
proof
now
per cases;
suppose
G in the LTLold of N1;
hence thesis by A15;
end;
suppose
A32: not G in the LTLold of N1;
G in LTLNew1 H by A30,TARSKI:def 1;
then G in LTLNew1 H \ the LTLold of N1 by A32,XBOOLE_0:def 5;
then G in the LTLnew of N2 by A31;
hence thesis by A19;
end;
end;
hence thesis;
end;
hence thesis;
end;
suppose
H in the LTLnew of N1 & (H is disjunctive or H is Until or H
is Release) & N2=SuccNode2(H,N1);
then
the LTLnew of N2 = ((the LTLnew of N1) \ {H}) \/ (LTLNew2 H \ the
LTLold of N1) by Def5;
then
A33: (LTLNew2 H \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
G in the LTLold of s1
proof
now
per cases;
suppose
G in the LTLold of N1;
hence thesis by A15;
end;
suppose
A34: not G in the LTLold of N1;
G in LTLNew2 H by A29,TARSKI:def 2;
then G in LTLNew2 H \ the LTLold of N1 by A34,XBOOLE_0:def 5;
then G in the LTLnew of N2 by A33;
hence thesis by A19;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
A35: H is disjunctive or H is Until implies the_left_argument_of H in the
LTLold of s1 or the_right_argument_of H in the LTLold of s1
proof
set G = the_right_argument_of H;
set F = the_left_argument_of H;
assume
A36: H is disjunctive or H is Until;
then
A37: LTLNew2 H = {G} by Def2;
A38: LTLNew1 H = {F} by A36,Def1;
now
per cases by A18;
suppose
H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
then
the LTLnew of N2 = ((the LTLnew of N1) \ {H}) \/ (LTLNew1 H \ the
LTLold of N1) by Def4;
then
A39: (LTLNew1 H \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
F in the LTLold of s1
proof
now
per cases;
suppose
F in the LTLold of N1;
hence thesis by A15;
end;
suppose
A40: not F in the LTLold of N1;
F in LTLNew1 H by A38,TARSKI:def 1;
then F in LTLNew1 H \ the LTLold of N1 by A40,XBOOLE_0:def 5;
then F in the LTLnew of N2 by A39;
hence thesis by A19;
end;
end;
hence thesis;
end;
hence thesis;
end;
suppose
H in the LTLnew of N1 & (H is disjunctive or H is Until or H
is Release) & N2=SuccNode2(H,N1);
then
the LTLnew of N2 = ((the LTLnew of N1) \ {H}) \/ (LTLNew2 H \ the
LTLold of N1) by Def5;
then
A41: (LTLNew2 H \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
G in the LTLold of s1
proof
now
per cases;
suppose
G in the LTLold of N1;
hence thesis by A15;
end;
suppose
A42: not G in the LTLold of N1;
G in LTLNew2 H by A37,TARSKI:def 1;
then G in LTLNew2 H \ the LTLold of N1 by A42,XBOOLE_0:def 5;
then G in the LTLnew of N2 by A41;
hence thesis by A19;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
A43: the LTLnext of N2 c= the LTLnext of s1 by A4,A8,A17,A16,Th31;
H is next implies the_argument_of H in the LTLnext of s1
proof
set F = the_argument_of H;
assume
A44: H is next;
then
A45: LTLNext H = {F} by Def3;
now
per cases by A18;
suppose
H in the LTLnew of N1 & N2 = SuccNode1(H,N1);
then the LTLnext of N2 = (the LTLnext of N1) \/ LTLNext H by Def4;
then LTLNext H c= the LTLnext of N2 by XBOOLE_1:7;
then
A46: LTLNext H c= the LTLnext of s1 by A43;
F in LTLNext H by A45,TARSKI:def 1;
hence thesis by A46;
end;
suppose
H in the LTLnew of N1 & (H is disjunctive or H is Until or H
is Release) & N2=SuccNode2(H,N1);
hence thesis by A44,MODELC_2:78;
end;
end;
hence thesis;
end;
hence thesis by A20,A35,A27;
end;
Lm29: s1 is_next_of s0 & s2 is_next_of s1 & F 'U' G in the LTLold of s1
implies G in the LTLold of s1 or F in the LTLold of s1 & F 'U' G in the LTLold
of s2
proof
assume that
A1: s1 is_next_of s0 and
A2: s2 is_next_of s1 and
A3: F 'U' G in the LTLold of s1;
set F1 = F 'U' G;
consider L such that
A4: 1<=len(L) and
A5: L is_Finseq_for v and
A6: L.1 = 'X' s0 and
A7: L.(len(L)) = s1 by A1;
A8: CastNode(L.1,v) = 'X' s0 by A6,Def16;
set n = len(L);
A9: CastNode(L.n,v) = s1 by A7,Def16;
1<n by A3,A4,A6,A7,XXREAL_0:1;
then consider m such that
A10: 1<= m & m<n and
A11: ( not F1 in the LTLold of CastNode(L.m,v))& F1 in the LTLold of
CastNode(L.(m+ 1),v) by A3,A5,A9,A8,Th27;
consider N1,N2 such that
A12: N1 = L.m and
A13: N2 = L.(m+1) and
A14: N2 is_succ_of N1 by A5,A10;
set m1=m+1;
A15: CastNode(L.(m+1),v) = N2 by A13,Def16;
A16: F1 is Until;
then
A17: LTLNext F1 = {F1} by Def3;
the_right_argument_of F1 = G by A16,MODELC_2:def 20;
then
A18: LTLNew2 F1 = {G} by A16,Def2;
the_left_argument_of F1 = F by A16,MODELC_2:def 19;
then
A19: LTLNew1 F1 = {F} by A16,Def1;
A20: CastNode(L.m,v) = N1 by A12,Def16;
then
A21: the LTLold of N1 c= the LTLold of s1 by A5,A9,A10,Th31;
A22: m1<=n & 1<=m1 by A10,NAT_1:13;
then
A23: the LTLnext of N2 c= the LTLnext of s1 by A5,A9,A15,Th31;
the LTLnew of CastNode(L.n,v) = {} v by A9,Def11;
then
A24: the LTLnew of N2 c= the LTLold of s1 by A5,A9,A15,A22,Th34;
A25: N2 is_succ_of N1,F1 by A11,A14,A20,A15,Th28;
not G in the LTLold of s1 implies F in the LTLold of s1 & F 'U' G in
the LTLold of s2
proof
assume
A26: not G in the LTLold of s1;
now
per cases by A25;
suppose
A27: F1 in the LTLnew of N1 & N2 = SuccNode1(F1,N1);
then the LTLnew of N2 = ((the LTLnew of N1) \ {F1}) \/ (LTLNew1 F1 \
the LTLold of N1) by Def4;
then
A28: (LTLNew1 F1 \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
A29: F in the LTLold of s1
proof
now
per cases;
suppose
F in the LTLold of N1;
hence thesis by A21;
end;
suppose
A30: not F in the LTLold of N1;
F in LTLNew1 F1 by A19,TARSKI:def 1;
then F in LTLNew1 F1 \ the LTLold of N1 by A30,XBOOLE_0:def 5;
then F in the LTLnew of N2 by A28;
hence thesis by A24;
end;
end;
hence thesis;
end;
the LTLnext of N2 = (the LTLnext of N1) \/ LTLNext F1 by A27,Def4;
then
A31: LTLNext F1 c= the LTLnext of N2 by XBOOLE_1:7;
F1 in LTLNext F1 by A17,TARSKI:def 1;
then F1 in the LTLnext of N2 by A31;
then
A32: F1 in the LTLnext of s1 by A23;
the LTLnext of s1 c= the LTLold of s2 by A2,Th37;
hence thesis by A29,A32;
end;
suppose
F1 in the LTLnew of N1 & (F1 is disjunctive or F1 is Until or
F1 is Release) & N2=SuccNode2(F1,N1);
then the LTLnew of N2 = ((the LTLnew of N1) \ {F1}) \/ (LTLNew2 F1 \
the LTLold of N1) by Def5;
then
A33: (LTLNew2 F1 \ the LTLold of N1) c= the LTLnew of N2 by XBOOLE_1:7;
G in the LTLold of s1
proof
now
per cases;
suppose
G in the LTLold of N1;
hence thesis by A21;
end;
suppose
A34: not G in the LTLold of N1;
G in LTLNew2 F1 by A18,TARSKI:def 1;
then G in LTLNew2 F1 \ the LTLold of N1 by A34,XBOOLE_0:def 5;
then G in the LTLnew of N2 by A33;
hence thesis by A24;
end;
end;
hence thesis;
end;
hence thesis by A26;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 & H is
Until implies the_right_argument_of H in the LTLold of s1 or
the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2
proof
assume that
A1: s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 and
A2: H is Until;
set G = the_right_argument_of H;
set F = the_left_argument_of H;
H = F 'U' G by A2,MODELC_2:8;
hence thesis by A1,Lm29;
end;
definition
let v;
func LTLNodes(v) -> non empty set means
:Def30:
for x being object
holds 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[object, object] 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 object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z being object such that
A2: P[x,y] and
A3: P[x,z];
consider y1,y2,y3 being Subset of Subformulae v, N1 being strict LTLnode
over v such that
A4: x = [[y1,y2],y3] and
A5: y = N1 & the LTLold of N1 = y1 & the LTLnew of N1 = y2 & the
LTLnext of N1 = y3 by A2;
consider z1,z2,z3 being Subset of Subformulae v, N2 being strict LTLnode
over v such that
A6: x = [[z1,z2],z3] and
A7: z = N2 & the LTLold of N2 = z1 & the LTLnew of N2 = z2 & the
LTLnext of N2 = z3 by A3;
A8: y3=z3 by A4,A6,XTUPLE_0:1;
A9: [y1,y2]= [z1,z2] by A4,A6,XTUPLE_0:1;
then y1=z1 by XTUPLE_0:1;
hence thesis by A5,A7,A9,A8,XTUPLE_0:1;
end;
consider IT being set such that
A10: for x being object holds x in IT iff
ex y being object 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 A10;
end;
then reconsider IT as non empty set;
A11: for x being object holds
(ex N being strict LTLnode over v st x=N) implies x in IT
proof let x be object;
assume ex N being strict LTLnode over v st x=N;
then consider N being strict LTLnode over v such that
A12: x = N;
set y3 = the LTLnext of N;
set y2 = the LTLnew of N;
set y1 = the LTLold 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 A10,A12;
end;
take IT;
for x being object holds
x in IT implies ex N being strict LTLnode over v st x=N
proof let x be object;
assume x in IT;
then ex y being object st y in Y & P[y,x] by A10;
hence thesis;
end;
hence thesis by A11;
end;
uniqueness
proof
let X,Y being non empty set;
(for x being object
holds x in X iff ex N being strict LTLnode over v st x=N) & (
for x being object
holds x in Y iff ex N being strict LTLnode over v st x=N) implies X = Y
proof
assume that
A13: for x being object
holds x in X iff ex N being strict LTLnode over v st x=N and
A14: for x being object
holds x in Y iff ex N being strict LTLnode over v st x=N;
for x being object holds x in X iff x in Y
proof
let x be object;
x in X iff ex N being strict LTLnode over v st x=N by A13;
hence thesis by A14;
end;
hence thesis by TARSKI:2;
end;
hence thesis;
end;
end;
registration
let v;
cluster LTLNodes(v) -> finite;
correctness
proof
deffunc F(set) = [ [the LTLold of CastNode($1,v), the LTLnew of CastNode(
$1,v) ], the LTLnext of CastNode($1,v) ];
set X = bool Subformulae v;
set LN = LTLNodes(v);
set Y = [:X,X,X:];
A1: for x st x in LN holds F(x) in Y
proof
let x;
set N1 = the LTLold of CastNode(x,v);
set N2 = the LTLnew of CastNode(x,v);
assume x in LN;
set M1 = [N1,N2];
set X1 = [:X,X:];
Y =[:X1,X:] & M1 in X1 by ZFMISC_1:87,def 3;
hence thesis by ZFMISC_1:87;
end;
ex f being Function of LN,Y st for x st x in LN holds f.x = F(x) from
FUNCT_2:sch 11(A1);
then consider f being Function of LN,Y such that
A2: for x st x in LN holds f.x = F(x);
for x1,x2 be object st x1 in LN & x2 in LN & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A3: x1 in LN and
A4: x2 in LN and
A5: f.x1 = f.x2;
A6: ex Nx2 being strict LTLnode over v st x2=Nx2 by A4,Def30;
set Nx23 = the LTLnext of CastNode(x2,v);
set Nx22 = the LTLnew of CastNode(x2,v);
set Nx21 = the LTLold of CastNode(x2,v);
A7: ex Nx1 being strict LTLnode over v st x1=Nx1 by A3,Def30;
reconsider x2 as strict LTLnode over v by A6;
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];
set Mx2 = [Nx21,Nx22];
A8: Nx22 = the LTLnew of x2 & Nx23 = the LTLnext of x2 by Def16;
reconsider x1 as strict LTLnode over v by A7;
A9: f.x1 = [Mx1,Nx13] & f.x2 = [Mx2,Nx23] by A2,A3,A4;
then
A10: Nx13 = Nx23 by A5,XTUPLE_0:1;
A11: Nx13 = the LTLnext of x1 & Nx21 = the LTLold of x2 by Def16;
A12: Nx11 = the LTLold of x1 & Nx12 = the LTLnew of x1 by Def16;
A13: Mx1 =Mx2 by A5,A9,XTUPLE_0:1;
then Nx11 = Nx21 by XTUPLE_0:1;
hence thesis by A12,A11,A8,A13,A10,XTUPLE_0:1;
end;
then
A14: f is one-to-one by FUNCT_2:19;
rng f is finite;
then dom (f") is finite by A14,FUNCT_1:33;
then dom f = LN & rng (f") is finite by FINSET_1:8,FUNCT_2:def 1;
hence thesis by A14,FUNCT_1:33;
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 Def30;
then init v in IT;
hence thesis;
end;
end;
registration
let v;
cluster LTLStates(v) -> finite;
correctness
proof
LTLStates(v) c= LTLNodes(v)
proof
let a be object;
assume a in LTLStates(v);
then ex x being Element of LTLNodes(v) st a=x & x is elementary strict
LTLnode over v;
hence thesis;
end;
hence thesis;
end;
end;
theorem
init v is Element of LTLStates(v)
proof
init v is Element of LTLNodes(v) by Def30;
then init v in LTLStates(v);
hence thesis;
end;
theorem Th44:
s is Element of LTLStates(v)
proof
s is Element of LTLNodes(v) by Def30;
then s in LTLStates(v);
hence thesis;
end;
theorem Th45:
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
A1: y=x and
A2: y is elementary strict LTLnode over v;
reconsider y as elementary strict LTLnode over v by A2;
take y;
thus thesis by A1;
end;
hence thesis by Th44;
end;
Lm30: X<>{} & X c= Seg n implies ex k st 1<=k & k<=n & k in X & for i st 1<=i &
i<k holds not i in X
proof
defpred P[Nat] means for X st X<>{} & X c= Seg $1 holds ex k st 1<=k & k<=$1
& k in X & for i st 1<=i & i<k holds not i in X;
A1: for m st P[m] holds P[m + 1]
proof
let m such that
A2: P[m];
set m1=m+1;
A3: Y<>{} & Y c= Seg m1 & not m1 in Y implies Y c= Seg m
proof
assume that
Y<>{} and
A4: Y c= Seg m1 and
A5: not m1 in Y;
Y c= Seg m
proof
let x be object;
assume
A6: x in Y;
then x in Seg m1 by A4;
then x in { j where j is Nat :1 <= j & j <= m1 } by FINSEQ_1:def 1;
then consider j being Nat such that
A7: x=j and
A8: 1 <= j and
A9: j <= m1;
j <m1 by A5,A6,A7,A9,XXREAL_0:1;
then j<=m by NAT_1:13;
hence thesis by A7,A8,FINSEQ_1:1;
end;
hence thesis;
end;
for X st X<>{} & X c= Seg m1 holds ex k st 1<=k & k<=m1 & k in X &
for i st 1<=i & i<k holds not i in X
proof
let X such that
A10: X<>{} and
A11: X c= Seg m1;
now
per cases;
suppose
not m1 in X;
then X c= Seg m by A3,A11;
then consider k such that
A12: 1<=k and
A13: k<= m and
A14: k in X & for i st 1<=i & i<k holds not i in X by A2,A10;
m<=m1 by NAT_1:11;
then k <= m1 by A13,XXREAL_0:2;
hence thesis by A12,A14;
end;
suppose
A15: m1 in X;
set X1 = X \ {m1};
m1 in {m1} by TARSKI:def 1;
then
A16: not m1 in X1 by XBOOLE_0:def 5;
A17: X1 c= Seg m1 by A11;
now
per cases;
suppose
A18: X1 <> {};
X1 c= Seg m by A3,A16,A17;
then consider k such that
A19: 1<=k and
A20: k<=m and
A21: k in X1 and
A22: for i st 1<=i & i<k holds not i in X1 by A2,A18;
m<=m1 by NAT_1:11;
then
A23: k <= m1 by A20,XXREAL_0:2;
for i st 1<=i & i<k holds not i in X
proof
let i;
assume 1<=i & i<k;
then (not i in {m1})& not i in X1 by A22,A23,TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by A19,A21,A23;
end;
suppose
X1 = {};
then X c= {m1} by XBOOLE_1:37;
then 1<=m1 & for i st 1<=i & i<m1 holds not i in X by NAT_1:11
,TARSKI:def 1;
hence thesis by A15;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
A24: P[0];
for m holds P[m] from NAT_1:sch 2 (A24,A1);
hence thesis;
end;
definition
let v;
let w;
let f be Function;
pred f is_succ_homomorphism v,w means
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);
pred f is_homomorphism v,w means
for x st x in LTLNodes(v) & CastNode
(x,v) is non elementary & w |= *CastNode(x,v) holds w |= *CastNode(f.x,v);
end;
theorem
for f being Function of LTLNodes(v),LTLNodes(v) st f
is_succ_homomorphism v,w holds f is_homomorphism v,w;
theorem Th47:
for f being Function of LTLNodes(v),LTLNodes(v) st f
is_homomorphism v,w holds for x st x in LTLNodes(v) & CastNode(x,v) is non
elementary & w |= *CastNode(x,v) holds for k st (for i st i<=k holds CastNode((
f|**i).x,v) is non elementary) holds w |= *CastNode((f|**k).x,v)
proof
set LN = LTLNodes(v);
let f be Function of LN,LN;
assume f is_homomorphism v,w;
then
A1: for y st y in LN & CastNode(y,v) is non elementary & w |= *CastNode(y,v)
holds w |= *CastNode(f.y,v);
for x st x in LN & CastNode(x,v) is non elementary & w |= *CastNode(x,v)
holds for k st (for i st i<=k holds CastNode((f|**i).x,v) is non elementary)
holds w |= *CastNode((f|**k).x,v)
proof
let x such that
A2: x in LN and
CastNode(x,v) is non elementary and
A3: w |= *CastNode(x,v);
for k st (for i st i<=k holds CastNode((f|**i).x,v) is non elementary)
holds w |= *CastNode((f|**k).x,v)
proof
defpred P[Nat] means (for i st i<=$1 holds CastNode((f|**i).x,v) is non
elementary) implies w |= *CastNode((f|**$1).x,v);
A4: for m st P[m] holds P[m+1]
proof
let m;
assume
A5: P[m];
P[m+1]
proof
set y = (f|**m).x;
A6: m<=m+1 by NAT_1:13;
A7: (f|**(m+1)).x = (f*(f|**m)).x by FUNCT_7:71
.= f.y by A2,FUNCT_2:15;
assume for i st i<=m+1 holds CastNode((f|**i).x,v) is non elementary;
then CastNode(y,v) is non elementary & w |= *CastNode(y,v) by A5,A6,
XXREAL_0:2;
hence thesis by A1,A2,A7,FUNCT_2:5;
end;
hence thesis;
end;
A8: P[0]
proof
assume for i st i<=0 holds CastNode((f|**i).x,v) is non elementary;
f|**0 = id LN by FUNCT_7:84;
hence thesis by A2,A3,FUNCT_1:18;
end;
A9: for m holds P[m] from NAT_1:sch 2 (A8,A4);
let k;
assume for i st i<=k holds CastNode((f|**i).x,v) is non elementary;
hence thesis by A9;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th48:
for f being Function of LTLNodes(v),LTLNodes(v) st f
is_succ_homomorphism v,w holds for x st x in LTLNodes(v) & CastNode(x,v) is non
elementary & w |= *CastNode(x,v) holds for k st (for i st i<=k holds CastNode((
f|**i).x,v) is non elementary) holds CastNode((f|**(k+1)).x,v) is_succ_of
CastNode((f|**k).x,v) & w |= *CastNode((f|**k).x,v)
proof
set LN = LTLNodes(v);
let f be Function of LN,LN;
assume
A1: f is_succ_homomorphism v,w;
then
A2: f is_homomorphism v,w;
for x st x in LN & CastNode(x,v) is non elementary & w |= *CastNode(x,v)
holds for k st (for i st i<=k holds CastNode((f|**i).x,v) is non elementary)
holds CastNode((f|**(k+1)).x,v) is_succ_of CastNode((f|**k).x,v) & w |= *
CastNode((f|**k).x,v)
proof
let x such that
A3: x in LN and
A4: CastNode(x,v) is non elementary & w |= *CastNode(x,v);
for k st (for i st i<=k holds CastNode((f|**i).x,v) is non elementary)
holds CastNode((f|**(k+1)).x,v) is_succ_of CastNode((f|**k).x,v) & w |= *
CastNode((f|**k).x,v)
proof
let k such that
A5: for i st i<=k holds CastNode((f|**i).x,v) is non elementary;
set y = (f|**k).x;
A6: y in LN by A3,FUNCT_2:5;
A7: (f|**(k+1)).x = (f*(f|**k)).x by FUNCT_7:71
.= f.y by A3,FUNCT_2:15;
CastNode(y,v) is non elementary & w |= *CastNode(y,v) by A2,A3,A4,A5,Th47
;
hence thesis by A1,A6,A7;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th49:
for f being Function of LTLNodes(v),LTLNodes(v) st f
is_succ_homomorphism v,w holds for x st x in LTLNodes(v) & CastNode(x,v) is non
elementary & w |= *CastNode(x,v) holds ex n st (for i st i<n holds CastNode((f
|**i).x,v) is non elementary) & CastNode((f|**n).x,v) is elementary
proof
set LN = LTLNodes(v);
let f be Function of LN,LN;
assume
A1: f is_succ_homomorphism v,w;
for x st x in LN & CastNode(x,v) is non elementary & w |= *CastNode(x,v)
holds ex n st (for i st i<n holds CastNode((f|**i).x,v) is non elementary) &
CastNode((f|**n).x,v) is elementary
proof
let x such that
A2: x in LN and
A3: CastNode(x,v) is non elementary and
A4: w |= *CastNode(x,v);
deffunc F(set) = (f|**CastNat($1)).x;
set len1=len(CastNode(f.x,v))+1;
0<0+len1;
then
A5: 1<=len1 by NAT_1:19;
reconsider len1 as Nat;
consider L such that
A6: len(L) =len1 & for k being Nat st k in dom L holds L.k=F(k) from
FINSEQ_1:sch 2;
set X ={m where m is Element of NAT: 1<=m & m<=len1 & CastNode((f|**m).x,v
) is elementary};
A7: Seg len1 = dom L by A6,FINSEQ_1:def 3;
A8: for k st 1<= k & k<=len(L) holds L.k= (f|**k).x
proof
let k;
assume 1<= k & k<=len(L);
then k in Seg len1 by A6,FINSEQ_1:1;
then L.k = (f|**CastNat(k)).x by A6,A7;
hence thesis by MODELC_2:def 1;
end;
A9: now
assume
A10: X = {};
A11: for k st 1<=k & k<=len(L) holds CastNode((f|**k).x,v) is non elementary
proof
let k such that
A12: 1<=k & k<=len(L);
reconsider k as Element of NAT by ORDINAL1:def 12;
not k in X by A10;
hence thesis by A6,A12;
end;
A13: for k st 1<= k & k<len(L) holds CastNode((f|**(k+1)).x,v) is_succ_of
CastNode((f|**k).x,v)
proof
let k such that
1<=k and
A14: k<len(L);
for i st i<=k holds CastNode((f|**i).x,v) is non elementary
proof
let i;
assume i<=k;
then
A15: i < len(L) by A14,XXREAL_0:2;
now
per cases by Lm6;
suppose
1<=i;
hence thesis by A11,A15;
end;
suppose
i = 0;
then f|**i = id LN by FUNCT_7:84;
hence thesis by A2,A3,FUNCT_1:18;
end;
end;
hence thesis;
end;
hence thesis by A1,A2,A3,A4,Th48;
end;
for m st 1 <= m & m < len(L) holds ex N,M st N = L.m & M=L.(m+1) &
M is_succ_of N
proof
let m such that
A16: 1 <= m & m < len(L);
set M = L.(m+1);
1<=m+1 & m+1<=len(L) by A16,NAT_1:13;
then
A17: M=(f|**(m+1)).x by A8;
then M in LN by A2,FUNCT_2:5;
then
A18: ex M1 being strict LTLnode over v st M=M1 by Def30;
set N = L.m;
A19: N=(f|**m).x by A8,A16;
then N in LN by A2,FUNCT_2:5;
then
A20: ex N1 being strict LTLnode over v st N=N1 by Def30;
reconsider M as strict LTLnode over v by A18;
reconsider N as strict LTLnode over v by A20;
CastNode(N,v) = N & CastNode(M,v) = M by Def16;
hence thesis by A13,A16,A19,A17;
end;
then L is_Finseq_for v;
then len(CastNode(L.len1,v)) <= len(CastNode(L.1,v)) -len1+1 by A5,A6
,Th36;
then len(CastNode(L.len1,v))<=len(CastNode((f|**1).x,v)) -len1+1 by A5,A6
,A8;
then len(CastNode(L.len1,v)) <= len(CastNode(f.x,v)) -len1 +1 by
FUNCT_7:70;
then len(CastNode((f|**len1).x,v)) <= 0 by A5,A6,A8;
then the LTLnew of CastNode((f|**len1).x,v) = {}v by Th22;
then CastNode((f|**len1).x,v) is elementary;
then len1 in X by A5;
hence contradiction by A10;
end;
X c= Seg len1
proof
let y be object;
assume y in X;
then
ex m being Element of NAT st y = m & 1<=m & m<=len1 & CastNode((f|**
m).x,v) is elementary;
hence thesis by FINSEQ_1:1;
end;
then consider n such that
1<=n and
A21: n<=len1 and
A22: n in X and
A23: for i st 1<=i & i<n holds not i in X by A9,Lm30;
A24: for i st i<n holds CastNode((f|**i).x,v) is non elementary
proof
let i such that
A25: i<n;
now
per cases by Lm6;
suppose
i=0;
then f|**i = id LN by FUNCT_7:84;
hence thesis by A2,A3,FUNCT_1:18;
end;
suppose
A26: 1<=i;
then
A27: not i in X by A23,A25;
now
assume
A28: CastNode((f|**i).x,v) is elementary;
reconsider i as Element of NAT by ORDINAL1:def 12;
i<len1 by A21,A25,XXREAL_0:2;
hence contradiction by A26,A27,A28;
end;
hence thesis;
end;
end;
hence thesis;
end;
CastNode((f|**n).x,v) is elementary
proof
ex m being Element of NAT st n=m & 1<=m & m<=len1 & CastNode((f|**m)
.x,v) is elementary by A22;
hence thesis;
end;
hence thesis by A24;
end;
hence thesis;
end;
theorem Th50:
for f being Function of LTLNodes(v),LTLNodes(v) st f
is_homomorphism v,w holds for x st x in LTLNodes(v) & CastNode(x,v) is non
elementary holds for k st CastNode((f|**k).x,v) is non elementary & w |= *
CastNode((f|**k).x,v) holds w |= *CastNode((f|**(k+1)).x,v)
proof
set LN = LTLNodes(v);
let f be Function of LN,LN;
assume
A1: f is_homomorphism v,w;
for x st x in LN & CastNode(x,v) is non elementary holds for k st
CastNode((f|**k).x,v) is non elementary & w |= *CastNode((f|**k).x,v) holds w
|= *CastNode((f|**(k+1)).x,v)
proof
let x such that
A2: x in LN and
CastNode(x,v) is non elementary;
for k st CastNode((f|**k).x,v) is non elementary & w |= *CastNode((f
|**k).x,v) holds w |= *CastNode((f|**(k+1)).x,v)
proof
let k such that
A3: CastNode((f|**k).x,v) is non elementary & w |= *CastNode((f|**k) .x,v);
set y = (f|**k).x;
A4: (f|**(k+1)).x = (f*(f|**k)).x by FUNCT_7:71
.= f.y by A2,FUNCT_2:15;
y in LN by A2,FUNCT_2:5;
hence thesis by A1,A3,A4;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th51:
for f being Function of LTLNodes(v),LTLNodes(v) st f
is_succ_homomorphism v,w holds for x st x in LTLNodes(v) & CastNode(x,v) is non
elementary & w |= *CastNode(x,v) holds ex n st (for i st i<n holds CastNode((f
|**i).x,v) is non elementary & CastNode((f|**(i+1)).x,v) is_succ_of CastNode((f
|**i).x,v)) & CastNode((f|**n).x,v) is elementary & for i st i<=n holds w |= *
CastNode((f|**i).x,v)
proof
set LN = LTLNodes(v);
let f be Function of LN,LN;
assume
A1: f is_succ_homomorphism v,w;
then
for y st y in LN & CastNode(y,v) is non elementary & w |= *CastNode(y,v)
holds w |= *CastNode(f.y,v);
then
A2: f is_homomorphism v,w;
for x st x in LTLNodes(v) & CastNode(x,v) is non elementary & w |= *
CastNode(x,v) holds ex n st (for i st i<n holds CastNode((f|**i).x,v) is non
elementary & CastNode((f|**(i+1)).x,v) is_succ_of CastNode((f|**i).x,v)) &
CastNode((f|**n).x,v) is elementary & for i st i<=n holds w |= *CastNode((f|**i
).x,v)
proof
let x such that
A3: x in LN and
A4: CastNode(x,v) is non elementary and
A5: w |= *CastNode(x,v);
consider n such that
A6: for i st i<n holds CastNode((f|**i).x,v) is non elementary and
A7: CastNode((f|**n).x,v) is elementary by A1,A3,A4,A5,Th49;
for i st i<n holds CastNode((f|**(i+1)).x,v) is_succ_of CastNode((f|**
i).x,v)
proof
let i;
assume
A8: i<n;
for j st j<=i holds CastNode((f|**j).x,v) is non elementary
proof
let j;
assume j<=i;
then j<n by A8,XXREAL_0:2;
hence thesis by A6;
end;
hence thesis by A1,A3,A4,A5,Th48;
end;
then
A9: for i st i<n holds CastNode((f|**i).x,v) is non elementary & CastNode(
(f|**(i+1)).x,v) is_succ_of CastNode((f|**i).x,v) by A6;
defpred P[Nat] means $1<=n implies for i st i<=$1 holds w |= *CastNode((f
|**i).x,v);
A10: for m st P[m] holds P[m+1]
proof
let m;
assume
A11: P[m];
P[m+1]
proof
assume
A12: m+1<=n;
then
A13: m<n by NAT_1:13;
then
A14: CastNode((f|**m).x,v) is non elementary by A6;
for i st i<=m+1 holds w |= *CastNode((f|**i).x,v)
proof
let i;
w |= *CastNode((f|**m).x,v) by A11,A12,NAT_1:13;
then
A15: w |= *CastNode((f|**(m+1)).x,v) by A2,A3,A4,A14,Th50;
assume i<=m+1;
hence thesis by A11,A13,A15,NAT_1:8;
end;
hence thesis;
end;
hence thesis;
end;
A16: P[0]
proof
assume 0<=n;
for i st i<=0 holds w |= *CastNode((f|**i).x,v)
proof
let i;
assume i<=0;
then i=0;
then f|**i = id LN by FUNCT_7:84;
hence thesis by A3,A5,FUNCT_1:18;
end;
hence thesis;
end;
for m holds P[m] from NAT_1:sch 2 (A16,A10);
then for i st i<=n holds w |= *CastNode((f|**i).x,v);
hence thesis by A7,A9;
end;
hence thesis;
end;
reserve q for sequence of LTLStates(v);
theorem Th52:
ex s st s = CastNode(q.n,v)
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
consider s such that
A1: s=q.n by Th45;
CastNode(q.n,v) = s by A1,Def16;
hence thesis;
end;
Lm31: F 'U' G in the LTLold of CastNode(q.1,v) & (for i holds CastNode(q.(i+1)
,v) is_next_of CastNode(q.i,v)) implies ((for i st 1<=i & i<n holds not G in
the LTLold of CastNode(q.i,v)) implies for i st 1<=i & i<n holds F in the
LTLold of CastNode(q.i,v) & F 'U' G in the LTLold of CastNode(q.i,v) )
proof
deffunc Node(Nat) = CastNode(q.$1,v);
assume that
A1: F 'U' G in the LTLold of Node(1) and
A2: for i holds Node(i+1) is_next_of Node(i);
defpred P[Nat] means (for i st 1<=i & i<$1 holds not G in the LTLold of Node
(i)) implies (for i st 1<=i & i<$1 holds (F in the LTLold of Node(i)) & (F 'U'
G in the LTLold of Node(i)));
A3: for k st P[k] holds P[k + 1]
proof
let k such that
A4: P[k];
set k1=k+1;
(for i st 1<=i & i<k1 holds not G in the LTLold of Node(i)) implies
for i st 1<=i & i<k1 holds F in the LTLold of Node(i) & F 'U' G in the LTLold
of Node(i)
proof
assume
A5: for i st 1<=i & i<k1 holds not G in the LTLold of Node(i);
A6: k<=k1 by NAT_1:11;
A7: for i st 1<=i & i<k holds not G in the LTLold of Node(i)
proof
let i such that
A8: 1<=i and
A9: i<k;
i<k1 by A6,A9,XXREAL_0:2;
hence thesis by A5,A8;
end;
for i st 1<=i & i<k1 holds F in the LTLold of Node(i) & F 'U' G in
the LTLold of Node(i)
proof
let i such that
A10: 1<=i and
A11: i<k1;
A12: i<=k by A11,NAT_1:13;
now
per cases by A12,XXREAL_0:1;
suppose
i < k;
hence thesis by A4,A7,A10;
end;
suppose
A13: i = k;
now
per cases by A10,A13,XXREAL_0:1;
suppose
A14: k=1;
A15: Node(0+1) is_next_of Node(0) & Node(1+1) is_next_of Node(
1) by A2;
consider s1 such that
A16: s1 = Node(1) by Th52;
not G in the LTLold of s1 by A5,A14,A16;
hence thesis by A1,A13,A14,A16,A15,Lm29;
end;
suppose
A17: 1<k;
set m = k-1;
reconsider m as Nat by A17,NAT_1:20;
set m1 = m-1;
1<m+1 by A17;
then
A18: 1<= m by NAT_1:13;
then reconsider m1 as Nat by NAT_1:21;
consider sm be elementary strict LTLnode over v such that
A19: sm = Node(m) by Th52;
A20: m < m+1 by NAT_1:19;
then m<k1 by A6,XXREAL_0:2;
then
A21: not G in the LTLold of sm by A5,A18,A19;
A22: (ex sk1 be elementary strict LTLnode over v st sk1 = Node
( k1) )& Node(m+1) is_next_of Node(m) by A2,Th52;
A23: (ex sm1 be elementary strict LTLnode over v st sm1 = Node
( m1) )& Node(m1+1) is_next_of Node(m1) by A2,Th52;
A24: Node(m+1) is_next_of Node(m) by A2;
A25: Node(k+1) is_next_of Node(k) by A2;
consider sk be elementary strict LTLnode over v such that
A26: sk = Node(k) by Th52;
A27: not G in the LTLold of sk by A5,A10,A11,A13,A26;
F 'U' G in the LTLold of sm by A4,A7,A18,A19,A20;
then F 'U' G in the LTLold of sk by A19,A26,A21,A23,A24,Lm29;
hence thesis by A13,A26,A27,A22,A25,Lm29;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A28: P[0];
for n holds P[n] from NAT_1:sch 2 (A28,A3);
hence thesis;
end;
theorem
H is Until & H in the LTLold of CastNode(q.1,v) & (for i holds
CastNode(q.(i+1),v) is_next_of CastNode(q.i,v)) implies ((for i st 1<=i & i<n
holds not the_right_argument_of H in the LTLold of CastNode(q.i,v)) implies for
i st 1<=i & i<n holds the_left_argument_of H in the LTLold of CastNode(q.i,v) &
H in the LTLold of CastNode(q.i,v) )
proof
deffunc Node(Nat) = CastNode(q.$1,v);
assume that
A1: H is Until and
A2: H in the LTLold of Node(1) & for i holds Node(i+1) is_next_of Node(i );
set G = the_right_argument_of H;
set F = the_left_argument_of H;
H = F 'U' G by A1,MODELC_2:8;
hence thesis by A2,Lm31;
end;
Lm32: F 'U' G in the LTLold of CastNode(q.1,v) & (for i holds CastNode(q.(i+1)
,v) is_next_of CastNode(q.i,v)) implies (for i st 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<j holds F 'U' G in the LTLold of CastNode(q.i,v) & F
in the LTLold of CastNode(q.i,v)
proof
deffunc Node(Nat) = CastNode(q.$1,v);
assume
A1: F 'U' G in the LTLold of Node(1) & for i holds Node(i+1) is_next_of
Node(i);
not (for i st 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<j holds F 'U' G in the LTLold of
Node(i) & F in the LTLold of Node(i)
proof
assume not (for i st 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
A2: k>=1 and
A3: 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;
ex m st 1<=m & m<=k & G in the LTLold of Node(m)
proof
now
per cases by A3;
suppose
A4: not (F 'U' G in the LTLold of Node(k) & F in the LTLold of Node(k) );
now
assume
A5: not ex m st 1<=m & m<=k & G in the LTLold of Node(m);
A6: for m st 1<=m & m<k1 holds not G in the LTLold of Node(m)
proof
let m such that
A7: 1<=m and
A8: m<k1;
m<=k by A8,NAT_1:13;
hence thesis by A5,A7;
end;
k<k1 by NAT_1:13;
hence contradiction by A1,A2,A4,A6,Lm31;
end;
hence thesis;
end;
suppose
G in the LTLold of Node(k);
hence thesis by A2;
end;
end;
hence thesis;
end;
then consider m0 such that
A9: 1<=m0 & m0<=k & G in the LTLold of Node(m0);
set X = {m where m is Element of NAT :1<=m & m<=k & G in the LTLold of
Node(m)};
A10: X c= Seg k
proof
let x be object;
assume x in X;
then ex m being Element of NAT st x = m & 1<=m & m<=k & G in the LTLold
of Node(m);
hence thesis by FINSEQ_1:1;
end;
reconsider m0 as Element of NAT by ORDINAL1:def 12;
m0 in X by A9;
then consider j such that
1<=j and
A11: j<=k and
A12: j in X and
A13: for i st 1<=i & i<j holds not i in X by A10,Lm30;
for i st 1<=i & i<j holds not G in the LTLold of Node(i)
proof
let i such that
A14: 1<=i and
A15: i<j;
A16: i<k by A11,A15,XXREAL_0:2;
reconsider i as Element of NAT by ORDINAL1:def 12;
not i in X by A13,A14,A15;
hence thesis by A14,A16;
end;
then
A17: for i st 1<=i & i<j holds F 'U' G in the LTLold of Node(i) & F in the
LTLold of Node(i) by A1,Lm31;
j>=1 & G in the LTLold of Node(j)
proof
ex m being Element of NAT st j = m & 1<=m & m<=k & G in the LTLold
of Node(m) by A12;
hence thesis;
end;
hence thesis by A17;
end;
hence thesis;
end;
theorem Th54:
H is Until & H in the LTLold of CastNode(q.1,v) & (for i holds
CastNode(q.(i+1),v) is_next_of CastNode(q.i,v)) implies (for i st 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<j holds H in the LTLold of CastNode(q.i,v) &
the_left_argument_of H in the LTLold of CastNode(q.i,v)
proof
deffunc Node(Nat) = CastNode(q.$1,v);
assume that
A1: H is Until and
A2: H in the LTLold of Node(1) & for i holds Node(i+1) is_next_of Node(i );
set G = the_right_argument_of H;
set F = the_left_argument_of H;
H = F 'U' G by A1,MODELC_2:8;
hence thesis by A2,Lm32;
end;
::some properties for choice function
theorem Th55:
union BOOL X = X
proof
{} c= X;
then BOOL X = bool X \ {{}} & {{}} c= bool X by ORDERS_1:def 3,ZFMISC_1:31;
then
A1: BOOL X \/ {{}} c= bool X by XBOOLE_1:8;
BOOL X \/ {{}} = (bool X \{{}}) \/{{}} by ORDERS_1:def 3
.= bool X \/{{}} by XBOOLE_1:39;
then bool X c= BOOL X \/ {{}} by XBOOLE_1:7;
then
A2: bool X = BOOL X \/ {{}} by A1,XBOOLE_0:def 10;
X = union bool X by ZFMISC_1:81
.= union BOOL X \/ union {{}} by A2,ZFMISC_1:78
.= union BOOL X \/ {} by ZFMISC_1:25;
hence thesis;
end;
theorem Th56:
N is non elementary implies the LTLnew of N <> {} & the LTLnew
of N in BOOL Subformulae v
by ORDERS_1:2;
registration
let v;
cluster union BOOL Subformulae v -> non empty;
correctness by Th55;
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
take f = the Choice_Function of BOOL Subformulae v;
A1: not {} in BOOL Subformulae v by ORDERS_1:1;
union BOOL Subformulae v = Subformulae v by Th55;
hence f is Function of BOOL Subformulae v,Subformulae v by ORDERS_1:90,A1;
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
:Def34:
U.(the LTLnew of N);
correctness
proof
set x = the LTLnew of N;
set a = U.x;
not {} in BOOL Subformulae v by ORDERS_1:1;
then
A2: U is Function of BOOL Subformulae v, union BOOL Subformulae v
by ORDERS_1:90;
x in BOOL Subformulae v by A1,Th56;
then U.x in union BOOL Subformulae v by FUNCT_2:5,A2;
then a in Subformulae v by Th55;
then ex F st F = a & F is_subformula_of v by MODELC_2:def 24;
hence thesis;
end;
end;
theorem Th58:
N is non elementary implies chosen_formula(U,N) in the LTLnew of N
proof
set x = the LTLnew of N;
set X = BOOL Subformulae v;
assume
A1: not N is elementary;
then ( not {} in X)& x in X by Th56,ORDERS_1:1;
then U.x in x by ORDERS_1:89;
hence thesis by A1,Def34;
end;
definition
let w;
let v;
let U;
let N;
func chosen_succ(w,v,U,N) -> strict LTLnode over v equals
:Def35:
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 Th59:
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 that
A1: w|=*N and
A2: N is non elementary;
set H = chosen_formula(U,N);
set SN = chosen_succ(w,v,U,N);
set H2 = the_right_argument_of H;
A3: H in the LTLnew of N by A2,Th58;
now
per cases;
suppose
A4: not H is Until & w |= *SuccNode1(H,N) or H is Until & w |/= H2;
then
A5: SN = SuccNode1(H,N) by Def35;
A6: w|=*SN
proof
now
per cases by A4;
suppose
not H is Until & w |= *SuccNode1(H,N);
hence thesis by Def35;
end;
suppose
A7: H is Until & w |/= H2;
set N2 = SuccNode2(H,N);
A8: w |= *SN or w |= *N2 by A1,A3,A5,A7,Lm19;
now
the LTLold of N2 =(the LTLold of N) \/ {H} by A3,Def5;
then
A9: H2
in the LTLold of N implies H2 in the LTLold of N2 by XBOOLE_0:def 3;
LTLNew2 H = {H2} by A7,Def2;
then H2 in LTLNew2 H by TARSKI:def 1;
then
A10: not H2 in the LTLold of N implies H2 in (LTLNew2 H \ the
LTLold of N) by XBOOLE_0:def 5;
assume
A11: not w |= *SN;
the LTLnew of N2 = ((the LTLnew of N) \ {H}) \/ (LTLNew2 H
\ the LTLold of N) by A3,Def5;
then not H2 in the LTLold of N implies H2 in the LTLnew of N2 by
A10,XBOOLE_0:def 3;
then H2 in *N2 by A9,Lm1;
hence contradiction by A7,A8,A11;
end;
hence thesis;
end;
end;
hence thesis;
end;
SN is_succ1_of N by A3,A5;
hence thesis by A6;
end;
suppose
A12: not ( not H is Until & w |= *SuccNode1(H,N) or H is Until & w |/= H2 );
set N1 = SuccNode1(H,N);
A13: SN = SuccNode2(H,N) by A12,Def35;
w|=*SN & SN is_succ_of N
proof
now
per cases by A12;
suppose
A14: H is Until & w |= H2;
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SNN = the LTLnew of SN;
LTLNew2 H = {H2} by A14,Def2;
then
A15: SNN = (NN \ {H}) \/ ({H2} \ NO) by A3,A13,Def5;
NN \ {H} c= NN by XBOOLE_1:36;
then
A16: SNN c= NN \/ {H2} by A15,XBOOLE_1:13;
set NX = the LTLnext of N;
set SNX = the LTLnext of SN;
set SNO = the LTLold of SN;
SNO =NO \/ {H} & {H} c= NN by A3,A13,Def5,ZFMISC_1:31;
then
A17: SNO c= NO \/ NN by XBOOLE_1:9;
A18: SNX = NX by A3,A13,Def5;
A19: G in *SN implies w|=G
proof
assume
A20: G in *SN;
now
per cases by A20,Lm1;
suppose
G in SNO;
then G in *N by A17,XBOOLE_0:def 3;
hence thesis by A1;
end;
suppose
G in SNN;
then G in NN or G in {H2} by A16,XBOOLE_0:def 3;
then G in *N or G = H2 by Lm1,TARSKI:def 1;
hence thesis by A1,A14;
end;
suppose
G in 'X' CastLTL(SNX);
then G in *N by A18,Lm1;
hence thesis by A1;
end;
end;
hence thesis;
end;
SN is_succ2_of N by A3,A13,A14;
hence thesis by A19;
end;
suppose
A21: 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,A3,A21,Lm16,Lm17;
end;
suppose
A22: H is disjunctive or H is Until or H is Release;
then SN is_succ2_of N by A3,A13;
hence thesis by A1,A3,A13,A21,A22,Lm18,Lm19,Lm20;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
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
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 NO = the LTLold of N;
set NN = the LTLnew of N;
assume N is non elementary;
then
A1: H in the LTLnew of N by Th58;
H is Until & w |= H2 implies (H2 in SNN or H2 in NO) & H in SNO
proof
assume that
A2: H is Until and
A3: w |= H2;
A4: SN = SuccNode2(H,N) by A2,A3,Def35;
LTLNew2 H = {H2} by A2,Def2;
then
A5: SNN = (NN \ {H}) \/ ({H2} \ NO) by A1,A4,Def5;
A6: now
per cases;
suppose
H2 in NO;
hence H2 in SNN or H2 in NO;
end;
suppose
A7: not H2 in NO;
H2 in {H2} by TARSKI:def 1;
then H2 in {H2} \ NO by A7,XBOOLE_0:def 5;
hence H2 in SNN or H2 in NO by A5,XBOOLE_0:def 3;
end;
end;
A8: H in {H} by TARSKI:def 1;
SNO =NO \/ {H} by A1,A4,Def5;
hence thesis by A8,A6,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 Th59;
hence thesis by Th25;
end;
definition
let w;
let v;
let U;
func choice_succ_func(w,v,U) -> Function of LTLNodes(v),LTLNodes(v) means
:
Def36: 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 Def30;
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 11(A1
);
take IT;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 being Function of LTLNodes(v),LTLNodes(v) such that
A3: for x st x in LTLNodes(v) holds f1.x = chosen_succ(w,v,U,CastNode(
x,v)) and
A4: for x st x in LTLNodes(v) holds f2.x = chosen_succ(w,v,U,CastNode( x,v));
for x being object st x in LTLNodes(v) holds f1.x = f2.x
proof
let x be object;
assume
A5: x in LTLNodes(v);
then f1.x = chosen_succ(w,v,U,CastNode(x,v)) by A3
.= f2.x by A4,A5;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th62:
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) and
A2: 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,Def36
.= SN by Def16;
hence thesis by A2,Th59;
end;
hence thesis;
end;
begin :: Definition of Negation inner most LTL.
definition
let H;
attr H is neg-inner-most means
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 for LTL-formula;
existence
proof
set a=atom.0;
take a;
A1: a is atomic;
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;
assume G is_subformula_of a;
then consider n,L such that
A2: 1 <= n and
len L = n and
A3: L.1 = G and
A4: L.n = a and
A5: 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;
n=1
proof
set k = n-1;
reconsider k as Nat by A2,NAT_1:21;
now
assume not n=1;
then 1<1+k by A2,XXREAL_0:1;
then
A6: 1<=k by NAT_1:19;
k<k+1 by XREAL_1:29;
then ex H1,G1 being LTL-formula st L.k = H1 & L.(k + 1) = G1 & H1
is_immediate_constituent_of G1 by A5,A6;
hence contradiction by A1,A4,MODELC_2:19;
end;
hence thesis;
end;
hence thesis by A1,A3,A4,MODELC_2:78;
end;
hence thesis;
end;
end;
definition
let H;
attr H is Sub_atomic means
H is atomic or ex G being LTL-formula st G is atomic & H = 'not' G;
end;
theorem Th63:
H is neg-inner-most & F is_subformula_of H implies F is neg-inner-most
by MODELC_2:35;
theorem Th64:
H is Sub_atomic iff H is atomic or H is negative &
the_argument_of H is atomic
proof
thus H is Sub_atomic implies H is atomic or H is negative & the_argument_of
H is atomic
proof
assume
A1: H is Sub_atomic;
per cases by A1;
suppose
H is atomic;
hence thesis;
end;
suppose
A2: ex G being LTL-formula st G is atomic & H = 'not' G;
then H is negative;
hence thesis by A2,MODELC_2:def 18;
end;
end;
thus H is atomic or H is negative & the_argument_of H is atomic implies H is
Sub_atomic
proof
assume
A3: H is atomic or H is negative & the_argument_of H is atomic;
per cases by A3;
suppose
H is atomic;
hence thesis;
end;
suppose
A4: H is negative & the_argument_of H is atomic;
then H = 'not' the_argument_of H by MODELC_2:def 18;
hence thesis by A4;
end;
end;
end;
theorem Th65:
H is neg-inner-most implies (H is Sub_atomic or H is conjunctive
or H is disjunctive or H is next or H is Until or H is Release)
proof
assume
A1: H is neg-inner-most;
per cases by MODELC_2:2;
suppose
H is atomic;
hence thesis;
end;
suppose
A2: H is negative;
set G = the_argument_of H;
A3: G is atomic by A1,A2;
H = 'not' G by A2,MODELC_2:def 18;
hence thesis by A3;
end;
suppose
H is conjunctive or H is disjunctive or H is next or H is Until or
H is Release;
hence thesis;
end;
end;
theorem
H is next & H is neg-inner-most implies the_argument_of H is neg-inner-most
proof
assume that
A1: H is next and
A2: H is neg-inner-most;
set F = the_argument_of H;
A3: F is_subformula_of H by A1,MODELC_2:30;
for G being LTL-formula st G is_subformula_of F holds G is negative
implies the_argument_of G is atomic
by A3,A2,MODELC_2:35;
hence thesis;
end;
theorem
(H is conjunctive or H is disjunctive or H is Until or H is Release) &
H is neg-inner-most implies the_left_argument_of H is neg-inner-most &
the_right_argument_of H is neg-inner-most
proof
assume that
A1: H is conjunctive or H is disjunctive or H is Until or H is Release and
A2: H is neg-inner-most;
set F2 = the_right_argument_of H;
A3: F2 is_subformula_of H by A1,MODELC_2:31;
A4: for G being LTL-formula st G is_subformula_of F2 holds G is negative
implies the_argument_of G is atomic
by A3,A2,MODELC_2:35;
set F1 = the_left_argument_of H;
A5: F1 is_subformula_of H by A1,MODELC_2:31;
for G being LTL-formula st G is_subformula_of F1 holds G is negative
implies the_argument_of G is atomic
by A5,A2,MODELC_2:35;
hence thesis by A4;
end;
begin :: Definition of Buchi Automaton (finite state & infinite word ) .
definition
let W be non empty set;
struct(1-sorted) BuchiAutomaton over W (# carrier -> 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
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,M1 for strict LTLnode over v;
reserve s,s1 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 be object;
assume y in X;
then ex x being LTL-formula st y=x & x is atomic & x in the LTLold of N;
hence thesis 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 be object;
assume y in X;
then ex x being LTL-formula st y=x & x is atomic & ('not' x) in the
LTLold of N;
hence thesis 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 be object;
assume a in X;
then ex y being Element of [: LTLStates(v),AtomicFamily, LTLStates(v) :]
st a=y & ex s,s1,x st y=[[s,x],s1] & s1 is_next_of s & x in Label_(s1);
hence thesis;
end;
then reconsider
X as Relation of [:LTLStates(v),AtomicFamily:], LTLStates(v) by
ZFMISC_1:def 3;
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) by Def30;
{y} c= LTLStates(v)
proof
let x be object;
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 object;
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 be object;
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 Th68:
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;
deffunc Run(Nat) = CastNode(run.$1,v);
set Run01=Run(0+1);
set Run00=Run(0);
A4: 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
A5: z = y and
A6: ex s,s1,x st y=[[s,x],s1] & s1 is_next_of s & x in Label_(s1);
consider s,s1,x such that
A7: y=[[s,x],s1] and
A8: s1 is_next_of s & x in Label_(s1) by A6;
A9: Run(i+1) = CastNode(s1,v) by A5,A7,XTUPLE_0:1
.= s1 by Def16;
A10: [s,x] = [run.i,Gzai(i)] by A5,A7,XTUPLE_0:1;
then Run(i) = CastNode(s,v) by XTUPLE_0:1
.= s by Def16;
hence thesis by A8,A10,A9,XTUPLE_0:1;
end;
then
A11: Run01 is_next_of Run00;
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;
A12: for i holds Run(i) = run.i
proof
let i;
reconsider i as Element of NAT by ORDINAL1:def 12;
run.i in LTLStates(v);
then
ex x being Element of LTLNodes(v) st run.i =x & x is elementary strict
LTLnode over v;
hence thesis by Def16;
end;
A13: 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;
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};
A14: X c= Y
proof
let x be object;
assume x in X;
then consider k being Element of NAT such that
A15: x=k and
A16: run.k in FSet;
Run(k) in FSet by A12,A16;
hence thesis by A15;
end;
assume FSet in FinalS_LTL(v);
hence thesis by A3,A14;
end;
A17: for n st P[n] holds P[n + 1]
proof
let n;
assume
A18: P[n];
A19: 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 that
A20: F is_subformula_of v and
A21: len(F)= n+1 and
A22: F in the LTLold of Run(i+1);
set zeta = Shift(w,i);
now
per cases by A20,Th63,Th65;
suppose
A23: F is Sub_atomic;
set Gi9=CastSeq(w,AtomicFamily)^\i;
set Gi=Gzai(i);
CastSeq(zeta,AtomicFamily) = Gi9 by MODELC_2:81;
then
A24: CastSeq(zeta,AtomicFamily).0 = CastSeq(w,AtomicFamily).(0+i) by
NAT_1:def 3
.= Gi;
Gi in Label_(Run(i+1)) by A4;
then consider X being Subset of atomic_LTL such that
A25: Gi = X and
A26: atomic_LTL(Run(i+1)) c= X and
A27: Neg_atomic_LTL(Run(i+1)) misses X;
A28: Neg_atomic_LTL(Run(i+1)) /\ X ={} by A27,XBOOLE_0:def 7;
now
per cases by A23,Th64;
suppose
A29: F is atomic;
then F in atomic_LTL(Run(i+1)) by A22;
hence thesis by A25,A26,A24,A29,MODELC_2:63;
end;
suppose
A30: F is negative & the_argument_of F is atomic;
set Fa= the_argument_of F;
A31: F = 'not' Fa by A30,MODELC_2:4;
then zeta |= F iff zeta |/= Fa by MODELC_2:64;
then
A32: zeta |= F iff not Fa in Gi by A24,A30,MODELC_2:63;
Fa in Neg_atomic_LTL(Run(i+1)) by A22,A30,A31;
hence thesis by A25,A28,A32,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
suppose
A33: F is conjunctive or F is disjunctive;
set h1 = the_left_argument_of F;
len(h1) < n+1 by A21,A33,MODELC_2:11;
then
A34: len(h1) <= n by NAT_1:13;
set Runi1 = Run(i+1);
set Runi = Run(i);
A35: Runi1 is_next_of Runi by A4;
set h2 = the_right_argument_of F;
len(h2) < n+1 by A21,A33,MODELC_2:11;
then
A36: len(h2) <= n by NAT_1:13;
reconsider Runi1 as elementary strict LTLnode over v by A35;
reconsider Runi as elementary strict LTLnode over v by A35;
A37: 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 Th41;
A38: h1 is_subformula_of F & h2 is_subformula_of F by A33,MODELC_2:31;
zeta |= F
proof
now
per cases by A33;
suppose
A39: F is conjunctive;
then
zeta |= h1 & zeta |= h2 by A4,A18,A20,A22,A38,A34,A36,A37,
MODELC_2:35;
then zeta |= h1 '&' h2 by MODELC_2:65;
hence thesis by A39,MODELC_2:6;
end;
suppose
A40: F is disjunctive;
then zeta |= h1 or zeta |= h2 by A4,A18,A20,A22,A38,A34,A36,A37
,MODELC_2:35;
then zeta |= h1 'or' h2 by MODELC_2:66;
hence thesis by A40,MODELC_2:7;
end;
end;
hence thesis;
end;
hence thesis;
end;
suppose
A41: F is next;
set i1=i+1;
set Runi1 = Run(i1);
set Runi2 = Run(i1+1);
Runi2 is_next_of Runi1 by A4;
then reconsider Runi2 as elementary strict LTLnode over v;
set Runi =Run(i);
A42: Runi1 is_next_of Runi by A4;
set h = the_argument_of F;
A43: h is_subformula_of F by A41,MODELC_2:30;
len(h) < n+1 by A21,A41,MODELC_2:10;
then
A44: len(h) <= n by NAT_1:13;
reconsider Runi1 as elementary strict LTLnode over v by A42;
reconsider Runi as elementary strict LTLnode over v by A42;
A45: Runi1 is_next_of Runi & F in the LTLold of Runi1 implies (F is
next implies h in the LTLnext of Runi1) by Th41;
the LTLnext of Runi1 c= the LTLold of Runi2 by A4,Th37;
then Shift(w,i1) |= h by A4,A18,A20,A22,A41,A43,A44,A45,MODELC_2:35;
then Shift(zeta,1) |= h by MODELC_2:80;
then zeta |= 'X' h by MODELC_2:67;
hence thesis by A41,MODELC_2:5;
end;
suppose
A46: F is Until;
set Fin = FinalS_LTL(F,v);
deffunc Fun(set) = run.(CastNat($1)+i);
set FRun = {k where k is Element of NAT:Run(k) in Fin};
A47: for x st x in NAT holds Fun(x) in LTLStates(v);
consider runQ being sequence of LTLStates(v) such that
A48: for x st x in NAT holds runQ.x = Fun(x) from FUNCT_2:sch 11(
A47);
reconsider runQ as sequence of LTLStates(v);
deffunc RunQ(Nat) = CastNode(runQ.$1,v);
A49: for m holds RunQ(m) = Run(m+i)
proof
let m;
reconsider m as Element of NAT by ORDINAL1:def 12;
RunQ(m) = CastNode(Fun(m),v) by A48
.= Run(m+i) by MODELC_2:def 1;
hence thesis;
end;
A50: for m holds RunQ(m+1) is_next_of RunQ(m)
proof
let m;
set m1 = m+i;
A51: RunQ(m+1) = Run((m+1)+i) by A49
.= Run(m1+1);
RunQ(m) = Run(m1) by A49;
hence thesis by A4,A51;
end;
set FRunQ = {k where k is Element of NAT:RunQ(k) in Fin};
A52: Fin in FinalS_LTL(v) by A20,A46;
A53: FRunQ is infinite
proof
set FRun2 = {k where k is Element of NAT:i<k & k in FRun};
set FRun1 = {k where k is Element of NAT:k<=i & k in FRun};
A54: FRun1 c= Seg i \/ {0}
proof
let x be object;
assume x in FRun1;
then consider k being Element of NAT such that
A55: x = k and
A56: k<=i and
k in FRun;
now
per cases;
suppose
k = 0;
then k in {0} by TARSKI:def 1;
hence thesis by A55,XBOOLE_0:def 3;
end;
suppose
k <> 0;
then 0<0+k;
then 1<= k by NAT_1:19;
then k in Seg i by A56,FINSEQ_1:1;
hence thesis by A55,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
A57: FRunQ is finite implies FRun2 is finite
proof
deffunc Fun(object) = CastNat($1)+i;
consider fun being Function such that
A58: dom fun = FRunQ &
for x being object st x in FRunQ holds fun.x =
Fun(x) from FUNCT_1:sch 3;
A59: x in FRun2 implies CastNat(x)-i in FRunQ
proof
assume x in FRun2;
then consider k being Element of NAT such that
A60: x = k and
A61: i< k and
A62: k in FRun;
set k2=k-i;
reconsider k2 as Element of NAT by A61,NAT_1:21;
A63: RunQ(k2) = Run(k2+i) by A49
.= Run(k);
(ex k1 being Element of NAT st k = k1 & Run(k1) in Fin )
& CastNat(x)-i = k2 by A60,A62,MODELC_2:def 1;
hence thesis by A63;
end;
A64: for y being object st y in FRun2
ex x being object st x in dom fun & y = fun.x
proof
let y be object such that
A65: y in FRun2;
consider k being Element of NAT such that
A66: y = k and
A67: i< k and
k in FRun by A65;
set x = CastNat(y)-i;
A68: x in dom fun by A59,A58,A65;
set k1 = k-i;
reconsider k1 as Nat by A67,NAT_1:21;
A69: x = k1 by A66,MODELC_2:def 1;
fun.x = Fun(x) by A59,A58,A65
.= k1 + i by A69,MODELC_2:def 1
.= y by A66;
hence thesis by A68;
end;
assume FRunQ is finite;
then rng fun is finite by A58,FINSET_1:8;
hence thesis by A64,FINSET_1:1,FUNCT_1:9;
end;
FRun c= FRun1 \/ FRun2
proof
let x be object;
assume
A70: x in FRun;
then ex k being Element of NAT st x = k & Run(k) in Fin;
then reconsider x as Element of NAT;
now
per cases;
suppose
x<=i;
then x in FRun1 by A70;
hence x in FRun1 \/ FRun2 by XBOOLE_0:def 3;
end;
suppose
i < x;
then x in FRun2 by A70;
hence x in FRun1 \/ FRun2 by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence thesis by A13,A52,A57,A54;
end;
set h2 = the_right_argument_of F;
set h1 = the_left_argument_of F;
len(h1) < n+1 by A21,A46,MODELC_2:11;
then
A71: len(h1) <= n by NAT_1:13;
A72: (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
A73: 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 not FRunQ c= {0};
then consider x being object such that
A74: x in FRunQ and
A75: not x in {0};
consider k being Element of NAT such that
A76: x = k and
A77: RunQ(k) in Fin by A74;
k <> 0 by A75,A76,TARSKI:def 1;
then 0<0+k;
then
A78: 1 <= k by NAT_1:19;
set RQk = RunQ(k);
consider y being Element of LTLStates(v) such that
A79: RQk = y and
A80: not F in the LTLold of CastNode(y,v) or h2 in the
LTLold of CastNode(y,v) by A77;
reconsider y as strict LTLnode over v by A79;
CastNode(y,v) = RunQ(k) by A79,Def16;
hence contradiction by A73,A78,A80;
end;
hence thesis;
end;
F in the LTLold of RunQ(1) by A22,A49;
then consider j such that
A81: j>=1 and
A82: h2 in the LTLold of RunQ(j) and
A83: for m st 1<=m & m<j holds F in the LTLold of RunQ(m) & h1
in the LTLold of RunQ(m) by A46,A50,A53,A72,Th54;
set j0 = j-1;
reconsider j0 as Nat by A81,NAT_1:21;
set j1=j0+i;
j1+1 = j+i;
then
A84: h2 in the LTLold of Run(j1+1) by A49,A82;
A85: h1 is_subformula_of F by A46,MODELC_2:31;
A86: for k st k<j0 holds Shift(zeta,k) |= h1
proof
let k such that
A87: k<j0;
set k1 = k+1;
set ki=k+i;
1<=k1 & k+1 < j0+1 by A87,NAT_1:11,XREAL_1:8;
then h1 in the LTLold of RunQ(k1) by A83;
then h1 in the LTLold of Run(k1+i) by A49;
then h1 in the LTLold of Run(ki+1);
then Shift(w,ki) |= h1 by A18,A20,A85,A71,MODELC_2:35;
hence thesis by MODELC_2:80;
end;
len(h2) < n+1 by A21,A46,MODELC_2:11;
then
A88: len(h2) <= n by NAT_1:13;
h2 is_subformula_of F by A46,MODELC_2:31;
then Shift(w,j1) |= h2 by A18,A20,A88,A84,MODELC_2:35;
then
A89: Shift(zeta,j0) |= h2 by MODELC_2:80;
F = h1 'U' h2 by A46,MODELC_2:8;
hence thesis by A89,A86,MODELC_2:68;
end;
suppose
A90: F is Release;
set h2 = the_right_argument_of F;
A91: h2 is_subformula_of F by A90,MODELC_2:31;
set h1 = the_left_argument_of F;
defpred M[Nat] means (for k st k < $1 holds Shift(zeta,k) |= 'not'
h1) implies Shift(zeta,$1) |= h2 & F in the LTLold of Run(i+1+$1);
len(h1) < n+1 by A21,A90,MODELC_2:11;
then
A92: len(h1) <= n by NAT_1:13;
len(h2) < n+1 by A21,A90,MODELC_2:11;
then
A93: len(h2) <= n by NAT_1:13;
A94: h1 is_subformula_of F by A90,MODELC_2:31;
A95: for j st M[j] holds M[j + 1]
proof
let j such that
A96: M[j];
M[j+1]
proof
set i1= i+j;
set Run1=Run(i1+1);
set Run0=Run(i1);
assume
A97: for k st k<j+1 holds Shift(zeta,k) |= 'not' h1;
A98: for k st k<j holds Shift(zeta,k) |= 'not' h1
proof
A99: j <= j+1 by NAT_1:11;
let k;
assume k<j;
then k<j+1 by A99,XXREAL_0:2;
hence thesis by A97;
end;
A100: Run1 is_next_of Run0 by A4;
then reconsider Run0 as elementary strict LTLnode over v;
set i2=i1+1;
set Run2=Run(i2+1);
A101: Run2 is_next_of Run1 by A4;
then reconsider Run2 as elementary strict LTLnode over v;
reconsider Run1 as elementary strict LTLnode over v by A100;
j<j+1 by NAT_1:13;
then
A102: Shift(zeta,j) |= 'not' h1 by A97;
A103: now
assume h1 in the LTLold of Run1;
then Shift(w,i1) |= h1 by A18,A20,A94,A92,MODELC_2:35;
then Shift(Shift(w,i),j) |= h1 by MODELC_2:80;
hence contradiction by A102,MODELC_2:64;
end;
A104: Run1 is_next_of Run0 & F is Release & F in the LTLold of
Run1 & not h1 in the LTLold of Run1 implies h2 in the LTLold of Run1 & F in the
LTLnext of Run1 by Th39;
then h2 in the LTLold of Run2 by A4,A90,A96,A101,A98,A103,Th40;
then
A105: Shift(w,i+(j+1)) |= h2 by A18,A20,A91,A93,MODELC_2:35;
F in the LTLold of Run2 by A4,A90,A96,A101,A98,A103,A104,Th40;
hence thesis by A105,MODELC_2:80;
end;
hence thesis;
end;
A106: F = h1 'R' h2 by A90,MODELC_2:9;
A107: (for j holds M[j]) implies zeta |= F
proof
assume for j holds M[j];
then for j holds ((for k st k<j holds Shift(zeta,k) |= 'not' h1)
implies Shift(zeta,j) |= h2);
hence thesis by A106,MODELC_2:69;
end;
A108: M[0]
proof
set Run0=Run(i);
set Run1=Run(i+1);
A109: Run1 is_next_of Run0 by A4;
then reconsider Run1 as elementary strict LTLnode over v;
reconsider Run0 as elementary strict LTLnode over v by A109;
assume for k st k < 0 holds Shift(zeta,k) |= 'not' h1;
A110: Shift(zeta,0) = Shift(w,i) by MODELC_2:79;
Run1 is_next_of Run0 & F in the LTLold of Run1 implies (F is
Release implies h2 in the LTLold of Run1) by Th41;
hence thesis by A4,A18,A20,A22,A90,A91,A93,A110,MODELC_2:35;
end;
for j holds M[j] from NAT_1:sch 2(A108,A95);
hence thesis by A107;
end;
end;
hence thesis;
end;
P[n+1]
proof
let i,F;
assume that
A111: F is_subformula_of v and
A112: len(F)<=n+1 and
A113: F in the LTLold of Run(i+1);
set L=len(F);
reconsider L as Nat;
now
per cases by A112,NAT_1:8;
suppose
L<=n;
hence thesis by A18,A111,A113;
end;
suppose
L = n+1;
hence thesis by A19,A111,A113;
end;
end;
hence thesis;
end;
hence thesis;
end;
A114: P[0] by MODELC_2:3;
A115: for n holds P[n] from NAT_1:sch 2(A114,A17);
set n = len v;
A116: v in {v} & len(v)<=n by TARSKI:def 1;
reconsider Run01 as elementary strict LTLnode over v by A11;
reconsider Run00 as elementary strict LTLnode over v by A11;
A117: the LTLnext of Run00 c= the LTLold of Run01 by A4,Th37;
Run(0) = CastNode(init v,v) by A1,TARSKI:def 1
.= init v by Def16;
then Shift(w,0) |= v by A117,A115,A116;
hence thesis by MODELC_2:79;
end;
definition
let w,v,U,N;
assume that
A1: N is non elementary and
A2: w |= *N;
func chosen_succ_end_num(w,v,U,N) -> Nat means
:Def48:
(for i st i<it holds
CastNode((choice_succ_func(w,v,U)|**i).N,v) is non elementary & CastNode((
choice_succ_func(w,v,U)|**(i+1)).N,v) is_succ_of CastNode((choice_succ_func(w,v
,U)|**i).N,v)) & CastNode((choice_succ_func(w,v,U)|**it).N,v) is elementary &
for i st i<=it holds w |= *CastNode((choice_succ_func(w,v,U)|**i).N,v);
existence
proof
A3: w |= *CastNode(N,v) by A2,Def16;
N in LTLNodes(v) & CastNode(N,v) is non elementary by A1,Def16,Def30;
hence thesis by A3,Th51,Th62;
end;
uniqueness
proof
set f = choice_succ_func(w,v,U);
let n1,n2 being Nat such that
A4: for i st i<n1 holds CastNode((f|**i).N,v) is non elementary &
CastNode(( f|**(i+1)).N,v) is_succ_of CastNode((f|**i).N,v) and
A5: CastNode((f|**n1).N,v) is elementary and
for i st i<=n1 holds w |= *CastNode((f|**i).N,v) and
A6: for i st i<n2 holds CastNode((f|**i).N,v) is non elementary &
CastNode((f|**(i+1)).N,v) is_succ_of CastNode((f|**i).N,v) and
A7: CastNode((f|**n2).N,v) is elementary and
for i st i<=n2 holds w |= *CastNode((f|**i).N,v);
now
assume
A8: n1<>n2;
now
per cases by A8,XXREAL_0:1;
suppose
n1<n2;
hence contradiction by A5,A6;
end;
suppose
n2<n1;
hence contradiction by A4,A7;
end;
end;
hence contradiction;
end;
hence thesis;
end;
end;
definition
let w;
let v;
let U;
let N;
assume
A1: w |= * ('X' N);
func chosen_next(w,v,U,N) -> elementary strict LTLnode over v equals
:Def49:
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 by A1,Def48;
end;
theorem Th69:
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;
assume
A1: w |= *N;
set n = chosen_succ_end_num(w,v,U,N);
set f = choice_succ_func(w,v,U);
set nextnode =CastNode((f|**n).N,v);
A2: N in LN by Def30;
now
per cases;
suppose
A3: N is non elementary;
deffunc F(set) = CastNode((f|**CastNat(CastNat($1)-1)).N,v);
set n1=n+1;
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
A4: len L = n1 and
A5: for k being Nat st k in dom L holds L.k=F(k);
A6: Seg n1 = dom L by A4,FINSEQ_1:def 3;
A7: 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:1;
then L.k=CastNode((f|**CastNat(CastNat(k)-1)).N,v) by A5,A6;
hence thesis by MODELC_2:def 1;
end;
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 that
A8: 1<=k and
A9: k<len(L);
set k1 = k-1;
reconsider k1 as Nat by A8,NAT_1:21;
set M1 = CastNode((f|**(k1+1)).N,v);
set kp=k+1;
1<=kp & kp<=n1 by A4,A8,A9,NAT_1:13;
then
A10: L.(k+1) = CastNode((f|**CastNat(kp-1)).N,v) by A7
.= M1 by MODELC_2:def 1;
set N1 = CastNode((f|**k1).N,v);
k-1<n1-1 by A4,A9,XREAL_1:14;
then
A11: M1 is_succ_of N1 by A1,A3,Def48;
L.k = CastNode((f|**CastNat(k1)).N,v) by A4,A7,A8,A9
.= N1 by MODELC_2:def 1;
hence thesis by A11,A10;
end;
then
A12: L is_Finseq_for v;
A13: 1<=n1 by NAT_1:11;
then
A14: L.(len L) = CastNode((f|**CastNat(n1-1)).N,v) by A4,A7
.= nextnode by MODELC_2:def 1;
A15: nextnode = chosen_next(w,v,U,s) by A1,A3,Def49;
L.1 = CastNode((f|**CastNat(1-1)).N,v) by A13,A7
.= CastNode((f|**0).N,v) by MODELC_2:def 1
.= CastNode((id LN).N,v) by FUNCT_7:84
.= CastNode(N,v) by A2,FUNCT_1:18
.='X' s by Def16;
hence thesis by A1,A3,A15,A13,A4,A14,A12,Def48;
end;
suppose
N is elementary;
then the LTLnew of N = the LTLnew of FinalNode v;
then
A16: chosen_next(w,v,U,s)= N by A1,Def49;
set L =<*N*>;
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 by FINSEQ_1:39;
then
A19: L is_Finseq_for v;
len L = 1 & L.1='X' s by FINSEQ_1:39;
hence thesis by A1,A16,A19;
end;
end;
hence thesis;
end;
definition
let w;
let v;
let U;
func chosen_run(w,v,U) -> sequence of LTLStates(v) means
:Def50:
it.0 = init
v & for n holds it.(n+1) = chosen_next(Shift(w,n),v,U,CastNode(it.n,v));
existence
proof
deffunc G(set,set) = chosen_next(Shift(w,CastNat($1)),v,U,CastNode($2,v));
set LS = LTLStates(v);
(ex y being set st ex f being Function st y = f.0 & dom f = NAT & f.0
= init v & for n being 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 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 Nat holds f.(n+1
) = G(n,f.n)) holds y1 = y2 from RECDEF_1:sch 12;
then consider IT being Function such that
A1: dom IT = NAT and
A2: IT.0 =init v and
A3: for n being Nat holds IT.(n+1) = G(n,IT.n);
A4: for n being Nat holds IT.(n+1) = G(n,IT.n)
by A3;
A5: 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 A4;
hence thesis by MODELC_2:def 1;
end;
for x being object st x in NAT holds IT.x in LS
proof
let x be object;
assume x in NAT;
then reconsider x as Nat;
A6: x=0 or 0<0+x;
now
per cases by A6,NAT_1:19;
suppose
A7: x = 0;
set y = IT.x;
reconsider y as Element of LTLNodes(v) by A2,A7,Def30;
IT.x = y;
hence thesis by A2,A7;
end;
suppose
A8: 1<=x;
set x1 = x-1;
reconsider x1 as Nat by A8,NAT_1:21;
set y = IT.x;
A9: y = IT.(x1+1) .= G(x1,IT.x1) by A4;
then reconsider y as Element of LTLNodes(v) by Def30;
IT.x = y;
hence thesis by A9;
end;
end;
hence thesis;
end;
then reconsider IT as sequence of LS by A1,FUNCT_2:3;
take IT;
thus thesis by A2,A5;
end;
uniqueness
proof
deffunc G(set,set) = chosen_next(Shift(w,CastNat($1)),v,U,CastNode($2,v));
deffunc G1(Nat,set) = chosen_next(Shift(w,$1),v,U,CastNode($2,v));
set LS = LTLStates(v);
A10: for f,g being sequence of 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 sequence of LS such that
A11: f.0 =init v and
A12: for n being Nat holds f.(n+1) = G(n,f.n) and
A13: g.0 =init v and
A14: for n being Nat holds g.(n+1) = G(n,g.n);
defpred P[Nat] means f.$1= g.$1;
A15: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume P[k];
then f.(k+1) = G(k,g.k) by A12
.= g.(k+1) by A14;
hence thesis;
end;
A16: P[0] by A11,A13;
for k being Nat holds P[k] from NAT_1:sch 2(A16,A15 );
then
A17: for x being object st x in dom f holds f.x = g.x;
dom f = NAT & dom g = NAT by FUNCT_2:def 1;
hence thesis by A17,FUNCT_1:2;
end;
for f,g being sequence of 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 sequence of LS such that
A18: f.0 =init v and
A19: for n holds f.(n+1) = G1(n,f.n) and
A20: g.0 =init v and
A21: for n holds g.(n+1) = G1(n,g.n);
A22: 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 A21;
hence thesis by MODELC_2:def 1;
end;
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 A19;
hence thesis by MODELC_2:def 1;
end;
hence thesis by A10,A18,A20,A22;
end;
hence thesis;
end;
end;
Lm33: 'X' CastLTL({} v)= {}
proof
now
assume 'X' CastLTL({} v) <> {};
then consider y being object such that
A1: y in 'X' CastLTL({} v) by XBOOLE_0:def 1;
ex x being LTL-formula st y=x & ex u being LTL-formula st u in CastLTL(
{} v) & x='X' u by A1;
hence contradiction;
end;
hence thesis;
end;
theorem Th70:
w |= * N implies Shift(w,1) |= * ('X' N)
proof
set XN = 'X' N;
assume
A1: w |= *N;
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 Lm1;
hence thesis by A1;
end;
then
A2: w |='X' CastLTL(the LTLnext of N);
*XN = CastLTL(the LTLnext of N) by Lm33;
hence thesis by A2,MODELC_2:77;
end;
theorem
w |= 'X' v implies w |= * (init v)
proof
assume
A1: w |= 'X' v;
for H be LTL-formula st H in 'X' CastLTL(Seed v) holds w|= H
proof
let H being LTL-formula;
assume H in 'X' CastLTL(Seed v);
then
ex x being LTL-formula st H=x & ex u being LTL-formula st u in CastLTL(
Seed v) & x='X' u;
hence thesis by A1,TARSKI:def 1;
end;
hence thesis;
end;
theorem Th72:
w |= v iff w |= *('X' init v)
proof
set N = init v;
set M = 'X' N;
A1: *M = {v} by Lm33;
A2: w |= *M implies w |= v
proof
assume
A3: w |= *M;
v in *M by A1,TARSKI:def 1;
hence thesis by A3;
end;
w |= v implies w |= *M
by A1,TARSKI:def 1;
hence thesis by A2;
end;
theorem Th73:
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;
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));
assume w |= v;
then
A1: w |= *('X' s) by Th72;
A2: CastNode(chosen_run(w,v,U).0,v) = CastNode(s,v) by Def50
.= s by Def16;
A3: for n st P[n] holds P[n+1]
proof
let n;
set s1=R(n);
s1 is elementary strict LTLnode over v
proof
now
per cases;
suppose
n = 0;
then s1 = CastNode(s,v) by Def50
.= s by Def16;
hence thesis;
end;
suppose
A4: 0 <n;
set m = n-1;
reconsider m as Nat by A4,NAT_1:20;
n = m+1;
then
s1 = CastNode(chosen_next(Shift(w,m),v,U, CastNode(chosen_run(w
,v,U).m,v)),v) by Def50
.= chosen_next(Shift(w,m),v,U, CastNode(chosen_run(w,v,U).m,v))
by Def16;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider s1 as elementary strict LTLnode over v;
set n1 =n+1;
set w1 = Shift(w,n);
set w2 = Shift(w,n1);
set s2=R(n1);
set s3=R(n1+1);
A5: s2 = CastNode( chosen_next (w1,v,U, CastNode(chosen_run(w,v,U).n,v) ),
v) by Def50
.= chosen_next(w1,v,U,s1) by Def16;
then reconsider s2 as elementary strict LTLnode over v;
A6: s3 = CastNode( chosen_next (w2,v,U, CastNode(chosen_run(w,v,U).n1,v) )
,v) by Def50
.= chosen_next(w2,v,U,s2) by Def16;
assume P[n];
then w2 = Shift(w1,1) & w1 |= *chosen_next(w1,v,U,s1) by Th69,MODELC_2:80;
then w2 |= * ('X' s2) by A5,Th70;
hence thesis by A6,Th69;
end;
R(0+1) = CastNode( chosen_next (Shift(w,0),v,U, CastNode(chosen_run(w,v,
U).0,v) ),v) by Def50
.= CastNode(chosen_next(w,v,U,s),v) by A2,MODELC_2:79
.= chosen_next(w,v,U,s) by Def16;
then
A7: P[0] by A1,A2,Th69,MODELC_2:79;
for n holds P[n] from NAT_1:sch 2(A7,A3);
hence thesis;
end;
theorem Th74:
w |= v implies for i holds H in the LTLold of CastNode(
chosen_run(w,v,U).(i+1),v) & H is Until & Shift(w,i)|=the_right_argument_of H
implies the_right_argument_of H in the LTLold of CastNode(chosen_run(w,v,U).(i+
1),v)
proof
assume
A1: w |= v;
for j holds H in the LTLold of CastNode(chosen_run(w,v,U).(j+1),v) & H
is Until & Shift(w,j)|=the_right_argument_of H implies the_right_argument_of H
in the LTLold of CastNode(chosen_run(w,v,U).(j+1),v)
proof
set LN = LTLNodes(v);
let j;
set s = CastNode(chosen_run(w,v,U).j,v);
set s1 = CastNode(chosen_run(w,v,U).(j+1),v);
set w0 = Shift(w,j);
set N = 'X' s;
set f = choice_succ_func(w0,v,U);
set n = chosen_succ_end_num(w0,v,U,N);
set nextnode =CastNode((f|**n).N,v);
A2: w0 |= *N by A1,Th73;
A3: N in LN by Def30;
now
per cases;
suppose
A4: N is non elementary;
deffunc F(set) = CastNode((f|**CastNat(CastNat($1)-1)).N,v);
set n1=n+1;
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
A5: len L = n1 and
A6: for k being Nat st k in dom L holds L.k=F(k);
A7: Seg n1 = dom L by A5,FINSEQ_1:def 3;
A8: 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:1;
then L.k=CastNode((f|**CastNat(CastNat(k)-1)).N,v) by A6,A7;
hence thesis by MODELC_2:def 1;
end;
A9: 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 that
A10: 1<=k and
A11: k<len(L);
set k1 = k-1;
reconsider k1 as Nat by A10,NAT_1:21;
set M1 = CastNode((f|**(k1+1)).N,v);
set kp=k+1;
1<=kp & kp<=n1 by A5,A10,A11,NAT_1:13;
then
A12: L.(k+1) = CastNode((f|**CastNat(kp-1)).N,v) by A8
.= M1 by MODELC_2:def 1;
set N1 = CastNode((f|**k1).N,v);
k-1<n1-1 by A5,A11,XREAL_1:14;
then
A13: M1 is_succ_of N1 by A2,A4,Def48;
L.k = CastNode((f|**CastNat(k1)).N,v) by A5,A8,A10,A11
.= N1 by MODELC_2:def 1;
hence thesis by A13,A12;
end;
then
A14: L is_Finseq_for v;
1<=n1 by NAT_1:11;
then
A15: L.1 = CastNode((f|**CastNat(1-1)).N,v) by A8
.= CastNode((f|**0).N,v) by MODELC_2:def 1
.= CastNode((id LN).N,v) by FUNCT_7:84
.= CastNode(N,v) by A3,FUNCT_1:18
.= N by Def16;
1<=n1 by NAT_1:11;
then
A16: L.(len L) = CastNode((f|**CastNat(n1-1)).N,v) by A5,A8
.= nextnode by MODELC_2:def 1;
A17: nextnode is elementary by A2,A4,Def48;
1<=len(L) by A5,NAT_1:11;
then
A18: len(L) >1 by A4,A15,A16,A17,XXREAL_0:1;
A19: 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 that
A20: H in the LTLold of nextnode and
A21: H is Until and
A22: w0|=H2;
the LTLold of CastNode(L.1,v) = {} v & the LTLold of CastNode(L
.len(L),v) = the LTLold of nextnode by A15,A16,Def16;
then consider m such that
A23: 1<= m and
A24: m<n1 and
A25: ( not H in the LTLold of CastNode(L.m,v))& H in the LTLold
of CastNode(L.(m+1) ,v) by A5,A14,A18,A20,Th27;
set mm1=m-1;
reconsider mm1 as Nat by A23,NAT_1:21;
set Nm1= (f|**mm1).N;
set m1 = m+1;
A26: Nm1 in LN by A3,FUNCT_2:5;
consider N1,N2 such that
A27: N1 = L.m and
A28: N2 = L.(m+1) and
A29: N2 is_succ_of N1 by A5,A9,A23,A24;
A30: N1 = CastNode((f|**CastNat(mm1)).N,v) by A8,A23,A24,A27
.= CastNode(Nm1,v) by MODELC_2:def 1;
A31: 1<=m1 & m1<=n1 by A23,A24,NAT_1:13;
then
A32: N2 = CastNode((f|**CastNat(m1-1)).N,v) by A8,A28
.= CastNode((f|**(mm1+1)).N,v) by MODELC_2:def 1
.= CastNode((f*(f|**mm1)).N,v) by FUNCT_7:71
.= CastNode(f.((f|**mm1).N),v) by A3,FUNCT_2:15
.= CastNode(chosen_succ(w0,v,U,CastNode(Nm1,v)),v) by A26,Def36
.= chosen_succ(w0,v,U,N1) by A30,Def16;
m-1<n1-1 by A24,XREAL_1:14;
then
A33: N1 is non elementary by A2,A4,A30,Def48;
chosen_formula(U,N1) = H
proof
set G = chosen_formula(U,N1);
set M2 = the LTLold of N2;
set M1 = the LTLold of N1;
set M0 = the LTLnew of N1;
A34: G in M0 by A33,Th58;
A35: M2 = M1 \/ {G}
proof
now
per cases;
suppose
not G is Until & w0 |= *SuccNode1(G,N1) or G is
Until & w0 |/= the_right_argument_of G;
then chosen_succ(w0,v,U,N1) = SuccNode1(G,N1) by Def35;
hence thesis by A32,A34,Def4;
end;
suppose
A36: not ( not G is Until & w0 |= *SuccNode1(G,N1) or G
is Until & w0 |/= the_right_argument_of G );
N2 = SuccNode2(G,N1) by A32,A36,Def35;
hence thesis by A34,Def5;
end;
end;
hence thesis;
end;
A37: ( not H in M1)& H in M2 by A25,A27,A28,Def16;
now
assume H <> G;
then not H in {G} by TARSKI:def 1;
hence contradiction by A37,A35,XBOOLE_0:def 3;
end;
hence thesis;
end;
then
A38: N2 = SuccNode2(H,N1) by A21,A22,A32,Def35;
A39: CastNode(L.(len(L)),v) = nextnode by A16,Def16;
N1 = CastNode(L.m,v) & N2 = CastNode(L.(m+1),v) by A27,A28,Def16;
then N2 is_succ_of N1,H by A25,A29,Th28;
then
A40: H in the LTLnew of N1;
the LTLnew of nextnode = {} by A17;
then
the LTLnew of CastNode(L.m1,v) c= the LTLold of CastNode(L.(len
(L)),v) by A5,A14,A31,A39,Th34;
then
A41: the LTLnew of N2 c= the LTLold of nextnode by A28,A39,Def16;
the LTLold of CastNode(L.m,v) c= the LTLold of CastNode(L.len(L
),v) by A5,A14,A23,A24,Th31;
then
A42: the LTLold of N1 c= the LTLold of nextnode by A27,A39,Def16;
LTLNew2 H = {H2} by A21,Def2;
then
A43: the LTLnew of N2 = ((the LTLnew of N1) \ {H}) \/ ({H2} \ the
LTLold of N1) by A38,A40,Def5;
now
per cases;
suppose
H2 in the LTLold of N1;
hence thesis by A42;
end;
suppose
A44: not H2 in the LTLold of N1;
H2 in {H2} by TARSKI:def 1;
then H2 in {H2} \ the LTLold of N1 by A44,XBOOLE_0:def 5;
then H2 in the LTLnew of N2 by A43,XBOOLE_0:def 3;
hence thesis by A41;
end;
end;
hence thesis;
end;
chosen_run(w,v,U).(j+1) = chosen_next(w0,v,U,s) by Def50
.=nextnode by A2,A4,Def49;
hence thesis by A19,Def16;
end;
suppose
N is elementary;
then the LTLnew of N = the LTLnew of FinalNode v;
then chosen_next(w0,v,U,s)= N by A2,Def49;
then s1 = CastNode(N,v) by Def50
.= N by Def16;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th75:
w |= v implies w is-accepted-by BAutomaton(v)
proof
set LS = LTLStates(v);
set LT = Tran_LTL(v);
set IS = InitS_LTL(v);
set FS = FinalS_LTL(v);
assume
A1: w |= 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
set chf = the 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 sequence of LS st for x st x in NAT holds run.x = R(x
) from FUNCT_2:sch 11(A2);
then consider run being sequence of LS such that
A3: for x st x in NAT holds run.x = R(x);
deffunc Run(Nat) = CastNode(run.$1,v);
A4: 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 12;
set Rn = Run(n);
run.n in LS;
then consider N being Element of LTLNodes(v) such that
A5: N = run.n and
A6: N is elementary strict LTLnode over v;
reconsider N as elementary strict LTLnode over v by A6;
the LTLnew of Rn = the LTLnew of N by A5,Def16
.= {} by Def11;
hence thesis by A5,A6,Def11;
end;
A7: for n holds run.n = chosen_run(w,v,chf).n
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
run.n = R(n) by A3;
hence thesis by MODELC_1:def 2;
end;
A8: for n holds Run(n+1) is_next_of Run(n) & Shift(w,n) |= * Run(n+1)
proof
let n;
set Rn = Run(n);
reconsider Rn as elementary strict LTLnode over v by A4;
set n1=n+1;
set w1 = Shift(w,n);
A9: run.n = chosen_run(w,v,chf).n by A7;
Run(n) = CastNode(chosen_run(w,v,chf).n,v) by A7;
then
A10: w1 |= * ('X' Rn) by A1,Th73;
run.n1 = chosen_run(w,v,chf).n1 by A7
.= chosen_next(w1,v,chf,Rn) by A9,Def50;
then Run(n1) = chosen_next(w1,v,chf,Rn) by Def16;
hence thesis by A10,Th69;
end;
A11: for n holds CastSeq(w,AtomicFamily).n in Label_(Run(n+1))
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
set Rn1 = Run(n+1);
set w1= Shift(w,n);
set X = CastSeq(w,AtomicFamily).n;
reconsider X as Subset of atomic_LTL;
CastSeq(w1,AtomicFamily) = CastSeq(w,AtomicFamily)^\n by MODELC_2:81;
then
A12: CastSeq(w1,AtomicFamily).0 = CastSeq(w,AtomicFamily).(0+n) by NAT_1:def 3
;
A13: w1 |= * Rn1 by A8;
A14: now
assume not Neg_atomic_LTL(Rn1) misses X;
then Neg_atomic_LTL(Rn1) /\ X <> {} by XBOOLE_0:def 7;
then consider a being object such that
A15: a in Neg_atomic_LTL(Rn1) /\ X by XBOOLE_0:def 1;
a in Neg_atomic_LTL(Rn1) by A15,XBOOLE_0:def 4;
then consider x being LTL-formula such that
A16: x = a & x is atomic and
A17: ('not' x) in the LTLold of Rn1;
('not' x) in * Rn1 by A17,Lm1;
then w1 |= ('not' x) by A13;
then
A18: w1 |/= x by MODELC_2:64;
a in X by A15,XBOOLE_0:def 4;
hence contradiction by A12,A16,A18,MODELC_2:63;
end;
atomic_LTL(Rn1) c= X
proof
let a be object;
assume a in atomic_LTL(Rn1);
then consider x being LTL-formula such that
A19: x = a & x is atomic and
A20: x in the LTLold of Rn1;
x in * Rn1 by A20,Lm1;
then w1 |= x by A13;
hence thesis by A12,A19,MODELC_2:63;
end;
hence thesis by A14;
end;
A21: 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 12;
set R = Run(n);
reconsider R as elementary strict LTLnode over v by A4;
set n1=n+1;
set r = run.n;
set r1 = run.n1;
set R1 = Run(n1);
set gA = CastSeq(w,AtomicFamily).n;
set y = [[r, gA], r1];
reconsider R1 as elementary strict LTLnode over v by A4;
[r, gA] in [: LS, AtomicFamily :] by ZFMISC_1:87;
then [[r, gA],r1] in [:[: LS, AtomicFamily :],LS:] by ZFMISC_1:87;
then
A22: y is Element of [: LS, AtomicFamily, LS:] by ZFMISC_1:def 3;
reconsider r1 as elementary strict LTLnode over v by A4;
reconsider r as elementary strict LTLnode over v by A4;
A23: R1 is_next_of R & gA in Label_(R1) by A8,A11;
R = r & R1 = r1 by Def16;
hence thesis by A22,A23;
end;
A24: 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 A7;
hence thesis by A1,Th74;
end;
A25: 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;
set FK = {k where k is Element of NAT:run.k in FSet};
assume FSet in FS;
then consider x being Element of bool LS such that
A26: FSet = x and
A27: ex F st F is_subformula_of v & F is Until & x= FinalS_LTL(F,v);
consider F such that
F is_subformula_of v and
A28: F is Until and
A29: x= FinalS_LTL(F,v) by A27;
set F2 = the_right_argument_of F;
set F1 = the_left_argument_of F;
A30: F = F1 'U' F2 by A28,MODELC_2:8;
now
assume not FK is infinite set;
then consider L such that
A31: FK = rng L by FINSEQ_1:52;
ex m st for k st m<=k holds not k in FK
proof
A32: len L = 0 or 0< 0+len L;
now
per cases by A32,NAT_1:19;
suppose
A33: 1<=len L;
set LEN = len L;
FK c= REAL
proof
let a be object;
assume a in FK;
then consider k being Element of NAT such that
A34: a=k & run.k in FSet;
k in REAL by XREAL_0:def 1;
hence thesis by A34;
end;
then reconsider L as FinSequence of REAL by A31,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 A33,FINSEQ_1:1;
then LEN in dom L by FINSEQ_1:def 3;
then b in rng L by FUNCT_1:3;
then ex k being Element of NAT st k=b & run.k in FSet by A31;
hence thesis by A33,RFINSEQ2:1;
end;
then reconsider iMAX as Nat by INT_1:53;
iMAX +1 is Nat;
then reconsider natMAX as Nat;
for k st natMAX<=k holds not k in FK
proof
let k;
assume
A35: natMAX <= k;
now
assume k in FK;
then consider i1 being object such that
A36: i1 in dom L and
A37: k = L.i1 by A31,FUNCT_1:def 3;
reconsider i1 as Element of NAT by A36;
i1 in Seg LEN by A36,FINSEQ_1:def 3;
then 1<=i1 & i1<=LEN by FINSEQ_1:1;
then k <= realMAX by A37,RFINSEQ2:1;
hence contradiction by A35,INT_1:32,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis;
end;
suppose
len L=0;
then L = {};
then for k st 0<=k holds not k in FK by A31;
hence thesis;
end;
end;
hence thesis;
end;
then consider m such that
A38: for k st m<=k holds not k in FK;
A39: 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
A40: not k in FK by A38;
reconsider k as Element of NAT by ORDINAL1:def 12;
set r = run.k;
reconsider r as elementary strict LTLnode over v by A4;
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 A26,A29;
hence contradiction by A40;
end;
hence thesis;
end;
set w1 = Shift(w,m);
set m1=m+1;
A41: w1 |= * Run(m1) by A8;
m<=m1 by NAT_1:11;
then F in the LTLold of Run(m1) by A39;
then F in * Run(m1) by Lm1;
then w1 |= F by A41;
then consider h such that
for j being Nat st j<h holds Shift(w1,j) |= F1 and
A42: Shift(w1,h) |= F2 by A30,MODELC_2:68;
set m2=m+h;
set m3 = m2+1;
m3 = m+(h+1);
then m<=m3 by NAT_1:11;
then
A43: F in the LTLold of Run(m3) & not F2 in the LTLold of Run(m3) by A39;
Shift(w,m2) |= F2 by A42,MODELC_2:80;
hence contradiction by A24,A28,A43;
end;
hence thesis;
end;
run.0 = chosen_run(w,v,chf).0 by A7
.= init v by Def50;
then run.0 in IS by TARSKI:def 1;
hence thesis by A21,A25;
end;
hence thesis;
end;
theorem
w is-accepted-by BAutomaton(v) iff w |= v by Th68,Th75;