let v be LTL-formula; :: thesis: for N1, N2 being strict LTLnode over v st N2 is_succ2_of N1 holds
len the LTLnew of N2 <= (len the LTLnew of N1) - 1
let N1, N2 be strict LTLnode over 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
( H is disjunctive or H is Until or H is Release ) and
A2: N2 = SuccNode2 (H,N1) ;
set M1 = the LTLnew of N1 \ {H};
set New2 = LTLNew2 (H,v);
set M2 = (LTLNew2 (H,v)) \ the LTLold of N1;
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, Def28;
then the LTLnew of N2 = M1 \/ M2 by A1, A2, Def5;
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 (LTLNew2 (H,v)) by Th15, XBOOLE_1:36;
len (LTLNew2 (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:6;
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