let H, v be LTL-formula; :: thesis: for s1, s0 being strict elementary LTLnode of v st s1 is_next_of s0 & H in the LTLold of s1 holds
( ( 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 ) )
let s1, s0 be strict elementary LTLnode of v; :: thesis: ( s1 is_next_of s0 & H in the LTLold of s1 implies ( ( 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 ) ) )
assume that
A1: s1 is_next_of s0 and
A2: H in the LTLold of s1 ; :: thesis: ( ( 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 ) )
consider L being FinSequence such that
A3: ( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s0 & L . (len L) = s1 ) by Def215, A1;
set n = len L;
A4: CastNode (L . (len L)),v = s1 by defCastNode01, A3;
then A5: the LTLnew of (CastNode (L . (len L)),v) = {} v by Defelementary;
a6: CastNode (L . 1),v = 'X' s0 by defCastNode01, A3;
1 < len L by A3, A2, XXREAL_0:1;
then consider m being Nat such that
A7: ( 1 <= m & m < len L ) and
A8: not H in the LTLold of (CastNode (L . m),v) and
A9: H in the LTLold of (CastNode (L . (m + 1)),v) by ThSucc03, A3, a6, A2, A4;
consider N1, N2 being strict LTLnode of v such that
A10: ( N1 = L . m & N2 = L . (m + 1) & N2 is_succ_of N1 ) by A3, A7, DefFinseq;
A11: CastNode (L . m),v = N1 by defCastNode01, A10;
A12: CastNode (L . (m + 1)),v = N2 by defCastNode01, A10;
A13: N2 is_succ_of N1,H by A8, A9, A11, A12, A10, ThSucc04;
A14: the LTLold of N1 c= the LTLold of s1 by A3, A7, ThSucc07, A4, A11;
set m1 = m + 1;
A15: ( len L <= len L & m + 1 <= len L & 1 <= m + 1 ) by A7, NAT_1:13;
then A16: the LTLnew of N2 c= the LTLold of s1 by A3, A5, ThSucc10, A4, A12;
A17: the LTLnext of N2 c= the LTLnext of s1 by A3, ThSucc07, A15, A4, A12;
A18: ( 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

assume B1: H is conjunctive ; :: thesis: ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 )
set F = the_left_argument_of H;
set G = the_right_argument_of H;
B2: LTLNew1 H = {(the_left_argument_of H),(the_right_argument_of H)} by B1, Def203;

now

per cases ( ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) or ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ) by A13, DefSucc01;

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

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

proof

now

per cases ( the_left_argument_of H in the LTLold of N1 or not the_left_argument_of H in the LTLold of N1 ) ;

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

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

end;

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

the_left_argument_of H in LTLNew1 H by B2, TARSKI:def 2;
then the_left_argument_of H in (LTLNew1 H) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then the_left_argument_of H in the LTLnew of N2 by C1;
hence the_left_argument_of H in the LTLold of s1 by A16; :: thesis: verum

end;

end;

end;

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

end;

the_right_argument_of H in the LTLold of s1

proof

now

per cases ( the_right_argument_of H in the LTLold of N1 or not the_right_argument_of H in the LTLold of N1 ) ;

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

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

end;

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

the_right_argument_of H in LTLNew1 H by B2, TARSKI:def 2;
then the_right_argument_of H in (LTLNew1 H) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by C1;
hence the_right_argument_of H in the LTLold of s1 by A16; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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

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

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: verum

end;

A19: ( ( 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

assume B1: ( H is disjunctive or H is Until ) ; :: thesis: ( the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 )
set F = the_left_argument_of H;
set G = the_right_argument_of H;
B2: LTLNew1 H = {(the_left_argument_of H)} by B1, Def203;
B3: LTLNew2 H = {(the_right_argument_of H)} by B1, Def204;

now

per cases ( ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) or ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ) by A13, DefSucc01;

suppose ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) ; :: thesis: ( the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 )

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew1 H) \ the LTLold of N1) by Def206;
then C1: (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 ( the_left_argument_of H in the LTLold of N1 or not the_left_argument_of H in the LTLold of N1 ) ;

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

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

end;

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

the_left_argument_of H in LTLNew1 H by B2, TARSKI:def 1;
then the_left_argument_of H in (LTLNew1 H) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then the_left_argument_of H in the LTLnew of N2 by C1;
hence the_left_argument_of H in the LTLold of s1 by A16; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew2 H) \ the LTLold of N1) by Def207;
then C1: (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 ( the_right_argument_of H in the LTLold of N1 or not the_right_argument_of H in the LTLold of N1 ) ;

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

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

end;

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

the_right_argument_of H in LTLNew2 H by B3, TARSKI:def 1;
then the_right_argument_of H in (LTLNew2 H) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by C1;
hence the_right_argument_of H in the LTLold of s1 by A16; :: thesis: verum

end;

end;

end;

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

end;

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

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: verum

end;

A20: ( H is next implies the_argument_of H in the LTLnext of s1 )

proof

assume B1: H is next ; :: thesis: the_argument_of H in the LTLnext of s1
set F = the_argument_of H;
B4: LTLNext H = {(the_argument_of H)} by B1, Def205;

now

per cases ( ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) or ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ) by A13, DefSucc01;

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

then the LTLnext of N2 = the LTLnext of N1 \/ (LTLNext H) by Def206;
then LTLNext H c= the LTLnext of N2 by XBOOLE_1:7;
then C1: LTLNext H c= the LTLnext of s1 by A17, XBOOLE_1:1;
the_argument_of H in LTLNext H by B4, TARSKI:def 1;
hence the_argument_of H in the LTLnext of s1 by C1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

proof

assume B1: H is Release ; :: thesis: the_right_argument_of H in the LTLold of s1
set F = the_left_argument_of H;
set G = the_right_argument_of H;
B2: LTLNew1 H = {(the_right_argument_of H)} by B1, Def203;
B3: LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} by B1, Def204;

now

per cases ( ( H in the LTLnew of N1 & N2 = SuccNode1 H,N1 ) or ( H in the LTLnew of N1 & ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 H,N1 ) ) by A13, DefSucc01;

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

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew1 H) \ the LTLold of N1) by Def206;
then C1: (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 ( the_right_argument_of H in the LTLold of N1 or not the_right_argument_of H in the LTLold of N1 ) ;

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

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

end;

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

the_right_argument_of H in LTLNew1 H by B2, TARSKI:def 1;
then the_right_argument_of H in (LTLNew1 H) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by C1;
hence the_right_argument_of H in the LTLold of s1 by A16; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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

then the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ((LTLNew2 H) \ the LTLold of N1) by Def207;
then C1: (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 ( the_right_argument_of H in the LTLold of N1 or not the_right_argument_of H in the LTLold of N1 ) ;

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

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

end;

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

the_right_argument_of H in LTLNew2 H by B3, TARSKI:def 2;
then the_right_argument_of H in (LTLNew2 H) \ the LTLold of N1 by D1, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by C1;
hence the_right_argument_of H in the LTLold of s1 by A16; :: thesis: verum

end;

end;

end;

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

end;

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

end;

end;

end;

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

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 A18, A19, A20; :: thesis: verum