let H, v be LTL-formula; :: thesis:
let s1, s0 be strict elementary LTLnode of v; :: thesis:
assume that
A1: s1 is_next_of s0 and
A2: H in the LTLold of s1 ; :: thesis:
consider L being FinSequence such that
A3: 1 <= len L and
A4: L is_Finseq_for v and
A5: L . 1 = 'X' s0 and
A6: L . (len L) = s1 by A1, Def20;
A7: CastNode (L . 1),v = 'X' s0 by A5, Def16;
set n = len L;
A8: CastNode (L . (len L)),v = s1 by A6, Def16;
1 < len L by A2, A3, A5, A6, XXREAL_0:1;
then consider m being Nat such that
A9: ( 1 <= m & m < len L ) and
A10: ( not H in the LTLold of (CastNode (L . m),v) & H in the LTLold of (CastNode (L . (m + 1)),v) ) by A2, A4, A8, A7, Th27;
consider N1, N2 being strict LTLnode of v such that
A11: N1 = L . m and
A12: N2 = L . (m + 1) and
A13: N2 is_succ_of N1 by A4, A9, Def19;
A14: CastNode (L . m),v = N1 by A11, Def16;
then A15: the LTLold of N1 c= the LTLold of s1 by A4, A8, A9, Th31;
set m1 = m + 1;
A16: ( m + 1 <= len L & 1 <= m + 1 ) by A9, NAT_1:13;
A17: CastNode (L . (m + 1)),v = N2 by A12, Def16;
then A18: N2 is_succ_of N1,H by A10, A13, A14, Th28;
the LTLnew of (CastNode (L . (len L)),v) = {} v by A8, Def11;
then A19: the LTLnew of N2 c= the LTLold of s1 by A4, A8, A17, A16, Th34;
A20: ( H is conjunctive implies ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) )

proof

set G = the_right_argument_of H;
set F = the_left_argument_of H;
assume A21: H is conjunctive ; :: thesis:
then A22: LTLNew1 H = {(the_left_argument_of H),(the_right_argument_of H)} by Def1;

now

per cases by A18, Def6;

suppose ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) ; :: thesis:

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew1 H) \ the LTLold of N1) by Def4;
then A23: (LTLNew1 H) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
A24: the_right_argument_of H in the LTLold of s1

proof

now

per cases ;

suppose the_right_argument_of H in the LTLold of N1 ; :: thesis:

hence the_right_argument_of H in the LTLold of s1 by A15; :: thesis:

end;

suppose A25: not the_right_argument_of H in the LTLold of N1 ; :: thesis:

the_right_argument_of H in LTLNew1 H by A22, TARSKI:def 2;
then the_right_argument_of H in (LTLNew1 H) \ the LTLold of N1 by A25, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by A23;
hence the_right_argument_of H in the LTLold of s1 by A19; :: thesis:

end;

end;

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

the_left_argument_of H in the LTLold of s1

proof

now

per cases ;

suppose the_left_argument_of H in the LTLold of N1 ; :: thesis:

hence the_left_argument_of H in the LTLold of s1 by A15; :: thesis:

end;

suppose A26: not the_left_argument_of H in the LTLold of N1 ; :: thesis:

the_left_argument_of H in LTLNew1 H by A22, TARSKI:def 2;
then the_left_argument_of H in (LTLNew1 H) \ the LTLold of N1 by A26, XBOOLE_0:def 5;
then the_left_argument_of H in the LTLnew of N2 by A23;
hence the_left_argument_of H in the LTLold of s1 by A19; :: thesis:

end;

end;

end;

hence the_left_argument_of H in the LTLold of s1 ; :: thesis:

end;

hence ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) by A24; :: thesis:

end;

suppose ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ; :: thesis:

hence ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) by A21, MODELC_2:78; :: thesis:

end;

end;

end;

hence ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) ; :: thesis:

end;

A27: ( H is Release implies the_right_argument_of H in the LTLold of s1 )

proof

set G = the_right_argument_of H;
set F = the_left_argument_of H;
assume A28: H is Release ; :: thesis:
then A29: LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} by Def2;
A30: LTLNew1 H = {(the_right_argument_of H)} by A28, Def1;

now

per cases by A18, Def6;

suppose ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) ; :: thesis:

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew1 H) \ the LTLold of N1) by Def4;
then A31: (LTLNew1 H) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
the_right_argument_of H in the LTLold of s1

proof

now

per cases ;

suppose the_right_argument_of H in the LTLold of N1 ; :: thesis:

hence the_right_argument_of H in the LTLold of s1 by A15; :: thesis:

end;

suppose A32: not the_right_argument_of H in the LTLold of N1 ; :: thesis:

