dirichlet_inverse_positive_criterion

Exact expanded first-order arithmetic statement

forall N F. (exists dst_positive_code_positive_criterion_input dst_positive_scale_positive_criterion_input dst_negative_code_positive_criterion_input dst_negative_scale_positive_criterion_input. (((F) = (((((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) * S ((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) + ((dst_positive_scale_positive_criterion_input) + (dst_positive_scale_positive_criterion_input))) + (((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)))) * S ((((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) * S ((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) + ((dst_positive_scale_positive_criterion_input) + (dst_positive_scale_positive_criterion_input))) + (((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)))) + ((((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input))) + (((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)))))) /\ (forall dst_index_positive_criterion_input. (exists pvs_le_gap_positive_criterion_inputdomain. pvs_le_gap_positive_criterion_inputdomain + (dst_index_positive_criterion_input) = (N)) -> exists dst_positive_positive_criterion_input dst_negative_positive_criterion_input dst_value_positive_criterion_input. ((((exists ff_h_pvs_positive_criterion_inputentrypositive. ff_h_pvs_positive_criterion_inputentrypositive + S (dst_positive_positive_criterion_input) = S ((S (dst_index_positive_criterion_input)) * dst_positive_scale_positive_criterion_input)) /\ exists ff_q_pvs_positive_criterion_inputentrypositive. dst_positive_code_positive_criterion_input = ff_q_pvs_positive_criterion_inputentrypositive * S ((S (dst_index_positive_criterion_input)) * dst_positive_scale_positive_criterion_input) + (dst_positive_positive_criterion_input))) /\ (((((exists ff_h_pvs_positive_criterion_inputentrynegative. ff_h_pvs_positive_criterion_inputentrynegative + S (dst_negative_positive_criterion_input) = S ((S (dst_index_positive_criterion_input)) * dst_negative_scale_positive_criterion_input)) /\ exists ff_q_pvs_positive_criterion_inputentrynegative. dst_negative_code_positive_criterion_input = ff_q_pvs_positive_criterion_inputentrynegative * S ((S (dst_index_positive_criterion_input)) * dst_negative_scale_positive_criterion_input) + (dst_negative_positive_criterion_input))) /\ (exists ge_balance_positive_positive_criterion_inputentryvalue ge_balance_negative_positive_criterion_inputentryvalue. (((((dst_value_positive_criterion_input) = 2 * (ge_balance_positive_positive_criterion_inputentryvalue) /\ (ge_balance_negative_positive_criterion_inputentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inputentryvaluedecode. (((dst_value_positive_criterion_input) = 2 * ge_signed_half_positive_criterion_inputentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inputentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inputentryvalue) = S ge_signed_half_positive_criterion_inputentryvaluedecode))) /\ ((dst_positive_positive_criterion_input) + ge_balance_negative_positive_criterion_inputentryvalue = (dst_negative_positive_criterion_input) + ge_balance_positive_positive_criterion_inputentryvalue))))))))) -> ~(N=0) -> (((exists G. (exists di_delta_positive_criterion_inverse. ((((exists dst_positive_code_positive_criterion_inversedeltatable dst_positive_scale_positive_criterion_inversedeltatable dst_negative_code_positive_criterion_inversedeltatable dst_negative_scale_positive_criterion_inversedeltatable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) * S ((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) + ((((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))))) /\ (forall dst_index_positive_criterion_inversedeltatable. (exists pvs_le_gap_positive_criterion_inversedeltatabledomain. pvs_le_gap_positive_criterion_inversedeltatabledomain + (dst_index_positive_criterion_inversedeltatable) = (N)) -> exists dst_positive_positive_criterion_inversedeltatable dst_negative_positive_criterion_inversedeltatable dst_value_positive_criterion_inversedeltatable. ((((exists ff_h_pvs_positive_criterion_inversedeltatableentrypositive. ff_h_pvs_positive_criterion_inversedeltatableentrypositive + S (dst_positive_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrypositive. dst_positive_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrypositive * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_positive_criterion_inversedeltatable))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltatableentrynegative. ff_h_pvs_positive_criterion_inversedeltatableentrynegative + S (dst_negative_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrynegative. dst_negative_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrynegative * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_positive_criterion_inversedeltatable))) /\ (exists ge_balance_positive_positive_criterion_inversedeltatableentryvalue ge_balance_negative_positive_criterion_inversedeltatableentryvalue. (((((dst_value_positive_criterion_inversedeltatable) = 2 * (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode. (((dst_value_positive_criterion_inversedeltatable) = 2 * ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = S ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltatable) + ge_balance_negative_positive_criterion_inversedeltatableentryvalue = (dst_negative_positive_criterion_inversedeltatable) + ge_balance_positive_positive_criterion_inversedeltatableentryvalue))))))))) /\ (forall du_index_positive_criterion_inversedelta du_value_positive_criterion_inversedelta. ~(du_index_positive_criterion_inversedelta=0) -> (exists pvs_le_gap_positive_criterion_inversedeltabound. pvs_le_gap_positive_criterion_inversedeltabound + (du_index_positive_criterion_inversedelta) = (N)) -> (exists dst_positive_code_positive_criterion_inversedeltaentry dst_positive_scale_positive_criterion_inversedeltaentry dst_negative_code_positive_criterion_inversedeltaentry dst_negative_scale_positive_criterion_inversedeltaentry dst_positive_positive_criterion_inversedeltaentry dst_negative_positive_criterion_inversedeltaentry. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) * S ((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) + ((((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrypositive. ff_h_pvs_positive_criterion_inversedeltaentrypositive + S (dst_positive_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrypositive. dst_positive_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrypositive * S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_positive_criterion_inversedeltaentry))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrynegative. ff_h_pvs_positive_criterion_inversedeltaentrynegative + S (dst_negative_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrynegative. dst_negative_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrynegative * S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_positive_criterion_inversedeltaentry))) /\ (exists ge_balance_positive_positive_criterion_inversedeltaentryvalue ge_balance_negative_positive_criterion_inversedeltaentryvalue. (((((du_value_positive_criterion_inversedelta) = 2 * (ge_balance_positive_positive_criterion_inversedeltaentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltaentryvaluedecode. (((du_value_positive_criterion_inversedelta) = 2 * ge_signed_half_positive_criterion_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = S ge_signed_half_positive_criterion_inversedeltaentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltaentry) + ge_balance_negative_positive_criterion_inversedeltaentryvalue = (dst_negative_positive_criterion_inversedeltaentry) + ge_balance_positive_positive_criterion_inversedeltaentryvalue))))))))) -> ((((du_index_positive_criterion_inversedelta)=1 -> (du_value_positive_criterion_inversedelta)=2) /\ (~((du_index_positive_criterion_inversedelta)=1) -> (du_value_positive_criterion_inversedelta)=0)))))) /\ (((((exists dst_positive_code_positive_criterion_inverseleftleft dst_positive_scale_positive_criterion_inverseleftleft dst_negative_code_positive_criterion_inverseleftleft dst_negative_scale_positive_criterion_inverseleftleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) + ((((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))))) /\ (forall dst_index_positive_criterion_inverseleftleft. (exists pvs_le_gap_positive_criterion_inverseleftleftdomain. pvs_le_gap_positive_criterion_inverseleftleftdomain + (dst_index_positive_criterion_inverseleftleft) = (N)) -> exists dst_positive_positive_criterion_inverseleftleft dst_negative_positive_criterion_inverseleftleft dst_value_positive_criterion_inverseleftleft. ((((exists ff_h_pvs_positive_criterion_inverseleftleftentrypositive. ff_h_pvs_positive_criterion_inverseleftleftentrypositive + S (dst_positive_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrypositive. dst_positive_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrypositive * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_positive_criterion_inverseleftleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftleftentrynegative. ff_h_pvs_positive_criterion_inverseleftleftentrynegative + S (dst_negative_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrynegative. dst_negative_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrynegative * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_positive_criterion_inverseleftleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftleftentryvalue ge_balance_negative_positive_criterion_inverseleftleftentryvalue. (((((dst_value_positive_criterion_inverseleftleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode. (((dst_value_positive_criterion_inverseleftleft) = 2 * ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = S ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftleft) + ge_balance_negative_positive_criterion_inverseleftleftentryvalue = (dst_negative_positive_criterion_inverseleftleft) + ge_balance_positive_positive_criterion_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftright dst_positive_scale_positive_criterion_inverseleftright dst_negative_code_positive_criterion_inverseleftright dst_negative_scale_positive_criterion_inverseleftright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) * S ((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) + ((((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))))) /\ (forall dst_index_positive_criterion_inverseleftright. (exists pvs_le_gap_positive_criterion_inverseleftrightdomain. pvs_le_gap_positive_criterion_inverseleftrightdomain + (dst_index_positive_criterion_inverseleftright) = (N)) -> exists dst_positive_positive_criterion_inverseleftright dst_negative_positive_criterion_inverseleftright dst_value_positive_criterion_inverseleftright. ((((exists ff_h_pvs_positive_criterion_inverseleftrightentrypositive. ff_h_pvs_positive_criterion_inverseleftrightentrypositive + S (dst_positive_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrypositive. dst_positive_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrypositive * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_positive_criterion_inverseleftright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftrightentrynegative. ff_h_pvs_positive_criterion_inverseleftrightentrynegative + S (dst_negative_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrynegative. dst_negative_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrynegative * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_positive_criterion_inverseleftright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftrightentryvalue ge_balance_negative_positive_criterion_inverseleftrightentryvalue. (((((dst_value_positive_criterion_inverseleftright) = 2 * (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode. (((dst_value_positive_criterion_inverseleftright) = 2 * ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = S ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftright) + ge_balance_negative_positive_criterion_inverseleftrightentryvalue = (dst_negative_positive_criterion_inverseleftright) + ge_balance_positive_positive_criterion_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverselefttable dst_positive_scale_positive_criterion_inverselefttable dst_negative_code_positive_criterion_inverselefttable dst_negative_scale_positive_criterion_inverselefttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) * S ((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) + ((((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))))) /\ (forall dst_index_positive_criterion_inverselefttable. (exists pvs_le_gap_positive_criterion_inverselefttabledomain. pvs_le_gap_positive_criterion_inverselefttabledomain + (dst_index_positive_criterion_inverselefttable) = (N)) -> exists dst_positive_positive_criterion_inverselefttable dst_negative_positive_criterion_inverselefttable dst_value_positive_criterion_inverselefttable. ((((exists ff_h_pvs_positive_criterion_inverselefttableentrypositive. ff_h_pvs_positive_criterion_inverselefttableentrypositive + S (dst_positive_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrypositive. dst_positive_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrypositive * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_positive_criterion_inverselefttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverselefttableentrynegative. ff_h_pvs_positive_criterion_inverselefttableentrynegative + S (dst_negative_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrynegative. dst_negative_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrynegative * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_positive_criterion_inverselefttable))) /\ (exists ge_balance_positive_positive_criterion_inverselefttableentryvalue ge_balance_negative_positive_criterion_inverselefttableentryvalue. (((((dst_value_positive_criterion_inverselefttable) = 2 * (ge_balance_positive_positive_criterion_inverselefttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverselefttableentryvaluedecode. (((dst_value_positive_criterion_inverselefttable) = 2 * ge_signed_half_positive_criterion_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = S ge_signed_half_positive_criterion_inverselefttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverselefttable) + ge_balance_negative_positive_criterion_inverselefttableentryvalue = (dst_negative_positive_criterion_inverselefttable) + ge_balance_positive_positive_criterion_inverselefttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseleft dc_output_positive_criterion_inverseleft. ~(dc_input_positive_criterion_inverseleft=0) -> (exists pvs_le_gap_positive_criterion_inverseleftdomain. pvs_le_gap_positive_criterion_inverseleftdomain + (dc_input_positive_criterion_inverseleft) = (N)) -> (exists dst_positive_code_positive_criterion_inverseleftlookup dst_positive_scale_positive_criterion_inverseleftlookup dst_negative_code_positive_criterion_inverseleftlookup dst_negative_scale_positive_criterion_inverseleftlookup dst_positive_positive_criterion_inverseleftlookup dst_negative_positive_criterion_inverseleftlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) + ((((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookuppositive. ff_h_pvs_positive_criterion_inverseleftlookuppositive + S (dst_positive_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookuppositive. dst_positive_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookuppositive * S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_positive_criterion_inverseleftlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookupnegative. ff_h_pvs_positive_criterion_inverseleftlookupnegative + S (dst_negative_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookupnegative. dst_negative_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookupnegative * S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_positive_criterion_inverseleftlookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftlookupvalue ge_balance_negative_positive_criterion_inverseleftlookupvalue. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftlookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftlookupvaluedecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = S ge_signed_half_positive_criterion_inverseleftlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftlookup) + ge_balance_negative_positive_criterion_inverseleftlookupvalue = (dst_negative_positive_criterion_inverseleftlookup) + ge_balance_positive_positive_criterion_inverseleftlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseleft)=0)) /\ (exists dc_mask_positive_criterion_inverseleftvalue. ((((exists dst_positive_code_positive_criterion_inverseleftvaluemasktable dst_positive_scale_positive_criterion_inverseleftvaluemasktable dst_negative_code_positive_criterion_inverseleftvaluemasktable dst_negative_scale_positive_criterion_inverseleftvaluemasktable. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverseleftvaluemasktable. (exists pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain. pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain + (dst_index_positive_criterion_inverseleftvaluemasktable) = (dc_input_positive_criterion_inverseleft)) -> exists dst_positive_positive_criterion_inverseleftvaluemasktable dst_negative_positive_criterion_inverseleftvaluemasktable dst_value_positive_criterion_inverseleftvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_positive_criterion_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_positive_criterion_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasktable) + ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue = (dst_negative_positive_criterion_inverseleftvaluemasktable) + ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverseleftvaluemask dc_value_positive_criterion_inverseleftvaluemask. (exists pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain. pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain + (dc_index_positive_criterion_inverseleftvaluemask) = (dc_input_positive_criterion_inverseleft)) -> (exists dst_positive_code_positive_criterion_inverseleftvaluemasklookup dst_positive_scale_positive_criterion_inverseleftvaluemasklookup dst_negative_code_positive_criterion_inverseleftvaluemasklookup dst_negative_scale_positive_criterion_inverseleftvaluemasklookup dst_positive_positive_criterion_inverseleftvaluemasklookup dst_negative_positive_criterion_inverseleftvaluemasklookup. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive + S (dst_positive_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive. dst_positive_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_positive_criterion_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative + S (dst_negative_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative. dst_negative_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_positive_criterion_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue. (((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasklookup) + ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue = (dst_negative_positive_criterion_inverseleftvaluemasklookup) + ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverseleftvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverseleftvaluemaskentry dc_left_positive_criterion_inverseleftvaluemaskentry dc_right_positive_criterion_inverseleftvaluemaskentry. (((dc_input_positive_criterion_inverseleft)=(dc_index_positive_criterion_inverseleftvaluemask)*dc_quotient_positive_criterion_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft dst_positive_positive_criterion_inverseleftvaluemaskentryleft dst_negative_positive_criterion_inverseleftvaluemaskentryleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_positive_criterion_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_positive_criterion_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryright dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright dst_negative_code_positive_criterion_inverseleftvaluemaskentryright dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright dst_positive_positive_criterion_inverseleftvaluemaskentryright dst_negative_positive_criterion_inverseleftvaluemaskentryright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_positive_criterion_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_positive_criterion_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverseleftvaluemaskentryproduct sto_an_positive_criterion_inverseleftvaluemaskentryproduct sto_bp_positive_criterion_inverseleftvaluemaskentryproduct sto_bn_positive_criterion_inverseleftvaluemaskentryproduct sto_cp_positive_criterion_inverseleftvaluemaskentryproduct sto_cn_positive_criterion_inverseleftvaluemaskentryproduct. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cn_positive_criterion_inverseleftvaluemaskentryproduct = (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cp_positive_criterion_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseleft) = (dc_index_positive_criterion_inverseleftvaluemask) * pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverseleftvaluefold dst_positive_scale_positive_criterion_inverseleftvaluefold dst_negative_code_positive_criterion_inverseleftvaluefold dst_negative_scale_positive_criterion_inverseleftvaluefold dst_positive_sum_positive_criterion_inverseleftvaluefold dst_negative_sum_positive_criterion_inverseleftvaluefold. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldpositive fs_v_dst_positive_criterion_inverseleftvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldnegative fs_v_dst_positive_criterion_inverseleftvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluefoldresult ge_balance_negative_positive_criterion_inverseleftvaluefoldresult. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = S ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverseleftvaluefold) + ge_balance_negative_positive_criterion_inverseleftvaluefoldresult = (dst_negative_sum_positive_criterion_inverseleftvaluefold) + ge_balance_positive_positive_criterion_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightleft dst_positive_scale_positive_criterion_inverserightleft dst_negative_code_positive_criterion_inverserightleft dst_negative_scale_positive_criterion_inverserightleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) * S ((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) + ((((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))))) /\ (forall dst_index_positive_criterion_inverserightleft. (exists pvs_le_gap_positive_criterion_inverserightleftdomain. pvs_le_gap_positive_criterion_inverserightleftdomain + (dst_index_positive_criterion_inverserightleft) = (N)) -> exists dst_positive_positive_criterion_inverserightleft dst_negative_positive_criterion_inverserightleft dst_value_positive_criterion_inverserightleft. ((((exists ff_h_pvs_positive_criterion_inverserightleftentrypositive. ff_h_pvs_positive_criterion_inverserightleftentrypositive + S (dst_positive_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrypositive. dst_positive_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrypositive * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_positive_criterion_inverserightleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightleftentrynegative. ff_h_pvs_positive_criterion_inverserightleftentrynegative + S (dst_negative_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrynegative. dst_negative_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrynegative * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_positive_criterion_inverserightleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightleftentryvalue ge_balance_negative_positive_criterion_inverserightleftentryvalue. (((((dst_value_positive_criterion_inverserightleft) = 2 * (ge_balance_positive_positive_criterion_inverserightleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightleftentryvaluedecode. (((dst_value_positive_criterion_inverserightleft) = 2 * ge_signed_half_positive_criterion_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = S ge_signed_half_positive_criterion_inverserightleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightleft) + ge_balance_negative_positive_criterion_inverserightleftentryvalue = (dst_negative_positive_criterion_inverserightleft) + ge_balance_positive_positive_criterion_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightright dst_positive_scale_positive_criterion_inverserightright dst_negative_code_positive_criterion_inverserightright dst_negative_scale_positive_criterion_inverserightright. (((F) = (((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) * S ((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) + ((((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))))) /\ (forall dst_index_positive_criterion_inverserightright. (exists pvs_le_gap_positive_criterion_inverserightrightdomain. pvs_le_gap_positive_criterion_inverserightrightdomain + (dst_index_positive_criterion_inverserightright) = (N)) -> exists dst_positive_positive_criterion_inverserightright dst_negative_positive_criterion_inverserightright dst_value_positive_criterion_inverserightright. ((((exists ff_h_pvs_positive_criterion_inverserightrightentrypositive. ff_h_pvs_positive_criterion_inverserightrightentrypositive + S (dst_positive_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrypositive. dst_positive_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrypositive * S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_positive_criterion_inverserightright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightrightentrynegative. ff_h_pvs_positive_criterion_inverserightrightentrynegative + S (dst_negative_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrynegative. dst_negative_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrynegative * S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_positive_criterion_inverserightright))) /\ (exists ge_balance_positive_positive_criterion_inverserightrightentryvalue ge_balance_negative_positive_criterion_inverserightrightentryvalue. (((((dst_value_positive_criterion_inverserightright) = 2 * (ge_balance_positive_positive_criterion_inverserightrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightrightentryvaluedecode. (((dst_value_positive_criterion_inverserightright) = 2 * ge_signed_half_positive_criterion_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = S ge_signed_half_positive_criterion_inverserightrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightright) + ge_balance_negative_positive_criterion_inverserightrightentryvalue = (dst_negative_positive_criterion_inverserightright) + ge_balance_positive_positive_criterion_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserighttable dst_positive_scale_positive_criterion_inverserighttable dst_negative_code_positive_criterion_inverserighttable dst_negative_scale_positive_criterion_inverserighttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) * S ((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) + ((((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))))) /\ (forall dst_index_positive_criterion_inverserighttable. (exists pvs_le_gap_positive_criterion_inverserighttabledomain. pvs_le_gap_positive_criterion_inverserighttabledomain + (dst_index_positive_criterion_inverserighttable) = (N)) -> exists dst_positive_positive_criterion_inverserighttable dst_negative_positive_criterion_inverserighttable dst_value_positive_criterion_inverserighttable. ((((exists ff_h_pvs_positive_criterion_inverserighttableentrypositive. ff_h_pvs_positive_criterion_inverserighttableentrypositive + S (dst_positive_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrypositive. dst_positive_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrypositive * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_positive_criterion_inverserighttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserighttableentrynegative. ff_h_pvs_positive_criterion_inverserighttableentrynegative + S (dst_negative_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrynegative. dst_negative_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrynegative * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_positive_criterion_inverserighttable))) /\ (exists ge_balance_positive_positive_criterion_inverserighttableentryvalue ge_balance_negative_positive_criterion_inverserighttableentryvalue. (((((dst_value_positive_criterion_inverserighttable) = 2 * (ge_balance_positive_positive_criterion_inverserighttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserighttableentryvaluedecode. (((dst_value_positive_criterion_inverserighttable) = 2 * ge_signed_half_positive_criterion_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = S ge_signed_half_positive_criterion_inverserighttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserighttable) + ge_balance_negative_positive_criterion_inverserighttableentryvalue = (dst_negative_positive_criterion_inverserighttable) + ge_balance_positive_positive_criterion_inverserighttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseright dc_output_positive_criterion_inverseright. ~(dc_input_positive_criterion_inverseright=0) -> (exists pvs_le_gap_positive_criterion_inverserightdomain. pvs_le_gap_positive_criterion_inverserightdomain + (dc_input_positive_criterion_inverseright) = (N)) -> (exists dst_positive_code_positive_criterion_inverserightlookup dst_positive_scale_positive_criterion_inverserightlookup dst_negative_code_positive_criterion_inverserightlookup dst_negative_scale_positive_criterion_inverserightlookup dst_positive_positive_criterion_inverserightlookup dst_negative_positive_criterion_inverserightlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) * S ((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) + ((((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookuppositive. ff_h_pvs_positive_criterion_inverserightlookuppositive + S (dst_positive_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookuppositive. dst_positive_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookuppositive * S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_positive_criterion_inverserightlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookupnegative. ff_h_pvs_positive_criterion_inverserightlookupnegative + S (dst_negative_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookupnegative. dst_negative_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookupnegative * S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_positive_criterion_inverserightlookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightlookupvalue ge_balance_negative_positive_criterion_inverserightlookupvalue. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightlookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightlookupvaluedecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = S ge_signed_half_positive_criterion_inverserightlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightlookup) + ge_balance_negative_positive_criterion_inverserightlookupvalue = (dst_negative_positive_criterion_inverserightlookup) + ge_balance_positive_positive_criterion_inverserightlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseright)=0)) /\ (exists dc_mask_positive_criterion_inverserightvalue. ((((exists dst_positive_code_positive_criterion_inverserightvaluemasktable dst_positive_scale_positive_criterion_inverserightvaluemasktable dst_negative_code_positive_criterion_inverserightvaluemasktable dst_negative_scale_positive_criterion_inverserightvaluemasktable. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverserightvaluemasktable. (exists pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain. pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain + (dst_index_positive_criterion_inverserightvaluemasktable) = (dc_input_positive_criterion_inverseright)) -> exists dst_positive_positive_criterion_inverserightvaluemasktable dst_negative_positive_criterion_inverserightvaluemasktable dst_value_positive_criterion_inverserightvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_positive_criterion_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_positive_criterion_inverserightvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasktable) + ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue = (dst_negative_positive_criterion_inverserightvaluemasktable) + ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverserightvaluemask dc_value_positive_criterion_inverserightvaluemask. (exists pvs_le_gap_positive_criterion_inverserightvaluemaskdomain. pvs_le_gap_positive_criterion_inverserightvaluemaskdomain + (dc_index_positive_criterion_inverserightvaluemask) = (dc_input_positive_criterion_inverseright)) -> (exists dst_positive_code_positive_criterion_inverserightvaluemasklookup dst_positive_scale_positive_criterion_inverserightvaluemasklookup dst_negative_code_positive_criterion_inverserightvaluemasklookup dst_negative_scale_positive_criterion_inverserightvaluemasklookup dst_positive_positive_criterion_inverserightvaluemasklookup dst_negative_positive_criterion_inverserightvaluemasklookup. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive + S (dst_positive_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive. dst_positive_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_positive_criterion_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative + S (dst_negative_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative. dst_negative_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_positive_criterion_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue. (((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasklookup) + ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue = (dst_negative_positive_criterion_inverserightvaluemasklookup) + ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverserightvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverserightvaluemaskentry dc_left_positive_criterion_inverserightvaluemaskentry dc_right_positive_criterion_inverserightvaluemaskentry. (((dc_input_positive_criterion_inverseright)=(dc_index_positive_criterion_inverserightvaluemask)*dc_quotient_positive_criterion_inverserightvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryleft dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft dst_negative_code_positive_criterion_inverserightvaluemaskentryleft dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft dst_positive_positive_criterion_inverserightvaluemaskentryleft dst_negative_positive_criterion_inverserightvaluemaskentryleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_positive_criterion_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_positive_criterion_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryright dst_positive_scale_positive_criterion_inverserightvaluemaskentryright dst_negative_code_positive_criterion_inverserightvaluemaskentryright dst_negative_scale_positive_criterion_inverserightvaluemaskentryright dst_positive_positive_criterion_inverserightvaluemaskentryright dst_negative_positive_criterion_inverserightvaluemaskentryright. (((F) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_positive_criterion_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_positive_criterion_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryright) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryright) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverserightvaluemaskentryproduct sto_an_positive_criterion_inverserightvaluemaskentryproduct sto_bp_positive_criterion_inverserightvaluemaskentryproduct sto_bn_positive_criterion_inverserightvaluemaskentryproduct sto_cp_positive_criterion_inverserightvaluemaskentryproduct sto_cn_positive_criterion_inverserightvaluemaskentryproduct. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct) + sto_cn_positive_criterion_inverserightvaluemaskentryproduct = (sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct) + sto_cp_positive_criterion_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverserightvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseright) = (dc_index_positive_criterion_inverserightvaluemask) * pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverserightvaluefold dst_positive_scale_positive_criterion_inverserightvaluefold dst_negative_code_positive_criterion_inverserightvaluefold dst_negative_scale_positive_criterion_inverserightvaluefold dst_positive_sum_positive_criterion_inverserightvaluefold dst_negative_sum_positive_criterion_inverserightvaluefold. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) + ((((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldpositive fs_v_dst_positive_criterion_inverserightvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldnegative fs_v_dst_positive_criterion_inverserightvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluefoldresult ge_balance_negative_positive_criterion_inverserightvaluefoldresult. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = S ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverserightvaluefold) + ge_balance_negative_positive_criterion_inverserightvaluefoldresult = (dst_negative_sum_positive_criterion_inverserightvaluefold) + ge_balance_positive_positive_criterion_inverserightvaluefoldresult))))))))))))))))))))))))) -> ((exists dst_positive_code_positive_criterion_unitpositive dst_positive_scale_positive_criterion_unitpositive dst_negative_code_positive_criterion_unitpositive dst_negative_scale_positive_criterion_unitpositive dst_positive_positive_criterion_unitpositive dst_negative_positive_criterion_unitpositive. (((F) = (((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) * S ((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) + ((((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivepositive. ff_h_pvs_positive_criterion_unitpositivepositive + S (dst_positive_positive_criterion_unitpositive) = S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivepositive. dst_positive_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_positive_criterion_unitpositive))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivenegative. ff_h_pvs_positive_criterion_unitpositivenegative + S (dst_negative_positive_criterion_unitpositive) = S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivenegative. dst_negative_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_positive_criterion_unitpositive))) /\ (exists ge_balance_positive_positive_criterion_unitpositivevalue ge_balance_negative_positive_criterion_unitpositivevalue. (((((2) = 2 * (ge_balance_positive_positive_criterion_unitpositivevalue) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitpositivevaluedecode. (((2) = 2 * ge_signed_half_positive_criterion_unitpositivevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitpositivevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = S ge_signed_half_positive_criterion_unitpositivevaluedecode))) /\ ((dst_positive_positive_criterion_unitpositive) + ge_balance_negative_positive_criterion_unitpositivevalue = (dst_negative_positive_criterion_unitpositive) + ge_balance_positive_positive_criterion_unitpositivevalue))))))))) \/ (exists dst_positive_code_positive_criterion_unitnegative dst_positive_scale_positive_criterion_unitnegative dst_negative_code_positive_criterion_unitnegative dst_negative_scale_positive_criterion_unitnegative dst_positive_positive_criterion_unitnegative dst_negative_positive_criterion_unitnegative. (((F) = (((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) * S ((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) + ((((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativepositive. ff_h_pvs_positive_criterion_unitnegativepositive + S (dst_positive_positive_criterion_unitnegative) = S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativepositive. dst_positive_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_positive_criterion_unitnegative))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativenegative. ff_h_pvs_positive_criterion_unitnegativenegative + S (dst_negative_positive_criterion_unitnegative) = S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativenegative. dst_negative_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_positive_criterion_unitnegative))) /\ (exists ge_balance_positive_positive_criterion_unitnegativevalue ge_balance_negative_positive_criterion_unitnegativevalue. (((((1) = 2 * (ge_balance_positive_positive_criterion_unitnegativevalue) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitnegativevaluedecode. (((1) = 2 * ge_signed_half_positive_criterion_unitnegativevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitnegativevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = S ge_signed_half_positive_criterion_unitnegativevaluedecode))) /\ ((dst_positive_positive_criterion_unitnegative) + ge_balance_negative_positive_criterion_unitnegativevalue = (dst_negative_positive_criterion_unitnegative) + ge_balance_positive_positive_criterion_unitnegativevalue))))))))))) /\ (((exists dst_positive_code_positive_criterion_unitpositive dst_positive_scale_positive_criterion_unitpositive dst_negative_code_positive_criterion_unitpositive dst_negative_scale_positive_criterion_unitpositive dst_positive_positive_criterion_unitpositive dst_negative_positive_criterion_unitpositive. (((F) = (((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) * S ((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) + ((((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivepositive. ff_h_pvs_positive_criterion_unitpositivepositive + S (dst_positive_positive_criterion_unitpositive) = S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivepositive. dst_positive_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_positive_criterion_unitpositive))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivenegative. ff_h_pvs_positive_criterion_unitpositivenegative + S (dst_negative_positive_criterion_unitpositive) = S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivenegative. dst_negative_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_positive_criterion_unitpositive))) /\ (exists ge_balance_positive_positive_criterion_unitpositivevalue ge_balance_negative_positive_criterion_unitpositivevalue. (((((2) = 2 * (ge_balance_positive_positive_criterion_unitpositivevalue) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitpositivevaluedecode. (((2) = 2 * ge_signed_half_positive_criterion_unitpositivevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitpositivevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = S ge_signed_half_positive_criterion_unitpositivevaluedecode))) /\ ((dst_positive_positive_criterion_unitpositive) + ge_balance_negative_positive_criterion_unitpositivevalue = (dst_negative_positive_criterion_unitpositive) + ge_balance_positive_positive_criterion_unitpositivevalue))))))))) \/ (exists dst_positive_code_positive_criterion_unitnegative dst_positive_scale_positive_criterion_unitnegative dst_negative_code_positive_criterion_unitnegative dst_negative_scale_positive_criterion_unitnegative dst_positive_positive_criterion_unitnegative dst_negative_positive_criterion_unitnegative. (((F) = (((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) * S ((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) + ((((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativepositive. ff_h_pvs_positive_criterion_unitnegativepositive + S (dst_positive_positive_criterion_unitnegative) = S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativepositive. dst_positive_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_positive_criterion_unitnegative))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativenegative. ff_h_pvs_positive_criterion_unitnegativenegative + S (dst_negative_positive_criterion_unitnegative) = S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativenegative. dst_negative_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_positive_criterion_unitnegative))) /\ (exists ge_balance_positive_positive_criterion_unitnegativevalue ge_balance_negative_positive_criterion_unitnegativevalue. (((((1) = 2 * (ge_balance_positive_positive_criterion_unitnegativevalue) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitnegativevaluedecode. (((1) = 2 * ge_signed_half_positive_criterion_unitnegativevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitnegativevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = S ge_signed_half_positive_criterion_unitnegativevaluedecode))) /\ ((dst_positive_positive_criterion_unitnegative) + ge_balance_negative_positive_criterion_unitnegativevalue = (dst_negative_positive_criterion_unitnegative) + ge_balance_positive_positive_criterion_unitnegativevalue)))))))))) -> exists G. (exists di_delta_positive_criterion_inverse. ((((exists dst_positive_code_positive_criterion_inversedeltatable dst_positive_scale_positive_criterion_inversedeltatable dst_negative_code_positive_criterion_inversedeltatable dst_negative_scale_positive_criterion_inversedeltatable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) * S ((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) + ((((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))))) /\ (forall dst_index_positive_criterion_inversedeltatable. (exists pvs_le_gap_positive_criterion_inversedeltatabledomain. pvs_le_gap_positive_criterion_inversedeltatabledomain + (dst_index_positive_criterion_inversedeltatable) = (N)) -> exists dst_positive_positive_criterion_inversedeltatable dst_negative_positive_criterion_inversedeltatable dst_value_positive_criterion_inversedeltatable. ((((exists ff_h_pvs_positive_criterion_inversedeltatableentrypositive. ff_h_pvs_positive_criterion_inversedeltatableentrypositive + S (dst_positive_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrypositive. dst_positive_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrypositive * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_positive_criterion_inversedeltatable))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltatableentrynegative. ff_h_pvs_positive_criterion_inversedeltatableentrynegative + S (dst_negative_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrynegative. dst_negative_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrynegative * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_positive_criterion_inversedeltatable))) /\ (exists ge_balance_positive_positive_criterion_inversedeltatableentryvalue ge_balance_negative_positive_criterion_inversedeltatableentryvalue. (((((dst_value_positive_criterion_inversedeltatable) = 2 * (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode. (((dst_value_positive_criterion_inversedeltatable) = 2 * ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = S ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltatable) + ge_balance_negative_positive_criterion_inversedeltatableentryvalue = (dst_negative_positive_criterion_inversedeltatable) + ge_balance_positive_positive_criterion_inversedeltatableentryvalue))))))))) /\ (forall du_index_positive_criterion_inversedelta du_value_positive_criterion_inversedelta. ~(du_index_positive_criterion_inversedelta=0) -> (exists pvs_le_gap_positive_criterion_inversedeltabound. pvs_le_gap_positive_criterion_inversedeltabound + (du_index_positive_criterion_inversedelta) = (N)) -> (exists dst_positive_code_positive_criterion_inversedeltaentry dst_positive_scale_positive_criterion_inversedeltaentry dst_negative_code_positive_criterion_inversedeltaentry dst_negative_scale_positive_criterion_inversedeltaentry dst_positive_positive_criterion_inversedeltaentry dst_negative_positive_criterion_inversedeltaentry. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) * S ((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) + ((((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrypositive. ff_h_pvs_positive_criterion_inversedeltaentrypositive + S (dst_positive_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrypositive. dst_positive_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrypositive * S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_positive_criterion_inversedeltaentry))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrynegative. ff_h_pvs_positive_criterion_inversedeltaentrynegative + S (dst_negative_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrynegative. dst_negative_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrynegative * S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_positive_criterion_inversedeltaentry))) /\ (exists ge_balance_positive_positive_criterion_inversedeltaentryvalue ge_balance_negative_positive_criterion_inversedeltaentryvalue. (((((du_value_positive_criterion_inversedelta) = 2 * (ge_balance_positive_positive_criterion_inversedeltaentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltaentryvaluedecode. (((du_value_positive_criterion_inversedelta) = 2 * ge_signed_half_positive_criterion_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = S ge_signed_half_positive_criterion_inversedeltaentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltaentry) + ge_balance_negative_positive_criterion_inversedeltaentryvalue = (dst_negative_positive_criterion_inversedeltaentry) + ge_balance_positive_positive_criterion_inversedeltaentryvalue))))))))) -> ((((du_index_positive_criterion_inversedelta)=1 -> (du_value_positive_criterion_inversedelta)=2) /\ (~((du_index_positive_criterion_inversedelta)=1) -> (du_value_positive_criterion_inversedelta)=0)))))) /\ (((((exists dst_positive_code_positive_criterion_inverseleftleft dst_positive_scale_positive_criterion_inverseleftleft dst_negative_code_positive_criterion_inverseleftleft dst_negative_scale_positive_criterion_inverseleftleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) + ((((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))))) /\ (forall dst_index_positive_criterion_inverseleftleft. (exists pvs_le_gap_positive_criterion_inverseleftleftdomain. pvs_le_gap_positive_criterion_inverseleftleftdomain + (dst_index_positive_criterion_inverseleftleft) = (N)) -> exists dst_positive_positive_criterion_inverseleftleft dst_negative_positive_criterion_inverseleftleft dst_value_positive_criterion_inverseleftleft. ((((exists ff_h_pvs_positive_criterion_inverseleftleftentrypositive. ff_h_pvs_positive_criterion_inverseleftleftentrypositive + S (dst_positive_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrypositive. dst_positive_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrypositive * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_positive_criterion_inverseleftleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftleftentrynegative. ff_h_pvs_positive_criterion_inverseleftleftentrynegative + S (dst_negative_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrynegative. dst_negative_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrynegative * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_positive_criterion_inverseleftleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftleftentryvalue ge_balance_negative_positive_criterion_inverseleftleftentryvalue. (((((dst_value_positive_criterion_inverseleftleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode. (((dst_value_positive_criterion_inverseleftleft) = 2 * ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = S ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftleft) + ge_balance_negative_positive_criterion_inverseleftleftentryvalue = (dst_negative_positive_criterion_inverseleftleft) + ge_balance_positive_positive_criterion_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftright dst_positive_scale_positive_criterion_inverseleftright dst_negative_code_positive_criterion_inverseleftright dst_negative_scale_positive_criterion_inverseleftright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) * S ((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) + ((((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))))) /\ (forall dst_index_positive_criterion_inverseleftright. (exists pvs_le_gap_positive_criterion_inverseleftrightdomain. pvs_le_gap_positive_criterion_inverseleftrightdomain + (dst_index_positive_criterion_inverseleftright) = (N)) -> exists dst_positive_positive_criterion_inverseleftright dst_negative_positive_criterion_inverseleftright dst_value_positive_criterion_inverseleftright. ((((exists ff_h_pvs_positive_criterion_inverseleftrightentrypositive. ff_h_pvs_positive_criterion_inverseleftrightentrypositive + S (dst_positive_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrypositive. dst_positive_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrypositive * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_positive_criterion_inverseleftright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftrightentrynegative. ff_h_pvs_positive_criterion_inverseleftrightentrynegative + S (dst_negative_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrynegative. dst_negative_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrynegative * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_positive_criterion_inverseleftright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftrightentryvalue ge_balance_negative_positive_criterion_inverseleftrightentryvalue. (((((dst_value_positive_criterion_inverseleftright) = 2 * (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode. (((dst_value_positive_criterion_inverseleftright) = 2 * ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = S ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftright) + ge_balance_negative_positive_criterion_inverseleftrightentryvalue = (dst_negative_positive_criterion_inverseleftright) + ge_balance_positive_positive_criterion_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverselefttable dst_positive_scale_positive_criterion_inverselefttable dst_negative_code_positive_criterion_inverselefttable dst_negative_scale_positive_criterion_inverselefttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) * S ((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) + ((((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))))) /\ (forall dst_index_positive_criterion_inverselefttable. (exists pvs_le_gap_positive_criterion_inverselefttabledomain. pvs_le_gap_positive_criterion_inverselefttabledomain + (dst_index_positive_criterion_inverselefttable) = (N)) -> exists dst_positive_positive_criterion_inverselefttable dst_negative_positive_criterion_inverselefttable dst_value_positive_criterion_inverselefttable. ((((exists ff_h_pvs_positive_criterion_inverselefttableentrypositive. ff_h_pvs_positive_criterion_inverselefttableentrypositive + S (dst_positive_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrypositive. dst_positive_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrypositive * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_positive_criterion_inverselefttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverselefttableentrynegative. ff_h_pvs_positive_criterion_inverselefttableentrynegative + S (dst_negative_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrynegative. dst_negative_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrynegative * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_positive_criterion_inverselefttable))) /\ (exists ge_balance_positive_positive_criterion_inverselefttableentryvalue ge_balance_negative_positive_criterion_inverselefttableentryvalue. (((((dst_value_positive_criterion_inverselefttable) = 2 * (ge_balance_positive_positive_criterion_inverselefttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverselefttableentryvaluedecode. (((dst_value_positive_criterion_inverselefttable) = 2 * ge_signed_half_positive_criterion_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = S ge_signed_half_positive_criterion_inverselefttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverselefttable) + ge_balance_negative_positive_criterion_inverselefttableentryvalue = (dst_negative_positive_criterion_inverselefttable) + ge_balance_positive_positive_criterion_inverselefttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseleft dc_output_positive_criterion_inverseleft. ~(dc_input_positive_criterion_inverseleft=0) -> (exists pvs_le_gap_positive_criterion_inverseleftdomain. pvs_le_gap_positive_criterion_inverseleftdomain + (dc_input_positive_criterion_inverseleft) = (N)) -> (exists dst_positive_code_positive_criterion_inverseleftlookup dst_positive_scale_positive_criterion_inverseleftlookup dst_negative_code_positive_criterion_inverseleftlookup dst_negative_scale_positive_criterion_inverseleftlookup dst_positive_positive_criterion_inverseleftlookup dst_negative_positive_criterion_inverseleftlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) + ((((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookuppositive. ff_h_pvs_positive_criterion_inverseleftlookuppositive + S (dst_positive_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookuppositive. dst_positive_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookuppositive * S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_positive_criterion_inverseleftlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookupnegative. ff_h_pvs_positive_criterion_inverseleftlookupnegative + S (dst_negative_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookupnegative. dst_negative_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookupnegative * S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_positive_criterion_inverseleftlookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftlookupvalue ge_balance_negative_positive_criterion_inverseleftlookupvalue. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftlookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftlookupvaluedecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = S ge_signed_half_positive_criterion_inverseleftlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftlookup) + ge_balance_negative_positive_criterion_inverseleftlookupvalue = (dst_negative_positive_criterion_inverseleftlookup) + ge_balance_positive_positive_criterion_inverseleftlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseleft)=0)) /\ (exists dc_mask_positive_criterion_inverseleftvalue. ((((exists dst_positive_code_positive_criterion_inverseleftvaluemasktable dst_positive_scale_positive_criterion_inverseleftvaluemasktable dst_negative_code_positive_criterion_inverseleftvaluemasktable dst_negative_scale_positive_criterion_inverseleftvaluemasktable. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverseleftvaluemasktable. (exists pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain. pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain + (dst_index_positive_criterion_inverseleftvaluemasktable) = (dc_input_positive_criterion_inverseleft)) -> exists dst_positive_positive_criterion_inverseleftvaluemasktable dst_negative_positive_criterion_inverseleftvaluemasktable dst_value_positive_criterion_inverseleftvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_positive_criterion_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_positive_criterion_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasktable) + ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue = (dst_negative_positive_criterion_inverseleftvaluemasktable) + ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverseleftvaluemask dc_value_positive_criterion_inverseleftvaluemask. (exists pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain. pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain + (dc_index_positive_criterion_inverseleftvaluemask) = (dc_input_positive_criterion_inverseleft)) -> (exists dst_positive_code_positive_criterion_inverseleftvaluemasklookup dst_positive_scale_positive_criterion_inverseleftvaluemasklookup dst_negative_code_positive_criterion_inverseleftvaluemasklookup dst_negative_scale_positive_criterion_inverseleftvaluemasklookup dst_positive_positive_criterion_inverseleftvaluemasklookup dst_negative_positive_criterion_inverseleftvaluemasklookup. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive + S (dst_positive_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive. dst_positive_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_positive_criterion_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative + S (dst_negative_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative. dst_negative_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_positive_criterion_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue. (((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasklookup) + ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue = (dst_negative_positive_criterion_inverseleftvaluemasklookup) + ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverseleftvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverseleftvaluemaskentry dc_left_positive_criterion_inverseleftvaluemaskentry dc_right_positive_criterion_inverseleftvaluemaskentry. (((dc_input_positive_criterion_inverseleft)=(dc_index_positive_criterion_inverseleftvaluemask)*dc_quotient_positive_criterion_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft dst_positive_positive_criterion_inverseleftvaluemaskentryleft dst_negative_positive_criterion_inverseleftvaluemaskentryleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_positive_criterion_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_positive_criterion_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryright dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright dst_negative_code_positive_criterion_inverseleftvaluemaskentryright dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright dst_positive_positive_criterion_inverseleftvaluemaskentryright dst_negative_positive_criterion_inverseleftvaluemaskentryright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_positive_criterion_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_positive_criterion_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverseleftvaluemaskentryproduct sto_an_positive_criterion_inverseleftvaluemaskentryproduct sto_bp_positive_criterion_inverseleftvaluemaskentryproduct sto_bn_positive_criterion_inverseleftvaluemaskentryproduct sto_cp_positive_criterion_inverseleftvaluemaskentryproduct sto_cn_positive_criterion_inverseleftvaluemaskentryproduct. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cn_positive_criterion_inverseleftvaluemaskentryproduct = (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cp_positive_criterion_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseleft) = (dc_index_positive_criterion_inverseleftvaluemask) * pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverseleftvaluefold dst_positive_scale_positive_criterion_inverseleftvaluefold dst_negative_code_positive_criterion_inverseleftvaluefold dst_negative_scale_positive_criterion_inverseleftvaluefold dst_positive_sum_positive_criterion_inverseleftvaluefold dst_negative_sum_positive_criterion_inverseleftvaluefold. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldpositive fs_v_dst_positive_criterion_inverseleftvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldnegative fs_v_dst_positive_criterion_inverseleftvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluefoldresult ge_balance_negative_positive_criterion_inverseleftvaluefoldresult. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = S ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverseleftvaluefold) + ge_balance_negative_positive_criterion_inverseleftvaluefoldresult = (dst_negative_sum_positive_criterion_inverseleftvaluefold) + ge_balance_positive_positive_criterion_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightleft dst_positive_scale_positive_criterion_inverserightleft dst_negative_code_positive_criterion_inverserightleft dst_negative_scale_positive_criterion_inverserightleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) * S ((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) + ((((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))))) /\ (forall dst_index_positive_criterion_inverserightleft. (exists pvs_le_gap_positive_criterion_inverserightleftdomain. pvs_le_gap_positive_criterion_inverserightleftdomain + (dst_index_positive_criterion_inverserightleft) = (N)) -> exists dst_positive_positive_criterion_inverserightleft dst_negative_positive_criterion_inverserightleft dst_value_positive_criterion_inverserightleft. ((((exists ff_h_pvs_positive_criterion_inverserightleftentrypositive. ff_h_pvs_positive_criterion_inverserightleftentrypositive + S (dst_positive_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrypositive. dst_positive_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrypositive * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_positive_criterion_inverserightleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightleftentrynegative. ff_h_pvs_positive_criterion_inverserightleftentrynegative + S (dst_negative_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrynegative. dst_negative_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrynegative * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_positive_criterion_inverserightleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightleftentryvalue ge_balance_negative_positive_criterion_inverserightleftentryvalue. (((((dst_value_positive_criterion_inverserightleft) = 2 * (ge_balance_positive_positive_criterion_inverserightleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightleftentryvaluedecode. (((dst_value_positive_criterion_inverserightleft) = 2 * ge_signed_half_positive_criterion_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = S ge_signed_half_positive_criterion_inverserightleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightleft) + ge_balance_negative_positive_criterion_inverserightleftentryvalue = (dst_negative_positive_criterion_inverserightleft) + ge_balance_positive_positive_criterion_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightright dst_positive_scale_positive_criterion_inverserightright dst_negative_code_positive_criterion_inverserightright dst_negative_scale_positive_criterion_inverserightright. (((F) = (((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) * S ((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) + ((((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))))) /\ (forall dst_index_positive_criterion_inverserightright. (exists pvs_le_gap_positive_criterion_inverserightrightdomain. pvs_le_gap_positive_criterion_inverserightrightdomain + (dst_index_positive_criterion_inverserightright) = (N)) -> exists dst_positive_positive_criterion_inverserightright dst_negative_positive_criterion_inverserightright dst_value_positive_criterion_inverserightright. ((((exists ff_h_pvs_positive_criterion_inverserightrightentrypositive. ff_h_pvs_positive_criterion_inverserightrightentrypositive + S (dst_positive_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrypositive. dst_positive_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrypositive * S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_positive_criterion_inverserightright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightrightentrynegative. ff_h_pvs_positive_criterion_inverserightrightentrynegative + S (dst_negative_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrynegative. dst_negative_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrynegative * S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_positive_criterion_inverserightright))) /\ (exists ge_balance_positive_positive_criterion_inverserightrightentryvalue ge_balance_negative_positive_criterion_inverserightrightentryvalue. (((((dst_value_positive_criterion_inverserightright) = 2 * (ge_balance_positive_positive_criterion_inverserightrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightrightentryvaluedecode. (((dst_value_positive_criterion_inverserightright) = 2 * ge_signed_half_positive_criterion_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = S ge_signed_half_positive_criterion_inverserightrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightright) + ge_balance_negative_positive_criterion_inverserightrightentryvalue = (dst_negative_positive_criterion_inverserightright) + ge_balance_positive_positive_criterion_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserighttable dst_positive_scale_positive_criterion_inverserighttable dst_negative_code_positive_criterion_inverserighttable dst_negative_scale_positive_criterion_inverserighttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) * S ((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) + ((((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))))) /\ (forall dst_index_positive_criterion_inverserighttable. (exists pvs_le_gap_positive_criterion_inverserighttabledomain. pvs_le_gap_positive_criterion_inverserighttabledomain + (dst_index_positive_criterion_inverserighttable) = (N)) -> exists dst_positive_positive_criterion_inverserighttable dst_negative_positive_criterion_inverserighttable dst_value_positive_criterion_inverserighttable. ((((exists ff_h_pvs_positive_criterion_inverserighttableentrypositive. ff_h_pvs_positive_criterion_inverserighttableentrypositive + S (dst_positive_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrypositive. dst_positive_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrypositive * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_positive_criterion_inverserighttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserighttableentrynegative. ff_h_pvs_positive_criterion_inverserighttableentrynegative + S (dst_negative_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrynegative. dst_negative_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrynegative * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_positive_criterion_inverserighttable))) /\ (exists ge_balance_positive_positive_criterion_inverserighttableentryvalue ge_balance_negative_positive_criterion_inverserighttableentryvalue. (((((dst_value_positive_criterion_inverserighttable) = 2 * (ge_balance_positive_positive_criterion_inverserighttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserighttableentryvaluedecode. (((dst_value_positive_criterion_inverserighttable) = 2 * ge_signed_half_positive_criterion_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = S ge_signed_half_positive_criterion_inverserighttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserighttable) + ge_balance_negative_positive_criterion_inverserighttableentryvalue = (dst_negative_positive_criterion_inverserighttable) + ge_balance_positive_positive_criterion_inverserighttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseright dc_output_positive_criterion_inverseright. ~(dc_input_positive_criterion_inverseright=0) -> (exists pvs_le_gap_positive_criterion_inverserightdomain. pvs_le_gap_positive_criterion_inverserightdomain + (dc_input_positive_criterion_inverseright) = (N)) -> (exists dst_positive_code_positive_criterion_inverserightlookup dst_positive_scale_positive_criterion_inverserightlookup dst_negative_code_positive_criterion_inverserightlookup dst_negative_scale_positive_criterion_inverserightlookup dst_positive_positive_criterion_inverserightlookup dst_negative_positive_criterion_inverserightlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) * S ((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) + ((((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookuppositive. ff_h_pvs_positive_criterion_inverserightlookuppositive + S (dst_positive_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookuppositive. dst_positive_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookuppositive * S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_positive_criterion_inverserightlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookupnegative. ff_h_pvs_positive_criterion_inverserightlookupnegative + S (dst_negative_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookupnegative. dst_negative_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookupnegative * S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_positive_criterion_inverserightlookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightlookupvalue ge_balance_negative_positive_criterion_inverserightlookupvalue. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightlookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightlookupvaluedecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = S ge_signed_half_positive_criterion_inverserightlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightlookup) + ge_balance_negative_positive_criterion_inverserightlookupvalue = (dst_negative_positive_criterion_inverserightlookup) + ge_balance_positive_positive_criterion_inverserightlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseright)=0)) /\ (exists dc_mask_positive_criterion_inverserightvalue. ((((exists dst_positive_code_positive_criterion_inverserightvaluemasktable dst_positive_scale_positive_criterion_inverserightvaluemasktable dst_negative_code_positive_criterion_inverserightvaluemasktable dst_negative_scale_positive_criterion_inverserightvaluemasktable. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverserightvaluemasktable. (exists pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain. pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain + (dst_index_positive_criterion_inverserightvaluemasktable) = (dc_input_positive_criterion_inverseright)) -> exists dst_positive_positive_criterion_inverserightvaluemasktable dst_negative_positive_criterion_inverserightvaluemasktable dst_value_positive_criterion_inverserightvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_positive_criterion_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_positive_criterion_inverserightvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasktable) + ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue = (dst_negative_positive_criterion_inverserightvaluemasktable) + ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverserightvaluemask dc_value_positive_criterion_inverserightvaluemask. (exists pvs_le_gap_positive_criterion_inverserightvaluemaskdomain. pvs_le_gap_positive_criterion_inverserightvaluemaskdomain + (dc_index_positive_criterion_inverserightvaluemask) = (dc_input_positive_criterion_inverseright)) -> (exists dst_positive_code_positive_criterion_inverserightvaluemasklookup dst_positive_scale_positive_criterion_inverserightvaluemasklookup dst_negative_code_positive_criterion_inverserightvaluemasklookup dst_negative_scale_positive_criterion_inverserightvaluemasklookup dst_positive_positive_criterion_inverserightvaluemasklookup dst_negative_positive_criterion_inverserightvaluemasklookup. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive + S (dst_positive_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive. dst_positive_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_positive_criterion_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative + S (dst_negative_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative. dst_negative_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_positive_criterion_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue. (((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasklookup) + ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue = (dst_negative_positive_criterion_inverserightvaluemasklookup) + ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverserightvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverserightvaluemaskentry dc_left_positive_criterion_inverserightvaluemaskentry dc_right_positive_criterion_inverserightvaluemaskentry. (((dc_input_positive_criterion_inverseright)=(dc_index_positive_criterion_inverserightvaluemask)*dc_quotient_positive_criterion_inverserightvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryleft dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft dst_negative_code_positive_criterion_inverserightvaluemaskentryleft dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft dst_positive_positive_criterion_inverserightvaluemaskentryleft dst_negative_positive_criterion_inverserightvaluemaskentryleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_positive_criterion_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_positive_criterion_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryright dst_positive_scale_positive_criterion_inverserightvaluemaskentryright dst_negative_code_positive_criterion_inverserightvaluemaskentryright dst_negative_scale_positive_criterion_inverserightvaluemaskentryright dst_positive_positive_criterion_inverserightvaluemaskentryright dst_negative_positive_criterion_inverserightvaluemaskentryright. (((F) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_positive_criterion_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_positive_criterion_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryright) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryright) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverserightvaluemaskentryproduct sto_an_positive_criterion_inverserightvaluemaskentryproduct sto_bp_positive_criterion_inverserightvaluemaskentryproduct sto_bn_positive_criterion_inverserightvaluemaskentryproduct sto_cp_positive_criterion_inverserightvaluemaskentryproduct sto_cn_positive_criterion_inverserightvaluemaskentryproduct. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct) + sto_cn_positive_criterion_inverserightvaluemaskentryproduct = (sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct) + sto_cp_positive_criterion_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverserightvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseright) = (dc_index_positive_criterion_inverserightvaluemask) * pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverserightvaluefold dst_positive_scale_positive_criterion_inverserightvaluefold dst_negative_code_positive_criterion_inverserightvaluefold dst_negative_scale_positive_criterion_inverserightvaluefold dst_positive_sum_positive_criterion_inverserightvaluefold dst_negative_sum_positive_criterion_inverserightvaluefold. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) + ((((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldpositive fs_v_dst_positive_criterion_inverserightvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldnegative fs_v_dst_positive_criterion_inverserightvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluefoldresult ge_balance_negative_positive_criterion_inverserightvaluefoldresult. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = S ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverserightvaluefold) + ge_balance_negative_positive_criterion_inverserightvaluefoldresult = (dst_negative_sum_positive_criterion_inverserightvaluefold) + ge_balance_positive_positive_criterion_inverserightvaluefoldresult))))))))))))))))))))))))))