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. (exists di_delta_inverse_necessary_source. ((((exists dst_positive_code_inverse_necessary_sourcedeltatable dst_positive_scale_inverse_necessary_sourcedeltatable dst_negative_code_inverse_necessary_sourcedeltatable dst_negative_scale_inverse_necessary_sourcedeltatable. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) * S ((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) + ((dst_positive_scale_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable))) + (((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)))) * S ((((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) * S ((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) + ((dst_positive_scale_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable))) + (((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)))) + ((((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable))) + (((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)))))) /\ (forall dst_index_inverse_necessary_sourcedeltatable. (exists pvs_le_gap_inverse_necessary_sourcedeltatabledomain. pvs_le_gap_inverse_necessary_sourcedeltatabledomain + (dst_index_inverse_necessary_sourcedeltatable) = (N)) -> exists dst_positive_inverse_necessary_sourcedeltatable dst_negative_inverse_necessary_sourcedeltatable dst_value_inverse_necessary_sourcedeltatable. ((((exists ff_h_pvs_inverse_necessary_sourcedeltatableentrypositive. ff_h_pvs_inverse_necessary_sourcedeltatableentrypositive + S (dst_positive_inverse_necessary_sourcedeltatable) = S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_positive_scale_inverse_necessary_sourcedeltatable)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltatableentrypositive. dst_positive_code_inverse_necessary_sourcedeltatable = ff_q_pvs_inverse_necessary_sourcedeltatableentrypositive * S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_positive_scale_inverse_necessary_sourcedeltatable) + (dst_positive_inverse_necessary_sourcedeltatable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcedeltatableentrynegative. ff_h_pvs_inverse_necessary_sourcedeltatableentrynegative + S (dst_negative_inverse_necessary_sourcedeltatable) = S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_negative_scale_inverse_necessary_sourcedeltatable)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltatableentrynegative. dst_negative_code_inverse_necessary_sourcedeltatable = ff_q_pvs_inverse_necessary_sourcedeltatableentrynegative * S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_inverse_necessary_sourcedeltatable))) /\ (exists ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue. (((((dst_value_inverse_necessary_sourcedeltatable) = 2 * (ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcedeltatableentryvaluedecode. (((dst_value_inverse_necessary_sourcedeltatable) = 2 * ge_signed_half_inverse_necessary_sourcedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue) = S ge_signed_half_inverse_necessary_sourcedeltatableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcedeltatable) + ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue = (dst_negative_inverse_necessary_sourcedeltatable) + ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue))))))))) /\ (forall du_index_inverse_necessary_sourcedelta du_value_inverse_necessary_sourcedelta. ~(du_index_inverse_necessary_sourcedelta=0) -> (exists pvs_le_gap_inverse_necessary_sourcedeltabound. pvs_le_gap_inverse_necessary_sourcedeltabound + (du_index_inverse_necessary_sourcedelta) = (N)) -> (exists dst_positive_code_inverse_necessary_sourcedeltaentry dst_positive_scale_inverse_necessary_sourcedeltaentry dst_negative_code_inverse_necessary_sourcedeltaentry dst_negative_scale_inverse_necessary_sourcedeltaentry dst_positive_inverse_necessary_sourcedeltaentry dst_negative_inverse_necessary_sourcedeltaentry. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) + ((dst_positive_scale_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry))) + (((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)))) * S ((((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) + ((dst_positive_scale_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry))) + (((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)))) + ((((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry))) + (((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcedeltaentrypositive. ff_h_pvs_inverse_necessary_sourcedeltaentrypositive + S (dst_positive_inverse_necessary_sourcedeltaentry) = S ((S (du_index_inverse_necessary_sourcedelta)) * dst_positive_scale_inverse_necessary_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltaentrypositive. dst_positive_code_inverse_necessary_sourcedeltaentry = ff_q_pvs_inverse_necessary_sourcedeltaentrypositive * S ((S (du_index_inverse_necessary_sourcedelta)) * dst_positive_scale_inverse_necessary_sourcedeltaentry) + (dst_positive_inverse_necessary_sourcedeltaentry))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcedeltaentrynegative. ff_h_pvs_inverse_necessary_sourcedeltaentrynegative + S (dst_negative_inverse_necessary_sourcedeltaentry) = S ((S (du_index_inverse_necessary_sourcedelta)) * dst_negative_scale_inverse_necessary_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltaentrynegative. dst_negative_code_inverse_necessary_sourcedeltaentry = ff_q_pvs_inverse_necessary_sourcedeltaentrynegative * S ((S (du_index_inverse_necessary_sourcedelta)) * dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_inverse_necessary_sourcedeltaentry))) /\ (exists ge_balance_positive_inverse_necessary_sourcedeltaentryvalue ge_balance_negative_inverse_necessary_sourcedeltaentryvalue. (((((du_value_inverse_necessary_sourcedelta) = 2 * (ge_balance_positive_inverse_necessary_sourcedeltaentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcedeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcedeltaentryvaluedecode. (((du_value_inverse_necessary_sourcedelta) = 2 * ge_signed_half_inverse_necessary_sourcedeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcedeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcedeltaentryvalue) = S ge_signed_half_inverse_necessary_sourcedeltaentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcedeltaentry) + ge_balance_negative_inverse_necessary_sourcedeltaentryvalue = (dst_negative_inverse_necessary_sourcedeltaentry) + ge_balance_positive_inverse_necessary_sourcedeltaentryvalue))))))))) -> ((((du_index_inverse_necessary_sourcedelta)=1 -> (du_value_inverse_necessary_sourcedelta)=2) /\ (~((du_index_inverse_necessary_sourcedelta)=1) -> (du_value_inverse_necessary_sourcedelta)=0)))))) /\ (((((exists dst_positive_code_inverse_necessary_sourceleftleft dst_positive_scale_inverse_necessary_sourceleftleft dst_negative_code_inverse_necessary_sourceleftleft dst_negative_scale_inverse_necessary_sourceleftleft. (((F) = (((((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) * S ((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) + ((dst_positive_scale_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft))) + (((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)))) * S ((((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) * S ((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) + ((dst_positive_scale_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft))) + (((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)))) + ((((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft))) + (((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)))))) /\ (forall dst_index_inverse_necessary_sourceleftleft. (exists pvs_le_gap_inverse_necessary_sourceleftleftdomain. pvs_le_gap_inverse_necessary_sourceleftleftdomain + (dst_index_inverse_necessary_sourceleftleft) = (N)) -> exists dst_positive_inverse_necessary_sourceleftleft dst_negative_inverse_necessary_sourceleftleft dst_value_inverse_necessary_sourceleftleft. ((((exists ff_h_pvs_inverse_necessary_sourceleftleftentrypositive. ff_h_pvs_inverse_necessary_sourceleftleftentrypositive + S (dst_positive_inverse_necessary_sourceleftleft) = S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_positive_scale_inverse_necessary_sourceleftleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftleftentrypositive. dst_positive_code_inverse_necessary_sourceleftleft = ff_q_pvs_inverse_necessary_sourceleftleftentrypositive * S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_positive_scale_inverse_necessary_sourceleftleft) + (dst_positive_inverse_necessary_sourceleftleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftleftentrynegative. ff_h_pvs_inverse_necessary_sourceleftleftentrynegative + S (dst_negative_inverse_necessary_sourceleftleft) = S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_negative_scale_inverse_necessary_sourceleftleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftleftentrynegative. dst_negative_code_inverse_necessary_sourceleftleft = ff_q_pvs_inverse_necessary_sourceleftleftentrynegative * S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_inverse_necessary_sourceleftleft))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftleftentryvalue ge_balance_negative_inverse_necessary_sourceleftleftentryvalue. (((((dst_value_inverse_necessary_sourceleftleft) = 2 * (ge_balance_positive_inverse_necessary_sourceleftleftentryvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftleftentryvaluedecode. (((dst_value_inverse_necessary_sourceleftleft) = 2 * ge_signed_half_inverse_necessary_sourceleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftleftentryvalue) = S ge_signed_half_inverse_necessary_sourceleftleftentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftleft) + ge_balance_negative_inverse_necessary_sourceleftleftentryvalue = (dst_negative_inverse_necessary_sourceleftleft) + ge_balance_positive_inverse_necessary_sourceleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourceleftright dst_positive_scale_inverse_necessary_sourceleftright dst_negative_code_inverse_necessary_sourceleftright dst_negative_scale_inverse_necessary_sourceleftright. (((G) = (((((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) * S ((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) + ((dst_positive_scale_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright))) + (((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)))) * S ((((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) * S ((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) + ((dst_positive_scale_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright))) + (((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)))) + ((((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright))) + (((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)))))) /\ (forall dst_index_inverse_necessary_sourceleftright. (exists pvs_le_gap_inverse_necessary_sourceleftrightdomain. pvs_le_gap_inverse_necessary_sourceleftrightdomain + (dst_index_inverse_necessary_sourceleftright) = (N)) -> exists dst_positive_inverse_necessary_sourceleftright dst_negative_inverse_necessary_sourceleftright dst_value_inverse_necessary_sourceleftright. ((((exists ff_h_pvs_inverse_necessary_sourceleftrightentrypositive. ff_h_pvs_inverse_necessary_sourceleftrightentrypositive + S (dst_positive_inverse_necessary_sourceleftright) = S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_positive_scale_inverse_necessary_sourceleftright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftrightentrypositive. dst_positive_code_inverse_necessary_sourceleftright = ff_q_pvs_inverse_necessary_sourceleftrightentrypositive * S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_positive_scale_inverse_necessary_sourceleftright) + (dst_positive_inverse_necessary_sourceleftright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftrightentrynegative. ff_h_pvs_inverse_necessary_sourceleftrightentrynegative + S (dst_negative_inverse_necessary_sourceleftright) = S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_negative_scale_inverse_necessary_sourceleftright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftrightentrynegative. dst_negative_code_inverse_necessary_sourceleftright = ff_q_pvs_inverse_necessary_sourceleftrightentrynegative * S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_inverse_necessary_sourceleftright))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftrightentryvalue ge_balance_negative_inverse_necessary_sourceleftrightentryvalue. (((((dst_value_inverse_necessary_sourceleftright) = 2 * (ge_balance_positive_inverse_necessary_sourceleftrightentryvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftrightentryvaluedecode. (((dst_value_inverse_necessary_sourceleftright) = 2 * ge_signed_half_inverse_necessary_sourceleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftrightentryvalue) = S ge_signed_half_inverse_necessary_sourceleftrightentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftright) + ge_balance_negative_inverse_necessary_sourceleftrightentryvalue = (dst_negative_inverse_necessary_sourceleftright) + ge_balance_positive_inverse_necessary_sourceleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcelefttable dst_positive_scale_inverse_necessary_sourcelefttable dst_negative_code_inverse_necessary_sourcelefttable dst_negative_scale_inverse_necessary_sourcelefttable. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) * S ((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) + ((dst_positive_scale_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable))) + (((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)))) * S ((((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) * S ((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) + ((dst_positive_scale_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable))) + (((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)))) + ((((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable))) + (((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)))))) /\ (forall dst_index_inverse_necessary_sourcelefttable. (exists pvs_le_gap_inverse_necessary_sourcelefttabledomain. pvs_le_gap_inverse_necessary_sourcelefttabledomain + (dst_index_inverse_necessary_sourcelefttable) = (N)) -> exists dst_positive_inverse_necessary_sourcelefttable dst_negative_inverse_necessary_sourcelefttable dst_value_inverse_necessary_sourcelefttable. ((((exists ff_h_pvs_inverse_necessary_sourcelefttableentrypositive. ff_h_pvs_inverse_necessary_sourcelefttableentrypositive + S (dst_positive_inverse_necessary_sourcelefttable) = S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_positive_scale_inverse_necessary_sourcelefttable)) /\ exists ff_q_pvs_inverse_necessary_sourcelefttableentrypositive. dst_positive_code_inverse_necessary_sourcelefttable = ff_q_pvs_inverse_necessary_sourcelefttableentrypositive * S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_positive_scale_inverse_necessary_sourcelefttable) + (dst_positive_inverse_necessary_sourcelefttable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcelefttableentrynegative. ff_h_pvs_inverse_necessary_sourcelefttableentrynegative + S (dst_negative_inverse_necessary_sourcelefttable) = S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_negative_scale_inverse_necessary_sourcelefttable)) /\ exists ff_q_pvs_inverse_necessary_sourcelefttableentrynegative. dst_negative_code_inverse_necessary_sourcelefttable = ff_q_pvs_inverse_necessary_sourcelefttableentrynegative * S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_inverse_necessary_sourcelefttable))) /\ (exists ge_balance_positive_inverse_necessary_sourcelefttableentryvalue ge_balance_negative_inverse_necessary_sourcelefttableentryvalue. (((((dst_value_inverse_necessary_sourcelefttable) = 2 * (ge_balance_positive_inverse_necessary_sourcelefttableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcelefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcelefttableentryvaluedecode. (((dst_value_inverse_necessary_sourcelefttable) = 2 * ge_signed_half_inverse_necessary_sourcelefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcelefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcelefttableentryvalue) = S ge_signed_half_inverse_necessary_sourcelefttableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcelefttable) + ge_balance_negative_inverse_necessary_sourcelefttableentryvalue = (dst_negative_inverse_necessary_sourcelefttable) + ge_balance_positive_inverse_necessary_sourcelefttableentryvalue))))))))) /\ (forall dc_input_inverse_necessary_sourceleft dc_output_inverse_necessary_sourceleft. ~(dc_input_inverse_necessary_sourceleft=0) -> (exists pvs_le_gap_inverse_necessary_sourceleftdomain. pvs_le_gap_inverse_necessary_sourceleftdomain + (dc_input_inverse_necessary_sourceleft) = (N)) -> (exists dst_positive_code_inverse_necessary_sourceleftlookup dst_positive_scale_inverse_necessary_sourceleftlookup dst_negative_code_inverse_necessary_sourceleftlookup dst_negative_scale_inverse_necessary_sourceleftlookup dst_positive_inverse_necessary_sourceleftlookup dst_negative_inverse_necessary_sourceleftlookup. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) * S ((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) + ((dst_positive_scale_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup))) + (((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)))) * S ((((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) * S ((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) + ((dst_positive_scale_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup))) + (((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)))) + ((((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup))) + (((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftlookuppositive. ff_h_pvs_inverse_necessary_sourceleftlookuppositive + S (dst_positive_inverse_necessary_sourceleftlookup) = S ((S (dc_input_inverse_necessary_sourceleft)) * dst_positive_scale_inverse_necessary_sourceleftlookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftlookuppositive. dst_positive_code_inverse_necessary_sourceleftlookup = ff_q_pvs_inverse_necessary_sourceleftlookuppositive * S ((S (dc_input_inverse_necessary_sourceleft)) * dst_positive_scale_inverse_necessary_sourceleftlookup) + (dst_positive_inverse_necessary_sourceleftlookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftlookupnegative. ff_h_pvs_inverse_necessary_sourceleftlookupnegative + S (dst_negative_inverse_necessary_sourceleftlookup) = S ((S (dc_input_inverse_necessary_sourceleft)) * dst_negative_scale_inverse_necessary_sourceleftlookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftlookupnegative. dst_negative_code_inverse_necessary_sourceleftlookup = ff_q_pvs_inverse_necessary_sourceleftlookupnegative * S ((S (dc_input_inverse_necessary_sourceleft)) * dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_inverse_necessary_sourceleftlookup))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftlookupvalue ge_balance_negative_inverse_necessary_sourceleftlookupvalue. (((((dc_output_inverse_necessary_sourceleft) = 2 * (ge_balance_positive_inverse_necessary_sourceleftlookupvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftlookupvaluedecode. (((dc_output_inverse_necessary_sourceleft) = 2 * ge_signed_half_inverse_necessary_sourceleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftlookupvalue) = S ge_signed_half_inverse_necessary_sourceleftlookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftlookup) + ge_balance_negative_inverse_necessary_sourceleftlookupvalue = (dst_negative_inverse_necessary_sourceleftlookup) + ge_balance_positive_inverse_necessary_sourceleftlookupvalue))))))))) -> (((~((dc_input_inverse_necessary_sourceleft)=0)) /\ (exists dc_mask_inverse_necessary_sourceleftvalue. ((((exists dst_positive_code_inverse_necessary_sourceleftvaluemasktable dst_positive_scale_inverse_necessary_sourceleftvaluemasktable dst_negative_code_inverse_necessary_sourceleftvaluemasktable dst_negative_scale_inverse_necessary_sourceleftvaluemasktable. (((dc_mask_inverse_necessary_sourceleftvalue) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)))))) /\ (forall dst_index_inverse_necessary_sourceleftvaluemasktable. (exists pvs_le_gap_inverse_necessary_sourceleftvaluemasktabledomain. pvs_le_gap_inverse_necessary_sourceleftvaluemasktabledomain + (dst_index_inverse_necessary_sourceleftvaluemasktable) = (dc_input_inverse_necessary_sourceleft)) -> exists dst_positive_inverse_necessary_sourceleftvaluemasktable dst_negative_inverse_necessary_sourceleftvaluemasktable dst_value_inverse_necessary_sourceleftvaluemasktable. ((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive. ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive + S (dst_positive_inverse_necessary_sourceleftvaluemasktable) = S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive. dst_positive_code_inverse_necessary_sourceleftvaluemasktable = ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive * S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_inverse_necessary_sourceleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative. ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative + S (dst_negative_inverse_necessary_sourceleftvaluemasktable) = S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative. dst_negative_code_inverse_necessary_sourceleftvaluemasktable = ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative * S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_inverse_necessary_sourceleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue. (((((dst_value_inverse_necessary_sourceleftvaluemasktable) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemasktableentryvaluedecode. (((dst_value_inverse_necessary_sourceleftvaluemasktable) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemasktable) + ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue = (dst_negative_inverse_necessary_sourceleftvaluemasktable) + ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_necessary_sourceleftvaluemask dc_value_inverse_necessary_sourceleftvaluemask. (exists pvs_le_gap_inverse_necessary_sourceleftvaluemaskdomain. pvs_le_gap_inverse_necessary_sourceleftvaluemaskdomain + (dc_index_inverse_necessary_sourceleftvaluemask) = (dc_input_inverse_necessary_sourceleft)) -> (exists dst_positive_code_inverse_necessary_sourceleftvaluemasklookup dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup dst_negative_code_inverse_necessary_sourceleftvaluemasklookup dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup dst_positive_inverse_necessary_sourceleftvaluemasklookup dst_negative_inverse_necessary_sourceleftvaluemasklookup. (((dc_mask_inverse_necessary_sourceleftvalue) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasklookuppositive. ff_h_pvs_inverse_necessary_sourceleftvaluemasklookuppositive + S (dst_positive_inverse_necessary_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasklookuppositive. dst_positive_code_inverse_necessary_sourceleftvaluemasklookup = ff_q_pvs_inverse_necessary_sourceleftvaluemasklookuppositive * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_inverse_necessary_sourceleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasklookupnegative. ff_h_pvs_inverse_necessary_sourceleftvaluemasklookupnegative + S (dst_negative_inverse_necessary_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasklookupnegative. dst_negative_code_inverse_necessary_sourceleftvaluemasklookup = ff_q_pvs_inverse_necessary_sourceleftvaluemasklookupnegative * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_inverse_necessary_sourceleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue. (((((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemasklookupvaluedecode. (((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemasklookup) + ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue = (dst_negative_inverse_necessary_sourceleftvaluemasklookup) + ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_necessary_sourceleftvaluemask)=0)) /\ (exists dc_quotient_inverse_necessary_sourceleftvaluemaskentry dc_left_inverse_necessary_sourceleftvaluemaskentry dc_right_inverse_necessary_sourceleftvaluemaskentry. (((dc_input_inverse_necessary_sourceleft)=(dc_index_inverse_necessary_sourceleftvaluemask)*dc_quotient_inverse_necessary_sourceleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft dst_positive_inverse_necessary_sourceleftvaluemaskentryleft dst_negative_inverse_necessary_sourceleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive + S (dst_positive_inverse_necessary_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive. dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_inverse_necessary_sourceleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative + S (dst_negative_inverse_necessary_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative. dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_inverse_necessary_sourceleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue. (((((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemaskentryleft) + ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue = (dst_negative_inverse_necessary_sourceleftvaluemaskentryleft) + ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright dst_positive_inverse_necessary_sourceleftvaluemaskentryright dst_negative_inverse_necessary_sourceleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive + S (dst_positive_inverse_necessary_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive. dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_inverse_necessary_sourceleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative + S (dst_negative_inverse_necessary_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative. dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_inverse_necessary_sourceleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue. (((((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemaskentryright) + ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue = (dst_negative_inverse_necessary_sourceleftvaluemaskentryright) + ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct sto_an_inverse_necessary_sourceleftvaluemaskentryproduct sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct. (((((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * (sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct) /\ (sto_an_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductleft. (((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_necessary_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * (sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct) /\ (sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductright. (((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * (sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct) /\ (sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductoutput. (((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct + sto_an_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct) + sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct = (sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct + sto_an_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct) + sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_necessary_sourceleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_necessary_sourceleftvaluemaskentrynondivisor. (dc_input_inverse_necessary_sourceleft) = (dc_index_inverse_necessary_sourceleftvaluemask) * pvs_factor_inverse_necessary_sourceleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_necessary_sourceleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_necessary_sourceleftvaluefold dst_positive_scale_inverse_necessary_sourceleftvaluefold dst_negative_code_inverse_necessary_sourceleftvaluefold dst_negative_scale_inverse_necessary_sourceleftvaluefold dst_positive_sum_inverse_necessary_sourceleftvaluefold dst_negative_sum_inverse_necessary_sourceleftvaluefold. (((dc_mask_inverse_necessary_sourceleftvalue) = (((((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold))) + (((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold))) + (((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold))) + (((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_necessary_sourceleftvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (dst_positive_sum_inverse_necessary_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps = S (dc_input_inverse_necessary_sourceleft)) -> exists fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_necessary_sourceleftvaluefold = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourceleftvaluefold) + (fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps = fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps + fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_necessary_sourceleftvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (dst_negative_sum_inverse_necessary_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps = S (dc_input_inverse_necessary_sourceleft)) -> exists fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_necessary_sourceleftvaluefold = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps = fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps + fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult. (((((dc_output_inverse_necessary_sourceleft) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluefoldresultdecode. (((dc_output_inverse_necessary_sourceleft) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult) = S ge_signed_half_inverse_necessary_sourceleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_necessary_sourceleftvaluefold) + ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult = (dst_negative_sum_inverse_necessary_sourceleftvaluefold) + ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerightleft dst_positive_scale_inverse_necessary_sourcerightleft dst_negative_code_inverse_necessary_sourcerightleft dst_negative_scale_inverse_necessary_sourcerightleft. (((G) = (((((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) * S ((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) + ((dst_positive_scale_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft))) + (((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)))) * S ((((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) * S ((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) + ((dst_positive_scale_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft))) + (((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)))) + ((((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft))) + (((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)))))) /\ (forall dst_index_inverse_necessary_sourcerightleft. (exists pvs_le_gap_inverse_necessary_sourcerightleftdomain. pvs_le_gap_inverse_necessary_sourcerightleftdomain + (dst_index_inverse_necessary_sourcerightleft) = (N)) -> exists dst_positive_inverse_necessary_sourcerightleft dst_negative_inverse_necessary_sourcerightleft dst_value_inverse_necessary_sourcerightleft. ((((exists ff_h_pvs_inverse_necessary_sourcerightleftentrypositive. ff_h_pvs_inverse_necessary_sourcerightleftentrypositive + S (dst_positive_inverse_necessary_sourcerightleft) = S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_positive_scale_inverse_necessary_sourcerightleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightleftentrypositive. dst_positive_code_inverse_necessary_sourcerightleft = ff_q_pvs_inverse_necessary_sourcerightleftentrypositive * S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_positive_scale_inverse_necessary_sourcerightleft) + (dst_positive_inverse_necessary_sourcerightleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightleftentrynegative. ff_h_pvs_inverse_necessary_sourcerightleftentrynegative + S (dst_negative_inverse_necessary_sourcerightleft) = S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_negative_scale_inverse_necessary_sourcerightleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightleftentrynegative. dst_negative_code_inverse_necessary_sourcerightleft = ff_q_pvs_inverse_necessary_sourcerightleftentrynegative * S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_inverse_necessary_sourcerightleft))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightleftentryvalue ge_balance_negative_inverse_necessary_sourcerightleftentryvalue. (((((dst_value_inverse_necessary_sourcerightleft) = 2 * (ge_balance_positive_inverse_necessary_sourcerightleftentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightleftentryvaluedecode. (((dst_value_inverse_necessary_sourcerightleft) = 2 * ge_signed_half_inverse_necessary_sourcerightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightleftentryvalue) = S ge_signed_half_inverse_necessary_sourcerightleftentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightleft) + ge_balance_negative_inverse_necessary_sourcerightleftentryvalue = (dst_negative_inverse_necessary_sourcerightleft) + ge_balance_positive_inverse_necessary_sourcerightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerightright dst_positive_scale_inverse_necessary_sourcerightright dst_negative_code_inverse_necessary_sourcerightright dst_negative_scale_inverse_necessary_sourcerightright. (((F) = (((((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) * S ((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) + ((dst_positive_scale_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright))) + (((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)))) * S ((((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) * S ((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) + ((dst_positive_scale_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright))) + (((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)))) + ((((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright))) + (((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)))))) /\ (forall dst_index_inverse_necessary_sourcerightright. (exists pvs_le_gap_inverse_necessary_sourcerightrightdomain. pvs_le_gap_inverse_necessary_sourcerightrightdomain + (dst_index_inverse_necessary_sourcerightright) = (N)) -> exists dst_positive_inverse_necessary_sourcerightright dst_negative_inverse_necessary_sourcerightright dst_value_inverse_necessary_sourcerightright. ((((exists ff_h_pvs_inverse_necessary_sourcerightrightentrypositive. ff_h_pvs_inverse_necessary_sourcerightrightentrypositive + S (dst_positive_inverse_necessary_sourcerightright) = S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_positive_scale_inverse_necessary_sourcerightright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightrightentrypositive. dst_positive_code_inverse_necessary_sourcerightright = ff_q_pvs_inverse_necessary_sourcerightrightentrypositive * S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_positive_scale_inverse_necessary_sourcerightright) + (dst_positive_inverse_necessary_sourcerightright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightrightentrynegative. ff_h_pvs_inverse_necessary_sourcerightrightentrynegative + S (dst_negative_inverse_necessary_sourcerightright) = S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_negative_scale_inverse_necessary_sourcerightright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightrightentrynegative. dst_negative_code_inverse_necessary_sourcerightright = ff_q_pvs_inverse_necessary_sourcerightrightentrynegative * S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_inverse_necessary_sourcerightright))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightrightentryvalue ge_balance_negative_inverse_necessary_sourcerightrightentryvalue. (((((dst_value_inverse_necessary_sourcerightright) = 2 * (ge_balance_positive_inverse_necessary_sourcerightrightentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightrightentryvaluedecode. (((dst_value_inverse_necessary_sourcerightright) = 2 * ge_signed_half_inverse_necessary_sourcerightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightrightentryvalue) = S ge_signed_half_inverse_necessary_sourcerightrightentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightright) + ge_balance_negative_inverse_necessary_sourcerightrightentryvalue = (dst_negative_inverse_necessary_sourcerightright) + ge_balance_positive_inverse_necessary_sourcerightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerighttable dst_positive_scale_inverse_necessary_sourcerighttable dst_negative_code_inverse_necessary_sourcerighttable dst_negative_scale_inverse_necessary_sourcerighttable. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) * S ((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) + ((dst_positive_scale_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable))) + (((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)))) * S ((((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) * S ((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) + ((dst_positive_scale_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable))) + (((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)))) + ((((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable))) + (((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)))))) /\ (forall dst_index_inverse_necessary_sourcerighttable. (exists pvs_le_gap_inverse_necessary_sourcerighttabledomain. pvs_le_gap_inverse_necessary_sourcerighttabledomain + (dst_index_inverse_necessary_sourcerighttable) = (N)) -> exists dst_positive_inverse_necessary_sourcerighttable dst_negative_inverse_necessary_sourcerighttable dst_value_inverse_necessary_sourcerighttable. ((((exists ff_h_pvs_inverse_necessary_sourcerighttableentrypositive. ff_h_pvs_inverse_necessary_sourcerighttableentrypositive + S (dst_positive_inverse_necessary_sourcerighttable) = S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_positive_scale_inverse_necessary_sourcerighttable)) /\ exists ff_q_pvs_inverse_necessary_sourcerighttableentrypositive. dst_positive_code_inverse_necessary_sourcerighttable = ff_q_pvs_inverse_necessary_sourcerighttableentrypositive * S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_positive_scale_inverse_necessary_sourcerighttable) + (dst_positive_inverse_necessary_sourcerighttable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerighttableentrynegative. ff_h_pvs_inverse_necessary_sourcerighttableentrynegative + S (dst_negative_inverse_necessary_sourcerighttable) = S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_negative_scale_inverse_necessary_sourcerighttable)) /\ exists ff_q_pvs_inverse_necessary_sourcerighttableentrynegative. dst_negative_code_inverse_necessary_sourcerighttable = ff_q_pvs_inverse_necessary_sourcerighttableentrynegative * S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_inverse_necessary_sourcerighttable))) /\ (exists ge_balance_positive_inverse_necessary_sourcerighttableentryvalue ge_balance_negative_inverse_necessary_sourcerighttableentryvalue. (((((dst_value_inverse_necessary_sourcerighttable) = 2 * (ge_balance_positive_inverse_necessary_sourcerighttableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerighttableentryvaluedecode. (((dst_value_inverse_necessary_sourcerighttable) = 2 * ge_signed_half_inverse_necessary_sourcerighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerighttableentryvalue) = S ge_signed_half_inverse_necessary_sourcerighttableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerighttable) + ge_balance_negative_inverse_necessary_sourcerighttableentryvalue = (dst_negative_inverse_necessary_sourcerighttable) + ge_balance_positive_inverse_necessary_sourcerighttableentryvalue))))))))) /\ (forall dc_input_inverse_necessary_sourceright dc_output_inverse_necessary_sourceright. ~(dc_input_inverse_necessary_sourceright=0) -> (exists pvs_le_gap_inverse_necessary_sourcerightdomain. pvs_le_gap_inverse_necessary_sourcerightdomain + (dc_input_inverse_necessary_sourceright) = (N)) -> (exists dst_positive_code_inverse_necessary_sourcerightlookup dst_positive_scale_inverse_necessary_sourcerightlookup dst_negative_code_inverse_necessary_sourcerightlookup dst_negative_scale_inverse_necessary_sourcerightlookup dst_positive_inverse_necessary_sourcerightlookup dst_negative_inverse_necessary_sourcerightlookup. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) * S ((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) + ((dst_positive_scale_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup))) + (((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)))) * S ((((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) * S ((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) + ((dst_positive_scale_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup))) + (((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)))) + ((((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup))) + (((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightlookuppositive. ff_h_pvs_inverse_necessary_sourcerightlookuppositive + S (dst_positive_inverse_necessary_sourcerightlookup) = S ((S (dc_input_inverse_necessary_sourceright)) * dst_positive_scale_inverse_necessary_sourcerightlookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightlookuppositive. dst_positive_code_inverse_necessary_sourcerightlookup = ff_q_pvs_inverse_necessary_sourcerightlookuppositive * S ((S (dc_input_inverse_necessary_sourceright)) * dst_positive_scale_inverse_necessary_sourcerightlookup) + (dst_positive_inverse_necessary_sourcerightlookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightlookupnegative. ff_h_pvs_inverse_necessary_sourcerightlookupnegative + S (dst_negative_inverse_necessary_sourcerightlookup) = S ((S (dc_input_inverse_necessary_sourceright)) * dst_negative_scale_inverse_necessary_sourcerightlookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightlookupnegative. dst_negative_code_inverse_necessary_sourcerightlookup = ff_q_pvs_inverse_necessary_sourcerightlookupnegative * S ((S (dc_input_inverse_necessary_sourceright)) * dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_inverse_necessary_sourcerightlookup))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightlookupvalue ge_balance_negative_inverse_necessary_sourcerightlookupvalue. (((((dc_output_inverse_necessary_sourceright) = 2 * (ge_balance_positive_inverse_necessary_sourcerightlookupvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightlookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightlookupvaluedecode. (((dc_output_inverse_necessary_sourceright) = 2 * ge_signed_half_inverse_necessary_sourcerightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightlookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightlookupvalue) = S ge_signed_half_inverse_necessary_sourcerightlookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightlookup) + ge_balance_negative_inverse_necessary_sourcerightlookupvalue = (dst_negative_inverse_necessary_sourcerightlookup) + ge_balance_positive_inverse_necessary_sourcerightlookupvalue))))))))) -> (((~((dc_input_inverse_necessary_sourceright)=0)) /\ (exists dc_mask_inverse_necessary_sourcerightvalue. ((((exists dst_positive_code_inverse_necessary_sourcerightvaluemasktable dst_positive_scale_inverse_necessary_sourcerightvaluemasktable dst_negative_code_inverse_necessary_sourcerightvaluemasktable dst_negative_scale_inverse_necessary_sourcerightvaluemasktable. (((dc_mask_inverse_necessary_sourcerightvalue) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)))))) /\ (forall dst_index_inverse_necessary_sourcerightvaluemasktable. (exists pvs_le_gap_inverse_necessary_sourcerightvaluemasktabledomain. pvs_le_gap_inverse_necessary_sourcerightvaluemasktabledomain + (dst_index_inverse_necessary_sourcerightvaluemasktable) = (dc_input_inverse_necessary_sourceright)) -> exists dst_positive_inverse_necessary_sourcerightvaluemasktable dst_negative_inverse_necessary_sourcerightvaluemasktable dst_value_inverse_necessary_sourcerightvaluemasktable. ((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive. ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive + S (dst_positive_inverse_necessary_sourcerightvaluemasktable) = S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive. dst_positive_code_inverse_necessary_sourcerightvaluemasktable = ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive * S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_inverse_necessary_sourcerightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative. ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative + S (dst_negative_inverse_necessary_sourcerightvaluemasktable) = S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative. dst_negative_code_inverse_necessary_sourcerightvaluemasktable = ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative * S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_inverse_necessary_sourcerightvaluemasktable))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue. (((((dst_value_inverse_necessary_sourcerightvaluemasktable) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemasktableentryvaluedecode. (((dst_value_inverse_necessary_sourcerightvaluemasktable) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemasktable) + ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue = (dst_negative_inverse_necessary_sourcerightvaluemasktable) + ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_necessary_sourcerightvaluemask dc_value_inverse_necessary_sourcerightvaluemask. (exists pvs_le_gap_inverse_necessary_sourcerightvaluemaskdomain. pvs_le_gap_inverse_necessary_sourcerightvaluemaskdomain + (dc_index_inverse_necessary_sourcerightvaluemask) = (dc_input_inverse_necessary_sourceright)) -> (exists dst_positive_code_inverse_necessary_sourcerightvaluemasklookup dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup dst_negative_code_inverse_necessary_sourcerightvaluemasklookup dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup dst_positive_inverse_necessary_sourcerightvaluemasklookup dst_negative_inverse_necessary_sourcerightvaluemasklookup. (((dc_mask_inverse_necessary_sourcerightvalue) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasklookuppositive. ff_h_pvs_inverse_necessary_sourcerightvaluemasklookuppositive + S (dst_positive_inverse_necessary_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasklookuppositive. dst_positive_code_inverse_necessary_sourcerightvaluemasklookup = ff_q_pvs_inverse_necessary_sourcerightvaluemasklookuppositive * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_inverse_necessary_sourcerightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasklookupnegative. ff_h_pvs_inverse_necessary_sourcerightvaluemasklookupnegative + S (dst_negative_inverse_necessary_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasklookupnegative. dst_negative_code_inverse_necessary_sourcerightvaluemasklookup = ff_q_pvs_inverse_necessary_sourcerightvaluemasklookupnegative * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_inverse_necessary_sourcerightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue. (((((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemasklookupvaluedecode. (((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemasklookup) + ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue = (dst_negative_inverse_necessary_sourcerightvaluemasklookup) + ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_necessary_sourcerightvaluemask)=0)) /\ (exists dc_quotient_inverse_necessary_sourcerightvaluemaskentry dc_left_inverse_necessary_sourcerightvaluemaskentry dc_right_inverse_necessary_sourcerightvaluemaskentry. (((dc_input_inverse_necessary_sourceright)=(dc_index_inverse_necessary_sourcerightvaluemask)*dc_quotient_inverse_necessary_sourcerightvaluemaskentry) /\ (((exists dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft dst_positive_inverse_necessary_sourcerightvaluemaskentryleft dst_negative_inverse_necessary_sourcerightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive + S (dst_positive_inverse_necessary_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive. dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_inverse_necessary_sourcerightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative + S (dst_negative_inverse_necessary_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative. dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_inverse_necessary_sourcerightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue. (((((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryleftvaluedecode. (((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemaskentryleft) + ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue = (dst_negative_inverse_necessary_sourcerightvaluemaskentryleft) + ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright dst_positive_inverse_necessary_sourcerightvaluemaskentryright dst_negative_inverse_necessary_sourcerightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive + S (dst_positive_inverse_necessary_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive. dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_inverse_necessary_sourcerightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative + S (dst_negative_inverse_necessary_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative. dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_inverse_necessary_sourcerightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue. (((((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryrightvaluedecode. (((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemaskentryright) + ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue = (dst_negative_inverse_necessary_sourcerightvaluemaskentryright) + ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct sto_an_inverse_necessary_sourcerightvaluemaskentryproduct sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct. (((((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * (sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct) /\ (sto_an_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductleft. (((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_necessary_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * (sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct) /\ (sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductright. (((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * (sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct) /\ (sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductoutput. (((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct + sto_an_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct) + sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct = (sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct + sto_an_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct) + sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_necessary_sourcerightvaluemask)=0 \/ ~(exists pvs_factor_inverse_necessary_sourcerightvaluemaskentrynondivisor. (dc_input_inverse_necessary_sourceright) = (dc_index_inverse_necessary_sourcerightvaluemask) * pvs_factor_inverse_necessary_sourcerightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_necessary_sourcerightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_necessary_sourcerightvaluefold dst_positive_scale_inverse_necessary_sourcerightvaluefold dst_negative_code_inverse_necessary_sourcerightvaluefold dst_negative_scale_inverse_necessary_sourcerightvaluefold dst_positive_sum_inverse_necessary_sourcerightvaluefold dst_negative_sum_inverse_necessary_sourcerightvaluefold. (((dc_mask_inverse_necessary_sourcerightvalue) = (((((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold))) + (((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold))) + (((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold))) + (((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)))))) /\ (((exists fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_necessary_sourcerightvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (dst_positive_sum_inverse_necessary_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps = S (dc_input_inverse_necessary_sourceright)) -> exists fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_necessary_sourcerightvaluefold = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourcerightvaluefold) + (fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps = fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps + fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_necessary_sourcerightvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (dst_negative_sum_inverse_necessary_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps = S (dc_input_inverse_necessary_sourceright)) -> exists fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_necessary_sourcerightvaluefold = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps = fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps + fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult. (((((dc_output_inverse_necessary_sourceright) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluefoldresultdecode. (((dc_output_inverse_necessary_sourceright) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult) = S ge_signed_half_inverse_necessary_sourcerightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_necessary_sourcerightvaluefold) + ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult = (dst_negative_sum_inverse_necessary_sourcerightvaluefold) + ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult)))))))))))))))))))))))) -> ~(N=0) -> ((exists dst_positive_code_inverse_necessary_resultpositive dst_positive_scale_inverse_necessary_resultpositive dst_negative_code_inverse_necessary_resultpositive dst_negative_scale_inverse_necessary_resultpositive dst_positive_inverse_necessary_resultpositive dst_negative_inverse_necessary_resultpositive. (((F) = (((((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) * S ((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) + ((dst_positive_scale_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive))) + (((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)))) * S ((((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) * S ((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) + ((dst_positive_scale_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive))) + (((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)))) + ((((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive))) + (((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)))))) /\ (((((exists ff_h_pvs_inverse_necessary_resultpositivepositive. ff_h_pvs_inverse_necessary_resultpositivepositive + S (dst_positive_inverse_necessary_resultpositive) = S ((S (1)) * dst_positive_scale_inverse_necessary_resultpositive)) /\ exists ff_q_pvs_inverse_necessary_resultpositivepositive. dst_positive_code_inverse_necessary_resultpositive = ff_q_pvs_inverse_necessary_resultpositivepositive * S ((S (1)) * dst_positive_scale_inverse_necessary_resultpositive) + (dst_positive_inverse_necessary_resultpositive))) /\ (((((exists ff_h_pvs_inverse_necessary_resultpositivenegative. ff_h_pvs_inverse_necessary_resultpositivenegative + S (dst_negative_inverse_necessary_resultpositive) = S ((S (1)) * dst_negative_scale_inverse_necessary_resultpositive)) /\ exists ff_q_pvs_inverse_necessary_resultpositivenegative. dst_negative_code_inverse_necessary_resultpositive = ff_q_pvs_inverse_necessary_resultpositivenegative * S ((S (1)) * dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_inverse_necessary_resultpositive))) /\ (exists ge_balance_positive_inverse_necessary_resultpositivevalue ge_balance_negative_inverse_necessary_resultpositivevalue. (((((2) = 2 * (ge_balance_positive_inverse_necessary_resultpositivevalue) /\ (ge_balance_negative_inverse_necessary_resultpositivevalue) = 0) \/ exists ge_signed_half_inverse_necessary_resultpositivevaluedecode. (((2) = 2 * ge_signed_half_inverse_necessary_resultpositivevaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_resultpositivevalue) = 0) /\ (ge_balance_negative_inverse_necessary_resultpositivevalue) = S ge_signed_half_inverse_necessary_resultpositivevaluedecode))) /\ ((dst_positive_inverse_necessary_resultpositive) + ge_balance_negative_inverse_necessary_resultpositivevalue = (dst_negative_inverse_necessary_resultpositive) + ge_balance_positive_inverse_necessary_resultpositivevalue))))))))) \/ (exists dst_positive_code_inverse_necessary_resultnegative dst_positive_scale_inverse_necessary_resultnegative dst_negative_code_inverse_necessary_resultnegative dst_negative_scale_inverse_necessary_resultnegative dst_positive_inverse_necessary_resultnegative dst_negative_inverse_necessary_resultnegative. (((F) = (((((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) * S ((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) + ((dst_positive_scale_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative))) + (((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)))) * S ((((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) * S ((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) + ((dst_positive_scale_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative))) + (((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)))) + ((((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative))) + (((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)))))) /\ (((((exists ff_h_pvs_inverse_necessary_resultnegativepositive. ff_h_pvs_inverse_necessary_resultnegativepositive + S (dst_positive_inverse_necessary_resultnegative) = S ((S (1)) * dst_positive_scale_inverse_necessary_resultnegative)) /\ exists ff_q_pvs_inverse_necessary_resultnegativepositive. dst_positive_code_inverse_necessary_resultnegative = ff_q_pvs_inverse_necessary_resultnegativepositive * S ((S (1)) * dst_positive_scale_inverse_necessary_resultnegative) + (dst_positive_inverse_necessary_resultnegative))) /\ (((((exists ff_h_pvs_inverse_necessary_resultnegativenegative. ff_h_pvs_inverse_necessary_resultnegativenegative + S (dst_negative_inverse_necessary_resultnegative) = S ((S (1)) * dst_negative_scale_inverse_necessary_resultnegative)) /\ exists ff_q_pvs_inverse_necessary_resultnegativenegative. dst_negative_code_inverse_necessary_resultnegative = ff_q_pvs_inverse_necessary_resultnegativenegative * S ((S (1)) * dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_inverse_necessary_resultnegative))) /\ (exists ge_balance_positive_inverse_necessary_resultnegativevalue ge_balance_negative_inverse_necessary_resultnegativevalue. (((((1) = 2 * (ge_balance_positive_inverse_necessary_resultnegativevalue) /\ (ge_balance_negative_inverse_necessary_resultnegativevalue) = 0) \/ exists ge_signed_half_inverse_necessary_resultnegativevaluedecode. (((1) = 2 * ge_signed_half_inverse_necessary_resultnegativevaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_resultnegativevalue) = 0) /\ (ge_balance_negative_inverse_necessary_resultnegativevalue) = S ge_signed_half_inverse_necessary_resultnegativevaluedecode))) /\ ((dst_positive_inverse_necessary_resultnegative) + ge_balance_negative_inverse_necessary_resultnegativevalue = (dst_negative_inverse_necessary_resultnegative) + ge_balance_positive_inverse_necessary_resultnegativevalue))))))))))Constructive proof overview
Generated structural guide
At the genuinely in-domain index one, the actual convolution is a signed product equal to one, forcing the original value to be +1 or -1; the nonempty-domain guard is essential.
The unchanged tactic script uses 6 declared prerequisites and contains 87 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
one_le_of_ne_zero Stable theorem; checked-use authorized divisor_signed_table_lookup Alpha theorem; checked-use authorized dirichlet_kronecker_delta_table_one_value Alpha theorem; checked-use authorized dirichlet_convolution_at_one_iff Alpha theorem; checked-use authorized dirichlet_signed_unit_product_classification Alpha theorem; checked-use authorized IV0002 dirichlet_unit_at_one_from_valueDirect 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 (1)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–11
03Establish hboundL12–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.
04Establish haL16–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
05Separate the logical casesL23–23
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L23
cases ha
06Establish hbL24–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
07Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
cases hb
08Establish heL32–38
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
09Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
cases he
10Establish heqL40–49
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table one value.
- L40
have heq : x3=2 - L41
specialize dirichlet_kronecker_delta_table_one_value (N) - L42
specialize dirichlet_kronecker_delta_table_one_value (x) - L43
specialize dirichlet_kronecker_delta_table_one_value (x3) - L44
apply dirichlet_kronecker_delta_table_one_value - L45
exact hi_witness_left - L46
exact hbound - L47
exact he_witness - L48
rewrite heq at he_witness - L49
rewrite heq at he_witness
11Establish hcL50–58
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hi witness right left right right right.
12Establish hiffL59–67
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution at one iff.
- L59
have hiff : (DirichletSum(F,G,1,2) → SignedMul(x1,x2,2)) ∧ (SignedMul(x1,x2,2) → DirichletSum(F,G,1,2))Definitions: SignedMulDirichletSum - L60
specialize dirichlet_convolution_at_one_iff (F) - L61
specialize dirichlet_convolution_at_one_iff (G) - L62
specialize dirichlet_convolution_at_one_iff (x1) - L63
specialize dirichlet_convolution_at_one_iff (x2) - L64
specialize dirichlet_convolution_at_one_iff (2) - L65
apply dirichlet_convolution_at_one_iff - L66
exact ha_witness - L67
exact hb_witness
13Separate the logical casesL68–68
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L68
cases hiff
14Establish hpL69–71
15Establish huL72–80
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet signed unit product classification.
- L72
have hu : (x1=2 /\ x2=2) \/ (x1=1 /\ x2=1) - L73
specialize dirichlet_signed_unit_product_classification (x1) - L74
specialize dirichlet_signed_unit_product_classification (x2) - L75
apply dirichlet_signed_unit_product_classification - L76
exact hp - L77
specialize dirichlet_unit_at_one_from_value (F) - L78
specialize dirichlet_unit_at_one_from_value (x1) - L79
apply dirichlet_unit_at_one_from_value - L80
exact ha_witness
16Separate the logical casesL81–83
17Use earlier factsL84–84
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L84
exact hu_left_left
18Separate the logical casesL85–86
19Use earlier factsL87–87
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L87
exact hu_right_left
Original exact command ledger · 87 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro hi - 0005
intro hn - 0006
cases hi - 0007
cases hi_witness - 0008
cases hi_witness_right - 0009
cases hi_witness_right_left - 0010
cases hi_witness_right_left_right - 0011
cases hi_witness_right_left_right_right - 0012
have hbound : exists pvs_le_gap_necessary_one_bound. pvs_le_gap_necessary_one_bound + (1) = (N) - 0013
specialize one_le_of_ne_zero (N) - 0014
apply one_le_of_ne_zero - 0015
exact hn - 0016
have ha : exists a. (exists dst_positive_code_necessary_lookup_ha dst_positive_scale_necessary_lookup_ha dst_negative_code_necessary_lookup_ha dst_negative_scale_necessary_lookup_ha dst_positive_necessary_lookup_ha dst_negative_necessary_lookup_ha. (((F) = (((((dst_positive_code_necessary_lookup_ha) + (dst_positive_scale_necessary_lookup_ha)) * S ((dst_positive_code_necessary_lookup_ha) + (dst_positive_scale_necessary_lookup_ha)) + ((dst_positive_scale_necessary_lookup_ha) + (dst_positive_scale_necessary_lookup_ha))) + (((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) * S ((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) + ((dst_negative_scale_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)))) * S ((((dst_positive_code_necessary_lookup_ha) + (dst_positive_scale_necessary_lookup_ha)) * S ((dst_positive_code_necessary_lookup_ha) + (dst_positive_scale_necessary_lookup_ha)) + ((dst_positive_scale_necessary_lookup_ha) + (dst_positive_scale_necessary_lookup_ha))) + (((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) * S ((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) + ((dst_negative_scale_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)))) + ((((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) * S ((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) + ((dst_negative_scale_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha))) + (((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) * S ((dst_negative_code_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)) + ((dst_negative_scale_necessary_lookup_ha) + (dst_negative_scale_necessary_lookup_ha)))))) /\ (((((exists ff_h_pvs_necessary_lookup_hapositive. ff_h_pvs_necessary_lookup_hapositive + S (dst_positive_necessary_lookup_ha) = S ((S (1)) * dst_positive_scale_necessary_lookup_ha)) /\ exists ff_q_pvs_necessary_lookup_hapositive. dst_positive_code_necessary_lookup_ha = ff_q_pvs_necessary_lookup_hapositive * S ((S (1)) * dst_positive_scale_necessary_lookup_ha) + (dst_positive_necessary_lookup_ha))) /\ (((((exists ff_h_pvs_necessary_lookup_hanegative. ff_h_pvs_necessary_lookup_hanegative + S (dst_negative_necessary_lookup_ha) = S ((S (1)) * dst_negative_scale_necessary_lookup_ha)) /\ exists ff_q_pvs_necessary_lookup_hanegative. dst_negative_code_necessary_lookup_ha = ff_q_pvs_necessary_lookup_hanegative * S ((S (1)) * dst_negative_scale_necessary_lookup_ha) + (dst_negative_necessary_lookup_ha))) /\ (exists ge_balance_positive_necessary_lookup_havalue ge_balance_negative_necessary_lookup_havalue. (((((a) = 2 * (ge_balance_positive_necessary_lookup_havalue) /\ (ge_balance_negative_necessary_lookup_havalue) = 0) \/ exists ge_signed_half_necessary_lookup_havaluedecode. (((a) = 2 * ge_signed_half_necessary_lookup_havaluedecode + 1 /\ (ge_balance_positive_necessary_lookup_havalue) = 0) /\ (ge_balance_negative_necessary_lookup_havalue) = S ge_signed_half_necessary_lookup_havaluedecode))) /\ ((dst_positive_necessary_lookup_ha) + ge_balance_negative_necessary_lookup_havalue = (dst_negative_necessary_lookup_ha) + ge_balance_positive_necessary_lookup_havalue))))))))) - 0017
specialize divisor_signed_table_lookup (N) - 0018
specialize divisor_signed_table_lookup (F) - 0019
specialize divisor_signed_table_lookup (1) - 0020
apply divisor_signed_table_lookup - 0021
exact hi_witness_right_left_left - 0022
exact hbound - 0023
cases ha - 0024
have hb : exists a. (exists dst_positive_code_necessary_lookup_hb dst_positive_scale_necessary_lookup_hb dst_negative_code_necessary_lookup_hb dst_negative_scale_necessary_lookup_hb dst_positive_necessary_lookup_hb dst_negative_necessary_lookup_hb. (((G) = (((((dst_positive_code_necessary_lookup_hb) + (dst_positive_scale_necessary_lookup_hb)) * S ((dst_positive_code_necessary_lookup_hb) + (dst_positive_scale_necessary_lookup_hb)) + ((dst_positive_scale_necessary_lookup_hb) + (dst_positive_scale_necessary_lookup_hb))) + (((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) * S ((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) + ((dst_negative_scale_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)))) * S ((((dst_positive_code_necessary_lookup_hb) + (dst_positive_scale_necessary_lookup_hb)) * S ((dst_positive_code_necessary_lookup_hb) + (dst_positive_scale_necessary_lookup_hb)) + ((dst_positive_scale_necessary_lookup_hb) + (dst_positive_scale_necessary_lookup_hb))) + (((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) * S ((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) + ((dst_negative_scale_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)))) + ((((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) * S ((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) + ((dst_negative_scale_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb))) + (((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) * S ((dst_negative_code_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)) + ((dst_negative_scale_necessary_lookup_hb) + (dst_negative_scale_necessary_lookup_hb)))))) /\ (((((exists ff_h_pvs_necessary_lookup_hbpositive. ff_h_pvs_necessary_lookup_hbpositive + S (dst_positive_necessary_lookup_hb) = S ((S (1)) * dst_positive_scale_necessary_lookup_hb)) /\ exists ff_q_pvs_necessary_lookup_hbpositive. dst_positive_code_necessary_lookup_hb = ff_q_pvs_necessary_lookup_hbpositive * S ((S (1)) * dst_positive_scale_necessary_lookup_hb) + (dst_positive_necessary_lookup_hb))) /\ (((((exists ff_h_pvs_necessary_lookup_hbnegative. ff_h_pvs_necessary_lookup_hbnegative + S (dst_negative_necessary_lookup_hb) = S ((S (1)) * dst_negative_scale_necessary_lookup_hb)) /\ exists ff_q_pvs_necessary_lookup_hbnegative. dst_negative_code_necessary_lookup_hb = ff_q_pvs_necessary_lookup_hbnegative * S ((S (1)) * dst_negative_scale_necessary_lookup_hb) + (dst_negative_necessary_lookup_hb))) /\ (exists ge_balance_positive_necessary_lookup_hbvalue ge_balance_negative_necessary_lookup_hbvalue. (((((a) = 2 * (ge_balance_positive_necessary_lookup_hbvalue) /\ (ge_balance_negative_necessary_lookup_hbvalue) = 0) \/ exists ge_signed_half_necessary_lookup_hbvaluedecode. (((a) = 2 * ge_signed_half_necessary_lookup_hbvaluedecode + 1 /\ (ge_balance_positive_necessary_lookup_hbvalue) = 0) /\ (ge_balance_negative_necessary_lookup_hbvalue) = S ge_signed_half_necessary_lookup_hbvaluedecode))) /\ ((dst_positive_necessary_lookup_hb) + ge_balance_negative_necessary_lookup_hbvalue = (dst_negative_necessary_lookup_hb) + ge_balance_positive_necessary_lookup_hbvalue))))))))) - 0025
specialize divisor_signed_table_lookup (N) - 0026
specialize divisor_signed_table_lookup (G) - 0027
specialize divisor_signed_table_lookup (1) - 0028
apply divisor_signed_table_lookup - 0029
exact hi_witness_right_left_right_left - 0030
exact hbound - 0031
cases hb - 0032
have he : exists a. (exists dst_positive_code_necessary_lookup_he dst_positive_scale_necessary_lookup_he dst_negative_code_necessary_lookup_he dst_negative_scale_necessary_lookup_he dst_positive_necessary_lookup_he dst_negative_necessary_lookup_he. (((x) = (((((dst_positive_code_necessary_lookup_he) + (dst_positive_scale_necessary_lookup_he)) * S ((dst_positive_code_necessary_lookup_he) + (dst_positive_scale_necessary_lookup_he)) + ((dst_positive_scale_necessary_lookup_he) + (dst_positive_scale_necessary_lookup_he))) + (((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) * S ((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) + ((dst_negative_scale_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)))) * S ((((dst_positive_code_necessary_lookup_he) + (dst_positive_scale_necessary_lookup_he)) * S ((dst_positive_code_necessary_lookup_he) + (dst_positive_scale_necessary_lookup_he)) + ((dst_positive_scale_necessary_lookup_he) + (dst_positive_scale_necessary_lookup_he))) + (((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) * S ((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) + ((dst_negative_scale_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)))) + ((((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) * S ((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) + ((dst_negative_scale_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he))) + (((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) * S ((dst_negative_code_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)) + ((dst_negative_scale_necessary_lookup_he) + (dst_negative_scale_necessary_lookup_he)))))) /\ (((((exists ff_h_pvs_necessary_lookup_hepositive. ff_h_pvs_necessary_lookup_hepositive + S (dst_positive_necessary_lookup_he) = S ((S (1)) * dst_positive_scale_necessary_lookup_he)) /\ exists ff_q_pvs_necessary_lookup_hepositive. dst_positive_code_necessary_lookup_he = ff_q_pvs_necessary_lookup_hepositive * S ((S (1)) * dst_positive_scale_necessary_lookup_he) + (dst_positive_necessary_lookup_he))) /\ (((((exists ff_h_pvs_necessary_lookup_henegative. ff_h_pvs_necessary_lookup_henegative + S (dst_negative_necessary_lookup_he) = S ((S (1)) * dst_negative_scale_necessary_lookup_he)) /\ exists ff_q_pvs_necessary_lookup_henegative. dst_negative_code_necessary_lookup_he = ff_q_pvs_necessary_lookup_henegative * S ((S (1)) * dst_negative_scale_necessary_lookup_he) + (dst_negative_necessary_lookup_he))) /\ (exists ge_balance_positive_necessary_lookup_hevalue ge_balance_negative_necessary_lookup_hevalue. (((((a) = 2 * (ge_balance_positive_necessary_lookup_hevalue) /\ (ge_balance_negative_necessary_lookup_hevalue) = 0) \/ exists ge_signed_half_necessary_lookup_hevaluedecode. (((a) = 2 * ge_signed_half_necessary_lookup_hevaluedecode + 1 /\ (ge_balance_positive_necessary_lookup_hevalue) = 0) /\ (ge_balance_negative_necessary_lookup_hevalue) = S ge_signed_half_necessary_lookup_hevaluedecode))) /\ ((dst_positive_necessary_lookup_he) + ge_balance_negative_necessary_lookup_hevalue = (dst_negative_necessary_lookup_he) + ge_balance_positive_necessary_lookup_hevalue))))))))) - 0033
specialize divisor_signed_table_lookup (N) - 0034
specialize divisor_signed_table_lookup (x) - 0035
specialize divisor_signed_table_lookup (1) - 0036
apply divisor_signed_table_lookup - 0037
exact hi_witness_right_left_right_right_left - 0038
exact hbound - 0039
cases he - 0040
have heq : x3=2 - 0041
specialize dirichlet_kronecker_delta_table_one_value (N) - 0042
specialize dirichlet_kronecker_delta_table_one_value (x) - 0043
specialize dirichlet_kronecker_delta_table_one_value (x3) - 0044
apply dirichlet_kronecker_delta_table_one_value - 0045
exact hi_witness_left - 0046
exact hbound - 0047
exact he_witness - 0048
rewrite heq at he_witness - 0049
rewrite heq at he_witness - 0050
have hc : ((~((1)=0)) /\ (exists dc_mask_necessary_one_convolution. ((((exists dst_positive_code_necessary_one_convolutionmasktable dst_positive_scale_necessary_one_convolutionmasktable dst_negative_code_necessary_one_convolutionmasktable dst_negative_scale_necessary_one_convolutionmasktable. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) * S ((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) + ((dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))) * S ((((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) * S ((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) + ((dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))) + ((((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))))) /\ (forall dst_index_necessary_one_convolutionmasktable. (exists pvs_le_gap_necessary_one_convolutionmasktabledomain. pvs_le_gap_necessary_one_convolutionmasktabledomain + (dst_index_necessary_one_convolutionmasktable) = (1)) -> exists dst_positive_necessary_one_convolutionmasktable dst_negative_necessary_one_convolutionmasktable dst_value_necessary_one_convolutionmasktable. ((((exists ff_h_pvs_necessary_one_convolutionmasktableentrypositive. ff_h_pvs_necessary_one_convolutionmasktableentrypositive + S (dst_positive_necessary_one_convolutionmasktable) = S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_positive_scale_necessary_one_convolutionmasktable)) /\ exists ff_q_pvs_necessary_one_convolutionmasktableentrypositive. dst_positive_code_necessary_one_convolutionmasktable = ff_q_pvs_necessary_one_convolutionmasktableentrypositive * S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_necessary_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasktableentrynegative. ff_h_pvs_necessary_one_convolutionmasktableentrynegative + S (dst_negative_necessary_one_convolutionmasktable) = S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_negative_scale_necessary_one_convolutionmasktable)) /\ exists ff_q_pvs_necessary_one_convolutionmasktableentrynegative. dst_negative_code_necessary_one_convolutionmasktable = ff_q_pvs_necessary_one_convolutionmasktableentrynegative * S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_necessary_one_convolutionmasktable))) /\ (exists ge_balance_positive_necessary_one_convolutionmasktableentryvalue ge_balance_negative_necessary_one_convolutionmasktableentryvalue. (((((dst_value_necessary_one_convolutionmasktable) = 2 * (ge_balance_positive_necessary_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_necessary_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode. (((dst_value_necessary_one_convolutionmasktable) = 2 * ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmasktableentryvalue) = S ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmasktable) + ge_balance_negative_necessary_one_convolutionmasktableentryvalue = (dst_negative_necessary_one_convolutionmasktable) + ge_balance_positive_necessary_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_necessary_one_convolutionmask dc_value_necessary_one_convolutionmask. (exists pvs_le_gap_necessary_one_convolutionmaskdomain. pvs_le_gap_necessary_one_convolutionmaskdomain + (dc_index_necessary_one_convolutionmask) = (1)) -> (exists dst_positive_code_necessary_one_convolutionmasklookup dst_positive_scale_necessary_one_convolutionmasklookup dst_negative_code_necessary_one_convolutionmasklookup dst_negative_scale_necessary_one_convolutionmasklookup dst_positive_necessary_one_convolutionmasklookup dst_negative_necessary_one_convolutionmasklookup. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) * S ((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) + ((dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))) * S ((((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) * S ((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) + ((dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))) + ((((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasklookuppositive. ff_h_pvs_necessary_one_convolutionmasklookuppositive + S (dst_positive_necessary_one_convolutionmasklookup) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmasklookup)) /\ exists ff_q_pvs_necessary_one_convolutionmasklookuppositive. dst_positive_code_necessary_one_convolutionmasklookup = ff_q_pvs_necessary_one_convolutionmasklookuppositive * S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_necessary_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasklookupnegative. ff_h_pvs_necessary_one_convolutionmasklookupnegative + S (dst_negative_necessary_one_convolutionmasklookup) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmasklookup)) /\ exists ff_q_pvs_necessary_one_convolutionmasklookupnegative. dst_negative_code_necessary_one_convolutionmasklookup = ff_q_pvs_necessary_one_convolutionmasklookupnegative * S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_necessary_one_convolutionmasklookup))) /\ (exists ge_balance_positive_necessary_one_convolutionmasklookupvalue ge_balance_negative_necessary_one_convolutionmasklookupvalue. (((((dc_value_necessary_one_convolutionmask) = 2 * (ge_balance_positive_necessary_one_convolutionmasklookupvalue) /\ (ge_balance_negative_necessary_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmasklookupvaluedecode. (((dc_value_necessary_one_convolutionmask) = 2 * ge_signed_half_necessary_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmasklookupvalue) = S ge_signed_half_necessary_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmasklookup) + ge_balance_negative_necessary_one_convolutionmasklookupvalue = (dst_negative_necessary_one_convolutionmasklookup) + ge_balance_positive_necessary_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_necessary_one_convolutionmask)=0)) /\ (exists dc_quotient_necessary_one_convolutionmaskentry dc_left_necessary_one_convolutionmaskentry dc_right_necessary_one_convolutionmaskentry. (((1)=(dc_index_necessary_one_convolutionmask)*dc_quotient_necessary_one_convolutionmaskentry) /\ (((exists dst_positive_code_necessary_one_convolutionmaskentryleft dst_positive_scale_necessary_one_convolutionmaskentryleft dst_negative_code_necessary_one_convolutionmaskentryleft dst_negative_scale_necessary_one_convolutionmaskentryleft dst_positive_necessary_one_convolutionmaskentryleft dst_negative_necessary_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) + ((dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) + ((dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))) + ((((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryleftpositive. ff_h_pvs_necessary_one_convolutionmaskentryleftpositive + S (dst_positive_necessary_one_convolutionmaskentryleft) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryleftpositive. dst_positive_code_necessary_one_convolutionmaskentryleft = ff_q_pvs_necessary_one_convolutionmaskentryleftpositive * S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_necessary_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryleftnegative. ff_h_pvs_necessary_one_convolutionmaskentryleftnegative + S (dst_negative_necessary_one_convolutionmaskentryleft) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryleftnegative. dst_negative_code_necessary_one_convolutionmaskentryleft = ff_q_pvs_necessary_one_convolutionmaskentryleftnegative * S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_necessary_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_necessary_one_convolutionmaskentryleftvalue ge_balance_negative_necessary_one_convolutionmaskentryleftvalue. (((((dc_left_necessary_one_convolutionmaskentry) = 2 * (ge_balance_positive_necessary_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_necessary_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode. (((dc_left_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmaskentryleftvalue) = S ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmaskentryleft) + ge_balance_negative_necessary_one_convolutionmaskentryleftvalue = (dst_negative_necessary_one_convolutionmaskentryleft) + ge_balance_positive_necessary_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_necessary_one_convolutionmaskentryright dst_positive_scale_necessary_one_convolutionmaskentryright dst_negative_code_necessary_one_convolutionmaskentryright dst_negative_scale_necessary_one_convolutionmaskentryright dst_positive_necessary_one_convolutionmaskentryright dst_negative_necessary_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) * S ((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) + ((dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))) * S ((((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) * S ((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) + ((dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))) + ((((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryrightpositive. ff_h_pvs_necessary_one_convolutionmaskentryrightpositive + S (dst_positive_necessary_one_convolutionmaskentryright) = S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_positive_scale_necessary_one_convolutionmaskentryright)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryrightpositive. dst_positive_code_necessary_one_convolutionmaskentryright = ff_q_pvs_necessary_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_necessary_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryrightnegative. ff_h_pvs_necessary_one_convolutionmaskentryrightnegative + S (dst_negative_necessary_one_convolutionmaskentryright) = S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_negative_scale_necessary_one_convolutionmaskentryright)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryrightnegative. dst_negative_code_necessary_one_convolutionmaskentryright = ff_q_pvs_necessary_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_necessary_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_necessary_one_convolutionmaskentryrightvalue ge_balance_negative_necessary_one_convolutionmaskentryrightvalue. (((((dc_right_necessary_one_convolutionmaskentry) = 2 * (ge_balance_positive_necessary_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_necessary_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode. (((dc_right_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmaskentryrightvalue) = S ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmaskentryright) + ge_balance_negative_necessary_one_convolutionmaskentryrightvalue = (dst_negative_necessary_one_convolutionmaskentryright) + ge_balance_positive_necessary_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_necessary_one_convolutionmaskentryproduct sto_an_necessary_one_convolutionmaskentryproduct sto_bp_necessary_one_convolutionmaskentryproduct sto_bn_necessary_one_convolutionmaskentryproduct sto_cp_necessary_one_convolutionmaskentryproduct sto_cn_necessary_one_convolutionmaskentryproduct. (((((dc_left_necessary_one_convolutionmaskentry) = 2 * (sto_ap_necessary_one_convolutionmaskentryproduct) /\ (sto_an_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductleft. (((dc_left_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_an_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_necessary_one_convolutionmaskentry) = 2 * (sto_bp_necessary_one_convolutionmaskentryproduct) /\ (sto_bn_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductright. (((dc_right_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductright + 1 /\ (sto_bp_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductright))) /\ ((((((dc_value_necessary_one_convolutionmask) = 2 * (sto_cp_necessary_one_convolutionmaskentryproduct) /\ (sto_cn_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductoutput. (((dc_value_necessary_one_convolutionmask) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_necessary_one_convolutionmaskentryproduct * sto_bp_necessary_one_convolutionmaskentryproduct + sto_an_necessary_one_convolutionmaskentryproduct * sto_bn_necessary_one_convolutionmaskentryproduct) + sto_cn_necessary_one_convolutionmaskentryproduct = (sto_ap_necessary_one_convolutionmaskentryproduct * sto_bn_necessary_one_convolutionmaskentryproduct + sto_an_necessary_one_convolutionmaskentryproduct * sto_bp_necessary_one_convolutionmaskentryproduct) + sto_cp_necessary_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_necessary_one_convolutionmask)=0 \/ ~(exists pvs_factor_necessary_one_convolutionmaskentrynondivisor. (1) = (dc_index_necessary_one_convolutionmask) * pvs_factor_necessary_one_convolutionmaskentrynondivisor)) /\ ((dc_value_necessary_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_necessary_one_convolutionfold dst_positive_scale_necessary_one_convolutionfold dst_negative_code_necessary_one_convolutionfold dst_negative_scale_necessary_one_convolutionfold dst_positive_sum_necessary_one_convolutionfold dst_negative_sum_necessary_one_convolutionfold. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) * S ((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) + ((dst_positive_scale_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))) * S ((((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) * S ((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) + ((dst_positive_scale_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))) + ((((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))))) /\ (((exists fs_u_dst_necessary_one_convolutionfoldpositive fs_v_dst_necessary_one_convolutionfoldpositive. ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_start. fs_h_dst_necessary_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_start. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_terminal. fs_h_dst_necessary_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_necessary_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_terminal. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldpositive) + (dst_positive_sum_necessary_one_convolutionfold))) /\ forall fs_i_dst_necessary_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_necessary_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_necessary_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_necessary_one_convolutionfoldpositive_body_steps fs_r_dst_necessary_one_convolutionfoldpositive_body_steps fs_s_dst_necessary_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_necessary_one_convolutionfold)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_necessary_one_convolutionfold = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_necessary_one_convolutionfold) + (fs_a_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (fs_r_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (fs_s_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_necessary_one_convolutionfoldpositive_body_steps = fs_r_dst_necessary_one_convolutionfoldpositive_body_steps + fs_a_dst_necessary_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_necessary_one_convolutionfoldnegative fs_v_dst_necessary_one_convolutionfoldnegative. ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_start. fs_h_dst_necessary_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_start. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_terminal. fs_h_dst_necessary_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_necessary_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_terminal. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldnegative) + (dst_negative_sum_necessary_one_convolutionfold))) /\ forall fs_i_dst_necessary_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_necessary_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_necessary_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_necessary_one_convolutionfoldnegative_body_steps fs_r_dst_necessary_one_convolutionfoldnegative_body_steps fs_s_dst_necessary_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_necessary_one_convolutionfold)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_necessary_one_convolutionfold = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_necessary_one_convolutionfold) + (fs_a_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (fs_r_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (fs_s_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_necessary_one_convolutionfoldnegative_body_steps = fs_r_dst_necessary_one_convolutionfoldnegative_body_steps + fs_a_dst_necessary_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_necessary_one_convolutionfoldresult ge_balance_negative_necessary_one_convolutionfoldresult. (((((2) = 2 * (ge_balance_positive_necessary_one_convolutionfoldresult) /\ (ge_balance_negative_necessary_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_necessary_one_convolutionfoldresultdecode. (((2) = 2 * ge_signed_half_necessary_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_necessary_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_necessary_one_convolutionfoldresult) = S ge_signed_half_necessary_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_necessary_one_convolutionfold) + ge_balance_negative_necessary_one_convolutionfoldresult = (dst_negative_sum_necessary_one_convolutionfold) + ge_balance_positive_necessary_one_convolutionfoldresult)))))))))))) - 0051
specialize hi_witness_right_left_right_right_right (1) - 0052
specialize hi_witness_right_left_right_right_right (2) - 0053
apply hi_witness_right_left_right_right_right - 0054
intro hz - 0055
apply PA1 - 0056
exact hz - 0057
exact hbound - 0058
exact he_witness - 0059
have hiff : (((((~((1)=0)) /\ (exists dc_mask_necessary_one_convolution. ((((exists dst_positive_code_necessary_one_convolutionmasktable dst_positive_scale_necessary_one_convolutionmasktable dst_negative_code_necessary_one_convolutionmasktable dst_negative_scale_necessary_one_convolutionmasktable. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) * S ((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) + ((dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))) * S ((((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) * S ((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) + ((dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))) + ((((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))))) /\ (forall dst_index_necessary_one_convolutionmasktable. (exists pvs_le_gap_necessary_one_convolutionmasktabledomain. pvs_le_gap_necessary_one_convolutionmasktabledomain + (dst_index_necessary_one_convolutionmasktable) = (1)) -> exists dst_positive_necessary_one_convolutionmasktable dst_negative_necessary_one_convolutionmasktable dst_value_necessary_one_convolutionmasktable. ((((exists ff_h_pvs_necessary_one_convolutionmasktableentrypositive. ff_h_pvs_necessary_one_convolutionmasktableentrypositive + S (dst_positive_necessary_one_convolutionmasktable) = S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_positive_scale_necessary_one_convolutionmasktable)) /\ exists ff_q_pvs_necessary_one_convolutionmasktableentrypositive. dst_positive_code_necessary_one_convolutionmasktable = ff_q_pvs_necessary_one_convolutionmasktableentrypositive * S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_necessary_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasktableentrynegative. ff_h_pvs_necessary_one_convolutionmasktableentrynegative + S (dst_negative_necessary_one_convolutionmasktable) = S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_negative_scale_necessary_one_convolutionmasktable)) /\ exists ff_q_pvs_necessary_one_convolutionmasktableentrynegative. dst_negative_code_necessary_one_convolutionmasktable = ff_q_pvs_necessary_one_convolutionmasktableentrynegative * S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_necessary_one_convolutionmasktable))) /\ (exists ge_balance_positive_necessary_one_convolutionmasktableentryvalue ge_balance_negative_necessary_one_convolutionmasktableentryvalue. (((((dst_value_necessary_one_convolutionmasktable) = 2 * (ge_balance_positive_necessary_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_necessary_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode. (((dst_value_necessary_one_convolutionmasktable) = 2 * ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmasktableentryvalue) = S ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmasktable) + ge_balance_negative_necessary_one_convolutionmasktableentryvalue = (dst_negative_necessary_one_convolutionmasktable) + ge_balance_positive_necessary_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_necessary_one_convolutionmask dc_value_necessary_one_convolutionmask. (exists pvs_le_gap_necessary_one_convolutionmaskdomain. pvs_le_gap_necessary_one_convolutionmaskdomain + (dc_index_necessary_one_convolutionmask) = (1)) -> (exists dst_positive_code_necessary_one_convolutionmasklookup dst_positive_scale_necessary_one_convolutionmasklookup dst_negative_code_necessary_one_convolutionmasklookup dst_negative_scale_necessary_one_convolutionmasklookup dst_positive_necessary_one_convolutionmasklookup dst_negative_necessary_one_convolutionmasklookup. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) * S ((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) + ((dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))) * S ((((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) * S ((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) + ((dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))) + ((((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasklookuppositive. ff_h_pvs_necessary_one_convolutionmasklookuppositive + S (dst_positive_necessary_one_convolutionmasklookup) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmasklookup)) /\ exists ff_q_pvs_necessary_one_convolutionmasklookuppositive. dst_positive_code_necessary_one_convolutionmasklookup = ff_q_pvs_necessary_one_convolutionmasklookuppositive * S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_necessary_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasklookupnegative. ff_h_pvs_necessary_one_convolutionmasklookupnegative + S (dst_negative_necessary_one_convolutionmasklookup) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmasklookup)) /\ exists ff_q_pvs_necessary_one_convolutionmasklookupnegative. dst_negative_code_necessary_one_convolutionmasklookup = ff_q_pvs_necessary_one_convolutionmasklookupnegative * S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_necessary_one_convolutionmasklookup))) /\ (exists ge_balance_positive_necessary_one_convolutionmasklookupvalue ge_balance_negative_necessary_one_convolutionmasklookupvalue. (((((dc_value_necessary_one_convolutionmask) = 2 * (ge_balance_positive_necessary_one_convolutionmasklookupvalue) /\ (ge_balance_negative_necessary_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmasklookupvaluedecode. (((dc_value_necessary_one_convolutionmask) = 2 * ge_signed_half_necessary_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmasklookupvalue) = S ge_signed_half_necessary_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmasklookup) + ge_balance_negative_necessary_one_convolutionmasklookupvalue = (dst_negative_necessary_one_convolutionmasklookup) + ge_balance_positive_necessary_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_necessary_one_convolutionmask)=0)) /\ (exists dc_quotient_necessary_one_convolutionmaskentry dc_left_necessary_one_convolutionmaskentry dc_right_necessary_one_convolutionmaskentry. (((1)=(dc_index_necessary_one_convolutionmask)*dc_quotient_necessary_one_convolutionmaskentry) /\ (((exists dst_positive_code_necessary_one_convolutionmaskentryleft dst_positive_scale_necessary_one_convolutionmaskentryleft dst_negative_code_necessary_one_convolutionmaskentryleft dst_negative_scale_necessary_one_convolutionmaskentryleft dst_positive_necessary_one_convolutionmaskentryleft dst_negative_necessary_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) + ((dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) + ((dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))) + ((((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryleftpositive. ff_h_pvs_necessary_one_convolutionmaskentryleftpositive + S (dst_positive_necessary_one_convolutionmaskentryleft) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryleftpositive. dst_positive_code_necessary_one_convolutionmaskentryleft = ff_q_pvs_necessary_one_convolutionmaskentryleftpositive * S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_necessary_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryleftnegative. ff_h_pvs_necessary_one_convolutionmaskentryleftnegative + S (dst_negative_necessary_one_convolutionmaskentryleft) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryleftnegative. dst_negative_code_necessary_one_convolutionmaskentryleft = ff_q_pvs_necessary_one_convolutionmaskentryleftnegative * S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_necessary_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_necessary_one_convolutionmaskentryleftvalue ge_balance_negative_necessary_one_convolutionmaskentryleftvalue. (((((dc_left_necessary_one_convolutionmaskentry) = 2 * (ge_balance_positive_necessary_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_necessary_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode. (((dc_left_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmaskentryleftvalue) = S ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmaskentryleft) + ge_balance_negative_necessary_one_convolutionmaskentryleftvalue = (dst_negative_necessary_one_convolutionmaskentryleft) + ge_balance_positive_necessary_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_necessary_one_convolutionmaskentryright dst_positive_scale_necessary_one_convolutionmaskentryright dst_negative_code_necessary_one_convolutionmaskentryright dst_negative_scale_necessary_one_convolutionmaskentryright dst_positive_necessary_one_convolutionmaskentryright dst_negative_necessary_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) * S ((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) + ((dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))) * S ((((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) * S ((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) + ((dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))) + ((((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryrightpositive. ff_h_pvs_necessary_one_convolutionmaskentryrightpositive + S (dst_positive_necessary_one_convolutionmaskentryright) = S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_positive_scale_necessary_one_convolutionmaskentryright)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryrightpositive. dst_positive_code_necessary_one_convolutionmaskentryright = ff_q_pvs_necessary_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_necessary_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryrightnegative. ff_h_pvs_necessary_one_convolutionmaskentryrightnegative + S (dst_negative_necessary_one_convolutionmaskentryright) = S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_negative_scale_necessary_one_convolutionmaskentryright)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryrightnegative. dst_negative_code_necessary_one_convolutionmaskentryright = ff_q_pvs_necessary_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_necessary_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_necessary_one_convolutionmaskentryrightvalue ge_balance_negative_necessary_one_convolutionmaskentryrightvalue. (((((dc_right_necessary_one_convolutionmaskentry) = 2 * (ge_balance_positive_necessary_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_necessary_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode. (((dc_right_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmaskentryrightvalue) = S ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmaskentryright) + ge_balance_negative_necessary_one_convolutionmaskentryrightvalue = (dst_negative_necessary_one_convolutionmaskentryright) + ge_balance_positive_necessary_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_necessary_one_convolutionmaskentryproduct sto_an_necessary_one_convolutionmaskentryproduct sto_bp_necessary_one_convolutionmaskentryproduct sto_bn_necessary_one_convolutionmaskentryproduct sto_cp_necessary_one_convolutionmaskentryproduct sto_cn_necessary_one_convolutionmaskentryproduct. (((((dc_left_necessary_one_convolutionmaskentry) = 2 * (sto_ap_necessary_one_convolutionmaskentryproduct) /\ (sto_an_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductleft. (((dc_left_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_an_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_necessary_one_convolutionmaskentry) = 2 * (sto_bp_necessary_one_convolutionmaskentryproduct) /\ (sto_bn_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductright. (((dc_right_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductright + 1 /\ (sto_bp_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductright))) /\ ((((((dc_value_necessary_one_convolutionmask) = 2 * (sto_cp_necessary_one_convolutionmaskentryproduct) /\ (sto_cn_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductoutput. (((dc_value_necessary_one_convolutionmask) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_necessary_one_convolutionmaskentryproduct * sto_bp_necessary_one_convolutionmaskentryproduct + sto_an_necessary_one_convolutionmaskentryproduct * sto_bn_necessary_one_convolutionmaskentryproduct) + sto_cn_necessary_one_convolutionmaskentryproduct = (sto_ap_necessary_one_convolutionmaskentryproduct * sto_bn_necessary_one_convolutionmaskentryproduct + sto_an_necessary_one_convolutionmaskentryproduct * sto_bp_necessary_one_convolutionmaskentryproduct) + sto_cp_necessary_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_necessary_one_convolutionmask)=0 \/ ~(exists pvs_factor_necessary_one_convolutionmaskentrynondivisor. (1) = (dc_index_necessary_one_convolutionmask) * pvs_factor_necessary_one_convolutionmaskentrynondivisor)) /\ ((dc_value_necessary_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_necessary_one_convolutionfold dst_positive_scale_necessary_one_convolutionfold dst_negative_code_necessary_one_convolutionfold dst_negative_scale_necessary_one_convolutionfold dst_positive_sum_necessary_one_convolutionfold dst_negative_sum_necessary_one_convolutionfold. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) * S ((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) + ((dst_positive_scale_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))) * S ((((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) * S ((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) + ((dst_positive_scale_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))) + ((((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))))) /\ (((exists fs_u_dst_necessary_one_convolutionfoldpositive fs_v_dst_necessary_one_convolutionfoldpositive. ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_start. fs_h_dst_necessary_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_start. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_terminal. fs_h_dst_necessary_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_necessary_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_terminal. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldpositive) + (dst_positive_sum_necessary_one_convolutionfold))) /\ forall fs_i_dst_necessary_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_necessary_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_necessary_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_necessary_one_convolutionfoldpositive_body_steps fs_r_dst_necessary_one_convolutionfoldpositive_body_steps fs_s_dst_necessary_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_necessary_one_convolutionfold)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_necessary_one_convolutionfold = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_necessary_one_convolutionfold) + (fs_a_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (fs_r_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (fs_s_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_necessary_one_convolutionfoldpositive_body_steps = fs_r_dst_necessary_one_convolutionfoldpositive_body_steps + fs_a_dst_necessary_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_necessary_one_convolutionfoldnegative fs_v_dst_necessary_one_convolutionfoldnegative. ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_start. fs_h_dst_necessary_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_start. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_terminal. fs_h_dst_necessary_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_necessary_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_terminal. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldnegative) + (dst_negative_sum_necessary_one_convolutionfold))) /\ forall fs_i_dst_necessary_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_necessary_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_necessary_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_necessary_one_convolutionfoldnegative_body_steps fs_r_dst_necessary_one_convolutionfoldnegative_body_steps fs_s_dst_necessary_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_necessary_one_convolutionfold)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_necessary_one_convolutionfold = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_necessary_one_convolutionfold) + (fs_a_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (fs_r_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (fs_s_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_necessary_one_convolutionfoldnegative_body_steps = fs_r_dst_necessary_one_convolutionfoldnegative_body_steps + fs_a_dst_necessary_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_necessary_one_convolutionfoldresult ge_balance_negative_necessary_one_convolutionfoldresult. (((((2) = 2 * (ge_balance_positive_necessary_one_convolutionfoldresult) /\ (ge_balance_negative_necessary_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_necessary_one_convolutionfoldresultdecode. (((2) = 2 * ge_signed_half_necessary_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_necessary_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_necessary_one_convolutionfoldresult) = S ge_signed_half_necessary_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_necessary_one_convolutionfold) + ge_balance_negative_necessary_one_convolutionfoldresult = (dst_negative_sum_necessary_one_convolutionfold) + ge_balance_positive_necessary_one_convolutionfoldresult))))))))))))) -> (exists sto_ap_necessary_one_product sto_an_necessary_one_product sto_bp_necessary_one_product sto_bn_necessary_one_product sto_cp_necessary_one_product sto_cn_necessary_one_product. (((((x1) = 2 * (sto_ap_necessary_one_product) /\ (sto_an_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productleft. (((x1) = 2 * ge_signed_half_necessary_one_productleft + 1 /\ (sto_ap_necessary_one_product) = 0) /\ (sto_an_necessary_one_product) = S ge_signed_half_necessary_one_productleft))) /\ ((((((x2) = 2 * (sto_bp_necessary_one_product) /\ (sto_bn_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productright. (((x2) = 2 * ge_signed_half_necessary_one_productright + 1 /\ (sto_bp_necessary_one_product) = 0) /\ (sto_bn_necessary_one_product) = S ge_signed_half_necessary_one_productright))) /\ ((((((2) = 2 * (sto_cp_necessary_one_product) /\ (sto_cn_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productoutput. (((2) = 2 * ge_signed_half_necessary_one_productoutput + 1 /\ (sto_cp_necessary_one_product) = 0) /\ (sto_cn_necessary_one_product) = S ge_signed_half_necessary_one_productoutput))) /\ ((sto_ap_necessary_one_product * sto_bp_necessary_one_product + sto_an_necessary_one_product * sto_bn_necessary_one_product) + sto_cn_necessary_one_product = (sto_ap_necessary_one_product * sto_bn_necessary_one_product + sto_an_necessary_one_product * sto_bp_necessary_one_product) + sto_cp_necessary_one_product)))))))) /\ ((exists sto_ap_necessary_one_product sto_an_necessary_one_product sto_bp_necessary_one_product sto_bn_necessary_one_product sto_cp_necessary_one_product sto_cn_necessary_one_product. (((((x1) = 2 * (sto_ap_necessary_one_product) /\ (sto_an_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productleft. (((x1) = 2 * ge_signed_half_necessary_one_productleft + 1 /\ (sto_ap_necessary_one_product) = 0) /\ (sto_an_necessary_one_product) = S ge_signed_half_necessary_one_productleft))) /\ ((((((x2) = 2 * (sto_bp_necessary_one_product) /\ (sto_bn_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productright. (((x2) = 2 * ge_signed_half_necessary_one_productright + 1 /\ (sto_bp_necessary_one_product) = 0) /\ (sto_bn_necessary_one_product) = S ge_signed_half_necessary_one_productright))) /\ ((((((2) = 2 * (sto_cp_necessary_one_product) /\ (sto_cn_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productoutput. (((2) = 2 * ge_signed_half_necessary_one_productoutput + 1 /\ (sto_cp_necessary_one_product) = 0) /\ (sto_cn_necessary_one_product) = S ge_signed_half_necessary_one_productoutput))) /\ ((sto_ap_necessary_one_product * sto_bp_necessary_one_product + sto_an_necessary_one_product * sto_bn_necessary_one_product) + sto_cn_necessary_one_product = (sto_ap_necessary_one_product * sto_bn_necessary_one_product + sto_an_necessary_one_product * sto_bp_necessary_one_product) + sto_cp_necessary_one_product))))))) -> (((~((1)=0)) /\ (exists dc_mask_necessary_one_convolution. ((((exists dst_positive_code_necessary_one_convolutionmasktable dst_positive_scale_necessary_one_convolutionmasktable dst_negative_code_necessary_one_convolutionmasktable dst_negative_scale_necessary_one_convolutionmasktable. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) * S ((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) + ((dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))) * S ((((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) * S ((dst_positive_code_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable)) + ((dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))) + ((((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable))) + (((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) * S ((dst_negative_code_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)) + ((dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_scale_necessary_one_convolutionmasktable)))))) /\ (forall dst_index_necessary_one_convolutionmasktable. (exists pvs_le_gap_necessary_one_convolutionmasktabledomain. pvs_le_gap_necessary_one_convolutionmasktabledomain + (dst_index_necessary_one_convolutionmasktable) = (1)) -> exists dst_positive_necessary_one_convolutionmasktable dst_negative_necessary_one_convolutionmasktable dst_value_necessary_one_convolutionmasktable. ((((exists ff_h_pvs_necessary_one_convolutionmasktableentrypositive. ff_h_pvs_necessary_one_convolutionmasktableentrypositive + S (dst_positive_necessary_one_convolutionmasktable) = S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_positive_scale_necessary_one_convolutionmasktable)) /\ exists ff_q_pvs_necessary_one_convolutionmasktableentrypositive. dst_positive_code_necessary_one_convolutionmasktable = ff_q_pvs_necessary_one_convolutionmasktableentrypositive * S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_positive_scale_necessary_one_convolutionmasktable) + (dst_positive_necessary_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasktableentrynegative. ff_h_pvs_necessary_one_convolutionmasktableentrynegative + S (dst_negative_necessary_one_convolutionmasktable) = S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_negative_scale_necessary_one_convolutionmasktable)) /\ exists ff_q_pvs_necessary_one_convolutionmasktableentrynegative. dst_negative_code_necessary_one_convolutionmasktable = ff_q_pvs_necessary_one_convolutionmasktableentrynegative * S ((S (dst_index_necessary_one_convolutionmasktable)) * dst_negative_scale_necessary_one_convolutionmasktable) + (dst_negative_necessary_one_convolutionmasktable))) /\ (exists ge_balance_positive_necessary_one_convolutionmasktableentryvalue ge_balance_negative_necessary_one_convolutionmasktableentryvalue. (((((dst_value_necessary_one_convolutionmasktable) = 2 * (ge_balance_positive_necessary_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_necessary_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode. (((dst_value_necessary_one_convolutionmasktable) = 2 * ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmasktableentryvalue) = S ge_signed_half_necessary_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmasktable) + ge_balance_negative_necessary_one_convolutionmasktableentryvalue = (dst_negative_necessary_one_convolutionmasktable) + ge_balance_positive_necessary_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_necessary_one_convolutionmask dc_value_necessary_one_convolutionmask. (exists pvs_le_gap_necessary_one_convolutionmaskdomain. pvs_le_gap_necessary_one_convolutionmaskdomain + (dc_index_necessary_one_convolutionmask) = (1)) -> (exists dst_positive_code_necessary_one_convolutionmasklookup dst_positive_scale_necessary_one_convolutionmasklookup dst_negative_code_necessary_one_convolutionmasklookup dst_negative_scale_necessary_one_convolutionmasklookup dst_positive_necessary_one_convolutionmasklookup dst_negative_necessary_one_convolutionmasklookup. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) * S ((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) + ((dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))) * S ((((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) * S ((dst_positive_code_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup)) + ((dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))) + ((((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup))) + (((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) * S ((dst_negative_code_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)) + ((dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_scale_necessary_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasklookuppositive. ff_h_pvs_necessary_one_convolutionmasklookuppositive + S (dst_positive_necessary_one_convolutionmasklookup) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmasklookup)) /\ exists ff_q_pvs_necessary_one_convolutionmasklookuppositive. dst_positive_code_necessary_one_convolutionmasklookup = ff_q_pvs_necessary_one_convolutionmasklookuppositive * S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmasklookup) + (dst_positive_necessary_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmasklookupnegative. ff_h_pvs_necessary_one_convolutionmasklookupnegative + S (dst_negative_necessary_one_convolutionmasklookup) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmasklookup)) /\ exists ff_q_pvs_necessary_one_convolutionmasklookupnegative. dst_negative_code_necessary_one_convolutionmasklookup = ff_q_pvs_necessary_one_convolutionmasklookupnegative * S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmasklookup) + (dst_negative_necessary_one_convolutionmasklookup))) /\ (exists ge_balance_positive_necessary_one_convolutionmasklookupvalue ge_balance_negative_necessary_one_convolutionmasklookupvalue. (((((dc_value_necessary_one_convolutionmask) = 2 * (ge_balance_positive_necessary_one_convolutionmasklookupvalue) /\ (ge_balance_negative_necessary_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmasklookupvaluedecode. (((dc_value_necessary_one_convolutionmask) = 2 * ge_signed_half_necessary_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmasklookupvalue) = S ge_signed_half_necessary_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmasklookup) + ge_balance_negative_necessary_one_convolutionmasklookupvalue = (dst_negative_necessary_one_convolutionmasklookup) + ge_balance_positive_necessary_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_necessary_one_convolutionmask)=0)) /\ (exists dc_quotient_necessary_one_convolutionmaskentry dc_left_necessary_one_convolutionmaskentry dc_right_necessary_one_convolutionmaskentry. (((1)=(dc_index_necessary_one_convolutionmask)*dc_quotient_necessary_one_convolutionmaskentry) /\ (((exists dst_positive_code_necessary_one_convolutionmaskentryleft dst_positive_scale_necessary_one_convolutionmaskentryleft dst_negative_code_necessary_one_convolutionmaskentryleft dst_negative_scale_necessary_one_convolutionmaskentryleft dst_positive_necessary_one_convolutionmaskentryleft dst_negative_necessary_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) + ((dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_positive_code_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft)) + ((dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))) + ((((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft))) + (((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) * S ((dst_negative_code_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)) + ((dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_scale_necessary_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryleftpositive. ff_h_pvs_necessary_one_convolutionmaskentryleftpositive + S (dst_positive_necessary_one_convolutionmaskentryleft) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryleftpositive. dst_positive_code_necessary_one_convolutionmaskentryleft = ff_q_pvs_necessary_one_convolutionmaskentryleftpositive * S ((S (dc_index_necessary_one_convolutionmask)) * dst_positive_scale_necessary_one_convolutionmaskentryleft) + (dst_positive_necessary_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryleftnegative. ff_h_pvs_necessary_one_convolutionmaskentryleftnegative + S (dst_negative_necessary_one_convolutionmaskentryleft) = S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryleftnegative. dst_negative_code_necessary_one_convolutionmaskentryleft = ff_q_pvs_necessary_one_convolutionmaskentryleftnegative * S ((S (dc_index_necessary_one_convolutionmask)) * dst_negative_scale_necessary_one_convolutionmaskentryleft) + (dst_negative_necessary_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_necessary_one_convolutionmaskentryleftvalue ge_balance_negative_necessary_one_convolutionmaskentryleftvalue. (((((dc_left_necessary_one_convolutionmaskentry) = 2 * (ge_balance_positive_necessary_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_necessary_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode. (((dc_left_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmaskentryleftvalue) = S ge_signed_half_necessary_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmaskentryleft) + ge_balance_negative_necessary_one_convolutionmaskentryleftvalue = (dst_negative_necessary_one_convolutionmaskentryleft) + ge_balance_positive_necessary_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_necessary_one_convolutionmaskentryright dst_positive_scale_necessary_one_convolutionmaskentryright dst_negative_code_necessary_one_convolutionmaskentryright dst_negative_scale_necessary_one_convolutionmaskentryright dst_positive_necessary_one_convolutionmaskentryright dst_negative_necessary_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) * S ((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) + ((dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))) * S ((((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) * S ((dst_positive_code_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright)) + ((dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))) + ((((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright))) + (((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) * S ((dst_negative_code_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)) + ((dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_scale_necessary_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryrightpositive. ff_h_pvs_necessary_one_convolutionmaskentryrightpositive + S (dst_positive_necessary_one_convolutionmaskentryright) = S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_positive_scale_necessary_one_convolutionmaskentryright)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryrightpositive. dst_positive_code_necessary_one_convolutionmaskentryright = ff_q_pvs_necessary_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_positive_scale_necessary_one_convolutionmaskentryright) + (dst_positive_necessary_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_necessary_one_convolutionmaskentryrightnegative. ff_h_pvs_necessary_one_convolutionmaskentryrightnegative + S (dst_negative_necessary_one_convolutionmaskentryright) = S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_negative_scale_necessary_one_convolutionmaskentryright)) /\ exists ff_q_pvs_necessary_one_convolutionmaskentryrightnegative. dst_negative_code_necessary_one_convolutionmaskentryright = ff_q_pvs_necessary_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_necessary_one_convolutionmaskentry)) * dst_negative_scale_necessary_one_convolutionmaskentryright) + (dst_negative_necessary_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_necessary_one_convolutionmaskentryrightvalue ge_balance_negative_necessary_one_convolutionmaskentryrightvalue. (((((dc_right_necessary_one_convolutionmaskentry) = 2 * (ge_balance_positive_necessary_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_necessary_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode. (((dc_right_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_necessary_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_necessary_one_convolutionmaskentryrightvalue) = S ge_signed_half_necessary_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_necessary_one_convolutionmaskentryright) + ge_balance_negative_necessary_one_convolutionmaskentryrightvalue = (dst_negative_necessary_one_convolutionmaskentryright) + ge_balance_positive_necessary_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_necessary_one_convolutionmaskentryproduct sto_an_necessary_one_convolutionmaskentryproduct sto_bp_necessary_one_convolutionmaskentryproduct sto_bn_necessary_one_convolutionmaskentryproduct sto_cp_necessary_one_convolutionmaskentryproduct sto_cn_necessary_one_convolutionmaskentryproduct. (((((dc_left_necessary_one_convolutionmaskentry) = 2 * (sto_ap_necessary_one_convolutionmaskentryproduct) /\ (sto_an_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductleft. (((dc_left_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_an_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_necessary_one_convolutionmaskentry) = 2 * (sto_bp_necessary_one_convolutionmaskentryproduct) /\ (sto_bn_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductright. (((dc_right_necessary_one_convolutionmaskentry) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductright + 1 /\ (sto_bp_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductright))) /\ ((((((dc_value_necessary_one_convolutionmask) = 2 * (sto_cp_necessary_one_convolutionmaskentryproduct) /\ (sto_cn_necessary_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_necessary_one_convolutionmaskentryproductoutput. (((dc_value_necessary_one_convolutionmask) = 2 * ge_signed_half_necessary_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_necessary_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_necessary_one_convolutionmaskentryproduct) = S ge_signed_half_necessary_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_necessary_one_convolutionmaskentryproduct * sto_bp_necessary_one_convolutionmaskentryproduct + sto_an_necessary_one_convolutionmaskentryproduct * sto_bn_necessary_one_convolutionmaskentryproduct) + sto_cn_necessary_one_convolutionmaskentryproduct = (sto_ap_necessary_one_convolutionmaskentryproduct * sto_bn_necessary_one_convolutionmaskentryproduct + sto_an_necessary_one_convolutionmaskentryproduct * sto_bp_necessary_one_convolutionmaskentryproduct) + sto_cp_necessary_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_necessary_one_convolutionmask)=0 \/ ~(exists pvs_factor_necessary_one_convolutionmaskentrynondivisor. (1) = (dc_index_necessary_one_convolutionmask) * pvs_factor_necessary_one_convolutionmaskentrynondivisor)) /\ ((dc_value_necessary_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_necessary_one_convolutionfold dst_positive_scale_necessary_one_convolutionfold dst_negative_code_necessary_one_convolutionfold dst_negative_scale_necessary_one_convolutionfold dst_positive_sum_necessary_one_convolutionfold dst_negative_sum_necessary_one_convolutionfold. (((dc_mask_necessary_one_convolution) = (((((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) * S ((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) + ((dst_positive_scale_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))) * S ((((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) * S ((dst_positive_code_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold)) + ((dst_positive_scale_necessary_one_convolutionfold) + (dst_positive_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))) + ((((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold))) + (((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) * S ((dst_negative_code_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)) + ((dst_negative_scale_necessary_one_convolutionfold) + (dst_negative_scale_necessary_one_convolutionfold)))))) /\ (((exists fs_u_dst_necessary_one_convolutionfoldpositive fs_v_dst_necessary_one_convolutionfoldpositive. ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_start. fs_h_dst_necessary_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_start. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_terminal. fs_h_dst_necessary_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_necessary_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_terminal. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldpositive) + (dst_positive_sum_necessary_one_convolutionfold))) /\ forall fs_i_dst_necessary_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_necessary_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_necessary_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_necessary_one_convolutionfoldpositive_body_steps fs_r_dst_necessary_one_convolutionfoldpositive_body_steps fs_s_dst_necessary_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_necessary_one_convolutionfold)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_necessary_one_convolutionfold = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_necessary_one_convolutionfold) + (fs_a_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (fs_r_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_necessary_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_necessary_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive)) /\ exists fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_necessary_one_convolutionfoldpositive = fs_q_dst_necessary_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_necessary_one_convolutionfoldpositive_body_steps)) * fs_v_dst_necessary_one_convolutionfoldpositive) + (fs_s_dst_necessary_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_necessary_one_convolutionfoldpositive_body_steps = fs_r_dst_necessary_one_convolutionfoldpositive_body_steps + fs_a_dst_necessary_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_necessary_one_convolutionfoldnegative fs_v_dst_necessary_one_convolutionfoldnegative. ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_start. fs_h_dst_necessary_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_start. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_terminal. fs_h_dst_necessary_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_necessary_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_terminal. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_necessary_one_convolutionfoldnegative) + (dst_negative_sum_necessary_one_convolutionfold))) /\ forall fs_i_dst_necessary_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_necessary_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_necessary_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_necessary_one_convolutionfoldnegative_body_steps fs_r_dst_necessary_one_convolutionfoldnegative_body_steps fs_s_dst_necessary_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_necessary_one_convolutionfold)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_necessary_one_convolutionfold = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_necessary_one_convolutionfold) + (fs_a_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (fs_r_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_necessary_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_necessary_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative)) /\ exists fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_necessary_one_convolutionfoldnegative = fs_q_dst_necessary_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_necessary_one_convolutionfoldnegative_body_steps)) * fs_v_dst_necessary_one_convolutionfoldnegative) + (fs_s_dst_necessary_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_necessary_one_convolutionfoldnegative_body_steps = fs_r_dst_necessary_one_convolutionfoldnegative_body_steps + fs_a_dst_necessary_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_necessary_one_convolutionfoldresult ge_balance_negative_necessary_one_convolutionfoldresult. (((((2) = 2 * (ge_balance_positive_necessary_one_convolutionfoldresult) /\ (ge_balance_negative_necessary_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_necessary_one_convolutionfoldresultdecode. (((2) = 2 * ge_signed_half_necessary_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_necessary_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_necessary_one_convolutionfoldresult) = S ge_signed_half_necessary_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_necessary_one_convolutionfold) + ge_balance_negative_necessary_one_convolutionfoldresult = (dst_negative_sum_necessary_one_convolutionfold) + ge_balance_positive_necessary_one_convolutionfoldresult))))))))))))))) - 0060
specialize dirichlet_convolution_at_one_iff (F) - 0061
specialize dirichlet_convolution_at_one_iff (G) - 0062
specialize dirichlet_convolution_at_one_iff (x1) - 0063
specialize dirichlet_convolution_at_one_iff (x2) - 0064
specialize dirichlet_convolution_at_one_iff (2) - 0065
apply dirichlet_convolution_at_one_iff - 0066
exact ha_witness - 0067
exact hb_witness - 0068
cases hiff - 0069
have hp : exists sto_ap_necessary_one_product sto_an_necessary_one_product sto_bp_necessary_one_product sto_bn_necessary_one_product sto_cp_necessary_one_product sto_cn_necessary_one_product. (((((x1) = 2 * (sto_ap_necessary_one_product) /\ (sto_an_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productleft. (((x1) = 2 * ge_signed_half_necessary_one_productleft + 1 /\ (sto_ap_necessary_one_product) = 0) /\ (sto_an_necessary_one_product) = S ge_signed_half_necessary_one_productleft))) /\ ((((((x2) = 2 * (sto_bp_necessary_one_product) /\ (sto_bn_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productright. (((x2) = 2 * ge_signed_half_necessary_one_productright + 1 /\ (sto_bp_necessary_one_product) = 0) /\ (sto_bn_necessary_one_product) = S ge_signed_half_necessary_one_productright))) /\ ((((((2) = 2 * (sto_cp_necessary_one_product) /\ (sto_cn_necessary_one_product) = 0) \/ exists ge_signed_half_necessary_one_productoutput. (((2) = 2 * ge_signed_half_necessary_one_productoutput + 1 /\ (sto_cp_necessary_one_product) = 0) /\ (sto_cn_necessary_one_product) = S ge_signed_half_necessary_one_productoutput))) /\ ((sto_ap_necessary_one_product * sto_bp_necessary_one_product + sto_an_necessary_one_product * sto_bn_necessary_one_product) + sto_cn_necessary_one_product = (sto_ap_necessary_one_product * sto_bn_necessary_one_product + sto_an_necessary_one_product * sto_bp_necessary_one_product) + sto_cp_necessary_one_product)))))) - 0070
apply hiff_left - 0071
exact hc - 0072
have hu : (x1=2 /\ x2=2) \/ (x1=1 /\ x2=1) - 0073
specialize dirichlet_signed_unit_product_classification (x1) - 0074
specialize dirichlet_signed_unit_product_classification (x2) - 0075
apply dirichlet_signed_unit_product_classification - 0076
exact hp - 0077
specialize dirichlet_unit_at_one_from_value (F) - 0078
specialize dirichlet_unit_at_one_from_value (x1) - 0079
apply dirichlet_unit_at_one_from_value - 0080
exact ha_witness - 0081
cases hu - 0082
cases hu_left - 0083
left - 0084
exact hu_left_left - 0085
cases hu_right - 0086
right - 0087
exact hu_right_left