dirichlet_convolution_last_entry_iff

Exact expanded first-order arithmetic statement

forall F G n a b z. ~(n=0) -> (exists dst_positive_code_endpoint_first dst_positive_scale_endpoint_first dst_negative_code_endpoint_first dst_negative_scale_endpoint_first dst_positive_endpoint_first dst_negative_endpoint_first. (((F) = (((((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) * S ((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) + ((dst_positive_scale_endpoint_first) + (dst_positive_scale_endpoint_first))) + (((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first)))) * S ((((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) * S ((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) + ((dst_positive_scale_endpoint_first) + (dst_positive_scale_endpoint_first))) + (((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first)))) + ((((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first))) + (((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first)))))) /\ (((((exists ff_h_pvs_endpoint_firstpositive. ff_h_pvs_endpoint_firstpositive + S (dst_positive_endpoint_first) = S ((S (n)) * dst_positive_scale_endpoint_first)) /\ exists ff_q_pvs_endpoint_firstpositive. dst_positive_code_endpoint_first = ff_q_pvs_endpoint_firstpositive * S ((S (n)) * dst_positive_scale_endpoint_first) + (dst_positive_endpoint_first))) /\ (((((exists ff_h_pvs_endpoint_firstnegative. ff_h_pvs_endpoint_firstnegative + S (dst_negative_endpoint_first) = S ((S (n)) * dst_negative_scale_endpoint_first)) /\ exists ff_q_pvs_endpoint_firstnegative. dst_negative_code_endpoint_first = ff_q_pvs_endpoint_firstnegative * S ((S (n)) * dst_negative_scale_endpoint_first) + (dst_negative_endpoint_first))) /\ (exists ge_balance_positive_endpoint_firstvalue ge_balance_negative_endpoint_firstvalue. (((((a) = 2 * (ge_balance_positive_endpoint_firstvalue) /\ (ge_balance_negative_endpoint_firstvalue) = 0) \/ exists ge_signed_half_endpoint_firstvaluedecode. (((a) = 2 * ge_signed_half_endpoint_firstvaluedecode + 1 /\ (ge_balance_positive_endpoint_firstvalue) = 0) /\ (ge_balance_negative_endpoint_firstvalue) = S ge_signed_half_endpoint_firstvaluedecode))) /\ ((dst_positive_endpoint_first) + ge_balance_negative_endpoint_firstvalue = (dst_negative_endpoint_first) + ge_balance_positive_endpoint_firstvalue))))))))) -> (exists dst_positive_code_endpoint_second dst_positive_scale_endpoint_second dst_negative_code_endpoint_second dst_negative_scale_endpoint_second dst_positive_endpoint_second dst_negative_endpoint_second. (((G) = (((((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) * S ((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) + ((dst_positive_scale_endpoint_second) + (dst_positive_scale_endpoint_second))) + (((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second)))) * S ((((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) * S ((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) + ((dst_positive_scale_endpoint_second) + (dst_positive_scale_endpoint_second))) + (((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second)))) + ((((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second))) + (((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second)))))) /\ (((((exists ff_h_pvs_endpoint_secondpositive. ff_h_pvs_endpoint_secondpositive + S (dst_positive_endpoint_second) = S ((S (1)) * dst_positive_scale_endpoint_second)) /\ exists ff_q_pvs_endpoint_secondpositive. dst_positive_code_endpoint_second = ff_q_pvs_endpoint_secondpositive * S ((S (1)) * dst_positive_scale_endpoint_second) + (dst_positive_endpoint_second))) /\ (((((exists ff_h_pvs_endpoint_secondnegative. ff_h_pvs_endpoint_secondnegative + S (dst_negative_endpoint_second) = S ((S (1)) * dst_negative_scale_endpoint_second)) /\ exists ff_q_pvs_endpoint_secondnegative. dst_negative_code_endpoint_second = ff_q_pvs_endpoint_secondnegative * S ((S (1)) * dst_negative_scale_endpoint_second) + (dst_negative_endpoint_second))) /\ (exists ge_balance_positive_endpoint_secondvalue ge_balance_negative_endpoint_secondvalue. (((((b) = 2 * (ge_balance_positive_endpoint_secondvalue) /\ (ge_balance_negative_endpoint_secondvalue) = 0) \/ exists ge_signed_half_endpoint_secondvaluedecode. (((b) = 2 * ge_signed_half_endpoint_secondvaluedecode + 1 /\ (ge_balance_positive_endpoint_secondvalue) = 0) /\ (ge_balance_negative_endpoint_secondvalue) = S ge_signed_half_endpoint_secondvaluedecode))) /\ ((dst_positive_endpoint_second) + ge_balance_negative_endpoint_secondvalue = (dst_negative_endpoint_second) + ge_balance_positive_endpoint_secondvalue))))))))) -> ((((((~((n)=0)) /\ (exists dc_quotient_endpoint_summand dc_left_endpoint_summand dc_right_endpoint_summand. (((n)=(n)*dc_quotient_endpoint_summand) /\ (((exists dst_positive_code_endpoint_summandleft dst_positive_scale_endpoint_summandleft dst_negative_code_endpoint_summandleft dst_negative_scale_endpoint_summandleft dst_positive_endpoint_summandleft dst_negative_endpoint_summandleft. (((F) = (((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) * S ((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) + ((((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))))) /\ (((((exists ff_h_pvs_endpoint_summandleftpositive. ff_h_pvs_endpoint_summandleftpositive + S (dst_positive_endpoint_summandleft) = S ((S (n)) * dst_positive_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftpositive. dst_positive_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftpositive * S ((S (n)) * dst_positive_scale_endpoint_summandleft) + (dst_positive_endpoint_summandleft))) /\ (((((exists ff_h_pvs_endpoint_summandleftnegative. ff_h_pvs_endpoint_summandleftnegative + S (dst_negative_endpoint_summandleft) = S ((S (n)) * dst_negative_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftnegative. dst_negative_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftnegative * S ((S (n)) * dst_negative_scale_endpoint_summandleft) + (dst_negative_endpoint_summandleft))) /\ (exists ge_balance_positive_endpoint_summandleftvalue ge_balance_negative_endpoint_summandleftvalue. (((((dc_left_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandleftvalue) /\ (ge_balance_negative_endpoint_summandleftvalue) = 0) \/ exists ge_signed_half_endpoint_summandleftvaluedecode. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandleftvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandleftvalue) = 0) /\ (ge_balance_negative_endpoint_summandleftvalue) = S ge_signed_half_endpoint_summandleftvaluedecode))) /\ ((dst_positive_endpoint_summandleft) + ge_balance_negative_endpoint_summandleftvalue = (dst_negative_endpoint_summandleft) + ge_balance_positive_endpoint_summandleftvalue))))))))) /\ (((exists dst_positive_code_endpoint_summandright dst_positive_scale_endpoint_summandright dst_negative_code_endpoint_summandright dst_negative_scale_endpoint_summandright dst_positive_endpoint_summandright dst_negative_endpoint_summandright. (((G) = (((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) * S ((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) + ((((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))))) /\ (((((exists ff_h_pvs_endpoint_summandrightpositive. ff_h_pvs_endpoint_summandrightpositive + S (dst_positive_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightpositive. dst_positive_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightpositive * S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright) + (dst_positive_endpoint_summandright))) /\ (((((exists ff_h_pvs_endpoint_summandrightnegative. ff_h_pvs_endpoint_summandrightnegative + S (dst_negative_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightnegative. dst_negative_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightnegative * S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright) + (dst_negative_endpoint_summandright))) /\ (exists ge_balance_positive_endpoint_summandrightvalue ge_balance_negative_endpoint_summandrightvalue. (((((dc_right_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandrightvalue) /\ (ge_balance_negative_endpoint_summandrightvalue) = 0) \/ exists ge_signed_half_endpoint_summandrightvaluedecode. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandrightvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandrightvalue) = 0) /\ (ge_balance_negative_endpoint_summandrightvalue) = S ge_signed_half_endpoint_summandrightvaluedecode))) /\ ((dst_positive_endpoint_summandright) + ge_balance_negative_endpoint_summandrightvalue = (dst_negative_endpoint_summandright) + ge_balance_positive_endpoint_summandrightvalue))))))))) /\ (exists sto_ap_endpoint_summandproduct sto_an_endpoint_summandproduct sto_bp_endpoint_summandproduct sto_bn_endpoint_summandproduct sto_cp_endpoint_summandproduct sto_cn_endpoint_summandproduct. (((((dc_left_endpoint_summand) = 2 * (sto_ap_endpoint_summandproduct) /\ (sto_an_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductleft. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductleft + 1 /\ (sto_ap_endpoint_summandproduct) = 0) /\ (sto_an_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductleft))) /\ ((((((dc_right_endpoint_summand) = 2 * (sto_bp_endpoint_summandproduct) /\ (sto_bn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductright. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductright + 1 /\ (sto_bp_endpoint_summandproduct) = 0) /\ (sto_bn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductright))) /\ ((((((z) = 2 * (sto_cp_endpoint_summandproduct) /\ (sto_cn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductoutput. (((z) = 2 * ge_signed_half_endpoint_summandproductoutput + 1 /\ (sto_cp_endpoint_summandproduct) = 0) /\ (sto_cn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductoutput))) /\ ((sto_ap_endpoint_summandproduct * sto_bp_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bn_endpoint_summandproduct) + sto_cn_endpoint_summandproduct = (sto_ap_endpoint_summandproduct * sto_bn_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bp_endpoint_summandproduct) + sto_cp_endpoint_summandproduct))))))))))))))) \/ ((((n)=0 \/ ~(exists pvs_factor_endpoint_summandnondivisor. (n) = (n) * pvs_factor_endpoint_summandnondivisor)) /\ ((z)=0)))) -> (exists sto_ap_endpoint_product sto_an_endpoint_product sto_bp_endpoint_product sto_bn_endpoint_product sto_cp_endpoint_product sto_cn_endpoint_product. (((((a) = 2 * (sto_ap_endpoint_product) /\ (sto_an_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productleft. (((a) = 2 * ge_signed_half_endpoint_productleft + 1 /\ (sto_ap_endpoint_product) = 0) /\ (sto_an_endpoint_product) = S ge_signed_half_endpoint_productleft))) /\ ((((((b) = 2 * (sto_bp_endpoint_product) /\ (sto_bn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productright. (((b) = 2 * ge_signed_half_endpoint_productright + 1 /\ (sto_bp_endpoint_product) = 0) /\ (sto_bn_endpoint_product) = S ge_signed_half_endpoint_productright))) /\ ((((((z) = 2 * (sto_cp_endpoint_product) /\ (sto_cn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productoutput. (((z) = 2 * ge_signed_half_endpoint_productoutput + 1 /\ (sto_cp_endpoint_product) = 0) /\ (sto_cn_endpoint_product) = S ge_signed_half_endpoint_productoutput))) /\ ((sto_ap_endpoint_product * sto_bp_endpoint_product + sto_an_endpoint_product * sto_bn_endpoint_product) + sto_cn_endpoint_product = (sto_ap_endpoint_product * sto_bn_endpoint_product + sto_an_endpoint_product * sto_bp_endpoint_product) + sto_cp_endpoint_product)))))))) /\ ((exists sto_ap_endpoint_product sto_an_endpoint_product sto_bp_endpoint_product sto_bn_endpoint_product sto_cp_endpoint_product sto_cn_endpoint_product. (((((a) = 2 * (sto_ap_endpoint_product) /\ (sto_an_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productleft. (((a) = 2 * ge_signed_half_endpoint_productleft + 1 /\ (sto_ap_endpoint_product) = 0) /\ (sto_an_endpoint_product) = S ge_signed_half_endpoint_productleft))) /\ ((((((b) = 2 * (sto_bp_endpoint_product) /\ (sto_bn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productright. (((b) = 2 * ge_signed_half_endpoint_productright + 1 /\ (sto_bp_endpoint_product) = 0) /\ (sto_bn_endpoint_product) = S ge_signed_half_endpoint_productright))) /\ ((((((z) = 2 * (sto_cp_endpoint_product) /\ (sto_cn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productoutput. (((z) = 2 * ge_signed_half_endpoint_productoutput + 1 /\ (sto_cp_endpoint_product) = 0) /\ (sto_cn_endpoint_product) = S ge_signed_half_endpoint_productoutput))) /\ ((sto_ap_endpoint_product * sto_bp_endpoint_product + sto_an_endpoint_product * sto_bn_endpoint_product) + sto_cn_endpoint_product = (sto_ap_endpoint_product * sto_bn_endpoint_product + sto_an_endpoint_product * sto_bp_endpoint_product) + sto_cp_endpoint_product))))))) -> ((((~((n)=0)) /\ (exists dc_quotient_endpoint_summand dc_left_endpoint_summand dc_right_endpoint_summand. (((n)=(n)*dc_quotient_endpoint_summand) /\ (((exists dst_positive_code_endpoint_summandleft dst_positive_scale_endpoint_summandleft dst_negative_code_endpoint_summandleft dst_negative_scale_endpoint_summandleft dst_positive_endpoint_summandleft dst_negative_endpoint_summandleft. (((F) = (((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) * S ((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) + ((((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))))) /\ (((((exists ff_h_pvs_endpoint_summandleftpositive. ff_h_pvs_endpoint_summandleftpositive + S (dst_positive_endpoint_summandleft) = S ((S (n)) * dst_positive_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftpositive. dst_positive_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftpositive * S ((S (n)) * dst_positive_scale_endpoint_summandleft) + (dst_positive_endpoint_summandleft))) /\ (((((exists ff_h_pvs_endpoint_summandleftnegative. ff_h_pvs_endpoint_summandleftnegative + S (dst_negative_endpoint_summandleft) = S ((S (n)) * dst_negative_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftnegative. dst_negative_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftnegative * S ((S (n)) * dst_negative_scale_endpoint_summandleft) + (dst_negative_endpoint_summandleft))) /\ (exists ge_balance_positive_endpoint_summandleftvalue ge_balance_negative_endpoint_summandleftvalue. (((((dc_left_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandleftvalue) /\ (ge_balance_negative_endpoint_summandleftvalue) = 0) \/ exists ge_signed_half_endpoint_summandleftvaluedecode. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandleftvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandleftvalue) = 0) /\ (ge_balance_negative_endpoint_summandleftvalue) = S ge_signed_half_endpoint_summandleftvaluedecode))) /\ ((dst_positive_endpoint_summandleft) + ge_balance_negative_endpoint_summandleftvalue = (dst_negative_endpoint_summandleft) + ge_balance_positive_endpoint_summandleftvalue))))))))) /\ (((exists dst_positive_code_endpoint_summandright dst_positive_scale_endpoint_summandright dst_negative_code_endpoint_summandright dst_negative_scale_endpoint_summandright dst_positive_endpoint_summandright dst_negative_endpoint_summandright. (((G) = (((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) * S ((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) + ((((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))))) /\ (((((exists ff_h_pvs_endpoint_summandrightpositive. ff_h_pvs_endpoint_summandrightpositive + S (dst_positive_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightpositive. dst_positive_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightpositive * S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright) + (dst_positive_endpoint_summandright))) /\ (((((exists ff_h_pvs_endpoint_summandrightnegative. ff_h_pvs_endpoint_summandrightnegative + S (dst_negative_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightnegative. dst_negative_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightnegative * S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright) + (dst_negative_endpoint_summandright))) /\ (exists ge_balance_positive_endpoint_summandrightvalue ge_balance_negative_endpoint_summandrightvalue. (((((dc_right_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandrightvalue) /\ (ge_balance_negative_endpoint_summandrightvalue) = 0) \/ exists ge_signed_half_endpoint_summandrightvaluedecode. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandrightvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandrightvalue) = 0) /\ (ge_balance_negative_endpoint_summandrightvalue) = S ge_signed_half_endpoint_summandrightvaluedecode))) /\ ((dst_positive_endpoint_summandright) + ge_balance_negative_endpoint_summandrightvalue = (dst_negative_endpoint_summandright) + ge_balance_positive_endpoint_summandrightvalue))))))))) /\ (exists sto_ap_endpoint_summandproduct sto_an_endpoint_summandproduct sto_bp_endpoint_summandproduct sto_bn_endpoint_summandproduct sto_cp_endpoint_summandproduct sto_cn_endpoint_summandproduct. (((((dc_left_endpoint_summand) = 2 * (sto_ap_endpoint_summandproduct) /\ (sto_an_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductleft. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductleft + 1 /\ (sto_ap_endpoint_summandproduct) = 0) /\ (sto_an_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductleft))) /\ ((((((dc_right_endpoint_summand) = 2 * (sto_bp_endpoint_summandproduct) /\ (sto_bn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductright. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductright + 1 /\ (sto_bp_endpoint_summandproduct) = 0) /\ (sto_bn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductright))) /\ ((((((z) = 2 * (sto_cp_endpoint_summandproduct) /\ (sto_cn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductoutput. (((z) = 2 * ge_signed_half_endpoint_summandproductoutput + 1 /\ (sto_cp_endpoint_summandproduct) = 0) /\ (sto_cn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductoutput))) /\ ((sto_ap_endpoint_summandproduct * sto_bp_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bn_endpoint_summandproduct) + sto_cn_endpoint_summandproduct = (sto_ap_endpoint_summandproduct * sto_bn_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bp_endpoint_summandproduct) + sto_cp_endpoint_summandproduct))))))))))))))) \/ ((((n)=0 \/ ~(exists pvs_factor_endpoint_summandnondivisor. (n) = (n) * pvs_factor_endpoint_summandnondivisor)) /\ ((z)=0))))))