let H be CTL-formula; :: thesis: ( ( H is conjunctive or H is ExistUntill ) implies ( 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 ExistUntill ) ; :: thesis: ( len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )
per cases ( H is conjunctive or H is ExistUntill ) by A1;
suppose H is conjunctive ; :: thesis: ( 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 Lm20;
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 (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 ExistUntill ; :: thesis: ( len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )
then H = (the_left_argument_of H) EU (the_right_argument_of H) by Lm21;
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 (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H ) by A4, A5, NAT_1:19; :: thesis: verum
end;
end;