let v be LTL-formula; :: thesis: for N2, N1 being strict LTLnode of v st N2 is_succ2_of N1 holds
len the LTLnew of N2 <= (len the LTLnew of N1) - 1
let N2, N1 be strict LTLnode of v; :: thesis: ( N2 is_succ2_of N1 implies len the LTLnew of N2 <= (len the LTLnew of N1) - 1 )
set NN1 = the LTLnew of N1;
set NN2 = the LTLnew of N2;
assume N2 is_succ2_of N1 ; :: thesis: len the LTLnew of N2 <= (len the LTLnew of N1) - 1
then consider H being LTL-formula such that
A1: H in the LTLnew of N1 and
A101: ( H is disjunctive or H is Until or H is Release ) and
A2: N2 = SuccNode2 H,N1 by Def209;
set New2 = LTLNew2 H,v;
set M1 = the LTLnew of N1 \ {H};
set M2 = (LTLNew2 H,v) \ the LTLold of N1;
reconsider NN1 = the LTLnew of N1 as Subset of (Subformulae v) ;
reconsider M1 = the LTLnew of N1 \ {H} as Subset of (Subformulae v) ;
reconsider M2 = (LTLNew2 H,v) \ the LTLold of N1 as Subset of (Subformulae v) ;
LTLNew2 H,v = LTLNew2 H by A1, defLTLNew201;
then A3: the LTLnew of N2 = M1 \/ M2 by A1, A101, A2, Def207;
A4: len M1 = (len NN1) - (len H) by A1, Thlen07;
A5: len (LTLNew2 H,v) <= (len H) - 1 by A1, lemlen06;
len M2 <= len (LTLNew2 H,v) by Thlen12, XBOOLE_1:36;
then len M2 <= (len H) - 1 by A5, XXREAL_0:2;
then A6: (len M1) + (len M2) <= (len M1) + ((len H) - 1) by XREAL_1:8;
len the LTLnew of N2 <= (len M1) + (len M2) by A3, Thlen13;
hence len the LTLnew of N2 <= (len the LTLnew of N1) - 1 by A6, A4, XXREAL_0:2; :: thesis: verum