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 A1: ( F 'U' G in the LTLold of H₁(1) & ( 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) ) );
A2: S₁[ 0 ] ;
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 B1: 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 C1: 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) )
C2: k <= k + 1 by NAT_1:11;
C3: 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 D1: ( 1 <= i & i < k ) ; :: thesis: not G in the LTLold of H₁(i)
( 1 <= i & i < k + 1 ) by D1, C2, XXREAL_0:2;
hence not G in the LTLold of H₁(i) by C1; :: 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 D1: ( 1 <= i & i < k + 1 ) ; :: thesis: ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) )
D101: i <= k by D1, NAT_1:13;

now

per cases ( i < k or i = k ) by D101, 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 D1, C3, B1; :: thesis: verum

end;

suppose D2: 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 D1, D2, XXREAL_0:1;

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

consider s0 being strict elementary LTLnode of v such that
E100: s0 = H₁( 0 ) by ThLTLStates04;
consider s1 being strict elementary LTLnode of v such that
E101: s1 = H₁(1) by ThLTLStates04;
consider s2 being strict elementary LTLnode of v such that
E102: s2 = H₁(2) by ThLTLStates04;
E104: ( H₁(0 + 1) is_next_of H₁( 0 ) & H₁(1 + 1) is_next_of H₁(1) ) by A1;
not G in the LTLold of s1 by C1, E1, E101;
hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) by lemUntil01, A1, E104, E100, E101, E102, D2, E1; :: thesis: verum

end;

suppose E2: 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 E2, NAT_1:20;
1 < m + 1 by E2;
then E201: 1 <= m by NAT_1:13;
set m1 = m - 1;
reconsider m1 = m - 1 as Nat by E201, NAT_1:21;
consider sm1 being strict elementary LTLnode of v such that
Esm1: sm1 = H₁(m1) by ThLTLStates04;
consider sm being strict elementary LTLnode of v such that
Esm: sm = H₁(m) by ThLTLStates04;
consider sk being strict elementary LTLnode of v such that
Esk: sk = H₁(k) by ThLTLStates04;
consider sk1 being strict elementary LTLnode of v such that
Esk1: sk1 = H₁(k + 1) by ThLTLStates04;
E202: m < m + 1 by NAT_1:19;
then E203: ( F in the LTLold of sm & F 'U' G in the LTLold of sm ) by E201, C3, B1, Esm;
m < k + 1 by E202, C2, XXREAL_0:2;
then E204: not G in the LTLold of sm by E201, C1, Esm;
( H₁(m1 + 1) is_next_of H₁(m1) & H₁(m + 1) is_next_of H₁(m) ) by A1;
then E205: F 'U' G in the LTLold of sk by Esm1, Esm, Esk, lemUntil01, E203, E204;
E207: not G in the LTLold of sk by D1, D2, C1, Esk;
( H₁(m + 1) is_next_of H₁(m) & H₁(k + 1) is_next_of H₁(k) ) by A1;
hence ( F in the LTLold of H₁(i) & F 'U' G in the LTLold of H₁(i) ) by Esm, Esk, Esk1, lemUntil01, E205, E207, D2; :: 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;

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