arithmetic_signed_table_append

Exact expanded first-order arithmetic statement

forall N F z. (exists dst_positive_code_append_input dst_positive_scale_append_input dst_negative_code_append_input dst_negative_scale_append_input. (((F) = (((((dst_positive_code_append_input) + (dst_positive_scale_append_input)) * S ((dst_positive_code_append_input) + (dst_positive_scale_append_input)) + ((dst_positive_scale_append_input) + (dst_positive_scale_append_input))) + (((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input)))) * S ((((dst_positive_code_append_input) + (dst_positive_scale_append_input)) * S ((dst_positive_code_append_input) + (dst_positive_scale_append_input)) + ((dst_positive_scale_append_input) + (dst_positive_scale_append_input))) + (((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input)))) + ((((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input))) + (((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input)))))) /\ (forall dst_index_append_input. (exists pvs_le_gap_append_inputdomain. pvs_le_gap_append_inputdomain + (dst_index_append_input) = (N)) -> exists dst_positive_append_input dst_negative_append_input dst_value_append_input. ((((exists ff_h_pvs_append_inputentrypositive. ff_h_pvs_append_inputentrypositive + S (dst_positive_append_input) = S ((S (dst_index_append_input)) * dst_positive_scale_append_input)) /\ exists ff_q_pvs_append_inputentrypositive. dst_positive_code_append_input = ff_q_pvs_append_inputentrypositive * S ((S (dst_index_append_input)) * dst_positive_scale_append_input) + (dst_positive_append_input))) /\ (((((exists ff_h_pvs_append_inputentrynegative. ff_h_pvs_append_inputentrynegative + S (dst_negative_append_input) = S ((S (dst_index_append_input)) * dst_negative_scale_append_input)) /\ exists ff_q_pvs_append_inputentrynegative. dst_negative_code_append_input = ff_q_pvs_append_inputentrynegative * S ((S (dst_index_append_input)) * dst_negative_scale_append_input) + (dst_negative_append_input))) /\ (exists ge_balance_positive_append_inputentryvalue ge_balance_negative_append_inputentryvalue. (((((dst_value_append_input) = 2 * (ge_balance_positive_append_inputentryvalue) /\ (ge_balance_negative_append_inputentryvalue) = 0) \/ exists ge_signed_half_append_inputentryvaluedecode. (((dst_value_append_input) = 2 * ge_signed_half_append_inputentryvaluedecode + 1 /\ (ge_balance_positive_append_inputentryvalue) = 0) /\ (ge_balance_negative_append_inputentryvalue) = S ge_signed_half_append_inputentryvaluedecode))) /\ ((dst_positive_append_input) + ge_balance_negative_append_inputentryvalue = (dst_negative_append_input) + ge_balance_positive_append_inputentryvalue))))))))) -> exists G. (((exists dst_positive_code_append_outputtable dst_positive_scale_append_outputtable dst_negative_code_append_outputtable dst_negative_scale_append_outputtable. (((G) = (((((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) * S ((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) + ((dst_positive_scale_append_outputtable) + (dst_positive_scale_append_outputtable))) + (((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable)))) * S ((((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) * S ((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) + ((dst_positive_scale_append_outputtable) + (dst_positive_scale_append_outputtable))) + (((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable)))) + ((((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable))) + (((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable)))))) /\ (forall dst_index_append_outputtable. (exists pvs_le_gap_append_outputtabledomain. pvs_le_gap_append_outputtabledomain + (dst_index_append_outputtable) = (S N)) -> exists dst_positive_append_outputtable dst_negative_append_outputtable dst_value_append_outputtable. ((((exists ff_h_pvs_append_outputtableentrypositive. ff_h_pvs_append_outputtableentrypositive + S (dst_positive_append_outputtable) = S ((S (dst_index_append_outputtable)) * dst_positive_scale_append_outputtable)) /\ exists ff_q_pvs_append_outputtableentrypositive. dst_positive_code_append_outputtable = ff_q_pvs_append_outputtableentrypositive * S ((S (dst_index_append_outputtable)) * dst_positive_scale_append_outputtable) + (dst_positive_append_outputtable))) /\ (((((exists ff_h_pvs_append_outputtableentrynegative. ff_h_pvs_append_outputtableentrynegative + S (dst_negative_append_outputtable) = S ((S (dst_index_append_outputtable)) * dst_negative_scale_append_outputtable)) /\ exists ff_q_pvs_append_outputtableentrynegative. dst_negative_code_append_outputtable = ff_q_pvs_append_outputtableentrynegative * S ((S (dst_index_append_outputtable)) * dst_negative_scale_append_outputtable) + (dst_negative_append_outputtable))) /\ (exists ge_balance_positive_append_outputtableentryvalue ge_balance_negative_append_outputtableentryvalue. (((((dst_value_append_outputtable) = 2 * (ge_balance_positive_append_outputtableentryvalue) /\ (ge_balance_negative_append_outputtableentryvalue) = 0) \/ exists ge_signed_half_append_outputtableentryvaluedecode. (((dst_value_append_outputtable) = 2 * ge_signed_half_append_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_append_outputtableentryvalue) = 0) /\ (ge_balance_negative_append_outputtableentryvalue) = S ge_signed_half_append_outputtableentryvaluedecode))) /\ ((dst_positive_append_outputtable) + ge_balance_negative_append_outputtableentryvalue = (dst_negative_append_outputtable) + ge_balance_positive_append_outputtableentryvalue))))))))) /\ (((forall dst_index_append_outputprefix dst_first_append_outputprefix dst_second_append_outputprefix. (exists pvs_gap_append_outputprefixbound. pvs_gap_append_outputprefixbound + S (dst_index_append_outputprefix) = (S N)) -> (exists dst_positive_code_append_outputprefixfirst dst_positive_scale_append_outputprefixfirst dst_negative_code_append_outputprefixfirst dst_negative_scale_append_outputprefixfirst dst_positive_append_outputprefixfirst dst_negative_append_outputprefixfirst. (((F) = (((((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) * S ((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) + ((dst_positive_scale_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst))) + (((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)))) * S ((((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) * S ((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) + ((dst_positive_scale_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst))) + (((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)))) + ((((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst))) + (((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)))))) /\ (((((exists ff_h_pvs_append_outputprefixfirstpositive. ff_h_pvs_append_outputprefixfirstpositive + S (dst_positive_append_outputprefixfirst) = S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixfirst)) /\ exists ff_q_pvs_append_outputprefixfirstpositive. dst_positive_code_append_outputprefixfirst = ff_q_pvs_append_outputprefixfirstpositive * S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixfirst) + (dst_positive_append_outputprefixfirst))) /\ (((((exists ff_h_pvs_append_outputprefixfirstnegative. ff_h_pvs_append_outputprefixfirstnegative + S (dst_negative_append_outputprefixfirst) = S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixfirst)) /\ exists ff_q_pvs_append_outputprefixfirstnegative. dst_negative_code_append_outputprefixfirst = ff_q_pvs_append_outputprefixfirstnegative * S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixfirst) + (dst_negative_append_outputprefixfirst))) /\ (exists ge_balance_positive_append_outputprefixfirstvalue ge_balance_negative_append_outputprefixfirstvalue. (((((dst_first_append_outputprefix) = 2 * (ge_balance_positive_append_outputprefixfirstvalue) /\ (ge_balance_negative_append_outputprefixfirstvalue) = 0) \/ exists ge_signed_half_append_outputprefixfirstvaluedecode. (((dst_first_append_outputprefix) = 2 * ge_signed_half_append_outputprefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_outputprefixfirstvalue) = 0) /\ (ge_balance_negative_append_outputprefixfirstvalue) = S ge_signed_half_append_outputprefixfirstvaluedecode))) /\ ((dst_positive_append_outputprefixfirst) + ge_balance_negative_append_outputprefixfirstvalue = (dst_negative_append_outputprefixfirst) + ge_balance_positive_append_outputprefixfirstvalue))))))))) -> (exists dst_positive_code_append_outputprefixsecond dst_positive_scale_append_outputprefixsecond dst_negative_code_append_outputprefixsecond dst_negative_scale_append_outputprefixsecond dst_positive_append_outputprefixsecond dst_negative_append_outputprefixsecond. (((G) = (((((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) * S ((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) + ((dst_positive_scale_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond))) + (((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)))) * S ((((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) * S ((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) + ((dst_positive_scale_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond))) + (((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)))) + ((((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond))) + (((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)))))) /\ (((((exists ff_h_pvs_append_outputprefixsecondpositive. ff_h_pvs_append_outputprefixsecondpositive + S (dst_positive_append_outputprefixsecond) = S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixsecond)) /\ exists ff_q_pvs_append_outputprefixsecondpositive. dst_positive_code_append_outputprefixsecond = ff_q_pvs_append_outputprefixsecondpositive * S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixsecond) + (dst_positive_append_outputprefixsecond))) /\ (((((exists ff_h_pvs_append_outputprefixsecondnegative. ff_h_pvs_append_outputprefixsecondnegative + S (dst_negative_append_outputprefixsecond) = S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixsecond)) /\ exists ff_q_pvs_append_outputprefixsecondnegative. dst_negative_code_append_outputprefixsecond = ff_q_pvs_append_outputprefixsecondnegative * S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixsecond) + (dst_negative_append_outputprefixsecond))) /\ (exists ge_balance_positive_append_outputprefixsecondvalue ge_balance_negative_append_outputprefixsecondvalue. (((((dst_second_append_outputprefix) = 2 * (ge_balance_positive_append_outputprefixsecondvalue) /\ (ge_balance_negative_append_outputprefixsecondvalue) = 0) \/ exists ge_signed_half_append_outputprefixsecondvaluedecode. (((dst_second_append_outputprefix) = 2 * ge_signed_half_append_outputprefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_outputprefixsecondvalue) = 0) /\ (ge_balance_negative_append_outputprefixsecondvalue) = S ge_signed_half_append_outputprefixsecondvaluedecode))) /\ ((dst_positive_append_outputprefixsecond) + ge_balance_negative_append_outputprefixsecondvalue = (dst_negative_append_outputprefixsecond) + ge_balance_positive_append_outputprefixsecondvalue))))))))) -> dst_first_append_outputprefix = dst_second_append_outputprefix) /\ (exists dst_positive_code_append_outputlast dst_positive_scale_append_outputlast dst_negative_code_append_outputlast dst_negative_scale_append_outputlast dst_positive_append_outputlast dst_negative_append_outputlast. (((G) = (((((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) * S ((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) + ((dst_positive_scale_append_outputlast) + (dst_positive_scale_append_outputlast))) + (((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast)))) * S ((((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) * S ((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) + ((dst_positive_scale_append_outputlast) + (dst_positive_scale_append_outputlast))) + (((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast)))) + ((((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast))) + (((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast)))))) /\ (((((exists ff_h_pvs_append_outputlastpositive. ff_h_pvs_append_outputlastpositive + S (dst_positive_append_outputlast) = S ((S (S N)) * dst_positive_scale_append_outputlast)) /\ exists ff_q_pvs_append_outputlastpositive. dst_positive_code_append_outputlast = ff_q_pvs_append_outputlastpositive * S ((S (S N)) * dst_positive_scale_append_outputlast) + (dst_positive_append_outputlast))) /\ (((((exists ff_h_pvs_append_outputlastnegative. ff_h_pvs_append_outputlastnegative + S (dst_negative_append_outputlast) = S ((S (S N)) * dst_negative_scale_append_outputlast)) /\ exists ff_q_pvs_append_outputlastnegative. dst_negative_code_append_outputlast = ff_q_pvs_append_outputlastnegative * S ((S (S N)) * dst_negative_scale_append_outputlast) + (dst_negative_append_outputlast))) /\ (exists ge_balance_positive_append_outputlastvalue ge_balance_negative_append_outputlastvalue. (((((z) = 2 * (ge_balance_positive_append_outputlastvalue) /\ (ge_balance_negative_append_outputlastvalue) = 0) \/ exists ge_signed_half_append_outputlastvaluedecode. (((z) = 2 * ge_signed_half_append_outputlastvaluedecode + 1 /\ (ge_balance_positive_append_outputlastvalue) = 0) /\ (ge_balance_negative_append_outputlastvalue) = S ge_signed_half_append_outputlastvaluedecode))) /\ ((dst_positive_append_outputlast) + ge_balance_negative_append_outputlastvalue = (dst_negative_append_outputlast) + ge_balance_positive_append_outputlastvalue)))))))))))))