len (GEN (w,q)) = (len w) + 1 by FSM_1:def 2;
hence not GEN (w,q) is empty ; :: thesis: verum