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 H₁( Nat) -> strict LTLnode of v = CastNode ((q . $1),v);
assume that
A1: F 'U' G in the LTLold of H₁(1) and
A2: for i being Nat holds H₁(i + 1) is_next_of H₁(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 S₁[ Nat] means ( ( for i being Nat st 1 <= i & i < $1 holds
not G in the LTLold of H₁(i) ) implies for i being Nat st 1 <= i & i < $1 holds
( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) );
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
( ( for i being Nat st 1 <= i & i < k + 1 holds
not G in the LTLold of H₁(i) ) implies for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) )

proof

assume A5: for i being Nat st 1 <= i & i < k + 1 holds
not G in the LTLold of H₁(i) ; :: thesis: for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(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 H₁(i)

proof

let i be Nat; :: thesis: ( 1 <= i & i < k implies not G in the LTLold of H₁(i) )
assume that
A8: 1 <= i and
A9: i < k ; :: thesis: not G in the LTLold of H₁(i)
i < k + 1 by A6, A9, XXREAL_0:2;
hence not G in the LTLold of H₁(i) by A5, A8; :: thesis: verum

end;

for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )

proof

let i be Nat; :: thesis: ( 1 <= i & i < k + 1 implies ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) )
assume that
A10: 1 <= i and
A11: i < k + 1 ; :: thesis: ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )
A12: i <= k by A11, NAT_1:13;

now

per cases ( i < k or i = k ) by A12, XXREAL_0:1;

suppose i < k ; :: thesis: ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )

hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) by A4, A7, A10; :: thesis: verum

end;

suppose A13: i = k ; :: thesis: ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )

now

per cases ( k = 1 or 1 < k ) by A10, A13, XXREAL_0:1;

suppose A14: k = 1 ; :: thesis: ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )

A15: ( H₁(0 + 1) is_next_of H₁( 0 ) & H₁(1 + 1) is_next_of H₁(1) ) by A2;
A16: ( ex s0 being strict elementary LTLnode of v st s0 = H₁( 0 ) & ex s2 being strict elementary LTLnode of v st s2 = H₁(2) ) by Th52;
consider s1 being strict elementary LTLnode of v such that
A17: s1 = H₁(1) by Th52;
not G in the LTLold of s1 by A5, A14, A17;
hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) by A1, A13, A14, A17, A16, A15, Lm30; :: thesis: verum

end;

suppose A18: 1 < k ; :: thesis: ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )

set m = k - 1;
reconsider m = k - 1 as Nat by A18, NAT_1:20;
set m1 = m - 1;
1 < m + 1 by A18;
then A19: 1 <= m by NAT_1:13;
then reconsider m1 = m - 1 as Nat by NAT_1:21;
consider sm being strict elementary LTLnode of v such that
A20: sm = H₁(m) by Th52;
A21: m < m + 1 by NAT_1:19;
then m < k + 1 by A6, XXREAL_0:2;
then A22: not G in the LTLold of sm by A5, A19, A20;
A23: ( ex sk1 being strict elementary LTLnode of v st sk1 = H₁(k + 1) & H₁(m + 1) is_next_of H₁(m) ) by A2, Th52;
A24: ( ex sm1 being strict elementary LTLnode of v st sm1 = H₁(m1) & H₁(m1 + 1) is_next_of H₁(m1) ) by A2, Th52;
A25: H₁(m + 1) is_next_of H₁(m) by A2;
A26: H₁(k + 1) is_next_of H₁(k) by A2;
consider sk being strict elementary LTLnode of v such that
A27: sk = H₁(k) by Th52;
A28: not G in the LTLold of sk by A5, A10, A11, A13, A27;
F 'U' G in the LTLold of sm by A4, A7, A19, A20, A21;
then F 'U' G in the LTLold of sk by A20, A27, A22, A24, A25, Lm30;
hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) by A13, A20, A27, A28, A23, A26, Lm30; :: thesis: verum

end;

end;

end;

hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) ; :: thesis: verum

end;

end;

end;

hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) ; :: thesis: verum

end;

hence for i being Nat st 1 <= i & i < k + 1 holds
( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) ; :: thesis: verum

end;

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

end;

A29: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A29, 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