signed_support_incidence_nonzero_source_image

Exact expanded first-order arithmetic statement

forall A r s i j z. (exists ssr_entry_value_nonzero_entry ssr_entry_image_nonzero_entry. ((exists dst_positive_code_nonzero_entrysource dst_positive_scale_nonzero_entrysource dst_negative_code_nonzero_entrysource dst_negative_scale_nonzero_entrysource dst_positive_nonzero_entrysource dst_negative_nonzero_entrysource. (((A) = (((((dst_positive_code_nonzero_entrysource) + (dst_positive_scale_nonzero_entrysource)) * S ((dst_positive_code_nonzero_entrysource) + (dst_positive_scale_nonzero_entrysource)) + ((dst_positive_scale_nonzero_entrysource) + (dst_positive_scale_nonzero_entrysource))) + (((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) * S ((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) + ((dst_negative_scale_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)))) * S ((((dst_positive_code_nonzero_entrysource) + (dst_positive_scale_nonzero_entrysource)) * S ((dst_positive_code_nonzero_entrysource) + (dst_positive_scale_nonzero_entrysource)) + ((dst_positive_scale_nonzero_entrysource) + (dst_positive_scale_nonzero_entrysource))) + (((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) * S ((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) + ((dst_negative_scale_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)))) + ((((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) * S ((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) + ((dst_negative_scale_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource))) + (((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) * S ((dst_negative_code_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)) + ((dst_negative_scale_nonzero_entrysource) + (dst_negative_scale_nonzero_entrysource)))))) /\ (((((exists ff_h_pvs_nonzero_entrysourcepositive. ff_h_pvs_nonzero_entrysourcepositive + S (dst_positive_nonzero_entrysource) = S ((S (i)) * dst_positive_scale_nonzero_entrysource)) /\ exists ff_q_pvs_nonzero_entrysourcepositive. dst_positive_code_nonzero_entrysource = ff_q_pvs_nonzero_entrysourcepositive * S ((S (i)) * dst_positive_scale_nonzero_entrysource) + (dst_positive_nonzero_entrysource))) /\ (((((exists ff_h_pvs_nonzero_entrysourcenegative. ff_h_pvs_nonzero_entrysourcenegative + S (dst_negative_nonzero_entrysource) = S ((S (i)) * dst_negative_scale_nonzero_entrysource)) /\ exists ff_q_pvs_nonzero_entrysourcenegative. dst_negative_code_nonzero_entrysource = ff_q_pvs_nonzero_entrysourcenegative * S ((S (i)) * dst_negative_scale_nonzero_entrysource) + (dst_negative_nonzero_entrysource))) /\ (exists ge_balance_positive_nonzero_entrysourcevalue ge_balance_negative_nonzero_entrysourcevalue. (((((ssr_entry_value_nonzero_entry) = 2 * (ge_balance_positive_nonzero_entrysourcevalue) /\ (ge_balance_negative_nonzero_entrysourcevalue) = 0) \/ exists ge_signed_half_nonzero_entrysourcevaluedecode. (((ssr_entry_value_nonzero_entry) = 2 * ge_signed_half_nonzero_entrysourcevaluedecode + 1 /\ (ge_balance_positive_nonzero_entrysourcevalue) = 0) /\ (ge_balance_negative_nonzero_entrysourcevalue) = S ge_signed_half_nonzero_entrysourcevaluedecode))) /\ ((dst_positive_nonzero_entrysource) + ge_balance_negative_nonzero_entrysourcevalue = (dst_negative_nonzero_entrysource) + ge_balance_positive_nonzero_entrysourcevalue))))))))) /\ (((((exists ff_h_pvs_nonzero_entrymap. ff_h_pvs_nonzero_entrymap + S (ssr_entry_image_nonzero_entry) = S ((S (i)) * s)) /\ exists ff_q_pvs_nonzero_entrymap. r = ff_q_pvs_nonzero_entrymap * S ((S (i)) * s) + (ssr_entry_image_nonzero_entry))) /\ (((((j)=(ssr_entry_image_nonzero_entry)) /\ ((z)=(ssr_entry_value_nonzero_entry)))) \/ (((~((j)=(ssr_entry_image_nonzero_entry))) /\ ((z)=0)))))))) -> ~(z=0) -> ((exists dst_positive_code_nonzero_source dst_positive_scale_nonzero_source dst_negative_code_nonzero_source dst_negative_scale_nonzero_source dst_positive_nonzero_source dst_negative_nonzero_source. (((A) = (((((dst_positive_code_nonzero_source) + (dst_positive_scale_nonzero_source)) * S ((dst_positive_code_nonzero_source) + (dst_positive_scale_nonzero_source)) + ((dst_positive_scale_nonzero_source) + (dst_positive_scale_nonzero_source))) + (((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) * S ((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) + ((dst_negative_scale_nonzero_source) + (dst_negative_scale_nonzero_source)))) * S ((((dst_positive_code_nonzero_source) + (dst_positive_scale_nonzero_source)) * S ((dst_positive_code_nonzero_source) + (dst_positive_scale_nonzero_source)) + ((dst_positive_scale_nonzero_source) + (dst_positive_scale_nonzero_source))) + (((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) * S ((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) + ((dst_negative_scale_nonzero_source) + (dst_negative_scale_nonzero_source)))) + ((((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) * S ((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) + ((dst_negative_scale_nonzero_source) + (dst_negative_scale_nonzero_source))) + (((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) * S ((dst_negative_code_nonzero_source) + (dst_negative_scale_nonzero_source)) + ((dst_negative_scale_nonzero_source) + (dst_negative_scale_nonzero_source)))))) /\ (((((exists ff_h_pvs_nonzero_sourcepositive. ff_h_pvs_nonzero_sourcepositive + S (dst_positive_nonzero_source) = S ((S (i)) * dst_positive_scale_nonzero_source)) /\ exists ff_q_pvs_nonzero_sourcepositive. dst_positive_code_nonzero_source = ff_q_pvs_nonzero_sourcepositive * S ((S (i)) * dst_positive_scale_nonzero_source) + (dst_positive_nonzero_source))) /\ (((((exists ff_h_pvs_nonzero_sourcenegative. ff_h_pvs_nonzero_sourcenegative + S (dst_negative_nonzero_source) = S ((S (i)) * dst_negative_scale_nonzero_source)) /\ exists ff_q_pvs_nonzero_sourcenegative. dst_negative_code_nonzero_source = ff_q_pvs_nonzero_sourcenegative * S ((S (i)) * dst_negative_scale_nonzero_source) + (dst_negative_nonzero_source))) /\ (exists ge_balance_positive_nonzero_sourcevalue ge_balance_negative_nonzero_sourcevalue. (((((z) = 2 * (ge_balance_positive_nonzero_sourcevalue) /\ (ge_balance_negative_nonzero_sourcevalue) = 0) \/ exists ge_signed_half_nonzero_sourcevaluedecode. (((z) = 2 * ge_signed_half_nonzero_sourcevaluedecode + 1 /\ (ge_balance_positive_nonzero_sourcevalue) = 0) /\ (ge_balance_negative_nonzero_sourcevalue) = S ge_signed_half_nonzero_sourcevaluedecode))) /\ ((dst_positive_nonzero_source) + ge_balance_negative_nonzero_sourcevalue = (dst_negative_nonzero_source) + ge_balance_positive_nonzero_sourcevalue))))))))) /\ (((exists ff_h_pvs_nonzero_map. ff_h_pvs_nonzero_map + S (j) = S ((S (i)) * s)) /\ exists ff_q_pvs_nonzero_map. r = ff_q_pvs_nonzero_map * S ((S (i)) * s) + (j))))