dirichlet_constant_one_table_value

Exact expanded first-order arithmetic statement

forall N U n z. (((exists dst_positive_code_one_lookup_tabletable dst_positive_scale_one_lookup_tabletable dst_negative_code_one_lookup_tabletable dst_negative_scale_one_lookup_tabletable. (((U) = (((((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) * S ((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) + ((dst_positive_scale_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable))) + (((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)))) * S ((((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) * S ((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) + ((dst_positive_scale_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable))) + (((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)))) + ((((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable))) + (((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)))))) /\ (forall dst_index_one_lookup_tabletable. (exists pvs_le_gap_one_lookup_tabletabledomain. pvs_le_gap_one_lookup_tabletabledomain + (dst_index_one_lookup_tabletable) = (N)) -> exists dst_positive_one_lookup_tabletable dst_negative_one_lookup_tabletable dst_value_one_lookup_tabletable. ((((exists ff_h_pvs_one_lookup_tabletableentrypositive. ff_h_pvs_one_lookup_tabletableentrypositive + S (dst_positive_one_lookup_tabletable) = S ((S (dst_index_one_lookup_tabletable)) * dst_positive_scale_one_lookup_tabletable)) /\ exists ff_q_pvs_one_lookup_tabletableentrypositive. dst_positive_code_one_lookup_tabletable = ff_q_pvs_one_lookup_tabletableentrypositive * S ((S (dst_index_one_lookup_tabletable)) * dst_positive_scale_one_lookup_tabletable) + (dst_positive_one_lookup_tabletable))) /\ (((((exists ff_h_pvs_one_lookup_tabletableentrynegative. ff_h_pvs_one_lookup_tabletableentrynegative + S (dst_negative_one_lookup_tabletable) = S ((S (dst_index_one_lookup_tabletable)) * dst_negative_scale_one_lookup_tabletable)) /\ exists ff_q_pvs_one_lookup_tabletableentrynegative. dst_negative_code_one_lookup_tabletable = ff_q_pvs_one_lookup_tabletableentrynegative * S ((S (dst_index_one_lookup_tabletable)) * dst_negative_scale_one_lookup_tabletable) + (dst_negative_one_lookup_tabletable))) /\ (exists ge_balance_positive_one_lookup_tabletableentryvalue ge_balance_negative_one_lookup_tabletableentryvalue. (((((dst_value_one_lookup_tabletable) = 2 * (ge_balance_positive_one_lookup_tabletableentryvalue) /\ (ge_balance_negative_one_lookup_tabletableentryvalue) = 0) \/ exists ge_signed_half_one_lookup_tabletableentryvaluedecode. (((dst_value_one_lookup_tabletable) = 2 * ge_signed_half_one_lookup_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_one_lookup_tabletableentryvalue) = 0) /\ (ge_balance_negative_one_lookup_tabletableentryvalue) = S ge_signed_half_one_lookup_tabletableentryvaluedecode))) /\ ((dst_positive_one_lookup_tabletable) + ge_balance_negative_one_lookup_tabletableentryvalue = (dst_negative_one_lookup_tabletable) + ge_balance_positive_one_lookup_tabletableentryvalue))))))))) /\ (forall du_index_one_lookup_table du_value_one_lookup_table. ~(du_index_one_lookup_table=0) -> (exists pvs_le_gap_one_lookup_tablebound. pvs_le_gap_one_lookup_tablebound + (du_index_one_lookup_table) = (N)) -> (exists dst_positive_code_one_lookup_tableentry dst_positive_scale_one_lookup_tableentry dst_negative_code_one_lookup_tableentry dst_negative_scale_one_lookup_tableentry dst_positive_one_lookup_tableentry dst_negative_one_lookup_tableentry. (((U) = (((((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) * S ((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) + ((dst_positive_scale_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry))) + (((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)))) * S ((((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) * S ((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) + ((dst_positive_scale_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry))) + (((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)))) + ((((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry))) + (((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)))))) /\ (((((exists ff_h_pvs_one_lookup_tableentrypositive. ff_h_pvs_one_lookup_tableentrypositive + S (dst_positive_one_lookup_tableentry) = S ((S (du_index_one_lookup_table)) * dst_positive_scale_one_lookup_tableentry)) /\ exists ff_q_pvs_one_lookup_tableentrypositive. dst_positive_code_one_lookup_tableentry = ff_q_pvs_one_lookup_tableentrypositive * S ((S (du_index_one_lookup_table)) * dst_positive_scale_one_lookup_tableentry) + (dst_positive_one_lookup_tableentry))) /\ (((((exists ff_h_pvs_one_lookup_tableentrynegative. ff_h_pvs_one_lookup_tableentrynegative + S (dst_negative_one_lookup_tableentry) = S ((S (du_index_one_lookup_table)) * dst_negative_scale_one_lookup_tableentry)) /\ exists ff_q_pvs_one_lookup_tableentrynegative. dst_negative_code_one_lookup_tableentry = ff_q_pvs_one_lookup_tableentrynegative * S ((S (du_index_one_lookup_table)) * dst_negative_scale_one_lookup_tableentry) + (dst_negative_one_lookup_tableentry))) /\ (exists ge_balance_positive_one_lookup_tableentryvalue ge_balance_negative_one_lookup_tableentryvalue. (((((du_value_one_lookup_table) = 2 * (ge_balance_positive_one_lookup_tableentryvalue) /\ (ge_balance_negative_one_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_one_lookup_tableentryvaluedecode. (((du_value_one_lookup_table) = 2 * ge_signed_half_one_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_one_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_one_lookup_tableentryvalue) = S ge_signed_half_one_lookup_tableentryvaluedecode))) /\ ((dst_positive_one_lookup_tableentry) + ge_balance_negative_one_lookup_tableentryvalue = (dst_negative_one_lookup_tableentry) + ge_balance_positive_one_lookup_tableentryvalue))))))))) -> du_value_one_lookup_table=2))) -> ~(n=0) -> (exists pvs_le_gap_one_lookup_bound. pvs_le_gap_one_lookup_bound + (n) = (N)) -> (exists dst_positive_code_one_lookup_entry dst_positive_scale_one_lookup_entry dst_negative_code_one_lookup_entry dst_negative_scale_one_lookup_entry dst_positive_one_lookup_entry dst_negative_one_lookup_entry. (((U) = (((((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) * S ((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) + ((dst_positive_scale_one_lookup_entry) + (dst_positive_scale_one_lookup_entry))) + (((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)))) * S ((((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) * S ((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) + ((dst_positive_scale_one_lookup_entry) + (dst_positive_scale_one_lookup_entry))) + (((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)))) + ((((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry))) + (((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)))))) /\ (((((exists ff_h_pvs_one_lookup_entrypositive. ff_h_pvs_one_lookup_entrypositive + S (dst_positive_one_lookup_entry) = S ((S (n)) * dst_positive_scale_one_lookup_entry)) /\ exists ff_q_pvs_one_lookup_entrypositive. dst_positive_code_one_lookup_entry = ff_q_pvs_one_lookup_entrypositive * S ((S (n)) * dst_positive_scale_one_lookup_entry) + (dst_positive_one_lookup_entry))) /\ (((((exists ff_h_pvs_one_lookup_entrynegative. ff_h_pvs_one_lookup_entrynegative + S (dst_negative_one_lookup_entry) = S ((S (n)) * dst_negative_scale_one_lookup_entry)) /\ exists ff_q_pvs_one_lookup_entrynegative. dst_negative_code_one_lookup_entry = ff_q_pvs_one_lookup_entrynegative * S ((S (n)) * dst_negative_scale_one_lookup_entry) + (dst_negative_one_lookup_entry))) /\ (exists ge_balance_positive_one_lookup_entryvalue ge_balance_negative_one_lookup_entryvalue. (((((z) = 2 * (ge_balance_positive_one_lookup_entryvalue) /\ (ge_balance_negative_one_lookup_entryvalue) = 0) \/ exists ge_signed_half_one_lookup_entryvaluedecode. (((z) = 2 * ge_signed_half_one_lookup_entryvaluedecode + 1 /\ (ge_balance_positive_one_lookup_entryvalue) = 0) /\ (ge_balance_negative_one_lookup_entryvalue) = S ge_signed_half_one_lookup_entryvaluedecode))) /\ ((dst_positive_one_lookup_entry) + ge_balance_negative_one_lookup_entryvalue = (dst_negative_one_lookup_entry) + ge_balance_positive_one_lookup_entryvalue))))))))) -> z=2