dirichlet_kronecker_delta_table_restrict

Exact expanded first-order arithmetic statement

forall N K E. (((exists dst_positive_code_delta_restrict_sourcetable dst_positive_scale_delta_restrict_sourcetable dst_negative_code_delta_restrict_sourcetable dst_negative_scale_delta_restrict_sourcetable. (((E) = (((((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) * S ((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) + ((dst_positive_scale_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable))) + (((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)))) * S ((((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) * S ((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) + ((dst_positive_scale_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable))) + (((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)))) + ((((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable))) + (((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)))))) /\ (forall dst_index_delta_restrict_sourcetable. (exists pvs_le_gap_delta_restrict_sourcetabledomain. pvs_le_gap_delta_restrict_sourcetabledomain + (dst_index_delta_restrict_sourcetable) = (N)) -> exists dst_positive_delta_restrict_sourcetable dst_negative_delta_restrict_sourcetable dst_value_delta_restrict_sourcetable. ((((exists ff_h_pvs_delta_restrict_sourcetableentrypositive. ff_h_pvs_delta_restrict_sourcetableentrypositive + S (dst_positive_delta_restrict_sourcetable) = S ((S (dst_index_delta_restrict_sourcetable)) * dst_positive_scale_delta_restrict_sourcetable)) /\ exists ff_q_pvs_delta_restrict_sourcetableentrypositive. dst_positive_code_delta_restrict_sourcetable = ff_q_pvs_delta_restrict_sourcetableentrypositive * S ((S (dst_index_delta_restrict_sourcetable)) * dst_positive_scale_delta_restrict_sourcetable) + (dst_positive_delta_restrict_sourcetable))) /\ (((((exists ff_h_pvs_delta_restrict_sourcetableentrynegative. ff_h_pvs_delta_restrict_sourcetableentrynegative + S (dst_negative_delta_restrict_sourcetable) = S ((S (dst_index_delta_restrict_sourcetable)) * dst_negative_scale_delta_restrict_sourcetable)) /\ exists ff_q_pvs_delta_restrict_sourcetableentrynegative. dst_negative_code_delta_restrict_sourcetable = ff_q_pvs_delta_restrict_sourcetableentrynegative * S ((S (dst_index_delta_restrict_sourcetable)) * dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_delta_restrict_sourcetable))) /\ (exists ge_balance_positive_delta_restrict_sourcetableentryvalue ge_balance_negative_delta_restrict_sourcetableentryvalue. (((((dst_value_delta_restrict_sourcetable) = 2 * (ge_balance_positive_delta_restrict_sourcetableentryvalue) /\ (ge_balance_negative_delta_restrict_sourcetableentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_sourcetableentryvaluedecode. (((dst_value_delta_restrict_sourcetable) = 2 * ge_signed_half_delta_restrict_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_sourcetableentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_sourcetableentryvalue) = S ge_signed_half_delta_restrict_sourcetableentryvaluedecode))) /\ ((dst_positive_delta_restrict_sourcetable) + ge_balance_negative_delta_restrict_sourcetableentryvalue = (dst_negative_delta_restrict_sourcetable) + ge_balance_positive_delta_restrict_sourcetableentryvalue))))))))) /\ (forall du_index_delta_restrict_source du_value_delta_restrict_source. ~(du_index_delta_restrict_source=0) -> (exists pvs_le_gap_delta_restrict_sourcebound. pvs_le_gap_delta_restrict_sourcebound + (du_index_delta_restrict_source) = (N)) -> (exists dst_positive_code_delta_restrict_sourceentry dst_positive_scale_delta_restrict_sourceentry dst_negative_code_delta_restrict_sourceentry dst_negative_scale_delta_restrict_sourceentry dst_positive_delta_restrict_sourceentry dst_negative_delta_restrict_sourceentry. (((E) = (((((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) * S ((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) + ((dst_positive_scale_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry))) + (((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)))) * S ((((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) * S ((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) + ((dst_positive_scale_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry))) + (((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)))) + ((((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry))) + (((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)))))) /\ (((((exists ff_h_pvs_delta_restrict_sourceentrypositive. ff_h_pvs_delta_restrict_sourceentrypositive + S (dst_positive_delta_restrict_sourceentry) = S ((S (du_index_delta_restrict_source)) * dst_positive_scale_delta_restrict_sourceentry)) /\ exists ff_q_pvs_delta_restrict_sourceentrypositive. dst_positive_code_delta_restrict_sourceentry = ff_q_pvs_delta_restrict_sourceentrypositive * S ((S (du_index_delta_restrict_source)) * dst_positive_scale_delta_restrict_sourceentry) + (dst_positive_delta_restrict_sourceentry))) /\ (((((exists ff_h_pvs_delta_restrict_sourceentrynegative. ff_h_pvs_delta_restrict_sourceentrynegative + S (dst_negative_delta_restrict_sourceentry) = S ((S (du_index_delta_restrict_source)) * dst_negative_scale_delta_restrict_sourceentry)) /\ exists ff_q_pvs_delta_restrict_sourceentrynegative. dst_negative_code_delta_restrict_sourceentry = ff_q_pvs_delta_restrict_sourceentrynegative * S ((S (du_index_delta_restrict_source)) * dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_delta_restrict_sourceentry))) /\ (exists ge_balance_positive_delta_restrict_sourceentryvalue ge_balance_negative_delta_restrict_sourceentryvalue. (((((du_value_delta_restrict_source) = 2 * (ge_balance_positive_delta_restrict_sourceentryvalue) /\ (ge_balance_negative_delta_restrict_sourceentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_sourceentryvaluedecode. (((du_value_delta_restrict_source) = 2 * ge_signed_half_delta_restrict_sourceentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_sourceentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_sourceentryvalue) = S ge_signed_half_delta_restrict_sourceentryvaluedecode))) /\ ((dst_positive_delta_restrict_sourceentry) + ge_balance_negative_delta_restrict_sourceentryvalue = (dst_negative_delta_restrict_sourceentry) + ge_balance_positive_delta_restrict_sourceentryvalue))))))))) -> ((((du_index_delta_restrict_source)=1 -> (du_value_delta_restrict_source)=2) /\ (~((du_index_delta_restrict_source)=1) -> (du_value_delta_restrict_source)=0)))))) -> (exists pvs_le_gap_delta_restrict_bound. pvs_le_gap_delta_restrict_bound + (K) = (N)) -> (((exists dst_positive_code_delta_restrict_resulttable dst_positive_scale_delta_restrict_resulttable dst_negative_code_delta_restrict_resulttable dst_negative_scale_delta_restrict_resulttable. (((E) = (((((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) * S ((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) + ((dst_positive_scale_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable))) + (((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)))) * S ((((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) * S ((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) + ((dst_positive_scale_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable))) + (((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)))) + ((((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable))) + (((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)))))) /\ (forall dst_index_delta_restrict_resulttable. (exists pvs_le_gap_delta_restrict_resulttabledomain. pvs_le_gap_delta_restrict_resulttabledomain + (dst_index_delta_restrict_resulttable) = (K)) -> exists dst_positive_delta_restrict_resulttable dst_negative_delta_restrict_resulttable dst_value_delta_restrict_resulttable. ((((exists ff_h_pvs_delta_restrict_resulttableentrypositive. ff_h_pvs_delta_restrict_resulttableentrypositive + S (dst_positive_delta_restrict_resulttable) = S ((S (dst_index_delta_restrict_resulttable)) * dst_positive_scale_delta_restrict_resulttable)) /\ exists ff_q_pvs_delta_restrict_resulttableentrypositive. dst_positive_code_delta_restrict_resulttable = ff_q_pvs_delta_restrict_resulttableentrypositive * S ((S (dst_index_delta_restrict_resulttable)) * dst_positive_scale_delta_restrict_resulttable) + (dst_positive_delta_restrict_resulttable))) /\ (((((exists ff_h_pvs_delta_restrict_resulttableentrynegative. ff_h_pvs_delta_restrict_resulttableentrynegative + S (dst_negative_delta_restrict_resulttable) = S ((S (dst_index_delta_restrict_resulttable)) * dst_negative_scale_delta_restrict_resulttable)) /\ exists ff_q_pvs_delta_restrict_resulttableentrynegative. dst_negative_code_delta_restrict_resulttable = ff_q_pvs_delta_restrict_resulttableentrynegative * S ((S (dst_index_delta_restrict_resulttable)) * dst_negative_scale_delta_restrict_resulttable) + (dst_negative_delta_restrict_resulttable))) /\ (exists ge_balance_positive_delta_restrict_resulttableentryvalue ge_balance_negative_delta_restrict_resulttableentryvalue. (((((dst_value_delta_restrict_resulttable) = 2 * (ge_balance_positive_delta_restrict_resulttableentryvalue) /\ (ge_balance_negative_delta_restrict_resulttableentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_resulttableentryvaluedecode. (((dst_value_delta_restrict_resulttable) = 2 * ge_signed_half_delta_restrict_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_resulttableentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_resulttableentryvalue) = S ge_signed_half_delta_restrict_resulttableentryvaluedecode))) /\ ((dst_positive_delta_restrict_resulttable) + ge_balance_negative_delta_restrict_resulttableentryvalue = (dst_negative_delta_restrict_resulttable) + ge_balance_positive_delta_restrict_resulttableentryvalue))))))))) /\ (forall du_index_delta_restrict_result du_value_delta_restrict_result. ~(du_index_delta_restrict_result=0) -> (exists pvs_le_gap_delta_restrict_resultbound. pvs_le_gap_delta_restrict_resultbound + (du_index_delta_restrict_result) = (K)) -> (exists dst_positive_code_delta_restrict_resultentry dst_positive_scale_delta_restrict_resultentry dst_negative_code_delta_restrict_resultentry dst_negative_scale_delta_restrict_resultentry dst_positive_delta_restrict_resultentry dst_negative_delta_restrict_resultentry. (((E) = (((((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) * S ((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) + ((dst_positive_scale_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry))) + (((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)))) * S ((((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) * S ((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) + ((dst_positive_scale_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry))) + (((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)))) + ((((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry))) + (((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)))))) /\ (((((exists ff_h_pvs_delta_restrict_resultentrypositive. ff_h_pvs_delta_restrict_resultentrypositive + S (dst_positive_delta_restrict_resultentry) = S ((S (du_index_delta_restrict_result)) * dst_positive_scale_delta_restrict_resultentry)) /\ exists ff_q_pvs_delta_restrict_resultentrypositive. dst_positive_code_delta_restrict_resultentry = ff_q_pvs_delta_restrict_resultentrypositive * S ((S (du_index_delta_restrict_result)) * dst_positive_scale_delta_restrict_resultentry) + (dst_positive_delta_restrict_resultentry))) /\ (((((exists ff_h_pvs_delta_restrict_resultentrynegative. ff_h_pvs_delta_restrict_resultentrynegative + S (dst_negative_delta_restrict_resultentry) = S ((S (du_index_delta_restrict_result)) * dst_negative_scale_delta_restrict_resultentry)) /\ exists ff_q_pvs_delta_restrict_resultentrynegative. dst_negative_code_delta_restrict_resultentry = ff_q_pvs_delta_restrict_resultentrynegative * S ((S (du_index_delta_restrict_result)) * dst_negative_scale_delta_restrict_resultentry) + (dst_negative_delta_restrict_resultentry))) /\ (exists ge_balance_positive_delta_restrict_resultentryvalue ge_balance_negative_delta_restrict_resultentryvalue. (((((du_value_delta_restrict_result) = 2 * (ge_balance_positive_delta_restrict_resultentryvalue) /\ (ge_balance_negative_delta_restrict_resultentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_resultentryvaluedecode. (((du_value_delta_restrict_result) = 2 * ge_signed_half_delta_restrict_resultentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_resultentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_resultentryvalue) = S ge_signed_half_delta_restrict_resultentryvaluedecode))) /\ ((dst_positive_delta_restrict_resultentry) + ge_balance_negative_delta_restrict_resultentryvalue = (dst_negative_delta_restrict_resultentry) + ge_balance_positive_delta_restrict_resultentryvalue))))))))) -> ((((du_index_delta_restrict_result)=1 -> (du_value_delta_restrict_result)=2) /\ (~((du_index_delta_restrict_result)=1) -> (du_value_delta_restrict_result)=0))))))