let v be LTL-formula; :: thesis: for N2, N1 being strict LTLnode of v st N2 is_succ1_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_succ1_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_succ1_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
A2: N2 = SuccNode1 H,N1 by Def208;
set New1 = LTLNew1 H,v;
set M1 = the LTLnew of N1 \ {H};
set M2 = (LTLNew1 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 = (LTLNew1 H,v) \ the LTLold of N1 as Subset of (Subformulae v) ;
LTLNew1 H,v = LTLNew1 H by A1, defLTLNew101;
then A3: the LTLnew of N2 = M1 \/ M2 by A1, A2, Def206;
A4: len M1 = (len NN1) - (len H) by A1, Thlen07;
A5: len (LTLNew1 H,v) <= (len H) - 1 by A1, lemlen05;
len M2 <= len (LTLNew1 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