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 Def7;
set M1 = the LTLnew of N1 \ {H};
set New1 = LTLNew1 H,v;
set M2 = (LTLNew1 H,v) \ the LTLold of N1;
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, Def27;
then the LTLnew of N2 = M1 \/ M2 by A1, A2, Def4;
then A3: len the LTLnew of N2 <= (len M1) + (len M2) by Th18;
reconsider NN1 = the LTLnew of N1 as Subset of (Subformulae v) ;
A4: len M2 <= len (LTLNew1 H,v) by Th15, XBOOLE_1:36;
len (LTLNew1 H,v) <= (len H) - 1 by A1, Lm28;
then len M2 <= (len H) - 1 by A4, XXREAL_0:2;
then A5: (len M1) + (len M2) <= (len M1) + ((len H) - 1) by XREAL_1:8;
len M1 = (len NN1) - (len H) by A1, Th10;
hence len the LTLnew of N2 <= (len the LTLnew of N1) - 1 by A5, A3, XXREAL_0:2; :: thesis: verum