let w be Element of Inf_seq AtomicFamily ; :: thesis: for v being neg-inner-most LTL-formula st w is-accepted-by BAutomaton v holds
w |= v
let v be neg-inner-most LTL-formula; :: thesis: ( w is-accepted-by BAutomaton v implies w |= v )
deffunc H₁( Nat) -> set = (CastSeq w,AtomicFamily ) . $1;
assume w is-accepted-by BAutomaton v ; :: thesis: w |= v
then consider run being sequence of (LTLStates v) such that
A1: run . 0 in InitS_LTL v and
A2: for i being Nat holds [[(run . i),H₁(i)],(run . (i + 1))] in Tran_LTL v and
A3: for FSet being set st FSet in FinalS_LTL v holds
{ k where k is Element of NAT : run . k in FSet } is infinite set by Def39;
deffunc H₂( Nat) -> strict LTLnode of v = CastNode (run . $1),v;
set Run01 = H₂(0 + 1);
set Run00 = H₂( 0 );
A4: for i being Nat holds
( H₂(i + 1) is_next_of H₂(i) & H₁(i) in Label_ H₂(i + 1) )

proof

let i be Nat; :: thesis: ( H₂(i + 1) is_next_of H₂(i) & H₁(i) in Label_ H₂(i + 1) )
set z = [[(run . i),H₁(i)],(run . (i + 1))];
[[(run . i),H₁(i)],(run . (i + 1))] in Tran_LTL v by A2;
then consider y being Element of [:(LTLStates v),AtomicFamily ,(LTLStates v):] such that
A5: [[(run . i),H₁(i)],(run . (i + 1))] = y and
A6: ex s, s1 being strict elementary LTLnode of v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) ;
consider s, s1 being strict elementary LTLnode of v, x being set such that
A7: y = [[s,x],s1] and
A8: ( s1 is_next_of s & x in Label_ s1 ) by A6;
A9: H₂(i + 1) = CastNode s1,v by A5, A7, ZFMISC_1:33
.= s1 by Def16 ;
A10: [s,x] = [(run . i),H₁(i)] by A5, A7, ZFMISC_1:33;
then H₂(i) = CastNode s,v by ZFMISC_1:33
.= s by Def16 ;
hence ( H₂(i + 1) is_next_of H₂(i) & H₁(i) in Label_ H₂(i + 1) ) by A8, A10, A9, ZFMISC_1:33; :: thesis: verum

end;

then A11: H₂(0 + 1) is_next_of H₂( 0 ) ;
defpred S₁[ Nat] means for i being Nat
for F being LTL-formula st F is_subformula_of v & len F <= $1 & F in the LTLold of H₂(i + 1) holds
Shift w,i |= F;
A12: for i being Nat holds H₂(i) = run . i

proof

let i be Nat; :: thesis: H₂(i) = run . i
reconsider i = i as Element of NAT by ORDINAL1:def 13;
run . i in LTLStates v ;
then ex x being Element of LTLNodes v st
( run . i = x & x is strict elementary LTLnode of v ) ;
hence H₂(i) = run . i by Def16; :: thesis: verum

end;

A13: for FSet being set st FSet in FinalS_LTL v holds
not { k where k is Element of NAT : H₂(k) in FSet } is finite

proof

let FSet be set ; :: thesis: ( FSet in FinalS_LTL v implies not { k where k is Element of NAT : H₂(k) in FSet } is finite )
set X = { k where k is Element of NAT : run . k in FSet } ;
set Y = { k where k is Element of NAT : H₂(k) in FSet } ;
A14: { k where k is Element of NAT : run . k in FSet } c= { k where k is Element of NAT : H₂(k) in FSet }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : run . k in FSet } or x in { k where k is Element of NAT : H₂(k) in FSet } )
assume x in { k where k is Element of NAT : run . k in FSet } ; :: thesis: x in { k where k is Element of NAT : H₂(k) in FSet }
then consider k being Element of NAT such that
A15: x = k and
A16: run . k in FSet ;
H₂(k) in FSet by A12, A16;
hence x in { k where k is Element of NAT : H₂(k) in FSet } by A15; :: thesis: verum

end;

