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 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: ( 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
B1: k >= 1 and
B2: ( 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;
B3: 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 B2;

suppose C1: ( 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 C100: for m being Nat holds
( not 1 <= m or not m <= k or not G in the LTLold of H₁(m) ) ; :: thesis: contradiction
C2: 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 D1: ( 1 <= m & m < k + 1 ) ; :: thesis: not G in the LTLold of H₁(m)
( 1 <= m & m <= k ) by D1, NAT_1:13;
hence not G in the LTLold of H₁(m) by C100; :: thesis: verum

end;

( 1 <= k & k < k + 1 ) by B1, NAT_1:13;
hence contradiction by C2, A1, A2, lemUntil02, C1; :: 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 B1; :: 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;

set X = { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } ;
consider m0 being Nat such that
B400: ( 1 <= m0 & m0 <= k & G in the LTLold of H₁(m0) ) by B3;
reconsider m0 = m0 as Element of NAT by ORDINAL1:def 13;
B4: m0 in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } by B400;
B5: { 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 consider m being Element of NAT such that
C1: ( x = m & 1 <= m & m <= k & G in the LTLold of H₁(m) ) ;
thus x in Seg k by C1, FINSEQ_1:3; :: thesis: verum

end;

consider j being Nat such that
B6: ( 1 <= j & j <= k ) and
B7: j in { m where m is Element of NAT : ( 1 <= m & m <= k & G in the LTLold of H₁(m) ) } and
B8: 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 B4, B5, lemExistMin;
B9: ( j >= 1 & G in the LTLold of H₁(j) )

proof

consider m being Element of NAT such that
C1: ( j = m & 1 <= m & m <= k & G in the LTLold of H₁(m) ) by B7;
thus ( j >= 1 & G in the LTLold of H₁(j) ) by C1; :: thesis: verum

end;

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 C1: ( 1 <= i & i < j ) ; :: thesis: not G in the LTLold of H₁(i)
C2: ( 1 <= i & i < k ) by B6, C1, 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 C1, B8;
hence not G in the LTLold of H₁(i) by C2; :: thesis: verum

end;

then 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, A2, lemUntil02;
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 B9; :: 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