finite_modular_dyson_upper_from_union

forall b c d e tb tc ub uc p t v. ~(p=0) -> t+v=p -> (forall fms_i_pullback fms_j_pullback. (exists fms_gap_pullback_i. fms_gap_pullback_i + S (fms_i_pullback) = (p)) -> (exists fms_gap_pullback_j. fms_gap_pullback_j + S (fms_j_pullback) = (p)) -> (exists fms_u_pullback fms_v_pullback. (fms_i_pullback + v) + (p) * fms_u_pullback = (fms_j_pullback) + (p) * fms_v_pullback) -> ((((((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * tc)) /\ exists fs_q_fms_pullback_target. tb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * tc) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * e)) /\ exists fs_q_fms_pullback_source. d = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * e) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * e)) /\ exists fs_q_fms_pullback_source. d = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * e) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * tc)) /\ exists fs_q_fms_pullback_target. tb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * tc) + (1))))))) -> (forall fms_i_binary. (exists fms_gap_binary. fms_gap_binary + S (fms_i_binary) = (p)) -> ((((((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * uc)) /\ exists fs_q_fms_binary_result. ub = fs_q_fms_binary_result * S ((S (fms_i_binary)) * uc) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * tc)) /\ exists fs_q_fms_binary_right. tb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * tc) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * tc)) /\ exists fs_q_fms_binary_right. tb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * tc) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * uc)) /\ exists fs_q_fms_binary_result. ub = fs_q_fms_binary_result * S ((S (fms_i_binary)) * uc) + (1))))))) -> (forall cd_output_upper. (exists fms_gap_cd_upper_bound. fms_gap_cd_upper_bound + S (cd_output_upper) = (p)) -> ((((((exists fs_h_cd_upper_result. fs_h_cd_upper_result + S (1) = S ((S (cd_output_upper)) * uc)) /\ exists fs_q_cd_upper_result. ub = fs_q_cd_upper_result * S ((S (cd_output_upper)) * uc) + (1))) -> ((((exists fs_h_cd_upper_old. fs_h_cd_upper_old + S (1) = S ((S (cd_output_upper)) * c)) /\ exists fs_q_cd_upper_old. b = fs_q_cd_upper_old * S ((S (cd_output_upper)) * c) + (1))) \/ (exists cd_source_upper. (((exists fms_gap_cd_upper_member. fms_gap_cd_upper_member + S (cd_source_upper) = (p)) /\ (((exists fs_h_fms_cd_upper_member. fs_h_fms_cd_upper_member + S (1) = S ((S (cd_source_upper)) * e)) /\ exists fs_q_fms_cd_upper_member. d = fs_q_fms_cd_upper_member * S ((S (cd_source_upper)) * e) + (1))))) /\ (exists fms_u_cd_upper_mod fms_v_cd_upper_mod. (cd_source_upper+t) + (p) * fms_u_cd_upper_mod = (cd_output_upper) + (p) * fms_v_cd_upper_mod)))) /\ (((((exists fs_h_cd_upper_old. fs_h_cd_upper_old + S (1) = S ((S (cd_output_upper)) * c)) /\ exists fs_q_cd_upper_old. b = fs_q_cd_upper_old * S ((S (cd_output_upper)) * c) + (1))) \/ (exists cd_source_upper. (((exists fms_gap_cd_upper_member. fms_gap_cd_upper_member + S (cd_source_upper) = (p)) /\ (((exists fs_h_fms_cd_upper_member. fs_h_fms_cd_upper_member + S (1) = S ((S (cd_source_upper)) * e)) /\ exists fs_q_fms_cd_upper_member. d = fs_q_fms_cd_upper_member * S ((S (cd_source_upper)) * e) + (1))))) /\ (exists fms_u_cd_upper_mod fms_v_cd_upper_mod. (cd_source_upper+t) + (p) * fms_u_cd_upper_mod = (cd_output_upper) + (p) * fms_v_cd_upper_mod))) -> (((exists fs_h_cd_upper_result. fs_h_cd_upper_result + S (1) = S ((S (cd_output_upper)) * uc)) /\ exists fs_q_cd_upper_result. ub = fs_q_cd_upper_result * S ((S (cd_output_upper)) * uc) + (1)))))))