dirichlet_convolution_entry_quotient_product

Exact expanded first-order arithmetic statement

forall F G n d q a b z. ~(d=0) -> n=d*q -> (exists dst_positive_code_read_left dst_positive_scale_read_left dst_negative_code_read_left dst_negative_scale_read_left dst_positive_read_left dst_negative_read_left. (((F) = (((((dst_positive_code_read_left) + (dst_positive_scale_read_left)) * S ((dst_positive_code_read_left) + (dst_positive_scale_read_left)) + ((dst_positive_scale_read_left) + (dst_positive_scale_read_left))) + (((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left)))) * S ((((dst_positive_code_read_left) + (dst_positive_scale_read_left)) * S ((dst_positive_code_read_left) + (dst_positive_scale_read_left)) + ((dst_positive_scale_read_left) + (dst_positive_scale_read_left))) + (((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left)))) + ((((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left))) + (((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left)))))) /\ (((((exists ff_h_pvs_read_leftpositive. ff_h_pvs_read_leftpositive + S (dst_positive_read_left) = S ((S (d)) * dst_positive_scale_read_left)) /\ exists ff_q_pvs_read_leftpositive. dst_positive_code_read_left = ff_q_pvs_read_leftpositive * S ((S (d)) * dst_positive_scale_read_left) + (dst_positive_read_left))) /\ (((((exists ff_h_pvs_read_leftnegative. ff_h_pvs_read_leftnegative + S (dst_negative_read_left) = S ((S (d)) * dst_negative_scale_read_left)) /\ exists ff_q_pvs_read_leftnegative. dst_negative_code_read_left = ff_q_pvs_read_leftnegative * S ((S (d)) * dst_negative_scale_read_left) + (dst_negative_read_left))) /\ (exists ge_balance_positive_read_leftvalue ge_balance_negative_read_leftvalue. (((((a) = 2 * (ge_balance_positive_read_leftvalue) /\ (ge_balance_negative_read_leftvalue) = 0) \/ exists ge_signed_half_read_leftvaluedecode. (((a) = 2 * ge_signed_half_read_leftvaluedecode + 1 /\ (ge_balance_positive_read_leftvalue) = 0) /\ (ge_balance_negative_read_leftvalue) = S ge_signed_half_read_leftvaluedecode))) /\ ((dst_positive_read_left) + ge_balance_negative_read_leftvalue = (dst_negative_read_left) + ge_balance_positive_read_leftvalue))))))))) -> (exists dst_positive_code_read_right dst_positive_scale_read_right dst_negative_code_read_right dst_negative_scale_read_right dst_positive_read_right dst_negative_read_right. (((G) = (((((dst_positive_code_read_right) + (dst_positive_scale_read_right)) * S ((dst_positive_code_read_right) + (dst_positive_scale_read_right)) + ((dst_positive_scale_read_right) + (dst_positive_scale_read_right))) + (((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right)))) * S ((((dst_positive_code_read_right) + (dst_positive_scale_read_right)) * S ((dst_positive_code_read_right) + (dst_positive_scale_read_right)) + ((dst_positive_scale_read_right) + (dst_positive_scale_read_right))) + (((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right)))) + ((((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right))) + (((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right)))))) /\ (((((exists ff_h_pvs_read_rightpositive. ff_h_pvs_read_rightpositive + S (dst_positive_read_right) = S ((S (q)) * dst_positive_scale_read_right)) /\ exists ff_q_pvs_read_rightpositive. dst_positive_code_read_right = ff_q_pvs_read_rightpositive * S ((S (q)) * dst_positive_scale_read_right) + (dst_positive_read_right))) /\ (((((exists ff_h_pvs_read_rightnegative. ff_h_pvs_read_rightnegative + S (dst_negative_read_right) = S ((S (q)) * dst_negative_scale_read_right)) /\ exists ff_q_pvs_read_rightnegative. dst_negative_code_read_right = ff_q_pvs_read_rightnegative * S ((S (q)) * dst_negative_scale_read_right) + (dst_negative_read_right))) /\ (exists ge_balance_positive_read_rightvalue ge_balance_negative_read_rightvalue. (((((b) = 2 * (ge_balance_positive_read_rightvalue) /\ (ge_balance_negative_read_rightvalue) = 0) \/ exists ge_signed_half_read_rightvaluedecode. (((b) = 2 * ge_signed_half_read_rightvaluedecode + 1 /\ (ge_balance_positive_read_rightvalue) = 0) /\ (ge_balance_negative_read_rightvalue) = S ge_signed_half_read_rightvaluedecode))) /\ ((dst_positive_read_right) + ge_balance_negative_read_rightvalue = (dst_negative_read_right) + ge_balance_positive_read_rightvalue))))))))) -> ((((~((d)=0)) /\ (exists dc_quotient_read_entry dc_left_read_entry dc_right_read_entry. (((n)=(d)*dc_quotient_read_entry) /\ (((exists dst_positive_code_read_entryleft dst_positive_scale_read_entryleft dst_negative_code_read_entryleft dst_negative_scale_read_entryleft dst_positive_read_entryleft dst_negative_read_entryleft. (((F) = (((((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) * S ((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) + ((dst_positive_scale_read_entryleft) + (dst_positive_scale_read_entryleft))) + (((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft)))) * S ((((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) * S ((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) + ((dst_positive_scale_read_entryleft) + (dst_positive_scale_read_entryleft))) + (((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft)))) + ((((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft))) + (((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft)))))) /\ (((((exists ff_h_pvs_read_entryleftpositive. ff_h_pvs_read_entryleftpositive + S (dst_positive_read_entryleft) = S ((S (d)) * dst_positive_scale_read_entryleft)) /\ exists ff_q_pvs_read_entryleftpositive. dst_positive_code_read_entryleft = ff_q_pvs_read_entryleftpositive * S ((S (d)) * dst_positive_scale_read_entryleft) + (dst_positive_read_entryleft))) /\ (((((exists ff_h_pvs_read_entryleftnegative. ff_h_pvs_read_entryleftnegative + S (dst_negative_read_entryleft) = S ((S (d)) * dst_negative_scale_read_entryleft)) /\ exists ff_q_pvs_read_entryleftnegative. dst_negative_code_read_entryleft = ff_q_pvs_read_entryleftnegative * S ((S (d)) * dst_negative_scale_read_entryleft) + (dst_negative_read_entryleft))) /\ (exists ge_balance_positive_read_entryleftvalue ge_balance_negative_read_entryleftvalue. (((((dc_left_read_entry) = 2 * (ge_balance_positive_read_entryleftvalue) /\ (ge_balance_negative_read_entryleftvalue) = 0) \/ exists ge_signed_half_read_entryleftvaluedecode. (((dc_left_read_entry) = 2 * ge_signed_half_read_entryleftvaluedecode + 1 /\ (ge_balance_positive_read_entryleftvalue) = 0) /\ (ge_balance_negative_read_entryleftvalue) = S ge_signed_half_read_entryleftvaluedecode))) /\ ((dst_positive_read_entryleft) + ge_balance_negative_read_entryleftvalue = (dst_negative_read_entryleft) + ge_balance_positive_read_entryleftvalue))))))))) /\ (((exists dst_positive_code_read_entryright dst_positive_scale_read_entryright dst_negative_code_read_entryright dst_negative_scale_read_entryright dst_positive_read_entryright dst_negative_read_entryright. (((G) = (((((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) * S ((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) + ((dst_positive_scale_read_entryright) + (dst_positive_scale_read_entryright))) + (((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright)))) * S ((((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) * S ((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) + ((dst_positive_scale_read_entryright) + (dst_positive_scale_read_entryright))) + (((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright)))) + ((((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright))) + (((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright)))))) /\ (((((exists ff_h_pvs_read_entryrightpositive. ff_h_pvs_read_entryrightpositive + S (dst_positive_read_entryright) = S ((S (dc_quotient_read_entry)) * dst_positive_scale_read_entryright)) /\ exists ff_q_pvs_read_entryrightpositive. dst_positive_code_read_entryright = ff_q_pvs_read_entryrightpositive * S ((S (dc_quotient_read_entry)) * dst_positive_scale_read_entryright) + (dst_positive_read_entryright))) /\ (((((exists ff_h_pvs_read_entryrightnegative. ff_h_pvs_read_entryrightnegative + S (dst_negative_read_entryright) = S ((S (dc_quotient_read_entry)) * dst_negative_scale_read_entryright)) /\ exists ff_q_pvs_read_entryrightnegative. dst_negative_code_read_entryright = ff_q_pvs_read_entryrightnegative * S ((S (dc_quotient_read_entry)) * dst_negative_scale_read_entryright) + (dst_negative_read_entryright))) /\ (exists ge_balance_positive_read_entryrightvalue ge_balance_negative_read_entryrightvalue. (((((dc_right_read_entry) = 2 * (ge_balance_positive_read_entryrightvalue) /\ (ge_balance_negative_read_entryrightvalue) = 0) \/ exists ge_signed_half_read_entryrightvaluedecode. (((dc_right_read_entry) = 2 * ge_signed_half_read_entryrightvaluedecode + 1 /\ (ge_balance_positive_read_entryrightvalue) = 0) /\ (ge_balance_negative_read_entryrightvalue) = S ge_signed_half_read_entryrightvaluedecode))) /\ ((dst_positive_read_entryright) + ge_balance_negative_read_entryrightvalue = (dst_negative_read_entryright) + ge_balance_positive_read_entryrightvalue))))))))) /\ (exists sto_ap_read_entryproduct sto_an_read_entryproduct sto_bp_read_entryproduct sto_bn_read_entryproduct sto_cp_read_entryproduct sto_cn_read_entryproduct. (((((dc_left_read_entry) = 2 * (sto_ap_read_entryproduct) /\ (sto_an_read_entryproduct) = 0) \/ exists ge_signed_half_read_entryproductleft. (((dc_left_read_entry) = 2 * ge_signed_half_read_entryproductleft + 1 /\ (sto_ap_read_entryproduct) = 0) /\ (sto_an_read_entryproduct) = S ge_signed_half_read_entryproductleft))) /\ ((((((dc_right_read_entry) = 2 * (sto_bp_read_entryproduct) /\ (sto_bn_read_entryproduct) = 0) \/ exists ge_signed_half_read_entryproductright. (((dc_right_read_entry) = 2 * ge_signed_half_read_entryproductright + 1 /\ (sto_bp_read_entryproduct) = 0) /\ (sto_bn_read_entryproduct) = S ge_signed_half_read_entryproductright))) /\ ((((((z) = 2 * (sto_cp_read_entryproduct) /\ (sto_cn_read_entryproduct) = 0) \/ exists ge_signed_half_read_entryproductoutput. (((z) = 2 * ge_signed_half_read_entryproductoutput + 1 /\ (sto_cp_read_entryproduct) = 0) /\ (sto_cn_read_entryproduct) = S ge_signed_half_read_entryproductoutput))) /\ ((sto_ap_read_entryproduct * sto_bp_read_entryproduct + sto_an_read_entryproduct * sto_bn_read_entryproduct) + sto_cn_read_entryproduct = (sto_ap_read_entryproduct * sto_bn_read_entryproduct + sto_an_read_entryproduct * sto_bp_read_entryproduct) + sto_cp_read_entryproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_read_entrynondivisor. (n) = (d) * pvs_factor_read_entrynondivisor)) /\ ((z)=0)))) -> (exists sto_ap_read_product sto_an_read_product sto_bp_read_product sto_bn_read_product sto_cp_read_product sto_cn_read_product. (((((a) = 2 * (sto_ap_read_product) /\ (sto_an_read_product) = 0) \/ exists ge_signed_half_read_productleft. (((a) = 2 * ge_signed_half_read_productleft + 1 /\ (sto_ap_read_product) = 0) /\ (sto_an_read_product) = S ge_signed_half_read_productleft))) /\ ((((((b) = 2 * (sto_bp_read_product) /\ (sto_bn_read_product) = 0) \/ exists ge_signed_half_read_productright. (((b) = 2 * ge_signed_half_read_productright + 1 /\ (sto_bp_read_product) = 0) /\ (sto_bn_read_product) = S ge_signed_half_read_productright))) /\ ((((((z) = 2 * (sto_cp_read_product) /\ (sto_cn_read_product) = 0) \/ exists ge_signed_half_read_productoutput. (((z) = 2 * ge_signed_half_read_productoutput + 1 /\ (sto_cp_read_product) = 0) /\ (sto_cn_read_product) = S ge_signed_half_read_productoutput))) /\ ((sto_ap_read_product * sto_bp_read_product + sto_an_read_product * sto_bn_read_product) + sto_cn_read_product = (sto_ap_read_product * sto_bn_read_product + sto_an_read_product * sto_bp_read_product) + sto_cp_read_product)))))))