assume FSet in FinalS_LTL v ; :: thesis: not { k where k is Element of NAT : H₂(k) in FSet } is finite
hence not { k where k is Element of NAT : H₂(k) in FSet } is finite by A3, A14; :: thesis: verum

end;

A17: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A18: S₁[n] ; :: thesis: S₁[n + 1]
A19: for i being Nat
for F being LTL-formula st F is_subformula_of v & len F = n + 1 & F in the LTLold of H₂(i + 1) holds
Shift w,i |= F

proof

let i be Nat; :: thesis: for F being LTL-formula st F is_subformula_of v & len F = n + 1 & F in the LTLold of H₂(i + 1) holds
Shift w,i |= F
let F be LTL-formula; :: thesis: ( F is_subformula_of v & len F = n + 1 & F in the LTLold of H₂(i + 1) implies Shift w,i |= F )
assume that
A20: F is_subformula_of v and
A21: len F = n + 1 and
A22: F in the LTLold of H₂(i + 1) ; :: thesis: Shift w,i |= F
set zeta = Shift w,i;

now

per cases ( F is Sub_atomic or F is conjunctive or F is disjunctive or F is next or F is Until or F is Release ) by A20, Th63, Th65;

suppose A23: F is Sub_atomic ; :: thesis: Shift w,i |= F

set Gi9 = Shift (CastSeq w,AtomicFamily ),i;
set Gi = H₁(i);
CastSeq (Shift w,i),AtomicFamily = Shift (CastSeq w,AtomicFamily ),i by MODELC_2:81;
then A24: (CastSeq (Shift w,i),AtomicFamily ) . 0 = (CastSeq w,AtomicFamily ) . (0 + i) by MODELC_2:def 45
.= H₁(i) ;
H₁(i) in Label_ H₂(i + 1) by A4;
then consider X being Subset of atomic_LTL such that
A25: H₁(i) = X and
A26: atomic_LTL H₂(i + 1) c= X and
A27: Neg_atomic_LTL H₂(i + 1) misses X ;
A28: (Neg_atomic_LTL H₂(i + 1)) /\ X = {} by A27, XBOOLE_0:def 7;

now

per cases ( F is atomic or ( F is negative & the_argument_of F is atomic ) ) by A23, Th64;

suppose A29: F is atomic ; :: thesis: Shift w,i |= F

then F in atomic_LTL H₂(i + 1) by A22;
hence Shift w,i |= F by A25, A26, A24, A29, MODELC_2:63; :: thesis: verum

end;

suppose A30: ( F is negative & the_argument_of F is atomic ) ; :: thesis: Shift w,i |= F

set Fa = the_argument_of F;
A31: F = 'not' (the_argument_of F) by A30, MODELC_2:4;
then ( Shift w,i |= F iff Shift w,i |/= the_argument_of F ) by MODELC_2:64;
then A32: ( Shift w,i |= F iff not the_argument_of F in H₁(i) ) by A24, A30, MODELC_2:63;
the_argument_of F in Neg_atomic_LTL H₂(i + 1) by A22, A30, A31;
hence Shift w,i |= F by A25, A28, A32, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence Shift w,i |= F ; :: thesis: verum

end;

suppose A33: ( F is conjunctive or F is disjunctive ) ; :: thesis: Shift w,i |= F

set h1 = the_left_argument_of F;
len (the_left_argument_of F) < n + 1 by A21, A33, MODELC_2:11;
then A34: len (the_left_argument_of F) <= n by NAT_1:13;
set Runi1 = H₂(i + 1);
set Runi = H₂(i);
A35: H₂(i + 1) is_next_of H₂(i) by A4;
set h2 = the_right_argument_of F;
len (the_right_argument_of F) < n + 1 by A21, A33, MODELC_2:11;
then A36: len (the_right_argument_of F) <= n by NAT_1:13;
reconsider Runi1 = H₂(i + 1) as strict elementary LTLnode of v by A35, Def20;
reconsider Runi = H₂(i) as strict elementary LTLnode of v by A35, Def20;
A37: ( Runi1 is_next_of Runi & F in the LTLold of Runi1 implies ( ( F is conjunctive implies ( the_left_argument_of F in the LTLold of Runi1 & the_right_argument_of F in the LTLold of Runi1 ) ) & ( not F is disjunctive or the_left_argument_of F in the LTLold of Runi1 or the_right_argument_of F in the LTLold of Runi1 ) ) ) by Th41;
A38: ( the_left_argument_of F is_subformula_of F & the_right_argument_of F is_subformula_of F ) by A33, MODELC_2:31;
Shift w,i |= F

