Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ∀ H. DirichletTable(N,F,G,H) → DirichletTable(N,G,F,H)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F G H. (((exists dst_positive_code_table_commutative_sourceleft dst_positive_scale_table_commutative_sourceleft dst_negative_code_table_commutative_sourceleft dst_negative_scale_table_commutative_sourceleft. (((F) = (((((dst_positive_code_table_commutative_sourceleft) + (dst_positive_scale_table_commutative_sourceleft)) * S ((dst_positive_code_table_commutative_sourceleft) + (dst_positive_scale_table_commutative_sourceleft)) + ((dst_positive_scale_table_commutative_sourceleft) + (dst_positive_scale_table_commutative_sourceleft))) + (((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) * S ((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) + ((dst_negative_scale_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)))) * S ((((dst_positive_code_table_commutative_sourceleft) + (dst_positive_scale_table_commutative_sourceleft)) * S ((dst_positive_code_table_commutative_sourceleft) + (dst_positive_scale_table_commutative_sourceleft)) + ((dst_positive_scale_table_commutative_sourceleft) + (dst_positive_scale_table_commutative_sourceleft))) + (((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) * S ((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) + ((dst_negative_scale_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)))) + ((((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) * S ((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) + ((dst_negative_scale_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft))) + (((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) * S ((dst_negative_code_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)) + ((dst_negative_scale_table_commutative_sourceleft) + (dst_negative_scale_table_commutative_sourceleft)))))) /\ (forall dst_index_table_commutative_sourceleft. (exists pvs_le_gap_table_commutative_sourceleftdomain. pvs_le_gap_table_commutative_sourceleftdomain + (dst_index_table_commutative_sourceleft) = (N)) -> exists dst_positive_table_commutative_sourceleft dst_negative_table_commutative_sourceleft dst_value_table_commutative_sourceleft. ((((exists ff_h_pvs_table_commutative_sourceleftentrypositive. ff_h_pvs_table_commutative_sourceleftentrypositive + S (dst_positive_table_commutative_sourceleft) = S ((S (dst_index_table_commutative_sourceleft)) * dst_positive_scale_table_commutative_sourceleft)) /\ exists ff_q_pvs_table_commutative_sourceleftentrypositive. dst_positive_code_table_commutative_sourceleft = ff_q_pvs_table_commutative_sourceleftentrypositive * S ((S (dst_index_table_commutative_sourceleft)) * dst_positive_scale_table_commutative_sourceleft) + (dst_positive_table_commutative_sourceleft))) /\ (((((exists ff_h_pvs_table_commutative_sourceleftentrynegative. ff_h_pvs_table_commutative_sourceleftentrynegative + S (dst_negative_table_commutative_sourceleft) = S ((S (dst_index_table_commutative_sourceleft)) * dst_negative_scale_table_commutative_sourceleft)) /\ exists ff_q_pvs_table_commutative_sourceleftentrynegative. dst_negative_code_table_commutative_sourceleft = ff_q_pvs_table_commutative_sourceleftentrynegative * S ((S (dst_index_table_commutative_sourceleft)) * dst_negative_scale_table_commutative_sourceleft) + (dst_negative_table_commutative_sourceleft))) /\ (exists ge_balance_positive_table_commutative_sourceleftentryvalue ge_balance_negative_table_commutative_sourceleftentryvalue. (((((dst_value_table_commutative_sourceleft) = 2 * (ge_balance_positive_table_commutative_sourceleftentryvalue) /\ (ge_balance_negative_table_commutative_sourceleftentryvalue) = 0) \/ exists ge_signed_half_table_commutative_sourceleftentryvaluedecode. (((dst_value_table_commutative_sourceleft) = 2 * ge_signed_half_table_commutative_sourceleftentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourceleftentryvalue) = 0) /\ (ge_balance_negative_table_commutative_sourceleftentryvalue) = S ge_signed_half_table_commutative_sourceleftentryvaluedecode))) /\ ((dst_positive_table_commutative_sourceleft) + ge_balance_negative_table_commutative_sourceleftentryvalue = (dst_negative_table_commutative_sourceleft) + ge_balance_positive_table_commutative_sourceleftentryvalue))))))))) /\ (((exists dst_positive_code_table_commutative_sourceright dst_positive_scale_table_commutative_sourceright dst_negative_code_table_commutative_sourceright dst_negative_scale_table_commutative_sourceright. (((G) = (((((dst_positive_code_table_commutative_sourceright) + (dst_positive_scale_table_commutative_sourceright)) * S ((dst_positive_code_table_commutative_sourceright) + (dst_positive_scale_table_commutative_sourceright)) + ((dst_positive_scale_table_commutative_sourceright) + (dst_positive_scale_table_commutative_sourceright))) + (((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) * S ((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) + ((dst_negative_scale_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)))) * S ((((dst_positive_code_table_commutative_sourceright) + (dst_positive_scale_table_commutative_sourceright)) * S ((dst_positive_code_table_commutative_sourceright) + (dst_positive_scale_table_commutative_sourceright)) + ((dst_positive_scale_table_commutative_sourceright) + (dst_positive_scale_table_commutative_sourceright))) + (((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) * S ((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) + ((dst_negative_scale_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)))) + ((((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) * S ((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) + ((dst_negative_scale_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright))) + (((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) * S ((dst_negative_code_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)) + ((dst_negative_scale_table_commutative_sourceright) + (dst_negative_scale_table_commutative_sourceright)))))) /\ (forall dst_index_table_commutative_sourceright. (exists pvs_le_gap_table_commutative_sourcerightdomain. pvs_le_gap_table_commutative_sourcerightdomain + (dst_index_table_commutative_sourceright) = (N)) -> exists dst_positive_table_commutative_sourceright dst_negative_table_commutative_sourceright dst_value_table_commutative_sourceright. ((((exists ff_h_pvs_table_commutative_sourcerightentrypositive. ff_h_pvs_table_commutative_sourcerightentrypositive + S (dst_positive_table_commutative_sourceright) = S ((S (dst_index_table_commutative_sourceright)) * dst_positive_scale_table_commutative_sourceright)) /\ exists ff_q_pvs_table_commutative_sourcerightentrypositive. dst_positive_code_table_commutative_sourceright = ff_q_pvs_table_commutative_sourcerightentrypositive * S ((S (dst_index_table_commutative_sourceright)) * dst_positive_scale_table_commutative_sourceright) + (dst_positive_table_commutative_sourceright))) /\ (((((exists ff_h_pvs_table_commutative_sourcerightentrynegative. ff_h_pvs_table_commutative_sourcerightentrynegative + S (dst_negative_table_commutative_sourceright) = S ((S (dst_index_table_commutative_sourceright)) * dst_negative_scale_table_commutative_sourceright)) /\ exists ff_q_pvs_table_commutative_sourcerightentrynegative. dst_negative_code_table_commutative_sourceright = ff_q_pvs_table_commutative_sourcerightentrynegative * S ((S (dst_index_table_commutative_sourceright)) * dst_negative_scale_table_commutative_sourceright) + (dst_negative_table_commutative_sourceright))) /\ (exists ge_balance_positive_table_commutative_sourcerightentryvalue ge_balance_negative_table_commutative_sourcerightentryvalue. (((((dst_value_table_commutative_sourceright) = 2 * (ge_balance_positive_table_commutative_sourcerightentryvalue) /\ (ge_balance_negative_table_commutative_sourcerightentryvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcerightentryvaluedecode. (((dst_value_table_commutative_sourceright) = 2 * ge_signed_half_table_commutative_sourcerightentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcerightentryvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcerightentryvalue) = S ge_signed_half_table_commutative_sourcerightentryvaluedecode))) /\ ((dst_positive_table_commutative_sourceright) + ge_balance_negative_table_commutative_sourcerightentryvalue = (dst_negative_table_commutative_sourceright) + ge_balance_positive_table_commutative_sourcerightentryvalue))))))))) /\ (((exists dst_positive_code_table_commutative_sourcetable dst_positive_scale_table_commutative_sourcetable dst_negative_code_table_commutative_sourcetable dst_negative_scale_table_commutative_sourcetable. (((H) = (((((dst_positive_code_table_commutative_sourcetable) + (dst_positive_scale_table_commutative_sourcetable)) * S ((dst_positive_code_table_commutative_sourcetable) + (dst_positive_scale_table_commutative_sourcetable)) + ((dst_positive_scale_table_commutative_sourcetable) + (dst_positive_scale_table_commutative_sourcetable))) + (((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) * S ((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) + ((dst_negative_scale_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)))) * S ((((dst_positive_code_table_commutative_sourcetable) + (dst_positive_scale_table_commutative_sourcetable)) * S ((dst_positive_code_table_commutative_sourcetable) + (dst_positive_scale_table_commutative_sourcetable)) + ((dst_positive_scale_table_commutative_sourcetable) + (dst_positive_scale_table_commutative_sourcetable))) + (((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) * S ((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) + ((dst_negative_scale_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)))) + ((((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) * S ((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) + ((dst_negative_scale_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable))) + (((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) * S ((dst_negative_code_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)) + ((dst_negative_scale_table_commutative_sourcetable) + (dst_negative_scale_table_commutative_sourcetable)))))) /\ (forall dst_index_table_commutative_sourcetable. (exists pvs_le_gap_table_commutative_sourcetabledomain. pvs_le_gap_table_commutative_sourcetabledomain + (dst_index_table_commutative_sourcetable) = (N)) -> exists dst_positive_table_commutative_sourcetable dst_negative_table_commutative_sourcetable dst_value_table_commutative_sourcetable. ((((exists ff_h_pvs_table_commutative_sourcetableentrypositive. ff_h_pvs_table_commutative_sourcetableentrypositive + S (dst_positive_table_commutative_sourcetable) = S ((S (dst_index_table_commutative_sourcetable)) * dst_positive_scale_table_commutative_sourcetable)) /\ exists ff_q_pvs_table_commutative_sourcetableentrypositive. dst_positive_code_table_commutative_sourcetable = ff_q_pvs_table_commutative_sourcetableentrypositive * S ((S (dst_index_table_commutative_sourcetable)) * dst_positive_scale_table_commutative_sourcetable) + (dst_positive_table_commutative_sourcetable))) /\ (((((exists ff_h_pvs_table_commutative_sourcetableentrynegative. ff_h_pvs_table_commutative_sourcetableentrynegative + S (dst_negative_table_commutative_sourcetable) = S ((S (dst_index_table_commutative_sourcetable)) * dst_negative_scale_table_commutative_sourcetable)) /\ exists ff_q_pvs_table_commutative_sourcetableentrynegative. dst_negative_code_table_commutative_sourcetable = ff_q_pvs_table_commutative_sourcetableentrynegative * S ((S (dst_index_table_commutative_sourcetable)) * dst_negative_scale_table_commutative_sourcetable) + (dst_negative_table_commutative_sourcetable))) /\ (exists ge_balance_positive_table_commutative_sourcetableentryvalue ge_balance_negative_table_commutative_sourcetableentryvalue. (((((dst_value_table_commutative_sourcetable) = 2 * (ge_balance_positive_table_commutative_sourcetableentryvalue) /\ (ge_balance_negative_table_commutative_sourcetableentryvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcetableentryvaluedecode. (((dst_value_table_commutative_sourcetable) = 2 * ge_signed_half_table_commutative_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcetableentryvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcetableentryvalue) = S ge_signed_half_table_commutative_sourcetableentryvaluedecode))) /\ ((dst_positive_table_commutative_sourcetable) + ge_balance_negative_table_commutative_sourcetableentryvalue = (dst_negative_table_commutative_sourcetable) + ge_balance_positive_table_commutative_sourcetableentryvalue))))))))) /\ (forall dc_input_table_commutative_source dc_output_table_commutative_source. ~(dc_input_table_commutative_source=0) -> (exists pvs_le_gap_table_commutative_sourcedomain. pvs_le_gap_table_commutative_sourcedomain + (dc_input_table_commutative_source) = (N)) -> (exists dst_positive_code_table_commutative_sourcelookup dst_positive_scale_table_commutative_sourcelookup dst_negative_code_table_commutative_sourcelookup dst_negative_scale_table_commutative_sourcelookup dst_positive_table_commutative_sourcelookup dst_negative_table_commutative_sourcelookup. (((H) = (((((dst_positive_code_table_commutative_sourcelookup) + (dst_positive_scale_table_commutative_sourcelookup)) * S ((dst_positive_code_table_commutative_sourcelookup) + (dst_positive_scale_table_commutative_sourcelookup)) + ((dst_positive_scale_table_commutative_sourcelookup) + (dst_positive_scale_table_commutative_sourcelookup))) + (((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) * S ((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) + ((dst_negative_scale_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)))) * S ((((dst_positive_code_table_commutative_sourcelookup) + (dst_positive_scale_table_commutative_sourcelookup)) * S ((dst_positive_code_table_commutative_sourcelookup) + (dst_positive_scale_table_commutative_sourcelookup)) + ((dst_positive_scale_table_commutative_sourcelookup) + (dst_positive_scale_table_commutative_sourcelookup))) + (((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) * S ((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) + ((dst_negative_scale_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)))) + ((((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) * S ((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) + ((dst_negative_scale_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup))) + (((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) * S ((dst_negative_code_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)) + ((dst_negative_scale_table_commutative_sourcelookup) + (dst_negative_scale_table_commutative_sourcelookup)))))) /\ (((((exists ff_h_pvs_table_commutative_sourcelookuppositive. ff_h_pvs_table_commutative_sourcelookuppositive + S (dst_positive_table_commutative_sourcelookup) = S ((S (dc_input_table_commutative_source)) * dst_positive_scale_table_commutative_sourcelookup)) /\ exists ff_q_pvs_table_commutative_sourcelookuppositive. dst_positive_code_table_commutative_sourcelookup = ff_q_pvs_table_commutative_sourcelookuppositive * S ((S (dc_input_table_commutative_source)) * dst_positive_scale_table_commutative_sourcelookup) + (dst_positive_table_commutative_sourcelookup))) /\ (((((exists ff_h_pvs_table_commutative_sourcelookupnegative. ff_h_pvs_table_commutative_sourcelookupnegative + S (dst_negative_table_commutative_sourcelookup) = S ((S (dc_input_table_commutative_source)) * dst_negative_scale_table_commutative_sourcelookup)) /\ exists ff_q_pvs_table_commutative_sourcelookupnegative. dst_negative_code_table_commutative_sourcelookup = ff_q_pvs_table_commutative_sourcelookupnegative * S ((S (dc_input_table_commutative_source)) * dst_negative_scale_table_commutative_sourcelookup) + (dst_negative_table_commutative_sourcelookup))) /\ (exists ge_balance_positive_table_commutative_sourcelookupvalue ge_balance_negative_table_commutative_sourcelookupvalue. (((((dc_output_table_commutative_source) = 2 * (ge_balance_positive_table_commutative_sourcelookupvalue) /\ (ge_balance_negative_table_commutative_sourcelookupvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcelookupvaluedecode. (((dc_output_table_commutative_source) = 2 * ge_signed_half_table_commutative_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcelookupvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcelookupvalue) = S ge_signed_half_table_commutative_sourcelookupvaluedecode))) /\ ((dst_positive_table_commutative_sourcelookup) + ge_balance_negative_table_commutative_sourcelookupvalue = (dst_negative_table_commutative_sourcelookup) + ge_balance_positive_table_commutative_sourcelookupvalue))))))))) -> (((~((dc_input_table_commutative_source)=0)) /\ (exists dc_mask_table_commutative_sourcevalue. ((((exists dst_positive_code_table_commutative_sourcevaluemasktable dst_positive_scale_table_commutative_sourcevaluemasktable dst_negative_code_table_commutative_sourcevaluemasktable dst_negative_scale_table_commutative_sourcevaluemasktable. (((dc_mask_table_commutative_sourcevalue) = (((((dst_positive_code_table_commutative_sourcevaluemasktable) + (dst_positive_scale_table_commutative_sourcevaluemasktable)) * S ((dst_positive_code_table_commutative_sourcevaluemasktable) + (dst_positive_scale_table_commutative_sourcevaluemasktable)) + ((dst_positive_scale_table_commutative_sourcevaluemasktable) + (dst_positive_scale_table_commutative_sourcevaluemasktable))) + (((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) * S ((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) + ((dst_negative_scale_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)))) * S ((((dst_positive_code_table_commutative_sourcevaluemasktable) + (dst_positive_scale_table_commutative_sourcevaluemasktable)) * S ((dst_positive_code_table_commutative_sourcevaluemasktable) + (dst_positive_scale_table_commutative_sourcevaluemasktable)) + ((dst_positive_scale_table_commutative_sourcevaluemasktable) + (dst_positive_scale_table_commutative_sourcevaluemasktable))) + (((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) * S ((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) + ((dst_negative_scale_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)))) + ((((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) * S ((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) + ((dst_negative_scale_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable))) + (((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) * S ((dst_negative_code_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)) + ((dst_negative_scale_table_commutative_sourcevaluemasktable) + (dst_negative_scale_table_commutative_sourcevaluemasktable)))))) /\ (forall dst_index_table_commutative_sourcevaluemasktable. (exists pvs_le_gap_table_commutative_sourcevaluemasktabledomain. pvs_le_gap_table_commutative_sourcevaluemasktabledomain + (dst_index_table_commutative_sourcevaluemasktable) = (dc_input_table_commutative_source)) -> exists dst_positive_table_commutative_sourcevaluemasktable dst_negative_table_commutative_sourcevaluemasktable dst_value_table_commutative_sourcevaluemasktable. ((((exists ff_h_pvs_table_commutative_sourcevaluemasktableentrypositive. ff_h_pvs_table_commutative_sourcevaluemasktableentrypositive + S (dst_positive_table_commutative_sourcevaluemasktable) = S ((S (dst_index_table_commutative_sourcevaluemasktable)) * dst_positive_scale_table_commutative_sourcevaluemasktable)) /\ exists ff_q_pvs_table_commutative_sourcevaluemasktableentrypositive. dst_positive_code_table_commutative_sourcevaluemasktable = ff_q_pvs_table_commutative_sourcevaluemasktableentrypositive * S ((S (dst_index_table_commutative_sourcevaluemasktable)) * dst_positive_scale_table_commutative_sourcevaluemasktable) + (dst_positive_table_commutative_sourcevaluemasktable))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemasktableentrynegative. ff_h_pvs_table_commutative_sourcevaluemasktableentrynegative + S (dst_negative_table_commutative_sourcevaluemasktable) = S ((S (dst_index_table_commutative_sourcevaluemasktable)) * dst_negative_scale_table_commutative_sourcevaluemasktable)) /\ exists ff_q_pvs_table_commutative_sourcevaluemasktableentrynegative. dst_negative_code_table_commutative_sourcevaluemasktable = ff_q_pvs_table_commutative_sourcevaluemasktableentrynegative * S ((S (dst_index_table_commutative_sourcevaluemasktable)) * dst_negative_scale_table_commutative_sourcevaluemasktable) + (dst_negative_table_commutative_sourcevaluemasktable))) /\ (exists ge_balance_positive_table_commutative_sourcevaluemasktableentryvalue ge_balance_negative_table_commutative_sourcevaluemasktableentryvalue. (((((dst_value_table_commutative_sourcevaluemasktable) = 2 * (ge_balance_positive_table_commutative_sourcevaluemasktableentryvalue) /\ (ge_balance_negative_table_commutative_sourcevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemasktableentryvaluedecode. (((dst_value_table_commutative_sourcevaluemasktable) = 2 * ge_signed_half_table_commutative_sourcevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcevaluemasktableentryvalue) = S ge_signed_half_table_commutative_sourcevaluemasktableentryvaluedecode))) /\ ((dst_positive_table_commutative_sourcevaluemasktable) + ge_balance_negative_table_commutative_sourcevaluemasktableentryvalue = (dst_negative_table_commutative_sourcevaluemasktable) + ge_balance_positive_table_commutative_sourcevaluemasktableentryvalue))))))))) /\ (forall dc_index_table_commutative_sourcevaluemask dc_value_table_commutative_sourcevaluemask. (exists pvs_le_gap_table_commutative_sourcevaluemaskdomain. pvs_le_gap_table_commutative_sourcevaluemaskdomain + (dc_index_table_commutative_sourcevaluemask) = (dc_input_table_commutative_source)) -> (exists dst_positive_code_table_commutative_sourcevaluemasklookup dst_positive_scale_table_commutative_sourcevaluemasklookup dst_negative_code_table_commutative_sourcevaluemasklookup dst_negative_scale_table_commutative_sourcevaluemasklookup dst_positive_table_commutative_sourcevaluemasklookup dst_negative_table_commutative_sourcevaluemasklookup. (((dc_mask_table_commutative_sourcevalue) = (((((dst_positive_code_table_commutative_sourcevaluemasklookup) + (dst_positive_scale_table_commutative_sourcevaluemasklookup)) * S ((dst_positive_code_table_commutative_sourcevaluemasklookup) + (dst_positive_scale_table_commutative_sourcevaluemasklookup)) + ((dst_positive_scale_table_commutative_sourcevaluemasklookup) + (dst_positive_scale_table_commutative_sourcevaluemasklookup))) + (((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) * S ((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) + ((dst_negative_scale_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)))) * S ((((dst_positive_code_table_commutative_sourcevaluemasklookup) + (dst_positive_scale_table_commutative_sourcevaluemasklookup)) * S ((dst_positive_code_table_commutative_sourcevaluemasklookup) + (dst_positive_scale_table_commutative_sourcevaluemasklookup)) + ((dst_positive_scale_table_commutative_sourcevaluemasklookup) + (dst_positive_scale_table_commutative_sourcevaluemasklookup))) + (((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) * S ((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) + ((dst_negative_scale_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)))) + ((((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) * S ((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) + ((dst_negative_scale_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup))) + (((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) * S ((dst_negative_code_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)) + ((dst_negative_scale_table_commutative_sourcevaluemasklookup) + (dst_negative_scale_table_commutative_sourcevaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemasklookuppositive. ff_h_pvs_table_commutative_sourcevaluemasklookuppositive + S (dst_positive_table_commutative_sourcevaluemasklookup) = S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_positive_scale_table_commutative_sourcevaluemasklookup)) /\ exists ff_q_pvs_table_commutative_sourcevaluemasklookuppositive. dst_positive_code_table_commutative_sourcevaluemasklookup = ff_q_pvs_table_commutative_sourcevaluemasklookuppositive * S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_positive_scale_table_commutative_sourcevaluemasklookup) + (dst_positive_table_commutative_sourcevaluemasklookup))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemasklookupnegative. ff_h_pvs_table_commutative_sourcevaluemasklookupnegative + S (dst_negative_table_commutative_sourcevaluemasklookup) = S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_negative_scale_table_commutative_sourcevaluemasklookup)) /\ exists ff_q_pvs_table_commutative_sourcevaluemasklookupnegative. dst_negative_code_table_commutative_sourcevaluemasklookup = ff_q_pvs_table_commutative_sourcevaluemasklookupnegative * S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_negative_scale_table_commutative_sourcevaluemasklookup) + (dst_negative_table_commutative_sourcevaluemasklookup))) /\ (exists ge_balance_positive_table_commutative_sourcevaluemasklookupvalue ge_balance_negative_table_commutative_sourcevaluemasklookupvalue. (((((dc_value_table_commutative_sourcevaluemask) = 2 * (ge_balance_positive_table_commutative_sourcevaluemasklookupvalue) /\ (ge_balance_negative_table_commutative_sourcevaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemasklookupvaluedecode. (((dc_value_table_commutative_sourcevaluemask) = 2 * ge_signed_half_table_commutative_sourcevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcevaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcevaluemasklookupvalue) = S ge_signed_half_table_commutative_sourcevaluemasklookupvaluedecode))) /\ ((dst_positive_table_commutative_sourcevaluemasklookup) + ge_balance_negative_table_commutative_sourcevaluemasklookupvalue = (dst_negative_table_commutative_sourcevaluemasklookup) + ge_balance_positive_table_commutative_sourcevaluemasklookupvalue))))))))) -> ((((~((dc_index_table_commutative_sourcevaluemask)=0)) /\ (exists dc_quotient_table_commutative_sourcevaluemaskentry dc_left_table_commutative_sourcevaluemaskentry dc_right_table_commutative_sourcevaluemaskentry. (((dc_input_table_commutative_source)=(dc_index_table_commutative_sourcevaluemask)*dc_quotient_table_commutative_sourcevaluemaskentry) /\ (((exists dst_positive_code_table_commutative_sourcevaluemaskentryleft dst_positive_scale_table_commutative_sourcevaluemaskentryleft dst_negative_code_table_commutative_sourcevaluemaskentryleft dst_negative_scale_table_commutative_sourcevaluemaskentryleft dst_positive_table_commutative_sourcevaluemaskentryleft dst_negative_table_commutative_sourcevaluemaskentryleft. (((F) = (((((dst_positive_code_table_commutative_sourcevaluemaskentryleft) + (dst_positive_scale_table_commutative_sourcevaluemaskentryleft)) * S ((dst_positive_code_table_commutative_sourcevaluemaskentryleft) + (dst_positive_scale_table_commutative_sourcevaluemaskentryleft)) + ((dst_positive_scale_table_commutative_sourcevaluemaskentryleft) + (dst_positive_scale_table_commutative_sourcevaluemaskentryleft))) + (((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)))) * S ((((dst_positive_code_table_commutative_sourcevaluemaskentryleft) + (dst_positive_scale_table_commutative_sourcevaluemaskentryleft)) * S ((dst_positive_code_table_commutative_sourcevaluemaskentryleft) + (dst_positive_scale_table_commutative_sourcevaluemaskentryleft)) + ((dst_positive_scale_table_commutative_sourcevaluemaskentryleft) + (dst_positive_scale_table_commutative_sourcevaluemaskentryleft))) + (((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)))) + ((((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft))) + (((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryleft) + (dst_negative_scale_table_commutative_sourcevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemaskentryleftpositive. ff_h_pvs_table_commutative_sourcevaluemaskentryleftpositive + S (dst_positive_table_commutative_sourcevaluemaskentryleft) = S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_positive_scale_table_commutative_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_table_commutative_sourcevaluemaskentryleftpositive. dst_positive_code_table_commutative_sourcevaluemaskentryleft = ff_q_pvs_table_commutative_sourcevaluemaskentryleftpositive * S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_positive_scale_table_commutative_sourcevaluemaskentryleft) + (dst_positive_table_commutative_sourcevaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemaskentryleftnegative. ff_h_pvs_table_commutative_sourcevaluemaskentryleftnegative + S (dst_negative_table_commutative_sourcevaluemaskentryleft) = S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_negative_scale_table_commutative_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_table_commutative_sourcevaluemaskentryleftnegative. dst_negative_code_table_commutative_sourcevaluemaskentryleft = ff_q_pvs_table_commutative_sourcevaluemaskentryleftnegative * S ((S (dc_index_table_commutative_sourcevaluemask)) * dst_negative_scale_table_commutative_sourcevaluemaskentryleft) + (dst_negative_table_commutative_sourcevaluemaskentryleft))) /\ (exists ge_balance_positive_table_commutative_sourcevaluemaskentryleftvalue ge_balance_negative_table_commutative_sourcevaluemaskentryleftvalue. (((((dc_left_table_commutative_sourcevaluemaskentry) = 2 * (ge_balance_positive_table_commutative_sourcevaluemaskentryleftvalue) /\ (ge_balance_negative_table_commutative_sourcevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemaskentryleftvaluedecode. (((dc_left_table_commutative_sourcevaluemaskentry) = 2 * ge_signed_half_table_commutative_sourcevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcevaluemaskentryleftvalue) = S ge_signed_half_table_commutative_sourcevaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_commutative_sourcevaluemaskentryleft) + ge_balance_negative_table_commutative_sourcevaluemaskentryleftvalue = (dst_negative_table_commutative_sourcevaluemaskentryleft) + ge_balance_positive_table_commutative_sourcevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_commutative_sourcevaluemaskentryright dst_positive_scale_table_commutative_sourcevaluemaskentryright dst_negative_code_table_commutative_sourcevaluemaskentryright dst_negative_scale_table_commutative_sourcevaluemaskentryright dst_positive_table_commutative_sourcevaluemaskentryright dst_negative_table_commutative_sourcevaluemaskentryright. (((G) = (((((dst_positive_code_table_commutative_sourcevaluemaskentryright) + (dst_positive_scale_table_commutative_sourcevaluemaskentryright)) * S ((dst_positive_code_table_commutative_sourcevaluemaskentryright) + (dst_positive_scale_table_commutative_sourcevaluemaskentryright)) + ((dst_positive_scale_table_commutative_sourcevaluemaskentryright) + (dst_positive_scale_table_commutative_sourcevaluemaskentryright))) + (((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)))) * S ((((dst_positive_code_table_commutative_sourcevaluemaskentryright) + (dst_positive_scale_table_commutative_sourcevaluemaskentryright)) * S ((dst_positive_code_table_commutative_sourcevaluemaskentryright) + (dst_positive_scale_table_commutative_sourcevaluemaskentryright)) + ((dst_positive_scale_table_commutative_sourcevaluemaskentryright) + (dst_positive_scale_table_commutative_sourcevaluemaskentryright))) + (((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)))) + ((((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright))) + (((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) * S ((dst_negative_code_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)) + ((dst_negative_scale_table_commutative_sourcevaluemaskentryright) + (dst_negative_scale_table_commutative_sourcevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemaskentryrightpositive. ff_h_pvs_table_commutative_sourcevaluemaskentryrightpositive + S (dst_positive_table_commutative_sourcevaluemaskentryright) = S ((S (dc_quotient_table_commutative_sourcevaluemaskentry)) * dst_positive_scale_table_commutative_sourcevaluemaskentryright)) /\ exists ff_q_pvs_table_commutative_sourcevaluemaskentryrightpositive. dst_positive_code_table_commutative_sourcevaluemaskentryright = ff_q_pvs_table_commutative_sourcevaluemaskentryrightpositive * S ((S (dc_quotient_table_commutative_sourcevaluemaskentry)) * dst_positive_scale_table_commutative_sourcevaluemaskentryright) + (dst_positive_table_commutative_sourcevaluemaskentryright))) /\ (((((exists ff_h_pvs_table_commutative_sourcevaluemaskentryrightnegative. ff_h_pvs_table_commutative_sourcevaluemaskentryrightnegative + S (dst_negative_table_commutative_sourcevaluemaskentryright) = S ((S (dc_quotient_table_commutative_sourcevaluemaskentry)) * dst_negative_scale_table_commutative_sourcevaluemaskentryright)) /\ exists ff_q_pvs_table_commutative_sourcevaluemaskentryrightnegative. dst_negative_code_table_commutative_sourcevaluemaskentryright = ff_q_pvs_table_commutative_sourcevaluemaskentryrightnegative * S ((S (dc_quotient_table_commutative_sourcevaluemaskentry)) * dst_negative_scale_table_commutative_sourcevaluemaskentryright) + (dst_negative_table_commutative_sourcevaluemaskentryright))) /\ (exists ge_balance_positive_table_commutative_sourcevaluemaskentryrightvalue ge_balance_negative_table_commutative_sourcevaluemaskentryrightvalue. (((((dc_right_table_commutative_sourcevaluemaskentry) = 2 * (ge_balance_positive_table_commutative_sourcevaluemaskentryrightvalue) /\ (ge_balance_negative_table_commutative_sourcevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemaskentryrightvaluedecode. (((dc_right_table_commutative_sourcevaluemaskentry) = 2 * ge_signed_half_table_commutative_sourcevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_commutative_sourcevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_commutative_sourcevaluemaskentryrightvalue) = S ge_signed_half_table_commutative_sourcevaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_commutative_sourcevaluemaskentryright) + ge_balance_negative_table_commutative_sourcevaluemaskentryrightvalue = (dst_negative_table_commutative_sourcevaluemaskentryright) + ge_balance_positive_table_commutative_sourcevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_commutative_sourcevaluemaskentryproduct sto_an_table_commutative_sourcevaluemaskentryproduct sto_bp_table_commutative_sourcevaluemaskentryproduct sto_bn_table_commutative_sourcevaluemaskentryproduct sto_cp_table_commutative_sourcevaluemaskentryproduct sto_cn_table_commutative_sourcevaluemaskentryproduct. (((((dc_left_table_commutative_sourcevaluemaskentry) = 2 * (sto_ap_table_commutative_sourcevaluemaskentryproduct) /\ (sto_an_table_commutative_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemaskentryproductleft. (((dc_left_table_commutative_sourcevaluemaskentry) = 2 * ge_signed_half_table_commutative_sourcevaluemaskentryproductleft + 1 /\ (sto_ap_table_commutative_sourcevaluemaskentryproduct) = 0) /\ (sto_an_table_commutative_sourcevaluemaskentryproduct) = S ge_signed_half_table_commutative_sourcevaluemaskentryproductleft))) /\ ((((((dc_right_table_commutative_sourcevaluemaskentry) = 2 * (sto_bp_table_commutative_sourcevaluemaskentryproduct) /\ (sto_bn_table_commutative_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemaskentryproductright. (((dc_right_table_commutative_sourcevaluemaskentry) = 2 * ge_signed_half_table_commutative_sourcevaluemaskentryproductright + 1 /\ (sto_bp_table_commutative_sourcevaluemaskentryproduct) = 0) /\ (sto_bn_table_commutative_sourcevaluemaskentryproduct) = S ge_signed_half_table_commutative_sourcevaluemaskentryproductright))) /\ ((((((dc_value_table_commutative_sourcevaluemask) = 2 * (sto_cp_table_commutative_sourcevaluemaskentryproduct) /\ (sto_cn_table_commutative_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluemaskentryproductoutput. (((dc_value_table_commutative_sourcevaluemask) = 2 * ge_signed_half_table_commutative_sourcevaluemaskentryproductoutput + 1 /\ (sto_cp_table_commutative_sourcevaluemaskentryproduct) = 0) /\ (sto_cn_table_commutative_sourcevaluemaskentryproduct) = S ge_signed_half_table_commutative_sourcevaluemaskentryproductoutput))) /\ ((sto_ap_table_commutative_sourcevaluemaskentryproduct * sto_bp_table_commutative_sourcevaluemaskentryproduct + sto_an_table_commutative_sourcevaluemaskentryproduct * sto_bn_table_commutative_sourcevaluemaskentryproduct) + sto_cn_table_commutative_sourcevaluemaskentryproduct = (sto_ap_table_commutative_sourcevaluemaskentryproduct * sto_bn_table_commutative_sourcevaluemaskentryproduct + sto_an_table_commutative_sourcevaluemaskentryproduct * sto_bp_table_commutative_sourcevaluemaskentryproduct) + sto_cp_table_commutative_sourcevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_commutative_sourcevaluemask)=0 \/ ~(exists pvs_factor_table_commutative_sourcevaluemaskentrynondivisor. (dc_input_table_commutative_source) = (dc_index_table_commutative_sourcevaluemask) * pvs_factor_table_commutative_sourcevaluemaskentrynondivisor)) /\ ((dc_value_table_commutative_sourcevaluemask)=0))))))) /\ (exists dst_positive_code_table_commutative_sourcevaluefold dst_positive_scale_table_commutative_sourcevaluefold dst_negative_code_table_commutative_sourcevaluefold dst_negative_scale_table_commutative_sourcevaluefold dst_positive_sum_table_commutative_sourcevaluefold dst_negative_sum_table_commutative_sourcevaluefold. (((dc_mask_table_commutative_sourcevalue) = (((((dst_positive_code_table_commutative_sourcevaluefold) + (dst_positive_scale_table_commutative_sourcevaluefold)) * S ((dst_positive_code_table_commutative_sourcevaluefold) + (dst_positive_scale_table_commutative_sourcevaluefold)) + ((dst_positive_scale_table_commutative_sourcevaluefold) + (dst_positive_scale_table_commutative_sourcevaluefold))) + (((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) * S ((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) + ((dst_negative_scale_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)))) * S ((((dst_positive_code_table_commutative_sourcevaluefold) + (dst_positive_scale_table_commutative_sourcevaluefold)) * S ((dst_positive_code_table_commutative_sourcevaluefold) + (dst_positive_scale_table_commutative_sourcevaluefold)) + ((dst_positive_scale_table_commutative_sourcevaluefold) + (dst_positive_scale_table_commutative_sourcevaluefold))) + (((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) * S ((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) + ((dst_negative_scale_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)))) + ((((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) * S ((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) + ((dst_negative_scale_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold))) + (((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) * S ((dst_negative_code_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)) + ((dst_negative_scale_table_commutative_sourcevaluefold) + (dst_negative_scale_table_commutative_sourcevaluefold)))))) /\ (((exists fs_u_dst_table_commutative_sourcevaluefoldpositive fs_v_dst_table_commutative_sourcevaluefoldpositive. ((((exists fs_h_dst_table_commutative_sourcevaluefoldpositive_body_start. fs_h_dst_table_commutative_sourcevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_commutative_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldpositive_body_start. fs_u_dst_table_commutative_sourcevaluefoldpositive = fs_q_dst_table_commutative_sourcevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_commutative_sourcevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_commutative_sourcevaluefoldpositive_body_terminal. fs_h_dst_table_commutative_sourcevaluefoldpositive_body_terminal + S (dst_positive_sum_table_commutative_sourcevaluefold) = S ((S (S (dc_input_table_commutative_source))) * fs_v_dst_table_commutative_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldpositive_body_terminal. fs_u_dst_table_commutative_sourcevaluefoldpositive = fs_q_dst_table_commutative_sourcevaluefoldpositive_body_terminal * S ((S (S (dc_input_table_commutative_source))) * fs_v_dst_table_commutative_sourcevaluefoldpositive) + (dst_positive_sum_table_commutative_sourcevaluefold))) /\ forall fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps. (exists fs_lt_dst_table_commutative_sourcevaluefoldpositive_body_steps_bound. fs_lt_dst_table_commutative_sourcevaluefoldpositive_body_steps_bound + S fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps = S (dc_input_table_commutative_source)) -> exists fs_a_dst_table_commutative_sourcevaluefoldpositive_body_steps fs_r_dst_table_commutative_sourcevaluefoldpositive_body_steps fs_s_dst_table_commutative_sourcevaluefoldpositive_body_steps. ((((exists fs_h_dst_table_commutative_sourcevaluefoldpositive_body_steps_summand. fs_h_dst_table_commutative_sourcevaluefoldpositive_body_steps_summand + S (fs_a_dst_table_commutative_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_table_commutative_sourcevaluefold)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldpositive_body_steps_summand. dst_positive_code_table_commutative_sourcevaluefold = fs_q_dst_table_commutative_sourcevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_table_commutative_sourcevaluefold) + (fs_a_dst_table_commutative_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_commutative_sourcevaluefoldpositive_body_steps_partial. fs_h_dst_table_commutative_sourcevaluefoldpositive_body_steps_partial + S (fs_r_dst_table_commutative_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldpositive_body_steps_partial. fs_u_dst_table_commutative_sourcevaluefoldpositive = fs_q_dst_table_commutative_sourcevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldpositive) + (fs_r_dst_table_commutative_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_commutative_sourcevaluefoldpositive_body_steps_successor. fs_h_dst_table_commutative_sourcevaluefoldpositive_body_steps_successor + S (fs_s_dst_table_commutative_sourcevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldpositive_body_steps_successor. fs_u_dst_table_commutative_sourcevaluefoldpositive = fs_q_dst_table_commutative_sourcevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_commutative_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldpositive) + (fs_s_dst_table_commutative_sourcevaluefoldpositive_body_steps))) /\ fs_s_dst_table_commutative_sourcevaluefoldpositive_body_steps = fs_r_dst_table_commutative_sourcevaluefoldpositive_body_steps + fs_a_dst_table_commutative_sourcevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_commutative_sourcevaluefoldnegative fs_v_dst_table_commutative_sourcevaluefoldnegative. ((((exists fs_h_dst_table_commutative_sourcevaluefoldnegative_body_start. fs_h_dst_table_commutative_sourcevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_commutative_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldnegative_body_start. fs_u_dst_table_commutative_sourcevaluefoldnegative = fs_q_dst_table_commutative_sourcevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_commutative_sourcevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_commutative_sourcevaluefoldnegative_body_terminal. fs_h_dst_table_commutative_sourcevaluefoldnegative_body_terminal + S (dst_negative_sum_table_commutative_sourcevaluefold) = S ((S (S (dc_input_table_commutative_source))) * fs_v_dst_table_commutative_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldnegative_body_terminal. fs_u_dst_table_commutative_sourcevaluefoldnegative = fs_q_dst_table_commutative_sourcevaluefoldnegative_body_terminal * S ((S (S (dc_input_table_commutative_source))) * fs_v_dst_table_commutative_sourcevaluefoldnegative) + (dst_negative_sum_table_commutative_sourcevaluefold))) /\ forall fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps. (exists fs_lt_dst_table_commutative_sourcevaluefoldnegative_body_steps_bound. fs_lt_dst_table_commutative_sourcevaluefoldnegative_body_steps_bound + S fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps = S (dc_input_table_commutative_source)) -> exists fs_a_dst_table_commutative_sourcevaluefoldnegative_body_steps fs_r_dst_table_commutative_sourcevaluefoldnegative_body_steps fs_s_dst_table_commutative_sourcevaluefoldnegative_body_steps. ((((exists fs_h_dst_table_commutative_sourcevaluefoldnegative_body_steps_summand. fs_h_dst_table_commutative_sourcevaluefoldnegative_body_steps_summand + S (fs_a_dst_table_commutative_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_table_commutative_sourcevaluefold)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldnegative_body_steps_summand. dst_negative_code_table_commutative_sourcevaluefold = fs_q_dst_table_commutative_sourcevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_table_commutative_sourcevaluefold) + (fs_a_dst_table_commutative_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_commutative_sourcevaluefoldnegative_body_steps_partial. fs_h_dst_table_commutative_sourcevaluefoldnegative_body_steps_partial + S (fs_r_dst_table_commutative_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldnegative_body_steps_partial. fs_u_dst_table_commutative_sourcevaluefoldnegative = fs_q_dst_table_commutative_sourcevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldnegative) + (fs_r_dst_table_commutative_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_commutative_sourcevaluefoldnegative_body_steps_successor. fs_h_dst_table_commutative_sourcevaluefoldnegative_body_steps_successor + S (fs_s_dst_table_commutative_sourcevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_commutative_sourcevaluefoldnegative_body_steps_successor. fs_u_dst_table_commutative_sourcevaluefoldnegative = fs_q_dst_table_commutative_sourcevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_commutative_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_sourcevaluefoldnegative) + (fs_s_dst_table_commutative_sourcevaluefoldnegative_body_steps))) /\ fs_s_dst_table_commutative_sourcevaluefoldnegative_body_steps = fs_r_dst_table_commutative_sourcevaluefoldnegative_body_steps + fs_a_dst_table_commutative_sourcevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_commutative_sourcevaluefoldresult ge_balance_negative_table_commutative_sourcevaluefoldresult. (((((dc_output_table_commutative_source) = 2 * (ge_balance_positive_table_commutative_sourcevaluefoldresult) /\ (ge_balance_negative_table_commutative_sourcevaluefoldresult) = 0) \/ exists ge_signed_half_table_commutative_sourcevaluefoldresultdecode. (((dc_output_table_commutative_source) = 2 * ge_signed_half_table_commutative_sourcevaluefoldresultdecode + 1 /\ (ge_balance_positive_table_commutative_sourcevaluefoldresult) = 0) /\ (ge_balance_negative_table_commutative_sourcevaluefoldresult) = S ge_signed_half_table_commutative_sourcevaluefoldresultdecode))) /\ ((dst_positive_sum_table_commutative_sourcevaluefold) + ge_balance_negative_table_commutative_sourcevaluefoldresult = (dst_negative_sum_table_commutative_sourcevaluefold) + ge_balance_positive_table_commutative_sourcevaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_table_commutative_resultleft dst_positive_scale_table_commutative_resultleft dst_negative_code_table_commutative_resultleft dst_negative_scale_table_commutative_resultleft. (((G) = (((((dst_positive_code_table_commutative_resultleft) + (dst_positive_scale_table_commutative_resultleft)) * S ((dst_positive_code_table_commutative_resultleft) + (dst_positive_scale_table_commutative_resultleft)) + ((dst_positive_scale_table_commutative_resultleft) + (dst_positive_scale_table_commutative_resultleft))) + (((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) * S ((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) + ((dst_negative_scale_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)))) * S ((((dst_positive_code_table_commutative_resultleft) + (dst_positive_scale_table_commutative_resultleft)) * S ((dst_positive_code_table_commutative_resultleft) + (dst_positive_scale_table_commutative_resultleft)) + ((dst_positive_scale_table_commutative_resultleft) + (dst_positive_scale_table_commutative_resultleft))) + (((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) * S ((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) + ((dst_negative_scale_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)))) + ((((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) * S ((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) + ((dst_negative_scale_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft))) + (((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) * S ((dst_negative_code_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)) + ((dst_negative_scale_table_commutative_resultleft) + (dst_negative_scale_table_commutative_resultleft)))))) /\ (forall dst_index_table_commutative_resultleft. (exists pvs_le_gap_table_commutative_resultleftdomain. pvs_le_gap_table_commutative_resultleftdomain + (dst_index_table_commutative_resultleft) = (N)) -> exists dst_positive_table_commutative_resultleft dst_negative_table_commutative_resultleft dst_value_table_commutative_resultleft. ((((exists ff_h_pvs_table_commutative_resultleftentrypositive. ff_h_pvs_table_commutative_resultleftentrypositive + S (dst_positive_table_commutative_resultleft) = S ((S (dst_index_table_commutative_resultleft)) * dst_positive_scale_table_commutative_resultleft)) /\ exists ff_q_pvs_table_commutative_resultleftentrypositive. dst_positive_code_table_commutative_resultleft = ff_q_pvs_table_commutative_resultleftentrypositive * S ((S (dst_index_table_commutative_resultleft)) * dst_positive_scale_table_commutative_resultleft) + (dst_positive_table_commutative_resultleft))) /\ (((((exists ff_h_pvs_table_commutative_resultleftentrynegative. ff_h_pvs_table_commutative_resultleftentrynegative + S (dst_negative_table_commutative_resultleft) = S ((S (dst_index_table_commutative_resultleft)) * dst_negative_scale_table_commutative_resultleft)) /\ exists ff_q_pvs_table_commutative_resultleftentrynegative. dst_negative_code_table_commutative_resultleft = ff_q_pvs_table_commutative_resultleftentrynegative * S ((S (dst_index_table_commutative_resultleft)) * dst_negative_scale_table_commutative_resultleft) + (dst_negative_table_commutative_resultleft))) /\ (exists ge_balance_positive_table_commutative_resultleftentryvalue ge_balance_negative_table_commutative_resultleftentryvalue. (((((dst_value_table_commutative_resultleft) = 2 * (ge_balance_positive_table_commutative_resultleftentryvalue) /\ (ge_balance_negative_table_commutative_resultleftentryvalue) = 0) \/ exists ge_signed_half_table_commutative_resultleftentryvaluedecode. (((dst_value_table_commutative_resultleft) = 2 * ge_signed_half_table_commutative_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultleftentryvalue) = 0) /\ (ge_balance_negative_table_commutative_resultleftentryvalue) = S ge_signed_half_table_commutative_resultleftentryvaluedecode))) /\ ((dst_positive_table_commutative_resultleft) + ge_balance_negative_table_commutative_resultleftentryvalue = (dst_negative_table_commutative_resultleft) + ge_balance_positive_table_commutative_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_table_commutative_resultright dst_positive_scale_table_commutative_resultright dst_negative_code_table_commutative_resultright dst_negative_scale_table_commutative_resultright. (((F) = (((((dst_positive_code_table_commutative_resultright) + (dst_positive_scale_table_commutative_resultright)) * S ((dst_positive_code_table_commutative_resultright) + (dst_positive_scale_table_commutative_resultright)) + ((dst_positive_scale_table_commutative_resultright) + (dst_positive_scale_table_commutative_resultright))) + (((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) * S ((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) + ((dst_negative_scale_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)))) * S ((((dst_positive_code_table_commutative_resultright) + (dst_positive_scale_table_commutative_resultright)) * S ((dst_positive_code_table_commutative_resultright) + (dst_positive_scale_table_commutative_resultright)) + ((dst_positive_scale_table_commutative_resultright) + (dst_positive_scale_table_commutative_resultright))) + (((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) * S ((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) + ((dst_negative_scale_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)))) + ((((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) * S ((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) + ((dst_negative_scale_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright))) + (((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) * S ((dst_negative_code_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)) + ((dst_negative_scale_table_commutative_resultright) + (dst_negative_scale_table_commutative_resultright)))))) /\ (forall dst_index_table_commutative_resultright. (exists pvs_le_gap_table_commutative_resultrightdomain. pvs_le_gap_table_commutative_resultrightdomain + (dst_index_table_commutative_resultright) = (N)) -> exists dst_positive_table_commutative_resultright dst_negative_table_commutative_resultright dst_value_table_commutative_resultright. ((((exists ff_h_pvs_table_commutative_resultrightentrypositive. ff_h_pvs_table_commutative_resultrightentrypositive + S (dst_positive_table_commutative_resultright) = S ((S (dst_index_table_commutative_resultright)) * dst_positive_scale_table_commutative_resultright)) /\ exists ff_q_pvs_table_commutative_resultrightentrypositive. dst_positive_code_table_commutative_resultright = ff_q_pvs_table_commutative_resultrightentrypositive * S ((S (dst_index_table_commutative_resultright)) * dst_positive_scale_table_commutative_resultright) + (dst_positive_table_commutative_resultright))) /\ (((((exists ff_h_pvs_table_commutative_resultrightentrynegative. ff_h_pvs_table_commutative_resultrightentrynegative + S (dst_negative_table_commutative_resultright) = S ((S (dst_index_table_commutative_resultright)) * dst_negative_scale_table_commutative_resultright)) /\ exists ff_q_pvs_table_commutative_resultrightentrynegative. dst_negative_code_table_commutative_resultright = ff_q_pvs_table_commutative_resultrightentrynegative * S ((S (dst_index_table_commutative_resultright)) * dst_negative_scale_table_commutative_resultright) + (dst_negative_table_commutative_resultright))) /\ (exists ge_balance_positive_table_commutative_resultrightentryvalue ge_balance_negative_table_commutative_resultrightentryvalue. (((((dst_value_table_commutative_resultright) = 2 * (ge_balance_positive_table_commutative_resultrightentryvalue) /\ (ge_balance_negative_table_commutative_resultrightentryvalue) = 0) \/ exists ge_signed_half_table_commutative_resultrightentryvaluedecode. (((dst_value_table_commutative_resultright) = 2 * ge_signed_half_table_commutative_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultrightentryvalue) = 0) /\ (ge_balance_negative_table_commutative_resultrightentryvalue) = S ge_signed_half_table_commutative_resultrightentryvaluedecode))) /\ ((dst_positive_table_commutative_resultright) + ge_balance_negative_table_commutative_resultrightentryvalue = (dst_negative_table_commutative_resultright) + ge_balance_positive_table_commutative_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_table_commutative_resulttable dst_positive_scale_table_commutative_resulttable dst_negative_code_table_commutative_resulttable dst_negative_scale_table_commutative_resulttable. (((H) = (((((dst_positive_code_table_commutative_resulttable) + (dst_positive_scale_table_commutative_resulttable)) * S ((dst_positive_code_table_commutative_resulttable) + (dst_positive_scale_table_commutative_resulttable)) + ((dst_positive_scale_table_commutative_resulttable) + (dst_positive_scale_table_commutative_resulttable))) + (((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) * S ((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) + ((dst_negative_scale_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)))) * S ((((dst_positive_code_table_commutative_resulttable) + (dst_positive_scale_table_commutative_resulttable)) * S ((dst_positive_code_table_commutative_resulttable) + (dst_positive_scale_table_commutative_resulttable)) + ((dst_positive_scale_table_commutative_resulttable) + (dst_positive_scale_table_commutative_resulttable))) + (((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) * S ((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) + ((dst_negative_scale_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)))) + ((((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) * S ((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) + ((dst_negative_scale_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable))) + (((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) * S ((dst_negative_code_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)) + ((dst_negative_scale_table_commutative_resulttable) + (dst_negative_scale_table_commutative_resulttable)))))) /\ (forall dst_index_table_commutative_resulttable. (exists pvs_le_gap_table_commutative_resulttabledomain. pvs_le_gap_table_commutative_resulttabledomain + (dst_index_table_commutative_resulttable) = (N)) -> exists dst_positive_table_commutative_resulttable dst_negative_table_commutative_resulttable dst_value_table_commutative_resulttable. ((((exists ff_h_pvs_table_commutative_resulttableentrypositive. ff_h_pvs_table_commutative_resulttableentrypositive + S (dst_positive_table_commutative_resulttable) = S ((S (dst_index_table_commutative_resulttable)) * dst_positive_scale_table_commutative_resulttable)) /\ exists ff_q_pvs_table_commutative_resulttableentrypositive. dst_positive_code_table_commutative_resulttable = ff_q_pvs_table_commutative_resulttableentrypositive * S ((S (dst_index_table_commutative_resulttable)) * dst_positive_scale_table_commutative_resulttable) + (dst_positive_table_commutative_resulttable))) /\ (((((exists ff_h_pvs_table_commutative_resulttableentrynegative. ff_h_pvs_table_commutative_resulttableentrynegative + S (dst_negative_table_commutative_resulttable) = S ((S (dst_index_table_commutative_resulttable)) * dst_negative_scale_table_commutative_resulttable)) /\ exists ff_q_pvs_table_commutative_resulttableentrynegative. dst_negative_code_table_commutative_resulttable = ff_q_pvs_table_commutative_resulttableentrynegative * S ((S (dst_index_table_commutative_resulttable)) * dst_negative_scale_table_commutative_resulttable) + (dst_negative_table_commutative_resulttable))) /\ (exists ge_balance_positive_table_commutative_resulttableentryvalue ge_balance_negative_table_commutative_resulttableentryvalue. (((((dst_value_table_commutative_resulttable) = 2 * (ge_balance_positive_table_commutative_resulttableentryvalue) /\ (ge_balance_negative_table_commutative_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_commutative_resulttableentryvaluedecode. (((dst_value_table_commutative_resulttable) = 2 * ge_signed_half_table_commutative_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_commutative_resulttableentryvalue) = S ge_signed_half_table_commutative_resulttableentryvaluedecode))) /\ ((dst_positive_table_commutative_resulttable) + ge_balance_negative_table_commutative_resulttableentryvalue = (dst_negative_table_commutative_resulttable) + ge_balance_positive_table_commutative_resulttableentryvalue))))))))) /\ (forall dc_input_table_commutative_result dc_output_table_commutative_result. ~(dc_input_table_commutative_result=0) -> (exists pvs_le_gap_table_commutative_resultdomain. pvs_le_gap_table_commutative_resultdomain + (dc_input_table_commutative_result) = (N)) -> (exists dst_positive_code_table_commutative_resultlookup dst_positive_scale_table_commutative_resultlookup dst_negative_code_table_commutative_resultlookup dst_negative_scale_table_commutative_resultlookup dst_positive_table_commutative_resultlookup dst_negative_table_commutative_resultlookup. (((H) = (((((dst_positive_code_table_commutative_resultlookup) + (dst_positive_scale_table_commutative_resultlookup)) * S ((dst_positive_code_table_commutative_resultlookup) + (dst_positive_scale_table_commutative_resultlookup)) + ((dst_positive_scale_table_commutative_resultlookup) + (dst_positive_scale_table_commutative_resultlookup))) + (((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) * S ((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) + ((dst_negative_scale_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)))) * S ((((dst_positive_code_table_commutative_resultlookup) + (dst_positive_scale_table_commutative_resultlookup)) * S ((dst_positive_code_table_commutative_resultlookup) + (dst_positive_scale_table_commutative_resultlookup)) + ((dst_positive_scale_table_commutative_resultlookup) + (dst_positive_scale_table_commutative_resultlookup))) + (((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) * S ((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) + ((dst_negative_scale_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)))) + ((((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) * S ((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) + ((dst_negative_scale_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup))) + (((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) * S ((dst_negative_code_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)) + ((dst_negative_scale_table_commutative_resultlookup) + (dst_negative_scale_table_commutative_resultlookup)))))) /\ (((((exists ff_h_pvs_table_commutative_resultlookuppositive. ff_h_pvs_table_commutative_resultlookuppositive + S (dst_positive_table_commutative_resultlookup) = S ((S (dc_input_table_commutative_result)) * dst_positive_scale_table_commutative_resultlookup)) /\ exists ff_q_pvs_table_commutative_resultlookuppositive. dst_positive_code_table_commutative_resultlookup = ff_q_pvs_table_commutative_resultlookuppositive * S ((S (dc_input_table_commutative_result)) * dst_positive_scale_table_commutative_resultlookup) + (dst_positive_table_commutative_resultlookup))) /\ (((((exists ff_h_pvs_table_commutative_resultlookupnegative. ff_h_pvs_table_commutative_resultlookupnegative + S (dst_negative_table_commutative_resultlookup) = S ((S (dc_input_table_commutative_result)) * dst_negative_scale_table_commutative_resultlookup)) /\ exists ff_q_pvs_table_commutative_resultlookupnegative. dst_negative_code_table_commutative_resultlookup = ff_q_pvs_table_commutative_resultlookupnegative * S ((S (dc_input_table_commutative_result)) * dst_negative_scale_table_commutative_resultlookup) + (dst_negative_table_commutative_resultlookup))) /\ (exists ge_balance_positive_table_commutative_resultlookupvalue ge_balance_negative_table_commutative_resultlookupvalue. (((((dc_output_table_commutative_result) = 2 * (ge_balance_positive_table_commutative_resultlookupvalue) /\ (ge_balance_negative_table_commutative_resultlookupvalue) = 0) \/ exists ge_signed_half_table_commutative_resultlookupvaluedecode. (((dc_output_table_commutative_result) = 2 * ge_signed_half_table_commutative_resultlookupvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultlookupvalue) = 0) /\ (ge_balance_negative_table_commutative_resultlookupvalue) = S ge_signed_half_table_commutative_resultlookupvaluedecode))) /\ ((dst_positive_table_commutative_resultlookup) + ge_balance_negative_table_commutative_resultlookupvalue = (dst_negative_table_commutative_resultlookup) + ge_balance_positive_table_commutative_resultlookupvalue))))))))) -> (((~((dc_input_table_commutative_result)=0)) /\ (exists dc_mask_table_commutative_resultvalue. ((((exists dst_positive_code_table_commutative_resultvaluemasktable dst_positive_scale_table_commutative_resultvaluemasktable dst_negative_code_table_commutative_resultvaluemasktable dst_negative_scale_table_commutative_resultvaluemasktable. (((dc_mask_table_commutative_resultvalue) = (((((dst_positive_code_table_commutative_resultvaluemasktable) + (dst_positive_scale_table_commutative_resultvaluemasktable)) * S ((dst_positive_code_table_commutative_resultvaluemasktable) + (dst_positive_scale_table_commutative_resultvaluemasktable)) + ((dst_positive_scale_table_commutative_resultvaluemasktable) + (dst_positive_scale_table_commutative_resultvaluemasktable))) + (((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) * S ((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) + ((dst_negative_scale_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)))) * S ((((dst_positive_code_table_commutative_resultvaluemasktable) + (dst_positive_scale_table_commutative_resultvaluemasktable)) * S ((dst_positive_code_table_commutative_resultvaluemasktable) + (dst_positive_scale_table_commutative_resultvaluemasktable)) + ((dst_positive_scale_table_commutative_resultvaluemasktable) + (dst_positive_scale_table_commutative_resultvaluemasktable))) + (((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) * S ((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) + ((dst_negative_scale_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)))) + ((((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) * S ((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) + ((dst_negative_scale_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable))) + (((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) * S ((dst_negative_code_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)) + ((dst_negative_scale_table_commutative_resultvaluemasktable) + (dst_negative_scale_table_commutative_resultvaluemasktable)))))) /\ (forall dst_index_table_commutative_resultvaluemasktable. (exists pvs_le_gap_table_commutative_resultvaluemasktabledomain. pvs_le_gap_table_commutative_resultvaluemasktabledomain + (dst_index_table_commutative_resultvaluemasktable) = (dc_input_table_commutative_result)) -> exists dst_positive_table_commutative_resultvaluemasktable dst_negative_table_commutative_resultvaluemasktable dst_value_table_commutative_resultvaluemasktable. ((((exists ff_h_pvs_table_commutative_resultvaluemasktableentrypositive. ff_h_pvs_table_commutative_resultvaluemasktableentrypositive + S (dst_positive_table_commutative_resultvaluemasktable) = S ((S (dst_index_table_commutative_resultvaluemasktable)) * dst_positive_scale_table_commutative_resultvaluemasktable)) /\ exists ff_q_pvs_table_commutative_resultvaluemasktableentrypositive. dst_positive_code_table_commutative_resultvaluemasktable = ff_q_pvs_table_commutative_resultvaluemasktableentrypositive * S ((S (dst_index_table_commutative_resultvaluemasktable)) * dst_positive_scale_table_commutative_resultvaluemasktable) + (dst_positive_table_commutative_resultvaluemasktable))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemasktableentrynegative. ff_h_pvs_table_commutative_resultvaluemasktableentrynegative + S (dst_negative_table_commutative_resultvaluemasktable) = S ((S (dst_index_table_commutative_resultvaluemasktable)) * dst_negative_scale_table_commutative_resultvaluemasktable)) /\ exists ff_q_pvs_table_commutative_resultvaluemasktableentrynegative. dst_negative_code_table_commutative_resultvaluemasktable = ff_q_pvs_table_commutative_resultvaluemasktableentrynegative * S ((S (dst_index_table_commutative_resultvaluemasktable)) * dst_negative_scale_table_commutative_resultvaluemasktable) + (dst_negative_table_commutative_resultvaluemasktable))) /\ (exists ge_balance_positive_table_commutative_resultvaluemasktableentryvalue ge_balance_negative_table_commutative_resultvaluemasktableentryvalue. (((((dst_value_table_commutative_resultvaluemasktable) = 2 * (ge_balance_positive_table_commutative_resultvaluemasktableentryvalue) /\ (ge_balance_negative_table_commutative_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemasktableentryvaluedecode. (((dst_value_table_commutative_resultvaluemasktable) = 2 * ge_signed_half_table_commutative_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_commutative_resultvaluemasktableentryvalue) = S ge_signed_half_table_commutative_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_commutative_resultvaluemasktable) + ge_balance_negative_table_commutative_resultvaluemasktableentryvalue = (dst_negative_table_commutative_resultvaluemasktable) + ge_balance_positive_table_commutative_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_commutative_resultvaluemask dc_value_table_commutative_resultvaluemask. (exists pvs_le_gap_table_commutative_resultvaluemaskdomain. pvs_le_gap_table_commutative_resultvaluemaskdomain + (dc_index_table_commutative_resultvaluemask) = (dc_input_table_commutative_result)) -> (exists dst_positive_code_table_commutative_resultvaluemasklookup dst_positive_scale_table_commutative_resultvaluemasklookup dst_negative_code_table_commutative_resultvaluemasklookup dst_negative_scale_table_commutative_resultvaluemasklookup dst_positive_table_commutative_resultvaluemasklookup dst_negative_table_commutative_resultvaluemasklookup. (((dc_mask_table_commutative_resultvalue) = (((((dst_positive_code_table_commutative_resultvaluemasklookup) + (dst_positive_scale_table_commutative_resultvaluemasklookup)) * S ((dst_positive_code_table_commutative_resultvaluemasklookup) + (dst_positive_scale_table_commutative_resultvaluemasklookup)) + ((dst_positive_scale_table_commutative_resultvaluemasklookup) + (dst_positive_scale_table_commutative_resultvaluemasklookup))) + (((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) * S ((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) + ((dst_negative_scale_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)))) * S ((((dst_positive_code_table_commutative_resultvaluemasklookup) + (dst_positive_scale_table_commutative_resultvaluemasklookup)) * S ((dst_positive_code_table_commutative_resultvaluemasklookup) + (dst_positive_scale_table_commutative_resultvaluemasklookup)) + ((dst_positive_scale_table_commutative_resultvaluemasklookup) + (dst_positive_scale_table_commutative_resultvaluemasklookup))) + (((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) * S ((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) + ((dst_negative_scale_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)))) + ((((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) * S ((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) + ((dst_negative_scale_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup))) + (((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) * S ((dst_negative_code_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)) + ((dst_negative_scale_table_commutative_resultvaluemasklookup) + (dst_negative_scale_table_commutative_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemasklookuppositive. ff_h_pvs_table_commutative_resultvaluemasklookuppositive + S (dst_positive_table_commutative_resultvaluemasklookup) = S ((S (dc_index_table_commutative_resultvaluemask)) * dst_positive_scale_table_commutative_resultvaluemasklookup)) /\ exists ff_q_pvs_table_commutative_resultvaluemasklookuppositive. dst_positive_code_table_commutative_resultvaluemasklookup = ff_q_pvs_table_commutative_resultvaluemasklookuppositive * S ((S (dc_index_table_commutative_resultvaluemask)) * dst_positive_scale_table_commutative_resultvaluemasklookup) + (dst_positive_table_commutative_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemasklookupnegative. ff_h_pvs_table_commutative_resultvaluemasklookupnegative + S (dst_negative_table_commutative_resultvaluemasklookup) = S ((S (dc_index_table_commutative_resultvaluemask)) * dst_negative_scale_table_commutative_resultvaluemasklookup)) /\ exists ff_q_pvs_table_commutative_resultvaluemasklookupnegative. dst_negative_code_table_commutative_resultvaluemasklookup = ff_q_pvs_table_commutative_resultvaluemasklookupnegative * S ((S (dc_index_table_commutative_resultvaluemask)) * dst_negative_scale_table_commutative_resultvaluemasklookup) + (dst_negative_table_commutative_resultvaluemasklookup))) /\ (exists ge_balance_positive_table_commutative_resultvaluemasklookupvalue ge_balance_negative_table_commutative_resultvaluemasklookupvalue. (((((dc_value_table_commutative_resultvaluemask) = 2 * (ge_balance_positive_table_commutative_resultvaluemasklookupvalue) /\ (ge_balance_negative_table_commutative_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemasklookupvaluedecode. (((dc_value_table_commutative_resultvaluemask) = 2 * ge_signed_half_table_commutative_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_commutative_resultvaluemasklookupvalue) = S ge_signed_half_table_commutative_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_table_commutative_resultvaluemasklookup) + ge_balance_negative_table_commutative_resultvaluemasklookupvalue = (dst_negative_table_commutative_resultvaluemasklookup) + ge_balance_positive_table_commutative_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_commutative_resultvaluemask)=0)) /\ (exists dc_quotient_table_commutative_resultvaluemaskentry dc_left_table_commutative_resultvaluemaskentry dc_right_table_commutative_resultvaluemaskentry. (((dc_input_table_commutative_result)=(dc_index_table_commutative_resultvaluemask)*dc_quotient_table_commutative_resultvaluemaskentry) /\ (((exists dst_positive_code_table_commutative_resultvaluemaskentryleft dst_positive_scale_table_commutative_resultvaluemaskentryleft dst_negative_code_table_commutative_resultvaluemaskentryleft dst_negative_scale_table_commutative_resultvaluemaskentryleft dst_positive_table_commutative_resultvaluemaskentryleft dst_negative_table_commutative_resultvaluemaskentryleft. (((G) = (((((dst_positive_code_table_commutative_resultvaluemaskentryleft) + (dst_positive_scale_table_commutative_resultvaluemaskentryleft)) * S ((dst_positive_code_table_commutative_resultvaluemaskentryleft) + (dst_positive_scale_table_commutative_resultvaluemaskentryleft)) + ((dst_positive_scale_table_commutative_resultvaluemaskentryleft) + (dst_positive_scale_table_commutative_resultvaluemaskentryleft))) + (((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)))) * S ((((dst_positive_code_table_commutative_resultvaluemaskentryleft) + (dst_positive_scale_table_commutative_resultvaluemaskentryleft)) * S ((dst_positive_code_table_commutative_resultvaluemaskentryleft) + (dst_positive_scale_table_commutative_resultvaluemaskentryleft)) + ((dst_positive_scale_table_commutative_resultvaluemaskentryleft) + (dst_positive_scale_table_commutative_resultvaluemaskentryleft))) + (((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)))) + ((((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft))) + (((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryleft) + (dst_negative_scale_table_commutative_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemaskentryleftpositive. ff_h_pvs_table_commutative_resultvaluemaskentryleftpositive + S (dst_positive_table_commutative_resultvaluemaskentryleft) = S ((S (dc_index_table_commutative_resultvaluemask)) * dst_positive_scale_table_commutative_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_commutative_resultvaluemaskentryleftpositive. dst_positive_code_table_commutative_resultvaluemaskentryleft = ff_q_pvs_table_commutative_resultvaluemaskentryleftpositive * S ((S (dc_index_table_commutative_resultvaluemask)) * dst_positive_scale_table_commutative_resultvaluemaskentryleft) + (dst_positive_table_commutative_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemaskentryleftnegative. ff_h_pvs_table_commutative_resultvaluemaskentryleftnegative + S (dst_negative_table_commutative_resultvaluemaskentryleft) = S ((S (dc_index_table_commutative_resultvaluemask)) * dst_negative_scale_table_commutative_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_commutative_resultvaluemaskentryleftnegative. dst_negative_code_table_commutative_resultvaluemaskentryleft = ff_q_pvs_table_commutative_resultvaluemaskentryleftnegative * S ((S (dc_index_table_commutative_resultvaluemask)) * dst_negative_scale_table_commutative_resultvaluemaskentryleft) + (dst_negative_table_commutative_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_table_commutative_resultvaluemaskentryleftvalue ge_balance_negative_table_commutative_resultvaluemaskentryleftvalue. (((((dc_left_table_commutative_resultvaluemaskentry) = 2 * (ge_balance_positive_table_commutative_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_table_commutative_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemaskentryleftvaluedecode. (((dc_left_table_commutative_resultvaluemaskentry) = 2 * ge_signed_half_table_commutative_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_commutative_resultvaluemaskentryleftvalue) = S ge_signed_half_table_commutative_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_commutative_resultvaluemaskentryleft) + ge_balance_negative_table_commutative_resultvaluemaskentryleftvalue = (dst_negative_table_commutative_resultvaluemaskentryleft) + ge_balance_positive_table_commutative_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_commutative_resultvaluemaskentryright dst_positive_scale_table_commutative_resultvaluemaskentryright dst_negative_code_table_commutative_resultvaluemaskentryright dst_negative_scale_table_commutative_resultvaluemaskentryright dst_positive_table_commutative_resultvaluemaskentryright dst_negative_table_commutative_resultvaluemaskentryright. (((F) = (((((dst_positive_code_table_commutative_resultvaluemaskentryright) + (dst_positive_scale_table_commutative_resultvaluemaskentryright)) * S ((dst_positive_code_table_commutative_resultvaluemaskentryright) + (dst_positive_scale_table_commutative_resultvaluemaskentryright)) + ((dst_positive_scale_table_commutative_resultvaluemaskentryright) + (dst_positive_scale_table_commutative_resultvaluemaskentryright))) + (((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)))) * S ((((dst_positive_code_table_commutative_resultvaluemaskentryright) + (dst_positive_scale_table_commutative_resultvaluemaskentryright)) * S ((dst_positive_code_table_commutative_resultvaluemaskentryright) + (dst_positive_scale_table_commutative_resultvaluemaskentryright)) + ((dst_positive_scale_table_commutative_resultvaluemaskentryright) + (dst_positive_scale_table_commutative_resultvaluemaskentryright))) + (((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)))) + ((((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright))) + (((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) * S ((dst_negative_code_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)) + ((dst_negative_scale_table_commutative_resultvaluemaskentryright) + (dst_negative_scale_table_commutative_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemaskentryrightpositive. ff_h_pvs_table_commutative_resultvaluemaskentryrightpositive + S (dst_positive_table_commutative_resultvaluemaskentryright) = S ((S (dc_quotient_table_commutative_resultvaluemaskentry)) * dst_positive_scale_table_commutative_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_commutative_resultvaluemaskentryrightpositive. dst_positive_code_table_commutative_resultvaluemaskentryright = ff_q_pvs_table_commutative_resultvaluemaskentryrightpositive * S ((S (dc_quotient_table_commutative_resultvaluemaskentry)) * dst_positive_scale_table_commutative_resultvaluemaskentryright) + (dst_positive_table_commutative_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_commutative_resultvaluemaskentryrightnegative. ff_h_pvs_table_commutative_resultvaluemaskentryrightnegative + S (dst_negative_table_commutative_resultvaluemaskentryright) = S ((S (dc_quotient_table_commutative_resultvaluemaskentry)) * dst_negative_scale_table_commutative_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_commutative_resultvaluemaskentryrightnegative. dst_negative_code_table_commutative_resultvaluemaskentryright = ff_q_pvs_table_commutative_resultvaluemaskentryrightnegative * S ((S (dc_quotient_table_commutative_resultvaluemaskentry)) * dst_negative_scale_table_commutative_resultvaluemaskentryright) + (dst_negative_table_commutative_resultvaluemaskentryright))) /\ (exists ge_balance_positive_table_commutative_resultvaluemaskentryrightvalue ge_balance_negative_table_commutative_resultvaluemaskentryrightvalue. (((((dc_right_table_commutative_resultvaluemaskentry) = 2 * (ge_balance_positive_table_commutative_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_table_commutative_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemaskentryrightvaluedecode. (((dc_right_table_commutative_resultvaluemaskentry) = 2 * ge_signed_half_table_commutative_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_commutative_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_commutative_resultvaluemaskentryrightvalue) = S ge_signed_half_table_commutative_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_commutative_resultvaluemaskentryright) + ge_balance_negative_table_commutative_resultvaluemaskentryrightvalue = (dst_negative_table_commutative_resultvaluemaskentryright) + ge_balance_positive_table_commutative_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_commutative_resultvaluemaskentryproduct sto_an_table_commutative_resultvaluemaskentryproduct sto_bp_table_commutative_resultvaluemaskentryproduct sto_bn_table_commutative_resultvaluemaskentryproduct sto_cp_table_commutative_resultvaluemaskentryproduct sto_cn_table_commutative_resultvaluemaskentryproduct. (((((dc_left_table_commutative_resultvaluemaskentry) = 2 * (sto_ap_table_commutative_resultvaluemaskentryproduct) /\ (sto_an_table_commutative_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemaskentryproductleft. (((dc_left_table_commutative_resultvaluemaskentry) = 2 * ge_signed_half_table_commutative_resultvaluemaskentryproductleft + 1 /\ (sto_ap_table_commutative_resultvaluemaskentryproduct) = 0) /\ (sto_an_table_commutative_resultvaluemaskentryproduct) = S ge_signed_half_table_commutative_resultvaluemaskentryproductleft))) /\ ((((((dc_right_table_commutative_resultvaluemaskentry) = 2 * (sto_bp_table_commutative_resultvaluemaskentryproduct) /\ (sto_bn_table_commutative_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemaskentryproductright. (((dc_right_table_commutative_resultvaluemaskentry) = 2 * ge_signed_half_table_commutative_resultvaluemaskentryproductright + 1 /\ (sto_bp_table_commutative_resultvaluemaskentryproduct) = 0) /\ (sto_bn_table_commutative_resultvaluemaskentryproduct) = S ge_signed_half_table_commutative_resultvaluemaskentryproductright))) /\ ((((((dc_value_table_commutative_resultvaluemask) = 2 * (sto_cp_table_commutative_resultvaluemaskentryproduct) /\ (sto_cn_table_commutative_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_commutative_resultvaluemaskentryproductoutput. (((dc_value_table_commutative_resultvaluemask) = 2 * ge_signed_half_table_commutative_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_table_commutative_resultvaluemaskentryproduct) = 0) /\ (sto_cn_table_commutative_resultvaluemaskentryproduct) = S ge_signed_half_table_commutative_resultvaluemaskentryproductoutput))) /\ ((sto_ap_table_commutative_resultvaluemaskentryproduct * sto_bp_table_commutative_resultvaluemaskentryproduct + sto_an_table_commutative_resultvaluemaskentryproduct * sto_bn_table_commutative_resultvaluemaskentryproduct) + sto_cn_table_commutative_resultvaluemaskentryproduct = (sto_ap_table_commutative_resultvaluemaskentryproduct * sto_bn_table_commutative_resultvaluemaskentryproduct + sto_an_table_commutative_resultvaluemaskentryproduct * sto_bp_table_commutative_resultvaluemaskentryproduct) + sto_cp_table_commutative_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_commutative_resultvaluemask)=0 \/ ~(exists pvs_factor_table_commutative_resultvaluemaskentrynondivisor. (dc_input_table_commutative_result) = (dc_index_table_commutative_resultvaluemask) * pvs_factor_table_commutative_resultvaluemaskentrynondivisor)) /\ ((dc_value_table_commutative_resultvaluemask)=0))))))) /\ (exists dst_positive_code_table_commutative_resultvaluefold dst_positive_scale_table_commutative_resultvaluefold dst_negative_code_table_commutative_resultvaluefold dst_negative_scale_table_commutative_resultvaluefold dst_positive_sum_table_commutative_resultvaluefold dst_negative_sum_table_commutative_resultvaluefold. (((dc_mask_table_commutative_resultvalue) = (((((dst_positive_code_table_commutative_resultvaluefold) + (dst_positive_scale_table_commutative_resultvaluefold)) * S ((dst_positive_code_table_commutative_resultvaluefold) + (dst_positive_scale_table_commutative_resultvaluefold)) + ((dst_positive_scale_table_commutative_resultvaluefold) + (dst_positive_scale_table_commutative_resultvaluefold))) + (((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) * S ((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) + ((dst_negative_scale_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)))) * S ((((dst_positive_code_table_commutative_resultvaluefold) + (dst_positive_scale_table_commutative_resultvaluefold)) * S ((dst_positive_code_table_commutative_resultvaluefold) + (dst_positive_scale_table_commutative_resultvaluefold)) + ((dst_positive_scale_table_commutative_resultvaluefold) + (dst_positive_scale_table_commutative_resultvaluefold))) + (((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) * S ((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) + ((dst_negative_scale_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)))) + ((((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) * S ((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) + ((dst_negative_scale_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold))) + (((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) * S ((dst_negative_code_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)) + ((dst_negative_scale_table_commutative_resultvaluefold) + (dst_negative_scale_table_commutative_resultvaluefold)))))) /\ (((exists fs_u_dst_table_commutative_resultvaluefoldpositive fs_v_dst_table_commutative_resultvaluefoldpositive. ((((exists fs_h_dst_table_commutative_resultvaluefoldpositive_body_start. fs_h_dst_table_commutative_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_commutative_resultvaluefoldpositive)) /\ exists fs_q_dst_table_commutative_resultvaluefoldpositive_body_start. fs_u_dst_table_commutative_resultvaluefoldpositive = fs_q_dst_table_commutative_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_commutative_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_commutative_resultvaluefoldpositive_body_terminal. fs_h_dst_table_commutative_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_table_commutative_resultvaluefold) = S ((S (S (dc_input_table_commutative_result))) * fs_v_dst_table_commutative_resultvaluefoldpositive)) /\ exists fs_q_dst_table_commutative_resultvaluefoldpositive_body_terminal. fs_u_dst_table_commutative_resultvaluefoldpositive = fs_q_dst_table_commutative_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_commutative_result))) * fs_v_dst_table_commutative_resultvaluefoldpositive) + (dst_positive_sum_table_commutative_resultvaluefold))) /\ forall fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_table_commutative_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_table_commutative_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps = S (dc_input_table_commutative_result)) -> exists fs_a_dst_table_commutative_resultvaluefoldpositive_body_steps fs_r_dst_table_commutative_resultvaluefoldpositive_body_steps fs_s_dst_table_commutative_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_commutative_resultvaluefoldpositive_body_steps_summand. fs_h_dst_table_commutative_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_commutative_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_commutative_resultvaluefold)) /\ exists fs_q_dst_table_commutative_resultvaluefoldpositive_body_steps_summand. dst_positive_code_table_commutative_resultvaluefold = fs_q_dst_table_commutative_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_commutative_resultvaluefold) + (fs_a_dst_table_commutative_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_commutative_resultvaluefoldpositive_body_steps_partial. fs_h_dst_table_commutative_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_commutative_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldpositive)) /\ exists fs_q_dst_table_commutative_resultvaluefoldpositive_body_steps_partial. fs_u_dst_table_commutative_resultvaluefoldpositive = fs_q_dst_table_commutative_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldpositive) + (fs_r_dst_table_commutative_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_commutative_resultvaluefoldpositive_body_steps_successor. fs_h_dst_table_commutative_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_commutative_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldpositive)) /\ exists fs_q_dst_table_commutative_resultvaluefoldpositive_body_steps_successor. fs_u_dst_table_commutative_resultvaluefoldpositive = fs_q_dst_table_commutative_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_commutative_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldpositive) + (fs_s_dst_table_commutative_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_table_commutative_resultvaluefoldpositive_body_steps = fs_r_dst_table_commutative_resultvaluefoldpositive_body_steps + fs_a_dst_table_commutative_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_commutative_resultvaluefoldnegative fs_v_dst_table_commutative_resultvaluefoldnegative. ((((exists fs_h_dst_table_commutative_resultvaluefoldnegative_body_start. fs_h_dst_table_commutative_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_commutative_resultvaluefoldnegative)) /\ exists fs_q_dst_table_commutative_resultvaluefoldnegative_body_start. fs_u_dst_table_commutative_resultvaluefoldnegative = fs_q_dst_table_commutative_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_commutative_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_commutative_resultvaluefoldnegative_body_terminal. fs_h_dst_table_commutative_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_table_commutative_resultvaluefold) = S ((S (S (dc_input_table_commutative_result))) * fs_v_dst_table_commutative_resultvaluefoldnegative)) /\ exists fs_q_dst_table_commutative_resultvaluefoldnegative_body_terminal. fs_u_dst_table_commutative_resultvaluefoldnegative = fs_q_dst_table_commutative_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_commutative_result))) * fs_v_dst_table_commutative_resultvaluefoldnegative) + (dst_negative_sum_table_commutative_resultvaluefold))) /\ forall fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_table_commutative_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_table_commutative_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps = S (dc_input_table_commutative_result)) -> exists fs_a_dst_table_commutative_resultvaluefoldnegative_body_steps fs_r_dst_table_commutative_resultvaluefoldnegative_body_steps fs_s_dst_table_commutative_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_commutative_resultvaluefoldnegative_body_steps_summand. fs_h_dst_table_commutative_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_commutative_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_commutative_resultvaluefold)) /\ exists fs_q_dst_table_commutative_resultvaluefoldnegative_body_steps_summand. dst_negative_code_table_commutative_resultvaluefold = fs_q_dst_table_commutative_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_commutative_resultvaluefold) + (fs_a_dst_table_commutative_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_commutative_resultvaluefoldnegative_body_steps_partial. fs_h_dst_table_commutative_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_commutative_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldnegative)) /\ exists fs_q_dst_table_commutative_resultvaluefoldnegative_body_steps_partial. fs_u_dst_table_commutative_resultvaluefoldnegative = fs_q_dst_table_commutative_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldnegative) + (fs_r_dst_table_commutative_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_commutative_resultvaluefoldnegative_body_steps_successor. fs_h_dst_table_commutative_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_commutative_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldnegative)) /\ exists fs_q_dst_table_commutative_resultvaluefoldnegative_body_steps_successor. fs_u_dst_table_commutative_resultvaluefoldnegative = fs_q_dst_table_commutative_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_commutative_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_commutative_resultvaluefoldnegative) + (fs_s_dst_table_commutative_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_table_commutative_resultvaluefoldnegative_body_steps = fs_r_dst_table_commutative_resultvaluefoldnegative_body_steps + fs_a_dst_table_commutative_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_commutative_resultvaluefoldresult ge_balance_negative_table_commutative_resultvaluefoldresult. (((((dc_output_table_commutative_result) = 2 * (ge_balance_positive_table_commutative_resultvaluefoldresult) /\ (ge_balance_negative_table_commutative_resultvaluefoldresult) = 0) \/ exists ge_signed_half_table_commutative_resultvaluefoldresultdecode. (((dc_output_table_commutative_result) = 2 * ge_signed_half_table_commutative_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_commutative_resultvaluefoldresult) = 0) /\ (ge_balance_negative_table_commutative_resultvaluefoldresult) = S ge_signed_half_table_commutative_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_table_commutative_resultvaluefold) + ge_balance_negative_table_commutative_resultvaluefoldresult = (dst_negative_sum_table_commutative_resultvaluefold) + ge_balance_positive_table_commutative_resultvaluefoldresult))))))))))))))))))))Complete tactic proof in conservative notation
All 34 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
34 script commands · 10 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–9
03Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact h_right_left
04Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
split
05Use earlier factsL12–12
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L12
exact h_left
06Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
split
07Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact h_right_right_left
08Fix variables and assumptionsL15–19
09Use earlier factsL20–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
specialize dirichlet_convolution_sum_swap (N) - L21
specialize dirichlet_convolution_sum_swap (F) - L22
specialize dirichlet_convolution_sum_swap (G) - L23
specialize dirichlet_convolution_sum_swap (n) - L24
specialize dirichlet_convolution_sum_swap (z) - L25
apply dirichlet_convolution_sum_swap - L26
exact h_left - L27
exact h_right_left - L28
exact hbound - L29
specialize h_right_right_right (n)
Original defined command ledger · 34 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro h - 0006
cases h - 0007
cases h_right - 0008
cases h_right_right - 0009
split - 0010
exact h_right_left - 0011
split - 0012
exact h_left - 0013
split - 0014
exact h_right_right_left - 0015
intro n - 0016
intro z - 0017
intro hn - 0018
intro hbound - 0019
intro hz - 0020
specialize dirichlet_convolution_sum_swap (N) - 0021
specialize dirichlet_convolution_sum_swap (F) - 0022
specialize dirichlet_convolution_sum_swap (G) - 0023
specialize dirichlet_convolution_sum_swap (n) - 0024
specialize dirichlet_convolution_sum_swap (z) - 0025
apply dirichlet_convolution_sum_swap - 0026
exact h_left - 0027
exact h_right_left - 0028
exact hbound - 0029
specialize h_right_right_right (n) - 0030
specialize h_right_right_right (z) - 0031
apply h_right_right_right - 0032
exact hn - 0033
exact hbound - 0034
exact hz