the_right_argument_of H in LTLNew1 H by A30, TARSKI:def 1;
then the_right_argument_of H in (LTLNew1 H) \ the LTLold of N1 by A32, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by A31;
hence the_right_argument_of H in the LTLold of s1 by A19; :: thesis:

end;

end;

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

suppose ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ; :: thesis:

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew2 H) \ the LTLold of N1) by Def5;
then A33: (LTLNew2 H) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
the_right_argument_of H in the LTLold of s1

proof

now

per cases ;

suppose the_right_argument_of H in the LTLold of N1 ; :: thesis:

hence the_right_argument_of H in the LTLold of s1 by A15; :: thesis:

end;

suppose A34: not the_right_argument_of H in the LTLold of N1 ; :: thesis:

the_right_argument_of H in LTLNew2 H by A29, TARSKI:def 2;
then the_right_argument_of H in (LTLNew2 H) \ the LTLold of N1 by A34, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by A33;
hence the_right_argument_of H in the LTLold of s1 by A19; :: thesis:

end;

end;

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

end;

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

A35: ( ( not H is disjunctive & not H is Until ) or the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 )

proof

set G = the_right_argument_of H;
set F = the_left_argument_of H;
assume A36: ( H is disjunctive or H is Until ) ; :: thesis:
then A37: LTLNew2 H = {(the_right_argument_of H)} by Def2;
A38: LTLNew1 H = {(the_left_argument_of H)} by A36, Def1;

now

per cases by A18, Def6;

suppose ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) ; :: thesis:

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew1 H) \ the LTLold of N1) by Def4;
then A39: (LTLNew1 H) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
the_left_argument_of H in the LTLold of s1

proof

now

per cases ;

suppose the_left_argument_of H in the LTLold of N1 ; :: thesis:

hence the_left_argument_of H in the LTLold of s1 by A15; :: thesis:

end;

suppose A40: not the_left_argument_of H in the LTLold of N1 ; :: thesis:

the_left_argument_of H in LTLNew1 H by A38, TARSKI:def 1;
then the_left_argument_of H in (LTLNew1 H) \ the LTLold of N1 by A40, XBOOLE_0:def 5;
then the_left_argument_of H in the LTLnew of N2 by A39;
hence the_left_argument_of H in the LTLold of s1 by A19; :: thesis:

end;

end;

end;

hence the_left_argument_of H in the LTLold of s1 ; :: thesis:

end;

hence ( the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) ; :: thesis:

end;

suppose ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ; :: thesis:

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew2 H) \ the LTLold of N1) by Def5;
then A41: (LTLNew2 H) \ the LTLold of N1 c= the LTLnew of N2 by XBOOLE_1:7;
the_right_argument_of H in the LTLold of s1

proof

now

per cases ;

suppose the_right_argument_of H in the LTLold of N1 ; :: thesis:

hence the_right_argument_of H in the LTLold of s1 by A15; :: thesis:

end;

suppose A42: not the_right_argument_of H in the LTLold of N1 ; :: thesis:

the_right_argument_of H in LTLNew2 H by A37, TARSKI:def 1;
then the_right_argument_of H in (LTLNew2 H) \ the LTLold of N1 by A42, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by A41;
hence the_right_argument_of H in the LTLold of s1 by A19; :: thesis:

end;

end;

end;

hence the_right_argument_of H in the LTLold of s1 ; :: thesis:

end;

hence ( the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) ; :: thesis:

end;

end;

end;

hence ( the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) ; :: thesis:

end;

A43: the LTLnext of N2 c= the LTLnext of s1 by A4, A8, A17, A16, Th31;
( H is next implies the_argument_of H in the LTLnext of s1 )

proof

set F = the_argument_of H;
assume A44: H is next ; :: thesis:
then A45: LTLNext H = {(the_argument_of H)} by Def3;

now

per cases by A18, Def6;

suppose ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) ; :: thesis:

then the LTLnext of N2 = the LTLnext of N1 \/ (LTLNext H) by Def4;
then LTLNext H c= the LTLnext of N2 by XBOOLE_1:7;
then A46: LTLNext H c= the LTLnext of s1 by A43, XBOOLE_1:1;
the_argument_of H in LTLNext H by A45, TARSKI:def 1;
hence the_argument_of H in the LTLnext of s1 by A46; :: thesis:

end;

suppose ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ; :: thesis:

hence the_argument_of H in the LTLnext of s1 by A44, MODELC_2:78; :: thesis:

end;

end;

end;

hence the_argument_of H in the LTLnext of s1 ; :: thesis:

end;

hence ( ( H is conjunctive implies ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) ) & ( ( not H is disjunctive & not H is Until ) or the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) & ( H is next implies the_argument_of H in the LTLnext of s1 ) & ( H is Release implies the_right_argument_of H in the LTLold of s1 ) ) by A20, A35, A27; :: thesis: