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 ) & ex i being Nat st
( i >= 1 & not ( 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) ) ) holds
ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode (q . j),v) & ( for i being Nat 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) ) ) )
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 ) & ex i being Nat st
( i >= 1 & not ( 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) ) ) implies ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode (q . j),v) & ( for i being Nat 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) ) ) ) )
deffunc H₁( Nat) -> strict LTLnode of v = CastNode (q . $1),v;
assume A1: ( F 'U' G in the LTLold of H₁(1) & ( for i being Nat holds H₁(i + 1) is_next_of H₁(i) ) ) ; :: thesis: ( for i being Nat 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 being Nat st
( j >= 1 & G in the LTLold of (CastNode (q . j),v) & ( for i being Nat 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) ) ) ) )
( ex i being Nat st
( i >= 1 & not ( F 'U' G in the LTLold of H₁(i) & F in the LTLold of H₁(i) & not G in the LTLold of H₁(i) ) ) implies ex j being Nat st
( j >= 1 & G in the LTLold of H₁(j) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of H₁(i) & F in the LTLold of H₁(i) ) ) ) )

proof

assume ex i being Nat st
( i >= 1 & not ( F 'U' G in the LTLold of H₁(i) & F in the LTLold of H₁(i) & not G in the LTLold of H₁(i) ) ) ; :: thesis: ex j being Nat st
( j >= 1 & G in the LTLold of H₁(j) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of H₁(i) & F in the LTLold of H₁(i) ) ) )
then consider k being Nat such that
A2: k >= 1 and
A3: ( not F 'U' G in the LTLold of H₁(k) or not F in the LTLold of H₁(k) or G in the LTLold of H₁(k) ) ;
set k1 = k + 1;
ex m being Nat st
( 1 <= m & m <= k & G in the LTLold of H₁(m) )

proof

now

per cases ( not F 'U' G in the LTLold of H₁(k) or not F in the LTLold of H₁(k) or G in the LTLold of H₁(k) ) by A3;

suppose A4: ( not F 'U' G in the LTLold of H₁(k) or not F in the LTLold of H₁(k) ) ; :: thesis: ex m being Nat st
( 1 <= m & m <= k & G in the LTLold of H₁(m) )

now

assume A5: for m being Nat holds
( not 1 <= m or not m <= k or not G in the LTLold of H₁(m) ) ; :: thesis: contradiction
A6: for m being Nat st 1 <= m & m < k + 1 holds
not G in the LTLold of H₁(m)

proof

let m be Nat; :: thesis: ( 1 <= m & m < k + 1 implies not G in the LTLold of H₁(m) )
assume that
A7: 1 <= m and
A8: m < k + 1 ; :: thesis: not G in the LTLold of H₁(m)
m <= k by A8, NAT_1:13;
hence not G in the LTLold of H₁(m) by A5, A7; :: thesis: verum

end;

k < k + 1 by NAT_1:13;
hence contradiction by A1, A2, A4, A6, Lm32; :: thesis: verum

end;

hence ex m being Nat st
( 1 <= m & m <= k & G in the LTLold of H₁(m) ) ; :: thesis: verum

end;

suppose G in the LTLold of H₁(k) ; :: thesis: ex m being Nat st
( 1 <= m & m <= k & G in the LTLold of H₁(m) )

hence ex m being Nat st
( 1 <= m & m <= k & G in the LTLold of H₁(m) ) by A2; :: thesis: verum

end;

end;

end;

hence ex m being Nat st
( 1 <= m & m <= k & G in the LTLold of H₁(m) ) ; :: thesis: verum

end;

then consider m0 being Nat such that
A9: ( 1 <= m0 & m0 <= k & G in the LTLold of H₁(m0) ) ;
set X = { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } ;
A10: { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } c= Seg k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } or x in Seg k )
assume x in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } ; :: thesis: x in Seg k
then ex m being Element of NAT st
( x = m & 1 <= m & m <= k & G in the LTLold of H₁(m) ) ;
hence x in Seg k by FINSEQ_1:3; :: thesis: verum

end;

reconsider m0 = m0 as Element of NAT by ORDINAL1:def 13;
m0 in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } by A9;
then consider j being Nat such that
1 <= j and
A11: j <= k and
A12: j in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } and
A13: for i being Nat st 1 <= i & i < j holds
not i in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } by A10, Lm31;
for i being Nat st 1 <= i & i < j holds
not G in the LTLold of H₁(i)

proof

let i be Nat; :: thesis: ( 1 <= i & i < j implies not G in the LTLold of H₁(i) )
assume that
A14: 1 <= i and
A15: i < j ; :: thesis: not G in the LTLold of H₁(i)
A16: i < k by A11, A15, XXREAL_0:2;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
not i in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } by A13, A14, A15;
hence not G in the LTLold of H₁(i) by A14, A16; :: thesis: verum

end;

then A17: for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of H₁(i) & F in the LTLold of H₁(i) ) by A1, Lm32;
( j >= 1 & G in the LTLold of H₁(j) )

proof

ex m being Element of NAT st
( j = m & 1 <= m & m <= k & G in the LTLold of H₁(m) ) by A12;
hence ( j >= 1 & G in the LTLold of H₁(j) ) ; :: thesis: verum

end;

hence ex j being Nat st
( j >= 1 & G in the LTLold of H₁(j) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of H₁(i) & F in the LTLold of H₁(i) ) ) ) by A17; :: thesis: verum

end;

hence ( for i being Nat 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 being Nat st
( j >= 1 & G in the LTLold of (CastNode (q . j),v) & ( for i being Nat 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) ) ) ) ) ; :: thesis: verum