polynomial_diagonal_sum_right_scale_congruent

forall p k ab ac L bb bc M sb sc i db dc eb ec N u v. (((exists pfa_gap_scalar_diagonal_operationscalar. pfa_gap_scalar_diagonal_operationscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_diagonal_operation. (exists pfa_gap_scalar_diagonal_operationindex. pfa_gap_scalar_diagonal_operationindex + S (pfp_index_scalar_diagonal_operation) = (M)) -> exists pfp_source_scalar_diagonal_operation pfp_value_scalar_diagonal_operation. ((((exists ff_h_pfp_scalar_diagonal_operationsource. ff_h_pfp_scalar_diagonal_operationsource + S (pfp_source_scalar_diagonal_operation) = S ((S (pfp_index_scalar_diagonal_operation)) * bc)) /\ exists ff_q_pfp_scalar_diagonal_operationsource. bb = ff_q_pfp_scalar_diagonal_operationsource * S ((S (pfp_index_scalar_diagonal_operation)) * bc) + (pfp_source_scalar_diagonal_operation))) /\ (((((exists ff_h_pfp_scalar_diagonal_operationtarget. ff_h_pfp_scalar_diagonal_operationtarget + S (pfp_value_scalar_diagonal_operation) = S ((S (pfp_index_scalar_diagonal_operation)) * sc)) /\ exists ff_q_pfp_scalar_diagonal_operationtarget. sb = ff_q_pfp_scalar_diagonal_operationtarget * S ((S (pfp_index_scalar_diagonal_operation)) * sc) + (pfp_value_scalar_diagonal_operation))) /\ ((((exists pfa_gap_scalar_diagonal_operationoperationleft. pfa_gap_scalar_diagonal_operationoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_diagonal_operationoperationright. pfa_gap_scalar_diagonal_operationoperationright + S (pfp_source_scalar_diagonal_operation) = (p)) /\ ((((exists pfa_gap_scalar_diagonal_operationoperationresultbound. pfa_gap_scalar_diagonal_operationoperationresultbound + S (pfp_value_scalar_diagonal_operation) = (p)) /\ ((exists pfa_offset_left_scalar_diagonal_operationoperationresultcongruence pfa_offset_right_scalar_diagonal_operationoperationresultcongruence. ((k) * (pfp_source_scalar_diagonal_operation)) + (p) * pfa_offset_left_scalar_diagonal_operationoperationresultcongruence = (pfp_value_scalar_diagonal_operation) + (p) * pfa_offset_right_scalar_diagonal_operationoperationresultcongruence))))))))))))))))) -> (forall pfc_index_scalar_diagonal_old. (exists pfa_gap_scalar_diagonal_oldbound. pfa_gap_scalar_diagonal_oldbound + S (pfc_index_scalar_diagonal_old) = (N)) -> exists pfc_value_scalar_diagonal_old. ((((exists ff_h_pfp_scalar_diagonal_oldentry. ff_h_pfp_scalar_diagonal_oldentry + S (pfc_value_scalar_diagonal_old) = S ((S (pfc_index_scalar_diagonal_old)) * dc)) /\ exists ff_q_pfp_scalar_diagonal_oldentry. db = ff_q_pfp_scalar_diagonal_oldentry * S ((S (pfc_index_scalar_diagonal_old)) * dc) + (pfc_value_scalar_diagonal_old))) /\ ((exists pfc_complement_scalar_diagonal_oldterm pfc_left_scalar_diagonal_oldterm pfc_right_scalar_diagonal_oldterm. (((pfc_index_scalar_diagonal_old)+pfc_complement_scalar_diagonal_oldterm=(i)) /\ ((((((exists pfa_gap_scalar_diagonal_oldtermleftinside. pfa_gap_scalar_diagonal_oldtermleftinside + S (pfc_index_scalar_diagonal_old) = (L)) /\ ((((exists ff_h_pfp_scalar_diagonal_oldtermleftentry. ff_h_pfp_scalar_diagonal_oldtermleftentry + S (pfc_left_scalar_diagonal_oldterm) = S ((S (pfc_index_scalar_diagonal_old)) * ac)) /\ exists ff_q_pfp_scalar_diagonal_oldtermleftentry. ab = ff_q_pfp_scalar_diagonal_oldtermleftentry * S ((S (pfc_index_scalar_diagonal_old)) * ac) + (pfc_left_scalar_diagonal_oldterm)))))) \/ (((exists pfc_gap_scalar_diagonal_oldtermleftoutside. pfc_gap_scalar_diagonal_oldtermleftoutside+(L)=(pfc_index_scalar_diagonal_old)) /\ (((pfc_left_scalar_diagonal_oldterm)=0))))) /\ ((((((exists pfa_gap_scalar_diagonal_oldtermrightinside. pfa_gap_scalar_diagonal_oldtermrightinside + S (pfc_complement_scalar_diagonal_oldterm) = (M)) /\ ((((exists ff_h_pfp_scalar_diagonal_oldtermrightentry. ff_h_pfp_scalar_diagonal_oldtermrightentry + S (pfc_right_scalar_diagonal_oldterm) = S ((S (pfc_complement_scalar_diagonal_oldterm)) * bc)) /\ exists ff_q_pfp_scalar_diagonal_oldtermrightentry. bb = ff_q_pfp_scalar_diagonal_oldtermrightentry * S ((S (pfc_complement_scalar_diagonal_oldterm)) * bc) + (pfc_right_scalar_diagonal_oldterm)))))) \/ (((exists pfc_gap_scalar_diagonal_oldtermrightoutside. pfc_gap_scalar_diagonal_oldtermrightoutside+(M)=(pfc_complement_scalar_diagonal_oldterm)) /\ (((pfc_right_scalar_diagonal_oldterm)=0))))) /\ (((pfc_value_scalar_diagonal_old)=pfc_left_scalar_diagonal_oldterm*pfc_right_scalar_diagonal_oldterm))))))))))) -> (exists fs_u_pfc_scalar_diagonal_old_sum fs_v_pfc_scalar_diagonal_old_sum. ((((exists fs_h_pfc_scalar_diagonal_old_sum_body_start. fs_h_pfc_scalar_diagonal_old_sum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_diagonal_old_sum)) /\ exists fs_q_pfc_scalar_diagonal_old_sum_body_start. fs_u_pfc_scalar_diagonal_old_sum = fs_q_pfc_scalar_diagonal_old_sum_body_start * S ((S (0)) * fs_v_pfc_scalar_diagonal_old_sum) + (0))) /\ ((((exists fs_h_pfc_scalar_diagonal_old_sum_body_terminal. fs_h_pfc_scalar_diagonal_old_sum_body_terminal + S (u) = S ((S (N)) * fs_v_pfc_scalar_diagonal_old_sum)) /\ exists fs_q_pfc_scalar_diagonal_old_sum_body_terminal. fs_u_pfc_scalar_diagonal_old_sum = fs_q_pfc_scalar_diagonal_old_sum_body_terminal * S ((S (N)) * fs_v_pfc_scalar_diagonal_old_sum) + (u))) /\ forall fs_i_pfc_scalar_diagonal_old_sum_body_steps. (exists fs_lt_pfc_scalar_diagonal_old_sum_body_steps_bound. fs_lt_pfc_scalar_diagonal_old_sum_body_steps_bound + S fs_i_pfc_scalar_diagonal_old_sum_body_steps = N) -> exists fs_a_pfc_scalar_diagonal_old_sum_body_steps fs_r_pfc_scalar_diagonal_old_sum_body_steps fs_s_pfc_scalar_diagonal_old_sum_body_steps. ((((exists fs_h_pfc_scalar_diagonal_old_sum_body_steps_summand. fs_h_pfc_scalar_diagonal_old_sum_body_steps_summand + S (fs_a_pfc_scalar_diagonal_old_sum_body_steps) = S ((S (fs_i_pfc_scalar_diagonal_old_sum_body_steps)) * dc)) /\ exists fs_q_pfc_scalar_diagonal_old_sum_body_steps_summand. db = fs_q_pfc_scalar_diagonal_old_sum_body_steps_summand * S ((S (fs_i_pfc_scalar_diagonal_old_sum_body_steps)) * dc) + (fs_a_pfc_scalar_diagonal_old_sum_body_steps))) /\ ((((exists fs_h_pfc_scalar_diagonal_old_sum_body_steps_partial. fs_h_pfc_scalar_diagonal_old_sum_body_steps_partial + S (fs_r_pfc_scalar_diagonal_old_sum_body_steps) = S ((S (fs_i_pfc_scalar_diagonal_old_sum_body_steps)) * fs_v_pfc_scalar_diagonal_old_sum)) /\ exists fs_q_pfc_scalar_diagonal_old_sum_body_steps_partial. fs_u_pfc_scalar_diagonal_old_sum = fs_q_pfc_scalar_diagonal_old_sum_body_steps_partial * S ((S (fs_i_pfc_scalar_diagonal_old_sum_body_steps)) * fs_v_pfc_scalar_diagonal_old_sum) + (fs_r_pfc_scalar_diagonal_old_sum_body_steps))) /\ ((((exists fs_h_pfc_scalar_diagonal_old_sum_body_steps_successor. fs_h_pfc_scalar_diagonal_old_sum_body_steps_successor + S (fs_s_pfc_scalar_diagonal_old_sum_body_steps) = S ((S (S fs_i_pfc_scalar_diagonal_old_sum_body_steps)) * fs_v_pfc_scalar_diagonal_old_sum)) /\ exists fs_q_pfc_scalar_diagonal_old_sum_body_steps_successor. fs_u_pfc_scalar_diagonal_old_sum = fs_q_pfc_scalar_diagonal_old_sum_body_steps_successor * S ((S (S fs_i_pfc_scalar_diagonal_old_sum_body_steps)) * fs_v_pfc_scalar_diagonal_old_sum) + (fs_s_pfc_scalar_diagonal_old_sum_body_steps))) /\ fs_s_pfc_scalar_diagonal_old_sum_body_steps = fs_r_pfc_scalar_diagonal_old_sum_body_steps + fs_a_pfc_scalar_diagonal_old_sum_body_steps)))))) -> (forall pfc_index_scalar_diagonal_new. (exists pfa_gap_scalar_diagonal_newbound. pfa_gap_scalar_diagonal_newbound + S (pfc_index_scalar_diagonal_new) = (N)) -> exists pfc_value_scalar_diagonal_new. ((((exists ff_h_pfp_scalar_diagonal_newentry. ff_h_pfp_scalar_diagonal_newentry + S (pfc_value_scalar_diagonal_new) = S ((S (pfc_index_scalar_diagonal_new)) * ec)) /\ exists ff_q_pfp_scalar_diagonal_newentry. eb = ff_q_pfp_scalar_diagonal_newentry * S ((S (pfc_index_scalar_diagonal_new)) * ec) + (pfc_value_scalar_diagonal_new))) /\ ((exists pfc_complement_scalar_diagonal_newterm pfc_left_scalar_diagonal_newterm pfc_right_scalar_diagonal_newterm. (((pfc_index_scalar_diagonal_new)+pfc_complement_scalar_diagonal_newterm=(i)) /\ ((((((exists pfa_gap_scalar_diagonal_newtermleftinside. pfa_gap_scalar_diagonal_newtermleftinside + S (pfc_index_scalar_diagonal_new) = (L)) /\ ((((exists ff_h_pfp_scalar_diagonal_newtermleftentry. ff_h_pfp_scalar_diagonal_newtermleftentry + S (pfc_left_scalar_diagonal_newterm) = S ((S (pfc_index_scalar_diagonal_new)) * ac)) /\ exists ff_q_pfp_scalar_diagonal_newtermleftentry. ab = ff_q_pfp_scalar_diagonal_newtermleftentry * S ((S (pfc_index_scalar_diagonal_new)) * ac) + (pfc_left_scalar_diagonal_newterm)))))) \/ (((exists pfc_gap_scalar_diagonal_newtermleftoutside. pfc_gap_scalar_diagonal_newtermleftoutside+(L)=(pfc_index_scalar_diagonal_new)) /\ (((pfc_left_scalar_diagonal_newterm)=0))))) /\ ((((((exists pfa_gap_scalar_diagonal_newtermrightinside. pfa_gap_scalar_diagonal_newtermrightinside + S (pfc_complement_scalar_diagonal_newterm) = (M)) /\ ((((exists ff_h_pfp_scalar_diagonal_newtermrightentry. ff_h_pfp_scalar_diagonal_newtermrightentry + S (pfc_right_scalar_diagonal_newterm) = S ((S (pfc_complement_scalar_diagonal_newterm)) * sc)) /\ exists ff_q_pfp_scalar_diagonal_newtermrightentry. sb = ff_q_pfp_scalar_diagonal_newtermrightentry * S ((S (pfc_complement_scalar_diagonal_newterm)) * sc) + (pfc_right_scalar_diagonal_newterm)))))) \/ (((exists pfc_gap_scalar_diagonal_newtermrightoutside. pfc_gap_scalar_diagonal_newtermrightoutside+(M)=(pfc_complement_scalar_diagonal_newterm)) /\ (((pfc_right_scalar_diagonal_newterm)=0))))) /\ (((pfc_value_scalar_diagonal_new)=pfc_left_scalar_diagonal_newterm*pfc_right_scalar_diagonal_newterm))))))))))) -> (exists fs_u_pfc_scalar_diagonal_new_sum fs_v_pfc_scalar_diagonal_new_sum. ((((exists fs_h_pfc_scalar_diagonal_new_sum_body_start. fs_h_pfc_scalar_diagonal_new_sum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_diagonal_new_sum)) /\ exists fs_q_pfc_scalar_diagonal_new_sum_body_start. fs_u_pfc_scalar_diagonal_new_sum = fs_q_pfc_scalar_diagonal_new_sum_body_start * S ((S (0)) * fs_v_pfc_scalar_diagonal_new_sum) + (0))) /\ ((((exists fs_h_pfc_scalar_diagonal_new_sum_body_terminal. fs_h_pfc_scalar_diagonal_new_sum_body_terminal + S (v) = S ((S (N)) * fs_v_pfc_scalar_diagonal_new_sum)) /\ exists fs_q_pfc_scalar_diagonal_new_sum_body_terminal. fs_u_pfc_scalar_diagonal_new_sum = fs_q_pfc_scalar_diagonal_new_sum_body_terminal * S ((S (N)) * fs_v_pfc_scalar_diagonal_new_sum) + (v))) /\ forall fs_i_pfc_scalar_diagonal_new_sum_body_steps. (exists fs_lt_pfc_scalar_diagonal_new_sum_body_steps_bound. fs_lt_pfc_scalar_diagonal_new_sum_body_steps_bound + S fs_i_pfc_scalar_diagonal_new_sum_body_steps = N) -> exists fs_a_pfc_scalar_diagonal_new_sum_body_steps fs_r_pfc_scalar_diagonal_new_sum_body_steps fs_s_pfc_scalar_diagonal_new_sum_body_steps. ((((exists fs_h_pfc_scalar_diagonal_new_sum_body_steps_summand. fs_h_pfc_scalar_diagonal_new_sum_body_steps_summand + S (fs_a_pfc_scalar_diagonal_new_sum_body_steps) = S ((S (fs_i_pfc_scalar_diagonal_new_sum_body_steps)) * ec)) /\ exists fs_q_pfc_scalar_diagonal_new_sum_body_steps_summand. eb = fs_q_pfc_scalar_diagonal_new_sum_body_steps_summand * S ((S (fs_i_pfc_scalar_diagonal_new_sum_body_steps)) * ec) + (fs_a_pfc_scalar_diagonal_new_sum_body_steps))) /\ ((((exists fs_h_pfc_scalar_diagonal_new_sum_body_steps_partial. fs_h_pfc_scalar_diagonal_new_sum_body_steps_partial + S (fs_r_pfc_scalar_diagonal_new_sum_body_steps) = S ((S (fs_i_pfc_scalar_diagonal_new_sum_body_steps)) * fs_v_pfc_scalar_diagonal_new_sum)) /\ exists fs_q_pfc_scalar_diagonal_new_sum_body_steps_partial. fs_u_pfc_scalar_diagonal_new_sum = fs_q_pfc_scalar_diagonal_new_sum_body_steps_partial * S ((S (fs_i_pfc_scalar_diagonal_new_sum_body_steps)) * fs_v_pfc_scalar_diagonal_new_sum) + (fs_r_pfc_scalar_diagonal_new_sum_body_steps))) /\ ((((exists fs_h_pfc_scalar_diagonal_new_sum_body_steps_successor. fs_h_pfc_scalar_diagonal_new_sum_body_steps_successor + S (fs_s_pfc_scalar_diagonal_new_sum_body_steps) = S ((S (S fs_i_pfc_scalar_diagonal_new_sum_body_steps)) * fs_v_pfc_scalar_diagonal_new_sum)) /\ exists fs_q_pfc_scalar_diagonal_new_sum_body_steps_successor. fs_u_pfc_scalar_diagonal_new_sum = fs_q_pfc_scalar_diagonal_new_sum_body_steps_successor * S ((S (S fs_i_pfc_scalar_diagonal_new_sum_body_steps)) * fs_v_pfc_scalar_diagonal_new_sum) + (fs_s_pfc_scalar_diagonal_new_sum_body_steps))) /\ fs_s_pfc_scalar_diagonal_new_sum_body_steps = fs_r_pfc_scalar_diagonal_new_sum_body_steps + fs_a_pfc_scalar_diagonal_new_sum_body_steps)))))) -> (exists pfa_offset_left_scalar_diagonal_result pfa_offset_right_scalar_diagonal_result. (k*u) + (p) * pfa_offset_left_scalar_diagonal_result = (v) + (p) * pfa_offset_right_scalar_diagonal_result)