proof

now

per cases ( F is conjunctive or F is disjunctive ) by A33;

suppose A39: F is conjunctive ; :: thesis: Shift w,i |= F

then ( Shift w,i |= the_left_argument_of F & Shift w,i |= the_right_argument_of F ) by A4, A18, A20, A22, A38, A34, A36, A37, MODELC_2:35;
then Shift w,i |= (the_left_argument_of F) '&' (the_right_argument_of F) by MODELC_2:65;
hence Shift w,i |= F by A39, MODELC_2:6; :: thesis: verum

end;

suppose A40: F is disjunctive ; :: thesis: Shift w,i |= F

then ( Shift w,i |= the_left_argument_of F or Shift w,i |= the_right_argument_of F ) by A4, A18, A20, A22, A38, A34, A36, A37, MODELC_2:35;
then Shift w,i |= (the_left_argument_of F) 'or' (the_right_argument_of F) by MODELC_2:66;
hence Shift w,i |= F by A40, MODELC_2:7; :: thesis: verum

end;

end;

end;

hence Shift w,i |= F ; :: thesis: verum

end;

hence Shift w,i |= F ; :: thesis: verum

end;

suppose A41: F is next ; :: thesis: Shift w,i |= F

set i1 = i + 1;
set Runi1 = H₂(i + 1);
set Runi2 = H₂((i + 1) + 1);
H₂((i + 1) + 1) is_next_of H₂(i + 1) by A4;
then reconsider Runi2 = H₂((i + 1) + 1) as strict elementary LTLnode of v by Def20;
set Runi = H₂(i);
A42: H₂(i + 1) is_next_of H₂(i) by A4;
set h = the_argument_of F;
A43: the_argument_of F is_subformula_of F by A41, MODELC_2:30;
len (the_argument_of F) < n + 1 by A21, A41, MODELC_2:10;
then A44: len (the_argument_of F) <= n by NAT_1:13;
reconsider Runi1 = H₂(i + 1) as strict elementary LTLnode of v by A42, Def20;
reconsider Runi = H₂(i) as strict elementary LTLnode of v by A42, Def20;
A45: ( Runi1 is_next_of Runi & F in the LTLold of Runi1 & F is next implies the_argument_of F in the LTLnext of Runi1 ) by Th41;
the LTLnext of Runi1 c= the LTLold of Runi2 by A4, Th37;
then Shift w,(i + 1) |= the_argument_of F by A4, A18, A20, A22, A41, A43, A44, A45, MODELC_2:35;
then Shift (Shift w,i),1 |= the_argument_of F by MODELC_2:80;
then Shift w,i |= 'X' (the_argument_of F) by MODELC_2:67;
hence Shift w,i |= F by A41, MODELC_2:5; :: thesis: verum

end;

suppose A46: F is Until ; :: thesis: Shift w,i |= F

