let H be LTL-formula; :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) implies ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) )
set iL = len (the_left_argument_of H);
set iR = len (the_right_argument_of H);
set iR1 = (len (the_right_argument_of H)) + 1;
assume A1: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) ; :: thesis: ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

per cases ( H is conjunctive or H is disjunctive or H is Until or H is Release ) by A1;

suppose H is conjunctive ; :: thesis: ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th6;
then A2: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by Lm2;
1 <= (len (the_right_argument_of H)) + 1 by NAT_1:11;
then A3: len (the_left_argument_of H) < (len (the_left_argument_of H)) + ((len (the_right_argument_of H)) + 1) by NAT_1:19;
1 <= 1 + (len (the_left_argument_of H)) by NAT_1:11;
hence ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) by A2, A3, NAT_1:19; :: thesis: verum

end;

suppose H is disjunctive ; :: thesis: ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

then H = (the_left_argument_of H) 'or' (the_right_argument_of H) by Th7;
then A4: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by Lm2;
1 <= (len (the_right_argument_of H)) + 1 by NAT_1:11;
then A5: len (the_left_argument_of H) < (len (the_left_argument_of H)) + ((len (the_right_argument_of H)) + 1) by NAT_1:19;
1 <= 1 + (len (the_left_argument_of H)) by NAT_1:11;
hence ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) by A4, A5, NAT_1:19; :: thesis: verum

end;

suppose H is Until ; :: thesis: ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

then H = (the_left_argument_of H) 'U' (the_right_argument_of H) by Th8;
then A6: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by Lm2;
1 <= (len (the_right_argument_of H)) + 1 by NAT_1:11;
then A7: len (the_left_argument_of H) < (len (the_left_argument_of H)) + ((len (the_right_argument_of H)) + 1) by NAT_1:19;
1 <= 1 + (len (the_left_argument_of H)) by NAT_1:11;
hence ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) by A6, A7, NAT_1:19; :: thesis: verum

end;

suppose H is Release ; :: thesis: ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

then H = (the_left_argument_of H) 'R' (the_right_argument_of H) by Th9;
then A8: len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) by Lm2;
1 <= (len (the_right_argument_of H)) + 1 by NAT_1:11;
then A9: len (the_left_argument_of H) < (len (the_left_argument_of H)) + ((len (the_right_argument_of H)) + 1) by NAT_1:19;
1 <= 1 + (len (the_left_argument_of H)) by NAT_1:11;
hence ( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) by A8, A9, NAT_1:19; :: thesis: verum

end;

end;