beta_sum_pointwise_mod_scale

forall p k ab ac bb bc L u v. (exists fs_u_pfc_scalar_sum_source fs_v_pfc_scalar_sum_source. ((((exists fs_h_pfc_scalar_sum_source_body_start. fs_h_pfc_scalar_sum_source_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_start. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_start * S ((S (0)) * fs_v_pfc_scalar_sum_source) + (0))) /\ ((((exists fs_h_pfc_scalar_sum_source_body_terminal. fs_h_pfc_scalar_sum_source_body_terminal + S (u) = S ((S (L)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_terminal. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_terminal * S ((S (L)) * fs_v_pfc_scalar_sum_source) + (u))) /\ forall fs_i_pfc_scalar_sum_source_body_steps. (exists fs_lt_pfc_scalar_sum_source_body_steps_bound. fs_lt_pfc_scalar_sum_source_body_steps_bound + S fs_i_pfc_scalar_sum_source_body_steps = L) -> exists fs_a_pfc_scalar_sum_source_body_steps fs_r_pfc_scalar_sum_source_body_steps fs_s_pfc_scalar_sum_source_body_steps. ((((exists fs_h_pfc_scalar_sum_source_body_steps_summand. fs_h_pfc_scalar_sum_source_body_steps_summand + S (fs_a_pfc_scalar_sum_source_body_steps) = S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * ac)) /\ exists fs_q_pfc_scalar_sum_source_body_steps_summand. ab = fs_q_pfc_scalar_sum_source_body_steps_summand * S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * ac) + (fs_a_pfc_scalar_sum_source_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_source_body_steps_partial. fs_h_pfc_scalar_sum_source_body_steps_partial + S (fs_r_pfc_scalar_sum_source_body_steps) = S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_steps_partial. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_steps_partial * S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source) + (fs_r_pfc_scalar_sum_source_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_source_body_steps_successor. fs_h_pfc_scalar_sum_source_body_steps_successor + S (fs_s_pfc_scalar_sum_source_body_steps) = S ((S (S fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_steps_successor. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_steps_successor * S ((S (S fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source) + (fs_s_pfc_scalar_sum_source_body_steps))) /\ fs_s_pfc_scalar_sum_source_body_steps = fs_r_pfc_scalar_sum_source_body_steps + fs_a_pfc_scalar_sum_source_body_steps)))))) -> (exists fs_u_pfc_scalar_sum_target fs_v_pfc_scalar_sum_target. ((((exists fs_h_pfc_scalar_sum_target_body_start. fs_h_pfc_scalar_sum_target_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_start. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_start * S ((S (0)) * fs_v_pfc_scalar_sum_target) + (0))) /\ ((((exists fs_h_pfc_scalar_sum_target_body_terminal. fs_h_pfc_scalar_sum_target_body_terminal + S (v) = S ((S (L)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_terminal. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_terminal * S ((S (L)) * fs_v_pfc_scalar_sum_target) + (v))) /\ forall fs_i_pfc_scalar_sum_target_body_steps. (exists fs_lt_pfc_scalar_sum_target_body_steps_bound. fs_lt_pfc_scalar_sum_target_body_steps_bound + S fs_i_pfc_scalar_sum_target_body_steps = L) -> exists fs_a_pfc_scalar_sum_target_body_steps fs_r_pfc_scalar_sum_target_body_steps fs_s_pfc_scalar_sum_target_body_steps. ((((exists fs_h_pfc_scalar_sum_target_body_steps_summand. fs_h_pfc_scalar_sum_target_body_steps_summand + S (fs_a_pfc_scalar_sum_target_body_steps) = S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * bc)) /\ exists fs_q_pfc_scalar_sum_target_body_steps_summand. bb = fs_q_pfc_scalar_sum_target_body_steps_summand * S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * bc) + (fs_a_pfc_scalar_sum_target_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_target_body_steps_partial. fs_h_pfc_scalar_sum_target_body_steps_partial + S (fs_r_pfc_scalar_sum_target_body_steps) = S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_steps_partial. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_steps_partial * S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target) + (fs_r_pfc_scalar_sum_target_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_target_body_steps_successor. fs_h_pfc_scalar_sum_target_body_steps_successor + S (fs_s_pfc_scalar_sum_target_body_steps) = S ((S (S fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_steps_successor. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_steps_successor * S ((S (S fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target) + (fs_s_pfc_scalar_sum_target_body_steps))) /\ fs_s_pfc_scalar_sum_target_body_steps = fs_r_pfc_scalar_sum_target_body_steps + fs_a_pfc_scalar_sum_target_body_steps)))))) -> (forall pfscalar_index_scalar_sum_points pfscalar_source_scalar_sum_points pfscalar_target_scalar_sum_points. (exists pfa_gap_scalar_sum_pointsindex. pfa_gap_scalar_sum_pointsindex + S (pfscalar_index_scalar_sum_points) = (L)) -> (((exists ff_h_pfp_scalar_sum_pointssource. ff_h_pfp_scalar_sum_pointssource + S (pfscalar_source_scalar_sum_points) = S ((S (pfscalar_index_scalar_sum_points)) * ac)) /\ exists ff_q_pfp_scalar_sum_pointssource. ab = ff_q_pfp_scalar_sum_pointssource * S ((S (pfscalar_index_scalar_sum_points)) * ac) + (pfscalar_source_scalar_sum_points))) -> (((exists ff_h_pfp_scalar_sum_pointstarget. ff_h_pfp_scalar_sum_pointstarget + S (pfscalar_target_scalar_sum_points) = S ((S (pfscalar_index_scalar_sum_points)) * bc)) /\ exists ff_q_pfp_scalar_sum_pointstarget. bb = ff_q_pfp_scalar_sum_pointstarget * S ((S (pfscalar_index_scalar_sum_points)) * bc) + (pfscalar_target_scalar_sum_points))) -> (exists pfa_offset_left_scalar_sum_pointscongruence pfa_offset_right_scalar_sum_pointscongruence. ((k)*pfscalar_source_scalar_sum_points) + (p) * pfa_offset_left_scalar_sum_pointscongruence = (pfscalar_target_scalar_sum_points) + (p) * pfa_offset_right_scalar_sum_pointscongruence)) -> (exists pfa_offset_left_scalar_sum_result pfa_offset_right_scalar_sum_result. (k*u) + (p) * pfa_offset_left_scalar_sum_result = (v) + (p) * pfa_offset_right_scalar_sum_result)