set Fin = FinalS_LTL F,v;
deffunc H₃( set ) -> set = run . ((CastNat $1) + i);
set FRun = { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ;
A47: for x being set st x in NAT holds
H₃(x) in LTLStates v

proof

let x be set ; :: thesis: ( x in NAT implies H₃(x) in LTLStates v )
assume x in NAT ; :: thesis: H₃(x) in LTLStates v
set y = (CastNat x) + i;
reconsider y = (CastNat x) + i as Element of NAT by ORDINAL1:def 13;
H₃(x) = run . y ;
hence H₃(x) in LTLStates v ; :: thesis: verum

end;

consider runQ being Function of NAT ,(LTLStates v) such that
A48: for x being set st x in NAT holds
runQ . x = H₃(x) from FUNCT_2:sch 2(A47);
reconsider runQ = runQ as sequence of (LTLStates v) ;
deffunc H₄( Nat) -> strict LTLnode of v = CastNode (runQ . $1),v;
A49: for m being Nat holds H₄(m) = H₂(m + i)

proof

let m be Nat; :: thesis: H₄(m) = H₂(m + i)
reconsider m = m as Element of NAT by ORDINAL1:def 13;
H₄(m) = CastNode H₃(m),v by A48
.= H₂(m + i) by MODELC_2:def 1 ;
hence H₄(m) = H₂(m + i) ; :: thesis: verum

end;

A50: for m being Nat holds H₄(m + 1) is_next_of H₄(m)

proof

let m be Nat; :: thesis: H₄(m + 1) is_next_of H₄(m)
set m1 = m + i;
A51: H₄(m + 1) = H₂((m + 1) + i) by A49
.= H₂((m + i) + 1) ;
H₄(m) = H₂(m + i) by A49;
hence H₄(m + 1) is_next_of H₄(m) by A4, A51; :: thesis: verum

end;

set FRunQ = { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } ;
A52: FinalS_LTL F,v in FinalS_LTL v by A20, A46;
A53: not { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite

proof

set FRun2 = { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } ;
set FRun1 = { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } ;
A54: { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } c= (Seg i) \/ {0 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } or x in (Seg i) \/ {0 } )
assume x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } ; :: thesis: x in (Seg i) \/ {0 }
then consider k being Element of NAT such that
A55: x = k and
A56: k <= i and
k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ;

now

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: x in (Seg i) \/ {0 }

then k in {0 } by TARSKI:def 1;
hence x in (Seg i) \/ {0 } by A55, XBOOLE_0:def 3; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: x in (Seg i) \/ {0 }

then 0 < 0 + k ;
then 1 <= k by NAT_1:19;
then k in Seg i by A56, FINSEQ_1:3;
hence x in (Seg i) \/ {0 } by A55, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (Seg i) \/ {0 } ; :: thesis: verum

end;

A57: ( { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite implies { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } is finite )

proof

deffunc H₅( set ) -> set = (CastNat $1) + i;
consider fun being Function such that
A58: ( dom fun = { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } & ( for x being set st x in { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } holds
fun . x = H₅(x) ) ) from FUNCT_1:sch 3();
A59: for x being set st x in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } holds
(CastNat x) - i in { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v }

proof

let x be set ; :: thesis: ( x in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } implies (CastNat x) - i in { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } )
assume x in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } ; :: thesis: (CastNat x) - i in { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v }
then consider k being Element of NAT such that
A60: x = k and
A61: i < k and
A62: k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ;
set k2 = k - i;
reconsider k2 = k - i as Element of NAT by A61, NAT_1:21;
A63: H₄(k2) = H₂(k2 + i) by A49
.= H₂(k) ;
( ex k1 being Element of NAT st
( k = k1 & H₂(k1) in FinalS_LTL F,v ) & (CastNat x) - i = k2 ) by A60, A62, MODELC_2:def 1;
hence (CastNat x) - i in { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } by A63; :: thesis: verum

end;

A64: for y being set st y in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } holds
ex x being set st
( x in dom fun & y = fun . x )

proof

let y be set ; :: thesis: ( y in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } implies ex x being set st
( x in dom fun & y = fun . x ) )
assume A65: y in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } ; :: thesis: ex x being set st
( x in dom fun & y = fun . x )
consider k being Element of NAT such that
A66: y = k and
A67: i < k and
k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } by A65;
set x = (CastNat y) - i;
A68: (CastNat y) - i in dom fun by A59, A58, A65;
set k1 = k - i;
reconsider k1 = k - i as Nat by A67, NAT_1:21;
A69: (CastNat y) - i = k1 by A66, MODELC_2:def 1;
fun . ((CastNat y) - i) = H₅((CastNat y) - i) by A59, A58, A65
.= k1 + i by A69, MODELC_2:def 1
.= y by A66 ;
hence ex x being set st
( x in dom fun & y = fun . x ) by A68; :: thesis: verum

end;

assume { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite ; :: thesis: { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } is finite
then rng fun is finite by A58, FINSET_1:26;
hence { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } is finite by A64, FINSET_1:13, FUNCT_1:19; :: thesis: verum

end;

{ k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } c= { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } or x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } )
assume A70: x in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ; :: thesis: x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) }
then ex k being Element of NAT st
( x = k & H₂(k) in FinalS_LTL F,v ) ;
then reconsider x = x as Element of NAT ;

