let n be Nat; :: thesis: for F, G, v being LTL-formula
for q being sequence of (LTLStates v) st F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ( for i being Nat st 1 <= i & i < n holds
not G in the LTLold of (CastNode ((q . i),v)) ) holds
for i being Nat 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)) )
let F, G, v be LTL-formula; :: thesis: for q being sequence of (LTLStates v) st F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ( for i being Nat st 1 <= i & i < n holds
not G in the LTLold of (CastNode ((q . i),v)) ) holds
for i being Nat 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)) )
let q be sequence of (LTLStates v); :: thesis: ( F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ( for i being Nat st 1 <= i & i < n holds
not G in the LTLold of (CastNode ((q . i),v)) ) implies for i being Nat 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)) ) )
deffunc H1( Nat) -> strict LTLnode over v = CastNode ((q . $1),v);
assume that
A1: F 'U' G in the LTLold of H1(1) and
A2: for i being Nat holds H1(i + 1) is_next_of H1(i) ; :: thesis: ( ex i being Nat st
( 1 <= i & i < n & G in the LTLold of (CastNode ((q . i),v)) ) or for i being Nat 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)) ) )
defpred S1[ Nat] means ( ( for i being Nat st 1 <= i & i < $1 holds
not G in the LTLold of H1(i) ) implies for i being Nat st 1 <= i & i < $1 holds
( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) );
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
( ( for i being Nat st 1 <= i & i < k + 1 holds
not G in the LTLold of H1(i) ) implies for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) )
proof
assume A5: for i being Nat st 1 <= i & i < k + 1 holds
not G in the LTLold of H1(i) ; :: thesis: for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
A6: k <= k + 1 by NAT_1:11;
A7: for i being Nat st 1 <= i & i < k holds
not G in the LTLold of H1(i)
proof
let i be Nat; :: thesis: ( 1 <= i & i < k implies not G in the LTLold of H1(i) )
assume that
A8: 1 <= i and
A9: i < k ; :: thesis: not G in the LTLold of H1(i)
i < k + 1 by A6, A9, XXREAL_0:2;
hence not G in the LTLold of H1(i) by A5, A8; :: thesis: verum
end;
for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
proof
let i be Nat; :: thesis: ( 1 <= i & i < k + 1 implies ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) )
assume that
A10: 1 <= i and
A11: i < k + 1 ; :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
A12: i <= k by A11, NAT_1:13;
now :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
per cases ( i < k or i = k ) by A12, XXREAL_0:1;
suppose i < k ; :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
hence ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) by A4, A7, A10; :: thesis: verum
end;
suppose A13: i = k ; :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
now :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
per cases ( k = 1 or 1 < k ) by A10, A13, XXREAL_0:1;
suppose A14: k = 1 ; :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
A15: ( H1(0 + 1) is_next_of H1( 0 ) & H1(1 + 1) is_next_of H1(1) ) by A2;
consider s1 being strict elementary LTLnode over v such that
A16: s1 = H1(1) by Th52;
not G in the LTLold of s1 by A5, A14, A16;
hence ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) by A1, A13, A14, A16, A15, Lm29; :: thesis: verum
end;
suppose A17: 1 < k ; :: thesis: ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) )
set m = k - 1;
reconsider m = k - 1 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 = m - 1 as Nat by NAT_1:21;
consider sm being strict elementary LTLnode over v such that
A19: sm = H1(m) by Th52;
A20: m < m + 1 by NAT_1:19;
then m < k + 1 by A6, XXREAL_0:2;
then A21: not G in the LTLold of sm by A5, A18, A19;
A22: ( ex sk1 being strict elementary LTLnode over v st sk1 = H1(k + 1) & H1(m + 1) is_next_of H1(m) ) by A2, Th52;
A23: ( ex sm1 being strict elementary LTLnode over v st sm1 = H1(m1) & H1(m1 + 1) is_next_of H1(m1) ) by A2, Th52;
A24: H1(m + 1) is_next_of H1(m) by A2;
A25: H1(k + 1) is_next_of H1(k) by A2;
consider sk being strict elementary LTLnode over v such that
A26: sk = H1(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 ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) by A13, A26, A27, A22, A25, Lm29; :: thesis: verum
end;
end;
end;
hence ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) ; :: thesis: verum
end;
end;
end;
hence ( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) ; :: thesis: verum
end;
hence for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H1(i) & F 'U' G in the LTLold of H1(i) ) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A28: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A28, A3);
 hence ( ex i being Nat st
( 1 <= i & i < n & G in the LTLold of (CastNode ((q . i),v)) ) or for i being Nat 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)) ) ) ; :: thesis: verum