divisor_signed_sum_successor_intro

Exact expanded first-order arithmetic statement

forall F l a b c. (exists dst_positive_code_step_sum dst_positive_scale_step_sum dst_negative_code_step_sum dst_negative_scale_step_sum dst_positive_sum_step_sum dst_negative_sum_step_sum. (((F) = (((((dst_positive_code_step_sum) + (dst_positive_scale_step_sum)) * S ((dst_positive_code_step_sum) + (dst_positive_scale_step_sum)) + ((dst_positive_scale_step_sum) + (dst_positive_scale_step_sum))) + (((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) * S ((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) + ((dst_negative_scale_step_sum) + (dst_negative_scale_step_sum)))) * S ((((dst_positive_code_step_sum) + (dst_positive_scale_step_sum)) * S ((dst_positive_code_step_sum) + (dst_positive_scale_step_sum)) + ((dst_positive_scale_step_sum) + (dst_positive_scale_step_sum))) + (((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) * S ((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) + ((dst_negative_scale_step_sum) + (dst_negative_scale_step_sum)))) + ((((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) * S ((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) + ((dst_negative_scale_step_sum) + (dst_negative_scale_step_sum))) + (((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) * S ((dst_negative_code_step_sum) + (dst_negative_scale_step_sum)) + ((dst_negative_scale_step_sum) + (dst_negative_scale_step_sum)))))) /\ (((exists fs_u_dst_step_sumpositive fs_v_dst_step_sumpositive. ((((exists fs_h_dst_step_sumpositive_body_start. fs_h_dst_step_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_step_sumpositive)) /\ exists fs_q_dst_step_sumpositive_body_start. fs_u_dst_step_sumpositive = fs_q_dst_step_sumpositive_body_start * S ((S (0)) * fs_v_dst_step_sumpositive) + (0))) /\ ((((exists fs_h_dst_step_sumpositive_body_terminal. fs_h_dst_step_sumpositive_body_terminal + S (dst_positive_sum_step_sum) = S ((S (l)) * fs_v_dst_step_sumpositive)) /\ exists fs_q_dst_step_sumpositive_body_terminal. fs_u_dst_step_sumpositive = fs_q_dst_step_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_step_sumpositive) + (dst_positive_sum_step_sum))) /\ forall fs_i_dst_step_sumpositive_body_steps. (exists fs_lt_dst_step_sumpositive_body_steps_bound. fs_lt_dst_step_sumpositive_body_steps_bound + S fs_i_dst_step_sumpositive_body_steps = l) -> exists fs_a_dst_step_sumpositive_body_steps fs_r_dst_step_sumpositive_body_steps fs_s_dst_step_sumpositive_body_steps. ((((exists fs_h_dst_step_sumpositive_body_steps_summand. fs_h_dst_step_sumpositive_body_steps_summand + S (fs_a_dst_step_sumpositive_body_steps) = S ((S (fs_i_dst_step_sumpositive_body_steps)) * dst_positive_scale_step_sum)) /\ exists fs_q_dst_step_sumpositive_body_steps_summand. dst_positive_code_step_sum = fs_q_dst_step_sumpositive_body_steps_summand * S ((S (fs_i_dst_step_sumpositive_body_steps)) * dst_positive_scale_step_sum) + (fs_a_dst_step_sumpositive_body_steps))) /\ ((((exists fs_h_dst_step_sumpositive_body_steps_partial. fs_h_dst_step_sumpositive_body_steps_partial + S (fs_r_dst_step_sumpositive_body_steps) = S ((S (fs_i_dst_step_sumpositive_body_steps)) * fs_v_dst_step_sumpositive)) /\ exists fs_q_dst_step_sumpositive_body_steps_partial. fs_u_dst_step_sumpositive = fs_q_dst_step_sumpositive_body_steps_partial * S ((S (fs_i_dst_step_sumpositive_body_steps)) * fs_v_dst_step_sumpositive) + (fs_r_dst_step_sumpositive_body_steps))) /\ ((((exists fs_h_dst_step_sumpositive_body_steps_successor. fs_h_dst_step_sumpositive_body_steps_successor + S (fs_s_dst_step_sumpositive_body_steps) = S ((S (S fs_i_dst_step_sumpositive_body_steps)) * fs_v_dst_step_sumpositive)) /\ exists fs_q_dst_step_sumpositive_body_steps_successor. fs_u_dst_step_sumpositive = fs_q_dst_step_sumpositive_body_steps_successor * S ((S (S fs_i_dst_step_sumpositive_body_steps)) * fs_v_dst_step_sumpositive) + (fs_s_dst_step_sumpositive_body_steps))) /\ fs_s_dst_step_sumpositive_body_steps = fs_r_dst_step_sumpositive_body_steps + fs_a_dst_step_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_step_sumnegative fs_v_dst_step_sumnegative. ((((exists fs_h_dst_step_sumnegative_body_start. fs_h_dst_step_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_step_sumnegative)) /\ exists fs_q_dst_step_sumnegative_body_start. fs_u_dst_step_sumnegative = fs_q_dst_step_sumnegative_body_start * S ((S (0)) * fs_v_dst_step_sumnegative) + (0))) /\ ((((exists fs_h_dst_step_sumnegative_body_terminal. fs_h_dst_step_sumnegative_body_terminal + S (dst_negative_sum_step_sum) = S ((S (l)) * fs_v_dst_step_sumnegative)) /\ exists fs_q_dst_step_sumnegative_body_terminal. fs_u_dst_step_sumnegative = fs_q_dst_step_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_step_sumnegative) + (dst_negative_sum_step_sum))) /\ forall fs_i_dst_step_sumnegative_body_steps. (exists fs_lt_dst_step_sumnegative_body_steps_bound. fs_lt_dst_step_sumnegative_body_steps_bound + S fs_i_dst_step_sumnegative_body_steps = l) -> exists fs_a_dst_step_sumnegative_body_steps fs_r_dst_step_sumnegative_body_steps fs_s_dst_step_sumnegative_body_steps. ((((exists fs_h_dst_step_sumnegative_body_steps_summand. fs_h_dst_step_sumnegative_body_steps_summand + S (fs_a_dst_step_sumnegative_body_steps) = S ((S (fs_i_dst_step_sumnegative_body_steps)) * dst_negative_scale_step_sum)) /\ exists fs_q_dst_step_sumnegative_body_steps_summand. dst_negative_code_step_sum = fs_q_dst_step_sumnegative_body_steps_summand * S ((S (fs_i_dst_step_sumnegative_body_steps)) * dst_negative_scale_step_sum) + (fs_a_dst_step_sumnegative_body_steps))) /\ ((((exists fs_h_dst_step_sumnegative_body_steps_partial. fs_h_dst_step_sumnegative_body_steps_partial + S (fs_r_dst_step_sumnegative_body_steps) = S ((S (fs_i_dst_step_sumnegative_body_steps)) * fs_v_dst_step_sumnegative)) /\ exists fs_q_dst_step_sumnegative_body_steps_partial. fs_u_dst_step_sumnegative = fs_q_dst_step_sumnegative_body_steps_partial * S ((S (fs_i_dst_step_sumnegative_body_steps)) * fs_v_dst_step_sumnegative) + (fs_r_dst_step_sumnegative_body_steps))) /\ ((((exists fs_h_dst_step_sumnegative_body_steps_successor. fs_h_dst_step_sumnegative_body_steps_successor + S (fs_s_dst_step_sumnegative_body_steps) = S ((S (S fs_i_dst_step_sumnegative_body_steps)) * fs_v_dst_step_sumnegative)) /\ exists fs_q_dst_step_sumnegative_body_steps_successor. fs_u_dst_step_sumnegative = fs_q_dst_step_sumnegative_body_steps_successor * S ((S (S fs_i_dst_step_sumnegative_body_steps)) * fs_v_dst_step_sumnegative) + (fs_s_dst_step_sumnegative_body_steps))) /\ fs_s_dst_step_sumnegative_body_steps = fs_r_dst_step_sumnegative_body_steps + fs_a_dst_step_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_step_sumresult ge_balance_negative_step_sumresult. (((((a) = 2 * (ge_balance_positive_step_sumresult) /\ (ge_balance_negative_step_sumresult) = 0) \/ exists ge_signed_half_step_sumresultdecode. (((a) = 2 * ge_signed_half_step_sumresultdecode + 1 /\ (ge_balance_positive_step_sumresult) = 0) /\ (ge_balance_negative_step_sumresult) = S ge_signed_half_step_sumresultdecode))) /\ ((dst_positive_sum_step_sum) + ge_balance_negative_step_sumresult = (dst_negative_sum_step_sum) + ge_balance_positive_step_sumresult))))))))) -> (exists dst_positive_code_step_entry dst_positive_scale_step_entry dst_negative_code_step_entry dst_negative_scale_step_entry dst_positive_step_entry dst_negative_step_entry. (((F) = (((((dst_positive_code_step_entry) + (dst_positive_scale_step_entry)) * S ((dst_positive_code_step_entry) + (dst_positive_scale_step_entry)) + ((dst_positive_scale_step_entry) + (dst_positive_scale_step_entry))) + (((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) * S ((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) + ((dst_negative_scale_step_entry) + (dst_negative_scale_step_entry)))) * S ((((dst_positive_code_step_entry) + (dst_positive_scale_step_entry)) * S ((dst_positive_code_step_entry) + (dst_positive_scale_step_entry)) + ((dst_positive_scale_step_entry) + (dst_positive_scale_step_entry))) + (((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) * S ((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) + ((dst_negative_scale_step_entry) + (dst_negative_scale_step_entry)))) + ((((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) * S ((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) + ((dst_negative_scale_step_entry) + (dst_negative_scale_step_entry))) + (((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) * S ((dst_negative_code_step_entry) + (dst_negative_scale_step_entry)) + ((dst_negative_scale_step_entry) + (dst_negative_scale_step_entry)))))) /\ (((((exists ff_h_pvs_step_entrypositive. ff_h_pvs_step_entrypositive + S (dst_positive_step_entry) = S ((S (l)) * dst_positive_scale_step_entry)) /\ exists ff_q_pvs_step_entrypositive. dst_positive_code_step_entry = ff_q_pvs_step_entrypositive * S ((S (l)) * dst_positive_scale_step_entry) + (dst_positive_step_entry))) /\ (((((exists ff_h_pvs_step_entrynegative. ff_h_pvs_step_entrynegative + S (dst_negative_step_entry) = S ((S (l)) * dst_negative_scale_step_entry)) /\ exists ff_q_pvs_step_entrynegative. dst_negative_code_step_entry = ff_q_pvs_step_entrynegative * S ((S (l)) * dst_negative_scale_step_entry) + (dst_negative_step_entry))) /\ (exists ge_balance_positive_step_entryvalue ge_balance_negative_step_entryvalue. (((((b) = 2 * (ge_balance_positive_step_entryvalue) /\ (ge_balance_negative_step_entryvalue) = 0) \/ exists ge_signed_half_step_entryvaluedecode. (((b) = 2 * ge_signed_half_step_entryvaluedecode + 1 /\ (ge_balance_positive_step_entryvalue) = 0) /\ (ge_balance_negative_step_entryvalue) = S ge_signed_half_step_entryvaluedecode))) /\ ((dst_positive_step_entry) + ge_balance_negative_step_entryvalue = (dst_negative_step_entry) + ge_balance_positive_step_entryvalue))))))))) -> (exists dsa_ap_step_add dsa_an_step_add dsa_bp_step_add dsa_bn_step_add dsa_cp_step_add dsa_cn_step_add. (((((a) = 2 * (dsa_ap_step_add) /\ (dsa_an_step_add) = 0) \/ exists ge_signed_half_step_addleft. (((a) = 2 * ge_signed_half_step_addleft + 1 /\ (dsa_ap_step_add) = 0) /\ (dsa_an_step_add) = S ge_signed_half_step_addleft))) /\ ((((((b) = 2 * (dsa_bp_step_add) /\ (dsa_bn_step_add) = 0) \/ exists ge_signed_half_step_addright. (((b) = 2 * ge_signed_half_step_addright + 1 /\ (dsa_bp_step_add) = 0) /\ (dsa_bn_step_add) = S ge_signed_half_step_addright))) /\ ((((((c) = 2 * (dsa_cp_step_add) /\ (dsa_cn_step_add) = 0) \/ exists ge_signed_half_step_addoutput. (((c) = 2 * ge_signed_half_step_addoutput + 1 /\ (dsa_cp_step_add) = 0) /\ (dsa_cn_step_add) = S ge_signed_half_step_addoutput))) /\ ((dsa_ap_step_add + dsa_bp_step_add) + dsa_cn_step_add = (dsa_an_step_add + dsa_bn_step_add) + dsa_cp_step_add))))))) -> (exists dst_positive_code_step_result dst_positive_scale_step_result dst_negative_code_step_result dst_negative_scale_step_result dst_positive_sum_step_result dst_negative_sum_step_result. (((F) = (((((dst_positive_code_step_result) + (dst_positive_scale_step_result)) * S ((dst_positive_code_step_result) + (dst_positive_scale_step_result)) + ((dst_positive_scale_step_result) + (dst_positive_scale_step_result))) + (((dst_negative_code_step_result) + (dst_negative_scale_step_result)) * S ((dst_negative_code_step_result) + (dst_negative_scale_step_result)) + ((dst_negative_scale_step_result) + (dst_negative_scale_step_result)))) * S ((((dst_positive_code_step_result) + (dst_positive_scale_step_result)) * S ((dst_positive_code_step_result) + (dst_positive_scale_step_result)) + ((dst_positive_scale_step_result) + (dst_positive_scale_step_result))) + (((dst_negative_code_step_result) + (dst_negative_scale_step_result)) * S ((dst_negative_code_step_result) + (dst_negative_scale_step_result)) + ((dst_negative_scale_step_result) + (dst_negative_scale_step_result)))) + ((((dst_negative_code_step_result) + (dst_negative_scale_step_result)) * S ((dst_negative_code_step_result) + (dst_negative_scale_step_result)) + ((dst_negative_scale_step_result) + (dst_negative_scale_step_result))) + (((dst_negative_code_step_result) + (dst_negative_scale_step_result)) * S ((dst_negative_code_step_result) + (dst_negative_scale_step_result)) + ((dst_negative_scale_step_result) + (dst_negative_scale_step_result)))))) /\ (((exists fs_u_dst_step_resultpositive fs_v_dst_step_resultpositive. ((((exists fs_h_dst_step_resultpositive_body_start. fs_h_dst_step_resultpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_step_resultpositive)) /\ exists fs_q_dst_step_resultpositive_body_start. fs_u_dst_step_resultpositive = fs_q_dst_step_resultpositive_body_start * S ((S (0)) * fs_v_dst_step_resultpositive) + (0))) /\ ((((exists fs_h_dst_step_resultpositive_body_terminal. fs_h_dst_step_resultpositive_body_terminal + S (dst_positive_sum_step_result) = S ((S (S l)) * fs_v_dst_step_resultpositive)) /\ exists fs_q_dst_step_resultpositive_body_terminal. fs_u_dst_step_resultpositive = fs_q_dst_step_resultpositive_body_terminal * S ((S (S l)) * fs_v_dst_step_resultpositive) + (dst_positive_sum_step_result))) /\ forall fs_i_dst_step_resultpositive_body_steps. (exists fs_lt_dst_step_resultpositive_body_steps_bound. fs_lt_dst_step_resultpositive_body_steps_bound + S fs_i_dst_step_resultpositive_body_steps = S l) -> exists fs_a_dst_step_resultpositive_body_steps fs_r_dst_step_resultpositive_body_steps fs_s_dst_step_resultpositive_body_steps. ((((exists fs_h_dst_step_resultpositive_body_steps_summand. fs_h_dst_step_resultpositive_body_steps_summand + S (fs_a_dst_step_resultpositive_body_steps) = S ((S (fs_i_dst_step_resultpositive_body_steps)) * dst_positive_scale_step_result)) /\ exists fs_q_dst_step_resultpositive_body_steps_summand. dst_positive_code_step_result = fs_q_dst_step_resultpositive_body_steps_summand * S ((S (fs_i_dst_step_resultpositive_body_steps)) * dst_positive_scale_step_result) + (fs_a_dst_step_resultpositive_body_steps))) /\ ((((exists fs_h_dst_step_resultpositive_body_steps_partial. fs_h_dst_step_resultpositive_body_steps_partial + S (fs_r_dst_step_resultpositive_body_steps) = S ((S (fs_i_dst_step_resultpositive_body_steps)) * fs_v_dst_step_resultpositive)) /\ exists fs_q_dst_step_resultpositive_body_steps_partial. fs_u_dst_step_resultpositive = fs_q_dst_step_resultpositive_body_steps_partial * S ((S (fs_i_dst_step_resultpositive_body_steps)) * fs_v_dst_step_resultpositive) + (fs_r_dst_step_resultpositive_body_steps))) /\ ((((exists fs_h_dst_step_resultpositive_body_steps_successor. fs_h_dst_step_resultpositive_body_steps_successor + S (fs_s_dst_step_resultpositive_body_steps) = S ((S (S fs_i_dst_step_resultpositive_body_steps)) * fs_v_dst_step_resultpositive)) /\ exists fs_q_dst_step_resultpositive_body_steps_successor. fs_u_dst_step_resultpositive = fs_q_dst_step_resultpositive_body_steps_successor * S ((S (S fs_i_dst_step_resultpositive_body_steps)) * fs_v_dst_step_resultpositive) + (fs_s_dst_step_resultpositive_body_steps))) /\ fs_s_dst_step_resultpositive_body_steps = fs_r_dst_step_resultpositive_body_steps + fs_a_dst_step_resultpositive_body_steps)))))) /\ (((exists fs_u_dst_step_resultnegative fs_v_dst_step_resultnegative. ((((exists fs_h_dst_step_resultnegative_body_start. fs_h_dst_step_resultnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_step_resultnegative)) /\ exists fs_q_dst_step_resultnegative_body_start. fs_u_dst_step_resultnegative = fs_q_dst_step_resultnegative_body_start * S ((S (0)) * fs_v_dst_step_resultnegative) + (0))) /\ ((((exists fs_h_dst_step_resultnegative_body_terminal. fs_h_dst_step_resultnegative_body_terminal + S (dst_negative_sum_step_result) = S ((S (S l)) * fs_v_dst_step_resultnegative)) /\ exists fs_q_dst_step_resultnegative_body_terminal. fs_u_dst_step_resultnegative = fs_q_dst_step_resultnegative_body_terminal * S ((S (S l)) * fs_v_dst_step_resultnegative) + (dst_negative_sum_step_result))) /\ forall fs_i_dst_step_resultnegative_body_steps. (exists fs_lt_dst_step_resultnegative_body_steps_bound. fs_lt_dst_step_resultnegative_body_steps_bound + S fs_i_dst_step_resultnegative_body_steps = S l) -> exists fs_a_dst_step_resultnegative_body_steps fs_r_dst_step_resultnegative_body_steps fs_s_dst_step_resultnegative_body_steps. ((((exists fs_h_dst_step_resultnegative_body_steps_summand. fs_h_dst_step_resultnegative_body_steps_summand + S (fs_a_dst_step_resultnegative_body_steps) = S ((S (fs_i_dst_step_resultnegative_body_steps)) * dst_negative_scale_step_result)) /\ exists fs_q_dst_step_resultnegative_body_steps_summand. dst_negative_code_step_result = fs_q_dst_step_resultnegative_body_steps_summand * S ((S (fs_i_dst_step_resultnegative_body_steps)) * dst_negative_scale_step_result) + (fs_a_dst_step_resultnegative_body_steps))) /\ ((((exists fs_h_dst_step_resultnegative_body_steps_partial. fs_h_dst_step_resultnegative_body_steps_partial + S (fs_r_dst_step_resultnegative_body_steps) = S ((S (fs_i_dst_step_resultnegative_body_steps)) * fs_v_dst_step_resultnegative)) /\ exists fs_q_dst_step_resultnegative_body_steps_partial. fs_u_dst_step_resultnegative = fs_q_dst_step_resultnegative_body_steps_partial * S ((S (fs_i_dst_step_resultnegative_body_steps)) * fs_v_dst_step_resultnegative) + (fs_r_dst_step_resultnegative_body_steps))) /\ ((((exists fs_h_dst_step_resultnegative_body_steps_successor. fs_h_dst_step_resultnegative_body_steps_successor + S (fs_s_dst_step_resultnegative_body_steps) = S ((S (S fs_i_dst_step_resultnegative_body_steps)) * fs_v_dst_step_resultnegative)) /\ exists fs_q_dst_step_resultnegative_body_steps_successor. fs_u_dst_step_resultnegative = fs_q_dst_step_resultnegative_body_steps_successor * S ((S (S fs_i_dst_step_resultnegative_body_steps)) * fs_v_dst_step_resultnegative) + (fs_s_dst_step_resultnegative_body_steps))) /\ fs_s_dst_step_resultnegative_body_steps = fs_r_dst_step_resultnegative_body_steps + fs_a_dst_step_resultnegative_body_steps)))))) /\ (exists ge_balance_positive_step_resultresult ge_balance_negative_step_resultresult. (((((c) = 2 * (ge_balance_positive_step_resultresult) /\ (ge_balance_negative_step_resultresult) = 0) \/ exists ge_signed_half_step_resultresultdecode. (((c) = 2 * ge_signed_half_step_resultresultdecode + 1 /\ (ge_balance_positive_step_resultresult) = 0) /\ (ge_balance_negative_step_resultresult) = S ge_signed_half_step_resultresultdecode))) /\ ((dst_positive_sum_step_result) + ge_balance_negative_step_resultresult = (dst_negative_sum_step_result) + ge_balance_positive_step_resultresult)))))))))