now

per cases ( x <= i or i < x ) ;

suppose x <= i ; :: thesis: x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) }

then x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } by A70;
hence x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose i < x ; :: thesis: x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) }

then x in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } by A70;
hence x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H₂(k) in FinalS_LTL F,v } ) } ; :: thesis: verum

end;

hence not { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite by A13, A52, A57, A54; :: thesis: verum

end;

set h2 = the_right_argument_of F;
set h1 = the_left_argument_of F;
len (the_left_argument_of F) < n + 1 by A21, A46, MODELC_2:11;
then A71: len (the_left_argument_of F) <= n by NAT_1:13;
A72: ( ( for m being Nat st m >= 1 holds
( F in the LTLold of H₄(m) & the_left_argument_of F in the LTLold of H₄(m) & not the_right_argument_of F in the LTLold of H₄(m) ) ) implies { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite )

proof

assume A73: for m being Nat st m >= 1 holds
( F in the LTLold of H₄(m) & the_left_argument_of F in the LTLold of H₄(m) & not the_right_argument_of F in the LTLold of H₄(m) ) ; :: thesis: { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite

now

assume not { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } c= {0 } ; :: thesis: contradiction
then consider x being set such that
A74: x in { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } and
A75: not x in {0 } by TARSKI:def 3;
consider k being Element of NAT such that
A76: x = k and
A77: H₄(k) in FinalS_LTL F,v by A74;
k <> 0 by A75, A76, TARSKI:def 1;
then 0 < 0 + k ;
then A78: 1 <= k by NAT_1:19;
set RQk = H₄(k);
consider y being Element of LTLStates v such that
A79: H₄(k) = y and
A80: ( not F in the LTLold of (CastNode y,v) or the_right_argument_of F in the LTLold of (CastNode y,v) ) by A77;
reconsider y = y as strict LTLnode of v by A79;
CastNode y,v = H₄(k) by A79, Def16;
hence contradiction by A73, A78, A80; :: thesis: verum

end;

hence { k where k is Element of NAT : H₄(k) in FinalS_LTL F,v } is finite ; :: thesis: verum

end;

F in the LTLold of H₄(1) by A22, A49;
then consider j being Nat such that
A81: j >= 1 and
A82: the_right_argument_of F in the LTLold of H₄(j) and
A83: for m being Nat st 1 <= m & m < j holds
( F in the LTLold of H₄(m) & the_left_argument_of F in the LTLold of H₄(m) ) by A46, A50, A53, A72, Th54;
set j0 = j - 1;
reconsider j0 = j - 1 as Nat by A81, NAT_1:21;
set j1 = j0 + i;
(j0 + i) + 1 = j + i ;
then A84: the_right_argument_of F in the LTLold of H₂((j0 + i) + 1) by A49, A82;
A85: the_left_argument_of F is_subformula_of F by A46, MODELC_2:31;
A86: for k being Nat st k < j0 holds
Shift (Shift w,i),k |= the_left_argument_of F

proof

let k be Nat; :: thesis: ( k < j0 implies Shift (Shift w,i),k |= the_left_argument_of F )
assume A87: k < j0 ; :: thesis: Shift (Shift w,i),k |= the_left_argument_of F
set k1 = k + 1;
set ki = k + i;
( 1 <= k + 1 & k + 1 < j0 + 1 ) by A87, NAT_1:11, XREAL_1:10;
then the_left_argument_of F in the LTLold of H₄(k + 1) by A83;
then the_left_argument_of F in the LTLold of H₂((k + 1) + i) by A49;
then the_left_argument_of F in the LTLold of H₂((k + i) + 1) ;
then Shift w,(k + i) |= the_left_argument_of F by A18, A20, A85, A71, MODELC_2:35;
hence Shift (Shift w,i),k |= the_left_argument_of F by MODELC_2:80; :: thesis: verum

end;

len (the_right_argument_of F) < n + 1 by A21, A46, MODELC_2:11;
then A88: len (the_right_argument_of F) <= n by NAT_1:13;
the_right_argument_of F is_subformula_of F by A46, MODELC_2:31;
then Shift w,(j0 + i) |= the_right_argument_of F by A18, A20, A88, A84, MODELC_2:35;
then A89: Shift (Shift w,i),j0 |= the_right_argument_of F by MODELC_2:80;
F = (the_left_argument_of F) 'U' (the_right_argument_of F) by A46, MODELC_2:8;
hence Shift w,i |= F by A89, A86, MODELC_2:68; :: thesis: verum

end;

suppose A90: F is Release ; :: thesis: Shift w,i |= F

set h2 = the_right_argument_of F;
A91: the_right_argument_of F is_subformula_of F by A90, MODELC_2:31;
set h1 = the_left_argument_of F;
defpred S₂[ Nat] means ( ( for k being Nat st k < $1 holds
Shift (Shift w,i),k |= 'not' (the_left_argument_of F) ) implies ( Shift (Shift w,i),$1 |= the_right_argument_of F & F in the LTLold of H₂((i + 1) + $1) ) );
len (the_left_argument_of F) < n + 1 by A21, A90, MODELC_2:11;
then A92: len (the_left_argument_of F) <= n by NAT_1:13;
len (the_right_argument_of F) < n + 1 by A21, A90, MODELC_2:11;
then A93: len (the_right_argument_of F) <= n by NAT_1:13;
A94: the_left_argument_of F is_subformula_of F by A90, MODELC_2:31;
A95: for j being Nat st S₂[j] holds
S₂[j + 1]

proof

let j be Nat; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A96: S₂[j] ; :: thesis: S₂[j + 1]
S₂[j + 1]

proof

set i1 = i + j;
set Run1 = H₂((i + j) + 1);
set Run0 = H₂(i + j);
assume A97: for k being Nat st k < j + 1 holds
Shift (Shift w,i),k |= 'not' (the_left_argument_of F) ; :: thesis: ( Shift (Shift w,i),(j + 1) |= the_right_argument_of F & F in the LTLold of H₂((i + 1) + (j + 1)) )
A98: for k being Nat st k < j holds
Shift (Shift w,i),k |= 'not' (the_left_argument_of F)

proof

A99: j <= j + 1 by NAT_1:11;
let k be Nat; :: thesis: ( k < j implies Shift (Shift w,i),k |= 'not' (the_left_argument_of F) )
assume k < j ; :: thesis: Shift (Shift w,i),k |= 'not' (the_left_argument_of F)
then k < j + 1 by A99, XXREAL_0:2;
hence Shift (Shift w,i),k |= 'not' (the_left_argument_of F) by A97; :: thesis: verum

end;

A100: H₂((i + j) + 1) is_next_of H₂(i + j) by A4;
then reconsider Run0 = H₂(i + j) as strict elementary LTLnode of v by Def20;
set i2 = (i + j) + 1;
set Run2 = H₂(((i + j) + 1) + 1);
A101: H₂(((i + j) + 1) + 1) is_next_of H₂((i + j) + 1) by A4;
then reconsider Run2 = H₂(((i + j) + 1) + 1) as strict elementary LTLnode of v by Def20;
reconsider Run1 = H₂((i + j) + 1) as strict elementary LTLnode of v by A100, Def20;
j < j + 1 by NAT_1:13;
then A102: Shift (Shift w,i),j |= 'not' (the_left_argument_of F) by A97;

A103: now

assume the_left_argument_of F in the LTLold of Run1 ; :: thesis: contradiction
then Shift w,(i + j) |= the_left_argument_of F by A18, A20, A94, A92, MODELC_2:35;
then Shift (Shift w,i),j |= the_left_argument_of F by MODELC_2:80;
hence contradiction by A102, MODELC_2:64; :: thesis: verum

end;

A104: ( Run1 is_next_of Run0 & F is Release & F in the LTLold of Run1 & not the_left_argument_of F in the LTLold of Run1 implies ( the_right_argument_of F in the LTLold of Run1 & F in the LTLnext of Run1 ) ) by Th39;
then the_right_argument_of F in the LTLold of Run2 by A4, A90, A96, A101, A98, A103, Th40;
then A105: Shift w,(i + (j + 1)) |= the_right_argument_of F by A18, A20, A91, A93, MODELC_2:35;
F in the LTLold of Run2 by A4, A90, A96, A101, A98, A103, A104, Th40;
hence ( Shift (Shift w,i),(j + 1) |= the_right_argument_of F & F in the LTLold of H₂((i + 1) + (j + 1)) ) by A105, MODELC_2:80; :: thesis: verum

end;

hence S₂[j + 1] ; :: thesis: verum

end;

A106: F = (the_left_argument_of F) 'R' (the_right_argument_of F) by A90, MODELC_2:9;
A107: ( ( for j being Nat holds S₂[j] ) implies Shift w,i |= F )

proof

assume for j being Nat holds S₂[j] ; :: thesis: Shift w,i |= F
then for j being Nat st ( for k being Nat st k < j holds
Shift (Shift w,i),k |= 'not' (the_left_argument_of F) ) holds
Shift (Shift w,i),j |= the_right_argument_of F ;
hence Shift w,i |= F by A106, MODELC_2:69; :: thesis: verum

end;

A108: S₂[ 0 ]

proof

set Run0 = H₂(i);
set Run1 = H₂(i + 1);
A109: H₂(i + 1) is_next_of H₂(i) by A4;
then reconsider Run1 = H₂(i + 1) as strict elementary LTLnode of v by Def20;
reconsider Run0 = H₂(i) as strict elementary LTLnode of v by A109, Def20;
assume for k being Nat st k < 0 holds
Shift (Shift w,i),k |= 'not' (the_left_argument_of F) ; :: thesis: ( Shift (Shift w,i),0 |= the_right_argument_of F & F in the LTLold of H₂((i + 1) + 0 ) )
A110: Shift (Shift w,i),0 = Shift w,i by MODELC_2:79;
( Run1 is_next_of Run0 & F in the LTLold of Run1 & F is Release implies the_right_argument_of F in the LTLold of Run1 ) by Th41;
hence ( Shift (Shift w,i),0 |= the_right_argument_of F & F in the LTLold of H₂((i + 1) + 0 ) ) by A4, A18, A20, A22, A90, A91, A93, A110, MODELC_2:35; :: thesis: verum

end;

for j being Nat holds S₂[j] from NAT_1:sch 2(A108, A95);
hence Shift w,i |= F by A107; :: thesis: verum

end;

end;

end;

hence Shift w,i |= F ; :: thesis: verum

end;

S₁[n + 1]

proof

let i be Nat; :: thesis: for F being LTL-formula st F is_subformula_of v & len F <= n + 1 & F in the LTLold of H₂(i + 1) holds
Shift w,i |= F
let F be LTL-formula; :: thesis: ( F is_subformula_of v & len F <= n + 1 & F in the LTLold of H₂(i + 1) implies Shift w,i |= F )
assume that
A111: F is_subformula_of v and
A112: len F <= n + 1 and
A113: F in the LTLold of H₂(i + 1) ; :: thesis: Shift w,i |= F
set L = len F;
reconsider L = len F as Nat ;

now

per cases ( L <= n or L = n + 1 ) by A112, NAT_1:8;

suppose L <= n ; :: thesis: Shift w,i |= F

hence Shift w,i |= F by A18, A111, A113; :: thesis: verum

end;

suppose L = n + 1 ; :: thesis: Shift w,i |= F

hence Shift w,i |= F by A19, A111, A113; :: thesis: verum

end;

end;

end;

hence Shift w,i |= F ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A114: S₁[ 0 ] by MODELC_2:3;
A115: for n being Nat holds S₁[n] from NAT_1:sch 2(A114, A17);
set n = len v;
A116: ( v in {v} & len v <= len v ) by TARSKI:def 1;
reconsider Run01 = H₂(0 + 1) as strict elementary LTLnode of v by A11, Def20;
reconsider Run00 = H₂( 0 ) as strict elementary LTLnode of v by A11, Def20;
A117: the LTLnext of Run00 c= the LTLold of Run01 by A4, Th37;
H₂( 0 ) = CastNode (init v),v by A1, TARSKI:def 1
.= init v by Def16 ;
then Shift w,0 |= v by A117, A115, A116, MODELC_2:27;
hence w |= v by MODELC_2:79; :: thesis: verum