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 H1( Nat) -> Element of AtomicFamily = (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),H1(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 ;
deffunc H2( Nat) -> strict LTLnode over v = CastNode ((run . $1),v);
set Run01 = H2(0 + 1);
set Run00 = H2( 0 );
A4: for i being Nat holds
( H2(i + 1) is_next_of H2(i) & H1(i) in Label_ H2(i + 1) )
proof
let i be Nat; :: thesis: ( H2(i + 1) is_next_of H2(i) & H1(i) in Label_ H2(i + 1) )
set z = [[(run . i),H1(i)],(run . (i + 1))];
[[(run . i),H1(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),H1(i)],(run . (i + 1))] = y and
A6: ex s, s1 being strict elementary LTLnode over 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 over 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: H2(i + 1) = CastNode (s1,v) by A5, A7, XTUPLE_0:1
.= s1 by Def16 ;
A10: [s,x] = [(run . i),H1(i)] by A5, A7, XTUPLE_0:1;
then H2(i) = CastNode (s,v) by XTUPLE_0:1
.= s by Def16 ;
hence ( H2(i + 1) is_next_of H2(i) & H1(i) in Label_ H2(i + 1) ) by A8, A10, A9, XTUPLE_0:1; :: thesis: verum
end;
then A11: H2(0 + 1) is_next_of H2( 0 ) ;
defpred S1[ 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 H2(i + 1) holds
Shift (w,i) |= F;
A12: for i being Nat holds H2(i) = run . i
proof
let i be Nat; :: thesis: H2(i) = run . i
reconsider i = 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 strict elementary LTLnode over v ) ;
hence H2(i) = run . i by Def16; :: thesis: verum
end;
A13: for FSet being set st FSet in FinalS_LTL v holds
{ k where k is Element of NAT : H2(k) in FSet } is infinite
proof
let FSet be set ; :: thesis: ( FSet in FinalS_LTL v implies { k where k is Element of NAT : H2(k) in FSet } is infinite )
set X = { k where k is Element of NAT : run . k in FSet } ;
set Y = { k where k is Element of NAT : H2(k) in FSet } ;
A14: { k where k is Element of NAT : run . k in FSet } c= { k where k is Element of NAT : H2(k) in FSet }
proof
let x be object ; :: 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 : H2(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 : H2(k) in FSet }
then consider k being Element of NAT such that
A15: x = k and
A16: run . k in FSet ;
H2(k) in FSet by A12, A16;
hence x in { k where k is Element of NAT : H2(k) in FSet } by A15; :: thesis: verum
end;
assume FSet in FinalS_LTL v ; :: thesis: { k where k is Element of NAT : H2(k) in FSet } is infinite
hence { k where k is Element of NAT : H2(k) in FSet } is infinite by A3, A14; :: thesis: verum
end;
A17: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A18: S1[n] ; :: thesis: S1[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 H2(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 H2(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 H2(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 H2(i + 1) ; :: thesis: Shift (w,i) |= F
set zeta = Shift (w,i);
now :: thesis: Shift (w,i) |= F
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 = (CastSeq (w,AtomicFamily)) ^\ i;
set Gi = H1(i);
CastSeq ((Shift (w,i)),AtomicFamily) = (CastSeq (w,AtomicFamily)) ^\ i by MODELC_2:81;
then A24: (CastSeq ((Shift (w,i)),AtomicFamily)) . 0 = (CastSeq (w,AtomicFamily)) . (0 + i) by NAT_1:def 3
.= H1(i) ;
H1(i) in Label_ H2(i + 1) by A4;
then consider X being Subset of atomic_LTL such that
A25: H1(i) = X and
A26: atomic_LTL H2(i + 1) c= X and
A27: Neg_atomic_LTL H2(i + 1) misses X ;
A28: (Neg_atomic_LTL H2(i + 1)) /\ X = {} by A27, XBOOLE_0:def 7;
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 = H2(i + 1);
set Runi = H2(i);
A35: H2(i + 1) is_next_of H2(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 = H2(i + 1) as strict elementary LTLnode over v by A35;
reconsider Runi = H2(i) as strict elementary LTLnode over v by A35;
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 :: thesis: Shift (w,i) |= F
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 = H2(i + 1);
set Runi2 = H2((i + 1) + 1);
H2((i + 1) + 1) is_next_of H2(i + 1) by A4;
then reconsider Runi2 = H2((i + 1) + 1) as strict elementary LTLnode over v ;
set Runi = H2(i);
A42: H2(i + 1) is_next_of H2(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 = H2(i + 1) as strict elementary LTLnode over v by A42;
reconsider Runi = H2(i) as strict elementary LTLnode over v by A42;
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 H3( set ) -> Element of LTLStates v = run . ((CastNat $1) + i);
set FRun = { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ;
A47: for x being set st x in NAT holds
H3(x) in LTLStates v ;
consider runQ being sequence of (LTLStates v) such that
A48: for x being set st x in NAT holds
runQ . x = H3(x) from FUNCT_2:sch 11(A47);
reconsider runQ = runQ as sequence of (LTLStates v) ;
deffunc H4( Nat) -> strict LTLnode over v = CastNode ((runQ . $1),v);
A49: for m being Nat holds H4(m) = H2(m + i)
proof
let m be Nat; :: thesis: H4(m) = H2(m + i)
reconsider m = m as Element of NAT by ORDINAL1:def 12;
H4(m) = CastNode (H3(m),v) by A48
.= H2(m + i) by MODELC_2:def 1 ;
hence H4(m) = H2(m + i) ; :: thesis: verum
end;
A50: for m being Nat holds H4(m + 1) is_next_of H4(m)
proof
let m be Nat; :: thesis: H4(m + 1) is_next_of H4(m)
set m1 = m + i;
A51: H4(m + 1) = H2((m + 1) + i) by A49
.= H2((m + i) + 1) ;
H4(m) = H2(m + i) by A49;
hence H4(m + 1) is_next_of H4(m) by A4, A51; :: thesis: verum
end;
set FRunQ = { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } ;
A52: FinalS_LTL (F,v) in FinalS_LTL v by A20, A46;
A53: { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } is infinite
proof
set FRun2 = { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(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 : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } c= (Seg i) \/ {0}
proof
let x be object ; :: 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 : H2(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 : H2(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 : H2(k) in FinalS_LTL (F,v) } ;
hence x in (Seg i) \/ {0} ; :: thesis: verum
end;
A57: ( { k where k is Element of NAT : H4(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 : H2(k) in FinalS_LTL (F,v) } ) } is finite )
proof
deffunc H5( object ) -> set = (CastNat $1) + i;
consider fun being Function such that
A58: ( dom fun = { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } & ( for x being object st x in { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } holds
fun . x = H5(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 : H2(k) in FinalS_LTL (F,v) } ) } holds
(CastNat x) - i in { k where k is Element of NAT : H4(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 : H2(k) in FinalS_LTL (F,v) } ) } implies (CastNat x) - i in { k where k is Element of NAT : H4(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 : H2(k) in FinalS_LTL (F,v) } ) } ; :: thesis: (CastNat x) - i in { k where k is Element of NAT : H4(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 : H2(k) in FinalS_LTL (F,v) } ;
set k2 = k - i;
reconsider k2 = k - i as Element of NAT by A61, NAT_1:21;
A63: H4(k2) = H2(k2 + i) by A49
.= H2(k) ;
( ex k1 being Element of NAT st
( k = k1 & H2(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 : H4(k) in FinalS_LTL (F,v) } by A63; :: thesis: verum
end;
A64: for y being object st y in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) } holds
ex x being object st
( x in dom fun & y = fun . x )
proof
let y be object ; :: thesis: ( y in { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) } implies ex x being object 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 : H2(k) in FinalS_LTL (F,v) } ) } ; :: thesis: ex x being object 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 : H2(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) = H5((CastNat y) - i) by A59, A58, A65
.= k1 + i by A69, MODELC_2:def 1
.= y by A66 ;
hence ex x being object st
( x in dom fun & y = fun . x ) by A68; :: thesis: verum
end;
assume { k where k is Element of NAT : H4(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 : H2(k) in FinalS_LTL (F,v) } ) } is finite
then rng fun is finite by A58, FINSET_1:8;
hence { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) } is finite by A64, FINSET_1:1, FUNCT_1:9; :: thesis: verum
end;
{ k where k is Element of NAT : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) } )
assume A70: x in { k where k is Element of NAT : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) }
then ex k being Element of NAT st
( x = k & H2(k) in FinalS_LTL (F,v) ) ;
then reconsider x = x as Element of NAT ;
now :: thesis: x in { k where k is Element of NAT : ( k <= i & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) }
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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(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 : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(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 : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(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 : H2(k) in FinalS_LTL (F,v) } ) } \/ { k where k is Element of NAT : ( i < k & k in { k where k is Element of NAT : H2(k) in FinalS_LTL (F,v) } ) } ; :: thesis: verum
end;
hence { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } is infinite 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 H4(m) & the_left_argument_of F in the LTLold of H4(m) & not the_right_argument_of F in the LTLold of H4(m) ) ) implies { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } is finite )
proof
assume A73: for m being Nat st m >= 1 holds
( F in the LTLold of H4(m) & the_left_argument_of F in the LTLold of H4(m) & not the_right_argument_of F in the LTLold of H4(m) ) ; :: thesis: { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } is finite
now :: thesis: { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } c= {0}
assume not { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } c= {0} ; :: thesis: contradiction
then consider x being object such that
A74: x in { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } and
A75: not x in {0} ;
consider k being Element of NAT such that
A76: x = k and
A77: H4(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 = H4(k);
consider y being Element of LTLStates v such that
A79: H4(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 over v by A79;
CastNode (y,v) = H4(k) by A79, Def16;
hence contradiction by A73, A78, A80; :: thesis: verum
end;
hence { k where k is Element of NAT : H4(k) in FinalS_LTL (F,v) } is finite ; :: thesis: verum
end;
F in the LTLold of H4(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 H4(j) and
A83: for m being Nat st 1 <= m & m < j holds
( F in the LTLold of H4(m) & the_left_argument_of F in the LTLold of H4(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 H2((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:8;
then the_left_argument_of F in the LTLold of H4(k + 1) by A83;
then the_left_argument_of F in the LTLold of H2((k + 1) + i) by A49;
then the_left_argument_of F in the LTLold of H2((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 S2[ 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 H2((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 S2[j] holds
S2[j + 1]
proof
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
assume A96: S2[j] ; :: thesis: S2[j + 1]
S2[j + 1]
proof
set i1 = i + j;
set Run1 = H2((i + j) + 1);
set Run0 = H2(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 H2((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: H2((i + j) + 1) is_next_of H2(i + j) by A4;
then reconsider Run0 = H2(i + j) as strict elementary LTLnode over v ;
set i2 = (i + j) + 1;
set Run2 = H2(((i + j) + 1) + 1);
A101: H2(((i + j) + 1) + 1) is_next_of H2((i + j) + 1) by A4;
then reconsider Run2 = H2(((i + j) + 1) + 1) as strict elementary LTLnode over v ;
reconsider Run1 = H2((i + j) + 1) as strict elementary LTLnode over v by A100;
j < j + 1 by NAT_1:13;
then A102: Shift ((Shift (w,i)),j) |= 'not' (the_left_argument_of F) by A97;
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 H2((i + 1) + (j + 1)) ) by A105, MODELC_2:80; :: thesis: verum
end;
hence S2[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 S2[j] ) implies Shift (w,i) |= F )
proof
assume for j being Nat holds S2[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: S2[ 0 ]
proof
set Run0 = H2(i);
set Run1 = H2(i + 1);
A109: H2(i + 1) is_next_of H2(i) by A4;
then reconsider Run1 = H2(i + 1) as strict elementary LTLnode over v ;
reconsider Run0 = H2(i) as strict elementary LTLnode over v by A109;
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 H2((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 H2((i + 1) + 0) ) by A4, A18, A20, A22, A90, A91, A93, A110, MODELC_2:35; :: thesis: verum
end;
for j being Nat holds S2[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;
S1[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 H2(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 H2(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 H2(i + 1) ; :: thesis: Shift (w,i) |= F
set L = len F;
reconsider L = len F as Nat ;
now :: thesis: Shift (w,i) |= F
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 S1[n + 1] ; :: thesis: verum
end;
A114: S1[ 0 ] by MODELC_2:3;
A115: for n being Nat holds S1[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 = H2(0 + 1) as strict elementary LTLnode over v by A11;
reconsider Run00 = H2( 0 ) as strict elementary LTLnode over v by A11;
A117: the LTLnext of Run00 c= the LTLold of Run01 by A4, Th37;
H2( 0 ) = CastNode ((init v),v) by A1, TARSKI:def 1
.= init v by Def16 ;
then Shift (w,0) |= v by A117, A115, A116;
hence w |= v by MODELC_2:79; :: thesis: verum