beta_sum_pointwise_add

forall b c d e f g l n m q. (exists ff_u_pointadd_left ff_v_pointadd_left. ((((exists ff_h_pointadd_left_start. ff_h_pointadd_left_start + S (0) = S ((S (0)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_start. ff_u_pointadd_left = ff_q_pointadd_left_start * S ((S (0)) * ff_v_pointadd_left) + (0))) /\ ((((exists ff_h_pointadd_left_terminal. ff_h_pointadd_left_terminal + S (n) = S ((S (l)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_terminal. ff_u_pointadd_left = ff_q_pointadd_left_terminal * S ((S (l)) * ff_v_pointadd_left) + (n))) /\ forall ff_i_pointadd_left. (exists ff_lt_pointadd_left_bound. ff_lt_pointadd_left_bound + S ff_i_pointadd_left = l) -> exists ff_a_pointadd_left ff_r_pointadd_left ff_s_pointadd_left. ((((exists ff_h_pointadd_left_summand. ff_h_pointadd_left_summand + S (ff_a_pointadd_left) = S ((S (ff_i_pointadd_left)) * c)) /\ exists ff_q_pointadd_left_summand. b = ff_q_pointadd_left_summand * S ((S (ff_i_pointadd_left)) * c) + (ff_a_pointadd_left))) /\ ((((exists ff_h_pointadd_left_partial. ff_h_pointadd_left_partial + S (ff_r_pointadd_left) = S ((S (ff_i_pointadd_left)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_partial. ff_u_pointadd_left = ff_q_pointadd_left_partial * S ((S (ff_i_pointadd_left)) * ff_v_pointadd_left) + (ff_r_pointadd_left))) /\ ((((exists ff_h_pointadd_left_successor. ff_h_pointadd_left_successor + S (ff_s_pointadd_left) = S ((S (S ff_i_pointadd_left)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_successor. ff_u_pointadd_left = ff_q_pointadd_left_successor * S ((S (S ff_i_pointadd_left)) * ff_v_pointadd_left) + (ff_s_pointadd_left))) /\ ff_s_pointadd_left = ff_r_pointadd_left + ff_a_pointadd_left)))))) -> (exists ff_u_pointadd_right ff_v_pointadd_right. ((((exists ff_h_pointadd_right_start. ff_h_pointadd_right_start + S (0) = S ((S (0)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_start. ff_u_pointadd_right = ff_q_pointadd_right_start * S ((S (0)) * ff_v_pointadd_right) + (0))) /\ ((((exists ff_h_pointadd_right_terminal. ff_h_pointadd_right_terminal + S (m) = S ((S (l)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_terminal. ff_u_pointadd_right = ff_q_pointadd_right_terminal * S ((S (l)) * ff_v_pointadd_right) + (m))) /\ forall ff_i_pointadd_right. (exists ff_lt_pointadd_right_bound. ff_lt_pointadd_right_bound + S ff_i_pointadd_right = l) -> exists ff_a_pointadd_right ff_r_pointadd_right ff_s_pointadd_right. ((((exists ff_h_pointadd_right_summand. ff_h_pointadd_right_summand + S (ff_a_pointadd_right) = S ((S (ff_i_pointadd_right)) * e)) /\ exists ff_q_pointadd_right_summand. d = ff_q_pointadd_right_summand * S ((S (ff_i_pointadd_right)) * e) + (ff_a_pointadd_right))) /\ ((((exists ff_h_pointadd_right_partial. ff_h_pointadd_right_partial + S (ff_r_pointadd_right) = S ((S (ff_i_pointadd_right)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_partial. ff_u_pointadd_right = ff_q_pointadd_right_partial * S ((S (ff_i_pointadd_right)) * ff_v_pointadd_right) + (ff_r_pointadd_right))) /\ ((((exists ff_h_pointadd_right_successor. ff_h_pointadd_right_successor + S (ff_s_pointadd_right) = S ((S (S ff_i_pointadd_right)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_successor. ff_u_pointadd_right = ff_q_pointadd_right_successor * S ((S (S ff_i_pointadd_right)) * ff_v_pointadd_right) + (ff_s_pointadd_right))) /\ ff_s_pointadd_right = ff_r_pointadd_right + ff_a_pointadd_right)))))) -> (exists ff_u_pointadd_total ff_v_pointadd_total. ((((exists ff_h_pointadd_total_start. ff_h_pointadd_total_start + S (0) = S ((S (0)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_start. ff_u_pointadd_total = ff_q_pointadd_total_start * S ((S (0)) * ff_v_pointadd_total) + (0))) /\ ((((exists ff_h_pointadd_total_terminal. ff_h_pointadd_total_terminal + S (q) = S ((S (l)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_terminal. ff_u_pointadd_total = ff_q_pointadd_total_terminal * S ((S (l)) * ff_v_pointadd_total) + (q))) /\ forall ff_i_pointadd_total. (exists ff_lt_pointadd_total_bound. ff_lt_pointadd_total_bound + S ff_i_pointadd_total = l) -> exists ff_a_pointadd_total ff_r_pointadd_total ff_s_pointadd_total. ((((exists ff_h_pointadd_total_summand. ff_h_pointadd_total_summand + S (ff_a_pointadd_total) = S ((S (ff_i_pointadd_total)) * g)) /\ exists ff_q_pointadd_total_summand. f = ff_q_pointadd_total_summand * S ((S (ff_i_pointadd_total)) * g) + (ff_a_pointadd_total))) /\ ((((exists ff_h_pointadd_total_partial. ff_h_pointadd_total_partial + S (ff_r_pointadd_total) = S ((S (ff_i_pointadd_total)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_partial. ff_u_pointadd_total = ff_q_pointadd_total_partial * S ((S (ff_i_pointadd_total)) * ff_v_pointadd_total) + (ff_r_pointadd_total))) /\ ((((exists ff_h_pointadd_total_successor. ff_h_pointadd_total_successor + S (ff_s_pointadd_total) = S ((S (S ff_i_pointadd_total)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_successor. ff_u_pointadd_total = ff_q_pointadd_total_successor * S ((S (S ff_i_pointadd_total)) * ff_v_pointadd_total) + (ff_s_pointadd_total))) /\ ff_s_pointadd_total = ff_r_pointadd_total + ff_a_pointadd_total)))))) -> (forall i a z s. (exists h. h + S i = l) -> (((exists ff_h_pointadd_left_entry. ff_h_pointadd_left_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pointadd_left_entry. b = ff_q_pointadd_left_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_pointadd_right_entry. ff_h_pointadd_right_entry + S (z) = S ((S (i)) * e)) /\ exists ff_q_pointadd_right_entry. d = ff_q_pointadd_right_entry * S ((S (i)) * e) + (z))) -> (((exists ff_h_pointadd_total_entry. ff_h_pointadd_total_entry + S (s) = S ((S (i)) * g)) /\ exists ff_q_pointadd_total_entry. f = ff_q_pointadd_total_entry * S ((S (i)) * g) + (s))) -> s = a + z) -> n + m = q