divisor_signed_sum_negation_transport

Exact expanded first-order arithmetic statement

forall F G pb pc nb nc l a b. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> ((G) = (((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))) * S ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))) + ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))))) -> (exists dst_positive_code_negation_source_sum dst_positive_scale_negation_source_sum dst_negative_code_negation_source_sum dst_negative_scale_negation_source_sum dst_positive_sum_negation_source_sum dst_negative_sum_negation_source_sum. (((F) = (((((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) * S ((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) + ((dst_positive_scale_negation_source_sum) + (dst_positive_scale_negation_source_sum))) + (((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum)))) * S ((((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) * S ((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) + ((dst_positive_scale_negation_source_sum) + (dst_positive_scale_negation_source_sum))) + (((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum)))) + ((((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum))) + (((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum)))))) /\ (((exists fs_u_dst_negation_source_sumpositive fs_v_dst_negation_source_sumpositive. ((((exists fs_h_dst_negation_source_sumpositive_body_start. fs_h_dst_negation_source_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_start. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_start * S ((S (0)) * fs_v_dst_negation_source_sumpositive) + (0))) /\ ((((exists fs_h_dst_negation_source_sumpositive_body_terminal. fs_h_dst_negation_source_sumpositive_body_terminal + S (dst_positive_sum_negation_source_sum) = S ((S (l)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_terminal. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_negation_source_sumpositive) + (dst_positive_sum_negation_source_sum))) /\ forall fs_i_dst_negation_source_sumpositive_body_steps. (exists fs_lt_dst_negation_source_sumpositive_body_steps_bound. fs_lt_dst_negation_source_sumpositive_body_steps_bound + S fs_i_dst_negation_source_sumpositive_body_steps = l) -> exists fs_a_dst_negation_source_sumpositive_body_steps fs_r_dst_negation_source_sumpositive_body_steps fs_s_dst_negation_source_sumpositive_body_steps. ((((exists fs_h_dst_negation_source_sumpositive_body_steps_summand. fs_h_dst_negation_source_sumpositive_body_steps_summand + S (fs_a_dst_negation_source_sumpositive_body_steps) = S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * dst_positive_scale_negation_source_sum)) /\ exists fs_q_dst_negation_source_sumpositive_body_steps_summand. dst_positive_code_negation_source_sum = fs_q_dst_negation_source_sumpositive_body_steps_summand * S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * dst_positive_scale_negation_source_sum) + (fs_a_dst_negation_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumpositive_body_steps_partial. fs_h_dst_negation_source_sumpositive_body_steps_partial + S (fs_r_dst_negation_source_sumpositive_body_steps) = S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_steps_partial. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_steps_partial * S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive) + (fs_r_dst_negation_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumpositive_body_steps_successor. fs_h_dst_negation_source_sumpositive_body_steps_successor + S (fs_s_dst_negation_source_sumpositive_body_steps) = S ((S (S fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_steps_successor. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_steps_successor * S ((S (S fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive) + (fs_s_dst_negation_source_sumpositive_body_steps))) /\ fs_s_dst_negation_source_sumpositive_body_steps = fs_r_dst_negation_source_sumpositive_body_steps + fs_a_dst_negation_source_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_negation_source_sumnegative fs_v_dst_negation_source_sumnegative. ((((exists fs_h_dst_negation_source_sumnegative_body_start. fs_h_dst_negation_source_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_start. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_start * S ((S (0)) * fs_v_dst_negation_source_sumnegative) + (0))) /\ ((((exists fs_h_dst_negation_source_sumnegative_body_terminal. fs_h_dst_negation_source_sumnegative_body_terminal + S (dst_negative_sum_negation_source_sum) = S ((S (l)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_terminal. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_negation_source_sumnegative) + (dst_negative_sum_negation_source_sum))) /\ forall fs_i_dst_negation_source_sumnegative_body_steps. (exists fs_lt_dst_negation_source_sumnegative_body_steps_bound. fs_lt_dst_negation_source_sumnegative_body_steps_bound + S fs_i_dst_negation_source_sumnegative_body_steps = l) -> exists fs_a_dst_negation_source_sumnegative_body_steps fs_r_dst_negation_source_sumnegative_body_steps fs_s_dst_negation_source_sumnegative_body_steps. ((((exists fs_h_dst_negation_source_sumnegative_body_steps_summand. fs_h_dst_negation_source_sumnegative_body_steps_summand + S (fs_a_dst_negation_source_sumnegative_body_steps) = S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * dst_negative_scale_negation_source_sum)) /\ exists fs_q_dst_negation_source_sumnegative_body_steps_summand. dst_negative_code_negation_source_sum = fs_q_dst_negation_source_sumnegative_body_steps_summand * S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * dst_negative_scale_negation_source_sum) + (fs_a_dst_negation_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumnegative_body_steps_partial. fs_h_dst_negation_source_sumnegative_body_steps_partial + S (fs_r_dst_negation_source_sumnegative_body_steps) = S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_steps_partial. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_steps_partial * S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative) + (fs_r_dst_negation_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumnegative_body_steps_successor. fs_h_dst_negation_source_sumnegative_body_steps_successor + S (fs_s_dst_negation_source_sumnegative_body_steps) = S ((S (S fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_steps_successor. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_steps_successor * S ((S (S fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative) + (fs_s_dst_negation_source_sumnegative_body_steps))) /\ fs_s_dst_negation_source_sumnegative_body_steps = fs_r_dst_negation_source_sumnegative_body_steps + fs_a_dst_negation_source_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_negation_source_sumresult ge_balance_negative_negation_source_sumresult. (((((a) = 2 * (ge_balance_positive_negation_source_sumresult) /\ (ge_balance_negative_negation_source_sumresult) = 0) \/ exists ge_signed_half_negation_source_sumresultdecode. (((a) = 2 * ge_signed_half_negation_source_sumresultdecode + 1 /\ (ge_balance_positive_negation_source_sumresult) = 0) /\ (ge_balance_negative_negation_source_sumresult) = S ge_signed_half_negation_source_sumresultdecode))) /\ ((dst_positive_sum_negation_source_sum) + ge_balance_negative_negation_source_sumresult = (dst_negative_sum_negation_source_sum) + ge_balance_positive_negation_source_sumresult))))))))) -> (exists mps_positive_negation_relation mps_negative_negation_relation. (((((a) = 2 * (mps_positive_negation_relation) /\ (mps_negative_negation_relation) = 0) \/ exists ge_signed_half_negation_relationsource. (((a) = 2 * ge_signed_half_negation_relationsource + 1 /\ (mps_positive_negation_relation) = 0) /\ (mps_negative_negation_relation) = S ge_signed_half_negation_relationsource))) /\ ((((b) = 2 * (mps_negative_negation_relation) /\ (mps_positive_negation_relation) = 0) \/ exists ge_signed_half_negation_relationtarget. (((b) = 2 * ge_signed_half_negation_relationtarget + 1 /\ (mps_negative_negation_relation) = 0) /\ (mps_positive_negation_relation) = S ge_signed_half_negation_relationtarget))))) -> (exists dst_positive_code_negation_target_sum dst_positive_scale_negation_target_sum dst_negative_code_negation_target_sum dst_negative_scale_negation_target_sum dst_positive_sum_negation_target_sum dst_negative_sum_negation_target_sum. (((G) = (((((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) * S ((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) + ((dst_positive_scale_negation_target_sum) + (dst_positive_scale_negation_target_sum))) + (((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum)))) * S ((((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) * S ((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) + ((dst_positive_scale_negation_target_sum) + (dst_positive_scale_negation_target_sum))) + (((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum)))) + ((((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum))) + (((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum)))))) /\ (((exists fs_u_dst_negation_target_sumpositive fs_v_dst_negation_target_sumpositive. ((((exists fs_h_dst_negation_target_sumpositive_body_start. fs_h_dst_negation_target_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_start. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_start * S ((S (0)) * fs_v_dst_negation_target_sumpositive) + (0))) /\ ((((exists fs_h_dst_negation_target_sumpositive_body_terminal. fs_h_dst_negation_target_sumpositive_body_terminal + S (dst_positive_sum_negation_target_sum) = S ((S (l)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_terminal. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_negation_target_sumpositive) + (dst_positive_sum_negation_target_sum))) /\ forall fs_i_dst_negation_target_sumpositive_body_steps. (exists fs_lt_dst_negation_target_sumpositive_body_steps_bound. fs_lt_dst_negation_target_sumpositive_body_steps_bound + S fs_i_dst_negation_target_sumpositive_body_steps = l) -> exists fs_a_dst_negation_target_sumpositive_body_steps fs_r_dst_negation_target_sumpositive_body_steps fs_s_dst_negation_target_sumpositive_body_steps. ((((exists fs_h_dst_negation_target_sumpositive_body_steps_summand. fs_h_dst_negation_target_sumpositive_body_steps_summand + S (fs_a_dst_negation_target_sumpositive_body_steps) = S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * dst_positive_scale_negation_target_sum)) /\ exists fs_q_dst_negation_target_sumpositive_body_steps_summand. dst_positive_code_negation_target_sum = fs_q_dst_negation_target_sumpositive_body_steps_summand * S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * dst_positive_scale_negation_target_sum) + (fs_a_dst_negation_target_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumpositive_body_steps_partial. fs_h_dst_negation_target_sumpositive_body_steps_partial + S (fs_r_dst_negation_target_sumpositive_body_steps) = S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_steps_partial. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_steps_partial * S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive) + (fs_r_dst_negation_target_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumpositive_body_steps_successor. fs_h_dst_negation_target_sumpositive_body_steps_successor + S (fs_s_dst_negation_target_sumpositive_body_steps) = S ((S (S fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_steps_successor. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_steps_successor * S ((S (S fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive) + (fs_s_dst_negation_target_sumpositive_body_steps))) /\ fs_s_dst_negation_target_sumpositive_body_steps = fs_r_dst_negation_target_sumpositive_body_steps + fs_a_dst_negation_target_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_negation_target_sumnegative fs_v_dst_negation_target_sumnegative. ((((exists fs_h_dst_negation_target_sumnegative_body_start. fs_h_dst_negation_target_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_start. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_start * S ((S (0)) * fs_v_dst_negation_target_sumnegative) + (0))) /\ ((((exists fs_h_dst_negation_target_sumnegative_body_terminal. fs_h_dst_negation_target_sumnegative_body_terminal + S (dst_negative_sum_negation_target_sum) = S ((S (l)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_terminal. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_negation_target_sumnegative) + (dst_negative_sum_negation_target_sum))) /\ forall fs_i_dst_negation_target_sumnegative_body_steps. (exists fs_lt_dst_negation_target_sumnegative_body_steps_bound. fs_lt_dst_negation_target_sumnegative_body_steps_bound + S fs_i_dst_negation_target_sumnegative_body_steps = l) -> exists fs_a_dst_negation_target_sumnegative_body_steps fs_r_dst_negation_target_sumnegative_body_steps fs_s_dst_negation_target_sumnegative_body_steps. ((((exists fs_h_dst_negation_target_sumnegative_body_steps_summand. fs_h_dst_negation_target_sumnegative_body_steps_summand + S (fs_a_dst_negation_target_sumnegative_body_steps) = S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * dst_negative_scale_negation_target_sum)) /\ exists fs_q_dst_negation_target_sumnegative_body_steps_summand. dst_negative_code_negation_target_sum = fs_q_dst_negation_target_sumnegative_body_steps_summand * S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * dst_negative_scale_negation_target_sum) + (fs_a_dst_negation_target_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumnegative_body_steps_partial. fs_h_dst_negation_target_sumnegative_body_steps_partial + S (fs_r_dst_negation_target_sumnegative_body_steps) = S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_steps_partial. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_steps_partial * S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative) + (fs_r_dst_negation_target_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumnegative_body_steps_successor. fs_h_dst_negation_target_sumnegative_body_steps_successor + S (fs_s_dst_negation_target_sumnegative_body_steps) = S ((S (S fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_steps_successor. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_steps_successor * S ((S (S fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative) + (fs_s_dst_negation_target_sumnegative_body_steps))) /\ fs_s_dst_negation_target_sumnegative_body_steps = fs_r_dst_negation_target_sumnegative_body_steps + fs_a_dst_negation_target_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_negation_target_sumresult ge_balance_negative_negation_target_sumresult. (((((b) = 2 * (ge_balance_positive_negation_target_sumresult) /\ (ge_balance_negative_negation_target_sumresult) = 0) \/ exists ge_signed_half_negation_target_sumresultdecode. (((b) = 2 * ge_signed_half_negation_target_sumresultdecode + 1 /\ (ge_balance_positive_negation_target_sumresult) = 0) /\ (ge_balance_negative_negation_target_sumresult) = S ge_signed_half_negation_target_sumresultdecode))) /\ ((dst_positive_sum_negation_target_sum) + ge_balance_negative_negation_target_sumresult = (dst_negative_sum_negation_target_sum) + ge_balance_positive_negation_target_sumresult)))))))))