finite_modular_dyson_lower_boundary_nonmember

forall b c d e u v p t h r. (forall cd_output_lower. (exists fms_gap_cd_lower_bound. fms_gap_cd_lower_bound + S (cd_output_lower) = (p)) -> ((((((exists fs_h_cd_lower_result. fs_h_cd_lower_result + S (1) = S ((S (cd_output_lower)) * v)) /\ exists fs_q_cd_lower_result. u = fs_q_cd_lower_result * S ((S (cd_output_lower)) * v) + (1))) -> ((((exists fs_h_cd_lower_old. fs_h_cd_lower_old + S (1) = S ((S (cd_output_lower)) * e)) /\ exists fs_q_cd_lower_old. d = fs_q_cd_lower_old * S ((S (cd_output_lower)) * e) + (1))) /\ (exists cd_source_lower. (((exists fms_gap_cd_lower_member. fms_gap_cd_lower_member + S (cd_source_lower) = (p)) /\ (((exists fs_h_fms_cd_lower_member. fs_h_fms_cd_lower_member + S (1) = S ((S (cd_source_lower)) * c)) /\ exists fs_q_fms_cd_lower_member. b = fs_q_fms_cd_lower_member * S ((S (cd_source_lower)) * c) + (1))))) /\ (exists fms_u_cd_lower_mod fms_v_cd_lower_mod. (cd_output_lower+t) + (p) * fms_u_cd_lower_mod = (cd_source_lower) + (p) * fms_v_cd_lower_mod)))) /\ (((((exists fs_h_cd_lower_old. fs_h_cd_lower_old + S (1) = S ((S (cd_output_lower)) * e)) /\ exists fs_q_cd_lower_old. d = fs_q_cd_lower_old * S ((S (cd_output_lower)) * e) + (1))) /\ (exists cd_source_lower. (((exists fms_gap_cd_lower_member. fms_gap_cd_lower_member + S (cd_source_lower) = (p)) /\ (((exists fs_h_fms_cd_lower_member. fs_h_fms_cd_lower_member + S (1) = S ((S (cd_source_lower)) * c)) /\ exists fs_q_fms_cd_lower_member. b = fs_q_fms_cd_lower_member * S ((S (cd_source_lower)) * c) + (1))))) /\ (exists fms_u_cd_lower_mod fms_v_cd_lower_mod. (cd_output_lower+t) + (p) * fms_u_cd_lower_mod = (cd_source_lower) + (p) * fms_v_cd_lower_mod))) -> (((exists fs_h_cd_lower_result. fs_h_cd_lower_result + S (1) = S ((S (cd_output_lower)) * v)) /\ exists fs_q_cd_lower_result. u = fs_q_cd_lower_result * S ((S (cd_output_lower)) * v) + (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)))))) -> (exists fms_gap_lt. fms_gap_lt + S (h) = (p)) -> ~(((exists fs_h_cd_boundary_missing. fs_h_cd_boundary_missing + S (1) = S ((S (h)) * v)) /\ exists fs_q_cd_boundary_missing. u = fs_q_cd_boundary_missing * S ((S (h)) * v) + (1)))