polynomial_diagonal_sum_left_append

forall ab ac AB AC bb bc d N a b db dc eb ec u v. (forall mdr_i_pfp_tri_sum_equal mdr_a_pfp_tri_sum_equal. (exists mdr_gap_pfp_tri_sum_equalb. mdr_gap_pfp_tri_sum_equalb + S (mdr_i_pfp_tri_sum_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_sum_equalo. ff_h_mdr_pfp_tri_sum_equalo + S (mdr_a_pfp_tri_sum_equal) = S ((S (mdr_i_pfp_tri_sum_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_sum_equalo. ab = ff_q_mdr_pfp_tri_sum_equalo * S ((S (mdr_i_pfp_tri_sum_equal)) * ac) + (mdr_a_pfp_tri_sum_equal))) -> (((exists ff_h_mdr_pfp_tri_sum_equaln. ff_h_mdr_pfp_tri_sum_equaln + S (mdr_a_pfp_tri_sum_equal) = S ((S (mdr_i_pfp_tri_sum_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_sum_equaln. AB = ff_q_mdr_pfp_tri_sum_equaln * S ((S (mdr_i_pfp_tri_sum_equal)) * AC) + (mdr_a_pfp_tri_sum_equal)))) -> (((exists ff_h_pfp_tri_sum_appended. ff_h_pfp_tri_sum_appended + S (a) = S ((S (N)) * AC)) /\ exists ff_q_pfp_tri_sum_appended. AB = ff_q_pfp_tri_sum_appended * S ((S (N)) * AC) + (a))) -> (((exists ff_h_pfp_tri_sum_head. ff_h_pfp_tri_sum_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_tri_sum_head. bb = ff_q_pfp_tri_sum_head * S ((S (0)) * bc) + (b))) -> (forall pfc_index_tri_sum_old_table. (exists pfa_gap_tri_sum_old_tablebound. pfa_gap_tri_sum_old_tablebound + S (pfc_index_tri_sum_old_table) = (S N)) -> exists pfc_value_tri_sum_old_table. ((((exists ff_h_pfp_tri_sum_old_tableentry. ff_h_pfp_tri_sum_old_tableentry + S (pfc_value_tri_sum_old_table) = S ((S (pfc_index_tri_sum_old_table)) * dc)) /\ exists ff_q_pfp_tri_sum_old_tableentry. db = ff_q_pfp_tri_sum_old_tableentry * S ((S (pfc_index_tri_sum_old_table)) * dc) + (pfc_value_tri_sum_old_table))) /\ ((exists pfc_complement_tri_sum_old_tableterm pfc_left_tri_sum_old_tableterm pfc_right_tri_sum_old_tableterm. (((pfc_index_tri_sum_old_table)+pfc_complement_tri_sum_old_tableterm=(N)) /\ ((((((exists pfa_gap_tri_sum_old_tabletermleftinside. pfa_gap_tri_sum_old_tabletermleftinside + S (pfc_index_tri_sum_old_table) = (N)) /\ ((((exists ff_h_pfp_tri_sum_old_tabletermleftentry. ff_h_pfp_tri_sum_old_tabletermleftentry + S (pfc_left_tri_sum_old_tableterm) = S ((S (pfc_index_tri_sum_old_table)) * ac)) /\ exists ff_q_pfp_tri_sum_old_tabletermleftentry. ab = ff_q_pfp_tri_sum_old_tabletermleftentry * S ((S (pfc_index_tri_sum_old_table)) * ac) + (pfc_left_tri_sum_old_tableterm)))))) \/ (((exists pfc_gap_tri_sum_old_tabletermleftoutside. pfc_gap_tri_sum_old_tabletermleftoutside+(N)=(pfc_index_tri_sum_old_table)) /\ (((pfc_left_tri_sum_old_tableterm)=0))))) /\ ((((((exists pfa_gap_tri_sum_old_tabletermrightinside. pfa_gap_tri_sum_old_tabletermrightinside + S (pfc_complement_tri_sum_old_tableterm) = (S d)) /\ ((((exists ff_h_pfp_tri_sum_old_tabletermrightentry. ff_h_pfp_tri_sum_old_tabletermrightentry + S (pfc_right_tri_sum_old_tableterm) = S ((S (pfc_complement_tri_sum_old_tableterm)) * bc)) /\ exists ff_q_pfp_tri_sum_old_tabletermrightentry. bb = ff_q_pfp_tri_sum_old_tabletermrightentry * S ((S (pfc_complement_tri_sum_old_tableterm)) * bc) + (pfc_right_tri_sum_old_tableterm)))))) \/ (((exists pfc_gap_tri_sum_old_tabletermrightoutside. pfc_gap_tri_sum_old_tabletermrightoutside+(S d)=(pfc_complement_tri_sum_old_tableterm)) /\ (((pfc_right_tri_sum_old_tableterm)=0))))) /\ (((pfc_value_tri_sum_old_table)=pfc_left_tri_sum_old_tableterm*pfc_right_tri_sum_old_tableterm))))))))))) -> (exists fs_u_pfc_tri_sum_old_actual fs_v_pfc_tri_sum_old_actual. ((((exists fs_h_pfc_tri_sum_old_actual_body_start. fs_h_pfc_tri_sum_old_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_start. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_start * S ((S (0)) * fs_v_pfc_tri_sum_old_actual) + (0))) /\ ((((exists fs_h_pfc_tri_sum_old_actual_body_terminal. fs_h_pfc_tri_sum_old_actual_body_terminal + S (u) = S ((S (S N)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_terminal. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_terminal * S ((S (S N)) * fs_v_pfc_tri_sum_old_actual) + (u))) /\ forall fs_i_pfc_tri_sum_old_actual_body_steps. (exists fs_lt_pfc_tri_sum_old_actual_body_steps_bound. fs_lt_pfc_tri_sum_old_actual_body_steps_bound + S fs_i_pfc_tri_sum_old_actual_body_steps = S N) -> exists fs_a_pfc_tri_sum_old_actual_body_steps fs_r_pfc_tri_sum_old_actual_body_steps fs_s_pfc_tri_sum_old_actual_body_steps. ((((exists fs_h_pfc_tri_sum_old_actual_body_steps_summand. fs_h_pfc_tri_sum_old_actual_body_steps_summand + S (fs_a_pfc_tri_sum_old_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * dc)) /\ exists fs_q_pfc_tri_sum_old_actual_body_steps_summand. db = fs_q_pfc_tri_sum_old_actual_body_steps_summand * S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * dc) + (fs_a_pfc_tri_sum_old_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_old_actual_body_steps_partial. fs_h_pfc_tri_sum_old_actual_body_steps_partial + S (fs_r_pfc_tri_sum_old_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_steps_partial. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_steps_partial * S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual) + (fs_r_pfc_tri_sum_old_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_old_actual_body_steps_successor. fs_h_pfc_tri_sum_old_actual_body_steps_successor + S (fs_s_pfc_tri_sum_old_actual_body_steps) = S ((S (S fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_steps_successor. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual) + (fs_s_pfc_tri_sum_old_actual_body_steps))) /\ fs_s_pfc_tri_sum_old_actual_body_steps = fs_r_pfc_tri_sum_old_actual_body_steps + fs_a_pfc_tri_sum_old_actual_body_steps)))))) -> (forall pfc_index_tri_sum_new_table. (exists pfa_gap_tri_sum_new_tablebound. pfa_gap_tri_sum_new_tablebound + S (pfc_index_tri_sum_new_table) = (S N)) -> exists pfc_value_tri_sum_new_table. ((((exists ff_h_pfp_tri_sum_new_tableentry. ff_h_pfp_tri_sum_new_tableentry + S (pfc_value_tri_sum_new_table) = S ((S (pfc_index_tri_sum_new_table)) * ec)) /\ exists ff_q_pfp_tri_sum_new_tableentry. eb = ff_q_pfp_tri_sum_new_tableentry * S ((S (pfc_index_tri_sum_new_table)) * ec) + (pfc_value_tri_sum_new_table))) /\ ((exists pfc_complement_tri_sum_new_tableterm pfc_left_tri_sum_new_tableterm pfc_right_tri_sum_new_tableterm. (((pfc_index_tri_sum_new_table)+pfc_complement_tri_sum_new_tableterm=(N)) /\ ((((((exists pfa_gap_tri_sum_new_tabletermleftinside. pfa_gap_tri_sum_new_tabletermleftinside + S (pfc_index_tri_sum_new_table) = (S N)) /\ ((((exists ff_h_pfp_tri_sum_new_tabletermleftentry. ff_h_pfp_tri_sum_new_tabletermleftentry + S (pfc_left_tri_sum_new_tableterm) = S ((S (pfc_index_tri_sum_new_table)) * AC)) /\ exists ff_q_pfp_tri_sum_new_tabletermleftentry. AB = ff_q_pfp_tri_sum_new_tabletermleftentry * S ((S (pfc_index_tri_sum_new_table)) * AC) + (pfc_left_tri_sum_new_tableterm)))))) \/ (((exists pfc_gap_tri_sum_new_tabletermleftoutside. pfc_gap_tri_sum_new_tabletermleftoutside+(S N)=(pfc_index_tri_sum_new_table)) /\ (((pfc_left_tri_sum_new_tableterm)=0))))) /\ ((((((exists pfa_gap_tri_sum_new_tabletermrightinside. pfa_gap_tri_sum_new_tabletermrightinside + S (pfc_complement_tri_sum_new_tableterm) = (S d)) /\ ((((exists ff_h_pfp_tri_sum_new_tabletermrightentry. ff_h_pfp_tri_sum_new_tabletermrightentry + S (pfc_right_tri_sum_new_tableterm) = S ((S (pfc_complement_tri_sum_new_tableterm)) * bc)) /\ exists ff_q_pfp_tri_sum_new_tabletermrightentry. bb = ff_q_pfp_tri_sum_new_tabletermrightentry * S ((S (pfc_complement_tri_sum_new_tableterm)) * bc) + (pfc_right_tri_sum_new_tableterm)))))) \/ (((exists pfc_gap_tri_sum_new_tabletermrightoutside. pfc_gap_tri_sum_new_tabletermrightoutside+(S d)=(pfc_complement_tri_sum_new_tableterm)) /\ (((pfc_right_tri_sum_new_tableterm)=0))))) /\ (((pfc_value_tri_sum_new_table)=pfc_left_tri_sum_new_tableterm*pfc_right_tri_sum_new_tableterm))))))))))) -> (exists fs_u_pfc_tri_sum_new_actual fs_v_pfc_tri_sum_new_actual. ((((exists fs_h_pfc_tri_sum_new_actual_body_start. fs_h_pfc_tri_sum_new_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_start. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_start * S ((S (0)) * fs_v_pfc_tri_sum_new_actual) + (0))) /\ ((((exists fs_h_pfc_tri_sum_new_actual_body_terminal. fs_h_pfc_tri_sum_new_actual_body_terminal + S (v) = S ((S (S N)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_terminal. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_terminal * S ((S (S N)) * fs_v_pfc_tri_sum_new_actual) + (v))) /\ forall fs_i_pfc_tri_sum_new_actual_body_steps. (exists fs_lt_pfc_tri_sum_new_actual_body_steps_bound. fs_lt_pfc_tri_sum_new_actual_body_steps_bound + S fs_i_pfc_tri_sum_new_actual_body_steps = S N) -> exists fs_a_pfc_tri_sum_new_actual_body_steps fs_r_pfc_tri_sum_new_actual_body_steps fs_s_pfc_tri_sum_new_actual_body_steps. ((((exists fs_h_pfc_tri_sum_new_actual_body_steps_summand. fs_h_pfc_tri_sum_new_actual_body_steps_summand + S (fs_a_pfc_tri_sum_new_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * ec)) /\ exists fs_q_pfc_tri_sum_new_actual_body_steps_summand. eb = fs_q_pfc_tri_sum_new_actual_body_steps_summand * S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * ec) + (fs_a_pfc_tri_sum_new_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_new_actual_body_steps_partial. fs_h_pfc_tri_sum_new_actual_body_steps_partial + S (fs_r_pfc_tri_sum_new_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_steps_partial. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_steps_partial * S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual) + (fs_r_pfc_tri_sum_new_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_new_actual_body_steps_successor. fs_h_pfc_tri_sum_new_actual_body_steps_successor + S (fs_s_pfc_tri_sum_new_actual_body_steps) = S ((S (S fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_steps_successor. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual) + (fs_s_pfc_tri_sum_new_actual_body_steps))) /\ fs_s_pfc_tri_sum_new_actual_body_steps = fs_r_pfc_tri_sum_new_actual_body_steps + fs_a_pfc_tri_sum_new_actual_body_steps)))))) -> v=u+a*b