dirichlet_unit_at_one_from_value

Exact expanded first-order arithmetic statement

forall F u. (exists dst_positive_code_unit_value_entry dst_positive_scale_unit_value_entry dst_negative_code_unit_value_entry dst_negative_scale_unit_value_entry dst_positive_unit_value_entry dst_negative_unit_value_entry. (((F) = (((((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) * S ((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) + ((dst_positive_scale_unit_value_entry) + (dst_positive_scale_unit_value_entry))) + (((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry)))) * S ((((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) * S ((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) + ((dst_positive_scale_unit_value_entry) + (dst_positive_scale_unit_value_entry))) + (((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry)))) + ((((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry))) + (((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry)))))) /\ (((((exists ff_h_pvs_unit_value_entrypositive. ff_h_pvs_unit_value_entrypositive + S (dst_positive_unit_value_entry) = S ((S (1)) * dst_positive_scale_unit_value_entry)) /\ exists ff_q_pvs_unit_value_entrypositive. dst_positive_code_unit_value_entry = ff_q_pvs_unit_value_entrypositive * S ((S (1)) * dst_positive_scale_unit_value_entry) + (dst_positive_unit_value_entry))) /\ (((((exists ff_h_pvs_unit_value_entrynegative. ff_h_pvs_unit_value_entrynegative + S (dst_negative_unit_value_entry) = S ((S (1)) * dst_negative_scale_unit_value_entry)) /\ exists ff_q_pvs_unit_value_entrynegative. dst_negative_code_unit_value_entry = ff_q_pvs_unit_value_entrynegative * S ((S (1)) * dst_negative_scale_unit_value_entry) + (dst_negative_unit_value_entry))) /\ (exists ge_balance_positive_unit_value_entryvalue ge_balance_negative_unit_value_entryvalue. (((((u) = 2 * (ge_balance_positive_unit_value_entryvalue) /\ (ge_balance_negative_unit_value_entryvalue) = 0) \/ exists ge_signed_half_unit_value_entryvaluedecode. (((u) = 2 * ge_signed_half_unit_value_entryvaluedecode + 1 /\ (ge_balance_positive_unit_value_entryvalue) = 0) /\ (ge_balance_negative_unit_value_entryvalue) = S ge_signed_half_unit_value_entryvaluedecode))) /\ ((dst_positive_unit_value_entry) + ge_balance_negative_unit_value_entryvalue = (dst_negative_unit_value_entry) + ge_balance_positive_unit_value_entryvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> ((exists dst_positive_code_unit_value_resultpositive dst_positive_scale_unit_value_resultpositive dst_negative_code_unit_value_resultpositive dst_negative_scale_unit_value_resultpositive dst_positive_unit_value_resultpositive dst_negative_unit_value_resultpositive. (((F) = (((((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) * S ((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) + ((dst_positive_scale_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive))) + (((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)))) * S ((((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) * S ((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) + ((dst_positive_scale_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive))) + (((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)))) + ((((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive))) + (((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)))))) /\ (((((exists ff_h_pvs_unit_value_resultpositivepositive. ff_h_pvs_unit_value_resultpositivepositive + S (dst_positive_unit_value_resultpositive) = S ((S (1)) * dst_positive_scale_unit_value_resultpositive)) /\ exists ff_q_pvs_unit_value_resultpositivepositive. dst_positive_code_unit_value_resultpositive = ff_q_pvs_unit_value_resultpositivepositive * S ((S (1)) * dst_positive_scale_unit_value_resultpositive) + (dst_positive_unit_value_resultpositive))) /\ (((((exists ff_h_pvs_unit_value_resultpositivenegative. ff_h_pvs_unit_value_resultpositivenegative + S (dst_negative_unit_value_resultpositive) = S ((S (1)) * dst_negative_scale_unit_value_resultpositive)) /\ exists ff_q_pvs_unit_value_resultpositivenegative. dst_negative_code_unit_value_resultpositive = ff_q_pvs_unit_value_resultpositivenegative * S ((S (1)) * dst_negative_scale_unit_value_resultpositive) + (dst_negative_unit_value_resultpositive))) /\ (exists ge_balance_positive_unit_value_resultpositivevalue ge_balance_negative_unit_value_resultpositivevalue. (((((2) = 2 * (ge_balance_positive_unit_value_resultpositivevalue) /\ (ge_balance_negative_unit_value_resultpositivevalue) = 0) \/ exists ge_signed_half_unit_value_resultpositivevaluedecode. (((2) = 2 * ge_signed_half_unit_value_resultpositivevaluedecode + 1 /\ (ge_balance_positive_unit_value_resultpositivevalue) = 0) /\ (ge_balance_negative_unit_value_resultpositivevalue) = S ge_signed_half_unit_value_resultpositivevaluedecode))) /\ ((dst_positive_unit_value_resultpositive) + ge_balance_negative_unit_value_resultpositivevalue = (dst_negative_unit_value_resultpositive) + ge_balance_positive_unit_value_resultpositivevalue))))))))) \/ (exists dst_positive_code_unit_value_resultnegative dst_positive_scale_unit_value_resultnegative dst_negative_code_unit_value_resultnegative dst_negative_scale_unit_value_resultnegative dst_positive_unit_value_resultnegative dst_negative_unit_value_resultnegative. (((F) = (((((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) * S ((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) + ((dst_positive_scale_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative))) + (((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)))) * S ((((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) * S ((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) + ((dst_positive_scale_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative))) + (((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)))) + ((((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative))) + (((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)))))) /\ (((((exists ff_h_pvs_unit_value_resultnegativepositive. ff_h_pvs_unit_value_resultnegativepositive + S (dst_positive_unit_value_resultnegative) = S ((S (1)) * dst_positive_scale_unit_value_resultnegative)) /\ exists ff_q_pvs_unit_value_resultnegativepositive. dst_positive_code_unit_value_resultnegative = ff_q_pvs_unit_value_resultnegativepositive * S ((S (1)) * dst_positive_scale_unit_value_resultnegative) + (dst_positive_unit_value_resultnegative))) /\ (((((exists ff_h_pvs_unit_value_resultnegativenegative. ff_h_pvs_unit_value_resultnegativenegative + S (dst_negative_unit_value_resultnegative) = S ((S (1)) * dst_negative_scale_unit_value_resultnegative)) /\ exists ff_q_pvs_unit_value_resultnegativenegative. dst_negative_code_unit_value_resultnegative = ff_q_pvs_unit_value_resultnegativenegative * S ((S (1)) * dst_negative_scale_unit_value_resultnegative) + (dst_negative_unit_value_resultnegative))) /\ (exists ge_balance_positive_unit_value_resultnegativevalue ge_balance_negative_unit_value_resultnegativevalue. (((((1) = 2 * (ge_balance_positive_unit_value_resultnegativevalue) /\ (ge_balance_negative_unit_value_resultnegativevalue) = 0) \/ exists ge_signed_half_unit_value_resultnegativevaluedecode. (((1) = 2 * ge_signed_half_unit_value_resultnegativevaluedecode + 1 /\ (ge_balance_positive_unit_value_resultnegativevalue) = 0) /\ (ge_balance_negative_unit_value_resultnegativevalue) = S ge_signed_half_unit_value_resultnegativevaluedecode))) /\ ((dst_positive_unit_value_resultnegative) + ge_balance_negative_unit_value_resultnegativevalue = (dst_negative_unit_value_resultnegative) + ge_balance_positive_unit_value_resultnegativevalue))))))))))