Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N F G H U n a V z. (exists dst_positive_code_row_entry_F dst_positive_scale_row_entry_F dst_negative_code_row_entry_F dst_negative_scale_row_entry_F. (((F) = (((((dst_positive_code_row_entry_F) + (dst_positive_scale_row_entry_F)) * S ((dst_positive_code_row_entry_F) + (dst_positive_scale_row_entry_F)) + ((dst_positive_scale_row_entry_F) + (dst_positive_scale_row_entry_F))) + (((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) * S ((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) + ((dst_negative_scale_row_entry_F) + (dst_negative_scale_row_entry_F)))) * S ((((dst_positive_code_row_entry_F) + (dst_positive_scale_row_entry_F)) * S ((dst_positive_code_row_entry_F) + (dst_positive_scale_row_entry_F)) + ((dst_positive_scale_row_entry_F) + (dst_positive_scale_row_entry_F))) + (((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) * S ((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) + ((dst_negative_scale_row_entry_F) + (dst_negative_scale_row_entry_F)))) + ((((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) * S ((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) + ((dst_negative_scale_row_entry_F) + (dst_negative_scale_row_entry_F))) + (((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) * S ((dst_negative_code_row_entry_F) + (dst_negative_scale_row_entry_F)) + ((dst_negative_scale_row_entry_F) + (dst_negative_scale_row_entry_F)))))) /\ (forall dst_index_row_entry_F. (exists pvs_le_gap_row_entry_Fdomain. pvs_le_gap_row_entry_Fdomain + (dst_index_row_entry_F) = (N)) -> exists dst_positive_row_entry_F dst_negative_row_entry_F dst_value_row_entry_F. ((((exists ff_h_pvs_row_entry_Fentrypositive. ff_h_pvs_row_entry_Fentrypositive + S (dst_positive_row_entry_F) = S ((S (dst_index_row_entry_F)) * dst_positive_scale_row_entry_F)) /\ exists ff_q_pvs_row_entry_Fentrypositive. dst_positive_code_row_entry_F = ff_q_pvs_row_entry_Fentrypositive * S ((S (dst_index_row_entry_F)) * dst_positive_scale_row_entry_F) + (dst_positive_row_entry_F))) /\ (((((exists ff_h_pvs_row_entry_Fentrynegative. ff_h_pvs_row_entry_Fentrynegative + S (dst_negative_row_entry_F) = S ((S (dst_index_row_entry_F)) * dst_negative_scale_row_entry_F)) /\ exists ff_q_pvs_row_entry_Fentrynegative. dst_negative_code_row_entry_F = ff_q_pvs_row_entry_Fentrynegative * S ((S (dst_index_row_entry_F)) * dst_negative_scale_row_entry_F) + (dst_negative_row_entry_F))) /\ (exists ge_balance_positive_row_entry_Fentryvalue ge_balance_negative_row_entry_Fentryvalue. (((((dst_value_row_entry_F) = 2 * (ge_balance_positive_row_entry_Fentryvalue) /\ (ge_balance_negative_row_entry_Fentryvalue) = 0) \/ exists ge_signed_half_row_entry_Fentryvaluedecode. (((dst_value_row_entry_F) = 2 * ge_signed_half_row_entry_Fentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_Fentryvalue) = 0) /\ (ge_balance_negative_row_entry_Fentryvalue) = S ge_signed_half_row_entry_Fentryvaluedecode))) /\ ((dst_positive_row_entry_F) + ge_balance_negative_row_entry_Fentryvalue = (dst_negative_row_entry_F) + ge_balance_positive_row_entry_Fentryvalue))))))))) -> (((exists dst_positive_code_row_entry_inner_tableleft dst_positive_scale_row_entry_inner_tableleft dst_negative_code_row_entry_inner_tableleft dst_negative_scale_row_entry_inner_tableleft. (((H) = (((((dst_positive_code_row_entry_inner_tableleft) + (dst_positive_scale_row_entry_inner_tableleft)) * S ((dst_positive_code_row_entry_inner_tableleft) + (dst_positive_scale_row_entry_inner_tableleft)) + ((dst_positive_scale_row_entry_inner_tableleft) + (dst_positive_scale_row_entry_inner_tableleft))) + (((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) * S ((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) + ((dst_negative_scale_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)))) * S ((((dst_positive_code_row_entry_inner_tableleft) + (dst_positive_scale_row_entry_inner_tableleft)) * S ((dst_positive_code_row_entry_inner_tableleft) + (dst_positive_scale_row_entry_inner_tableleft)) + ((dst_positive_scale_row_entry_inner_tableleft) + (dst_positive_scale_row_entry_inner_tableleft))) + (((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) * S ((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) + ((dst_negative_scale_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)))) + ((((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) * S ((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) + ((dst_negative_scale_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft))) + (((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) * S ((dst_negative_code_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)) + ((dst_negative_scale_row_entry_inner_tableleft) + (dst_negative_scale_row_entry_inner_tableleft)))))) /\ (forall dst_index_row_entry_inner_tableleft. (exists pvs_le_gap_row_entry_inner_tableleftdomain. pvs_le_gap_row_entry_inner_tableleftdomain + (dst_index_row_entry_inner_tableleft) = (N)) -> exists dst_positive_row_entry_inner_tableleft dst_negative_row_entry_inner_tableleft dst_value_row_entry_inner_tableleft. ((((exists ff_h_pvs_row_entry_inner_tableleftentrypositive. ff_h_pvs_row_entry_inner_tableleftentrypositive + S (dst_positive_row_entry_inner_tableleft) = S ((S (dst_index_row_entry_inner_tableleft)) * dst_positive_scale_row_entry_inner_tableleft)) /\ exists ff_q_pvs_row_entry_inner_tableleftentrypositive. dst_positive_code_row_entry_inner_tableleft = ff_q_pvs_row_entry_inner_tableleftentrypositive * S ((S (dst_index_row_entry_inner_tableleft)) * dst_positive_scale_row_entry_inner_tableleft) + (dst_positive_row_entry_inner_tableleft))) /\ (((((exists ff_h_pvs_row_entry_inner_tableleftentrynegative. ff_h_pvs_row_entry_inner_tableleftentrynegative + S (dst_negative_row_entry_inner_tableleft) = S ((S (dst_index_row_entry_inner_tableleft)) * dst_negative_scale_row_entry_inner_tableleft)) /\ exists ff_q_pvs_row_entry_inner_tableleftentrynegative. dst_negative_code_row_entry_inner_tableleft = ff_q_pvs_row_entry_inner_tableleftentrynegative * S ((S (dst_index_row_entry_inner_tableleft)) * dst_negative_scale_row_entry_inner_tableleft) + (dst_negative_row_entry_inner_tableleft))) /\ (exists ge_balance_positive_row_entry_inner_tableleftentryvalue ge_balance_negative_row_entry_inner_tableleftentryvalue. (((((dst_value_row_entry_inner_tableleft) = 2 * (ge_balance_positive_row_entry_inner_tableleftentryvalue) /\ (ge_balance_negative_row_entry_inner_tableleftentryvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tableleftentryvaluedecode. (((dst_value_row_entry_inner_tableleft) = 2 * ge_signed_half_row_entry_inner_tableleftentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tableleftentryvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tableleftentryvalue) = S ge_signed_half_row_entry_inner_tableleftentryvaluedecode))) /\ ((dst_positive_row_entry_inner_tableleft) + ge_balance_negative_row_entry_inner_tableleftentryvalue = (dst_negative_row_entry_inner_tableleft) + ge_balance_positive_row_entry_inner_tableleftentryvalue))))))))) /\ (((exists dst_positive_code_row_entry_inner_tableright dst_positive_scale_row_entry_inner_tableright dst_negative_code_row_entry_inner_tableright dst_negative_scale_row_entry_inner_tableright. (((G) = (((((dst_positive_code_row_entry_inner_tableright) + (dst_positive_scale_row_entry_inner_tableright)) * S ((dst_positive_code_row_entry_inner_tableright) + (dst_positive_scale_row_entry_inner_tableright)) + ((dst_positive_scale_row_entry_inner_tableright) + (dst_positive_scale_row_entry_inner_tableright))) + (((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) * S ((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) + ((dst_negative_scale_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)))) * S ((((dst_positive_code_row_entry_inner_tableright) + (dst_positive_scale_row_entry_inner_tableright)) * S ((dst_positive_code_row_entry_inner_tableright) + (dst_positive_scale_row_entry_inner_tableright)) + ((dst_positive_scale_row_entry_inner_tableright) + (dst_positive_scale_row_entry_inner_tableright))) + (((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) * S ((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) + ((dst_negative_scale_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)))) + ((((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) * S ((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) + ((dst_negative_scale_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright))) + (((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) * S ((dst_negative_code_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)) + ((dst_negative_scale_row_entry_inner_tableright) + (dst_negative_scale_row_entry_inner_tableright)))))) /\ (forall dst_index_row_entry_inner_tableright. (exists pvs_le_gap_row_entry_inner_tablerightdomain. pvs_le_gap_row_entry_inner_tablerightdomain + (dst_index_row_entry_inner_tableright) = (N)) -> exists dst_positive_row_entry_inner_tableright dst_negative_row_entry_inner_tableright dst_value_row_entry_inner_tableright. ((((exists ff_h_pvs_row_entry_inner_tablerightentrypositive. ff_h_pvs_row_entry_inner_tablerightentrypositive + S (dst_positive_row_entry_inner_tableright) = S ((S (dst_index_row_entry_inner_tableright)) * dst_positive_scale_row_entry_inner_tableright)) /\ exists ff_q_pvs_row_entry_inner_tablerightentrypositive. dst_positive_code_row_entry_inner_tableright = ff_q_pvs_row_entry_inner_tablerightentrypositive * S ((S (dst_index_row_entry_inner_tableright)) * dst_positive_scale_row_entry_inner_tableright) + (dst_positive_row_entry_inner_tableright))) /\ (((((exists ff_h_pvs_row_entry_inner_tablerightentrynegative. ff_h_pvs_row_entry_inner_tablerightentrynegative + S (dst_negative_row_entry_inner_tableright) = S ((S (dst_index_row_entry_inner_tableright)) * dst_negative_scale_row_entry_inner_tableright)) /\ exists ff_q_pvs_row_entry_inner_tablerightentrynegative. dst_negative_code_row_entry_inner_tableright = ff_q_pvs_row_entry_inner_tablerightentrynegative * S ((S (dst_index_row_entry_inner_tableright)) * dst_negative_scale_row_entry_inner_tableright) + (dst_negative_row_entry_inner_tableright))) /\ (exists ge_balance_positive_row_entry_inner_tablerightentryvalue ge_balance_negative_row_entry_inner_tablerightentryvalue. (((((dst_value_row_entry_inner_tableright) = 2 * (ge_balance_positive_row_entry_inner_tablerightentryvalue) /\ (ge_balance_negative_row_entry_inner_tablerightentryvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tablerightentryvaluedecode. (((dst_value_row_entry_inner_tableright) = 2 * ge_signed_half_row_entry_inner_tablerightentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tablerightentryvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tablerightentryvalue) = S ge_signed_half_row_entry_inner_tablerightentryvaluedecode))) /\ ((dst_positive_row_entry_inner_tableright) + ge_balance_negative_row_entry_inner_tablerightentryvalue = (dst_negative_row_entry_inner_tableright) + ge_balance_positive_row_entry_inner_tablerightentryvalue))))))))) /\ (((exists dst_positive_code_row_entry_inner_tabletable dst_positive_scale_row_entry_inner_tabletable dst_negative_code_row_entry_inner_tabletable dst_negative_scale_row_entry_inner_tabletable. (((U) = (((((dst_positive_code_row_entry_inner_tabletable) + (dst_positive_scale_row_entry_inner_tabletable)) * S ((dst_positive_code_row_entry_inner_tabletable) + (dst_positive_scale_row_entry_inner_tabletable)) + ((dst_positive_scale_row_entry_inner_tabletable) + (dst_positive_scale_row_entry_inner_tabletable))) + (((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) * S ((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) + ((dst_negative_scale_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)))) * S ((((dst_positive_code_row_entry_inner_tabletable) + (dst_positive_scale_row_entry_inner_tabletable)) * S ((dst_positive_code_row_entry_inner_tabletable) + (dst_positive_scale_row_entry_inner_tabletable)) + ((dst_positive_scale_row_entry_inner_tabletable) + (dst_positive_scale_row_entry_inner_tabletable))) + (((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) * S ((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) + ((dst_negative_scale_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)))) + ((((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) * S ((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) + ((dst_negative_scale_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable))) + (((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) * S ((dst_negative_code_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)) + ((dst_negative_scale_row_entry_inner_tabletable) + (dst_negative_scale_row_entry_inner_tabletable)))))) /\ (forall dst_index_row_entry_inner_tabletable. (exists pvs_le_gap_row_entry_inner_tabletabledomain. pvs_le_gap_row_entry_inner_tabletabledomain + (dst_index_row_entry_inner_tabletable) = (N)) -> exists dst_positive_row_entry_inner_tabletable dst_negative_row_entry_inner_tabletable dst_value_row_entry_inner_tabletable. ((((exists ff_h_pvs_row_entry_inner_tabletableentrypositive. ff_h_pvs_row_entry_inner_tabletableentrypositive + S (dst_positive_row_entry_inner_tabletable) = S ((S (dst_index_row_entry_inner_tabletable)) * dst_positive_scale_row_entry_inner_tabletable)) /\ exists ff_q_pvs_row_entry_inner_tabletableentrypositive. dst_positive_code_row_entry_inner_tabletable = ff_q_pvs_row_entry_inner_tabletableentrypositive * S ((S (dst_index_row_entry_inner_tabletable)) * dst_positive_scale_row_entry_inner_tabletable) + (dst_positive_row_entry_inner_tabletable))) /\ (((((exists ff_h_pvs_row_entry_inner_tabletableentrynegative. ff_h_pvs_row_entry_inner_tabletableentrynegative + S (dst_negative_row_entry_inner_tabletable) = S ((S (dst_index_row_entry_inner_tabletable)) * dst_negative_scale_row_entry_inner_tabletable)) /\ exists ff_q_pvs_row_entry_inner_tabletableentrynegative. dst_negative_code_row_entry_inner_tabletable = ff_q_pvs_row_entry_inner_tabletableentrynegative * S ((S (dst_index_row_entry_inner_tabletable)) * dst_negative_scale_row_entry_inner_tabletable) + (dst_negative_row_entry_inner_tabletable))) /\ (exists ge_balance_positive_row_entry_inner_tabletableentryvalue ge_balance_negative_row_entry_inner_tabletableentryvalue. (((((dst_value_row_entry_inner_tabletable) = 2 * (ge_balance_positive_row_entry_inner_tabletableentryvalue) /\ (ge_balance_negative_row_entry_inner_tabletableentryvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tabletableentryvaluedecode. (((dst_value_row_entry_inner_tabletable) = 2 * ge_signed_half_row_entry_inner_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tabletableentryvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tabletableentryvalue) = S ge_signed_half_row_entry_inner_tabletableentryvaluedecode))) /\ ((dst_positive_row_entry_inner_tabletable) + ge_balance_negative_row_entry_inner_tabletableentryvalue = (dst_negative_row_entry_inner_tabletable) + ge_balance_positive_row_entry_inner_tabletableentryvalue))))))))) /\ (forall dc_input_row_entry_inner_table dc_output_row_entry_inner_table. ~(dc_input_row_entry_inner_table=0) -> (exists pvs_le_gap_row_entry_inner_tabledomain. pvs_le_gap_row_entry_inner_tabledomain + (dc_input_row_entry_inner_table) = (N)) -> (exists dst_positive_code_row_entry_inner_tablelookup dst_positive_scale_row_entry_inner_tablelookup dst_negative_code_row_entry_inner_tablelookup dst_negative_scale_row_entry_inner_tablelookup dst_positive_row_entry_inner_tablelookup dst_negative_row_entry_inner_tablelookup. (((U) = (((((dst_positive_code_row_entry_inner_tablelookup) + (dst_positive_scale_row_entry_inner_tablelookup)) * S ((dst_positive_code_row_entry_inner_tablelookup) + (dst_positive_scale_row_entry_inner_tablelookup)) + ((dst_positive_scale_row_entry_inner_tablelookup) + (dst_positive_scale_row_entry_inner_tablelookup))) + (((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) * S ((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) + ((dst_negative_scale_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)))) * S ((((dst_positive_code_row_entry_inner_tablelookup) + (dst_positive_scale_row_entry_inner_tablelookup)) * S ((dst_positive_code_row_entry_inner_tablelookup) + (dst_positive_scale_row_entry_inner_tablelookup)) + ((dst_positive_scale_row_entry_inner_tablelookup) + (dst_positive_scale_row_entry_inner_tablelookup))) + (((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) * S ((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) + ((dst_negative_scale_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)))) + ((((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) * S ((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) + ((dst_negative_scale_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup))) + (((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) * S ((dst_negative_code_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)) + ((dst_negative_scale_row_entry_inner_tablelookup) + (dst_negative_scale_row_entry_inner_tablelookup)))))) /\ (((((exists ff_h_pvs_row_entry_inner_tablelookuppositive. ff_h_pvs_row_entry_inner_tablelookuppositive + S (dst_positive_row_entry_inner_tablelookup) = S ((S (dc_input_row_entry_inner_table)) * dst_positive_scale_row_entry_inner_tablelookup)) /\ exists ff_q_pvs_row_entry_inner_tablelookuppositive. dst_positive_code_row_entry_inner_tablelookup = ff_q_pvs_row_entry_inner_tablelookuppositive * S ((S (dc_input_row_entry_inner_table)) * dst_positive_scale_row_entry_inner_tablelookup) + (dst_positive_row_entry_inner_tablelookup))) /\ (((((exists ff_h_pvs_row_entry_inner_tablelookupnegative. ff_h_pvs_row_entry_inner_tablelookupnegative + S (dst_negative_row_entry_inner_tablelookup) = S ((S (dc_input_row_entry_inner_table)) * dst_negative_scale_row_entry_inner_tablelookup)) /\ exists ff_q_pvs_row_entry_inner_tablelookupnegative. dst_negative_code_row_entry_inner_tablelookup = ff_q_pvs_row_entry_inner_tablelookupnegative * S ((S (dc_input_row_entry_inner_table)) * dst_negative_scale_row_entry_inner_tablelookup) + (dst_negative_row_entry_inner_tablelookup))) /\ (exists ge_balance_positive_row_entry_inner_tablelookupvalue ge_balance_negative_row_entry_inner_tablelookupvalue. (((((dc_output_row_entry_inner_table) = 2 * (ge_balance_positive_row_entry_inner_tablelookupvalue) /\ (ge_balance_negative_row_entry_inner_tablelookupvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tablelookupvaluedecode. (((dc_output_row_entry_inner_table) = 2 * ge_signed_half_row_entry_inner_tablelookupvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tablelookupvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tablelookupvalue) = S ge_signed_half_row_entry_inner_tablelookupvaluedecode))) /\ ((dst_positive_row_entry_inner_tablelookup) + ge_balance_negative_row_entry_inner_tablelookupvalue = (dst_negative_row_entry_inner_tablelookup) + ge_balance_positive_row_entry_inner_tablelookupvalue))))))))) -> (((~((dc_input_row_entry_inner_table)=0)) /\ (exists dc_mask_row_entry_inner_tablevalue. ((((exists dst_positive_code_row_entry_inner_tablevaluemasktable dst_positive_scale_row_entry_inner_tablevaluemasktable dst_negative_code_row_entry_inner_tablevaluemasktable dst_negative_scale_row_entry_inner_tablevaluemasktable. (((dc_mask_row_entry_inner_tablevalue) = (((((dst_positive_code_row_entry_inner_tablevaluemasktable) + (dst_positive_scale_row_entry_inner_tablevaluemasktable)) * S ((dst_positive_code_row_entry_inner_tablevaluemasktable) + (dst_positive_scale_row_entry_inner_tablevaluemasktable)) + ((dst_positive_scale_row_entry_inner_tablevaluemasktable) + (dst_positive_scale_row_entry_inner_tablevaluemasktable))) + (((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) * S ((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) + ((dst_negative_scale_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)))) * S ((((dst_positive_code_row_entry_inner_tablevaluemasktable) + (dst_positive_scale_row_entry_inner_tablevaluemasktable)) * S ((dst_positive_code_row_entry_inner_tablevaluemasktable) + (dst_positive_scale_row_entry_inner_tablevaluemasktable)) + ((dst_positive_scale_row_entry_inner_tablevaluemasktable) + (dst_positive_scale_row_entry_inner_tablevaluemasktable))) + (((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) * S ((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) + ((dst_negative_scale_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)))) + ((((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) * S ((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) + ((dst_negative_scale_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable))) + (((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) * S ((dst_negative_code_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)) + ((dst_negative_scale_row_entry_inner_tablevaluemasktable) + (dst_negative_scale_row_entry_inner_tablevaluemasktable)))))) /\ (forall dst_index_row_entry_inner_tablevaluemasktable. (exists pvs_le_gap_row_entry_inner_tablevaluemasktabledomain. pvs_le_gap_row_entry_inner_tablevaluemasktabledomain + (dst_index_row_entry_inner_tablevaluemasktable) = (dc_input_row_entry_inner_table)) -> exists dst_positive_row_entry_inner_tablevaluemasktable dst_negative_row_entry_inner_tablevaluemasktable dst_value_row_entry_inner_tablevaluemasktable. ((((exists ff_h_pvs_row_entry_inner_tablevaluemasktableentrypositive. ff_h_pvs_row_entry_inner_tablevaluemasktableentrypositive + S (dst_positive_row_entry_inner_tablevaluemasktable) = S ((S (dst_index_row_entry_inner_tablevaluemasktable)) * dst_positive_scale_row_entry_inner_tablevaluemasktable)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemasktableentrypositive. dst_positive_code_row_entry_inner_tablevaluemasktable = ff_q_pvs_row_entry_inner_tablevaluemasktableentrypositive * S ((S (dst_index_row_entry_inner_tablevaluemasktable)) * dst_positive_scale_row_entry_inner_tablevaluemasktable) + (dst_positive_row_entry_inner_tablevaluemasktable))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemasktableentrynegative. ff_h_pvs_row_entry_inner_tablevaluemasktableentrynegative + S (dst_negative_row_entry_inner_tablevaluemasktable) = S ((S (dst_index_row_entry_inner_tablevaluemasktable)) * dst_negative_scale_row_entry_inner_tablevaluemasktable)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemasktableentrynegative. dst_negative_code_row_entry_inner_tablevaluemasktable = ff_q_pvs_row_entry_inner_tablevaluemasktableentrynegative * S ((S (dst_index_row_entry_inner_tablevaluemasktable)) * dst_negative_scale_row_entry_inner_tablevaluemasktable) + (dst_negative_row_entry_inner_tablevaluemasktable))) /\ (exists ge_balance_positive_row_entry_inner_tablevaluemasktableentryvalue ge_balance_negative_row_entry_inner_tablevaluemasktableentryvalue. (((((dst_value_row_entry_inner_tablevaluemasktable) = 2 * (ge_balance_positive_row_entry_inner_tablevaluemasktableentryvalue) /\ (ge_balance_negative_row_entry_inner_tablevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemasktableentryvaluedecode. (((dst_value_row_entry_inner_tablevaluemasktable) = 2 * ge_signed_half_row_entry_inner_tablevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tablevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tablevaluemasktableentryvalue) = S ge_signed_half_row_entry_inner_tablevaluemasktableentryvaluedecode))) /\ ((dst_positive_row_entry_inner_tablevaluemasktable) + ge_balance_negative_row_entry_inner_tablevaluemasktableentryvalue = (dst_negative_row_entry_inner_tablevaluemasktable) + ge_balance_positive_row_entry_inner_tablevaluemasktableentryvalue))))))))) /\ (forall dc_index_row_entry_inner_tablevaluemask dc_value_row_entry_inner_tablevaluemask. (exists pvs_le_gap_row_entry_inner_tablevaluemaskdomain. pvs_le_gap_row_entry_inner_tablevaluemaskdomain + (dc_index_row_entry_inner_tablevaluemask) = (dc_input_row_entry_inner_table)) -> (exists dst_positive_code_row_entry_inner_tablevaluemasklookup dst_positive_scale_row_entry_inner_tablevaluemasklookup dst_negative_code_row_entry_inner_tablevaluemasklookup dst_negative_scale_row_entry_inner_tablevaluemasklookup dst_positive_row_entry_inner_tablevaluemasklookup dst_negative_row_entry_inner_tablevaluemasklookup. (((dc_mask_row_entry_inner_tablevalue) = (((((dst_positive_code_row_entry_inner_tablevaluemasklookup) + (dst_positive_scale_row_entry_inner_tablevaluemasklookup)) * S ((dst_positive_code_row_entry_inner_tablevaluemasklookup) + (dst_positive_scale_row_entry_inner_tablevaluemasklookup)) + ((dst_positive_scale_row_entry_inner_tablevaluemasklookup) + (dst_positive_scale_row_entry_inner_tablevaluemasklookup))) + (((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) * S ((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) + ((dst_negative_scale_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)))) * S ((((dst_positive_code_row_entry_inner_tablevaluemasklookup) + (dst_positive_scale_row_entry_inner_tablevaluemasklookup)) * S ((dst_positive_code_row_entry_inner_tablevaluemasklookup) + (dst_positive_scale_row_entry_inner_tablevaluemasklookup)) + ((dst_positive_scale_row_entry_inner_tablevaluemasklookup) + (dst_positive_scale_row_entry_inner_tablevaluemasklookup))) + (((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) * S ((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) + ((dst_negative_scale_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)))) + ((((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) * S ((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) + ((dst_negative_scale_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup))) + (((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) * S ((dst_negative_code_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)) + ((dst_negative_scale_row_entry_inner_tablevaluemasklookup) + (dst_negative_scale_row_entry_inner_tablevaluemasklookup)))))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemasklookuppositive. ff_h_pvs_row_entry_inner_tablevaluemasklookuppositive + S (dst_positive_row_entry_inner_tablevaluemasklookup) = S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_positive_scale_row_entry_inner_tablevaluemasklookup)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemasklookuppositive. dst_positive_code_row_entry_inner_tablevaluemasklookup = ff_q_pvs_row_entry_inner_tablevaluemasklookuppositive * S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_positive_scale_row_entry_inner_tablevaluemasklookup) + (dst_positive_row_entry_inner_tablevaluemasklookup))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemasklookupnegative. ff_h_pvs_row_entry_inner_tablevaluemasklookupnegative + S (dst_negative_row_entry_inner_tablevaluemasklookup) = S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_negative_scale_row_entry_inner_tablevaluemasklookup)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemasklookupnegative. dst_negative_code_row_entry_inner_tablevaluemasklookup = ff_q_pvs_row_entry_inner_tablevaluemasklookupnegative * S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_negative_scale_row_entry_inner_tablevaluemasklookup) + (dst_negative_row_entry_inner_tablevaluemasklookup))) /\ (exists ge_balance_positive_row_entry_inner_tablevaluemasklookupvalue ge_balance_negative_row_entry_inner_tablevaluemasklookupvalue. (((((dc_value_row_entry_inner_tablevaluemask) = 2 * (ge_balance_positive_row_entry_inner_tablevaluemasklookupvalue) /\ (ge_balance_negative_row_entry_inner_tablevaluemasklookupvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemasklookupvaluedecode. (((dc_value_row_entry_inner_tablevaluemask) = 2 * ge_signed_half_row_entry_inner_tablevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tablevaluemasklookupvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tablevaluemasklookupvalue) = S ge_signed_half_row_entry_inner_tablevaluemasklookupvaluedecode))) /\ ((dst_positive_row_entry_inner_tablevaluemasklookup) + ge_balance_negative_row_entry_inner_tablevaluemasklookupvalue = (dst_negative_row_entry_inner_tablevaluemasklookup) + ge_balance_positive_row_entry_inner_tablevaluemasklookupvalue))))))))) -> ((((~((dc_index_row_entry_inner_tablevaluemask)=0)) /\ (exists dc_quotient_row_entry_inner_tablevaluemaskentry dc_left_row_entry_inner_tablevaluemaskentry dc_right_row_entry_inner_tablevaluemaskentry. (((dc_input_row_entry_inner_table)=(dc_index_row_entry_inner_tablevaluemask)*dc_quotient_row_entry_inner_tablevaluemaskentry) /\ (((exists dst_positive_code_row_entry_inner_tablevaluemaskentryleft dst_positive_scale_row_entry_inner_tablevaluemaskentryleft dst_negative_code_row_entry_inner_tablevaluemaskentryleft dst_negative_scale_row_entry_inner_tablevaluemaskentryleft dst_positive_row_entry_inner_tablevaluemaskentryleft dst_negative_row_entry_inner_tablevaluemaskentryleft. (((H) = (((((dst_positive_code_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryleft)) * S ((dst_positive_code_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryleft)) + ((dst_positive_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryleft))) + (((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)))) * S ((((dst_positive_code_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryleft)) * S ((dst_positive_code_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryleft)) + ((dst_positive_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryleft))) + (((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)))) + ((((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft))) + (((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemaskentryleftpositive. ff_h_pvs_row_entry_inner_tablevaluemaskentryleftpositive + S (dst_positive_row_entry_inner_tablevaluemaskentryleft) = S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_positive_scale_row_entry_inner_tablevaluemaskentryleft)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemaskentryleftpositive. dst_positive_code_row_entry_inner_tablevaluemaskentryleft = ff_q_pvs_row_entry_inner_tablevaluemaskentryleftpositive * S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_positive_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_positive_row_entry_inner_tablevaluemaskentryleft))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemaskentryleftnegative. ff_h_pvs_row_entry_inner_tablevaluemaskentryleftnegative + S (dst_negative_row_entry_inner_tablevaluemaskentryleft) = S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_negative_scale_row_entry_inner_tablevaluemaskentryleft)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemaskentryleftnegative. dst_negative_code_row_entry_inner_tablevaluemaskentryleft = ff_q_pvs_row_entry_inner_tablevaluemaskentryleftnegative * S ((S (dc_index_row_entry_inner_tablevaluemask)) * dst_negative_scale_row_entry_inner_tablevaluemaskentryleft) + (dst_negative_row_entry_inner_tablevaluemaskentryleft))) /\ (exists ge_balance_positive_row_entry_inner_tablevaluemaskentryleftvalue ge_balance_negative_row_entry_inner_tablevaluemaskentryleftvalue. (((((dc_left_row_entry_inner_tablevaluemaskentry) = 2 * (ge_balance_positive_row_entry_inner_tablevaluemaskentryleftvalue) /\ (ge_balance_negative_row_entry_inner_tablevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemaskentryleftvaluedecode. (((dc_left_row_entry_inner_tablevaluemaskentry) = 2 * ge_signed_half_row_entry_inner_tablevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tablevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tablevaluemaskentryleftvalue) = S ge_signed_half_row_entry_inner_tablevaluemaskentryleftvaluedecode))) /\ ((dst_positive_row_entry_inner_tablevaluemaskentryleft) + ge_balance_negative_row_entry_inner_tablevaluemaskentryleftvalue = (dst_negative_row_entry_inner_tablevaluemaskentryleft) + ge_balance_positive_row_entry_inner_tablevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_row_entry_inner_tablevaluemaskentryright dst_positive_scale_row_entry_inner_tablevaluemaskentryright dst_negative_code_row_entry_inner_tablevaluemaskentryright dst_negative_scale_row_entry_inner_tablevaluemaskentryright dst_positive_row_entry_inner_tablevaluemaskentryright dst_negative_row_entry_inner_tablevaluemaskentryright. (((G) = (((((dst_positive_code_row_entry_inner_tablevaluemaskentryright) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryright)) * S ((dst_positive_code_row_entry_inner_tablevaluemaskentryright) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryright)) + ((dst_positive_scale_row_entry_inner_tablevaluemaskentryright) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryright))) + (((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)))) * S ((((dst_positive_code_row_entry_inner_tablevaluemaskentryright) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryright)) * S ((dst_positive_code_row_entry_inner_tablevaluemaskentryright) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryright)) + ((dst_positive_scale_row_entry_inner_tablevaluemaskentryright) + (dst_positive_scale_row_entry_inner_tablevaluemaskentryright))) + (((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)))) + ((((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright))) + (((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) * S ((dst_negative_code_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) + ((dst_negative_scale_row_entry_inner_tablevaluemaskentryright) + (dst_negative_scale_row_entry_inner_tablevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemaskentryrightpositive. ff_h_pvs_row_entry_inner_tablevaluemaskentryrightpositive + S (dst_positive_row_entry_inner_tablevaluemaskentryright) = S ((S (dc_quotient_row_entry_inner_tablevaluemaskentry)) * dst_positive_scale_row_entry_inner_tablevaluemaskentryright)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemaskentryrightpositive. dst_positive_code_row_entry_inner_tablevaluemaskentryright = ff_q_pvs_row_entry_inner_tablevaluemaskentryrightpositive * S ((S (dc_quotient_row_entry_inner_tablevaluemaskentry)) * dst_positive_scale_row_entry_inner_tablevaluemaskentryright) + (dst_positive_row_entry_inner_tablevaluemaskentryright))) /\ (((((exists ff_h_pvs_row_entry_inner_tablevaluemaskentryrightnegative. ff_h_pvs_row_entry_inner_tablevaluemaskentryrightnegative + S (dst_negative_row_entry_inner_tablevaluemaskentryright) = S ((S (dc_quotient_row_entry_inner_tablevaluemaskentry)) * dst_negative_scale_row_entry_inner_tablevaluemaskentryright)) /\ exists ff_q_pvs_row_entry_inner_tablevaluemaskentryrightnegative. dst_negative_code_row_entry_inner_tablevaluemaskentryright = ff_q_pvs_row_entry_inner_tablevaluemaskentryrightnegative * S ((S (dc_quotient_row_entry_inner_tablevaluemaskentry)) * dst_negative_scale_row_entry_inner_tablevaluemaskentryright) + (dst_negative_row_entry_inner_tablevaluemaskentryright))) /\ (exists ge_balance_positive_row_entry_inner_tablevaluemaskentryrightvalue ge_balance_negative_row_entry_inner_tablevaluemaskentryrightvalue. (((((dc_right_row_entry_inner_tablevaluemaskentry) = 2 * (ge_balance_positive_row_entry_inner_tablevaluemaskentryrightvalue) /\ (ge_balance_negative_row_entry_inner_tablevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemaskentryrightvaluedecode. (((dc_right_row_entry_inner_tablevaluemaskentry) = 2 * ge_signed_half_row_entry_inner_tablevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_row_entry_inner_tablevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_row_entry_inner_tablevaluemaskentryrightvalue) = S ge_signed_half_row_entry_inner_tablevaluemaskentryrightvaluedecode))) /\ ((dst_positive_row_entry_inner_tablevaluemaskentryright) + ge_balance_negative_row_entry_inner_tablevaluemaskentryrightvalue = (dst_negative_row_entry_inner_tablevaluemaskentryright) + ge_balance_positive_row_entry_inner_tablevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_row_entry_inner_tablevaluemaskentryproduct sto_an_row_entry_inner_tablevaluemaskentryproduct sto_bp_row_entry_inner_tablevaluemaskentryproduct sto_bn_row_entry_inner_tablevaluemaskentryproduct sto_cp_row_entry_inner_tablevaluemaskentryproduct sto_cn_row_entry_inner_tablevaluemaskentryproduct. (((((dc_left_row_entry_inner_tablevaluemaskentry) = 2 * (sto_ap_row_entry_inner_tablevaluemaskentryproduct) /\ (sto_an_row_entry_inner_tablevaluemaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemaskentryproductleft. (((dc_left_row_entry_inner_tablevaluemaskentry) = 2 * ge_signed_half_row_entry_inner_tablevaluemaskentryproductleft + 1 /\ (sto_ap_row_entry_inner_tablevaluemaskentryproduct) = 0) /\ (sto_an_row_entry_inner_tablevaluemaskentryproduct) = S ge_signed_half_row_entry_inner_tablevaluemaskentryproductleft))) /\ ((((((dc_right_row_entry_inner_tablevaluemaskentry) = 2 * (sto_bp_row_entry_inner_tablevaluemaskentryproduct) /\ (sto_bn_row_entry_inner_tablevaluemaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemaskentryproductright. (((dc_right_row_entry_inner_tablevaluemaskentry) = 2 * ge_signed_half_row_entry_inner_tablevaluemaskentryproductright + 1 /\ (sto_bp_row_entry_inner_tablevaluemaskentryproduct) = 0) /\ (sto_bn_row_entry_inner_tablevaluemaskentryproduct) = S ge_signed_half_row_entry_inner_tablevaluemaskentryproductright))) /\ ((((((dc_value_row_entry_inner_tablevaluemask) = 2 * (sto_cp_row_entry_inner_tablevaluemaskentryproduct) /\ (sto_cn_row_entry_inner_tablevaluemaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluemaskentryproductoutput. (((dc_value_row_entry_inner_tablevaluemask) = 2 * ge_signed_half_row_entry_inner_tablevaluemaskentryproductoutput + 1 /\ (sto_cp_row_entry_inner_tablevaluemaskentryproduct) = 0) /\ (sto_cn_row_entry_inner_tablevaluemaskentryproduct) = S ge_signed_half_row_entry_inner_tablevaluemaskentryproductoutput))) /\ ((sto_ap_row_entry_inner_tablevaluemaskentryproduct * sto_bp_row_entry_inner_tablevaluemaskentryproduct + sto_an_row_entry_inner_tablevaluemaskentryproduct * sto_bn_row_entry_inner_tablevaluemaskentryproduct) + sto_cn_row_entry_inner_tablevaluemaskentryproduct = (sto_ap_row_entry_inner_tablevaluemaskentryproduct * sto_bn_row_entry_inner_tablevaluemaskentryproduct + sto_an_row_entry_inner_tablevaluemaskentryproduct * sto_bp_row_entry_inner_tablevaluemaskentryproduct) + sto_cp_row_entry_inner_tablevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_row_entry_inner_tablevaluemask)=0 \/ ~(exists pvs_factor_row_entry_inner_tablevaluemaskentrynondivisor. (dc_input_row_entry_inner_table) = (dc_index_row_entry_inner_tablevaluemask) * pvs_factor_row_entry_inner_tablevaluemaskentrynondivisor)) /\ ((dc_value_row_entry_inner_tablevaluemask)=0))))))) /\ (exists dst_positive_code_row_entry_inner_tablevaluefold dst_positive_scale_row_entry_inner_tablevaluefold dst_negative_code_row_entry_inner_tablevaluefold dst_negative_scale_row_entry_inner_tablevaluefold dst_positive_sum_row_entry_inner_tablevaluefold dst_negative_sum_row_entry_inner_tablevaluefold. (((dc_mask_row_entry_inner_tablevalue) = (((((dst_positive_code_row_entry_inner_tablevaluefold) + (dst_positive_scale_row_entry_inner_tablevaluefold)) * S ((dst_positive_code_row_entry_inner_tablevaluefold) + (dst_positive_scale_row_entry_inner_tablevaluefold)) + ((dst_positive_scale_row_entry_inner_tablevaluefold) + (dst_positive_scale_row_entry_inner_tablevaluefold))) + (((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) * S ((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) + ((dst_negative_scale_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)))) * S ((((dst_positive_code_row_entry_inner_tablevaluefold) + (dst_positive_scale_row_entry_inner_tablevaluefold)) * S ((dst_positive_code_row_entry_inner_tablevaluefold) + (dst_positive_scale_row_entry_inner_tablevaluefold)) + ((dst_positive_scale_row_entry_inner_tablevaluefold) + (dst_positive_scale_row_entry_inner_tablevaluefold))) + (((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) * S ((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) + ((dst_negative_scale_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)))) + ((((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) * S ((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) + ((dst_negative_scale_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold))) + (((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) * S ((dst_negative_code_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)) + ((dst_negative_scale_row_entry_inner_tablevaluefold) + (dst_negative_scale_row_entry_inner_tablevaluefold)))))) /\ (((exists fs_u_dst_row_entry_inner_tablevaluefoldpositive fs_v_dst_row_entry_inner_tablevaluefoldpositive. ((((exists fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_start. fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_start. fs_u_dst_row_entry_inner_tablevaluefoldpositive = fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_row_entry_inner_tablevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_terminal. fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_terminal + S (dst_positive_sum_row_entry_inner_tablevaluefold) = S ((S (S (dc_input_row_entry_inner_table))) * fs_v_dst_row_entry_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_terminal. fs_u_dst_row_entry_inner_tablevaluefoldpositive = fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_terminal * S ((S (S (dc_input_row_entry_inner_table))) * fs_v_dst_row_entry_inner_tablevaluefoldpositive) + (dst_positive_sum_row_entry_inner_tablevaluefold))) /\ forall fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps. (exists fs_lt_dst_row_entry_inner_tablevaluefoldpositive_body_steps_bound. fs_lt_dst_row_entry_inner_tablevaluefoldpositive_body_steps_bound + S fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps = S (dc_input_row_entry_inner_table)) -> exists fs_a_dst_row_entry_inner_tablevaluefoldpositive_body_steps fs_r_dst_row_entry_inner_tablevaluefoldpositive_body_steps fs_s_dst_row_entry_inner_tablevaluefoldpositive_body_steps. ((((exists fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_steps_summand. fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_steps_summand + S (fs_a_dst_row_entry_inner_tablevaluefoldpositive_body_steps) = S ((S (fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps)) * dst_positive_scale_row_entry_inner_tablevaluefold)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_steps_summand. dst_positive_code_row_entry_inner_tablevaluefold = fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps)) * dst_positive_scale_row_entry_inner_tablevaluefold) + (fs_a_dst_row_entry_inner_tablevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_steps_partial. fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_steps_partial + S (fs_r_dst_row_entry_inner_tablevaluefoldpositive_body_steps) = S ((S (fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_steps_partial. fs_u_dst_row_entry_inner_tablevaluefoldpositive = fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldpositive) + (fs_r_dst_row_entry_inner_tablevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_steps_successor. fs_h_dst_row_entry_inner_tablevaluefoldpositive_body_steps_successor + S (fs_s_dst_row_entry_inner_tablevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldpositive)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_steps_successor. fs_u_dst_row_entry_inner_tablevaluefoldpositive = fs_q_dst_row_entry_inner_tablevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_row_entry_inner_tablevaluefoldpositive_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldpositive) + (fs_s_dst_row_entry_inner_tablevaluefoldpositive_body_steps))) /\ fs_s_dst_row_entry_inner_tablevaluefoldpositive_body_steps = fs_r_dst_row_entry_inner_tablevaluefoldpositive_body_steps + fs_a_dst_row_entry_inner_tablevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_row_entry_inner_tablevaluefoldnegative fs_v_dst_row_entry_inner_tablevaluefoldnegative. ((((exists fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_start. fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_start. fs_u_dst_row_entry_inner_tablevaluefoldnegative = fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_row_entry_inner_tablevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_terminal. fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_terminal + S (dst_negative_sum_row_entry_inner_tablevaluefold) = S ((S (S (dc_input_row_entry_inner_table))) * fs_v_dst_row_entry_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_terminal. fs_u_dst_row_entry_inner_tablevaluefoldnegative = fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_terminal * S ((S (S (dc_input_row_entry_inner_table))) * fs_v_dst_row_entry_inner_tablevaluefoldnegative) + (dst_negative_sum_row_entry_inner_tablevaluefold))) /\ forall fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps. (exists fs_lt_dst_row_entry_inner_tablevaluefoldnegative_body_steps_bound. fs_lt_dst_row_entry_inner_tablevaluefoldnegative_body_steps_bound + S fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps = S (dc_input_row_entry_inner_table)) -> exists fs_a_dst_row_entry_inner_tablevaluefoldnegative_body_steps fs_r_dst_row_entry_inner_tablevaluefoldnegative_body_steps fs_s_dst_row_entry_inner_tablevaluefoldnegative_body_steps. ((((exists fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_steps_summand. fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_steps_summand + S (fs_a_dst_row_entry_inner_tablevaluefoldnegative_body_steps) = S ((S (fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps)) * dst_negative_scale_row_entry_inner_tablevaluefold)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_steps_summand. dst_negative_code_row_entry_inner_tablevaluefold = fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps)) * dst_negative_scale_row_entry_inner_tablevaluefold) + (fs_a_dst_row_entry_inner_tablevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_steps_partial. fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_steps_partial + S (fs_r_dst_row_entry_inner_tablevaluefoldnegative_body_steps) = S ((S (fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_steps_partial. fs_u_dst_row_entry_inner_tablevaluefoldnegative = fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldnegative) + (fs_r_dst_row_entry_inner_tablevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_steps_successor. fs_h_dst_row_entry_inner_tablevaluefoldnegative_body_steps_successor + S (fs_s_dst_row_entry_inner_tablevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldnegative)) /\ exists fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_steps_successor. fs_u_dst_row_entry_inner_tablevaluefoldnegative = fs_q_dst_row_entry_inner_tablevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_row_entry_inner_tablevaluefoldnegative_body_steps)) * fs_v_dst_row_entry_inner_tablevaluefoldnegative) + (fs_s_dst_row_entry_inner_tablevaluefoldnegative_body_steps))) /\ fs_s_dst_row_entry_inner_tablevaluefoldnegative_body_steps = fs_r_dst_row_entry_inner_tablevaluefoldnegative_body_steps + fs_a_dst_row_entry_inner_tablevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_row_entry_inner_tablevaluefoldresult ge_balance_negative_row_entry_inner_tablevaluefoldresult. (((((dc_output_row_entry_inner_table) = 2 * (ge_balance_positive_row_entry_inner_tablevaluefoldresult) /\ (ge_balance_negative_row_entry_inner_tablevaluefoldresult) = 0) \/ exists ge_signed_half_row_entry_inner_tablevaluefoldresultdecode. (((dc_output_row_entry_inner_table) = 2 * ge_signed_half_row_entry_inner_tablevaluefoldresultdecode + 1 /\ (ge_balance_positive_row_entry_inner_tablevaluefoldresult) = 0) /\ (ge_balance_negative_row_entry_inner_tablevaluefoldresult) = S ge_signed_half_row_entry_inner_tablevaluefoldresultdecode))) /\ ((dst_positive_sum_row_entry_inner_tablevaluefold) + ge_balance_negative_row_entry_inner_tablevaluefoldresult = (dst_negative_sum_row_entry_inner_tablevaluefold) + ge_balance_positive_row_entry_inner_tablevaluefoldresult)))))))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_row_entry_domain. pvs_le_gap_row_entry_domain + (n) = (N)) -> (exists pvs_le_gap_row_entry_index. pvs_le_gap_row_entry_index + (a) = (n)) -> (((exists dst_positive_code_row_entry_valuestable dst_positive_scale_row_entry_valuestable dst_negative_code_row_entry_valuestable dst_negative_scale_row_entry_valuestable. (((V) = (((((dst_positive_code_row_entry_valuestable) + (dst_positive_scale_row_entry_valuestable)) * S ((dst_positive_code_row_entry_valuestable) + (dst_positive_scale_row_entry_valuestable)) + ((dst_positive_scale_row_entry_valuestable) + (dst_positive_scale_row_entry_valuestable))) + (((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) * S ((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) + ((dst_negative_scale_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)))) * S ((((dst_positive_code_row_entry_valuestable) + (dst_positive_scale_row_entry_valuestable)) * S ((dst_positive_code_row_entry_valuestable) + (dst_positive_scale_row_entry_valuestable)) + ((dst_positive_scale_row_entry_valuestable) + (dst_positive_scale_row_entry_valuestable))) + (((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) * S ((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) + ((dst_negative_scale_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)))) + ((((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) * S ((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) + ((dst_negative_scale_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable))) + (((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) * S ((dst_negative_code_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)) + ((dst_negative_scale_row_entry_valuestable) + (dst_negative_scale_row_entry_valuestable)))))) /\ (forall dst_index_row_entry_valuestable. (exists pvs_le_gap_row_entry_valuestabledomain. pvs_le_gap_row_entry_valuestabledomain + (dst_index_row_entry_valuestable) = (S (n))) -> exists dst_positive_row_entry_valuestable dst_negative_row_entry_valuestable dst_value_row_entry_valuestable. ((((exists ff_h_pvs_row_entry_valuestableentrypositive. ff_h_pvs_row_entry_valuestableentrypositive + S (dst_positive_row_entry_valuestable) = S ((S (dst_index_row_entry_valuestable)) * dst_positive_scale_row_entry_valuestable)) /\ exists ff_q_pvs_row_entry_valuestableentrypositive. dst_positive_code_row_entry_valuestable = ff_q_pvs_row_entry_valuestableentrypositive * S ((S (dst_index_row_entry_valuestable)) * dst_positive_scale_row_entry_valuestable) + (dst_positive_row_entry_valuestable))) /\ (((((exists ff_h_pvs_row_entry_valuestableentrynegative. ff_h_pvs_row_entry_valuestableentrynegative + S (dst_negative_row_entry_valuestable) = S ((S (dst_index_row_entry_valuestable)) * dst_negative_scale_row_entry_valuestable)) /\ exists ff_q_pvs_row_entry_valuestableentrynegative. dst_negative_code_row_entry_valuestable = ff_q_pvs_row_entry_valuestableentrynegative * S ((S (dst_index_row_entry_valuestable)) * dst_negative_scale_row_entry_valuestable) + (dst_negative_row_entry_valuestable))) /\ (exists ge_balance_positive_row_entry_valuestableentryvalue ge_balance_negative_row_entry_valuestableentryvalue. (((((dst_value_row_entry_valuestable) = 2 * (ge_balance_positive_row_entry_valuestableentryvalue) /\ (ge_balance_negative_row_entry_valuestableentryvalue) = 0) \/ exists ge_signed_half_row_entry_valuestableentryvaluedecode. (((dst_value_row_entry_valuestable) = 2 * ge_signed_half_row_entry_valuestableentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_valuestableentryvalue) = 0) /\ (ge_balance_negative_row_entry_valuestableentryvalue) = S ge_signed_half_row_entry_valuestableentryvaluedecode))) /\ ((dst_positive_row_entry_valuestable) + ge_balance_negative_row_entry_valuestableentryvalue = (dst_negative_row_entry_valuestable) + ge_balance_positive_row_entry_valuestableentryvalue))))))))) /\ (forall dfg_factor_column_row_entry_values dfg_factor_value_row_entry_values. (exists pvs_le_gap_row_entry_valuesbound. pvs_le_gap_row_entry_valuesbound + (dfg_factor_column_row_entry_values) = (n)) -> (exists dst_positive_code_row_entry_valueslookup dst_positive_scale_row_entry_valueslookup dst_negative_code_row_entry_valueslookup dst_negative_scale_row_entry_valueslookup dst_positive_row_entry_valueslookup dst_negative_row_entry_valueslookup. (((V) = (((((dst_positive_code_row_entry_valueslookup) + (dst_positive_scale_row_entry_valueslookup)) * S ((dst_positive_code_row_entry_valueslookup) + (dst_positive_scale_row_entry_valueslookup)) + ((dst_positive_scale_row_entry_valueslookup) + (dst_positive_scale_row_entry_valueslookup))) + (((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) * S ((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) + ((dst_negative_scale_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)))) * S ((((dst_positive_code_row_entry_valueslookup) + (dst_positive_scale_row_entry_valueslookup)) * S ((dst_positive_code_row_entry_valueslookup) + (dst_positive_scale_row_entry_valueslookup)) + ((dst_positive_scale_row_entry_valueslookup) + (dst_positive_scale_row_entry_valueslookup))) + (((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) * S ((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) + ((dst_negative_scale_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)))) + ((((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) * S ((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) + ((dst_negative_scale_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup))) + (((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) * S ((dst_negative_code_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)) + ((dst_negative_scale_row_entry_valueslookup) + (dst_negative_scale_row_entry_valueslookup)))))) /\ (((((exists ff_h_pvs_row_entry_valueslookuppositive. ff_h_pvs_row_entry_valueslookuppositive + S (dst_positive_row_entry_valueslookup) = S ((S (dfg_factor_column_row_entry_values)) * dst_positive_scale_row_entry_valueslookup)) /\ exists ff_q_pvs_row_entry_valueslookuppositive. dst_positive_code_row_entry_valueslookup = ff_q_pvs_row_entry_valueslookuppositive * S ((S (dfg_factor_column_row_entry_values)) * dst_positive_scale_row_entry_valueslookup) + (dst_positive_row_entry_valueslookup))) /\ (((((exists ff_h_pvs_row_entry_valueslookupnegative. ff_h_pvs_row_entry_valueslookupnegative + S (dst_negative_row_entry_valueslookup) = S ((S (dfg_factor_column_row_entry_values)) * dst_negative_scale_row_entry_valueslookup)) /\ exists ff_q_pvs_row_entry_valueslookupnegative. dst_negative_code_row_entry_valueslookup = ff_q_pvs_row_entry_valueslookupnegative * S ((S (dfg_factor_column_row_entry_values)) * dst_negative_scale_row_entry_valueslookup) + (dst_negative_row_entry_valueslookup))) /\ (exists ge_balance_positive_row_entry_valueslookupvalue ge_balance_negative_row_entry_valueslookupvalue. (((((dfg_factor_value_row_entry_values) = 2 * (ge_balance_positive_row_entry_valueslookupvalue) /\ (ge_balance_negative_row_entry_valueslookupvalue) = 0) \/ exists ge_signed_half_row_entry_valueslookupvaluedecode. (((dfg_factor_value_row_entry_values) = 2 * ge_signed_half_row_entry_valueslookupvaluedecode + 1 /\ (ge_balance_positive_row_entry_valueslookupvalue) = 0) /\ (ge_balance_negative_row_entry_valueslookupvalue) = S ge_signed_half_row_entry_valueslookupvaluedecode))) /\ ((dst_positive_row_entry_valueslookup) + ge_balance_negative_row_entry_valueslookupvalue = (dst_negative_row_entry_valueslookup) + ge_balance_positive_row_entry_valueslookupvalue))))))))) -> ((((~((a)=0)) /\ (((~((dfg_factor_column_row_entry_values)=0)) /\ (exists dfg_middle_row_entry_valuesentry dfg_first_row_entry_valuesentry dfg_last_row_entry_valuesentry dfg_value_row_entry_valuesentry. (((n)=((a)*(dfg_factor_column_row_entry_values))*dfg_middle_row_entry_valuesentry) /\ (((exists dst_positive_code_row_entry_valuesentryfirst dst_positive_scale_row_entry_valuesentryfirst dst_negative_code_row_entry_valuesentryfirst dst_negative_scale_row_entry_valuesentryfirst dst_positive_row_entry_valuesentryfirst dst_negative_row_entry_valuesentryfirst. (((F) = (((((dst_positive_code_row_entry_valuesentryfirst) + (dst_positive_scale_row_entry_valuesentryfirst)) * S ((dst_positive_code_row_entry_valuesentryfirst) + (dst_positive_scale_row_entry_valuesentryfirst)) + ((dst_positive_scale_row_entry_valuesentryfirst) + (dst_positive_scale_row_entry_valuesentryfirst))) + (((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) * S ((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) + ((dst_negative_scale_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)))) * S ((((dst_positive_code_row_entry_valuesentryfirst) + (dst_positive_scale_row_entry_valuesentryfirst)) * S ((dst_positive_code_row_entry_valuesentryfirst) + (dst_positive_scale_row_entry_valuesentryfirst)) + ((dst_positive_scale_row_entry_valuesentryfirst) + (dst_positive_scale_row_entry_valuesentryfirst))) + (((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) * S ((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) + ((dst_negative_scale_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)))) + ((((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) * S ((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) + ((dst_negative_scale_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst))) + (((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) * S ((dst_negative_code_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)) + ((dst_negative_scale_row_entry_valuesentryfirst) + (dst_negative_scale_row_entry_valuesentryfirst)))))) /\ (((((exists ff_h_pvs_row_entry_valuesentryfirstpositive. ff_h_pvs_row_entry_valuesentryfirstpositive + S (dst_positive_row_entry_valuesentryfirst) = S ((S (a)) * dst_positive_scale_row_entry_valuesentryfirst)) /\ exists ff_q_pvs_row_entry_valuesentryfirstpositive. dst_positive_code_row_entry_valuesentryfirst = ff_q_pvs_row_entry_valuesentryfirstpositive * S ((S (a)) * dst_positive_scale_row_entry_valuesentryfirst) + (dst_positive_row_entry_valuesentryfirst))) /\ (((((exists ff_h_pvs_row_entry_valuesentryfirstnegative. ff_h_pvs_row_entry_valuesentryfirstnegative + S (dst_negative_row_entry_valuesentryfirst) = S ((S (a)) * dst_negative_scale_row_entry_valuesentryfirst)) /\ exists ff_q_pvs_row_entry_valuesentryfirstnegative. dst_negative_code_row_entry_valuesentryfirst = ff_q_pvs_row_entry_valuesentryfirstnegative * S ((S (a)) * dst_negative_scale_row_entry_valuesentryfirst) + (dst_negative_row_entry_valuesentryfirst))) /\ (exists ge_balance_positive_row_entry_valuesentryfirstvalue ge_balance_negative_row_entry_valuesentryfirstvalue. (((((dfg_first_row_entry_valuesentry) = 2 * (ge_balance_positive_row_entry_valuesentryfirstvalue) /\ (ge_balance_negative_row_entry_valuesentryfirstvalue) = 0) \/ exists ge_signed_half_row_entry_valuesentryfirstvaluedecode. (((dfg_first_row_entry_valuesentry) = 2 * ge_signed_half_row_entry_valuesentryfirstvaluedecode + 1 /\ (ge_balance_positive_row_entry_valuesentryfirstvalue) = 0) /\ (ge_balance_negative_row_entry_valuesentryfirstvalue) = S ge_signed_half_row_entry_valuesentryfirstvaluedecode))) /\ ((dst_positive_row_entry_valuesentryfirst) + ge_balance_negative_row_entry_valuesentryfirstvalue = (dst_negative_row_entry_valuesentryfirst) + ge_balance_positive_row_entry_valuesentryfirstvalue))))))))) /\ (((exists dst_positive_code_row_entry_valuesentrylast dst_positive_scale_row_entry_valuesentrylast dst_negative_code_row_entry_valuesentrylast dst_negative_scale_row_entry_valuesentrylast dst_positive_row_entry_valuesentrylast dst_negative_row_entry_valuesentrylast. (((H) = (((((dst_positive_code_row_entry_valuesentrylast) + (dst_positive_scale_row_entry_valuesentrylast)) * S ((dst_positive_code_row_entry_valuesentrylast) + (dst_positive_scale_row_entry_valuesentrylast)) + ((dst_positive_scale_row_entry_valuesentrylast) + (dst_positive_scale_row_entry_valuesentrylast))) + (((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) * S ((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) + ((dst_negative_scale_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)))) * S ((((dst_positive_code_row_entry_valuesentrylast) + (dst_positive_scale_row_entry_valuesentrylast)) * S ((dst_positive_code_row_entry_valuesentrylast) + (dst_positive_scale_row_entry_valuesentrylast)) + ((dst_positive_scale_row_entry_valuesentrylast) + (dst_positive_scale_row_entry_valuesentrylast))) + (((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) * S ((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) + ((dst_negative_scale_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)))) + ((((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) * S ((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) + ((dst_negative_scale_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast))) + (((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) * S ((dst_negative_code_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)) + ((dst_negative_scale_row_entry_valuesentrylast) + (dst_negative_scale_row_entry_valuesentrylast)))))) /\ (((((exists ff_h_pvs_row_entry_valuesentrylastpositive. ff_h_pvs_row_entry_valuesentrylastpositive + S (dst_positive_row_entry_valuesentrylast) = S ((S (dfg_factor_column_row_entry_values)) * dst_positive_scale_row_entry_valuesentrylast)) /\ exists ff_q_pvs_row_entry_valuesentrylastpositive. dst_positive_code_row_entry_valuesentrylast = ff_q_pvs_row_entry_valuesentrylastpositive * S ((S (dfg_factor_column_row_entry_values)) * dst_positive_scale_row_entry_valuesentrylast) + (dst_positive_row_entry_valuesentrylast))) /\ (((((exists ff_h_pvs_row_entry_valuesentrylastnegative. ff_h_pvs_row_entry_valuesentrylastnegative + S (dst_negative_row_entry_valuesentrylast) = S ((S (dfg_factor_column_row_entry_values)) * dst_negative_scale_row_entry_valuesentrylast)) /\ exists ff_q_pvs_row_entry_valuesentrylastnegative. dst_negative_code_row_entry_valuesentrylast = ff_q_pvs_row_entry_valuesentrylastnegative * S ((S (dfg_factor_column_row_entry_values)) * dst_negative_scale_row_entry_valuesentrylast) + (dst_negative_row_entry_valuesentrylast))) /\ (exists ge_balance_positive_row_entry_valuesentrylastvalue ge_balance_negative_row_entry_valuesentrylastvalue. (((((dfg_last_row_entry_valuesentry) = 2 * (ge_balance_positive_row_entry_valuesentrylastvalue) /\ (ge_balance_negative_row_entry_valuesentrylastvalue) = 0) \/ exists ge_signed_half_row_entry_valuesentrylastvaluedecode. (((dfg_last_row_entry_valuesentry) = 2 * ge_signed_half_row_entry_valuesentrylastvaluedecode + 1 /\ (ge_balance_positive_row_entry_valuesentrylastvalue) = 0) /\ (ge_balance_negative_row_entry_valuesentrylastvalue) = S ge_signed_half_row_entry_valuesentrylastvaluedecode))) /\ ((dst_positive_row_entry_valuesentrylast) + ge_balance_negative_row_entry_valuesentrylastvalue = (dst_negative_row_entry_valuesentrylast) + ge_balance_positive_row_entry_valuesentrylastvalue))))))))) /\ (((exists dst_positive_code_row_entry_valuesentrymiddle dst_positive_scale_row_entry_valuesentrymiddle dst_negative_code_row_entry_valuesentrymiddle dst_negative_scale_row_entry_valuesentrymiddle dst_positive_row_entry_valuesentrymiddle dst_negative_row_entry_valuesentrymiddle. (((G) = (((((dst_positive_code_row_entry_valuesentrymiddle) + (dst_positive_scale_row_entry_valuesentrymiddle)) * S ((dst_positive_code_row_entry_valuesentrymiddle) + (dst_positive_scale_row_entry_valuesentrymiddle)) + ((dst_positive_scale_row_entry_valuesentrymiddle) + (dst_positive_scale_row_entry_valuesentrymiddle))) + (((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) * S ((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) + ((dst_negative_scale_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)))) * S ((((dst_positive_code_row_entry_valuesentrymiddle) + (dst_positive_scale_row_entry_valuesentrymiddle)) * S ((dst_positive_code_row_entry_valuesentrymiddle) + (dst_positive_scale_row_entry_valuesentrymiddle)) + ((dst_positive_scale_row_entry_valuesentrymiddle) + (dst_positive_scale_row_entry_valuesentrymiddle))) + (((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) * S ((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) + ((dst_negative_scale_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)))) + ((((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) * S ((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) + ((dst_negative_scale_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle))) + (((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) * S ((dst_negative_code_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)) + ((dst_negative_scale_row_entry_valuesentrymiddle) + (dst_negative_scale_row_entry_valuesentrymiddle)))))) /\ (((((exists ff_h_pvs_row_entry_valuesentrymiddlepositive. ff_h_pvs_row_entry_valuesentrymiddlepositive + S (dst_positive_row_entry_valuesentrymiddle) = S ((S (dfg_middle_row_entry_valuesentry)) * dst_positive_scale_row_entry_valuesentrymiddle)) /\ exists ff_q_pvs_row_entry_valuesentrymiddlepositive. dst_positive_code_row_entry_valuesentrymiddle = ff_q_pvs_row_entry_valuesentrymiddlepositive * S ((S (dfg_middle_row_entry_valuesentry)) * dst_positive_scale_row_entry_valuesentrymiddle) + (dst_positive_row_entry_valuesentrymiddle))) /\ (((((exists ff_h_pvs_row_entry_valuesentrymiddlenegative. ff_h_pvs_row_entry_valuesentrymiddlenegative + S (dst_negative_row_entry_valuesentrymiddle) = S ((S (dfg_middle_row_entry_valuesentry)) * dst_negative_scale_row_entry_valuesentrymiddle)) /\ exists ff_q_pvs_row_entry_valuesentrymiddlenegative. dst_negative_code_row_entry_valuesentrymiddle = ff_q_pvs_row_entry_valuesentrymiddlenegative * S ((S (dfg_middle_row_entry_valuesentry)) * dst_negative_scale_row_entry_valuesentrymiddle) + (dst_negative_row_entry_valuesentrymiddle))) /\ (exists ge_balance_positive_row_entry_valuesentrymiddlevalue ge_balance_negative_row_entry_valuesentrymiddlevalue. (((((dfg_value_row_entry_valuesentry) = 2 * (ge_balance_positive_row_entry_valuesentrymiddlevalue) /\ (ge_balance_negative_row_entry_valuesentrymiddlevalue) = 0) \/ exists ge_signed_half_row_entry_valuesentrymiddlevaluedecode. (((dfg_value_row_entry_valuesentry) = 2 * ge_signed_half_row_entry_valuesentrymiddlevaluedecode + 1 /\ (ge_balance_positive_row_entry_valuesentrymiddlevalue) = 0) /\ (ge_balance_negative_row_entry_valuesentrymiddlevalue) = S ge_signed_half_row_entry_valuesentrymiddlevaluedecode))) /\ ((dst_positive_row_entry_valuesentrymiddle) + ge_balance_negative_row_entry_valuesentrymiddlevalue = (dst_negative_row_entry_valuesentrymiddle) + ge_balance_positive_row_entry_valuesentrymiddlevalue))))))))) /\ (exists dfg_inner_row_entry_valuesentryproduct. ((exists sto_ap_row_entry_valuesentryproductinner sto_an_row_entry_valuesentryproductinner sto_bp_row_entry_valuesentryproductinner sto_bn_row_entry_valuesentryproductinner sto_cp_row_entry_valuesentryproductinner sto_cn_row_entry_valuesentryproductinner. (((((dfg_last_row_entry_valuesentry) = 2 * (sto_ap_row_entry_valuesentryproductinner) /\ (sto_an_row_entry_valuesentryproductinner) = 0) \/ exists ge_signed_half_row_entry_valuesentryproductinnerleft. (((dfg_last_row_entry_valuesentry) = 2 * ge_signed_half_row_entry_valuesentryproductinnerleft + 1 /\ (sto_ap_row_entry_valuesentryproductinner) = 0) /\ (sto_an_row_entry_valuesentryproductinner) = S ge_signed_half_row_entry_valuesentryproductinnerleft))) /\ ((((((dfg_value_row_entry_valuesentry) = 2 * (sto_bp_row_entry_valuesentryproductinner) /\ (sto_bn_row_entry_valuesentryproductinner) = 0) \/ exists ge_signed_half_row_entry_valuesentryproductinnerright. (((dfg_value_row_entry_valuesentry) = 2 * ge_signed_half_row_entry_valuesentryproductinnerright + 1 /\ (sto_bp_row_entry_valuesentryproductinner) = 0) /\ (sto_bn_row_entry_valuesentryproductinner) = S ge_signed_half_row_entry_valuesentryproductinnerright))) /\ ((((((dfg_inner_row_entry_valuesentryproduct) = 2 * (sto_cp_row_entry_valuesentryproductinner) /\ (sto_cn_row_entry_valuesentryproductinner) = 0) \/ exists ge_signed_half_row_entry_valuesentryproductinneroutput. (((dfg_inner_row_entry_valuesentryproduct) = 2 * ge_signed_half_row_entry_valuesentryproductinneroutput + 1 /\ (sto_cp_row_entry_valuesentryproductinner) = 0) /\ (sto_cn_row_entry_valuesentryproductinner) = S ge_signed_half_row_entry_valuesentryproductinneroutput))) /\ ((sto_ap_row_entry_valuesentryproductinner * sto_bp_row_entry_valuesentryproductinner + sto_an_row_entry_valuesentryproductinner * sto_bn_row_entry_valuesentryproductinner) + sto_cn_row_entry_valuesentryproductinner = (sto_ap_row_entry_valuesentryproductinner * sto_bn_row_entry_valuesentryproductinner + sto_an_row_entry_valuesentryproductinner * sto_bp_row_entry_valuesentryproductinner) + sto_cp_row_entry_valuesentryproductinner))))))) /\ (exists sto_ap_row_entry_valuesentryproductouter sto_an_row_entry_valuesentryproductouter sto_bp_row_entry_valuesentryproductouter sto_bn_row_entry_valuesentryproductouter sto_cp_row_entry_valuesentryproductouter sto_cn_row_entry_valuesentryproductouter. (((((dfg_first_row_entry_valuesentry) = 2 * (sto_ap_row_entry_valuesentryproductouter) /\ (sto_an_row_entry_valuesentryproductouter) = 0) \/ exists ge_signed_half_row_entry_valuesentryproductouterleft. (((dfg_first_row_entry_valuesentry) = 2 * ge_signed_half_row_entry_valuesentryproductouterleft + 1 /\ (sto_ap_row_entry_valuesentryproductouter) = 0) /\ (sto_an_row_entry_valuesentryproductouter) = S ge_signed_half_row_entry_valuesentryproductouterleft))) /\ ((((((dfg_inner_row_entry_valuesentryproduct) = 2 * (sto_bp_row_entry_valuesentryproductouter) /\ (sto_bn_row_entry_valuesentryproductouter) = 0) \/ exists ge_signed_half_row_entry_valuesentryproductouterright. (((dfg_inner_row_entry_valuesentryproduct) = 2 * ge_signed_half_row_entry_valuesentryproductouterright + 1 /\ (sto_bp_row_entry_valuesentryproductouter) = 0) /\ (sto_bn_row_entry_valuesentryproductouter) = S ge_signed_half_row_entry_valuesentryproductouterright))) /\ ((((((dfg_factor_value_row_entry_values) = 2 * (sto_cp_row_entry_valuesentryproductouter) /\ (sto_cn_row_entry_valuesentryproductouter) = 0) \/ exists ge_signed_half_row_entry_valuesentryproductouteroutput. (((dfg_factor_value_row_entry_values) = 2 * ge_signed_half_row_entry_valuesentryproductouteroutput + 1 /\ (sto_cp_row_entry_valuesentryproductouter) = 0) /\ (sto_cn_row_entry_valuesentryproductouter) = S ge_signed_half_row_entry_valuesentryproductouteroutput))) /\ ((sto_ap_row_entry_valuesentryproductouter * sto_bp_row_entry_valuesentryproductouter + sto_an_row_entry_valuesentryproductouter * sto_bn_row_entry_valuesentryproductouter) + sto_cn_row_entry_valuesentryproductouter = (sto_ap_row_entry_valuesentryproductouter * sto_bn_row_entry_valuesentryproductouter + sto_an_row_entry_valuesentryproductouter * sto_bp_row_entry_valuesentryproductouter) + sto_cp_row_entry_valuesentryproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((dfg_factor_column_row_entry_values)=0 \/ ~(exists pvs_factor_row_entry_valuesentryomittednondivisor. (n) = ((a)*(dfg_factor_column_row_entry_values)) * pvs_factor_row_entry_valuesentryomittednondivisor))) /\ ((dfg_factor_value_row_entry_values)=0))))))) -> (exists dst_positive_code_row_entry_sum dst_positive_scale_row_entry_sum dst_negative_code_row_entry_sum dst_negative_scale_row_entry_sum dst_positive_sum_row_entry_sum dst_negative_sum_row_entry_sum. (((V) = (((((dst_positive_code_row_entry_sum) + (dst_positive_scale_row_entry_sum)) * S ((dst_positive_code_row_entry_sum) + (dst_positive_scale_row_entry_sum)) + ((dst_positive_scale_row_entry_sum) + (dst_positive_scale_row_entry_sum))) + (((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) * S ((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) + ((dst_negative_scale_row_entry_sum) + (dst_negative_scale_row_entry_sum)))) * S ((((dst_positive_code_row_entry_sum) + (dst_positive_scale_row_entry_sum)) * S ((dst_positive_code_row_entry_sum) + (dst_positive_scale_row_entry_sum)) + ((dst_positive_scale_row_entry_sum) + (dst_positive_scale_row_entry_sum))) + (((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) * S ((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) + ((dst_negative_scale_row_entry_sum) + (dst_negative_scale_row_entry_sum)))) + ((((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) * S ((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) + ((dst_negative_scale_row_entry_sum) + (dst_negative_scale_row_entry_sum))) + (((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) * S ((dst_negative_code_row_entry_sum) + (dst_negative_scale_row_entry_sum)) + ((dst_negative_scale_row_entry_sum) + (dst_negative_scale_row_entry_sum)))))) /\ (((exists fs_u_dst_row_entry_sumpositive fs_v_dst_row_entry_sumpositive. ((((exists fs_h_dst_row_entry_sumpositive_body_start. fs_h_dst_row_entry_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_sumpositive)) /\ exists fs_q_dst_row_entry_sumpositive_body_start. fs_u_dst_row_entry_sumpositive = fs_q_dst_row_entry_sumpositive_body_start * S ((S (0)) * fs_v_dst_row_entry_sumpositive) + (0))) /\ ((((exists fs_h_dst_row_entry_sumpositive_body_terminal. fs_h_dst_row_entry_sumpositive_body_terminal + S (dst_positive_sum_row_entry_sum) = S ((S (S n)) * fs_v_dst_row_entry_sumpositive)) /\ exists fs_q_dst_row_entry_sumpositive_body_terminal. fs_u_dst_row_entry_sumpositive = fs_q_dst_row_entry_sumpositive_body_terminal * S ((S (S n)) * fs_v_dst_row_entry_sumpositive) + (dst_positive_sum_row_entry_sum))) /\ forall fs_i_dst_row_entry_sumpositive_body_steps. (exists fs_lt_dst_row_entry_sumpositive_body_steps_bound. fs_lt_dst_row_entry_sumpositive_body_steps_bound + S fs_i_dst_row_entry_sumpositive_body_steps = S n) -> exists fs_a_dst_row_entry_sumpositive_body_steps fs_r_dst_row_entry_sumpositive_body_steps fs_s_dst_row_entry_sumpositive_body_steps. ((((exists fs_h_dst_row_entry_sumpositive_body_steps_summand. fs_h_dst_row_entry_sumpositive_body_steps_summand + S (fs_a_dst_row_entry_sumpositive_body_steps) = S ((S (fs_i_dst_row_entry_sumpositive_body_steps)) * dst_positive_scale_row_entry_sum)) /\ exists fs_q_dst_row_entry_sumpositive_body_steps_summand. dst_positive_code_row_entry_sum = fs_q_dst_row_entry_sumpositive_body_steps_summand * S ((S (fs_i_dst_row_entry_sumpositive_body_steps)) * dst_positive_scale_row_entry_sum) + (fs_a_dst_row_entry_sumpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_sumpositive_body_steps_partial. fs_h_dst_row_entry_sumpositive_body_steps_partial + S (fs_r_dst_row_entry_sumpositive_body_steps) = S ((S (fs_i_dst_row_entry_sumpositive_body_steps)) * fs_v_dst_row_entry_sumpositive)) /\ exists fs_q_dst_row_entry_sumpositive_body_steps_partial. fs_u_dst_row_entry_sumpositive = fs_q_dst_row_entry_sumpositive_body_steps_partial * S ((S (fs_i_dst_row_entry_sumpositive_body_steps)) * fs_v_dst_row_entry_sumpositive) + (fs_r_dst_row_entry_sumpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_sumpositive_body_steps_successor. fs_h_dst_row_entry_sumpositive_body_steps_successor + S (fs_s_dst_row_entry_sumpositive_body_steps) = S ((S (S fs_i_dst_row_entry_sumpositive_body_steps)) * fs_v_dst_row_entry_sumpositive)) /\ exists fs_q_dst_row_entry_sumpositive_body_steps_successor. fs_u_dst_row_entry_sumpositive = fs_q_dst_row_entry_sumpositive_body_steps_successor * S ((S (S fs_i_dst_row_entry_sumpositive_body_steps)) * fs_v_dst_row_entry_sumpositive) + (fs_s_dst_row_entry_sumpositive_body_steps))) /\ fs_s_dst_row_entry_sumpositive_body_steps = fs_r_dst_row_entry_sumpositive_body_steps + fs_a_dst_row_entry_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_row_entry_sumnegative fs_v_dst_row_entry_sumnegative. ((((exists fs_h_dst_row_entry_sumnegative_body_start. fs_h_dst_row_entry_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_sumnegative)) /\ exists fs_q_dst_row_entry_sumnegative_body_start. fs_u_dst_row_entry_sumnegative = fs_q_dst_row_entry_sumnegative_body_start * S ((S (0)) * fs_v_dst_row_entry_sumnegative) + (0))) /\ ((((exists fs_h_dst_row_entry_sumnegative_body_terminal. fs_h_dst_row_entry_sumnegative_body_terminal + S (dst_negative_sum_row_entry_sum) = S ((S (S n)) * fs_v_dst_row_entry_sumnegative)) /\ exists fs_q_dst_row_entry_sumnegative_body_terminal. fs_u_dst_row_entry_sumnegative = fs_q_dst_row_entry_sumnegative_body_terminal * S ((S (S n)) * fs_v_dst_row_entry_sumnegative) + (dst_negative_sum_row_entry_sum))) /\ forall fs_i_dst_row_entry_sumnegative_body_steps. (exists fs_lt_dst_row_entry_sumnegative_body_steps_bound. fs_lt_dst_row_entry_sumnegative_body_steps_bound + S fs_i_dst_row_entry_sumnegative_body_steps = S n) -> exists fs_a_dst_row_entry_sumnegative_body_steps fs_r_dst_row_entry_sumnegative_body_steps fs_s_dst_row_entry_sumnegative_body_steps. ((((exists fs_h_dst_row_entry_sumnegative_body_steps_summand. fs_h_dst_row_entry_sumnegative_body_steps_summand + S (fs_a_dst_row_entry_sumnegative_body_steps) = S ((S (fs_i_dst_row_entry_sumnegative_body_steps)) * dst_negative_scale_row_entry_sum)) /\ exists fs_q_dst_row_entry_sumnegative_body_steps_summand. dst_negative_code_row_entry_sum = fs_q_dst_row_entry_sumnegative_body_steps_summand * S ((S (fs_i_dst_row_entry_sumnegative_body_steps)) * dst_negative_scale_row_entry_sum) + (fs_a_dst_row_entry_sumnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_sumnegative_body_steps_partial. fs_h_dst_row_entry_sumnegative_body_steps_partial + S (fs_r_dst_row_entry_sumnegative_body_steps) = S ((S (fs_i_dst_row_entry_sumnegative_body_steps)) * fs_v_dst_row_entry_sumnegative)) /\ exists fs_q_dst_row_entry_sumnegative_body_steps_partial. fs_u_dst_row_entry_sumnegative = fs_q_dst_row_entry_sumnegative_body_steps_partial * S ((S (fs_i_dst_row_entry_sumnegative_body_steps)) * fs_v_dst_row_entry_sumnegative) + (fs_r_dst_row_entry_sumnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_sumnegative_body_steps_successor. fs_h_dst_row_entry_sumnegative_body_steps_successor + S (fs_s_dst_row_entry_sumnegative_body_steps) = S ((S (S fs_i_dst_row_entry_sumnegative_body_steps)) * fs_v_dst_row_entry_sumnegative)) /\ exists fs_q_dst_row_entry_sumnegative_body_steps_successor. fs_u_dst_row_entry_sumnegative = fs_q_dst_row_entry_sumnegative_body_steps_successor * S ((S (S fs_i_dst_row_entry_sumnegative_body_steps)) * fs_v_dst_row_entry_sumnegative) + (fs_s_dst_row_entry_sumnegative_body_steps))) /\ fs_s_dst_row_entry_sumnegative_body_steps = fs_r_dst_row_entry_sumnegative_body_steps + fs_a_dst_row_entry_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_row_entry_sumresult ge_balance_negative_row_entry_sumresult. (((((z) = 2 * (ge_balance_positive_row_entry_sumresult) /\ (ge_balance_negative_row_entry_sumresult) = 0) \/ exists ge_signed_half_row_entry_sumresultdecode. (((z) = 2 * ge_signed_half_row_entry_sumresultdecode + 1 /\ (ge_balance_positive_row_entry_sumresult) = 0) /\ (ge_balance_negative_row_entry_sumresult) = S ge_signed_half_row_entry_sumresultdecode))) /\ ((dst_positive_sum_row_entry_sum) + ge_balance_negative_row_entry_sumresult = (dst_negative_sum_row_entry_sum) + ge_balance_positive_row_entry_sumresult))))))))) -> ((((~((a)=0)) /\ (exists dc_quotient_row_entry_result dc_left_row_entry_result dc_right_row_entry_result. (((n)=(a)*dc_quotient_row_entry_result) /\ (((exists dst_positive_code_row_entry_resultleft dst_positive_scale_row_entry_resultleft dst_negative_code_row_entry_resultleft dst_negative_scale_row_entry_resultleft dst_positive_row_entry_resultleft dst_negative_row_entry_resultleft. (((F) = (((((dst_positive_code_row_entry_resultleft) + (dst_positive_scale_row_entry_resultleft)) * S ((dst_positive_code_row_entry_resultleft) + (dst_positive_scale_row_entry_resultleft)) + ((dst_positive_scale_row_entry_resultleft) + (dst_positive_scale_row_entry_resultleft))) + (((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) * S ((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) + ((dst_negative_scale_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)))) * S ((((dst_positive_code_row_entry_resultleft) + (dst_positive_scale_row_entry_resultleft)) * S ((dst_positive_code_row_entry_resultleft) + (dst_positive_scale_row_entry_resultleft)) + ((dst_positive_scale_row_entry_resultleft) + (dst_positive_scale_row_entry_resultleft))) + (((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) * S ((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) + ((dst_negative_scale_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)))) + ((((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) * S ((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) + ((dst_negative_scale_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft))) + (((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) * S ((dst_negative_code_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)) + ((dst_negative_scale_row_entry_resultleft) + (dst_negative_scale_row_entry_resultleft)))))) /\ (((((exists ff_h_pvs_row_entry_resultleftpositive. ff_h_pvs_row_entry_resultleftpositive + S (dst_positive_row_entry_resultleft) = S ((S (a)) * dst_positive_scale_row_entry_resultleft)) /\ exists ff_q_pvs_row_entry_resultleftpositive. dst_positive_code_row_entry_resultleft = ff_q_pvs_row_entry_resultleftpositive * S ((S (a)) * dst_positive_scale_row_entry_resultleft) + (dst_positive_row_entry_resultleft))) /\ (((((exists ff_h_pvs_row_entry_resultleftnegative. ff_h_pvs_row_entry_resultleftnegative + S (dst_negative_row_entry_resultleft) = S ((S (a)) * dst_negative_scale_row_entry_resultleft)) /\ exists ff_q_pvs_row_entry_resultleftnegative. dst_negative_code_row_entry_resultleft = ff_q_pvs_row_entry_resultleftnegative * S ((S (a)) * dst_negative_scale_row_entry_resultleft) + (dst_negative_row_entry_resultleft))) /\ (exists ge_balance_positive_row_entry_resultleftvalue ge_balance_negative_row_entry_resultleftvalue. (((((dc_left_row_entry_result) = 2 * (ge_balance_positive_row_entry_resultleftvalue) /\ (ge_balance_negative_row_entry_resultleftvalue) = 0) \/ exists ge_signed_half_row_entry_resultleftvaluedecode. (((dc_left_row_entry_result) = 2 * ge_signed_half_row_entry_resultleftvaluedecode + 1 /\ (ge_balance_positive_row_entry_resultleftvalue) = 0) /\ (ge_balance_negative_row_entry_resultleftvalue) = S ge_signed_half_row_entry_resultleftvaluedecode))) /\ ((dst_positive_row_entry_resultleft) + ge_balance_negative_row_entry_resultleftvalue = (dst_negative_row_entry_resultleft) + ge_balance_positive_row_entry_resultleftvalue))))))))) /\ (((exists dst_positive_code_row_entry_resultright dst_positive_scale_row_entry_resultright dst_negative_code_row_entry_resultright dst_negative_scale_row_entry_resultright dst_positive_row_entry_resultright dst_negative_row_entry_resultright. (((U) = (((((dst_positive_code_row_entry_resultright) + (dst_positive_scale_row_entry_resultright)) * S ((dst_positive_code_row_entry_resultright) + (dst_positive_scale_row_entry_resultright)) + ((dst_positive_scale_row_entry_resultright) + (dst_positive_scale_row_entry_resultright))) + (((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) * S ((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) + ((dst_negative_scale_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)))) * S ((((dst_positive_code_row_entry_resultright) + (dst_positive_scale_row_entry_resultright)) * S ((dst_positive_code_row_entry_resultright) + (dst_positive_scale_row_entry_resultright)) + ((dst_positive_scale_row_entry_resultright) + (dst_positive_scale_row_entry_resultright))) + (((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) * S ((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) + ((dst_negative_scale_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)))) + ((((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) * S ((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) + ((dst_negative_scale_row_entry_resultright) + (dst_negative_scale_row_entry_resultright))) + (((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) * S ((dst_negative_code_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)) + ((dst_negative_scale_row_entry_resultright) + (dst_negative_scale_row_entry_resultright)))))) /\ (((((exists ff_h_pvs_row_entry_resultrightpositive. ff_h_pvs_row_entry_resultrightpositive + S (dst_positive_row_entry_resultright) = S ((S (dc_quotient_row_entry_result)) * dst_positive_scale_row_entry_resultright)) /\ exists ff_q_pvs_row_entry_resultrightpositive. dst_positive_code_row_entry_resultright = ff_q_pvs_row_entry_resultrightpositive * S ((S (dc_quotient_row_entry_result)) * dst_positive_scale_row_entry_resultright) + (dst_positive_row_entry_resultright))) /\ (((((exists ff_h_pvs_row_entry_resultrightnegative. ff_h_pvs_row_entry_resultrightnegative + S (dst_negative_row_entry_resultright) = S ((S (dc_quotient_row_entry_result)) * dst_negative_scale_row_entry_resultright)) /\ exists ff_q_pvs_row_entry_resultrightnegative. dst_negative_code_row_entry_resultright = ff_q_pvs_row_entry_resultrightnegative * S ((S (dc_quotient_row_entry_result)) * dst_negative_scale_row_entry_resultright) + (dst_negative_row_entry_resultright))) /\ (exists ge_balance_positive_row_entry_resultrightvalue ge_balance_negative_row_entry_resultrightvalue. (((((dc_right_row_entry_result) = 2 * (ge_balance_positive_row_entry_resultrightvalue) /\ (ge_balance_negative_row_entry_resultrightvalue) = 0) \/ exists ge_signed_half_row_entry_resultrightvaluedecode. (((dc_right_row_entry_result) = 2 * ge_signed_half_row_entry_resultrightvaluedecode + 1 /\ (ge_balance_positive_row_entry_resultrightvalue) = 0) /\ (ge_balance_negative_row_entry_resultrightvalue) = S ge_signed_half_row_entry_resultrightvaluedecode))) /\ ((dst_positive_row_entry_resultright) + ge_balance_negative_row_entry_resultrightvalue = (dst_negative_row_entry_resultright) + ge_balance_positive_row_entry_resultrightvalue))))))))) /\ (exists sto_ap_row_entry_resultproduct sto_an_row_entry_resultproduct sto_bp_row_entry_resultproduct sto_bn_row_entry_resultproduct sto_cp_row_entry_resultproduct sto_cn_row_entry_resultproduct. (((((dc_left_row_entry_result) = 2 * (sto_ap_row_entry_resultproduct) /\ (sto_an_row_entry_resultproduct) = 0) \/ exists ge_signed_half_row_entry_resultproductleft. (((dc_left_row_entry_result) = 2 * ge_signed_half_row_entry_resultproductleft + 1 /\ (sto_ap_row_entry_resultproduct) = 0) /\ (sto_an_row_entry_resultproduct) = S ge_signed_half_row_entry_resultproductleft))) /\ ((((((dc_right_row_entry_result) = 2 * (sto_bp_row_entry_resultproduct) /\ (sto_bn_row_entry_resultproduct) = 0) \/ exists ge_signed_half_row_entry_resultproductright. (((dc_right_row_entry_result) = 2 * ge_signed_half_row_entry_resultproductright + 1 /\ (sto_bp_row_entry_resultproduct) = 0) /\ (sto_bn_row_entry_resultproduct) = S ge_signed_half_row_entry_resultproductright))) /\ ((((((z) = 2 * (sto_cp_row_entry_resultproduct) /\ (sto_cn_row_entry_resultproduct) = 0) \/ exists ge_signed_half_row_entry_resultproductoutput. (((z) = 2 * ge_signed_half_row_entry_resultproductoutput + 1 /\ (sto_cp_row_entry_resultproduct) = 0) /\ (sto_cn_row_entry_resultproduct) = S ge_signed_half_row_entry_resultproductoutput))) /\ ((sto_ap_row_entry_resultproduct * sto_bp_row_entry_resultproduct + sto_an_row_entry_resultproduct * sto_bn_row_entry_resultproduct) + sto_cn_row_entry_resultproduct = (sto_ap_row_entry_resultproduct * sto_bn_row_entry_resultproduct + sto_an_row_entry_resultproduct * sto_bp_row_entry_resultproduct) + sto_cp_row_entry_resultproduct))))))))))))))) \/ ((((a)=0 \/ ~(exists pvs_factor_row_entry_resultnondivisor. (n) = (a) * pvs_factor_row_entry_resultnondivisor)) /\ ((z)=0))))Constructive proof overview
Generated structural guide
Each actual factor-row total is precisely an outer convolution summand of the genuine inner output table, with all positive-index bounds proved.
The unchanged tactic script uses 13 declared prerequisites and contains 158 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
eq_decidable Stable theorem; checked-use authorized DF0018 dirichlet_factor_row_zero_sum multiple_decidable_nonzero Stable theorem; checked-use authorized signed_table_lookup_any Alpha theorem; checked-use authorized DF0019 dirichlet_factor_row_sum_product signed_table_domain_resize Alpha theorem; checked-use authorized dirichlet_convolution_table_lookup Alpha theorem; checked-use authorized factor_nonzero_right Alpha theorem; checked-use authorized le_trans Stable theorem; checked-use authorized divisor_le_nonzero Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized dirichlet_convolution_sum_functional Alpha theorem; checked-use authorized dirichlet_convolution_entry_from_quotient Alpha theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–16
03Establish haL17–20
04Separate the logical casesL21–24
05Use earlier factsL25–34
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact ha_left - L26
specialize dirichlet_factor_row_zero_sum (F) - L27
specialize dirichlet_factor_row_zero_sum (G) - L28
specialize dirichlet_factor_row_zero_sum (H) - L29
specialize dirichlet_factor_row_zero_sum (n) - L30
specialize dirichlet_factor_row_zero_sum (a) - L31
specialize dirichlet_factor_row_zero_sum (V) - L32
specialize dirichlet_factor_row_zero_sum (z) - L33
apply dirichlet_factor_row_zero_sum - L34
exact hr
06Separate the logical casesL35–35
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L35
left
07Use earlier factsL36–37
08Establish hdL38–42
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple decidable nonzero.
- L38
have hd : (exists pvs_factor_row_entry_divisor. (n) = (a) * pvs_factor_row_entry_divisor) \/ ~(exists pvs_factor_row_entry_nondivisor. (n) = (a) * pvs_factor_row_entry_nondivisor) - L39
specialize multiple_decidable_nonzero (a) - L40
specialize multiple_decidable_nonzero (n) - L41
apply multiple_decidable_nonzero - L42
exact ha_right
09Separate the logical casesL43–44
10Establish hfL45–50
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.
11Separate the logical casesL51–51
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L51
cases hf
12Establish hiL52–61
Establish this local claim before using it. It is not an additional assumption.
- L52
have hi : ∃ v. DirichletSum(H,G,x,v) ∧ SignedMul(x1,v,z)Definitions: SignedMulDirichletSum - L53
specialize dirichlet_factor_row_sum_product (F) - L54
specialize dirichlet_factor_row_sum_product (G) - L55
specialize dirichlet_factor_row_sum_product (H) - L56
specialize dirichlet_factor_row_sum_product (n) - L57
specialize dirichlet_factor_row_sum_product (a) - L58
specialize dirichlet_factor_row_sum_product (x) - L59
specialize dirichlet_factor_row_sum_product (x1) - L60
specialize dirichlet_factor_row_sum_product (V) - L61
specialize dirichlet_factor_row_sum_product (z)
13Use earlier factsL62–66
14Separate the logical casesL67–69
15Use earlier factsL70–74
16Separate the logical casesL75–77
17Use earlier factsL78–84
18Separate the logical casesL85–86
19Establish htL87–96
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution table lookup.
- L87
have ht : ∃ v. ArithAt(U,x,v) ∧ DirichletSum(H,G,x,v)Definitions: ArithAtDirichletSum - L88
specialize dirichlet_convolution_table_lookup (N) - L89
specialize dirichlet_convolution_table_lookup (H) - L90
specialize dirichlet_convolution_table_lookup (G) - L91
specialize dirichlet_convolution_table_lookup (U) - L92
specialize dirichlet_convolution_table_lookup (x) - L93
apply dirichlet_convolution_table_lookup - L94
exact hU - L95
intro hx0 - L96
specialize factor_nonzero_right (n)
20Use earlier factsL97–106
Instantiate or apply named facts and discharge the corresponding proof obligations.
21Use earlier factsL107–110
22Construct an explicit witnessL111–111
Supply the displayed value, then prove that it has the required property.
- L111
exists a
23Calculate and transport equalitiesL112–112
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L112
trans a*x
24Use earlier factsL113–115
25Separate the logical casesL116–117
26Establish hvalueL118–127
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution sum functional.
- L118
have hvalue : x2=x3 - L119
specialize dirichlet_convolution_sum_functional (H) - L120
specialize dirichlet_convolution_sum_functional (G) - L121
specialize dirichlet_convolution_sum_functional (x) - L122
specialize dirichlet_convolution_sum_functional (x2) - L123
specialize dirichlet_convolution_sum_functional (x3) - L124
apply dirichlet_convolution_sum_functional - L125
exact hi_witness_left - L126
exact ht_witness_right - L127
rewrite hvalue at hi_witness_right
27Calculate and transport equalitiesL128–128
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L128
rewrite hvalue at hi_witness_right
28Use earlier factsL129–138
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L129
specialize dirichlet_convolution_entry_from_quotient (F) - L130
specialize dirichlet_convolution_entry_from_quotient (U) - L131
specialize dirichlet_convolution_entry_from_quotient (n) - L132
specialize dirichlet_convolution_entry_from_quotient (a) - L133
specialize dirichlet_convolution_entry_from_quotient (x) - L134
specialize dirichlet_convolution_entry_from_quotient (x1) - L135
specialize dirichlet_convolution_entry_from_quotient (x3) - L136
specialize dirichlet_convolution_entry_from_quotient (z) - L137
apply dirichlet_convolution_entry_from_quotient - L138
exact ha_right
29Use earlier factsL139–142
30Separate the logical casesL143–145
31Use earlier factsL146–155
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L146
exact hd_right - L147
specialize dirichlet_factor_row_zero_sum (F) - L148
specialize dirichlet_factor_row_zero_sum (G) - L149
specialize dirichlet_factor_row_zero_sum (H) - L150
specialize dirichlet_factor_row_zero_sum (n) - L151
specialize dirichlet_factor_row_zero_sum (a) - L152
specialize dirichlet_factor_row_zero_sum (V) - L153
specialize dirichlet_factor_row_zero_sum (z) - L154
apply dirichlet_factor_row_zero_sum - L155
exact hr
32Separate the logical casesL156–156
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L156
right
Original exact command ledger · 158 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro U - 0006
intro n - 0007
intro a - 0008
intro V - 0009
intro z - 0010
intro hF - 0011
intro hU - 0012
intro hn - 0013
intro hnN - 0014
intro haN - 0015
intro hr - 0016
intro hz - 0017
have ha : a=0 \/ ~(a=0) - 0018
specialize eq_decidable (a) - 0019
specialize eq_decidable (0) - 0020
apply eq_decidable - 0021
cases ha - 0022
right - 0023
split - 0024
left - 0025
exact ha_left - 0026
specialize dirichlet_factor_row_zero_sum (F) - 0027
specialize dirichlet_factor_row_zero_sum (G) - 0028
specialize dirichlet_factor_row_zero_sum (H) - 0029
specialize dirichlet_factor_row_zero_sum (n) - 0030
specialize dirichlet_factor_row_zero_sum (a) - 0031
specialize dirichlet_factor_row_zero_sum (V) - 0032
specialize dirichlet_factor_row_zero_sum (z) - 0033
apply dirichlet_factor_row_zero_sum - 0034
exact hr - 0035
left - 0036
exact ha_left - 0037
exact hz - 0038
have hd : (exists pvs_factor_row_entry_divisor. (n) = (a) * pvs_factor_row_entry_divisor) \/ ~(exists pvs_factor_row_entry_nondivisor. (n) = (a) * pvs_factor_row_entry_nondivisor) - 0039
specialize multiple_decidable_nonzero (a) - 0040
specialize multiple_decidable_nonzero (n) - 0041
apply multiple_decidable_nonzero - 0042
exact ha_right - 0043
cases hd - 0044
cases hd_left - 0045
have hf : exists u. (exists dst_positive_code_row_entry_first dst_positive_scale_row_entry_first dst_negative_code_row_entry_first dst_negative_scale_row_entry_first dst_positive_row_entry_first dst_negative_row_entry_first. (((F) = (((((dst_positive_code_row_entry_first) + (dst_positive_scale_row_entry_first)) * S ((dst_positive_code_row_entry_first) + (dst_positive_scale_row_entry_first)) + ((dst_positive_scale_row_entry_first) + (dst_positive_scale_row_entry_first))) + (((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) * S ((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) + ((dst_negative_scale_row_entry_first) + (dst_negative_scale_row_entry_first)))) * S ((((dst_positive_code_row_entry_first) + (dst_positive_scale_row_entry_first)) * S ((dst_positive_code_row_entry_first) + (dst_positive_scale_row_entry_first)) + ((dst_positive_scale_row_entry_first) + (dst_positive_scale_row_entry_first))) + (((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) * S ((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) + ((dst_negative_scale_row_entry_first) + (dst_negative_scale_row_entry_first)))) + ((((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) * S ((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) + ((dst_negative_scale_row_entry_first) + (dst_negative_scale_row_entry_first))) + (((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) * S ((dst_negative_code_row_entry_first) + (dst_negative_scale_row_entry_first)) + ((dst_negative_scale_row_entry_first) + (dst_negative_scale_row_entry_first)))))) /\ (((((exists ff_h_pvs_row_entry_firstpositive. ff_h_pvs_row_entry_firstpositive + S (dst_positive_row_entry_first) = S ((S (a)) * dst_positive_scale_row_entry_first)) /\ exists ff_q_pvs_row_entry_firstpositive. dst_positive_code_row_entry_first = ff_q_pvs_row_entry_firstpositive * S ((S (a)) * dst_positive_scale_row_entry_first) + (dst_positive_row_entry_first))) /\ (((((exists ff_h_pvs_row_entry_firstnegative. ff_h_pvs_row_entry_firstnegative + S (dst_negative_row_entry_first) = S ((S (a)) * dst_negative_scale_row_entry_first)) /\ exists ff_q_pvs_row_entry_firstnegative. dst_negative_code_row_entry_first = ff_q_pvs_row_entry_firstnegative * S ((S (a)) * dst_negative_scale_row_entry_first) + (dst_negative_row_entry_first))) /\ (exists ge_balance_positive_row_entry_firstvalue ge_balance_negative_row_entry_firstvalue. (((((u) = 2 * (ge_balance_positive_row_entry_firstvalue) /\ (ge_balance_negative_row_entry_firstvalue) = 0) \/ exists ge_signed_half_row_entry_firstvaluedecode. (((u) = 2 * ge_signed_half_row_entry_firstvaluedecode + 1 /\ (ge_balance_positive_row_entry_firstvalue) = 0) /\ (ge_balance_negative_row_entry_firstvalue) = S ge_signed_half_row_entry_firstvaluedecode))) /\ ((dst_positive_row_entry_first) + ge_balance_negative_row_entry_firstvalue = (dst_negative_row_entry_first) + ge_balance_positive_row_entry_firstvalue))))))))) - 0046
specialize signed_table_lookup_any (N) - 0047
specialize signed_table_lookup_any (F) - 0048
specialize signed_table_lookup_any (a) - 0049
apply signed_table_lookup_any - 0050
exact hF - 0051
cases hf - 0052
have hi : exists v. (((((~((x)=0)) /\ (exists dc_mask_row_entry_inner. ((((exists dst_positive_code_row_entry_innermasktable dst_positive_scale_row_entry_innermasktable dst_negative_code_row_entry_innermasktable dst_negative_scale_row_entry_innermasktable. (((dc_mask_row_entry_inner) = (((((dst_positive_code_row_entry_innermasktable) + (dst_positive_scale_row_entry_innermasktable)) * S ((dst_positive_code_row_entry_innermasktable) + (dst_positive_scale_row_entry_innermasktable)) + ((dst_positive_scale_row_entry_innermasktable) + (dst_positive_scale_row_entry_innermasktable))) + (((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) * S ((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) + ((dst_negative_scale_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)))) * S ((((dst_positive_code_row_entry_innermasktable) + (dst_positive_scale_row_entry_innermasktable)) * S ((dst_positive_code_row_entry_innermasktable) + (dst_positive_scale_row_entry_innermasktable)) + ((dst_positive_scale_row_entry_innermasktable) + (dst_positive_scale_row_entry_innermasktable))) + (((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) * S ((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) + ((dst_negative_scale_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)))) + ((((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) * S ((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) + ((dst_negative_scale_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable))) + (((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) * S ((dst_negative_code_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)) + ((dst_negative_scale_row_entry_innermasktable) + (dst_negative_scale_row_entry_innermasktable)))))) /\ (forall dst_index_row_entry_innermasktable. (exists pvs_le_gap_row_entry_innermasktabledomain. pvs_le_gap_row_entry_innermasktabledomain + (dst_index_row_entry_innermasktable) = (x)) -> exists dst_positive_row_entry_innermasktable dst_negative_row_entry_innermasktable dst_value_row_entry_innermasktable. ((((exists ff_h_pvs_row_entry_innermasktableentrypositive. ff_h_pvs_row_entry_innermasktableentrypositive + S (dst_positive_row_entry_innermasktable) = S ((S (dst_index_row_entry_innermasktable)) * dst_positive_scale_row_entry_innermasktable)) /\ exists ff_q_pvs_row_entry_innermasktableentrypositive. dst_positive_code_row_entry_innermasktable = ff_q_pvs_row_entry_innermasktableentrypositive * S ((S (dst_index_row_entry_innermasktable)) * dst_positive_scale_row_entry_innermasktable) + (dst_positive_row_entry_innermasktable))) /\ (((((exists ff_h_pvs_row_entry_innermasktableentrynegative. ff_h_pvs_row_entry_innermasktableentrynegative + S (dst_negative_row_entry_innermasktable) = S ((S (dst_index_row_entry_innermasktable)) * dst_negative_scale_row_entry_innermasktable)) /\ exists ff_q_pvs_row_entry_innermasktableentrynegative. dst_negative_code_row_entry_innermasktable = ff_q_pvs_row_entry_innermasktableentrynegative * S ((S (dst_index_row_entry_innermasktable)) * dst_negative_scale_row_entry_innermasktable) + (dst_negative_row_entry_innermasktable))) /\ (exists ge_balance_positive_row_entry_innermasktableentryvalue ge_balance_negative_row_entry_innermasktableentryvalue. (((((dst_value_row_entry_innermasktable) = 2 * (ge_balance_positive_row_entry_innermasktableentryvalue) /\ (ge_balance_negative_row_entry_innermasktableentryvalue) = 0) \/ exists ge_signed_half_row_entry_innermasktableentryvaluedecode. (((dst_value_row_entry_innermasktable) = 2 * ge_signed_half_row_entry_innermasktableentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_innermasktableentryvalue) = 0) /\ (ge_balance_negative_row_entry_innermasktableentryvalue) = S ge_signed_half_row_entry_innermasktableentryvaluedecode))) /\ ((dst_positive_row_entry_innermasktable) + ge_balance_negative_row_entry_innermasktableentryvalue = (dst_negative_row_entry_innermasktable) + ge_balance_positive_row_entry_innermasktableentryvalue))))))))) /\ (forall dc_index_row_entry_innermask dc_value_row_entry_innermask. (exists pvs_le_gap_row_entry_innermaskdomain. pvs_le_gap_row_entry_innermaskdomain + (dc_index_row_entry_innermask) = (x)) -> (exists dst_positive_code_row_entry_innermasklookup dst_positive_scale_row_entry_innermasklookup dst_negative_code_row_entry_innermasklookup dst_negative_scale_row_entry_innermasklookup dst_positive_row_entry_innermasklookup dst_negative_row_entry_innermasklookup. (((dc_mask_row_entry_inner) = (((((dst_positive_code_row_entry_innermasklookup) + (dst_positive_scale_row_entry_innermasklookup)) * S ((dst_positive_code_row_entry_innermasklookup) + (dst_positive_scale_row_entry_innermasklookup)) + ((dst_positive_scale_row_entry_innermasklookup) + (dst_positive_scale_row_entry_innermasklookup))) + (((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) * S ((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) + ((dst_negative_scale_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)))) * S ((((dst_positive_code_row_entry_innermasklookup) + (dst_positive_scale_row_entry_innermasklookup)) * S ((dst_positive_code_row_entry_innermasklookup) + (dst_positive_scale_row_entry_innermasklookup)) + ((dst_positive_scale_row_entry_innermasklookup) + (dst_positive_scale_row_entry_innermasklookup))) + (((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) * S ((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) + ((dst_negative_scale_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)))) + ((((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) * S ((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) + ((dst_negative_scale_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup))) + (((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) * S ((dst_negative_code_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)) + ((dst_negative_scale_row_entry_innermasklookup) + (dst_negative_scale_row_entry_innermasklookup)))))) /\ (((((exists ff_h_pvs_row_entry_innermasklookuppositive. ff_h_pvs_row_entry_innermasklookuppositive + S (dst_positive_row_entry_innermasklookup) = S ((S (dc_index_row_entry_innermask)) * dst_positive_scale_row_entry_innermasklookup)) /\ exists ff_q_pvs_row_entry_innermasklookuppositive. dst_positive_code_row_entry_innermasklookup = ff_q_pvs_row_entry_innermasklookuppositive * S ((S (dc_index_row_entry_innermask)) * dst_positive_scale_row_entry_innermasklookup) + (dst_positive_row_entry_innermasklookup))) /\ (((((exists ff_h_pvs_row_entry_innermasklookupnegative. ff_h_pvs_row_entry_innermasklookupnegative + S (dst_negative_row_entry_innermasklookup) = S ((S (dc_index_row_entry_innermask)) * dst_negative_scale_row_entry_innermasklookup)) /\ exists ff_q_pvs_row_entry_innermasklookupnegative. dst_negative_code_row_entry_innermasklookup = ff_q_pvs_row_entry_innermasklookupnegative * S ((S (dc_index_row_entry_innermask)) * dst_negative_scale_row_entry_innermasklookup) + (dst_negative_row_entry_innermasklookup))) /\ (exists ge_balance_positive_row_entry_innermasklookupvalue ge_balance_negative_row_entry_innermasklookupvalue. (((((dc_value_row_entry_innermask) = 2 * (ge_balance_positive_row_entry_innermasklookupvalue) /\ (ge_balance_negative_row_entry_innermasklookupvalue) = 0) \/ exists ge_signed_half_row_entry_innermasklookupvaluedecode. (((dc_value_row_entry_innermask) = 2 * ge_signed_half_row_entry_innermasklookupvaluedecode + 1 /\ (ge_balance_positive_row_entry_innermasklookupvalue) = 0) /\ (ge_balance_negative_row_entry_innermasklookupvalue) = S ge_signed_half_row_entry_innermasklookupvaluedecode))) /\ ((dst_positive_row_entry_innermasklookup) + ge_balance_negative_row_entry_innermasklookupvalue = (dst_negative_row_entry_innermasklookup) + ge_balance_positive_row_entry_innermasklookupvalue))))))))) -> ((((~((dc_index_row_entry_innermask)=0)) /\ (exists dc_quotient_row_entry_innermaskentry dc_left_row_entry_innermaskentry dc_right_row_entry_innermaskentry. (((x)=(dc_index_row_entry_innermask)*dc_quotient_row_entry_innermaskentry) /\ (((exists dst_positive_code_row_entry_innermaskentryleft dst_positive_scale_row_entry_innermaskentryleft dst_negative_code_row_entry_innermaskentryleft dst_negative_scale_row_entry_innermaskentryleft dst_positive_row_entry_innermaskentryleft dst_negative_row_entry_innermaskentryleft. (((H) = (((((dst_positive_code_row_entry_innermaskentryleft) + (dst_positive_scale_row_entry_innermaskentryleft)) * S ((dst_positive_code_row_entry_innermaskentryleft) + (dst_positive_scale_row_entry_innermaskentryleft)) + ((dst_positive_scale_row_entry_innermaskentryleft) + (dst_positive_scale_row_entry_innermaskentryleft))) + (((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) * S ((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) + ((dst_negative_scale_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)))) * S ((((dst_positive_code_row_entry_innermaskentryleft) + (dst_positive_scale_row_entry_innermaskentryleft)) * S ((dst_positive_code_row_entry_innermaskentryleft) + (dst_positive_scale_row_entry_innermaskentryleft)) + ((dst_positive_scale_row_entry_innermaskentryleft) + (dst_positive_scale_row_entry_innermaskentryleft))) + (((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) * S ((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) + ((dst_negative_scale_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)))) + ((((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) * S ((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) + ((dst_negative_scale_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft))) + (((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) * S ((dst_negative_code_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)) + ((dst_negative_scale_row_entry_innermaskentryleft) + (dst_negative_scale_row_entry_innermaskentryleft)))))) /\ (((((exists ff_h_pvs_row_entry_innermaskentryleftpositive. ff_h_pvs_row_entry_innermaskentryleftpositive + S (dst_positive_row_entry_innermaskentryleft) = S ((S (dc_index_row_entry_innermask)) * dst_positive_scale_row_entry_innermaskentryleft)) /\ exists ff_q_pvs_row_entry_innermaskentryleftpositive. dst_positive_code_row_entry_innermaskentryleft = ff_q_pvs_row_entry_innermaskentryleftpositive * S ((S (dc_index_row_entry_innermask)) * dst_positive_scale_row_entry_innermaskentryleft) + (dst_positive_row_entry_innermaskentryleft))) /\ (((((exists ff_h_pvs_row_entry_innermaskentryleftnegative. ff_h_pvs_row_entry_innermaskentryleftnegative + S (dst_negative_row_entry_innermaskentryleft) = S ((S (dc_index_row_entry_innermask)) * dst_negative_scale_row_entry_innermaskentryleft)) /\ exists ff_q_pvs_row_entry_innermaskentryleftnegative. dst_negative_code_row_entry_innermaskentryleft = ff_q_pvs_row_entry_innermaskentryleftnegative * S ((S (dc_index_row_entry_innermask)) * dst_negative_scale_row_entry_innermaskentryleft) + (dst_negative_row_entry_innermaskentryleft))) /\ (exists ge_balance_positive_row_entry_innermaskentryleftvalue ge_balance_negative_row_entry_innermaskentryleftvalue. (((((dc_left_row_entry_innermaskentry) = 2 * (ge_balance_positive_row_entry_innermaskentryleftvalue) /\ (ge_balance_negative_row_entry_innermaskentryleftvalue) = 0) \/ exists ge_signed_half_row_entry_innermaskentryleftvaluedecode. (((dc_left_row_entry_innermaskentry) = 2 * ge_signed_half_row_entry_innermaskentryleftvaluedecode + 1 /\ (ge_balance_positive_row_entry_innermaskentryleftvalue) = 0) /\ (ge_balance_negative_row_entry_innermaskentryleftvalue) = S ge_signed_half_row_entry_innermaskentryleftvaluedecode))) /\ ((dst_positive_row_entry_innermaskentryleft) + ge_balance_negative_row_entry_innermaskentryleftvalue = (dst_negative_row_entry_innermaskentryleft) + ge_balance_positive_row_entry_innermaskentryleftvalue))))))))) /\ (((exists dst_positive_code_row_entry_innermaskentryright dst_positive_scale_row_entry_innermaskentryright dst_negative_code_row_entry_innermaskentryright dst_negative_scale_row_entry_innermaskentryright dst_positive_row_entry_innermaskentryright dst_negative_row_entry_innermaskentryright. (((G) = (((((dst_positive_code_row_entry_innermaskentryright) + (dst_positive_scale_row_entry_innermaskentryright)) * S ((dst_positive_code_row_entry_innermaskentryright) + (dst_positive_scale_row_entry_innermaskentryright)) + ((dst_positive_scale_row_entry_innermaskentryright) + (dst_positive_scale_row_entry_innermaskentryright))) + (((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) * S ((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) + ((dst_negative_scale_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)))) * S ((((dst_positive_code_row_entry_innermaskentryright) + (dst_positive_scale_row_entry_innermaskentryright)) * S ((dst_positive_code_row_entry_innermaskentryright) + (dst_positive_scale_row_entry_innermaskentryright)) + ((dst_positive_scale_row_entry_innermaskentryright) + (dst_positive_scale_row_entry_innermaskentryright))) + (((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) * S ((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) + ((dst_negative_scale_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)))) + ((((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) * S ((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) + ((dst_negative_scale_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright))) + (((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) * S ((dst_negative_code_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)) + ((dst_negative_scale_row_entry_innermaskentryright) + (dst_negative_scale_row_entry_innermaskentryright)))))) /\ (((((exists ff_h_pvs_row_entry_innermaskentryrightpositive. ff_h_pvs_row_entry_innermaskentryrightpositive + S (dst_positive_row_entry_innermaskentryright) = S ((S (dc_quotient_row_entry_innermaskentry)) * dst_positive_scale_row_entry_innermaskentryright)) /\ exists ff_q_pvs_row_entry_innermaskentryrightpositive. dst_positive_code_row_entry_innermaskentryright = ff_q_pvs_row_entry_innermaskentryrightpositive * S ((S (dc_quotient_row_entry_innermaskentry)) * dst_positive_scale_row_entry_innermaskentryright) + (dst_positive_row_entry_innermaskentryright))) /\ (((((exists ff_h_pvs_row_entry_innermaskentryrightnegative. ff_h_pvs_row_entry_innermaskentryrightnegative + S (dst_negative_row_entry_innermaskentryright) = S ((S (dc_quotient_row_entry_innermaskentry)) * dst_negative_scale_row_entry_innermaskentryright)) /\ exists ff_q_pvs_row_entry_innermaskentryrightnegative. dst_negative_code_row_entry_innermaskentryright = ff_q_pvs_row_entry_innermaskentryrightnegative * S ((S (dc_quotient_row_entry_innermaskentry)) * dst_negative_scale_row_entry_innermaskentryright) + (dst_negative_row_entry_innermaskentryright))) /\ (exists ge_balance_positive_row_entry_innermaskentryrightvalue ge_balance_negative_row_entry_innermaskentryrightvalue. (((((dc_right_row_entry_innermaskentry) = 2 * (ge_balance_positive_row_entry_innermaskentryrightvalue) /\ (ge_balance_negative_row_entry_innermaskentryrightvalue) = 0) \/ exists ge_signed_half_row_entry_innermaskentryrightvaluedecode. (((dc_right_row_entry_innermaskentry) = 2 * ge_signed_half_row_entry_innermaskentryrightvaluedecode + 1 /\ (ge_balance_positive_row_entry_innermaskentryrightvalue) = 0) /\ (ge_balance_negative_row_entry_innermaskentryrightvalue) = S ge_signed_half_row_entry_innermaskentryrightvaluedecode))) /\ ((dst_positive_row_entry_innermaskentryright) + ge_balance_negative_row_entry_innermaskentryrightvalue = (dst_negative_row_entry_innermaskentryright) + ge_balance_positive_row_entry_innermaskentryrightvalue))))))))) /\ (exists sto_ap_row_entry_innermaskentryproduct sto_an_row_entry_innermaskentryproduct sto_bp_row_entry_innermaskentryproduct sto_bn_row_entry_innermaskentryproduct sto_cp_row_entry_innermaskentryproduct sto_cn_row_entry_innermaskentryproduct. (((((dc_left_row_entry_innermaskentry) = 2 * (sto_ap_row_entry_innermaskentryproduct) /\ (sto_an_row_entry_innermaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_innermaskentryproductleft. (((dc_left_row_entry_innermaskentry) = 2 * ge_signed_half_row_entry_innermaskentryproductleft + 1 /\ (sto_ap_row_entry_innermaskentryproduct) = 0) /\ (sto_an_row_entry_innermaskentryproduct) = S ge_signed_half_row_entry_innermaskentryproductleft))) /\ ((((((dc_right_row_entry_innermaskentry) = 2 * (sto_bp_row_entry_innermaskentryproduct) /\ (sto_bn_row_entry_innermaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_innermaskentryproductright. (((dc_right_row_entry_innermaskentry) = 2 * ge_signed_half_row_entry_innermaskentryproductright + 1 /\ (sto_bp_row_entry_innermaskentryproduct) = 0) /\ (sto_bn_row_entry_innermaskentryproduct) = S ge_signed_half_row_entry_innermaskentryproductright))) /\ ((((((dc_value_row_entry_innermask) = 2 * (sto_cp_row_entry_innermaskentryproduct) /\ (sto_cn_row_entry_innermaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_innermaskentryproductoutput. (((dc_value_row_entry_innermask) = 2 * ge_signed_half_row_entry_innermaskentryproductoutput + 1 /\ (sto_cp_row_entry_innermaskentryproduct) = 0) /\ (sto_cn_row_entry_innermaskentryproduct) = S ge_signed_half_row_entry_innermaskentryproductoutput))) /\ ((sto_ap_row_entry_innermaskentryproduct * sto_bp_row_entry_innermaskentryproduct + sto_an_row_entry_innermaskentryproduct * sto_bn_row_entry_innermaskentryproduct) + sto_cn_row_entry_innermaskentryproduct = (sto_ap_row_entry_innermaskentryproduct * sto_bn_row_entry_innermaskentryproduct + sto_an_row_entry_innermaskentryproduct * sto_bp_row_entry_innermaskentryproduct) + sto_cp_row_entry_innermaskentryproduct))))))))))))))) \/ ((((dc_index_row_entry_innermask)=0 \/ ~(exists pvs_factor_row_entry_innermaskentrynondivisor. (x) = (dc_index_row_entry_innermask) * pvs_factor_row_entry_innermaskentrynondivisor)) /\ ((dc_value_row_entry_innermask)=0))))))) /\ (exists dst_positive_code_row_entry_innerfold dst_positive_scale_row_entry_innerfold dst_negative_code_row_entry_innerfold dst_negative_scale_row_entry_innerfold dst_positive_sum_row_entry_innerfold dst_negative_sum_row_entry_innerfold. (((dc_mask_row_entry_inner) = (((((dst_positive_code_row_entry_innerfold) + (dst_positive_scale_row_entry_innerfold)) * S ((dst_positive_code_row_entry_innerfold) + (dst_positive_scale_row_entry_innerfold)) + ((dst_positive_scale_row_entry_innerfold) + (dst_positive_scale_row_entry_innerfold))) + (((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) * S ((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) + ((dst_negative_scale_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)))) * S ((((dst_positive_code_row_entry_innerfold) + (dst_positive_scale_row_entry_innerfold)) * S ((dst_positive_code_row_entry_innerfold) + (dst_positive_scale_row_entry_innerfold)) + ((dst_positive_scale_row_entry_innerfold) + (dst_positive_scale_row_entry_innerfold))) + (((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) * S ((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) + ((dst_negative_scale_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)))) + ((((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) * S ((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) + ((dst_negative_scale_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold))) + (((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) * S ((dst_negative_code_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)) + ((dst_negative_scale_row_entry_innerfold) + (dst_negative_scale_row_entry_innerfold)))))) /\ (((exists fs_u_dst_row_entry_innerfoldpositive fs_v_dst_row_entry_innerfoldpositive. ((((exists fs_h_dst_row_entry_innerfoldpositive_body_start. fs_h_dst_row_entry_innerfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_innerfoldpositive)) /\ exists fs_q_dst_row_entry_innerfoldpositive_body_start. fs_u_dst_row_entry_innerfoldpositive = fs_q_dst_row_entry_innerfoldpositive_body_start * S ((S (0)) * fs_v_dst_row_entry_innerfoldpositive) + (0))) /\ ((((exists fs_h_dst_row_entry_innerfoldpositive_body_terminal. fs_h_dst_row_entry_innerfoldpositive_body_terminal + S (dst_positive_sum_row_entry_innerfold) = S ((S (S (x))) * fs_v_dst_row_entry_innerfoldpositive)) /\ exists fs_q_dst_row_entry_innerfoldpositive_body_terminal. fs_u_dst_row_entry_innerfoldpositive = fs_q_dst_row_entry_innerfoldpositive_body_terminal * S ((S (S (x))) * fs_v_dst_row_entry_innerfoldpositive) + (dst_positive_sum_row_entry_innerfold))) /\ forall fs_i_dst_row_entry_innerfoldpositive_body_steps. (exists fs_lt_dst_row_entry_innerfoldpositive_body_steps_bound. fs_lt_dst_row_entry_innerfoldpositive_body_steps_bound + S fs_i_dst_row_entry_innerfoldpositive_body_steps = S (x)) -> exists fs_a_dst_row_entry_innerfoldpositive_body_steps fs_r_dst_row_entry_innerfoldpositive_body_steps fs_s_dst_row_entry_innerfoldpositive_body_steps. ((((exists fs_h_dst_row_entry_innerfoldpositive_body_steps_summand. fs_h_dst_row_entry_innerfoldpositive_body_steps_summand + S (fs_a_dst_row_entry_innerfoldpositive_body_steps) = S ((S (fs_i_dst_row_entry_innerfoldpositive_body_steps)) * dst_positive_scale_row_entry_innerfold)) /\ exists fs_q_dst_row_entry_innerfoldpositive_body_steps_summand. dst_positive_code_row_entry_innerfold = fs_q_dst_row_entry_innerfoldpositive_body_steps_summand * S ((S (fs_i_dst_row_entry_innerfoldpositive_body_steps)) * dst_positive_scale_row_entry_innerfold) + (fs_a_dst_row_entry_innerfoldpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_innerfoldpositive_body_steps_partial. fs_h_dst_row_entry_innerfoldpositive_body_steps_partial + S (fs_r_dst_row_entry_innerfoldpositive_body_steps) = S ((S (fs_i_dst_row_entry_innerfoldpositive_body_steps)) * fs_v_dst_row_entry_innerfoldpositive)) /\ exists fs_q_dst_row_entry_innerfoldpositive_body_steps_partial. fs_u_dst_row_entry_innerfoldpositive = fs_q_dst_row_entry_innerfoldpositive_body_steps_partial * S ((S (fs_i_dst_row_entry_innerfoldpositive_body_steps)) * fs_v_dst_row_entry_innerfoldpositive) + (fs_r_dst_row_entry_innerfoldpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_innerfoldpositive_body_steps_successor. fs_h_dst_row_entry_innerfoldpositive_body_steps_successor + S (fs_s_dst_row_entry_innerfoldpositive_body_steps) = S ((S (S fs_i_dst_row_entry_innerfoldpositive_body_steps)) * fs_v_dst_row_entry_innerfoldpositive)) /\ exists fs_q_dst_row_entry_innerfoldpositive_body_steps_successor. fs_u_dst_row_entry_innerfoldpositive = fs_q_dst_row_entry_innerfoldpositive_body_steps_successor * S ((S (S fs_i_dst_row_entry_innerfoldpositive_body_steps)) * fs_v_dst_row_entry_innerfoldpositive) + (fs_s_dst_row_entry_innerfoldpositive_body_steps))) /\ fs_s_dst_row_entry_innerfoldpositive_body_steps = fs_r_dst_row_entry_innerfoldpositive_body_steps + fs_a_dst_row_entry_innerfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_row_entry_innerfoldnegative fs_v_dst_row_entry_innerfoldnegative. ((((exists fs_h_dst_row_entry_innerfoldnegative_body_start. fs_h_dst_row_entry_innerfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_innerfoldnegative)) /\ exists fs_q_dst_row_entry_innerfoldnegative_body_start. fs_u_dst_row_entry_innerfoldnegative = fs_q_dst_row_entry_innerfoldnegative_body_start * S ((S (0)) * fs_v_dst_row_entry_innerfoldnegative) + (0))) /\ ((((exists fs_h_dst_row_entry_innerfoldnegative_body_terminal. fs_h_dst_row_entry_innerfoldnegative_body_terminal + S (dst_negative_sum_row_entry_innerfold) = S ((S (S (x))) * fs_v_dst_row_entry_innerfoldnegative)) /\ exists fs_q_dst_row_entry_innerfoldnegative_body_terminal. fs_u_dst_row_entry_innerfoldnegative = fs_q_dst_row_entry_innerfoldnegative_body_terminal * S ((S (S (x))) * fs_v_dst_row_entry_innerfoldnegative) + (dst_negative_sum_row_entry_innerfold))) /\ forall fs_i_dst_row_entry_innerfoldnegative_body_steps. (exists fs_lt_dst_row_entry_innerfoldnegative_body_steps_bound. fs_lt_dst_row_entry_innerfoldnegative_body_steps_bound + S fs_i_dst_row_entry_innerfoldnegative_body_steps = S (x)) -> exists fs_a_dst_row_entry_innerfoldnegative_body_steps fs_r_dst_row_entry_innerfoldnegative_body_steps fs_s_dst_row_entry_innerfoldnegative_body_steps. ((((exists fs_h_dst_row_entry_innerfoldnegative_body_steps_summand. fs_h_dst_row_entry_innerfoldnegative_body_steps_summand + S (fs_a_dst_row_entry_innerfoldnegative_body_steps) = S ((S (fs_i_dst_row_entry_innerfoldnegative_body_steps)) * dst_negative_scale_row_entry_innerfold)) /\ exists fs_q_dst_row_entry_innerfoldnegative_body_steps_summand. dst_negative_code_row_entry_innerfold = fs_q_dst_row_entry_innerfoldnegative_body_steps_summand * S ((S (fs_i_dst_row_entry_innerfoldnegative_body_steps)) * dst_negative_scale_row_entry_innerfold) + (fs_a_dst_row_entry_innerfoldnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_innerfoldnegative_body_steps_partial. fs_h_dst_row_entry_innerfoldnegative_body_steps_partial + S (fs_r_dst_row_entry_innerfoldnegative_body_steps) = S ((S (fs_i_dst_row_entry_innerfoldnegative_body_steps)) * fs_v_dst_row_entry_innerfoldnegative)) /\ exists fs_q_dst_row_entry_innerfoldnegative_body_steps_partial. fs_u_dst_row_entry_innerfoldnegative = fs_q_dst_row_entry_innerfoldnegative_body_steps_partial * S ((S (fs_i_dst_row_entry_innerfoldnegative_body_steps)) * fs_v_dst_row_entry_innerfoldnegative) + (fs_r_dst_row_entry_innerfoldnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_innerfoldnegative_body_steps_successor. fs_h_dst_row_entry_innerfoldnegative_body_steps_successor + S (fs_s_dst_row_entry_innerfoldnegative_body_steps) = S ((S (S fs_i_dst_row_entry_innerfoldnegative_body_steps)) * fs_v_dst_row_entry_innerfoldnegative)) /\ exists fs_q_dst_row_entry_innerfoldnegative_body_steps_successor. fs_u_dst_row_entry_innerfoldnegative = fs_q_dst_row_entry_innerfoldnegative_body_steps_successor * S ((S (S fs_i_dst_row_entry_innerfoldnegative_body_steps)) * fs_v_dst_row_entry_innerfoldnegative) + (fs_s_dst_row_entry_innerfoldnegative_body_steps))) /\ fs_s_dst_row_entry_innerfoldnegative_body_steps = fs_r_dst_row_entry_innerfoldnegative_body_steps + fs_a_dst_row_entry_innerfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_row_entry_innerfoldresult ge_balance_negative_row_entry_innerfoldresult. (((((v) = 2 * (ge_balance_positive_row_entry_innerfoldresult) /\ (ge_balance_negative_row_entry_innerfoldresult) = 0) \/ exists ge_signed_half_row_entry_innerfoldresultdecode. (((v) = 2 * ge_signed_half_row_entry_innerfoldresultdecode + 1 /\ (ge_balance_positive_row_entry_innerfoldresult) = 0) /\ (ge_balance_negative_row_entry_innerfoldresult) = S ge_signed_half_row_entry_innerfoldresultdecode))) /\ ((dst_positive_sum_row_entry_innerfold) + ge_balance_negative_row_entry_innerfoldresult = (dst_negative_sum_row_entry_innerfold) + ge_balance_positive_row_entry_innerfoldresult))))))))))))) /\ (exists sto_ap_row_entry_scaled sto_an_row_entry_scaled sto_bp_row_entry_scaled sto_bn_row_entry_scaled sto_cp_row_entry_scaled sto_cn_row_entry_scaled. (((((x1) = 2 * (sto_ap_row_entry_scaled) /\ (sto_an_row_entry_scaled) = 0) \/ exists ge_signed_half_row_entry_scaledleft. (((x1) = 2 * ge_signed_half_row_entry_scaledleft + 1 /\ (sto_ap_row_entry_scaled) = 0) /\ (sto_an_row_entry_scaled) = S ge_signed_half_row_entry_scaledleft))) /\ ((((((v) = 2 * (sto_bp_row_entry_scaled) /\ (sto_bn_row_entry_scaled) = 0) \/ exists ge_signed_half_row_entry_scaledright. (((v) = 2 * ge_signed_half_row_entry_scaledright + 1 /\ (sto_bp_row_entry_scaled) = 0) /\ (sto_bn_row_entry_scaled) = S ge_signed_half_row_entry_scaledright))) /\ ((((((z) = 2 * (sto_cp_row_entry_scaled) /\ (sto_cn_row_entry_scaled) = 0) \/ exists ge_signed_half_row_entry_scaledoutput. (((z) = 2 * ge_signed_half_row_entry_scaledoutput + 1 /\ (sto_cp_row_entry_scaled) = 0) /\ (sto_cn_row_entry_scaled) = S ge_signed_half_row_entry_scaledoutput))) /\ ((sto_ap_row_entry_scaled * sto_bp_row_entry_scaled + sto_an_row_entry_scaled * sto_bn_row_entry_scaled) + sto_cn_row_entry_scaled = (sto_ap_row_entry_scaled * sto_bn_row_entry_scaled + sto_an_row_entry_scaled * sto_bp_row_entry_scaled) + sto_cp_row_entry_scaled))))))))) - 0053
specialize dirichlet_factor_row_sum_product (F) - 0054
specialize dirichlet_factor_row_sum_product (G) - 0055
specialize dirichlet_factor_row_sum_product (H) - 0056
specialize dirichlet_factor_row_sum_product (n) - 0057
specialize dirichlet_factor_row_sum_product (a) - 0058
specialize dirichlet_factor_row_sum_product (x) - 0059
specialize dirichlet_factor_row_sum_product (x1) - 0060
specialize dirichlet_factor_row_sum_product (V) - 0061
specialize dirichlet_factor_row_sum_product (z) - 0062
apply dirichlet_factor_row_sum_product - 0063
specialize signed_table_domain_resize (N) - 0064
specialize signed_table_domain_resize (0) - 0065
specialize signed_table_domain_resize (H) - 0066
apply signed_table_domain_resize - 0067
cases hU - 0068
cases hU_right - 0069
cases hU_right_right - 0070
exact hU_left - 0071
specialize signed_table_domain_resize (N) - 0072
specialize signed_table_domain_resize (0) - 0073
specialize signed_table_domain_resize (G) - 0074
apply signed_table_domain_resize - 0075
cases hU - 0076
cases hU_right - 0077
cases hU_right_right - 0078
exact hU_right_left - 0079
exact hn - 0080
exact ha_right - 0081
exact hd_left_witness - 0082
exact hf_witness - 0083
exact hr - 0084
exact hz - 0085
cases hi - 0086
cases hi_witness - 0087
have ht : exists v. (((exists dst_positive_code_row_entry_output_lookup dst_positive_scale_row_entry_output_lookup dst_negative_code_row_entry_output_lookup dst_negative_scale_row_entry_output_lookup dst_positive_row_entry_output_lookup dst_negative_row_entry_output_lookup. (((U) = (((((dst_positive_code_row_entry_output_lookup) + (dst_positive_scale_row_entry_output_lookup)) * S ((dst_positive_code_row_entry_output_lookup) + (dst_positive_scale_row_entry_output_lookup)) + ((dst_positive_scale_row_entry_output_lookup) + (dst_positive_scale_row_entry_output_lookup))) + (((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) * S ((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) + ((dst_negative_scale_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)))) * S ((((dst_positive_code_row_entry_output_lookup) + (dst_positive_scale_row_entry_output_lookup)) * S ((dst_positive_code_row_entry_output_lookup) + (dst_positive_scale_row_entry_output_lookup)) + ((dst_positive_scale_row_entry_output_lookup) + (dst_positive_scale_row_entry_output_lookup))) + (((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) * S ((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) + ((dst_negative_scale_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)))) + ((((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) * S ((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) + ((dst_negative_scale_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup))) + (((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) * S ((dst_negative_code_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)) + ((dst_negative_scale_row_entry_output_lookup) + (dst_negative_scale_row_entry_output_lookup)))))) /\ (((((exists ff_h_pvs_row_entry_output_lookuppositive. ff_h_pvs_row_entry_output_lookuppositive + S (dst_positive_row_entry_output_lookup) = S ((S (x)) * dst_positive_scale_row_entry_output_lookup)) /\ exists ff_q_pvs_row_entry_output_lookuppositive. dst_positive_code_row_entry_output_lookup = ff_q_pvs_row_entry_output_lookuppositive * S ((S (x)) * dst_positive_scale_row_entry_output_lookup) + (dst_positive_row_entry_output_lookup))) /\ (((((exists ff_h_pvs_row_entry_output_lookupnegative. ff_h_pvs_row_entry_output_lookupnegative + S (dst_negative_row_entry_output_lookup) = S ((S (x)) * dst_negative_scale_row_entry_output_lookup)) /\ exists ff_q_pvs_row_entry_output_lookupnegative. dst_negative_code_row_entry_output_lookup = ff_q_pvs_row_entry_output_lookupnegative * S ((S (x)) * dst_negative_scale_row_entry_output_lookup) + (dst_negative_row_entry_output_lookup))) /\ (exists ge_balance_positive_row_entry_output_lookupvalue ge_balance_negative_row_entry_output_lookupvalue. (((((v) = 2 * (ge_balance_positive_row_entry_output_lookupvalue) /\ (ge_balance_negative_row_entry_output_lookupvalue) = 0) \/ exists ge_signed_half_row_entry_output_lookupvaluedecode. (((v) = 2 * ge_signed_half_row_entry_output_lookupvaluedecode + 1 /\ (ge_balance_positive_row_entry_output_lookupvalue) = 0) /\ (ge_balance_negative_row_entry_output_lookupvalue) = S ge_signed_half_row_entry_output_lookupvaluedecode))) /\ ((dst_positive_row_entry_output_lookup) + ge_balance_negative_row_entry_output_lookupvalue = (dst_negative_row_entry_output_lookup) + ge_balance_positive_row_entry_output_lookupvalue))))))))) /\ (((~((x)=0)) /\ (exists dc_mask_row_entry_output_conv. ((((exists dst_positive_code_row_entry_output_convmasktable dst_positive_scale_row_entry_output_convmasktable dst_negative_code_row_entry_output_convmasktable dst_negative_scale_row_entry_output_convmasktable. (((dc_mask_row_entry_output_conv) = (((((dst_positive_code_row_entry_output_convmasktable) + (dst_positive_scale_row_entry_output_convmasktable)) * S ((dst_positive_code_row_entry_output_convmasktable) + (dst_positive_scale_row_entry_output_convmasktable)) + ((dst_positive_scale_row_entry_output_convmasktable) + (dst_positive_scale_row_entry_output_convmasktable))) + (((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) * S ((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) + ((dst_negative_scale_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)))) * S ((((dst_positive_code_row_entry_output_convmasktable) + (dst_positive_scale_row_entry_output_convmasktable)) * S ((dst_positive_code_row_entry_output_convmasktable) + (dst_positive_scale_row_entry_output_convmasktable)) + ((dst_positive_scale_row_entry_output_convmasktable) + (dst_positive_scale_row_entry_output_convmasktable))) + (((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) * S ((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) + ((dst_negative_scale_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)))) + ((((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) * S ((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) + ((dst_negative_scale_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable))) + (((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) * S ((dst_negative_code_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)) + ((dst_negative_scale_row_entry_output_convmasktable) + (dst_negative_scale_row_entry_output_convmasktable)))))) /\ (forall dst_index_row_entry_output_convmasktable. (exists pvs_le_gap_row_entry_output_convmasktabledomain. pvs_le_gap_row_entry_output_convmasktabledomain + (dst_index_row_entry_output_convmasktable) = (x)) -> exists dst_positive_row_entry_output_convmasktable dst_negative_row_entry_output_convmasktable dst_value_row_entry_output_convmasktable. ((((exists ff_h_pvs_row_entry_output_convmasktableentrypositive. ff_h_pvs_row_entry_output_convmasktableentrypositive + S (dst_positive_row_entry_output_convmasktable) = S ((S (dst_index_row_entry_output_convmasktable)) * dst_positive_scale_row_entry_output_convmasktable)) /\ exists ff_q_pvs_row_entry_output_convmasktableentrypositive. dst_positive_code_row_entry_output_convmasktable = ff_q_pvs_row_entry_output_convmasktableentrypositive * S ((S (dst_index_row_entry_output_convmasktable)) * dst_positive_scale_row_entry_output_convmasktable) + (dst_positive_row_entry_output_convmasktable))) /\ (((((exists ff_h_pvs_row_entry_output_convmasktableentrynegative. ff_h_pvs_row_entry_output_convmasktableentrynegative + S (dst_negative_row_entry_output_convmasktable) = S ((S (dst_index_row_entry_output_convmasktable)) * dst_negative_scale_row_entry_output_convmasktable)) /\ exists ff_q_pvs_row_entry_output_convmasktableentrynegative. dst_negative_code_row_entry_output_convmasktable = ff_q_pvs_row_entry_output_convmasktableentrynegative * S ((S (dst_index_row_entry_output_convmasktable)) * dst_negative_scale_row_entry_output_convmasktable) + (dst_negative_row_entry_output_convmasktable))) /\ (exists ge_balance_positive_row_entry_output_convmasktableentryvalue ge_balance_negative_row_entry_output_convmasktableentryvalue. (((((dst_value_row_entry_output_convmasktable) = 2 * (ge_balance_positive_row_entry_output_convmasktableentryvalue) /\ (ge_balance_negative_row_entry_output_convmasktableentryvalue) = 0) \/ exists ge_signed_half_row_entry_output_convmasktableentryvaluedecode. (((dst_value_row_entry_output_convmasktable) = 2 * ge_signed_half_row_entry_output_convmasktableentryvaluedecode + 1 /\ (ge_balance_positive_row_entry_output_convmasktableentryvalue) = 0) /\ (ge_balance_negative_row_entry_output_convmasktableentryvalue) = S ge_signed_half_row_entry_output_convmasktableentryvaluedecode))) /\ ((dst_positive_row_entry_output_convmasktable) + ge_balance_negative_row_entry_output_convmasktableentryvalue = (dst_negative_row_entry_output_convmasktable) + ge_balance_positive_row_entry_output_convmasktableentryvalue))))))))) /\ (forall dc_index_row_entry_output_convmask dc_value_row_entry_output_convmask. (exists pvs_le_gap_row_entry_output_convmaskdomain. pvs_le_gap_row_entry_output_convmaskdomain + (dc_index_row_entry_output_convmask) = (x)) -> (exists dst_positive_code_row_entry_output_convmasklookup dst_positive_scale_row_entry_output_convmasklookup dst_negative_code_row_entry_output_convmasklookup dst_negative_scale_row_entry_output_convmasklookup dst_positive_row_entry_output_convmasklookup dst_negative_row_entry_output_convmasklookup. (((dc_mask_row_entry_output_conv) = (((((dst_positive_code_row_entry_output_convmasklookup) + (dst_positive_scale_row_entry_output_convmasklookup)) * S ((dst_positive_code_row_entry_output_convmasklookup) + (dst_positive_scale_row_entry_output_convmasklookup)) + ((dst_positive_scale_row_entry_output_convmasklookup) + (dst_positive_scale_row_entry_output_convmasklookup))) + (((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) * S ((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) + ((dst_negative_scale_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)))) * S ((((dst_positive_code_row_entry_output_convmasklookup) + (dst_positive_scale_row_entry_output_convmasklookup)) * S ((dst_positive_code_row_entry_output_convmasklookup) + (dst_positive_scale_row_entry_output_convmasklookup)) + ((dst_positive_scale_row_entry_output_convmasklookup) + (dst_positive_scale_row_entry_output_convmasklookup))) + (((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) * S ((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) + ((dst_negative_scale_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)))) + ((((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) * S ((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) + ((dst_negative_scale_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup))) + (((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) * S ((dst_negative_code_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)) + ((dst_negative_scale_row_entry_output_convmasklookup) + (dst_negative_scale_row_entry_output_convmasklookup)))))) /\ (((((exists ff_h_pvs_row_entry_output_convmasklookuppositive. ff_h_pvs_row_entry_output_convmasklookuppositive + S (dst_positive_row_entry_output_convmasklookup) = S ((S (dc_index_row_entry_output_convmask)) * dst_positive_scale_row_entry_output_convmasklookup)) /\ exists ff_q_pvs_row_entry_output_convmasklookuppositive. dst_positive_code_row_entry_output_convmasklookup = ff_q_pvs_row_entry_output_convmasklookuppositive * S ((S (dc_index_row_entry_output_convmask)) * dst_positive_scale_row_entry_output_convmasklookup) + (dst_positive_row_entry_output_convmasklookup))) /\ (((((exists ff_h_pvs_row_entry_output_convmasklookupnegative. ff_h_pvs_row_entry_output_convmasklookupnegative + S (dst_negative_row_entry_output_convmasklookup) = S ((S (dc_index_row_entry_output_convmask)) * dst_negative_scale_row_entry_output_convmasklookup)) /\ exists ff_q_pvs_row_entry_output_convmasklookupnegative. dst_negative_code_row_entry_output_convmasklookup = ff_q_pvs_row_entry_output_convmasklookupnegative * S ((S (dc_index_row_entry_output_convmask)) * dst_negative_scale_row_entry_output_convmasklookup) + (dst_negative_row_entry_output_convmasklookup))) /\ (exists ge_balance_positive_row_entry_output_convmasklookupvalue ge_balance_negative_row_entry_output_convmasklookupvalue. (((((dc_value_row_entry_output_convmask) = 2 * (ge_balance_positive_row_entry_output_convmasklookupvalue) /\ (ge_balance_negative_row_entry_output_convmasklookupvalue) = 0) \/ exists ge_signed_half_row_entry_output_convmasklookupvaluedecode. (((dc_value_row_entry_output_convmask) = 2 * ge_signed_half_row_entry_output_convmasklookupvaluedecode + 1 /\ (ge_balance_positive_row_entry_output_convmasklookupvalue) = 0) /\ (ge_balance_negative_row_entry_output_convmasklookupvalue) = S ge_signed_half_row_entry_output_convmasklookupvaluedecode))) /\ ((dst_positive_row_entry_output_convmasklookup) + ge_balance_negative_row_entry_output_convmasklookupvalue = (dst_negative_row_entry_output_convmasklookup) + ge_balance_positive_row_entry_output_convmasklookupvalue))))))))) -> ((((~((dc_index_row_entry_output_convmask)=0)) /\ (exists dc_quotient_row_entry_output_convmaskentry dc_left_row_entry_output_convmaskentry dc_right_row_entry_output_convmaskentry. (((x)=(dc_index_row_entry_output_convmask)*dc_quotient_row_entry_output_convmaskentry) /\ (((exists dst_positive_code_row_entry_output_convmaskentryleft dst_positive_scale_row_entry_output_convmaskentryleft dst_negative_code_row_entry_output_convmaskentryleft dst_negative_scale_row_entry_output_convmaskentryleft dst_positive_row_entry_output_convmaskentryleft dst_negative_row_entry_output_convmaskentryleft. (((H) = (((((dst_positive_code_row_entry_output_convmaskentryleft) + (dst_positive_scale_row_entry_output_convmaskentryleft)) * S ((dst_positive_code_row_entry_output_convmaskentryleft) + (dst_positive_scale_row_entry_output_convmaskentryleft)) + ((dst_positive_scale_row_entry_output_convmaskentryleft) + (dst_positive_scale_row_entry_output_convmaskentryleft))) + (((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) * S ((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) + ((dst_negative_scale_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)))) * S ((((dst_positive_code_row_entry_output_convmaskentryleft) + (dst_positive_scale_row_entry_output_convmaskentryleft)) * S ((dst_positive_code_row_entry_output_convmaskentryleft) + (dst_positive_scale_row_entry_output_convmaskentryleft)) + ((dst_positive_scale_row_entry_output_convmaskentryleft) + (dst_positive_scale_row_entry_output_convmaskentryleft))) + (((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) * S ((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) + ((dst_negative_scale_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)))) + ((((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) * S ((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) + ((dst_negative_scale_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft))) + (((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) * S ((dst_negative_code_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)) + ((dst_negative_scale_row_entry_output_convmaskentryleft) + (dst_negative_scale_row_entry_output_convmaskentryleft)))))) /\ (((((exists ff_h_pvs_row_entry_output_convmaskentryleftpositive. ff_h_pvs_row_entry_output_convmaskentryleftpositive + S (dst_positive_row_entry_output_convmaskentryleft) = S ((S (dc_index_row_entry_output_convmask)) * dst_positive_scale_row_entry_output_convmaskentryleft)) /\ exists ff_q_pvs_row_entry_output_convmaskentryleftpositive. dst_positive_code_row_entry_output_convmaskentryleft = ff_q_pvs_row_entry_output_convmaskentryleftpositive * S ((S (dc_index_row_entry_output_convmask)) * dst_positive_scale_row_entry_output_convmaskentryleft) + (dst_positive_row_entry_output_convmaskentryleft))) /\ (((((exists ff_h_pvs_row_entry_output_convmaskentryleftnegative. ff_h_pvs_row_entry_output_convmaskentryleftnegative + S (dst_negative_row_entry_output_convmaskentryleft) = S ((S (dc_index_row_entry_output_convmask)) * dst_negative_scale_row_entry_output_convmaskentryleft)) /\ exists ff_q_pvs_row_entry_output_convmaskentryleftnegative. dst_negative_code_row_entry_output_convmaskentryleft = ff_q_pvs_row_entry_output_convmaskentryleftnegative * S ((S (dc_index_row_entry_output_convmask)) * dst_negative_scale_row_entry_output_convmaskentryleft) + (dst_negative_row_entry_output_convmaskentryleft))) /\ (exists ge_balance_positive_row_entry_output_convmaskentryleftvalue ge_balance_negative_row_entry_output_convmaskentryleftvalue. (((((dc_left_row_entry_output_convmaskentry) = 2 * (ge_balance_positive_row_entry_output_convmaskentryleftvalue) /\ (ge_balance_negative_row_entry_output_convmaskentryleftvalue) = 0) \/ exists ge_signed_half_row_entry_output_convmaskentryleftvaluedecode. (((dc_left_row_entry_output_convmaskentry) = 2 * ge_signed_half_row_entry_output_convmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_row_entry_output_convmaskentryleftvalue) = 0) /\ (ge_balance_negative_row_entry_output_convmaskentryleftvalue) = S ge_signed_half_row_entry_output_convmaskentryleftvaluedecode))) /\ ((dst_positive_row_entry_output_convmaskentryleft) + ge_balance_negative_row_entry_output_convmaskentryleftvalue = (dst_negative_row_entry_output_convmaskentryleft) + ge_balance_positive_row_entry_output_convmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_row_entry_output_convmaskentryright dst_positive_scale_row_entry_output_convmaskentryright dst_negative_code_row_entry_output_convmaskentryright dst_negative_scale_row_entry_output_convmaskentryright dst_positive_row_entry_output_convmaskentryright dst_negative_row_entry_output_convmaskentryright. (((G) = (((((dst_positive_code_row_entry_output_convmaskentryright) + (dst_positive_scale_row_entry_output_convmaskentryright)) * S ((dst_positive_code_row_entry_output_convmaskentryright) + (dst_positive_scale_row_entry_output_convmaskentryright)) + ((dst_positive_scale_row_entry_output_convmaskentryright) + (dst_positive_scale_row_entry_output_convmaskentryright))) + (((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) * S ((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) + ((dst_negative_scale_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)))) * S ((((dst_positive_code_row_entry_output_convmaskentryright) + (dst_positive_scale_row_entry_output_convmaskentryright)) * S ((dst_positive_code_row_entry_output_convmaskentryright) + (dst_positive_scale_row_entry_output_convmaskentryright)) + ((dst_positive_scale_row_entry_output_convmaskentryright) + (dst_positive_scale_row_entry_output_convmaskentryright))) + (((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) * S ((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) + ((dst_negative_scale_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)))) + ((((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) * S ((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) + ((dst_negative_scale_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright))) + (((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) * S ((dst_negative_code_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)) + ((dst_negative_scale_row_entry_output_convmaskentryright) + (dst_negative_scale_row_entry_output_convmaskentryright)))))) /\ (((((exists ff_h_pvs_row_entry_output_convmaskentryrightpositive. ff_h_pvs_row_entry_output_convmaskentryrightpositive + S (dst_positive_row_entry_output_convmaskentryright) = S ((S (dc_quotient_row_entry_output_convmaskentry)) * dst_positive_scale_row_entry_output_convmaskentryright)) /\ exists ff_q_pvs_row_entry_output_convmaskentryrightpositive. dst_positive_code_row_entry_output_convmaskentryright = ff_q_pvs_row_entry_output_convmaskentryrightpositive * S ((S (dc_quotient_row_entry_output_convmaskentry)) * dst_positive_scale_row_entry_output_convmaskentryright) + (dst_positive_row_entry_output_convmaskentryright))) /\ (((((exists ff_h_pvs_row_entry_output_convmaskentryrightnegative. ff_h_pvs_row_entry_output_convmaskentryrightnegative + S (dst_negative_row_entry_output_convmaskentryright) = S ((S (dc_quotient_row_entry_output_convmaskentry)) * dst_negative_scale_row_entry_output_convmaskentryright)) /\ exists ff_q_pvs_row_entry_output_convmaskentryrightnegative. dst_negative_code_row_entry_output_convmaskentryright = ff_q_pvs_row_entry_output_convmaskentryrightnegative * S ((S (dc_quotient_row_entry_output_convmaskentry)) * dst_negative_scale_row_entry_output_convmaskentryright) + (dst_negative_row_entry_output_convmaskentryright))) /\ (exists ge_balance_positive_row_entry_output_convmaskentryrightvalue ge_balance_negative_row_entry_output_convmaskentryrightvalue. (((((dc_right_row_entry_output_convmaskentry) = 2 * (ge_balance_positive_row_entry_output_convmaskentryrightvalue) /\ (ge_balance_negative_row_entry_output_convmaskentryrightvalue) = 0) \/ exists ge_signed_half_row_entry_output_convmaskentryrightvaluedecode. (((dc_right_row_entry_output_convmaskentry) = 2 * ge_signed_half_row_entry_output_convmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_row_entry_output_convmaskentryrightvalue) = 0) /\ (ge_balance_negative_row_entry_output_convmaskentryrightvalue) = S ge_signed_half_row_entry_output_convmaskentryrightvaluedecode))) /\ ((dst_positive_row_entry_output_convmaskentryright) + ge_balance_negative_row_entry_output_convmaskentryrightvalue = (dst_negative_row_entry_output_convmaskentryright) + ge_balance_positive_row_entry_output_convmaskentryrightvalue))))))))) /\ (exists sto_ap_row_entry_output_convmaskentryproduct sto_an_row_entry_output_convmaskentryproduct sto_bp_row_entry_output_convmaskentryproduct sto_bn_row_entry_output_convmaskentryproduct sto_cp_row_entry_output_convmaskentryproduct sto_cn_row_entry_output_convmaskentryproduct. (((((dc_left_row_entry_output_convmaskentry) = 2 * (sto_ap_row_entry_output_convmaskentryproduct) /\ (sto_an_row_entry_output_convmaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_output_convmaskentryproductleft. (((dc_left_row_entry_output_convmaskentry) = 2 * ge_signed_half_row_entry_output_convmaskentryproductleft + 1 /\ (sto_ap_row_entry_output_convmaskentryproduct) = 0) /\ (sto_an_row_entry_output_convmaskentryproduct) = S ge_signed_half_row_entry_output_convmaskentryproductleft))) /\ ((((((dc_right_row_entry_output_convmaskentry) = 2 * (sto_bp_row_entry_output_convmaskentryproduct) /\ (sto_bn_row_entry_output_convmaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_output_convmaskentryproductright. (((dc_right_row_entry_output_convmaskentry) = 2 * ge_signed_half_row_entry_output_convmaskentryproductright + 1 /\ (sto_bp_row_entry_output_convmaskentryproduct) = 0) /\ (sto_bn_row_entry_output_convmaskentryproduct) = S ge_signed_half_row_entry_output_convmaskentryproductright))) /\ ((((((dc_value_row_entry_output_convmask) = 2 * (sto_cp_row_entry_output_convmaskentryproduct) /\ (sto_cn_row_entry_output_convmaskentryproduct) = 0) \/ exists ge_signed_half_row_entry_output_convmaskentryproductoutput. (((dc_value_row_entry_output_convmask) = 2 * ge_signed_half_row_entry_output_convmaskentryproductoutput + 1 /\ (sto_cp_row_entry_output_convmaskentryproduct) = 0) /\ (sto_cn_row_entry_output_convmaskentryproduct) = S ge_signed_half_row_entry_output_convmaskentryproductoutput))) /\ ((sto_ap_row_entry_output_convmaskentryproduct * sto_bp_row_entry_output_convmaskentryproduct + sto_an_row_entry_output_convmaskentryproduct * sto_bn_row_entry_output_convmaskentryproduct) + sto_cn_row_entry_output_convmaskentryproduct = (sto_ap_row_entry_output_convmaskentryproduct * sto_bn_row_entry_output_convmaskentryproduct + sto_an_row_entry_output_convmaskentryproduct * sto_bp_row_entry_output_convmaskentryproduct) + sto_cp_row_entry_output_convmaskentryproduct))))))))))))))) \/ ((((dc_index_row_entry_output_convmask)=0 \/ ~(exists pvs_factor_row_entry_output_convmaskentrynondivisor. (x) = (dc_index_row_entry_output_convmask) * pvs_factor_row_entry_output_convmaskentrynondivisor)) /\ ((dc_value_row_entry_output_convmask)=0))))))) /\ (exists dst_positive_code_row_entry_output_convfold dst_positive_scale_row_entry_output_convfold dst_negative_code_row_entry_output_convfold dst_negative_scale_row_entry_output_convfold dst_positive_sum_row_entry_output_convfold dst_negative_sum_row_entry_output_convfold. (((dc_mask_row_entry_output_conv) = (((((dst_positive_code_row_entry_output_convfold) + (dst_positive_scale_row_entry_output_convfold)) * S ((dst_positive_code_row_entry_output_convfold) + (dst_positive_scale_row_entry_output_convfold)) + ((dst_positive_scale_row_entry_output_convfold) + (dst_positive_scale_row_entry_output_convfold))) + (((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) * S ((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) + ((dst_negative_scale_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)))) * S ((((dst_positive_code_row_entry_output_convfold) + (dst_positive_scale_row_entry_output_convfold)) * S ((dst_positive_code_row_entry_output_convfold) + (dst_positive_scale_row_entry_output_convfold)) + ((dst_positive_scale_row_entry_output_convfold) + (dst_positive_scale_row_entry_output_convfold))) + (((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) * S ((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) + ((dst_negative_scale_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)))) + ((((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) * S ((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) + ((dst_negative_scale_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold))) + (((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) * S ((dst_negative_code_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)) + ((dst_negative_scale_row_entry_output_convfold) + (dst_negative_scale_row_entry_output_convfold)))))) /\ (((exists fs_u_dst_row_entry_output_convfoldpositive fs_v_dst_row_entry_output_convfoldpositive. ((((exists fs_h_dst_row_entry_output_convfoldpositive_body_start. fs_h_dst_row_entry_output_convfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_output_convfoldpositive)) /\ exists fs_q_dst_row_entry_output_convfoldpositive_body_start. fs_u_dst_row_entry_output_convfoldpositive = fs_q_dst_row_entry_output_convfoldpositive_body_start * S ((S (0)) * fs_v_dst_row_entry_output_convfoldpositive) + (0))) /\ ((((exists fs_h_dst_row_entry_output_convfoldpositive_body_terminal. fs_h_dst_row_entry_output_convfoldpositive_body_terminal + S (dst_positive_sum_row_entry_output_convfold) = S ((S (S (x))) * fs_v_dst_row_entry_output_convfoldpositive)) /\ exists fs_q_dst_row_entry_output_convfoldpositive_body_terminal. fs_u_dst_row_entry_output_convfoldpositive = fs_q_dst_row_entry_output_convfoldpositive_body_terminal * S ((S (S (x))) * fs_v_dst_row_entry_output_convfoldpositive) + (dst_positive_sum_row_entry_output_convfold))) /\ forall fs_i_dst_row_entry_output_convfoldpositive_body_steps. (exists fs_lt_dst_row_entry_output_convfoldpositive_body_steps_bound. fs_lt_dst_row_entry_output_convfoldpositive_body_steps_bound + S fs_i_dst_row_entry_output_convfoldpositive_body_steps = S (x)) -> exists fs_a_dst_row_entry_output_convfoldpositive_body_steps fs_r_dst_row_entry_output_convfoldpositive_body_steps fs_s_dst_row_entry_output_convfoldpositive_body_steps. ((((exists fs_h_dst_row_entry_output_convfoldpositive_body_steps_summand. fs_h_dst_row_entry_output_convfoldpositive_body_steps_summand + S (fs_a_dst_row_entry_output_convfoldpositive_body_steps) = S ((S (fs_i_dst_row_entry_output_convfoldpositive_body_steps)) * dst_positive_scale_row_entry_output_convfold)) /\ exists fs_q_dst_row_entry_output_convfoldpositive_body_steps_summand. dst_positive_code_row_entry_output_convfold = fs_q_dst_row_entry_output_convfoldpositive_body_steps_summand * S ((S (fs_i_dst_row_entry_output_convfoldpositive_body_steps)) * dst_positive_scale_row_entry_output_convfold) + (fs_a_dst_row_entry_output_convfoldpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_output_convfoldpositive_body_steps_partial. fs_h_dst_row_entry_output_convfoldpositive_body_steps_partial + S (fs_r_dst_row_entry_output_convfoldpositive_body_steps) = S ((S (fs_i_dst_row_entry_output_convfoldpositive_body_steps)) * fs_v_dst_row_entry_output_convfoldpositive)) /\ exists fs_q_dst_row_entry_output_convfoldpositive_body_steps_partial. fs_u_dst_row_entry_output_convfoldpositive = fs_q_dst_row_entry_output_convfoldpositive_body_steps_partial * S ((S (fs_i_dst_row_entry_output_convfoldpositive_body_steps)) * fs_v_dst_row_entry_output_convfoldpositive) + (fs_r_dst_row_entry_output_convfoldpositive_body_steps))) /\ ((((exists fs_h_dst_row_entry_output_convfoldpositive_body_steps_successor. fs_h_dst_row_entry_output_convfoldpositive_body_steps_successor + S (fs_s_dst_row_entry_output_convfoldpositive_body_steps) = S ((S (S fs_i_dst_row_entry_output_convfoldpositive_body_steps)) * fs_v_dst_row_entry_output_convfoldpositive)) /\ exists fs_q_dst_row_entry_output_convfoldpositive_body_steps_successor. fs_u_dst_row_entry_output_convfoldpositive = fs_q_dst_row_entry_output_convfoldpositive_body_steps_successor * S ((S (S fs_i_dst_row_entry_output_convfoldpositive_body_steps)) * fs_v_dst_row_entry_output_convfoldpositive) + (fs_s_dst_row_entry_output_convfoldpositive_body_steps))) /\ fs_s_dst_row_entry_output_convfoldpositive_body_steps = fs_r_dst_row_entry_output_convfoldpositive_body_steps + fs_a_dst_row_entry_output_convfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_row_entry_output_convfoldnegative fs_v_dst_row_entry_output_convfoldnegative. ((((exists fs_h_dst_row_entry_output_convfoldnegative_body_start. fs_h_dst_row_entry_output_convfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_entry_output_convfoldnegative)) /\ exists fs_q_dst_row_entry_output_convfoldnegative_body_start. fs_u_dst_row_entry_output_convfoldnegative = fs_q_dst_row_entry_output_convfoldnegative_body_start * S ((S (0)) * fs_v_dst_row_entry_output_convfoldnegative) + (0))) /\ ((((exists fs_h_dst_row_entry_output_convfoldnegative_body_terminal. fs_h_dst_row_entry_output_convfoldnegative_body_terminal + S (dst_negative_sum_row_entry_output_convfold) = S ((S (S (x))) * fs_v_dst_row_entry_output_convfoldnegative)) /\ exists fs_q_dst_row_entry_output_convfoldnegative_body_terminal. fs_u_dst_row_entry_output_convfoldnegative = fs_q_dst_row_entry_output_convfoldnegative_body_terminal * S ((S (S (x))) * fs_v_dst_row_entry_output_convfoldnegative) + (dst_negative_sum_row_entry_output_convfold))) /\ forall fs_i_dst_row_entry_output_convfoldnegative_body_steps. (exists fs_lt_dst_row_entry_output_convfoldnegative_body_steps_bound. fs_lt_dst_row_entry_output_convfoldnegative_body_steps_bound + S fs_i_dst_row_entry_output_convfoldnegative_body_steps = S (x)) -> exists fs_a_dst_row_entry_output_convfoldnegative_body_steps fs_r_dst_row_entry_output_convfoldnegative_body_steps fs_s_dst_row_entry_output_convfoldnegative_body_steps. ((((exists fs_h_dst_row_entry_output_convfoldnegative_body_steps_summand. fs_h_dst_row_entry_output_convfoldnegative_body_steps_summand + S (fs_a_dst_row_entry_output_convfoldnegative_body_steps) = S ((S (fs_i_dst_row_entry_output_convfoldnegative_body_steps)) * dst_negative_scale_row_entry_output_convfold)) /\ exists fs_q_dst_row_entry_output_convfoldnegative_body_steps_summand. dst_negative_code_row_entry_output_convfold = fs_q_dst_row_entry_output_convfoldnegative_body_steps_summand * S ((S (fs_i_dst_row_entry_output_convfoldnegative_body_steps)) * dst_negative_scale_row_entry_output_convfold) + (fs_a_dst_row_entry_output_convfoldnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_output_convfoldnegative_body_steps_partial. fs_h_dst_row_entry_output_convfoldnegative_body_steps_partial + S (fs_r_dst_row_entry_output_convfoldnegative_body_steps) = S ((S (fs_i_dst_row_entry_output_convfoldnegative_body_steps)) * fs_v_dst_row_entry_output_convfoldnegative)) /\ exists fs_q_dst_row_entry_output_convfoldnegative_body_steps_partial. fs_u_dst_row_entry_output_convfoldnegative = fs_q_dst_row_entry_output_convfoldnegative_body_steps_partial * S ((S (fs_i_dst_row_entry_output_convfoldnegative_body_steps)) * fs_v_dst_row_entry_output_convfoldnegative) + (fs_r_dst_row_entry_output_convfoldnegative_body_steps))) /\ ((((exists fs_h_dst_row_entry_output_convfoldnegative_body_steps_successor. fs_h_dst_row_entry_output_convfoldnegative_body_steps_successor + S (fs_s_dst_row_entry_output_convfoldnegative_body_steps) = S ((S (S fs_i_dst_row_entry_output_convfoldnegative_body_steps)) * fs_v_dst_row_entry_output_convfoldnegative)) /\ exists fs_q_dst_row_entry_output_convfoldnegative_body_steps_successor. fs_u_dst_row_entry_output_convfoldnegative = fs_q_dst_row_entry_output_convfoldnegative_body_steps_successor * S ((S (S fs_i_dst_row_entry_output_convfoldnegative_body_steps)) * fs_v_dst_row_entry_output_convfoldnegative) + (fs_s_dst_row_entry_output_convfoldnegative_body_steps))) /\ fs_s_dst_row_entry_output_convfoldnegative_body_steps = fs_r_dst_row_entry_output_convfoldnegative_body_steps + fs_a_dst_row_entry_output_convfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_row_entry_output_convfoldresult ge_balance_negative_row_entry_output_convfoldresult. (((((v) = 2 * (ge_balance_positive_row_entry_output_convfoldresult) /\ (ge_balance_negative_row_entry_output_convfoldresult) = 0) \/ exists ge_signed_half_row_entry_output_convfoldresultdecode. (((v) = 2 * ge_signed_half_row_entry_output_convfoldresultdecode + 1 /\ (ge_balance_positive_row_entry_output_convfoldresult) = 0) /\ (ge_balance_negative_row_entry_output_convfoldresult) = S ge_signed_half_row_entry_output_convfoldresultdecode))) /\ ((dst_positive_sum_row_entry_output_convfold) + ge_balance_negative_row_entry_output_convfoldresult = (dst_negative_sum_row_entry_output_convfold) + ge_balance_positive_row_entry_output_convfoldresult))))))))))))))) - 0088
specialize dirichlet_convolution_table_lookup (N) - 0089
specialize dirichlet_convolution_table_lookup (H) - 0090
specialize dirichlet_convolution_table_lookup (G) - 0091
specialize dirichlet_convolution_table_lookup (U) - 0092
specialize dirichlet_convolution_table_lookup (x) - 0093
apply dirichlet_convolution_table_lookup - 0094
exact hU - 0095
intro hx0 - 0096
specialize factor_nonzero_right (n) - 0097
specialize factor_nonzero_right (a) - 0098
specialize factor_nonzero_right (x) - 0099
apply factor_nonzero_right - 0100
exact hn - 0101
exact hd_left_witness - 0102
exact hx0 - 0103
specialize le_trans (x) - 0104
specialize le_trans (n) - 0105
specialize le_trans (N) - 0106
apply le_trans - 0107
specialize divisor_le_nonzero (x) - 0108
specialize divisor_le_nonzero (n) - 0109
apply divisor_le_nonzero - 0110
exact hn - 0111
exists a - 0112
trans a*x - 0113
exact hd_left_witness - 0114
apply mul_comm - 0115
exact hnN - 0116
cases ht - 0117
cases ht_witness - 0118
have hvalue : x2=x3 - 0119
specialize dirichlet_convolution_sum_functional (H) - 0120
specialize dirichlet_convolution_sum_functional (G) - 0121
specialize dirichlet_convolution_sum_functional (x) - 0122
specialize dirichlet_convolution_sum_functional (x2) - 0123
specialize dirichlet_convolution_sum_functional (x3) - 0124
apply dirichlet_convolution_sum_functional - 0125
exact hi_witness_left - 0126
exact ht_witness_right - 0127
rewrite hvalue at hi_witness_right - 0128
rewrite hvalue at hi_witness_right - 0129
specialize dirichlet_convolution_entry_from_quotient (F) - 0130
specialize dirichlet_convolution_entry_from_quotient (U) - 0131
specialize dirichlet_convolution_entry_from_quotient (n) - 0132
specialize dirichlet_convolution_entry_from_quotient (a) - 0133
specialize dirichlet_convolution_entry_from_quotient (x) - 0134
specialize dirichlet_convolution_entry_from_quotient (x1) - 0135
specialize dirichlet_convolution_entry_from_quotient (x3) - 0136
specialize dirichlet_convolution_entry_from_quotient (z) - 0137
apply dirichlet_convolution_entry_from_quotient - 0138
exact ha_right - 0139
exact hd_left_witness - 0140
exact hf_witness - 0141
exact ht_witness_left - 0142
exact hi_witness_right - 0143
right - 0144
split - 0145
right - 0146
exact hd_right - 0147
specialize dirichlet_factor_row_zero_sum (F) - 0148
specialize dirichlet_factor_row_zero_sum (G) - 0149
specialize dirichlet_factor_row_zero_sum (H) - 0150
specialize dirichlet_factor_row_zero_sum (n) - 0151
specialize dirichlet_factor_row_zero_sum (a) - 0152
specialize dirichlet_factor_row_zero_sum (V) - 0153
specialize dirichlet_factor_row_zero_sum (z) - 0154
apply dirichlet_factor_row_zero_sum - 0155
exact hr - 0156
right - 0157
exact hd_right - 0158
exact hz