finite_modular_dyson_strict_sizes

forall b c d e ub uc vb vc p t h r K L l. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((K)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((K)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (uc))) /\ exists ff_q_fms_count_summand. (ub) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (uc)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (uc))) /\ exists ff_q_fms_count_decoded. (ub) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (uc)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((L)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((L)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (vc))) /\ exists ff_q_fms_count_summand. (vb) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (vc)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (vc))) /\ exists ff_q_fms_count_decoded. (vb) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (vc)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((l)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((l)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (((forall cd_output_dyson_upper. (exists fms_gap_cd_dyson_upper_bound. fms_gap_cd_dyson_upper_bound + S (cd_output_dyson_upper) = (p)) -> ((((((exists fs_h_cd_dyson_upper_result. fs_h_cd_dyson_upper_result + S (1) = S ((S (cd_output_dyson_upper)) * uc)) /\ exists fs_q_cd_dyson_upper_result. ub = fs_q_cd_dyson_upper_result * S ((S (cd_output_dyson_upper)) * uc) + (1))) -> ((((exists fs_h_cd_dyson_upper_old. fs_h_cd_dyson_upper_old + S (1) = S ((S (cd_output_dyson_upper)) * c)) /\ exists fs_q_cd_dyson_upper_old. b = fs_q_cd_dyson_upper_old * S ((S (cd_output_dyson_upper)) * c) + (1))) \/ (exists cd_source_dyson_upper. (((exists fms_gap_cd_dyson_upper_member. fms_gap_cd_dyson_upper_member + S (cd_source_dyson_upper) = (p)) /\ (((exists fs_h_fms_cd_dyson_upper_member. fs_h_fms_cd_dyson_upper_member + S (1) = S ((S (cd_source_dyson_upper)) * e)) /\ exists fs_q_fms_cd_dyson_upper_member. d = fs_q_fms_cd_dyson_upper_member * S ((S (cd_source_dyson_upper)) * e) + (1))))) /\ (exists fms_u_cd_dyson_upper_mod fms_v_cd_dyson_upper_mod. (cd_source_dyson_upper+t) + (p) * fms_u_cd_dyson_upper_mod = (cd_output_dyson_upper) + (p) * fms_v_cd_dyson_upper_mod)))) /\ (((((exists fs_h_cd_dyson_upper_old. fs_h_cd_dyson_upper_old + S (1) = S ((S (cd_output_dyson_upper)) * c)) /\ exists fs_q_cd_dyson_upper_old. b = fs_q_cd_dyson_upper_old * S ((S (cd_output_dyson_upper)) * c) + (1))) \/ (exists cd_source_dyson_upper. (((exists fms_gap_cd_dyson_upper_member. fms_gap_cd_dyson_upper_member + S (cd_source_dyson_upper) = (p)) /\ (((exists fs_h_fms_cd_dyson_upper_member. fs_h_fms_cd_dyson_upper_member + S (1) = S ((S (cd_source_dyson_upper)) * e)) /\ exists fs_q_fms_cd_dyson_upper_member. d = fs_q_fms_cd_dyson_upper_member * S ((S (cd_source_dyson_upper)) * e) + (1))))) /\ (exists fms_u_cd_dyson_upper_mod fms_v_cd_dyson_upper_mod. (cd_source_dyson_upper+t) + (p) * fms_u_cd_dyson_upper_mod = (cd_output_dyson_upper) + (p) * fms_v_cd_dyson_upper_mod))) -> (((exists fs_h_cd_dyson_upper_result. fs_h_cd_dyson_upper_result + S (1) = S ((S (cd_output_dyson_upper)) * uc)) /\ exists fs_q_cd_dyson_upper_result. ub = fs_q_cd_dyson_upper_result * S ((S (cd_output_dyson_upper)) * uc) + (1))))))) /\ (forall cd_output_dyson_lower. (exists fms_gap_cd_dyson_lower_bound. fms_gap_cd_dyson_lower_bound + S (cd_output_dyson_lower) = (p)) -> ((((((exists fs_h_cd_dyson_lower_result. fs_h_cd_dyson_lower_result + S (1) = S ((S (cd_output_dyson_lower)) * vc)) /\ exists fs_q_cd_dyson_lower_result. vb = fs_q_cd_dyson_lower_result * S ((S (cd_output_dyson_lower)) * vc) + (1))) -> ((((exists fs_h_cd_dyson_lower_old. fs_h_cd_dyson_lower_old + S (1) = S ((S (cd_output_dyson_lower)) * e)) /\ exists fs_q_cd_dyson_lower_old. d = fs_q_cd_dyson_lower_old * S ((S (cd_output_dyson_lower)) * e) + (1))) /\ (exists cd_source_dyson_lower. (((exists fms_gap_cd_dyson_lower_member. fms_gap_cd_dyson_lower_member + S (cd_source_dyson_lower) = (p)) /\ (((exists fs_h_fms_cd_dyson_lower_member. fs_h_fms_cd_dyson_lower_member + S (1) = S ((S (cd_source_dyson_lower)) * c)) /\ exists fs_q_fms_cd_dyson_lower_member. b = fs_q_fms_cd_dyson_lower_member * S ((S (cd_source_dyson_lower)) * c) + (1))))) /\ (exists fms_u_cd_dyson_lower_mod fms_v_cd_dyson_lower_mod. (cd_output_dyson_lower+t) + (p) * fms_u_cd_dyson_lower_mod = (cd_source_dyson_lower) + (p) * fms_v_cd_dyson_lower_mod)))) /\ (((((exists fs_h_cd_dyson_lower_old. fs_h_cd_dyson_lower_old + S (1) = S ((S (cd_output_dyson_lower)) * e)) /\ exists fs_q_cd_dyson_lower_old. d = fs_q_cd_dyson_lower_old * S ((S (cd_output_dyson_lower)) * e) + (1))) /\ (exists cd_source_dyson_lower. (((exists fms_gap_cd_dyson_lower_member. fms_gap_cd_dyson_lower_member + S (cd_source_dyson_lower) = (p)) /\ (((exists fs_h_fms_cd_dyson_lower_member. fs_h_fms_cd_dyson_lower_member + S (1) = S ((S (cd_source_dyson_lower)) * c)) /\ exists fs_q_fms_cd_dyson_lower_member. b = fs_q_fms_cd_dyson_lower_member * S ((S (cd_source_dyson_lower)) * c) + (1))))) /\ (exists fms_u_cd_dyson_lower_mod fms_v_cd_dyson_lower_mod. (cd_output_dyson_lower+t) + (p) * fms_u_cd_dyson_lower_mod = (cd_source_dyson_lower) + (p) * fms_v_cd_dyson_lower_mod))) -> (((exists fs_h_cd_dyson_lower_result. fs_h_cd_dyson_lower_result + S (1) = S ((S (cd_output_dyson_lower)) * vc)) /\ exists fs_q_cd_dyson_lower_result. vb = fs_q_cd_dyson_lower_result * S ((S (cd_output_dyson_lower)) * vc) + (1))))))))) -> (((exists fms_gap_member. fms_gap_member + S (0) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (0)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (0)) * e) + (1))))) -> (((exists fms_gap_member. fms_gap_member + S (h) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (h)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (h)) * e) + (1))))) -> ((((exists fms_gap_cd_boundary_source. fms_gap_cd_boundary_source + S (t) = (p)) /\ (((exists fs_h_fms_cd_boundary_source. fs_h_fms_cd_boundary_source + S (1) = S ((S (t)) * c)) /\ exists fs_q_fms_cd_boundary_source. b = fs_q_fms_cd_boundary_source * S ((S (t)) * c) + (1))))) /\ ((exists fms_gap_cd_boundary_target. fms_gap_cd_boundary_target + S (r) = (p)) /\ ((exists fms_u_cd_boundary_shift fms_v_cd_boundary_shift. (t+h) + (p) * fms_u_cd_boundary_shift = (r) + (p) * fms_v_cd_boundary_shift) /\ ~(((exists fs_h_cd_boundary_outside. fs_h_cd_boundary_outside + S (1) = S ((S (r)) * c)) /\ exists fs_q_cd_boundary_outside. b = fs_q_cd_boundary_outside * S ((S (r)) * c) + (1)))))) -> ~(K=0) /\ (~(L=0) /\ (exists fms_gap_lt. fms_gap_lt + S (L) = (l)))