Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N F G H. (exists di_delta_inverse_involution_first. ((((exists dst_positive_code_inverse_involution_firstdeltatable dst_positive_scale_inverse_involution_firstdeltatable dst_negative_code_inverse_involution_firstdeltatable dst_negative_scale_inverse_involution_firstdeltatable. (((di_delta_inverse_involution_first) = (((((dst_positive_code_inverse_involution_firstdeltatable) + (dst_positive_scale_inverse_involution_firstdeltatable)) * S ((dst_positive_code_inverse_involution_firstdeltatable) + (dst_positive_scale_inverse_involution_firstdeltatable)) + ((dst_positive_scale_inverse_involution_firstdeltatable) + (dst_positive_scale_inverse_involution_firstdeltatable))) + (((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) * S ((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) + ((dst_negative_scale_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)))) * S ((((dst_positive_code_inverse_involution_firstdeltatable) + (dst_positive_scale_inverse_involution_firstdeltatable)) * S ((dst_positive_code_inverse_involution_firstdeltatable) + (dst_positive_scale_inverse_involution_firstdeltatable)) + ((dst_positive_scale_inverse_involution_firstdeltatable) + (dst_positive_scale_inverse_involution_firstdeltatable))) + (((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) * S ((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) + ((dst_negative_scale_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)))) + ((((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) * S ((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) + ((dst_negative_scale_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable))) + (((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) * S ((dst_negative_code_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)) + ((dst_negative_scale_inverse_involution_firstdeltatable) + (dst_negative_scale_inverse_involution_firstdeltatable)))))) /\ (forall dst_index_inverse_involution_firstdeltatable. (exists pvs_le_gap_inverse_involution_firstdeltatabledomain. pvs_le_gap_inverse_involution_firstdeltatabledomain + (dst_index_inverse_involution_firstdeltatable) = (N)) -> exists dst_positive_inverse_involution_firstdeltatable dst_negative_inverse_involution_firstdeltatable dst_value_inverse_involution_firstdeltatable. ((((exists ff_h_pvs_inverse_involution_firstdeltatableentrypositive. ff_h_pvs_inverse_involution_firstdeltatableentrypositive + S (dst_positive_inverse_involution_firstdeltatable) = S ((S (dst_index_inverse_involution_firstdeltatable)) * dst_positive_scale_inverse_involution_firstdeltatable)) /\ exists ff_q_pvs_inverse_involution_firstdeltatableentrypositive. dst_positive_code_inverse_involution_firstdeltatable = ff_q_pvs_inverse_involution_firstdeltatableentrypositive * S ((S (dst_index_inverse_involution_firstdeltatable)) * dst_positive_scale_inverse_involution_firstdeltatable) + (dst_positive_inverse_involution_firstdeltatable))) /\ (((((exists ff_h_pvs_inverse_involution_firstdeltatableentrynegative. ff_h_pvs_inverse_involution_firstdeltatableentrynegative + S (dst_negative_inverse_involution_firstdeltatable) = S ((S (dst_index_inverse_involution_firstdeltatable)) * dst_negative_scale_inverse_involution_firstdeltatable)) /\ exists ff_q_pvs_inverse_involution_firstdeltatableentrynegative. dst_negative_code_inverse_involution_firstdeltatable = ff_q_pvs_inverse_involution_firstdeltatableentrynegative * S ((S (dst_index_inverse_involution_firstdeltatable)) * dst_negative_scale_inverse_involution_firstdeltatable) + (dst_negative_inverse_involution_firstdeltatable))) /\ (exists ge_balance_positive_inverse_involution_firstdeltatableentryvalue ge_balance_negative_inverse_involution_firstdeltatableentryvalue. (((((dst_value_inverse_involution_firstdeltatable) = 2 * (ge_balance_positive_inverse_involution_firstdeltatableentryvalue) /\ (ge_balance_negative_inverse_involution_firstdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstdeltatableentryvaluedecode. (((dst_value_inverse_involution_firstdeltatable) = 2 * ge_signed_half_inverse_involution_firstdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstdeltatableentryvalue) = S ge_signed_half_inverse_involution_firstdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstdeltatable) + ge_balance_negative_inverse_involution_firstdeltatableentryvalue = (dst_negative_inverse_involution_firstdeltatable) + ge_balance_positive_inverse_involution_firstdeltatableentryvalue))))))))) /\ (forall du_index_inverse_involution_firstdelta du_value_inverse_involution_firstdelta. ~(du_index_inverse_involution_firstdelta=0) -> (exists pvs_le_gap_inverse_involution_firstdeltabound. pvs_le_gap_inverse_involution_firstdeltabound + (du_index_inverse_involution_firstdelta) = (N)) -> (exists dst_positive_code_inverse_involution_firstdeltaentry dst_positive_scale_inverse_involution_firstdeltaentry dst_negative_code_inverse_involution_firstdeltaentry dst_negative_scale_inverse_involution_firstdeltaentry dst_positive_inverse_involution_firstdeltaentry dst_negative_inverse_involution_firstdeltaentry. (((di_delta_inverse_involution_first) = (((((dst_positive_code_inverse_involution_firstdeltaentry) + (dst_positive_scale_inverse_involution_firstdeltaentry)) * S ((dst_positive_code_inverse_involution_firstdeltaentry) + (dst_positive_scale_inverse_involution_firstdeltaentry)) + ((dst_positive_scale_inverse_involution_firstdeltaentry) + (dst_positive_scale_inverse_involution_firstdeltaentry))) + (((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) * S ((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) + ((dst_negative_scale_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)))) * S ((((dst_positive_code_inverse_involution_firstdeltaentry) + (dst_positive_scale_inverse_involution_firstdeltaentry)) * S ((dst_positive_code_inverse_involution_firstdeltaentry) + (dst_positive_scale_inverse_involution_firstdeltaentry)) + ((dst_positive_scale_inverse_involution_firstdeltaentry) + (dst_positive_scale_inverse_involution_firstdeltaentry))) + (((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) * S ((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) + ((dst_negative_scale_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)))) + ((((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) * S ((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) + ((dst_negative_scale_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry))) + (((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) * S ((dst_negative_code_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)) + ((dst_negative_scale_inverse_involution_firstdeltaentry) + (dst_negative_scale_inverse_involution_firstdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstdeltaentrypositive. ff_h_pvs_inverse_involution_firstdeltaentrypositive + S (dst_positive_inverse_involution_firstdeltaentry) = S ((S (du_index_inverse_involution_firstdelta)) * dst_positive_scale_inverse_involution_firstdeltaentry)) /\ exists ff_q_pvs_inverse_involution_firstdeltaentrypositive. dst_positive_code_inverse_involution_firstdeltaentry = ff_q_pvs_inverse_involution_firstdeltaentrypositive * S ((S (du_index_inverse_involution_firstdelta)) * dst_positive_scale_inverse_involution_firstdeltaentry) + (dst_positive_inverse_involution_firstdeltaentry))) /\ (((((exists ff_h_pvs_inverse_involution_firstdeltaentrynegative. ff_h_pvs_inverse_involution_firstdeltaentrynegative + S (dst_negative_inverse_involution_firstdeltaentry) = S ((S (du_index_inverse_involution_firstdelta)) * dst_negative_scale_inverse_involution_firstdeltaentry)) /\ exists ff_q_pvs_inverse_involution_firstdeltaentrynegative. dst_negative_code_inverse_involution_firstdeltaentry = ff_q_pvs_inverse_involution_firstdeltaentrynegative * S ((S (du_index_inverse_involution_firstdelta)) * dst_negative_scale_inverse_involution_firstdeltaentry) + (dst_negative_inverse_involution_firstdeltaentry))) /\ (exists ge_balance_positive_inverse_involution_firstdeltaentryvalue ge_balance_negative_inverse_involution_firstdeltaentryvalue. (((((du_value_inverse_involution_firstdelta) = 2 * (ge_balance_positive_inverse_involution_firstdeltaentryvalue) /\ (ge_balance_negative_inverse_involution_firstdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstdeltaentryvaluedecode. (((du_value_inverse_involution_firstdelta) = 2 * ge_signed_half_inverse_involution_firstdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstdeltaentryvalue) = S ge_signed_half_inverse_involution_firstdeltaentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstdeltaentry) + ge_balance_negative_inverse_involution_firstdeltaentryvalue = (dst_negative_inverse_involution_firstdeltaentry) + ge_balance_positive_inverse_involution_firstdeltaentryvalue))))))))) -> ((((du_index_inverse_involution_firstdelta)=1 -> (du_value_inverse_involution_firstdelta)=2) /\ (~((du_index_inverse_involution_firstdelta)=1) -> (du_value_inverse_involution_firstdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_involution_firstleftleft dst_positive_scale_inverse_involution_firstleftleft dst_negative_code_inverse_involution_firstleftleft dst_negative_scale_inverse_involution_firstleftleft. (((F) = (((((dst_positive_code_inverse_involution_firstleftleft) + (dst_positive_scale_inverse_involution_firstleftleft)) * S ((dst_positive_code_inverse_involution_firstleftleft) + (dst_positive_scale_inverse_involution_firstleftleft)) + ((dst_positive_scale_inverse_involution_firstleftleft) + (dst_positive_scale_inverse_involution_firstleftleft))) + (((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) * S ((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) + ((dst_negative_scale_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)))) * S ((((dst_positive_code_inverse_involution_firstleftleft) + (dst_positive_scale_inverse_involution_firstleftleft)) * S ((dst_positive_code_inverse_involution_firstleftleft) + (dst_positive_scale_inverse_involution_firstleftleft)) + ((dst_positive_scale_inverse_involution_firstleftleft) + (dst_positive_scale_inverse_involution_firstleftleft))) + (((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) * S ((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) + ((dst_negative_scale_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)))) + ((((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) * S ((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) + ((dst_negative_scale_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft))) + (((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) * S ((dst_negative_code_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)) + ((dst_negative_scale_inverse_involution_firstleftleft) + (dst_negative_scale_inverse_involution_firstleftleft)))))) /\ (forall dst_index_inverse_involution_firstleftleft. (exists pvs_le_gap_inverse_involution_firstleftleftdomain. pvs_le_gap_inverse_involution_firstleftleftdomain + (dst_index_inverse_involution_firstleftleft) = (N)) -> exists dst_positive_inverse_involution_firstleftleft dst_negative_inverse_involution_firstleftleft dst_value_inverse_involution_firstleftleft. ((((exists ff_h_pvs_inverse_involution_firstleftleftentrypositive. ff_h_pvs_inverse_involution_firstleftleftentrypositive + S (dst_positive_inverse_involution_firstleftleft) = S ((S (dst_index_inverse_involution_firstleftleft)) * dst_positive_scale_inverse_involution_firstleftleft)) /\ exists ff_q_pvs_inverse_involution_firstleftleftentrypositive. dst_positive_code_inverse_involution_firstleftleft = ff_q_pvs_inverse_involution_firstleftleftentrypositive * S ((S (dst_index_inverse_involution_firstleftleft)) * dst_positive_scale_inverse_involution_firstleftleft) + (dst_positive_inverse_involution_firstleftleft))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftleftentrynegative. ff_h_pvs_inverse_involution_firstleftleftentrynegative + S (dst_negative_inverse_involution_firstleftleft) = S ((S (dst_index_inverse_involution_firstleftleft)) * dst_negative_scale_inverse_involution_firstleftleft)) /\ exists ff_q_pvs_inverse_involution_firstleftleftentrynegative. dst_negative_code_inverse_involution_firstleftleft = ff_q_pvs_inverse_involution_firstleftleftentrynegative * S ((S (dst_index_inverse_involution_firstleftleft)) * dst_negative_scale_inverse_involution_firstleftleft) + (dst_negative_inverse_involution_firstleftleft))) /\ (exists ge_balance_positive_inverse_involution_firstleftleftentryvalue ge_balance_negative_inverse_involution_firstleftleftentryvalue. (((((dst_value_inverse_involution_firstleftleft) = 2 * (ge_balance_positive_inverse_involution_firstleftleftentryvalue) /\ (ge_balance_negative_inverse_involution_firstleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftleftentryvaluedecode. (((dst_value_inverse_involution_firstleftleft) = 2 * ge_signed_half_inverse_involution_firstleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftleftentryvalue) = S ge_signed_half_inverse_involution_firstleftleftentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftleft) + ge_balance_negative_inverse_involution_firstleftleftentryvalue = (dst_negative_inverse_involution_firstleftleft) + ge_balance_positive_inverse_involution_firstleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_firstleftright dst_positive_scale_inverse_involution_firstleftright dst_negative_code_inverse_involution_firstleftright dst_negative_scale_inverse_involution_firstleftright. (((G) = (((((dst_positive_code_inverse_involution_firstleftright) + (dst_positive_scale_inverse_involution_firstleftright)) * S ((dst_positive_code_inverse_involution_firstleftright) + (dst_positive_scale_inverse_involution_firstleftright)) + ((dst_positive_scale_inverse_involution_firstleftright) + (dst_positive_scale_inverse_involution_firstleftright))) + (((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) * S ((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) + ((dst_negative_scale_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)))) * S ((((dst_positive_code_inverse_involution_firstleftright) + (dst_positive_scale_inverse_involution_firstleftright)) * S ((dst_positive_code_inverse_involution_firstleftright) + (dst_positive_scale_inverse_involution_firstleftright)) + ((dst_positive_scale_inverse_involution_firstleftright) + (dst_positive_scale_inverse_involution_firstleftright))) + (((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) * S ((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) + ((dst_negative_scale_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)))) + ((((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) * S ((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) + ((dst_negative_scale_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright))) + (((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) * S ((dst_negative_code_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)) + ((dst_negative_scale_inverse_involution_firstleftright) + (dst_negative_scale_inverse_involution_firstleftright)))))) /\ (forall dst_index_inverse_involution_firstleftright. (exists pvs_le_gap_inverse_involution_firstleftrightdomain. pvs_le_gap_inverse_involution_firstleftrightdomain + (dst_index_inverse_involution_firstleftright) = (N)) -> exists dst_positive_inverse_involution_firstleftright dst_negative_inverse_involution_firstleftright dst_value_inverse_involution_firstleftright. ((((exists ff_h_pvs_inverse_involution_firstleftrightentrypositive. ff_h_pvs_inverse_involution_firstleftrightentrypositive + S (dst_positive_inverse_involution_firstleftright) = S ((S (dst_index_inverse_involution_firstleftright)) * dst_positive_scale_inverse_involution_firstleftright)) /\ exists ff_q_pvs_inverse_involution_firstleftrightentrypositive. dst_positive_code_inverse_involution_firstleftright = ff_q_pvs_inverse_involution_firstleftrightentrypositive * S ((S (dst_index_inverse_involution_firstleftright)) * dst_positive_scale_inverse_involution_firstleftright) + (dst_positive_inverse_involution_firstleftright))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftrightentrynegative. ff_h_pvs_inverse_involution_firstleftrightentrynegative + S (dst_negative_inverse_involution_firstleftright) = S ((S (dst_index_inverse_involution_firstleftright)) * dst_negative_scale_inverse_involution_firstleftright)) /\ exists ff_q_pvs_inverse_involution_firstleftrightentrynegative. dst_negative_code_inverse_involution_firstleftright = ff_q_pvs_inverse_involution_firstleftrightentrynegative * S ((S (dst_index_inverse_involution_firstleftright)) * dst_negative_scale_inverse_involution_firstleftright) + (dst_negative_inverse_involution_firstleftright))) /\ (exists ge_balance_positive_inverse_involution_firstleftrightentryvalue ge_balance_negative_inverse_involution_firstleftrightentryvalue. (((((dst_value_inverse_involution_firstleftright) = 2 * (ge_balance_positive_inverse_involution_firstleftrightentryvalue) /\ (ge_balance_negative_inverse_involution_firstleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftrightentryvaluedecode. (((dst_value_inverse_involution_firstleftright) = 2 * ge_signed_half_inverse_involution_firstleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftrightentryvalue) = S ge_signed_half_inverse_involution_firstleftrightentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftright) + ge_balance_negative_inverse_involution_firstleftrightentryvalue = (dst_negative_inverse_involution_firstleftright) + ge_balance_positive_inverse_involution_firstleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_firstlefttable dst_positive_scale_inverse_involution_firstlefttable dst_negative_code_inverse_involution_firstlefttable dst_negative_scale_inverse_involution_firstlefttable. (((di_delta_inverse_involution_first) = (((((dst_positive_code_inverse_involution_firstlefttable) + (dst_positive_scale_inverse_involution_firstlefttable)) * S ((dst_positive_code_inverse_involution_firstlefttable) + (dst_positive_scale_inverse_involution_firstlefttable)) + ((dst_positive_scale_inverse_involution_firstlefttable) + (dst_positive_scale_inverse_involution_firstlefttable))) + (((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) * S ((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) + ((dst_negative_scale_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)))) * S ((((dst_positive_code_inverse_involution_firstlefttable) + (dst_positive_scale_inverse_involution_firstlefttable)) * S ((dst_positive_code_inverse_involution_firstlefttable) + (dst_positive_scale_inverse_involution_firstlefttable)) + ((dst_positive_scale_inverse_involution_firstlefttable) + (dst_positive_scale_inverse_involution_firstlefttable))) + (((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) * S ((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) + ((dst_negative_scale_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)))) + ((((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) * S ((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) + ((dst_negative_scale_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable))) + (((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) * S ((dst_negative_code_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)) + ((dst_negative_scale_inverse_involution_firstlefttable) + (dst_negative_scale_inverse_involution_firstlefttable)))))) /\ (forall dst_index_inverse_involution_firstlefttable. (exists pvs_le_gap_inverse_involution_firstlefttabledomain. pvs_le_gap_inverse_involution_firstlefttabledomain + (dst_index_inverse_involution_firstlefttable) = (N)) -> exists dst_positive_inverse_involution_firstlefttable dst_negative_inverse_involution_firstlefttable dst_value_inverse_involution_firstlefttable. ((((exists ff_h_pvs_inverse_involution_firstlefttableentrypositive. ff_h_pvs_inverse_involution_firstlefttableentrypositive + S (dst_positive_inverse_involution_firstlefttable) = S ((S (dst_index_inverse_involution_firstlefttable)) * dst_positive_scale_inverse_involution_firstlefttable)) /\ exists ff_q_pvs_inverse_involution_firstlefttableentrypositive. dst_positive_code_inverse_involution_firstlefttable = ff_q_pvs_inverse_involution_firstlefttableentrypositive * S ((S (dst_index_inverse_involution_firstlefttable)) * dst_positive_scale_inverse_involution_firstlefttable) + (dst_positive_inverse_involution_firstlefttable))) /\ (((((exists ff_h_pvs_inverse_involution_firstlefttableentrynegative. ff_h_pvs_inverse_involution_firstlefttableentrynegative + S (dst_negative_inverse_involution_firstlefttable) = S ((S (dst_index_inverse_involution_firstlefttable)) * dst_negative_scale_inverse_involution_firstlefttable)) /\ exists ff_q_pvs_inverse_involution_firstlefttableentrynegative. dst_negative_code_inverse_involution_firstlefttable = ff_q_pvs_inverse_involution_firstlefttableentrynegative * S ((S (dst_index_inverse_involution_firstlefttable)) * dst_negative_scale_inverse_involution_firstlefttable) + (dst_negative_inverse_involution_firstlefttable))) /\ (exists ge_balance_positive_inverse_involution_firstlefttableentryvalue ge_balance_negative_inverse_involution_firstlefttableentryvalue. (((((dst_value_inverse_involution_firstlefttable) = 2 * (ge_balance_positive_inverse_involution_firstlefttableentryvalue) /\ (ge_balance_negative_inverse_involution_firstlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstlefttableentryvaluedecode. (((dst_value_inverse_involution_firstlefttable) = 2 * ge_signed_half_inverse_involution_firstlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstlefttableentryvalue) = S ge_signed_half_inverse_involution_firstlefttableentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstlefttable) + ge_balance_negative_inverse_involution_firstlefttableentryvalue = (dst_negative_inverse_involution_firstlefttable) + ge_balance_positive_inverse_involution_firstlefttableentryvalue))))))))) /\ (forall dc_input_inverse_involution_firstleft dc_output_inverse_involution_firstleft. ~(dc_input_inverse_involution_firstleft=0) -> (exists pvs_le_gap_inverse_involution_firstleftdomain. pvs_le_gap_inverse_involution_firstleftdomain + (dc_input_inverse_involution_firstleft) = (N)) -> (exists dst_positive_code_inverse_involution_firstleftlookup dst_positive_scale_inverse_involution_firstleftlookup dst_negative_code_inverse_involution_firstleftlookup dst_negative_scale_inverse_involution_firstleftlookup dst_positive_inverse_involution_firstleftlookup dst_negative_inverse_involution_firstleftlookup. (((di_delta_inverse_involution_first) = (((((dst_positive_code_inverse_involution_firstleftlookup) + (dst_positive_scale_inverse_involution_firstleftlookup)) * S ((dst_positive_code_inverse_involution_firstleftlookup) + (dst_positive_scale_inverse_involution_firstleftlookup)) + ((dst_positive_scale_inverse_involution_firstleftlookup) + (dst_positive_scale_inverse_involution_firstleftlookup))) + (((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) * S ((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) + ((dst_negative_scale_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)))) * S ((((dst_positive_code_inverse_involution_firstleftlookup) + (dst_positive_scale_inverse_involution_firstleftlookup)) * S ((dst_positive_code_inverse_involution_firstleftlookup) + (dst_positive_scale_inverse_involution_firstleftlookup)) + ((dst_positive_scale_inverse_involution_firstleftlookup) + (dst_positive_scale_inverse_involution_firstleftlookup))) + (((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) * S ((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) + ((dst_negative_scale_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)))) + ((((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) * S ((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) + ((dst_negative_scale_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup))) + (((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) * S ((dst_negative_code_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)) + ((dst_negative_scale_inverse_involution_firstleftlookup) + (dst_negative_scale_inverse_involution_firstleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftlookuppositive. ff_h_pvs_inverse_involution_firstleftlookuppositive + S (dst_positive_inverse_involution_firstleftlookup) = S ((S (dc_input_inverse_involution_firstleft)) * dst_positive_scale_inverse_involution_firstleftlookup)) /\ exists ff_q_pvs_inverse_involution_firstleftlookuppositive. dst_positive_code_inverse_involution_firstleftlookup = ff_q_pvs_inverse_involution_firstleftlookuppositive * S ((S (dc_input_inverse_involution_firstleft)) * dst_positive_scale_inverse_involution_firstleftlookup) + (dst_positive_inverse_involution_firstleftlookup))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftlookupnegative. ff_h_pvs_inverse_involution_firstleftlookupnegative + S (dst_negative_inverse_involution_firstleftlookup) = S ((S (dc_input_inverse_involution_firstleft)) * dst_negative_scale_inverse_involution_firstleftlookup)) /\ exists ff_q_pvs_inverse_involution_firstleftlookupnegative. dst_negative_code_inverse_involution_firstleftlookup = ff_q_pvs_inverse_involution_firstleftlookupnegative * S ((S (dc_input_inverse_involution_firstleft)) * dst_negative_scale_inverse_involution_firstleftlookup) + (dst_negative_inverse_involution_firstleftlookup))) /\ (exists ge_balance_positive_inverse_involution_firstleftlookupvalue ge_balance_negative_inverse_involution_firstleftlookupvalue. (((((dc_output_inverse_involution_firstleft) = 2 * (ge_balance_positive_inverse_involution_firstleftlookupvalue) /\ (ge_balance_negative_inverse_involution_firstleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftlookupvaluedecode. (((dc_output_inverse_involution_firstleft) = 2 * ge_signed_half_inverse_involution_firstleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftlookupvalue) = S ge_signed_half_inverse_involution_firstleftlookupvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftlookup) + ge_balance_negative_inverse_involution_firstleftlookupvalue = (dst_negative_inverse_involution_firstleftlookup) + ge_balance_positive_inverse_involution_firstleftlookupvalue))))))))) -> (((~((dc_input_inverse_involution_firstleft)=0)) /\ (exists dc_mask_inverse_involution_firstleftvalue. ((((exists dst_positive_code_inverse_involution_firstleftvaluemasktable dst_positive_scale_inverse_involution_firstleftvaluemasktable dst_negative_code_inverse_involution_firstleftvaluemasktable dst_negative_scale_inverse_involution_firstleftvaluemasktable. (((dc_mask_inverse_involution_firstleftvalue) = (((((dst_positive_code_inverse_involution_firstleftvaluemasktable) + (dst_positive_scale_inverse_involution_firstleftvaluemasktable)) * S ((dst_positive_code_inverse_involution_firstleftvaluemasktable) + (dst_positive_scale_inverse_involution_firstleftvaluemasktable)) + ((dst_positive_scale_inverse_involution_firstleftvaluemasktable) + (dst_positive_scale_inverse_involution_firstleftvaluemasktable))) + (((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)))) * S ((((dst_positive_code_inverse_involution_firstleftvaluemasktable) + (dst_positive_scale_inverse_involution_firstleftvaluemasktable)) * S ((dst_positive_code_inverse_involution_firstleftvaluemasktable) + (dst_positive_scale_inverse_involution_firstleftvaluemasktable)) + ((dst_positive_scale_inverse_involution_firstleftvaluemasktable) + (dst_positive_scale_inverse_involution_firstleftvaluemasktable))) + (((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)))) + ((((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable))) + (((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasktable) + (dst_negative_scale_inverse_involution_firstleftvaluemasktable)))))) /\ (forall dst_index_inverse_involution_firstleftvaluemasktable. (exists pvs_le_gap_inverse_involution_firstleftvaluemasktabledomain. pvs_le_gap_inverse_involution_firstleftvaluemasktabledomain + (dst_index_inverse_involution_firstleftvaluemasktable) = (dc_input_inverse_involution_firstleft)) -> exists dst_positive_inverse_involution_firstleftvaluemasktable dst_negative_inverse_involution_firstleftvaluemasktable dst_value_inverse_involution_firstleftvaluemasktable. ((((exists ff_h_pvs_inverse_involution_firstleftvaluemasktableentrypositive. ff_h_pvs_inverse_involution_firstleftvaluemasktableentrypositive + S (dst_positive_inverse_involution_firstleftvaluemasktable) = S ((S (dst_index_inverse_involution_firstleftvaluemasktable)) * dst_positive_scale_inverse_involution_firstleftvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemasktableentrypositive. dst_positive_code_inverse_involution_firstleftvaluemasktable = ff_q_pvs_inverse_involution_firstleftvaluemasktableentrypositive * S ((S (dst_index_inverse_involution_firstleftvaluemasktable)) * dst_positive_scale_inverse_involution_firstleftvaluemasktable) + (dst_positive_inverse_involution_firstleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemasktableentrynegative. ff_h_pvs_inverse_involution_firstleftvaluemasktableentrynegative + S (dst_negative_inverse_involution_firstleftvaluemasktable) = S ((S (dst_index_inverse_involution_firstleftvaluemasktable)) * dst_negative_scale_inverse_involution_firstleftvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemasktableentrynegative. dst_negative_code_inverse_involution_firstleftvaluemasktable = ff_q_pvs_inverse_involution_firstleftvaluemasktableentrynegative * S ((S (dst_index_inverse_involution_firstleftvaluemasktable)) * dst_negative_scale_inverse_involution_firstleftvaluemasktable) + (dst_negative_inverse_involution_firstleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_involution_firstleftvaluemasktableentryvalue ge_balance_negative_inverse_involution_firstleftvaluemasktableentryvalue. (((((dst_value_inverse_involution_firstleftvaluemasktable) = 2 * (ge_balance_positive_inverse_involution_firstleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_involution_firstleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemasktableentryvaluedecode. (((dst_value_inverse_involution_firstleftvaluemasktable) = 2 * ge_signed_half_inverse_involution_firstleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftvaluemasktableentryvalue) = S ge_signed_half_inverse_involution_firstleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftvaluemasktable) + ge_balance_negative_inverse_involution_firstleftvaluemasktableentryvalue = (dst_negative_inverse_involution_firstleftvaluemasktable) + ge_balance_positive_inverse_involution_firstleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_involution_firstleftvaluemask dc_value_inverse_involution_firstleftvaluemask. (exists pvs_le_gap_inverse_involution_firstleftvaluemaskdomain. pvs_le_gap_inverse_involution_firstleftvaluemaskdomain + (dc_index_inverse_involution_firstleftvaluemask) = (dc_input_inverse_involution_firstleft)) -> (exists dst_positive_code_inverse_involution_firstleftvaluemasklookup dst_positive_scale_inverse_involution_firstleftvaluemasklookup dst_negative_code_inverse_involution_firstleftvaluemasklookup dst_negative_scale_inverse_involution_firstleftvaluemasklookup dst_positive_inverse_involution_firstleftvaluemasklookup dst_negative_inverse_involution_firstleftvaluemasklookup. (((dc_mask_inverse_involution_firstleftvalue) = (((((dst_positive_code_inverse_involution_firstleftvaluemasklookup) + (dst_positive_scale_inverse_involution_firstleftvaluemasklookup)) * S ((dst_positive_code_inverse_involution_firstleftvaluemasklookup) + (dst_positive_scale_inverse_involution_firstleftvaluemasklookup)) + ((dst_positive_scale_inverse_involution_firstleftvaluemasklookup) + (dst_positive_scale_inverse_involution_firstleftvaluemasklookup))) + (((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_involution_firstleftvaluemasklookup) + (dst_positive_scale_inverse_involution_firstleftvaluemasklookup)) * S ((dst_positive_code_inverse_involution_firstleftvaluemasklookup) + (dst_positive_scale_inverse_involution_firstleftvaluemasklookup)) + ((dst_positive_scale_inverse_involution_firstleftvaluemasklookup) + (dst_positive_scale_inverse_involution_firstleftvaluemasklookup))) + (((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)))) + ((((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup))) + (((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstleftvaluemasklookup) + (dst_negative_scale_inverse_involution_firstleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemasklookuppositive. ff_h_pvs_inverse_involution_firstleftvaluemasklookuppositive + S (dst_positive_inverse_involution_firstleftvaluemasklookup) = S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_positive_scale_inverse_involution_firstleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemasklookuppositive. dst_positive_code_inverse_involution_firstleftvaluemasklookup = ff_q_pvs_inverse_involution_firstleftvaluemasklookuppositive * S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_positive_scale_inverse_involution_firstleftvaluemasklookup) + (dst_positive_inverse_involution_firstleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemasklookupnegative. ff_h_pvs_inverse_involution_firstleftvaluemasklookupnegative + S (dst_negative_inverse_involution_firstleftvaluemasklookup) = S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_negative_scale_inverse_involution_firstleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemasklookupnegative. dst_negative_code_inverse_involution_firstleftvaluemasklookup = ff_q_pvs_inverse_involution_firstleftvaluemasklookupnegative * S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_negative_scale_inverse_involution_firstleftvaluemasklookup) + (dst_negative_inverse_involution_firstleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_involution_firstleftvaluemasklookupvalue ge_balance_negative_inverse_involution_firstleftvaluemasklookupvalue. (((((dc_value_inverse_involution_firstleftvaluemask) = 2 * (ge_balance_positive_inverse_involution_firstleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_involution_firstleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemasklookupvaluedecode. (((dc_value_inverse_involution_firstleftvaluemask) = 2 * ge_signed_half_inverse_involution_firstleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftvaluemasklookupvalue) = S ge_signed_half_inverse_involution_firstleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftvaluemasklookup) + ge_balance_negative_inverse_involution_firstleftvaluemasklookupvalue = (dst_negative_inverse_involution_firstleftvaluemasklookup) + ge_balance_positive_inverse_involution_firstleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_involution_firstleftvaluemask)=0)) /\ (exists dc_quotient_inverse_involution_firstleftvaluemaskentry dc_left_inverse_involution_firstleftvaluemaskentry dc_right_inverse_involution_firstleftvaluemaskentry. (((dc_input_inverse_involution_firstleft)=(dc_index_inverse_involution_firstleftvaluemask)*dc_quotient_inverse_involution_firstleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_involution_firstleftvaluemaskentryleft dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft dst_negative_code_inverse_involution_firstleftvaluemaskentryleft dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft dst_positive_inverse_involution_firstleftvaluemaskentryleft dst_negative_inverse_involution_firstleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemaskentryleftpositive. ff_h_pvs_inverse_involution_firstleftvaluemaskentryleftpositive + S (dst_positive_inverse_involution_firstleftvaluemaskentryleft) = S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemaskentryleftpositive. dst_positive_code_inverse_involution_firstleftvaluemaskentryleft = ff_q_pvs_inverse_involution_firstleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_positive_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_positive_inverse_involution_firstleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemaskentryleftnegative. ff_h_pvs_inverse_involution_firstleftvaluemaskentryleftnegative + S (dst_negative_inverse_involution_firstleftvaluemaskentryleft) = S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemaskentryleftnegative. dst_negative_code_inverse_involution_firstleftvaluemaskentryleft = ff_q_pvs_inverse_involution_firstleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_involution_firstleftvaluemask)) * dst_negative_scale_inverse_involution_firstleftvaluemaskentryleft) + (dst_negative_inverse_involution_firstleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_involution_firstleftvaluemaskentryleftvalue ge_balance_negative_inverse_involution_firstleftvaluemaskentryleftvalue. (((((dc_left_inverse_involution_firstleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_firstleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_involution_firstleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_involution_firstleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_involution_firstleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftvaluemaskentryleft) + ge_balance_negative_inverse_involution_firstleftvaluemaskentryleftvalue = (dst_negative_inverse_involution_firstleftvaluemaskentryleft) + ge_balance_positive_inverse_involution_firstleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_firstleftvaluemaskentryright dst_positive_scale_inverse_involution_firstleftvaluemaskentryright dst_negative_code_inverse_involution_firstleftvaluemaskentryright dst_negative_scale_inverse_involution_firstleftvaluemaskentryright dst_positive_inverse_involution_firstleftvaluemaskentryright dst_negative_inverse_involution_firstleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryright))) + (((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstleftvaluemaskentryright))) + (((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright))) + (((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemaskentryrightpositive. ff_h_pvs_inverse_involution_firstleftvaluemaskentryrightpositive + S (dst_positive_inverse_involution_firstleftvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_firstleftvaluemaskentry)) * dst_positive_scale_inverse_involution_firstleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemaskentryrightpositive. dst_positive_code_inverse_involution_firstleftvaluemaskentryright = ff_q_pvs_inverse_involution_firstleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_involution_firstleftvaluemaskentry)) * dst_positive_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_positive_inverse_involution_firstleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_involution_firstleftvaluemaskentryrightnegative. ff_h_pvs_inverse_involution_firstleftvaluemaskentryrightnegative + S (dst_negative_inverse_involution_firstleftvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_firstleftvaluemaskentry)) * dst_negative_scale_inverse_involution_firstleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_firstleftvaluemaskentryrightnegative. dst_negative_code_inverse_involution_firstleftvaluemaskentryright = ff_q_pvs_inverse_involution_firstleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_involution_firstleftvaluemaskentry)) * dst_negative_scale_inverse_involution_firstleftvaluemaskentryright) + (dst_negative_inverse_involution_firstleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_involution_firstleftvaluemaskentryrightvalue ge_balance_negative_inverse_involution_firstleftvaluemaskentryrightvalue. (((((dc_right_inverse_involution_firstleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_firstleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_involution_firstleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_involution_firstleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_involution_firstleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_involution_firstleftvaluemaskentryright) + ge_balance_negative_inverse_involution_firstleftvaluemaskentryrightvalue = (dst_negative_inverse_involution_firstleftvaluemaskentryright) + ge_balance_positive_inverse_involution_firstleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_involution_firstleftvaluemaskentryproduct sto_an_inverse_involution_firstleftvaluemaskentryproduct sto_bp_inverse_involution_firstleftvaluemaskentryproduct sto_bn_inverse_involution_firstleftvaluemaskentryproduct sto_cp_inverse_involution_firstleftvaluemaskentryproduct sto_cn_inverse_involution_firstleftvaluemaskentryproduct. (((((dc_left_inverse_involution_firstleftvaluemaskentry) = 2 * (sto_ap_inverse_involution_firstleftvaluemaskentryproduct) /\ (sto_an_inverse_involution_firstleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemaskentryproductleft. (((dc_left_inverse_involution_firstleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_involution_firstleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_involution_firstleftvaluemaskentryproduct) = S ge_signed_half_inverse_involution_firstleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_involution_firstleftvaluemaskentry) = 2 * (sto_bp_inverse_involution_firstleftvaluemaskentryproduct) /\ (sto_bn_inverse_involution_firstleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemaskentryproductright. (((dc_right_inverse_involution_firstleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_involution_firstleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_involution_firstleftvaluemaskentryproduct) = S ge_signed_half_inverse_involution_firstleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_involution_firstleftvaluemask) = 2 * (sto_cp_inverse_involution_firstleftvaluemaskentryproduct) /\ (sto_cn_inverse_involution_firstleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluemaskentryproductoutput. (((dc_value_inverse_involution_firstleftvaluemask) = 2 * ge_signed_half_inverse_involution_firstleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_involution_firstleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_involution_firstleftvaluemaskentryproduct) = S ge_signed_half_inverse_involution_firstleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_involution_firstleftvaluemaskentryproduct * sto_bp_inverse_involution_firstleftvaluemaskentryproduct + sto_an_inverse_involution_firstleftvaluemaskentryproduct * sto_bn_inverse_involution_firstleftvaluemaskentryproduct) + sto_cn_inverse_involution_firstleftvaluemaskentryproduct = (sto_ap_inverse_involution_firstleftvaluemaskentryproduct * sto_bn_inverse_involution_firstleftvaluemaskentryproduct + sto_an_inverse_involution_firstleftvaluemaskentryproduct * sto_bp_inverse_involution_firstleftvaluemaskentryproduct) + sto_cp_inverse_involution_firstleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_involution_firstleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_involution_firstleftvaluemaskentrynondivisor. (dc_input_inverse_involution_firstleft) = (dc_index_inverse_involution_firstleftvaluemask) * pvs_factor_inverse_involution_firstleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_involution_firstleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_involution_firstleftvaluefold dst_positive_scale_inverse_involution_firstleftvaluefold dst_negative_code_inverse_involution_firstleftvaluefold dst_negative_scale_inverse_involution_firstleftvaluefold dst_positive_sum_inverse_involution_firstleftvaluefold dst_negative_sum_inverse_involution_firstleftvaluefold. (((dc_mask_inverse_involution_firstleftvalue) = (((((dst_positive_code_inverse_involution_firstleftvaluefold) + (dst_positive_scale_inverse_involution_firstleftvaluefold)) * S ((dst_positive_code_inverse_involution_firstleftvaluefold) + (dst_positive_scale_inverse_involution_firstleftvaluefold)) + ((dst_positive_scale_inverse_involution_firstleftvaluefold) + (dst_positive_scale_inverse_involution_firstleftvaluefold))) + (((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) * S ((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) + ((dst_negative_scale_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)))) * S ((((dst_positive_code_inverse_involution_firstleftvaluefold) + (dst_positive_scale_inverse_involution_firstleftvaluefold)) * S ((dst_positive_code_inverse_involution_firstleftvaluefold) + (dst_positive_scale_inverse_involution_firstleftvaluefold)) + ((dst_positive_scale_inverse_involution_firstleftvaluefold) + (dst_positive_scale_inverse_involution_firstleftvaluefold))) + (((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) * S ((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) + ((dst_negative_scale_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)))) + ((((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) * S ((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) + ((dst_negative_scale_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold))) + (((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) * S ((dst_negative_code_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)) + ((dst_negative_scale_inverse_involution_firstleftvaluefold) + (dst_negative_scale_inverse_involution_firstleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_involution_firstleftvaluefoldpositive fs_v_dst_inverse_involution_firstleftvaluefoldpositive. ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_start. fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_start. fs_u_dst_inverse_involution_firstleftvaluefoldpositive = fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_involution_firstleftvaluefold) = S ((S (S (dc_input_inverse_involution_firstleft))) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_involution_firstleftvaluefoldpositive = fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_involution_firstleft))) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive) + (dst_positive_sum_inverse_involution_firstleftvaluefold))) /\ forall fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps = S (dc_input_inverse_involution_firstleft)) -> exists fs_a_dst_inverse_involution_firstleftvaluefoldpositive_body_steps fs_r_dst_inverse_involution_firstleftvaluefoldpositive_body_steps fs_s_dst_inverse_involution_firstleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_involution_firstleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_firstleftvaluefold)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_involution_firstleftvaluefold = fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_firstleftvaluefold) + (fs_a_dst_inverse_involution_firstleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_involution_firstleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_involution_firstleftvaluefoldpositive = fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive) + (fs_r_dst_inverse_involution_firstleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_involution_firstleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_involution_firstleftvaluefoldpositive = fs_q_dst_inverse_involution_firstleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldpositive) + (fs_s_dst_inverse_involution_firstleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_involution_firstleftvaluefoldpositive_body_steps = fs_r_dst_inverse_involution_firstleftvaluefoldpositive_body_steps + fs_a_dst_inverse_involution_firstleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_involution_firstleftvaluefoldnegative fs_v_dst_inverse_involution_firstleftvaluefoldnegative. ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_start. fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_start. fs_u_dst_inverse_involution_firstleftvaluefoldnegative = fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_involution_firstleftvaluefold) = S ((S (S (dc_input_inverse_involution_firstleft))) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_involution_firstleftvaluefoldnegative = fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_involution_firstleft))) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative) + (dst_negative_sum_inverse_involution_firstleftvaluefold))) /\ forall fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps = S (dc_input_inverse_involution_firstleft)) -> exists fs_a_dst_inverse_involution_firstleftvaluefoldnegative_body_steps fs_r_dst_inverse_involution_firstleftvaluefoldnegative_body_steps fs_s_dst_inverse_involution_firstleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_involution_firstleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_firstleftvaluefold)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_involution_firstleftvaluefold = fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_firstleftvaluefold) + (fs_a_dst_inverse_involution_firstleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_involution_firstleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_involution_firstleftvaluefoldnegative = fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative) + (fs_r_dst_inverse_involution_firstleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_involution_firstleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_involution_firstleftvaluefoldnegative = fs_q_dst_inverse_involution_firstleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstleftvaluefoldnegative) + (fs_s_dst_inverse_involution_firstleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_involution_firstleftvaluefoldnegative_body_steps = fs_r_dst_inverse_involution_firstleftvaluefoldnegative_body_steps + fs_a_dst_inverse_involution_firstleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_involution_firstleftvaluefoldresult ge_balance_negative_inverse_involution_firstleftvaluefoldresult. (((((dc_output_inverse_involution_firstleft) = 2 * (ge_balance_positive_inverse_involution_firstleftvaluefoldresult) /\ (ge_balance_negative_inverse_involution_firstleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_involution_firstleftvaluefoldresultdecode. (((dc_output_inverse_involution_firstleft) = 2 * ge_signed_half_inverse_involution_firstleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_involution_firstleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_involution_firstleftvaluefoldresult) = S ge_signed_half_inverse_involution_firstleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_involution_firstleftvaluefold) + ge_balance_negative_inverse_involution_firstleftvaluefoldresult = (dst_negative_sum_inverse_involution_firstleftvaluefold) + ge_balance_positive_inverse_involution_firstleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_involution_firstrightleft dst_positive_scale_inverse_involution_firstrightleft dst_negative_code_inverse_involution_firstrightleft dst_negative_scale_inverse_involution_firstrightleft. (((G) = (((((dst_positive_code_inverse_involution_firstrightleft) + (dst_positive_scale_inverse_involution_firstrightleft)) * S ((dst_positive_code_inverse_involution_firstrightleft) + (dst_positive_scale_inverse_involution_firstrightleft)) + ((dst_positive_scale_inverse_involution_firstrightleft) + (dst_positive_scale_inverse_involution_firstrightleft))) + (((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) * S ((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) + ((dst_negative_scale_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)))) * S ((((dst_positive_code_inverse_involution_firstrightleft) + (dst_positive_scale_inverse_involution_firstrightleft)) * S ((dst_positive_code_inverse_involution_firstrightleft) + (dst_positive_scale_inverse_involution_firstrightleft)) + ((dst_positive_scale_inverse_involution_firstrightleft) + (dst_positive_scale_inverse_involution_firstrightleft))) + (((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) * S ((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) + ((dst_negative_scale_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)))) + ((((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) * S ((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) + ((dst_negative_scale_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft))) + (((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) * S ((dst_negative_code_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)) + ((dst_negative_scale_inverse_involution_firstrightleft) + (dst_negative_scale_inverse_involution_firstrightleft)))))) /\ (forall dst_index_inverse_involution_firstrightleft. (exists pvs_le_gap_inverse_involution_firstrightleftdomain. pvs_le_gap_inverse_involution_firstrightleftdomain + (dst_index_inverse_involution_firstrightleft) = (N)) -> exists dst_positive_inverse_involution_firstrightleft dst_negative_inverse_involution_firstrightleft dst_value_inverse_involution_firstrightleft. ((((exists ff_h_pvs_inverse_involution_firstrightleftentrypositive. ff_h_pvs_inverse_involution_firstrightleftentrypositive + S (dst_positive_inverse_involution_firstrightleft) = S ((S (dst_index_inverse_involution_firstrightleft)) * dst_positive_scale_inverse_involution_firstrightleft)) /\ exists ff_q_pvs_inverse_involution_firstrightleftentrypositive. dst_positive_code_inverse_involution_firstrightleft = ff_q_pvs_inverse_involution_firstrightleftentrypositive * S ((S (dst_index_inverse_involution_firstrightleft)) * dst_positive_scale_inverse_involution_firstrightleft) + (dst_positive_inverse_involution_firstrightleft))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightleftentrynegative. ff_h_pvs_inverse_involution_firstrightleftentrynegative + S (dst_negative_inverse_involution_firstrightleft) = S ((S (dst_index_inverse_involution_firstrightleft)) * dst_negative_scale_inverse_involution_firstrightleft)) /\ exists ff_q_pvs_inverse_involution_firstrightleftentrynegative. dst_negative_code_inverse_involution_firstrightleft = ff_q_pvs_inverse_involution_firstrightleftentrynegative * S ((S (dst_index_inverse_involution_firstrightleft)) * dst_negative_scale_inverse_involution_firstrightleft) + (dst_negative_inverse_involution_firstrightleft))) /\ (exists ge_balance_positive_inverse_involution_firstrightleftentryvalue ge_balance_negative_inverse_involution_firstrightleftentryvalue. (((((dst_value_inverse_involution_firstrightleft) = 2 * (ge_balance_positive_inverse_involution_firstrightleftentryvalue) /\ (ge_balance_negative_inverse_involution_firstrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightleftentryvaluedecode. (((dst_value_inverse_involution_firstrightleft) = 2 * ge_signed_half_inverse_involution_firstrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightleftentryvalue) = S ge_signed_half_inverse_involution_firstrightleftentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightleft) + ge_balance_negative_inverse_involution_firstrightleftentryvalue = (dst_negative_inverse_involution_firstrightleft) + ge_balance_positive_inverse_involution_firstrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_firstrightright dst_positive_scale_inverse_involution_firstrightright dst_negative_code_inverse_involution_firstrightright dst_negative_scale_inverse_involution_firstrightright. (((F) = (((((dst_positive_code_inverse_involution_firstrightright) + (dst_positive_scale_inverse_involution_firstrightright)) * S ((dst_positive_code_inverse_involution_firstrightright) + (dst_positive_scale_inverse_involution_firstrightright)) + ((dst_positive_scale_inverse_involution_firstrightright) + (dst_positive_scale_inverse_involution_firstrightright))) + (((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) * S ((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) + ((dst_negative_scale_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)))) * S ((((dst_positive_code_inverse_involution_firstrightright) + (dst_positive_scale_inverse_involution_firstrightright)) * S ((dst_positive_code_inverse_involution_firstrightright) + (dst_positive_scale_inverse_involution_firstrightright)) + ((dst_positive_scale_inverse_involution_firstrightright) + (dst_positive_scale_inverse_involution_firstrightright))) + (((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) * S ((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) + ((dst_negative_scale_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)))) + ((((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) * S ((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) + ((dst_negative_scale_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright))) + (((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) * S ((dst_negative_code_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)) + ((dst_negative_scale_inverse_involution_firstrightright) + (dst_negative_scale_inverse_involution_firstrightright)))))) /\ (forall dst_index_inverse_involution_firstrightright. (exists pvs_le_gap_inverse_involution_firstrightrightdomain. pvs_le_gap_inverse_involution_firstrightrightdomain + (dst_index_inverse_involution_firstrightright) = (N)) -> exists dst_positive_inverse_involution_firstrightright dst_negative_inverse_involution_firstrightright dst_value_inverse_involution_firstrightright. ((((exists ff_h_pvs_inverse_involution_firstrightrightentrypositive. ff_h_pvs_inverse_involution_firstrightrightentrypositive + S (dst_positive_inverse_involution_firstrightright) = S ((S (dst_index_inverse_involution_firstrightright)) * dst_positive_scale_inverse_involution_firstrightright)) /\ exists ff_q_pvs_inverse_involution_firstrightrightentrypositive. dst_positive_code_inverse_involution_firstrightright = ff_q_pvs_inverse_involution_firstrightrightentrypositive * S ((S (dst_index_inverse_involution_firstrightright)) * dst_positive_scale_inverse_involution_firstrightright) + (dst_positive_inverse_involution_firstrightright))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightrightentrynegative. ff_h_pvs_inverse_involution_firstrightrightentrynegative + S (dst_negative_inverse_involution_firstrightright) = S ((S (dst_index_inverse_involution_firstrightright)) * dst_negative_scale_inverse_involution_firstrightright)) /\ exists ff_q_pvs_inverse_involution_firstrightrightentrynegative. dst_negative_code_inverse_involution_firstrightright = ff_q_pvs_inverse_involution_firstrightrightentrynegative * S ((S (dst_index_inverse_involution_firstrightright)) * dst_negative_scale_inverse_involution_firstrightright) + (dst_negative_inverse_involution_firstrightright))) /\ (exists ge_balance_positive_inverse_involution_firstrightrightentryvalue ge_balance_negative_inverse_involution_firstrightrightentryvalue. (((((dst_value_inverse_involution_firstrightright) = 2 * (ge_balance_positive_inverse_involution_firstrightrightentryvalue) /\ (ge_balance_negative_inverse_involution_firstrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightrightentryvaluedecode. (((dst_value_inverse_involution_firstrightright) = 2 * ge_signed_half_inverse_involution_firstrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightrightentryvalue) = S ge_signed_half_inverse_involution_firstrightrightentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightright) + ge_balance_negative_inverse_involution_firstrightrightentryvalue = (dst_negative_inverse_involution_firstrightright) + ge_balance_positive_inverse_involution_firstrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_firstrighttable dst_positive_scale_inverse_involution_firstrighttable dst_negative_code_inverse_involution_firstrighttable dst_negative_scale_inverse_involution_firstrighttable. (((di_delta_inverse_involution_first) = (((((dst_positive_code_inverse_involution_firstrighttable) + (dst_positive_scale_inverse_involution_firstrighttable)) * S ((dst_positive_code_inverse_involution_firstrighttable) + (dst_positive_scale_inverse_involution_firstrighttable)) + ((dst_positive_scale_inverse_involution_firstrighttable) + (dst_positive_scale_inverse_involution_firstrighttable))) + (((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) * S ((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) + ((dst_negative_scale_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)))) * S ((((dst_positive_code_inverse_involution_firstrighttable) + (dst_positive_scale_inverse_involution_firstrighttable)) * S ((dst_positive_code_inverse_involution_firstrighttable) + (dst_positive_scale_inverse_involution_firstrighttable)) + ((dst_positive_scale_inverse_involution_firstrighttable) + (dst_positive_scale_inverse_involution_firstrighttable))) + (((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) * S ((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) + ((dst_negative_scale_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)))) + ((((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) * S ((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) + ((dst_negative_scale_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable))) + (((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) * S ((dst_negative_code_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)) + ((dst_negative_scale_inverse_involution_firstrighttable) + (dst_negative_scale_inverse_involution_firstrighttable)))))) /\ (forall dst_index_inverse_involution_firstrighttable. (exists pvs_le_gap_inverse_involution_firstrighttabledomain. pvs_le_gap_inverse_involution_firstrighttabledomain + (dst_index_inverse_involution_firstrighttable) = (N)) -> exists dst_positive_inverse_involution_firstrighttable dst_negative_inverse_involution_firstrighttable dst_value_inverse_involution_firstrighttable. ((((exists ff_h_pvs_inverse_involution_firstrighttableentrypositive. ff_h_pvs_inverse_involution_firstrighttableentrypositive + S (dst_positive_inverse_involution_firstrighttable) = S ((S (dst_index_inverse_involution_firstrighttable)) * dst_positive_scale_inverse_involution_firstrighttable)) /\ exists ff_q_pvs_inverse_involution_firstrighttableentrypositive. dst_positive_code_inverse_involution_firstrighttable = ff_q_pvs_inverse_involution_firstrighttableentrypositive * S ((S (dst_index_inverse_involution_firstrighttable)) * dst_positive_scale_inverse_involution_firstrighttable) + (dst_positive_inverse_involution_firstrighttable))) /\ (((((exists ff_h_pvs_inverse_involution_firstrighttableentrynegative. ff_h_pvs_inverse_involution_firstrighttableentrynegative + S (dst_negative_inverse_involution_firstrighttable) = S ((S (dst_index_inverse_involution_firstrighttable)) * dst_negative_scale_inverse_involution_firstrighttable)) /\ exists ff_q_pvs_inverse_involution_firstrighttableentrynegative. dst_negative_code_inverse_involution_firstrighttable = ff_q_pvs_inverse_involution_firstrighttableentrynegative * S ((S (dst_index_inverse_involution_firstrighttable)) * dst_negative_scale_inverse_involution_firstrighttable) + (dst_negative_inverse_involution_firstrighttable))) /\ (exists ge_balance_positive_inverse_involution_firstrighttableentryvalue ge_balance_negative_inverse_involution_firstrighttableentryvalue. (((((dst_value_inverse_involution_firstrighttable) = 2 * (ge_balance_positive_inverse_involution_firstrighttableentryvalue) /\ (ge_balance_negative_inverse_involution_firstrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrighttableentryvaluedecode. (((dst_value_inverse_involution_firstrighttable) = 2 * ge_signed_half_inverse_involution_firstrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrighttableentryvalue) = S ge_signed_half_inverse_involution_firstrighttableentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstrighttable) + ge_balance_negative_inverse_involution_firstrighttableentryvalue = (dst_negative_inverse_involution_firstrighttable) + ge_balance_positive_inverse_involution_firstrighttableentryvalue))))))))) /\ (forall dc_input_inverse_involution_firstright dc_output_inverse_involution_firstright. ~(dc_input_inverse_involution_firstright=0) -> (exists pvs_le_gap_inverse_involution_firstrightdomain. pvs_le_gap_inverse_involution_firstrightdomain + (dc_input_inverse_involution_firstright) = (N)) -> (exists dst_positive_code_inverse_involution_firstrightlookup dst_positive_scale_inverse_involution_firstrightlookup dst_negative_code_inverse_involution_firstrightlookup dst_negative_scale_inverse_involution_firstrightlookup dst_positive_inverse_involution_firstrightlookup dst_negative_inverse_involution_firstrightlookup. (((di_delta_inverse_involution_first) = (((((dst_positive_code_inverse_involution_firstrightlookup) + (dst_positive_scale_inverse_involution_firstrightlookup)) * S ((dst_positive_code_inverse_involution_firstrightlookup) + (dst_positive_scale_inverse_involution_firstrightlookup)) + ((dst_positive_scale_inverse_involution_firstrightlookup) + (dst_positive_scale_inverse_involution_firstrightlookup))) + (((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) * S ((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) + ((dst_negative_scale_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)))) * S ((((dst_positive_code_inverse_involution_firstrightlookup) + (dst_positive_scale_inverse_involution_firstrightlookup)) * S ((dst_positive_code_inverse_involution_firstrightlookup) + (dst_positive_scale_inverse_involution_firstrightlookup)) + ((dst_positive_scale_inverse_involution_firstrightlookup) + (dst_positive_scale_inverse_involution_firstrightlookup))) + (((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) * S ((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) + ((dst_negative_scale_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)))) + ((((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) * S ((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) + ((dst_negative_scale_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup))) + (((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) * S ((dst_negative_code_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)) + ((dst_negative_scale_inverse_involution_firstrightlookup) + (dst_negative_scale_inverse_involution_firstrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightlookuppositive. ff_h_pvs_inverse_involution_firstrightlookuppositive + S (dst_positive_inverse_involution_firstrightlookup) = S ((S (dc_input_inverse_involution_firstright)) * dst_positive_scale_inverse_involution_firstrightlookup)) /\ exists ff_q_pvs_inverse_involution_firstrightlookuppositive. dst_positive_code_inverse_involution_firstrightlookup = ff_q_pvs_inverse_involution_firstrightlookuppositive * S ((S (dc_input_inverse_involution_firstright)) * dst_positive_scale_inverse_involution_firstrightlookup) + (dst_positive_inverse_involution_firstrightlookup))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightlookupnegative. ff_h_pvs_inverse_involution_firstrightlookupnegative + S (dst_negative_inverse_involution_firstrightlookup) = S ((S (dc_input_inverse_involution_firstright)) * dst_negative_scale_inverse_involution_firstrightlookup)) /\ exists ff_q_pvs_inverse_involution_firstrightlookupnegative. dst_negative_code_inverse_involution_firstrightlookup = ff_q_pvs_inverse_involution_firstrightlookupnegative * S ((S (dc_input_inverse_involution_firstright)) * dst_negative_scale_inverse_involution_firstrightlookup) + (dst_negative_inverse_involution_firstrightlookup))) /\ (exists ge_balance_positive_inverse_involution_firstrightlookupvalue ge_balance_negative_inverse_involution_firstrightlookupvalue. (((((dc_output_inverse_involution_firstright) = 2 * (ge_balance_positive_inverse_involution_firstrightlookupvalue) /\ (ge_balance_negative_inverse_involution_firstrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightlookupvaluedecode. (((dc_output_inverse_involution_firstright) = 2 * ge_signed_half_inverse_involution_firstrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightlookupvalue) = S ge_signed_half_inverse_involution_firstrightlookupvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightlookup) + ge_balance_negative_inverse_involution_firstrightlookupvalue = (dst_negative_inverse_involution_firstrightlookup) + ge_balance_positive_inverse_involution_firstrightlookupvalue))))))))) -> (((~((dc_input_inverse_involution_firstright)=0)) /\ (exists dc_mask_inverse_involution_firstrightvalue. ((((exists dst_positive_code_inverse_involution_firstrightvaluemasktable dst_positive_scale_inverse_involution_firstrightvaluemasktable dst_negative_code_inverse_involution_firstrightvaluemasktable dst_negative_scale_inverse_involution_firstrightvaluemasktable. (((dc_mask_inverse_involution_firstrightvalue) = (((((dst_positive_code_inverse_involution_firstrightvaluemasktable) + (dst_positive_scale_inverse_involution_firstrightvaluemasktable)) * S ((dst_positive_code_inverse_involution_firstrightvaluemasktable) + (dst_positive_scale_inverse_involution_firstrightvaluemasktable)) + ((dst_positive_scale_inverse_involution_firstrightvaluemasktable) + (dst_positive_scale_inverse_involution_firstrightvaluemasktable))) + (((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)))) * S ((((dst_positive_code_inverse_involution_firstrightvaluemasktable) + (dst_positive_scale_inverse_involution_firstrightvaluemasktable)) * S ((dst_positive_code_inverse_involution_firstrightvaluemasktable) + (dst_positive_scale_inverse_involution_firstrightvaluemasktable)) + ((dst_positive_scale_inverse_involution_firstrightvaluemasktable) + (dst_positive_scale_inverse_involution_firstrightvaluemasktable))) + (((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)))) + ((((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable))) + (((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasktable) + (dst_negative_scale_inverse_involution_firstrightvaluemasktable)))))) /\ (forall dst_index_inverse_involution_firstrightvaluemasktable. (exists pvs_le_gap_inverse_involution_firstrightvaluemasktabledomain. pvs_le_gap_inverse_involution_firstrightvaluemasktabledomain + (dst_index_inverse_involution_firstrightvaluemasktable) = (dc_input_inverse_involution_firstright)) -> exists dst_positive_inverse_involution_firstrightvaluemasktable dst_negative_inverse_involution_firstrightvaluemasktable dst_value_inverse_involution_firstrightvaluemasktable. ((((exists ff_h_pvs_inverse_involution_firstrightvaluemasktableentrypositive. ff_h_pvs_inverse_involution_firstrightvaluemasktableentrypositive + S (dst_positive_inverse_involution_firstrightvaluemasktable) = S ((S (dst_index_inverse_involution_firstrightvaluemasktable)) * dst_positive_scale_inverse_involution_firstrightvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemasktableentrypositive. dst_positive_code_inverse_involution_firstrightvaluemasktable = ff_q_pvs_inverse_involution_firstrightvaluemasktableentrypositive * S ((S (dst_index_inverse_involution_firstrightvaluemasktable)) * dst_positive_scale_inverse_involution_firstrightvaluemasktable) + (dst_positive_inverse_involution_firstrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemasktableentrynegative. ff_h_pvs_inverse_involution_firstrightvaluemasktableentrynegative + S (dst_negative_inverse_involution_firstrightvaluemasktable) = S ((S (dst_index_inverse_involution_firstrightvaluemasktable)) * dst_negative_scale_inverse_involution_firstrightvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemasktableentrynegative. dst_negative_code_inverse_involution_firstrightvaluemasktable = ff_q_pvs_inverse_involution_firstrightvaluemasktableentrynegative * S ((S (dst_index_inverse_involution_firstrightvaluemasktable)) * dst_negative_scale_inverse_involution_firstrightvaluemasktable) + (dst_negative_inverse_involution_firstrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_involution_firstrightvaluemasktableentryvalue ge_balance_negative_inverse_involution_firstrightvaluemasktableentryvalue. (((((dst_value_inverse_involution_firstrightvaluemasktable) = 2 * (ge_balance_positive_inverse_involution_firstrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_involution_firstrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemasktableentryvaluedecode. (((dst_value_inverse_involution_firstrightvaluemasktable) = 2 * ge_signed_half_inverse_involution_firstrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightvaluemasktableentryvalue) = S ge_signed_half_inverse_involution_firstrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightvaluemasktable) + ge_balance_negative_inverse_involution_firstrightvaluemasktableentryvalue = (dst_negative_inverse_involution_firstrightvaluemasktable) + ge_balance_positive_inverse_involution_firstrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_involution_firstrightvaluemask dc_value_inverse_involution_firstrightvaluemask. (exists pvs_le_gap_inverse_involution_firstrightvaluemaskdomain. pvs_le_gap_inverse_involution_firstrightvaluemaskdomain + (dc_index_inverse_involution_firstrightvaluemask) = (dc_input_inverse_involution_firstright)) -> (exists dst_positive_code_inverse_involution_firstrightvaluemasklookup dst_positive_scale_inverse_involution_firstrightvaluemasklookup dst_negative_code_inverse_involution_firstrightvaluemasklookup dst_negative_scale_inverse_involution_firstrightvaluemasklookup dst_positive_inverse_involution_firstrightvaluemasklookup dst_negative_inverse_involution_firstrightvaluemasklookup. (((dc_mask_inverse_involution_firstrightvalue) = (((((dst_positive_code_inverse_involution_firstrightvaluemasklookup) + (dst_positive_scale_inverse_involution_firstrightvaluemasklookup)) * S ((dst_positive_code_inverse_involution_firstrightvaluemasklookup) + (dst_positive_scale_inverse_involution_firstrightvaluemasklookup)) + ((dst_positive_scale_inverse_involution_firstrightvaluemasklookup) + (dst_positive_scale_inverse_involution_firstrightvaluemasklookup))) + (((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_involution_firstrightvaluemasklookup) + (dst_positive_scale_inverse_involution_firstrightvaluemasklookup)) * S ((dst_positive_code_inverse_involution_firstrightvaluemasklookup) + (dst_positive_scale_inverse_involution_firstrightvaluemasklookup)) + ((dst_positive_scale_inverse_involution_firstrightvaluemasklookup) + (dst_positive_scale_inverse_involution_firstrightvaluemasklookup))) + (((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)))) + ((((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup))) + (((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_firstrightvaluemasklookup) + (dst_negative_scale_inverse_involution_firstrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemasklookuppositive. ff_h_pvs_inverse_involution_firstrightvaluemasklookuppositive + S (dst_positive_inverse_involution_firstrightvaluemasklookup) = S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_positive_scale_inverse_involution_firstrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemasklookuppositive. dst_positive_code_inverse_involution_firstrightvaluemasklookup = ff_q_pvs_inverse_involution_firstrightvaluemasklookuppositive * S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_positive_scale_inverse_involution_firstrightvaluemasklookup) + (dst_positive_inverse_involution_firstrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemasklookupnegative. ff_h_pvs_inverse_involution_firstrightvaluemasklookupnegative + S (dst_negative_inverse_involution_firstrightvaluemasklookup) = S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_negative_scale_inverse_involution_firstrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemasklookupnegative. dst_negative_code_inverse_involution_firstrightvaluemasklookup = ff_q_pvs_inverse_involution_firstrightvaluemasklookupnegative * S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_negative_scale_inverse_involution_firstrightvaluemasklookup) + (dst_negative_inverse_involution_firstrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_involution_firstrightvaluemasklookupvalue ge_balance_negative_inverse_involution_firstrightvaluemasklookupvalue. (((((dc_value_inverse_involution_firstrightvaluemask) = 2 * (ge_balance_positive_inverse_involution_firstrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_involution_firstrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemasklookupvaluedecode. (((dc_value_inverse_involution_firstrightvaluemask) = 2 * ge_signed_half_inverse_involution_firstrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightvaluemasklookupvalue) = S ge_signed_half_inverse_involution_firstrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightvaluemasklookup) + ge_balance_negative_inverse_involution_firstrightvaluemasklookupvalue = (dst_negative_inverse_involution_firstrightvaluemasklookup) + ge_balance_positive_inverse_involution_firstrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_involution_firstrightvaluemask)=0)) /\ (exists dc_quotient_inverse_involution_firstrightvaluemaskentry dc_left_inverse_involution_firstrightvaluemaskentry dc_right_inverse_involution_firstrightvaluemaskentry. (((dc_input_inverse_involution_firstright)=(dc_index_inverse_involution_firstrightvaluemask)*dc_quotient_inverse_involution_firstrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_involution_firstrightvaluemaskentryleft dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft dst_negative_code_inverse_involution_firstrightvaluemaskentryleft dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft dst_positive_inverse_involution_firstrightvaluemaskentryleft dst_negative_inverse_involution_firstrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemaskentryleftpositive. ff_h_pvs_inverse_involution_firstrightvaluemaskentryleftpositive + S (dst_positive_inverse_involution_firstrightvaluemaskentryleft) = S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemaskentryleftpositive. dst_positive_code_inverse_involution_firstrightvaluemaskentryleft = ff_q_pvs_inverse_involution_firstrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_positive_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_positive_inverse_involution_firstrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemaskentryleftnegative. ff_h_pvs_inverse_involution_firstrightvaluemaskentryleftnegative + S (dst_negative_inverse_involution_firstrightvaluemaskentryleft) = S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemaskentryleftnegative. dst_negative_code_inverse_involution_firstrightvaluemaskentryleft = ff_q_pvs_inverse_involution_firstrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_involution_firstrightvaluemask)) * dst_negative_scale_inverse_involution_firstrightvaluemaskentryleft) + (dst_negative_inverse_involution_firstrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_involution_firstrightvaluemaskentryleftvalue ge_balance_negative_inverse_involution_firstrightvaluemaskentryleftvalue. (((((dc_left_inverse_involution_firstrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_firstrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_involution_firstrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_involution_firstrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_involution_firstrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightvaluemaskentryleft) + ge_balance_negative_inverse_involution_firstrightvaluemaskentryleftvalue = (dst_negative_inverse_involution_firstrightvaluemaskentryleft) + ge_balance_positive_inverse_involution_firstrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_firstrightvaluemaskentryright dst_positive_scale_inverse_involution_firstrightvaluemaskentryright dst_negative_code_inverse_involution_firstrightvaluemaskentryright dst_negative_scale_inverse_involution_firstrightvaluemaskentryright dst_positive_inverse_involution_firstrightvaluemaskentryright dst_negative_inverse_involution_firstrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryright))) + (((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_firstrightvaluemaskentryright))) + (((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright))) + (((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemaskentryrightpositive. ff_h_pvs_inverse_involution_firstrightvaluemaskentryrightpositive + S (dst_positive_inverse_involution_firstrightvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_firstrightvaluemaskentry)) * dst_positive_scale_inverse_involution_firstrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemaskentryrightpositive. dst_positive_code_inverse_involution_firstrightvaluemaskentryright = ff_q_pvs_inverse_involution_firstrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_involution_firstrightvaluemaskentry)) * dst_positive_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_positive_inverse_involution_firstrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_involution_firstrightvaluemaskentryrightnegative. ff_h_pvs_inverse_involution_firstrightvaluemaskentryrightnegative + S (dst_negative_inverse_involution_firstrightvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_firstrightvaluemaskentry)) * dst_negative_scale_inverse_involution_firstrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_firstrightvaluemaskentryrightnegative. dst_negative_code_inverse_involution_firstrightvaluemaskentryright = ff_q_pvs_inverse_involution_firstrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_involution_firstrightvaluemaskentry)) * dst_negative_scale_inverse_involution_firstrightvaluemaskentryright) + (dst_negative_inverse_involution_firstrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_involution_firstrightvaluemaskentryrightvalue ge_balance_negative_inverse_involution_firstrightvaluemaskentryrightvalue. (((((dc_right_inverse_involution_firstrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_firstrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_involution_firstrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_involution_firstrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_involution_firstrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_involution_firstrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_involution_firstrightvaluemaskentryright) + ge_balance_negative_inverse_involution_firstrightvaluemaskentryrightvalue = (dst_negative_inverse_involution_firstrightvaluemaskentryright) + ge_balance_positive_inverse_involution_firstrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_involution_firstrightvaluemaskentryproduct sto_an_inverse_involution_firstrightvaluemaskentryproduct sto_bp_inverse_involution_firstrightvaluemaskentryproduct sto_bn_inverse_involution_firstrightvaluemaskentryproduct sto_cp_inverse_involution_firstrightvaluemaskentryproduct sto_cn_inverse_involution_firstrightvaluemaskentryproduct. (((((dc_left_inverse_involution_firstrightvaluemaskentry) = 2 * (sto_ap_inverse_involution_firstrightvaluemaskentryproduct) /\ (sto_an_inverse_involution_firstrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemaskentryproductleft. (((dc_left_inverse_involution_firstrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_involution_firstrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_involution_firstrightvaluemaskentryproduct) = S ge_signed_half_inverse_involution_firstrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_involution_firstrightvaluemaskentry) = 2 * (sto_bp_inverse_involution_firstrightvaluemaskentryproduct) /\ (sto_bn_inverse_involution_firstrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemaskentryproductright. (((dc_right_inverse_involution_firstrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_firstrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_involution_firstrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_involution_firstrightvaluemaskentryproduct) = S ge_signed_half_inverse_involution_firstrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_involution_firstrightvaluemask) = 2 * (sto_cp_inverse_involution_firstrightvaluemaskentryproduct) /\ (sto_cn_inverse_involution_firstrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluemaskentryproductoutput. (((dc_value_inverse_involution_firstrightvaluemask) = 2 * ge_signed_half_inverse_involution_firstrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_involution_firstrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_involution_firstrightvaluemaskentryproduct) = S ge_signed_half_inverse_involution_firstrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_involution_firstrightvaluemaskentryproduct * sto_bp_inverse_involution_firstrightvaluemaskentryproduct + sto_an_inverse_involution_firstrightvaluemaskentryproduct * sto_bn_inverse_involution_firstrightvaluemaskentryproduct) + sto_cn_inverse_involution_firstrightvaluemaskentryproduct = (sto_ap_inverse_involution_firstrightvaluemaskentryproduct * sto_bn_inverse_involution_firstrightvaluemaskentryproduct + sto_an_inverse_involution_firstrightvaluemaskentryproduct * sto_bp_inverse_involution_firstrightvaluemaskentryproduct) + sto_cp_inverse_involution_firstrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_involution_firstrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_involution_firstrightvaluemaskentrynondivisor. (dc_input_inverse_involution_firstright) = (dc_index_inverse_involution_firstrightvaluemask) * pvs_factor_inverse_involution_firstrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_involution_firstrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_involution_firstrightvaluefold dst_positive_scale_inverse_involution_firstrightvaluefold dst_negative_code_inverse_involution_firstrightvaluefold dst_negative_scale_inverse_involution_firstrightvaluefold dst_positive_sum_inverse_involution_firstrightvaluefold dst_negative_sum_inverse_involution_firstrightvaluefold. (((dc_mask_inverse_involution_firstrightvalue) = (((((dst_positive_code_inverse_involution_firstrightvaluefold) + (dst_positive_scale_inverse_involution_firstrightvaluefold)) * S ((dst_positive_code_inverse_involution_firstrightvaluefold) + (dst_positive_scale_inverse_involution_firstrightvaluefold)) + ((dst_positive_scale_inverse_involution_firstrightvaluefold) + (dst_positive_scale_inverse_involution_firstrightvaluefold))) + (((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) * S ((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) + ((dst_negative_scale_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)))) * S ((((dst_positive_code_inverse_involution_firstrightvaluefold) + (dst_positive_scale_inverse_involution_firstrightvaluefold)) * S ((dst_positive_code_inverse_involution_firstrightvaluefold) + (dst_positive_scale_inverse_involution_firstrightvaluefold)) + ((dst_positive_scale_inverse_involution_firstrightvaluefold) + (dst_positive_scale_inverse_involution_firstrightvaluefold))) + (((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) * S ((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) + ((dst_negative_scale_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)))) + ((((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) * S ((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) + ((dst_negative_scale_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold))) + (((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) * S ((dst_negative_code_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)) + ((dst_negative_scale_inverse_involution_firstrightvaluefold) + (dst_negative_scale_inverse_involution_firstrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_involution_firstrightvaluefoldpositive fs_v_dst_inverse_involution_firstrightvaluefoldpositive. ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_start. fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_start. fs_u_dst_inverse_involution_firstrightvaluefoldpositive = fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_involution_firstrightvaluefold) = S ((S (S (dc_input_inverse_involution_firstright))) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_involution_firstrightvaluefoldpositive = fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_involution_firstright))) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive) + (dst_positive_sum_inverse_involution_firstrightvaluefold))) /\ forall fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps = S (dc_input_inverse_involution_firstright)) -> exists fs_a_dst_inverse_involution_firstrightvaluefoldpositive_body_steps fs_r_dst_inverse_involution_firstrightvaluefoldpositive_body_steps fs_s_dst_inverse_involution_firstrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_involution_firstrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_firstrightvaluefold)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_involution_firstrightvaluefold = fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_firstrightvaluefold) + (fs_a_dst_inverse_involution_firstrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_involution_firstrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_involution_firstrightvaluefoldpositive = fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive) + (fs_r_dst_inverse_involution_firstrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_involution_firstrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_involution_firstrightvaluefoldpositive = fs_q_dst_inverse_involution_firstrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldpositive) + (fs_s_dst_inverse_involution_firstrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_involution_firstrightvaluefoldpositive_body_steps = fs_r_dst_inverse_involution_firstrightvaluefoldpositive_body_steps + fs_a_dst_inverse_involution_firstrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_involution_firstrightvaluefoldnegative fs_v_dst_inverse_involution_firstrightvaluefoldnegative. ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_start. fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_start. fs_u_dst_inverse_involution_firstrightvaluefoldnegative = fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_involution_firstrightvaluefold) = S ((S (S (dc_input_inverse_involution_firstright))) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_involution_firstrightvaluefoldnegative = fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_involution_firstright))) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative) + (dst_negative_sum_inverse_involution_firstrightvaluefold))) /\ forall fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps = S (dc_input_inverse_involution_firstright)) -> exists fs_a_dst_inverse_involution_firstrightvaluefoldnegative_body_steps fs_r_dst_inverse_involution_firstrightvaluefoldnegative_body_steps fs_s_dst_inverse_involution_firstrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_involution_firstrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_firstrightvaluefold)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_involution_firstrightvaluefold = fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_firstrightvaluefold) + (fs_a_dst_inverse_involution_firstrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_involution_firstrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_involution_firstrightvaluefoldnegative = fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative) + (fs_r_dst_inverse_involution_firstrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_involution_firstrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_involution_firstrightvaluefoldnegative = fs_q_dst_inverse_involution_firstrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_firstrightvaluefoldnegative) + (fs_s_dst_inverse_involution_firstrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_involution_firstrightvaluefoldnegative_body_steps = fs_r_dst_inverse_involution_firstrightvaluefoldnegative_body_steps + fs_a_dst_inverse_involution_firstrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_involution_firstrightvaluefoldresult ge_balance_negative_inverse_involution_firstrightvaluefoldresult. (((((dc_output_inverse_involution_firstright) = 2 * (ge_balance_positive_inverse_involution_firstrightvaluefoldresult) /\ (ge_balance_negative_inverse_involution_firstrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_involution_firstrightvaluefoldresultdecode. (((dc_output_inverse_involution_firstright) = 2 * ge_signed_half_inverse_involution_firstrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_involution_firstrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_involution_firstrightvaluefoldresult) = S ge_signed_half_inverse_involution_firstrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_involution_firstrightvaluefold) + ge_balance_negative_inverse_involution_firstrightvaluefoldresult = (dst_negative_sum_inverse_involution_firstrightvaluefold) + ge_balance_positive_inverse_involution_firstrightvaluefoldresult)))))))))))))))))))))))) -> (exists di_delta_inverse_involution_second. ((((exists dst_positive_code_inverse_involution_seconddeltatable dst_positive_scale_inverse_involution_seconddeltatable dst_negative_code_inverse_involution_seconddeltatable dst_negative_scale_inverse_involution_seconddeltatable. (((di_delta_inverse_involution_second) = (((((dst_positive_code_inverse_involution_seconddeltatable) + (dst_positive_scale_inverse_involution_seconddeltatable)) * S ((dst_positive_code_inverse_involution_seconddeltatable) + (dst_positive_scale_inverse_involution_seconddeltatable)) + ((dst_positive_scale_inverse_involution_seconddeltatable) + (dst_positive_scale_inverse_involution_seconddeltatable))) + (((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) * S ((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) + ((dst_negative_scale_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)))) * S ((((dst_positive_code_inverse_involution_seconddeltatable) + (dst_positive_scale_inverse_involution_seconddeltatable)) * S ((dst_positive_code_inverse_involution_seconddeltatable) + (dst_positive_scale_inverse_involution_seconddeltatable)) + ((dst_positive_scale_inverse_involution_seconddeltatable) + (dst_positive_scale_inverse_involution_seconddeltatable))) + (((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) * S ((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) + ((dst_negative_scale_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)))) + ((((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) * S ((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) + ((dst_negative_scale_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable))) + (((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) * S ((dst_negative_code_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)) + ((dst_negative_scale_inverse_involution_seconddeltatable) + (dst_negative_scale_inverse_involution_seconddeltatable)))))) /\ (forall dst_index_inverse_involution_seconddeltatable. (exists pvs_le_gap_inverse_involution_seconddeltatabledomain. pvs_le_gap_inverse_involution_seconddeltatabledomain + (dst_index_inverse_involution_seconddeltatable) = (N)) -> exists dst_positive_inverse_involution_seconddeltatable dst_negative_inverse_involution_seconddeltatable dst_value_inverse_involution_seconddeltatable. ((((exists ff_h_pvs_inverse_involution_seconddeltatableentrypositive. ff_h_pvs_inverse_involution_seconddeltatableentrypositive + S (dst_positive_inverse_involution_seconddeltatable) = S ((S (dst_index_inverse_involution_seconddeltatable)) * dst_positive_scale_inverse_involution_seconddeltatable)) /\ exists ff_q_pvs_inverse_involution_seconddeltatableentrypositive. dst_positive_code_inverse_involution_seconddeltatable = ff_q_pvs_inverse_involution_seconddeltatableentrypositive * S ((S (dst_index_inverse_involution_seconddeltatable)) * dst_positive_scale_inverse_involution_seconddeltatable) + (dst_positive_inverse_involution_seconddeltatable))) /\ (((((exists ff_h_pvs_inverse_involution_seconddeltatableentrynegative. ff_h_pvs_inverse_involution_seconddeltatableentrynegative + S (dst_negative_inverse_involution_seconddeltatable) = S ((S (dst_index_inverse_involution_seconddeltatable)) * dst_negative_scale_inverse_involution_seconddeltatable)) /\ exists ff_q_pvs_inverse_involution_seconddeltatableentrynegative. dst_negative_code_inverse_involution_seconddeltatable = ff_q_pvs_inverse_involution_seconddeltatableentrynegative * S ((S (dst_index_inverse_involution_seconddeltatable)) * dst_negative_scale_inverse_involution_seconddeltatable) + (dst_negative_inverse_involution_seconddeltatable))) /\ (exists ge_balance_positive_inverse_involution_seconddeltatableentryvalue ge_balance_negative_inverse_involution_seconddeltatableentryvalue. (((((dst_value_inverse_involution_seconddeltatable) = 2 * (ge_balance_positive_inverse_involution_seconddeltatableentryvalue) /\ (ge_balance_negative_inverse_involution_seconddeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_seconddeltatableentryvaluedecode. (((dst_value_inverse_involution_seconddeltatable) = 2 * ge_signed_half_inverse_involution_seconddeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_seconddeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_seconddeltatableentryvalue) = S ge_signed_half_inverse_involution_seconddeltatableentryvaluedecode))) /\ ((dst_positive_inverse_involution_seconddeltatable) + ge_balance_negative_inverse_involution_seconddeltatableentryvalue = (dst_negative_inverse_involution_seconddeltatable) + ge_balance_positive_inverse_involution_seconddeltatableentryvalue))))))))) /\ (forall du_index_inverse_involution_seconddelta du_value_inverse_involution_seconddelta. ~(du_index_inverse_involution_seconddelta=0) -> (exists pvs_le_gap_inverse_involution_seconddeltabound. pvs_le_gap_inverse_involution_seconddeltabound + (du_index_inverse_involution_seconddelta) = (N)) -> (exists dst_positive_code_inverse_involution_seconddeltaentry dst_positive_scale_inverse_involution_seconddeltaentry dst_negative_code_inverse_involution_seconddeltaentry dst_negative_scale_inverse_involution_seconddeltaentry dst_positive_inverse_involution_seconddeltaentry dst_negative_inverse_involution_seconddeltaentry. (((di_delta_inverse_involution_second) = (((((dst_positive_code_inverse_involution_seconddeltaentry) + (dst_positive_scale_inverse_involution_seconddeltaentry)) * S ((dst_positive_code_inverse_involution_seconddeltaentry) + (dst_positive_scale_inverse_involution_seconddeltaentry)) + ((dst_positive_scale_inverse_involution_seconddeltaentry) + (dst_positive_scale_inverse_involution_seconddeltaentry))) + (((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) * S ((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) + ((dst_negative_scale_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)))) * S ((((dst_positive_code_inverse_involution_seconddeltaentry) + (dst_positive_scale_inverse_involution_seconddeltaentry)) * S ((dst_positive_code_inverse_involution_seconddeltaentry) + (dst_positive_scale_inverse_involution_seconddeltaentry)) + ((dst_positive_scale_inverse_involution_seconddeltaentry) + (dst_positive_scale_inverse_involution_seconddeltaentry))) + (((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) * S ((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) + ((dst_negative_scale_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)))) + ((((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) * S ((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) + ((dst_negative_scale_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry))) + (((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) * S ((dst_negative_code_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)) + ((dst_negative_scale_inverse_involution_seconddeltaentry) + (dst_negative_scale_inverse_involution_seconddeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_involution_seconddeltaentrypositive. ff_h_pvs_inverse_involution_seconddeltaentrypositive + S (dst_positive_inverse_involution_seconddeltaentry) = S ((S (du_index_inverse_involution_seconddelta)) * dst_positive_scale_inverse_involution_seconddeltaentry)) /\ exists ff_q_pvs_inverse_involution_seconddeltaentrypositive. dst_positive_code_inverse_involution_seconddeltaentry = ff_q_pvs_inverse_involution_seconddeltaentrypositive * S ((S (du_index_inverse_involution_seconddelta)) * dst_positive_scale_inverse_involution_seconddeltaentry) + (dst_positive_inverse_involution_seconddeltaentry))) /\ (((((exists ff_h_pvs_inverse_involution_seconddeltaentrynegative. ff_h_pvs_inverse_involution_seconddeltaentrynegative + S (dst_negative_inverse_involution_seconddeltaentry) = S ((S (du_index_inverse_involution_seconddelta)) * dst_negative_scale_inverse_involution_seconddeltaentry)) /\ exists ff_q_pvs_inverse_involution_seconddeltaentrynegative. dst_negative_code_inverse_involution_seconddeltaentry = ff_q_pvs_inverse_involution_seconddeltaentrynegative * S ((S (du_index_inverse_involution_seconddelta)) * dst_negative_scale_inverse_involution_seconddeltaentry) + (dst_negative_inverse_involution_seconddeltaentry))) /\ (exists ge_balance_positive_inverse_involution_seconddeltaentryvalue ge_balance_negative_inverse_involution_seconddeltaentryvalue. (((((du_value_inverse_involution_seconddelta) = 2 * (ge_balance_positive_inverse_involution_seconddeltaentryvalue) /\ (ge_balance_negative_inverse_involution_seconddeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_seconddeltaentryvaluedecode. (((du_value_inverse_involution_seconddelta) = 2 * ge_signed_half_inverse_involution_seconddeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_seconddeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_seconddeltaentryvalue) = S ge_signed_half_inverse_involution_seconddeltaentryvaluedecode))) /\ ((dst_positive_inverse_involution_seconddeltaentry) + ge_balance_negative_inverse_involution_seconddeltaentryvalue = (dst_negative_inverse_involution_seconddeltaentry) + ge_balance_positive_inverse_involution_seconddeltaentryvalue))))))))) -> ((((du_index_inverse_involution_seconddelta)=1 -> (du_value_inverse_involution_seconddelta)=2) /\ (~((du_index_inverse_involution_seconddelta)=1) -> (du_value_inverse_involution_seconddelta)=0)))))) /\ (((((exists dst_positive_code_inverse_involution_secondleftleft dst_positive_scale_inverse_involution_secondleftleft dst_negative_code_inverse_involution_secondleftleft dst_negative_scale_inverse_involution_secondleftleft. (((G) = (((((dst_positive_code_inverse_involution_secondleftleft) + (dst_positive_scale_inverse_involution_secondleftleft)) * S ((dst_positive_code_inverse_involution_secondleftleft) + (dst_positive_scale_inverse_involution_secondleftleft)) + ((dst_positive_scale_inverse_involution_secondleftleft) + (dst_positive_scale_inverse_involution_secondleftleft))) + (((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) * S ((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) + ((dst_negative_scale_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)))) * S ((((dst_positive_code_inverse_involution_secondleftleft) + (dst_positive_scale_inverse_involution_secondleftleft)) * S ((dst_positive_code_inverse_involution_secondleftleft) + (dst_positive_scale_inverse_involution_secondleftleft)) + ((dst_positive_scale_inverse_involution_secondleftleft) + (dst_positive_scale_inverse_involution_secondleftleft))) + (((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) * S ((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) + ((dst_negative_scale_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)))) + ((((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) * S ((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) + ((dst_negative_scale_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft))) + (((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) * S ((dst_negative_code_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)) + ((dst_negative_scale_inverse_involution_secondleftleft) + (dst_negative_scale_inverse_involution_secondleftleft)))))) /\ (forall dst_index_inverse_involution_secondleftleft. (exists pvs_le_gap_inverse_involution_secondleftleftdomain. pvs_le_gap_inverse_involution_secondleftleftdomain + (dst_index_inverse_involution_secondleftleft) = (N)) -> exists dst_positive_inverse_involution_secondleftleft dst_negative_inverse_involution_secondleftleft dst_value_inverse_involution_secondleftleft. ((((exists ff_h_pvs_inverse_involution_secondleftleftentrypositive. ff_h_pvs_inverse_involution_secondleftleftentrypositive + S (dst_positive_inverse_involution_secondleftleft) = S ((S (dst_index_inverse_involution_secondleftleft)) * dst_positive_scale_inverse_involution_secondleftleft)) /\ exists ff_q_pvs_inverse_involution_secondleftleftentrypositive. dst_positive_code_inverse_involution_secondleftleft = ff_q_pvs_inverse_involution_secondleftleftentrypositive * S ((S (dst_index_inverse_involution_secondleftleft)) * dst_positive_scale_inverse_involution_secondleftleft) + (dst_positive_inverse_involution_secondleftleft))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftleftentrynegative. ff_h_pvs_inverse_involution_secondleftleftentrynegative + S (dst_negative_inverse_involution_secondleftleft) = S ((S (dst_index_inverse_involution_secondleftleft)) * dst_negative_scale_inverse_involution_secondleftleft)) /\ exists ff_q_pvs_inverse_involution_secondleftleftentrynegative. dst_negative_code_inverse_involution_secondleftleft = ff_q_pvs_inverse_involution_secondleftleftentrynegative * S ((S (dst_index_inverse_involution_secondleftleft)) * dst_negative_scale_inverse_involution_secondleftleft) + (dst_negative_inverse_involution_secondleftleft))) /\ (exists ge_balance_positive_inverse_involution_secondleftleftentryvalue ge_balance_negative_inverse_involution_secondleftleftentryvalue. (((((dst_value_inverse_involution_secondleftleft) = 2 * (ge_balance_positive_inverse_involution_secondleftleftentryvalue) /\ (ge_balance_negative_inverse_involution_secondleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftleftentryvaluedecode. (((dst_value_inverse_involution_secondleftleft) = 2 * ge_signed_half_inverse_involution_secondleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftleftentryvalue) = S ge_signed_half_inverse_involution_secondleftleftentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftleft) + ge_balance_negative_inverse_involution_secondleftleftentryvalue = (dst_negative_inverse_involution_secondleftleft) + ge_balance_positive_inverse_involution_secondleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_secondleftright dst_positive_scale_inverse_involution_secondleftright dst_negative_code_inverse_involution_secondleftright dst_negative_scale_inverse_involution_secondleftright. (((H) = (((((dst_positive_code_inverse_involution_secondleftright) + (dst_positive_scale_inverse_involution_secondleftright)) * S ((dst_positive_code_inverse_involution_secondleftright) + (dst_positive_scale_inverse_involution_secondleftright)) + ((dst_positive_scale_inverse_involution_secondleftright) + (dst_positive_scale_inverse_involution_secondleftright))) + (((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) * S ((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) + ((dst_negative_scale_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)))) * S ((((dst_positive_code_inverse_involution_secondleftright) + (dst_positive_scale_inverse_involution_secondleftright)) * S ((dst_positive_code_inverse_involution_secondleftright) + (dst_positive_scale_inverse_involution_secondleftright)) + ((dst_positive_scale_inverse_involution_secondleftright) + (dst_positive_scale_inverse_involution_secondleftright))) + (((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) * S ((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) + ((dst_negative_scale_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)))) + ((((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) * S ((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) + ((dst_negative_scale_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright))) + (((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) * S ((dst_negative_code_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)) + ((dst_negative_scale_inverse_involution_secondleftright) + (dst_negative_scale_inverse_involution_secondleftright)))))) /\ (forall dst_index_inverse_involution_secondleftright. (exists pvs_le_gap_inverse_involution_secondleftrightdomain. pvs_le_gap_inverse_involution_secondleftrightdomain + (dst_index_inverse_involution_secondleftright) = (N)) -> exists dst_positive_inverse_involution_secondleftright dst_negative_inverse_involution_secondleftright dst_value_inverse_involution_secondleftright. ((((exists ff_h_pvs_inverse_involution_secondleftrightentrypositive. ff_h_pvs_inverse_involution_secondleftrightentrypositive + S (dst_positive_inverse_involution_secondleftright) = S ((S (dst_index_inverse_involution_secondleftright)) * dst_positive_scale_inverse_involution_secondleftright)) /\ exists ff_q_pvs_inverse_involution_secondleftrightentrypositive. dst_positive_code_inverse_involution_secondleftright = ff_q_pvs_inverse_involution_secondleftrightentrypositive * S ((S (dst_index_inverse_involution_secondleftright)) * dst_positive_scale_inverse_involution_secondleftright) + (dst_positive_inverse_involution_secondleftright))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftrightentrynegative. ff_h_pvs_inverse_involution_secondleftrightentrynegative + S (dst_negative_inverse_involution_secondleftright) = S ((S (dst_index_inverse_involution_secondleftright)) * dst_negative_scale_inverse_involution_secondleftright)) /\ exists ff_q_pvs_inverse_involution_secondleftrightentrynegative. dst_negative_code_inverse_involution_secondleftright = ff_q_pvs_inverse_involution_secondleftrightentrynegative * S ((S (dst_index_inverse_involution_secondleftright)) * dst_negative_scale_inverse_involution_secondleftright) + (dst_negative_inverse_involution_secondleftright))) /\ (exists ge_balance_positive_inverse_involution_secondleftrightentryvalue ge_balance_negative_inverse_involution_secondleftrightentryvalue. (((((dst_value_inverse_involution_secondleftright) = 2 * (ge_balance_positive_inverse_involution_secondleftrightentryvalue) /\ (ge_balance_negative_inverse_involution_secondleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftrightentryvaluedecode. (((dst_value_inverse_involution_secondleftright) = 2 * ge_signed_half_inverse_involution_secondleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftrightentryvalue) = S ge_signed_half_inverse_involution_secondleftrightentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftright) + ge_balance_negative_inverse_involution_secondleftrightentryvalue = (dst_negative_inverse_involution_secondleftright) + ge_balance_positive_inverse_involution_secondleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_secondlefttable dst_positive_scale_inverse_involution_secondlefttable dst_negative_code_inverse_involution_secondlefttable dst_negative_scale_inverse_involution_secondlefttable. (((di_delta_inverse_involution_second) = (((((dst_positive_code_inverse_involution_secondlefttable) + (dst_positive_scale_inverse_involution_secondlefttable)) * S ((dst_positive_code_inverse_involution_secondlefttable) + (dst_positive_scale_inverse_involution_secondlefttable)) + ((dst_positive_scale_inverse_involution_secondlefttable) + (dst_positive_scale_inverse_involution_secondlefttable))) + (((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) * S ((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) + ((dst_negative_scale_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)))) * S ((((dst_positive_code_inverse_involution_secondlefttable) + (dst_positive_scale_inverse_involution_secondlefttable)) * S ((dst_positive_code_inverse_involution_secondlefttable) + (dst_positive_scale_inverse_involution_secondlefttable)) + ((dst_positive_scale_inverse_involution_secondlefttable) + (dst_positive_scale_inverse_involution_secondlefttable))) + (((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) * S ((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) + ((dst_negative_scale_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)))) + ((((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) * S ((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) + ((dst_negative_scale_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable))) + (((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) * S ((dst_negative_code_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)) + ((dst_negative_scale_inverse_involution_secondlefttable) + (dst_negative_scale_inverse_involution_secondlefttable)))))) /\ (forall dst_index_inverse_involution_secondlefttable. (exists pvs_le_gap_inverse_involution_secondlefttabledomain. pvs_le_gap_inverse_involution_secondlefttabledomain + (dst_index_inverse_involution_secondlefttable) = (N)) -> exists dst_positive_inverse_involution_secondlefttable dst_negative_inverse_involution_secondlefttable dst_value_inverse_involution_secondlefttable. ((((exists ff_h_pvs_inverse_involution_secondlefttableentrypositive. ff_h_pvs_inverse_involution_secondlefttableentrypositive + S (dst_positive_inverse_involution_secondlefttable) = S ((S (dst_index_inverse_involution_secondlefttable)) * dst_positive_scale_inverse_involution_secondlefttable)) /\ exists ff_q_pvs_inverse_involution_secondlefttableentrypositive. dst_positive_code_inverse_involution_secondlefttable = ff_q_pvs_inverse_involution_secondlefttableentrypositive * S ((S (dst_index_inverse_involution_secondlefttable)) * dst_positive_scale_inverse_involution_secondlefttable) + (dst_positive_inverse_involution_secondlefttable))) /\ (((((exists ff_h_pvs_inverse_involution_secondlefttableentrynegative. ff_h_pvs_inverse_involution_secondlefttableentrynegative + S (dst_negative_inverse_involution_secondlefttable) = S ((S (dst_index_inverse_involution_secondlefttable)) * dst_negative_scale_inverse_involution_secondlefttable)) /\ exists ff_q_pvs_inverse_involution_secondlefttableentrynegative. dst_negative_code_inverse_involution_secondlefttable = ff_q_pvs_inverse_involution_secondlefttableentrynegative * S ((S (dst_index_inverse_involution_secondlefttable)) * dst_negative_scale_inverse_involution_secondlefttable) + (dst_negative_inverse_involution_secondlefttable))) /\ (exists ge_balance_positive_inverse_involution_secondlefttableentryvalue ge_balance_negative_inverse_involution_secondlefttableentryvalue. (((((dst_value_inverse_involution_secondlefttable) = 2 * (ge_balance_positive_inverse_involution_secondlefttableentryvalue) /\ (ge_balance_negative_inverse_involution_secondlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondlefttableentryvaluedecode. (((dst_value_inverse_involution_secondlefttable) = 2 * ge_signed_half_inverse_involution_secondlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondlefttableentryvalue) = S ge_signed_half_inverse_involution_secondlefttableentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondlefttable) + ge_balance_negative_inverse_involution_secondlefttableentryvalue = (dst_negative_inverse_involution_secondlefttable) + ge_balance_positive_inverse_involution_secondlefttableentryvalue))))))))) /\ (forall dc_input_inverse_involution_secondleft dc_output_inverse_involution_secondleft. ~(dc_input_inverse_involution_secondleft=0) -> (exists pvs_le_gap_inverse_involution_secondleftdomain. pvs_le_gap_inverse_involution_secondleftdomain + (dc_input_inverse_involution_secondleft) = (N)) -> (exists dst_positive_code_inverse_involution_secondleftlookup dst_positive_scale_inverse_involution_secondleftlookup dst_negative_code_inverse_involution_secondleftlookup dst_negative_scale_inverse_involution_secondleftlookup dst_positive_inverse_involution_secondleftlookup dst_negative_inverse_involution_secondleftlookup. (((di_delta_inverse_involution_second) = (((((dst_positive_code_inverse_involution_secondleftlookup) + (dst_positive_scale_inverse_involution_secondleftlookup)) * S ((dst_positive_code_inverse_involution_secondleftlookup) + (dst_positive_scale_inverse_involution_secondleftlookup)) + ((dst_positive_scale_inverse_involution_secondleftlookup) + (dst_positive_scale_inverse_involution_secondleftlookup))) + (((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) * S ((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) + ((dst_negative_scale_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)))) * S ((((dst_positive_code_inverse_involution_secondleftlookup) + (dst_positive_scale_inverse_involution_secondleftlookup)) * S ((dst_positive_code_inverse_involution_secondleftlookup) + (dst_positive_scale_inverse_involution_secondleftlookup)) + ((dst_positive_scale_inverse_involution_secondleftlookup) + (dst_positive_scale_inverse_involution_secondleftlookup))) + (((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) * S ((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) + ((dst_negative_scale_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)))) + ((((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) * S ((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) + ((dst_negative_scale_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup))) + (((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) * S ((dst_negative_code_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)) + ((dst_negative_scale_inverse_involution_secondleftlookup) + (dst_negative_scale_inverse_involution_secondleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftlookuppositive. ff_h_pvs_inverse_involution_secondleftlookuppositive + S (dst_positive_inverse_involution_secondleftlookup) = S ((S (dc_input_inverse_involution_secondleft)) * dst_positive_scale_inverse_involution_secondleftlookup)) /\ exists ff_q_pvs_inverse_involution_secondleftlookuppositive. dst_positive_code_inverse_involution_secondleftlookup = ff_q_pvs_inverse_involution_secondleftlookuppositive * S ((S (dc_input_inverse_involution_secondleft)) * dst_positive_scale_inverse_involution_secondleftlookup) + (dst_positive_inverse_involution_secondleftlookup))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftlookupnegative. ff_h_pvs_inverse_involution_secondleftlookupnegative + S (dst_negative_inverse_involution_secondleftlookup) = S ((S (dc_input_inverse_involution_secondleft)) * dst_negative_scale_inverse_involution_secondleftlookup)) /\ exists ff_q_pvs_inverse_involution_secondleftlookupnegative. dst_negative_code_inverse_involution_secondleftlookup = ff_q_pvs_inverse_involution_secondleftlookupnegative * S ((S (dc_input_inverse_involution_secondleft)) * dst_negative_scale_inverse_involution_secondleftlookup) + (dst_negative_inverse_involution_secondleftlookup))) /\ (exists ge_balance_positive_inverse_involution_secondleftlookupvalue ge_balance_negative_inverse_involution_secondleftlookupvalue. (((((dc_output_inverse_involution_secondleft) = 2 * (ge_balance_positive_inverse_involution_secondleftlookupvalue) /\ (ge_balance_negative_inverse_involution_secondleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftlookupvaluedecode. (((dc_output_inverse_involution_secondleft) = 2 * ge_signed_half_inverse_involution_secondleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftlookupvalue) = S ge_signed_half_inverse_involution_secondleftlookupvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftlookup) + ge_balance_negative_inverse_involution_secondleftlookupvalue = (dst_negative_inverse_involution_secondleftlookup) + ge_balance_positive_inverse_involution_secondleftlookupvalue))))))))) -> (((~((dc_input_inverse_involution_secondleft)=0)) /\ (exists dc_mask_inverse_involution_secondleftvalue. ((((exists dst_positive_code_inverse_involution_secondleftvaluemasktable dst_positive_scale_inverse_involution_secondleftvaluemasktable dst_negative_code_inverse_involution_secondleftvaluemasktable dst_negative_scale_inverse_involution_secondleftvaluemasktable. (((dc_mask_inverse_involution_secondleftvalue) = (((((dst_positive_code_inverse_involution_secondleftvaluemasktable) + (dst_positive_scale_inverse_involution_secondleftvaluemasktable)) * S ((dst_positive_code_inverse_involution_secondleftvaluemasktable) + (dst_positive_scale_inverse_involution_secondleftvaluemasktable)) + ((dst_positive_scale_inverse_involution_secondleftvaluemasktable) + (dst_positive_scale_inverse_involution_secondleftvaluemasktable))) + (((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)))) * S ((((dst_positive_code_inverse_involution_secondleftvaluemasktable) + (dst_positive_scale_inverse_involution_secondleftvaluemasktable)) * S ((dst_positive_code_inverse_involution_secondleftvaluemasktable) + (dst_positive_scale_inverse_involution_secondleftvaluemasktable)) + ((dst_positive_scale_inverse_involution_secondleftvaluemasktable) + (dst_positive_scale_inverse_involution_secondleftvaluemasktable))) + (((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)))) + ((((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable))) + (((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasktable) + (dst_negative_scale_inverse_involution_secondleftvaluemasktable)))))) /\ (forall dst_index_inverse_involution_secondleftvaluemasktable. (exists pvs_le_gap_inverse_involution_secondleftvaluemasktabledomain. pvs_le_gap_inverse_involution_secondleftvaluemasktabledomain + (dst_index_inverse_involution_secondleftvaluemasktable) = (dc_input_inverse_involution_secondleft)) -> exists dst_positive_inverse_involution_secondleftvaluemasktable dst_negative_inverse_involution_secondleftvaluemasktable dst_value_inverse_involution_secondleftvaluemasktable. ((((exists ff_h_pvs_inverse_involution_secondleftvaluemasktableentrypositive. ff_h_pvs_inverse_involution_secondleftvaluemasktableentrypositive + S (dst_positive_inverse_involution_secondleftvaluemasktable) = S ((S (dst_index_inverse_involution_secondleftvaluemasktable)) * dst_positive_scale_inverse_involution_secondleftvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemasktableentrypositive. dst_positive_code_inverse_involution_secondleftvaluemasktable = ff_q_pvs_inverse_involution_secondleftvaluemasktableentrypositive * S ((S (dst_index_inverse_involution_secondleftvaluemasktable)) * dst_positive_scale_inverse_involution_secondleftvaluemasktable) + (dst_positive_inverse_involution_secondleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemasktableentrynegative. ff_h_pvs_inverse_involution_secondleftvaluemasktableentrynegative + S (dst_negative_inverse_involution_secondleftvaluemasktable) = S ((S (dst_index_inverse_involution_secondleftvaluemasktable)) * dst_negative_scale_inverse_involution_secondleftvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemasktableentrynegative. dst_negative_code_inverse_involution_secondleftvaluemasktable = ff_q_pvs_inverse_involution_secondleftvaluemasktableentrynegative * S ((S (dst_index_inverse_involution_secondleftvaluemasktable)) * dst_negative_scale_inverse_involution_secondleftvaluemasktable) + (dst_negative_inverse_involution_secondleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_involution_secondleftvaluemasktableentryvalue ge_balance_negative_inverse_involution_secondleftvaluemasktableentryvalue. (((((dst_value_inverse_involution_secondleftvaluemasktable) = 2 * (ge_balance_positive_inverse_involution_secondleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_involution_secondleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemasktableentryvaluedecode. (((dst_value_inverse_involution_secondleftvaluemasktable) = 2 * ge_signed_half_inverse_involution_secondleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftvaluemasktableentryvalue) = S ge_signed_half_inverse_involution_secondleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftvaluemasktable) + ge_balance_negative_inverse_involution_secondleftvaluemasktableentryvalue = (dst_negative_inverse_involution_secondleftvaluemasktable) + ge_balance_positive_inverse_involution_secondleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_involution_secondleftvaluemask dc_value_inverse_involution_secondleftvaluemask. (exists pvs_le_gap_inverse_involution_secondleftvaluemaskdomain. pvs_le_gap_inverse_involution_secondleftvaluemaskdomain + (dc_index_inverse_involution_secondleftvaluemask) = (dc_input_inverse_involution_secondleft)) -> (exists dst_positive_code_inverse_involution_secondleftvaluemasklookup dst_positive_scale_inverse_involution_secondleftvaluemasklookup dst_negative_code_inverse_involution_secondleftvaluemasklookup dst_negative_scale_inverse_involution_secondleftvaluemasklookup dst_positive_inverse_involution_secondleftvaluemasklookup dst_negative_inverse_involution_secondleftvaluemasklookup. (((dc_mask_inverse_involution_secondleftvalue) = (((((dst_positive_code_inverse_involution_secondleftvaluemasklookup) + (dst_positive_scale_inverse_involution_secondleftvaluemasklookup)) * S ((dst_positive_code_inverse_involution_secondleftvaluemasklookup) + (dst_positive_scale_inverse_involution_secondleftvaluemasklookup)) + ((dst_positive_scale_inverse_involution_secondleftvaluemasklookup) + (dst_positive_scale_inverse_involution_secondleftvaluemasklookup))) + (((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_involution_secondleftvaluemasklookup) + (dst_positive_scale_inverse_involution_secondleftvaluemasklookup)) * S ((dst_positive_code_inverse_involution_secondleftvaluemasklookup) + (dst_positive_scale_inverse_involution_secondleftvaluemasklookup)) + ((dst_positive_scale_inverse_involution_secondleftvaluemasklookup) + (dst_positive_scale_inverse_involution_secondleftvaluemasklookup))) + (((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)))) + ((((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup))) + (((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondleftvaluemasklookup) + (dst_negative_scale_inverse_involution_secondleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemasklookuppositive. ff_h_pvs_inverse_involution_secondleftvaluemasklookuppositive + S (dst_positive_inverse_involution_secondleftvaluemasklookup) = S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_positive_scale_inverse_involution_secondleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemasklookuppositive. dst_positive_code_inverse_involution_secondleftvaluemasklookup = ff_q_pvs_inverse_involution_secondleftvaluemasklookuppositive * S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_positive_scale_inverse_involution_secondleftvaluemasklookup) + (dst_positive_inverse_involution_secondleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemasklookupnegative. ff_h_pvs_inverse_involution_secondleftvaluemasklookupnegative + S (dst_negative_inverse_involution_secondleftvaluemasklookup) = S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_negative_scale_inverse_involution_secondleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemasklookupnegative. dst_negative_code_inverse_involution_secondleftvaluemasklookup = ff_q_pvs_inverse_involution_secondleftvaluemasklookupnegative * S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_negative_scale_inverse_involution_secondleftvaluemasklookup) + (dst_negative_inverse_involution_secondleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_involution_secondleftvaluemasklookupvalue ge_balance_negative_inverse_involution_secondleftvaluemasklookupvalue. (((((dc_value_inverse_involution_secondleftvaluemask) = 2 * (ge_balance_positive_inverse_involution_secondleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_involution_secondleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemasklookupvaluedecode. (((dc_value_inverse_involution_secondleftvaluemask) = 2 * ge_signed_half_inverse_involution_secondleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftvaluemasklookupvalue) = S ge_signed_half_inverse_involution_secondleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftvaluemasklookup) + ge_balance_negative_inverse_involution_secondleftvaluemasklookupvalue = (dst_negative_inverse_involution_secondleftvaluemasklookup) + ge_balance_positive_inverse_involution_secondleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_involution_secondleftvaluemask)=0)) /\ (exists dc_quotient_inverse_involution_secondleftvaluemaskentry dc_left_inverse_involution_secondleftvaluemaskentry dc_right_inverse_involution_secondleftvaluemaskentry. (((dc_input_inverse_involution_secondleft)=(dc_index_inverse_involution_secondleftvaluemask)*dc_quotient_inverse_involution_secondleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_involution_secondleftvaluemaskentryleft dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft dst_negative_code_inverse_involution_secondleftvaluemaskentryleft dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft dst_positive_inverse_involution_secondleftvaluemaskentryleft dst_negative_inverse_involution_secondleftvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemaskentryleftpositive. ff_h_pvs_inverse_involution_secondleftvaluemaskentryleftpositive + S (dst_positive_inverse_involution_secondleftvaluemaskentryleft) = S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemaskentryleftpositive. dst_positive_code_inverse_involution_secondleftvaluemaskentryleft = ff_q_pvs_inverse_involution_secondleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_positive_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_positive_inverse_involution_secondleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemaskentryleftnegative. ff_h_pvs_inverse_involution_secondleftvaluemaskentryleftnegative + S (dst_negative_inverse_involution_secondleftvaluemaskentryleft) = S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemaskentryleftnegative. dst_negative_code_inverse_involution_secondleftvaluemaskentryleft = ff_q_pvs_inverse_involution_secondleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_involution_secondleftvaluemask)) * dst_negative_scale_inverse_involution_secondleftvaluemaskentryleft) + (dst_negative_inverse_involution_secondleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_involution_secondleftvaluemaskentryleftvalue ge_balance_negative_inverse_involution_secondleftvaluemaskentryleftvalue. (((((dc_left_inverse_involution_secondleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_secondleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_involution_secondleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_involution_secondleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_involution_secondleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftvaluemaskentryleft) + ge_balance_negative_inverse_involution_secondleftvaluemaskentryleftvalue = (dst_negative_inverse_involution_secondleftvaluemaskentryleft) + ge_balance_positive_inverse_involution_secondleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_secondleftvaluemaskentryright dst_positive_scale_inverse_involution_secondleftvaluemaskentryright dst_negative_code_inverse_involution_secondleftvaluemaskentryright dst_negative_scale_inverse_involution_secondleftvaluemaskentryright dst_positive_inverse_involution_secondleftvaluemaskentryright dst_negative_inverse_involution_secondleftvaluemaskentryright. (((H) = (((((dst_positive_code_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryright))) + (((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondleftvaluemaskentryright))) + (((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright))) + (((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemaskentryrightpositive. ff_h_pvs_inverse_involution_secondleftvaluemaskentryrightpositive + S (dst_positive_inverse_involution_secondleftvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_secondleftvaluemaskentry)) * dst_positive_scale_inverse_involution_secondleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemaskentryrightpositive. dst_positive_code_inverse_involution_secondleftvaluemaskentryright = ff_q_pvs_inverse_involution_secondleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_involution_secondleftvaluemaskentry)) * dst_positive_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_positive_inverse_involution_secondleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_involution_secondleftvaluemaskentryrightnegative. ff_h_pvs_inverse_involution_secondleftvaluemaskentryrightnegative + S (dst_negative_inverse_involution_secondleftvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_secondleftvaluemaskentry)) * dst_negative_scale_inverse_involution_secondleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_secondleftvaluemaskentryrightnegative. dst_negative_code_inverse_involution_secondleftvaluemaskentryright = ff_q_pvs_inverse_involution_secondleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_involution_secondleftvaluemaskentry)) * dst_negative_scale_inverse_involution_secondleftvaluemaskentryright) + (dst_negative_inverse_involution_secondleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_involution_secondleftvaluemaskentryrightvalue ge_balance_negative_inverse_involution_secondleftvaluemaskentryrightvalue. (((((dc_right_inverse_involution_secondleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_secondleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_involution_secondleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_involution_secondleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_involution_secondleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_involution_secondleftvaluemaskentryright) + ge_balance_negative_inverse_involution_secondleftvaluemaskentryrightvalue = (dst_negative_inverse_involution_secondleftvaluemaskentryright) + ge_balance_positive_inverse_involution_secondleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_involution_secondleftvaluemaskentryproduct sto_an_inverse_involution_secondleftvaluemaskentryproduct sto_bp_inverse_involution_secondleftvaluemaskentryproduct sto_bn_inverse_involution_secondleftvaluemaskentryproduct sto_cp_inverse_involution_secondleftvaluemaskentryproduct sto_cn_inverse_involution_secondleftvaluemaskentryproduct. (((((dc_left_inverse_involution_secondleftvaluemaskentry) = 2 * (sto_ap_inverse_involution_secondleftvaluemaskentryproduct) /\ (sto_an_inverse_involution_secondleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemaskentryproductleft. (((dc_left_inverse_involution_secondleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_involution_secondleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_involution_secondleftvaluemaskentryproduct) = S ge_signed_half_inverse_involution_secondleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_involution_secondleftvaluemaskentry) = 2 * (sto_bp_inverse_involution_secondleftvaluemaskentryproduct) /\ (sto_bn_inverse_involution_secondleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemaskentryproductright. (((dc_right_inverse_involution_secondleftvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_involution_secondleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_involution_secondleftvaluemaskentryproduct) = S ge_signed_half_inverse_involution_secondleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_involution_secondleftvaluemask) = 2 * (sto_cp_inverse_involution_secondleftvaluemaskentryproduct) /\ (sto_cn_inverse_involution_secondleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluemaskentryproductoutput. (((dc_value_inverse_involution_secondleftvaluemask) = 2 * ge_signed_half_inverse_involution_secondleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_involution_secondleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_involution_secondleftvaluemaskentryproduct) = S ge_signed_half_inverse_involution_secondleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_involution_secondleftvaluemaskentryproduct * sto_bp_inverse_involution_secondleftvaluemaskentryproduct + sto_an_inverse_involution_secondleftvaluemaskentryproduct * sto_bn_inverse_involution_secondleftvaluemaskentryproduct) + sto_cn_inverse_involution_secondleftvaluemaskentryproduct = (sto_ap_inverse_involution_secondleftvaluemaskentryproduct * sto_bn_inverse_involution_secondleftvaluemaskentryproduct + sto_an_inverse_involution_secondleftvaluemaskentryproduct * sto_bp_inverse_involution_secondleftvaluemaskentryproduct) + sto_cp_inverse_involution_secondleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_involution_secondleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_involution_secondleftvaluemaskentrynondivisor. (dc_input_inverse_involution_secondleft) = (dc_index_inverse_involution_secondleftvaluemask) * pvs_factor_inverse_involution_secondleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_involution_secondleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_involution_secondleftvaluefold dst_positive_scale_inverse_involution_secondleftvaluefold dst_negative_code_inverse_involution_secondleftvaluefold dst_negative_scale_inverse_involution_secondleftvaluefold dst_positive_sum_inverse_involution_secondleftvaluefold dst_negative_sum_inverse_involution_secondleftvaluefold. (((dc_mask_inverse_involution_secondleftvalue) = (((((dst_positive_code_inverse_involution_secondleftvaluefold) + (dst_positive_scale_inverse_involution_secondleftvaluefold)) * S ((dst_positive_code_inverse_involution_secondleftvaluefold) + (dst_positive_scale_inverse_involution_secondleftvaluefold)) + ((dst_positive_scale_inverse_involution_secondleftvaluefold) + (dst_positive_scale_inverse_involution_secondleftvaluefold))) + (((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) * S ((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) + ((dst_negative_scale_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)))) * S ((((dst_positive_code_inverse_involution_secondleftvaluefold) + (dst_positive_scale_inverse_involution_secondleftvaluefold)) * S ((dst_positive_code_inverse_involution_secondleftvaluefold) + (dst_positive_scale_inverse_involution_secondleftvaluefold)) + ((dst_positive_scale_inverse_involution_secondleftvaluefold) + (dst_positive_scale_inverse_involution_secondleftvaluefold))) + (((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) * S ((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) + ((dst_negative_scale_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)))) + ((((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) * S ((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) + ((dst_negative_scale_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold))) + (((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) * S ((dst_negative_code_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)) + ((dst_negative_scale_inverse_involution_secondleftvaluefold) + (dst_negative_scale_inverse_involution_secondleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_involution_secondleftvaluefoldpositive fs_v_dst_inverse_involution_secondleftvaluefoldpositive. ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_start. fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_start. fs_u_dst_inverse_involution_secondleftvaluefoldpositive = fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_involution_secondleftvaluefold) = S ((S (S (dc_input_inverse_involution_secondleft))) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_involution_secondleftvaluefoldpositive = fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_involution_secondleft))) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive) + (dst_positive_sum_inverse_involution_secondleftvaluefold))) /\ forall fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps = S (dc_input_inverse_involution_secondleft)) -> exists fs_a_dst_inverse_involution_secondleftvaluefoldpositive_body_steps fs_r_dst_inverse_involution_secondleftvaluefoldpositive_body_steps fs_s_dst_inverse_involution_secondleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_involution_secondleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_secondleftvaluefold)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_involution_secondleftvaluefold = fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_secondleftvaluefold) + (fs_a_dst_inverse_involution_secondleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_involution_secondleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_involution_secondleftvaluefoldpositive = fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive) + (fs_r_dst_inverse_involution_secondleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_involution_secondleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_involution_secondleftvaluefoldpositive = fs_q_dst_inverse_involution_secondleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldpositive) + (fs_s_dst_inverse_involution_secondleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_involution_secondleftvaluefoldpositive_body_steps = fs_r_dst_inverse_involution_secondleftvaluefoldpositive_body_steps + fs_a_dst_inverse_involution_secondleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_involution_secondleftvaluefoldnegative fs_v_dst_inverse_involution_secondleftvaluefoldnegative. ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_start. fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_start. fs_u_dst_inverse_involution_secondleftvaluefoldnegative = fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_involution_secondleftvaluefold) = S ((S (S (dc_input_inverse_involution_secondleft))) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_involution_secondleftvaluefoldnegative = fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_involution_secondleft))) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative) + (dst_negative_sum_inverse_involution_secondleftvaluefold))) /\ forall fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps = S (dc_input_inverse_involution_secondleft)) -> exists fs_a_dst_inverse_involution_secondleftvaluefoldnegative_body_steps fs_r_dst_inverse_involution_secondleftvaluefoldnegative_body_steps fs_s_dst_inverse_involution_secondleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_involution_secondleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_secondleftvaluefold)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_involution_secondleftvaluefold = fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_secondleftvaluefold) + (fs_a_dst_inverse_involution_secondleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_involution_secondleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_involution_secondleftvaluefoldnegative = fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative) + (fs_r_dst_inverse_involution_secondleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_involution_secondleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_involution_secondleftvaluefoldnegative = fs_q_dst_inverse_involution_secondleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondleftvaluefoldnegative) + (fs_s_dst_inverse_involution_secondleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_involution_secondleftvaluefoldnegative_body_steps = fs_r_dst_inverse_involution_secondleftvaluefoldnegative_body_steps + fs_a_dst_inverse_involution_secondleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_involution_secondleftvaluefoldresult ge_balance_negative_inverse_involution_secondleftvaluefoldresult. (((((dc_output_inverse_involution_secondleft) = 2 * (ge_balance_positive_inverse_involution_secondleftvaluefoldresult) /\ (ge_balance_negative_inverse_involution_secondleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_involution_secondleftvaluefoldresultdecode. (((dc_output_inverse_involution_secondleft) = 2 * ge_signed_half_inverse_involution_secondleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_involution_secondleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_involution_secondleftvaluefoldresult) = S ge_signed_half_inverse_involution_secondleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_involution_secondleftvaluefold) + ge_balance_negative_inverse_involution_secondleftvaluefoldresult = (dst_negative_sum_inverse_involution_secondleftvaluefold) + ge_balance_positive_inverse_involution_secondleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_involution_secondrightleft dst_positive_scale_inverse_involution_secondrightleft dst_negative_code_inverse_involution_secondrightleft dst_negative_scale_inverse_involution_secondrightleft. (((H) = (((((dst_positive_code_inverse_involution_secondrightleft) + (dst_positive_scale_inverse_involution_secondrightleft)) * S ((dst_positive_code_inverse_involution_secondrightleft) + (dst_positive_scale_inverse_involution_secondrightleft)) + ((dst_positive_scale_inverse_involution_secondrightleft) + (dst_positive_scale_inverse_involution_secondrightleft))) + (((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) * S ((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) + ((dst_negative_scale_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)))) * S ((((dst_positive_code_inverse_involution_secondrightleft) + (dst_positive_scale_inverse_involution_secondrightleft)) * S ((dst_positive_code_inverse_involution_secondrightleft) + (dst_positive_scale_inverse_involution_secondrightleft)) + ((dst_positive_scale_inverse_involution_secondrightleft) + (dst_positive_scale_inverse_involution_secondrightleft))) + (((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) * S ((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) + ((dst_negative_scale_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)))) + ((((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) * S ((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) + ((dst_negative_scale_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft))) + (((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) * S ((dst_negative_code_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)) + ((dst_negative_scale_inverse_involution_secondrightleft) + (dst_negative_scale_inverse_involution_secondrightleft)))))) /\ (forall dst_index_inverse_involution_secondrightleft. (exists pvs_le_gap_inverse_involution_secondrightleftdomain. pvs_le_gap_inverse_involution_secondrightleftdomain + (dst_index_inverse_involution_secondrightleft) = (N)) -> exists dst_positive_inverse_involution_secondrightleft dst_negative_inverse_involution_secondrightleft dst_value_inverse_involution_secondrightleft. ((((exists ff_h_pvs_inverse_involution_secondrightleftentrypositive. ff_h_pvs_inverse_involution_secondrightleftentrypositive + S (dst_positive_inverse_involution_secondrightleft) = S ((S (dst_index_inverse_involution_secondrightleft)) * dst_positive_scale_inverse_involution_secondrightleft)) /\ exists ff_q_pvs_inverse_involution_secondrightleftentrypositive. dst_positive_code_inverse_involution_secondrightleft = ff_q_pvs_inverse_involution_secondrightleftentrypositive * S ((S (dst_index_inverse_involution_secondrightleft)) * dst_positive_scale_inverse_involution_secondrightleft) + (dst_positive_inverse_involution_secondrightleft))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightleftentrynegative. ff_h_pvs_inverse_involution_secondrightleftentrynegative + S (dst_negative_inverse_involution_secondrightleft) = S ((S (dst_index_inverse_involution_secondrightleft)) * dst_negative_scale_inverse_involution_secondrightleft)) /\ exists ff_q_pvs_inverse_involution_secondrightleftentrynegative. dst_negative_code_inverse_involution_secondrightleft = ff_q_pvs_inverse_involution_secondrightleftentrynegative * S ((S (dst_index_inverse_involution_secondrightleft)) * dst_negative_scale_inverse_involution_secondrightleft) + (dst_negative_inverse_involution_secondrightleft))) /\ (exists ge_balance_positive_inverse_involution_secondrightleftentryvalue ge_balance_negative_inverse_involution_secondrightleftentryvalue. (((((dst_value_inverse_involution_secondrightleft) = 2 * (ge_balance_positive_inverse_involution_secondrightleftentryvalue) /\ (ge_balance_negative_inverse_involution_secondrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightleftentryvaluedecode. (((dst_value_inverse_involution_secondrightleft) = 2 * ge_signed_half_inverse_involution_secondrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightleftentryvalue) = S ge_signed_half_inverse_involution_secondrightleftentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightleft) + ge_balance_negative_inverse_involution_secondrightleftentryvalue = (dst_negative_inverse_involution_secondrightleft) + ge_balance_positive_inverse_involution_secondrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_secondrightright dst_positive_scale_inverse_involution_secondrightright dst_negative_code_inverse_involution_secondrightright dst_negative_scale_inverse_involution_secondrightright. (((G) = (((((dst_positive_code_inverse_involution_secondrightright) + (dst_positive_scale_inverse_involution_secondrightright)) * S ((dst_positive_code_inverse_involution_secondrightright) + (dst_positive_scale_inverse_involution_secondrightright)) + ((dst_positive_scale_inverse_involution_secondrightright) + (dst_positive_scale_inverse_involution_secondrightright))) + (((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) * S ((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) + ((dst_negative_scale_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)))) * S ((((dst_positive_code_inverse_involution_secondrightright) + (dst_positive_scale_inverse_involution_secondrightright)) * S ((dst_positive_code_inverse_involution_secondrightright) + (dst_positive_scale_inverse_involution_secondrightright)) + ((dst_positive_scale_inverse_involution_secondrightright) + (dst_positive_scale_inverse_involution_secondrightright))) + (((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) * S ((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) + ((dst_negative_scale_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)))) + ((((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) * S ((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) + ((dst_negative_scale_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright))) + (((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) * S ((dst_negative_code_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)) + ((dst_negative_scale_inverse_involution_secondrightright) + (dst_negative_scale_inverse_involution_secondrightright)))))) /\ (forall dst_index_inverse_involution_secondrightright. (exists pvs_le_gap_inverse_involution_secondrightrightdomain. pvs_le_gap_inverse_involution_secondrightrightdomain + (dst_index_inverse_involution_secondrightright) = (N)) -> exists dst_positive_inverse_involution_secondrightright dst_negative_inverse_involution_secondrightright dst_value_inverse_involution_secondrightright. ((((exists ff_h_pvs_inverse_involution_secondrightrightentrypositive. ff_h_pvs_inverse_involution_secondrightrightentrypositive + S (dst_positive_inverse_involution_secondrightright) = S ((S (dst_index_inverse_involution_secondrightright)) * dst_positive_scale_inverse_involution_secondrightright)) /\ exists ff_q_pvs_inverse_involution_secondrightrightentrypositive. dst_positive_code_inverse_involution_secondrightright = ff_q_pvs_inverse_involution_secondrightrightentrypositive * S ((S (dst_index_inverse_involution_secondrightright)) * dst_positive_scale_inverse_involution_secondrightright) + (dst_positive_inverse_involution_secondrightright))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightrightentrynegative. ff_h_pvs_inverse_involution_secondrightrightentrynegative + S (dst_negative_inverse_involution_secondrightright) = S ((S (dst_index_inverse_involution_secondrightright)) * dst_negative_scale_inverse_involution_secondrightright)) /\ exists ff_q_pvs_inverse_involution_secondrightrightentrynegative. dst_negative_code_inverse_involution_secondrightright = ff_q_pvs_inverse_involution_secondrightrightentrynegative * S ((S (dst_index_inverse_involution_secondrightright)) * dst_negative_scale_inverse_involution_secondrightright) + (dst_negative_inverse_involution_secondrightright))) /\ (exists ge_balance_positive_inverse_involution_secondrightrightentryvalue ge_balance_negative_inverse_involution_secondrightrightentryvalue. (((((dst_value_inverse_involution_secondrightright) = 2 * (ge_balance_positive_inverse_involution_secondrightrightentryvalue) /\ (ge_balance_negative_inverse_involution_secondrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightrightentryvaluedecode. (((dst_value_inverse_involution_secondrightright) = 2 * ge_signed_half_inverse_involution_secondrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightrightentryvalue) = S ge_signed_half_inverse_involution_secondrightrightentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightright) + ge_balance_negative_inverse_involution_secondrightrightentryvalue = (dst_negative_inverse_involution_secondrightright) + ge_balance_positive_inverse_involution_secondrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_secondrighttable dst_positive_scale_inverse_involution_secondrighttable dst_negative_code_inverse_involution_secondrighttable dst_negative_scale_inverse_involution_secondrighttable. (((di_delta_inverse_involution_second) = (((((dst_positive_code_inverse_involution_secondrighttable) + (dst_positive_scale_inverse_involution_secondrighttable)) * S ((dst_positive_code_inverse_involution_secondrighttable) + (dst_positive_scale_inverse_involution_secondrighttable)) + ((dst_positive_scale_inverse_involution_secondrighttable) + (dst_positive_scale_inverse_involution_secondrighttable))) + (((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) * S ((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) + ((dst_negative_scale_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)))) * S ((((dst_positive_code_inverse_involution_secondrighttable) + (dst_positive_scale_inverse_involution_secondrighttable)) * S ((dst_positive_code_inverse_involution_secondrighttable) + (dst_positive_scale_inverse_involution_secondrighttable)) + ((dst_positive_scale_inverse_involution_secondrighttable) + (dst_positive_scale_inverse_involution_secondrighttable))) + (((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) * S ((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) + ((dst_negative_scale_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)))) + ((((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) * S ((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) + ((dst_negative_scale_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable))) + (((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) * S ((dst_negative_code_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)) + ((dst_negative_scale_inverse_involution_secondrighttable) + (dst_negative_scale_inverse_involution_secondrighttable)))))) /\ (forall dst_index_inverse_involution_secondrighttable. (exists pvs_le_gap_inverse_involution_secondrighttabledomain. pvs_le_gap_inverse_involution_secondrighttabledomain + (dst_index_inverse_involution_secondrighttable) = (N)) -> exists dst_positive_inverse_involution_secondrighttable dst_negative_inverse_involution_secondrighttable dst_value_inverse_involution_secondrighttable. ((((exists ff_h_pvs_inverse_involution_secondrighttableentrypositive. ff_h_pvs_inverse_involution_secondrighttableentrypositive + S (dst_positive_inverse_involution_secondrighttable) = S ((S (dst_index_inverse_involution_secondrighttable)) * dst_positive_scale_inverse_involution_secondrighttable)) /\ exists ff_q_pvs_inverse_involution_secondrighttableentrypositive. dst_positive_code_inverse_involution_secondrighttable = ff_q_pvs_inverse_involution_secondrighttableentrypositive * S ((S (dst_index_inverse_involution_secondrighttable)) * dst_positive_scale_inverse_involution_secondrighttable) + (dst_positive_inverse_involution_secondrighttable))) /\ (((((exists ff_h_pvs_inverse_involution_secondrighttableentrynegative. ff_h_pvs_inverse_involution_secondrighttableentrynegative + S (dst_negative_inverse_involution_secondrighttable) = S ((S (dst_index_inverse_involution_secondrighttable)) * dst_negative_scale_inverse_involution_secondrighttable)) /\ exists ff_q_pvs_inverse_involution_secondrighttableentrynegative. dst_negative_code_inverse_involution_secondrighttable = ff_q_pvs_inverse_involution_secondrighttableentrynegative * S ((S (dst_index_inverse_involution_secondrighttable)) * dst_negative_scale_inverse_involution_secondrighttable) + (dst_negative_inverse_involution_secondrighttable))) /\ (exists ge_balance_positive_inverse_involution_secondrighttableentryvalue ge_balance_negative_inverse_involution_secondrighttableentryvalue. (((((dst_value_inverse_involution_secondrighttable) = 2 * (ge_balance_positive_inverse_involution_secondrighttableentryvalue) /\ (ge_balance_negative_inverse_involution_secondrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrighttableentryvaluedecode. (((dst_value_inverse_involution_secondrighttable) = 2 * ge_signed_half_inverse_involution_secondrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrighttableentryvalue) = S ge_signed_half_inverse_involution_secondrighttableentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondrighttable) + ge_balance_negative_inverse_involution_secondrighttableentryvalue = (dst_negative_inverse_involution_secondrighttable) + ge_balance_positive_inverse_involution_secondrighttableentryvalue))))))))) /\ (forall dc_input_inverse_involution_secondright dc_output_inverse_involution_secondright. ~(dc_input_inverse_involution_secondright=0) -> (exists pvs_le_gap_inverse_involution_secondrightdomain. pvs_le_gap_inverse_involution_secondrightdomain + (dc_input_inverse_involution_secondright) = (N)) -> (exists dst_positive_code_inverse_involution_secondrightlookup dst_positive_scale_inverse_involution_secondrightlookup dst_negative_code_inverse_involution_secondrightlookup dst_negative_scale_inverse_involution_secondrightlookup dst_positive_inverse_involution_secondrightlookup dst_negative_inverse_involution_secondrightlookup. (((di_delta_inverse_involution_second) = (((((dst_positive_code_inverse_involution_secondrightlookup) + (dst_positive_scale_inverse_involution_secondrightlookup)) * S ((dst_positive_code_inverse_involution_secondrightlookup) + (dst_positive_scale_inverse_involution_secondrightlookup)) + ((dst_positive_scale_inverse_involution_secondrightlookup) + (dst_positive_scale_inverse_involution_secondrightlookup))) + (((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) * S ((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) + ((dst_negative_scale_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)))) * S ((((dst_positive_code_inverse_involution_secondrightlookup) + (dst_positive_scale_inverse_involution_secondrightlookup)) * S ((dst_positive_code_inverse_involution_secondrightlookup) + (dst_positive_scale_inverse_involution_secondrightlookup)) + ((dst_positive_scale_inverse_involution_secondrightlookup) + (dst_positive_scale_inverse_involution_secondrightlookup))) + (((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) * S ((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) + ((dst_negative_scale_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)))) + ((((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) * S ((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) + ((dst_negative_scale_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup))) + (((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) * S ((dst_negative_code_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)) + ((dst_negative_scale_inverse_involution_secondrightlookup) + (dst_negative_scale_inverse_involution_secondrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightlookuppositive. ff_h_pvs_inverse_involution_secondrightlookuppositive + S (dst_positive_inverse_involution_secondrightlookup) = S ((S (dc_input_inverse_involution_secondright)) * dst_positive_scale_inverse_involution_secondrightlookup)) /\ exists ff_q_pvs_inverse_involution_secondrightlookuppositive. dst_positive_code_inverse_involution_secondrightlookup = ff_q_pvs_inverse_involution_secondrightlookuppositive * S ((S (dc_input_inverse_involution_secondright)) * dst_positive_scale_inverse_involution_secondrightlookup) + (dst_positive_inverse_involution_secondrightlookup))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightlookupnegative. ff_h_pvs_inverse_involution_secondrightlookupnegative + S (dst_negative_inverse_involution_secondrightlookup) = S ((S (dc_input_inverse_involution_secondright)) * dst_negative_scale_inverse_involution_secondrightlookup)) /\ exists ff_q_pvs_inverse_involution_secondrightlookupnegative. dst_negative_code_inverse_involution_secondrightlookup = ff_q_pvs_inverse_involution_secondrightlookupnegative * S ((S (dc_input_inverse_involution_secondright)) * dst_negative_scale_inverse_involution_secondrightlookup) + (dst_negative_inverse_involution_secondrightlookup))) /\ (exists ge_balance_positive_inverse_involution_secondrightlookupvalue ge_balance_negative_inverse_involution_secondrightlookupvalue. (((((dc_output_inverse_involution_secondright) = 2 * (ge_balance_positive_inverse_involution_secondrightlookupvalue) /\ (ge_balance_negative_inverse_involution_secondrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightlookupvaluedecode. (((dc_output_inverse_involution_secondright) = 2 * ge_signed_half_inverse_involution_secondrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightlookupvalue) = S ge_signed_half_inverse_involution_secondrightlookupvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightlookup) + ge_balance_negative_inverse_involution_secondrightlookupvalue = (dst_negative_inverse_involution_secondrightlookup) + ge_balance_positive_inverse_involution_secondrightlookupvalue))))))))) -> (((~((dc_input_inverse_involution_secondright)=0)) /\ (exists dc_mask_inverse_involution_secondrightvalue. ((((exists dst_positive_code_inverse_involution_secondrightvaluemasktable dst_positive_scale_inverse_involution_secondrightvaluemasktable dst_negative_code_inverse_involution_secondrightvaluemasktable dst_negative_scale_inverse_involution_secondrightvaluemasktable. (((dc_mask_inverse_involution_secondrightvalue) = (((((dst_positive_code_inverse_involution_secondrightvaluemasktable) + (dst_positive_scale_inverse_involution_secondrightvaluemasktable)) * S ((dst_positive_code_inverse_involution_secondrightvaluemasktable) + (dst_positive_scale_inverse_involution_secondrightvaluemasktable)) + ((dst_positive_scale_inverse_involution_secondrightvaluemasktable) + (dst_positive_scale_inverse_involution_secondrightvaluemasktable))) + (((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)))) * S ((((dst_positive_code_inverse_involution_secondrightvaluemasktable) + (dst_positive_scale_inverse_involution_secondrightvaluemasktable)) * S ((dst_positive_code_inverse_involution_secondrightvaluemasktable) + (dst_positive_scale_inverse_involution_secondrightvaluemasktable)) + ((dst_positive_scale_inverse_involution_secondrightvaluemasktable) + (dst_positive_scale_inverse_involution_secondrightvaluemasktable))) + (((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)))) + ((((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable))) + (((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasktable) + (dst_negative_scale_inverse_involution_secondrightvaluemasktable)))))) /\ (forall dst_index_inverse_involution_secondrightvaluemasktable. (exists pvs_le_gap_inverse_involution_secondrightvaluemasktabledomain. pvs_le_gap_inverse_involution_secondrightvaluemasktabledomain + (dst_index_inverse_involution_secondrightvaluemasktable) = (dc_input_inverse_involution_secondright)) -> exists dst_positive_inverse_involution_secondrightvaluemasktable dst_negative_inverse_involution_secondrightvaluemasktable dst_value_inverse_involution_secondrightvaluemasktable. ((((exists ff_h_pvs_inverse_involution_secondrightvaluemasktableentrypositive. ff_h_pvs_inverse_involution_secondrightvaluemasktableentrypositive + S (dst_positive_inverse_involution_secondrightvaluemasktable) = S ((S (dst_index_inverse_involution_secondrightvaluemasktable)) * dst_positive_scale_inverse_involution_secondrightvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemasktableentrypositive. dst_positive_code_inverse_involution_secondrightvaluemasktable = ff_q_pvs_inverse_involution_secondrightvaluemasktableentrypositive * S ((S (dst_index_inverse_involution_secondrightvaluemasktable)) * dst_positive_scale_inverse_involution_secondrightvaluemasktable) + (dst_positive_inverse_involution_secondrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemasktableentrynegative. ff_h_pvs_inverse_involution_secondrightvaluemasktableentrynegative + S (dst_negative_inverse_involution_secondrightvaluemasktable) = S ((S (dst_index_inverse_involution_secondrightvaluemasktable)) * dst_negative_scale_inverse_involution_secondrightvaluemasktable)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemasktableentrynegative. dst_negative_code_inverse_involution_secondrightvaluemasktable = ff_q_pvs_inverse_involution_secondrightvaluemasktableentrynegative * S ((S (dst_index_inverse_involution_secondrightvaluemasktable)) * dst_negative_scale_inverse_involution_secondrightvaluemasktable) + (dst_negative_inverse_involution_secondrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_involution_secondrightvaluemasktableentryvalue ge_balance_negative_inverse_involution_secondrightvaluemasktableentryvalue. (((((dst_value_inverse_involution_secondrightvaluemasktable) = 2 * (ge_balance_positive_inverse_involution_secondrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_involution_secondrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemasktableentryvaluedecode. (((dst_value_inverse_involution_secondrightvaluemasktable) = 2 * ge_signed_half_inverse_involution_secondrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightvaluemasktableentryvalue) = S ge_signed_half_inverse_involution_secondrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightvaluemasktable) + ge_balance_negative_inverse_involution_secondrightvaluemasktableentryvalue = (dst_negative_inverse_involution_secondrightvaluemasktable) + ge_balance_positive_inverse_involution_secondrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_involution_secondrightvaluemask dc_value_inverse_involution_secondrightvaluemask. (exists pvs_le_gap_inverse_involution_secondrightvaluemaskdomain. pvs_le_gap_inverse_involution_secondrightvaluemaskdomain + (dc_index_inverse_involution_secondrightvaluemask) = (dc_input_inverse_involution_secondright)) -> (exists dst_positive_code_inverse_involution_secondrightvaluemasklookup dst_positive_scale_inverse_involution_secondrightvaluemasklookup dst_negative_code_inverse_involution_secondrightvaluemasklookup dst_negative_scale_inverse_involution_secondrightvaluemasklookup dst_positive_inverse_involution_secondrightvaluemasklookup dst_negative_inverse_involution_secondrightvaluemasklookup. (((dc_mask_inverse_involution_secondrightvalue) = (((((dst_positive_code_inverse_involution_secondrightvaluemasklookup) + (dst_positive_scale_inverse_involution_secondrightvaluemasklookup)) * S ((dst_positive_code_inverse_involution_secondrightvaluemasklookup) + (dst_positive_scale_inverse_involution_secondrightvaluemasklookup)) + ((dst_positive_scale_inverse_involution_secondrightvaluemasklookup) + (dst_positive_scale_inverse_involution_secondrightvaluemasklookup))) + (((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_involution_secondrightvaluemasklookup) + (dst_positive_scale_inverse_involution_secondrightvaluemasklookup)) * S ((dst_positive_code_inverse_involution_secondrightvaluemasklookup) + (dst_positive_scale_inverse_involution_secondrightvaluemasklookup)) + ((dst_positive_scale_inverse_involution_secondrightvaluemasklookup) + (dst_positive_scale_inverse_involution_secondrightvaluemasklookup))) + (((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)))) + ((((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup))) + (((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) * S ((dst_negative_code_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) + ((dst_negative_scale_inverse_involution_secondrightvaluemasklookup) + (dst_negative_scale_inverse_involution_secondrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemasklookuppositive. ff_h_pvs_inverse_involution_secondrightvaluemasklookuppositive + S (dst_positive_inverse_involution_secondrightvaluemasklookup) = S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_positive_scale_inverse_involution_secondrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemasklookuppositive. dst_positive_code_inverse_involution_secondrightvaluemasklookup = ff_q_pvs_inverse_involution_secondrightvaluemasklookuppositive * S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_positive_scale_inverse_involution_secondrightvaluemasklookup) + (dst_positive_inverse_involution_secondrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemasklookupnegative. ff_h_pvs_inverse_involution_secondrightvaluemasklookupnegative + S (dst_negative_inverse_involution_secondrightvaluemasklookup) = S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_negative_scale_inverse_involution_secondrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemasklookupnegative. dst_negative_code_inverse_involution_secondrightvaluemasklookup = ff_q_pvs_inverse_involution_secondrightvaluemasklookupnegative * S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_negative_scale_inverse_involution_secondrightvaluemasklookup) + (dst_negative_inverse_involution_secondrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_involution_secondrightvaluemasklookupvalue ge_balance_negative_inverse_involution_secondrightvaluemasklookupvalue. (((((dc_value_inverse_involution_secondrightvaluemask) = 2 * (ge_balance_positive_inverse_involution_secondrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_involution_secondrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemasklookupvaluedecode. (((dc_value_inverse_involution_secondrightvaluemask) = 2 * ge_signed_half_inverse_involution_secondrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightvaluemasklookupvalue) = S ge_signed_half_inverse_involution_secondrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightvaluemasklookup) + ge_balance_negative_inverse_involution_secondrightvaluemasklookupvalue = (dst_negative_inverse_involution_secondrightvaluemasklookup) + ge_balance_positive_inverse_involution_secondrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_involution_secondrightvaluemask)=0)) /\ (exists dc_quotient_inverse_involution_secondrightvaluemaskentry dc_left_inverse_involution_secondrightvaluemaskentry dc_right_inverse_involution_secondrightvaluemaskentry. (((dc_input_inverse_involution_secondright)=(dc_index_inverse_involution_secondrightvaluemask)*dc_quotient_inverse_involution_secondrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_involution_secondrightvaluemaskentryleft dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft dst_negative_code_inverse_involution_secondrightvaluemaskentryleft dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft dst_positive_inverse_involution_secondrightvaluemaskentryleft dst_negative_inverse_involution_secondrightvaluemaskentryleft. (((H) = (((((dst_positive_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft))) + (((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemaskentryleftpositive. ff_h_pvs_inverse_involution_secondrightvaluemaskentryleftpositive + S (dst_positive_inverse_involution_secondrightvaluemaskentryleft) = S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemaskentryleftpositive. dst_positive_code_inverse_involution_secondrightvaluemaskentryleft = ff_q_pvs_inverse_involution_secondrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_positive_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_positive_inverse_involution_secondrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemaskentryleftnegative. ff_h_pvs_inverse_involution_secondrightvaluemaskentryleftnegative + S (dst_negative_inverse_involution_secondrightvaluemaskentryleft) = S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemaskentryleftnegative. dst_negative_code_inverse_involution_secondrightvaluemaskentryleft = ff_q_pvs_inverse_involution_secondrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_involution_secondrightvaluemask)) * dst_negative_scale_inverse_involution_secondrightvaluemaskentryleft) + (dst_negative_inverse_involution_secondrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_involution_secondrightvaluemaskentryleftvalue ge_balance_negative_inverse_involution_secondrightvaluemaskentryleftvalue. (((((dc_left_inverse_involution_secondrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_secondrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_involution_secondrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_involution_secondrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_involution_secondrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightvaluemaskentryleft) + ge_balance_negative_inverse_involution_secondrightvaluemaskentryleftvalue = (dst_negative_inverse_involution_secondrightvaluemaskentryleft) + ge_balance_positive_inverse_involution_secondrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_involution_secondrightvaluemaskentryright dst_positive_scale_inverse_involution_secondrightvaluemaskentryright dst_negative_code_inverse_involution_secondrightvaluemaskentryright dst_negative_scale_inverse_involution_secondrightvaluemaskentryright dst_positive_inverse_involution_secondrightvaluemaskentryright dst_negative_inverse_involution_secondrightvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryright))) + (((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryright)) * S ((dst_positive_code_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryright)) + ((dst_positive_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_scale_inverse_involution_secondrightvaluemaskentryright))) + (((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright))) + (((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) * S ((dst_negative_code_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) + ((dst_negative_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemaskentryrightpositive. ff_h_pvs_inverse_involution_secondrightvaluemaskentryrightpositive + S (dst_positive_inverse_involution_secondrightvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_secondrightvaluemaskentry)) * dst_positive_scale_inverse_involution_secondrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemaskentryrightpositive. dst_positive_code_inverse_involution_secondrightvaluemaskentryright = ff_q_pvs_inverse_involution_secondrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_involution_secondrightvaluemaskentry)) * dst_positive_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_positive_inverse_involution_secondrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_involution_secondrightvaluemaskentryrightnegative. ff_h_pvs_inverse_involution_secondrightvaluemaskentryrightnegative + S (dst_negative_inverse_involution_secondrightvaluemaskentryright) = S ((S (dc_quotient_inverse_involution_secondrightvaluemaskentry)) * dst_negative_scale_inverse_involution_secondrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_involution_secondrightvaluemaskentryrightnegative. dst_negative_code_inverse_involution_secondrightvaluemaskentryright = ff_q_pvs_inverse_involution_secondrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_involution_secondrightvaluemaskentry)) * dst_negative_scale_inverse_involution_secondrightvaluemaskentryright) + (dst_negative_inverse_involution_secondrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_involution_secondrightvaluemaskentryrightvalue ge_balance_negative_inverse_involution_secondrightvaluemaskentryrightvalue. (((((dc_right_inverse_involution_secondrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_involution_secondrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_involution_secondrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_involution_secondrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_involution_secondrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_involution_secondrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_involution_secondrightvaluemaskentryright) + ge_balance_negative_inverse_involution_secondrightvaluemaskentryrightvalue = (dst_negative_inverse_involution_secondrightvaluemaskentryright) + ge_balance_positive_inverse_involution_secondrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_involution_secondrightvaluemaskentryproduct sto_an_inverse_involution_secondrightvaluemaskentryproduct sto_bp_inverse_involution_secondrightvaluemaskentryproduct sto_bn_inverse_involution_secondrightvaluemaskentryproduct sto_cp_inverse_involution_secondrightvaluemaskentryproduct sto_cn_inverse_involution_secondrightvaluemaskentryproduct. (((((dc_left_inverse_involution_secondrightvaluemaskentry) = 2 * (sto_ap_inverse_involution_secondrightvaluemaskentryproduct) /\ (sto_an_inverse_involution_secondrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemaskentryproductleft. (((dc_left_inverse_involution_secondrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_involution_secondrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_involution_secondrightvaluemaskentryproduct) = S ge_signed_half_inverse_involution_secondrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_involution_secondrightvaluemaskentry) = 2 * (sto_bp_inverse_involution_secondrightvaluemaskentryproduct) /\ (sto_bn_inverse_involution_secondrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemaskentryproductright. (((dc_right_inverse_involution_secondrightvaluemaskentry) = 2 * ge_signed_half_inverse_involution_secondrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_involution_secondrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_involution_secondrightvaluemaskentryproduct) = S ge_signed_half_inverse_involution_secondrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_involution_secondrightvaluemask) = 2 * (sto_cp_inverse_involution_secondrightvaluemaskentryproduct) /\ (sto_cn_inverse_involution_secondrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluemaskentryproductoutput. (((dc_value_inverse_involution_secondrightvaluemask) = 2 * ge_signed_half_inverse_involution_secondrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_involution_secondrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_involution_secondrightvaluemaskentryproduct) = S ge_signed_half_inverse_involution_secondrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_involution_secondrightvaluemaskentryproduct * sto_bp_inverse_involution_secondrightvaluemaskentryproduct + sto_an_inverse_involution_secondrightvaluemaskentryproduct * sto_bn_inverse_involution_secondrightvaluemaskentryproduct) + sto_cn_inverse_involution_secondrightvaluemaskentryproduct = (sto_ap_inverse_involution_secondrightvaluemaskentryproduct * sto_bn_inverse_involution_secondrightvaluemaskentryproduct + sto_an_inverse_involution_secondrightvaluemaskentryproduct * sto_bp_inverse_involution_secondrightvaluemaskentryproduct) + sto_cp_inverse_involution_secondrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_involution_secondrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_involution_secondrightvaluemaskentrynondivisor. (dc_input_inverse_involution_secondright) = (dc_index_inverse_involution_secondrightvaluemask) * pvs_factor_inverse_involution_secondrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_involution_secondrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_involution_secondrightvaluefold dst_positive_scale_inverse_involution_secondrightvaluefold dst_negative_code_inverse_involution_secondrightvaluefold dst_negative_scale_inverse_involution_secondrightvaluefold dst_positive_sum_inverse_involution_secondrightvaluefold dst_negative_sum_inverse_involution_secondrightvaluefold. (((dc_mask_inverse_involution_secondrightvalue) = (((((dst_positive_code_inverse_involution_secondrightvaluefold) + (dst_positive_scale_inverse_involution_secondrightvaluefold)) * S ((dst_positive_code_inverse_involution_secondrightvaluefold) + (dst_positive_scale_inverse_involution_secondrightvaluefold)) + ((dst_positive_scale_inverse_involution_secondrightvaluefold) + (dst_positive_scale_inverse_involution_secondrightvaluefold))) + (((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) * S ((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) + ((dst_negative_scale_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)))) * S ((((dst_positive_code_inverse_involution_secondrightvaluefold) + (dst_positive_scale_inverse_involution_secondrightvaluefold)) * S ((dst_positive_code_inverse_involution_secondrightvaluefold) + (dst_positive_scale_inverse_involution_secondrightvaluefold)) + ((dst_positive_scale_inverse_involution_secondrightvaluefold) + (dst_positive_scale_inverse_involution_secondrightvaluefold))) + (((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) * S ((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) + ((dst_negative_scale_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)))) + ((((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) * S ((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) + ((dst_negative_scale_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold))) + (((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) * S ((dst_negative_code_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)) + ((dst_negative_scale_inverse_involution_secondrightvaluefold) + (dst_negative_scale_inverse_involution_secondrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_involution_secondrightvaluefoldpositive fs_v_dst_inverse_involution_secondrightvaluefoldpositive. ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_start. fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_start. fs_u_dst_inverse_involution_secondrightvaluefoldpositive = fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_involution_secondrightvaluefold) = S ((S (S (dc_input_inverse_involution_secondright))) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_involution_secondrightvaluefoldpositive = fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_involution_secondright))) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive) + (dst_positive_sum_inverse_involution_secondrightvaluefold))) /\ forall fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps = S (dc_input_inverse_involution_secondright)) -> exists fs_a_dst_inverse_involution_secondrightvaluefoldpositive_body_steps fs_r_dst_inverse_involution_secondrightvaluefoldpositive_body_steps fs_s_dst_inverse_involution_secondrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_involution_secondrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_secondrightvaluefold)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_involution_secondrightvaluefold = fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_involution_secondrightvaluefold) + (fs_a_dst_inverse_involution_secondrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_involution_secondrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_involution_secondrightvaluefoldpositive = fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive) + (fs_r_dst_inverse_involution_secondrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_involution_secondrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_involution_secondrightvaluefoldpositive = fs_q_dst_inverse_involution_secondrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldpositive) + (fs_s_dst_inverse_involution_secondrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_involution_secondrightvaluefoldpositive_body_steps = fs_r_dst_inverse_involution_secondrightvaluefoldpositive_body_steps + fs_a_dst_inverse_involution_secondrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_involution_secondrightvaluefoldnegative fs_v_dst_inverse_involution_secondrightvaluefoldnegative. ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_start. fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_start. fs_u_dst_inverse_involution_secondrightvaluefoldnegative = fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_involution_secondrightvaluefold) = S ((S (S (dc_input_inverse_involution_secondright))) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_involution_secondrightvaluefoldnegative = fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_involution_secondright))) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative) + (dst_negative_sum_inverse_involution_secondrightvaluefold))) /\ forall fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps = S (dc_input_inverse_involution_secondright)) -> exists fs_a_dst_inverse_involution_secondrightvaluefoldnegative_body_steps fs_r_dst_inverse_involution_secondrightvaluefoldnegative_body_steps fs_s_dst_inverse_involution_secondrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_involution_secondrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_secondrightvaluefold)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_involution_secondrightvaluefold = fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_involution_secondrightvaluefold) + (fs_a_dst_inverse_involution_secondrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_involution_secondrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_involution_secondrightvaluefoldnegative = fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative) + (fs_r_dst_inverse_involution_secondrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_involution_secondrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_involution_secondrightvaluefoldnegative = fs_q_dst_inverse_involution_secondrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_involution_secondrightvaluefoldnegative) + (fs_s_dst_inverse_involution_secondrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_involution_secondrightvaluefoldnegative_body_steps = fs_r_dst_inverse_involution_secondrightvaluefoldnegative_body_steps + fs_a_dst_inverse_involution_secondrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_involution_secondrightvaluefoldresult ge_balance_negative_inverse_involution_secondrightvaluefoldresult. (((((dc_output_inverse_involution_secondright) = 2 * (ge_balance_positive_inverse_involution_secondrightvaluefoldresult) /\ (ge_balance_negative_inverse_involution_secondrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_involution_secondrightvaluefoldresultdecode. (((dc_output_inverse_involution_secondright) = 2 * ge_signed_half_inverse_involution_secondrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_involution_secondrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_involution_secondrightvaluefoldresult) = S ge_signed_half_inverse_involution_secondrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_involution_secondrightvaluefold) + ge_balance_negative_inverse_involution_secondrightvaluefoldresult = (dst_negative_sum_inverse_involution_secondrightvaluefold) + ge_balance_positive_inverse_involution_secondrightvaluefoldresult)))))))))))))))))))))))) -> (forall dm_index_inverse_involution_result dm_first_value_inverse_involution_result dm_second_value_inverse_involution_result. ~(dm_index_inverse_involution_result=0) -> (exists pvs_le_gap_inverse_involution_resultdomain. pvs_le_gap_inverse_involution_resultdomain + (dm_index_inverse_involution_result) = (N)) -> (exists dst_positive_code_inverse_involution_resultfirst dst_positive_scale_inverse_involution_resultfirst dst_negative_code_inverse_involution_resultfirst dst_negative_scale_inverse_involution_resultfirst dst_positive_inverse_involution_resultfirst dst_negative_inverse_involution_resultfirst. (((F) = (((((dst_positive_code_inverse_involution_resultfirst) + (dst_positive_scale_inverse_involution_resultfirst)) * S ((dst_positive_code_inverse_involution_resultfirst) + (dst_positive_scale_inverse_involution_resultfirst)) + ((dst_positive_scale_inverse_involution_resultfirst) + (dst_positive_scale_inverse_involution_resultfirst))) + (((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) * S ((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) + ((dst_negative_scale_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)))) * S ((((dst_positive_code_inverse_involution_resultfirst) + (dst_positive_scale_inverse_involution_resultfirst)) * S ((dst_positive_code_inverse_involution_resultfirst) + (dst_positive_scale_inverse_involution_resultfirst)) + ((dst_positive_scale_inverse_involution_resultfirst) + (dst_positive_scale_inverse_involution_resultfirst))) + (((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) * S ((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) + ((dst_negative_scale_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)))) + ((((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) * S ((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) + ((dst_negative_scale_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst))) + (((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) * S ((dst_negative_code_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)) + ((dst_negative_scale_inverse_involution_resultfirst) + (dst_negative_scale_inverse_involution_resultfirst)))))) /\ (((((exists ff_h_pvs_inverse_involution_resultfirstpositive. ff_h_pvs_inverse_involution_resultfirstpositive + S (dst_positive_inverse_involution_resultfirst) = S ((S (dm_index_inverse_involution_result)) * dst_positive_scale_inverse_involution_resultfirst)) /\ exists ff_q_pvs_inverse_involution_resultfirstpositive. dst_positive_code_inverse_involution_resultfirst = ff_q_pvs_inverse_involution_resultfirstpositive * S ((S (dm_index_inverse_involution_result)) * dst_positive_scale_inverse_involution_resultfirst) + (dst_positive_inverse_involution_resultfirst))) /\ (((((exists ff_h_pvs_inverse_involution_resultfirstnegative. ff_h_pvs_inverse_involution_resultfirstnegative + S (dst_negative_inverse_involution_resultfirst) = S ((S (dm_index_inverse_involution_result)) * dst_negative_scale_inverse_involution_resultfirst)) /\ exists ff_q_pvs_inverse_involution_resultfirstnegative. dst_negative_code_inverse_involution_resultfirst = ff_q_pvs_inverse_involution_resultfirstnegative * S ((S (dm_index_inverse_involution_result)) * dst_negative_scale_inverse_involution_resultfirst) + (dst_negative_inverse_involution_resultfirst))) /\ (exists ge_balance_positive_inverse_involution_resultfirstvalue ge_balance_negative_inverse_involution_resultfirstvalue. (((((dm_first_value_inverse_involution_result) = 2 * (ge_balance_positive_inverse_involution_resultfirstvalue) /\ (ge_balance_negative_inverse_involution_resultfirstvalue) = 0) \/ exists ge_signed_half_inverse_involution_resultfirstvaluedecode. (((dm_first_value_inverse_involution_result) = 2 * ge_signed_half_inverse_involution_resultfirstvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_resultfirstvalue) = 0) /\ (ge_balance_negative_inverse_involution_resultfirstvalue) = S ge_signed_half_inverse_involution_resultfirstvaluedecode))) /\ ((dst_positive_inverse_involution_resultfirst) + ge_balance_negative_inverse_involution_resultfirstvalue = (dst_negative_inverse_involution_resultfirst) + ge_balance_positive_inverse_involution_resultfirstvalue))))))))) -> (exists dst_positive_code_inverse_involution_resultsecond dst_positive_scale_inverse_involution_resultsecond dst_negative_code_inverse_involution_resultsecond dst_negative_scale_inverse_involution_resultsecond dst_positive_inverse_involution_resultsecond dst_negative_inverse_involution_resultsecond. (((H) = (((((dst_positive_code_inverse_involution_resultsecond) + (dst_positive_scale_inverse_involution_resultsecond)) * S ((dst_positive_code_inverse_involution_resultsecond) + (dst_positive_scale_inverse_involution_resultsecond)) + ((dst_positive_scale_inverse_involution_resultsecond) + (dst_positive_scale_inverse_involution_resultsecond))) + (((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) * S ((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) + ((dst_negative_scale_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)))) * S ((((dst_positive_code_inverse_involution_resultsecond) + (dst_positive_scale_inverse_involution_resultsecond)) * S ((dst_positive_code_inverse_involution_resultsecond) + (dst_positive_scale_inverse_involution_resultsecond)) + ((dst_positive_scale_inverse_involution_resultsecond) + (dst_positive_scale_inverse_involution_resultsecond))) + (((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) * S ((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) + ((dst_negative_scale_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)))) + ((((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) * S ((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) + ((dst_negative_scale_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond))) + (((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) * S ((dst_negative_code_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)) + ((dst_negative_scale_inverse_involution_resultsecond) + (dst_negative_scale_inverse_involution_resultsecond)))))) /\ (((((exists ff_h_pvs_inverse_involution_resultsecondpositive. ff_h_pvs_inverse_involution_resultsecondpositive + S (dst_positive_inverse_involution_resultsecond) = S ((S (dm_index_inverse_involution_result)) * dst_positive_scale_inverse_involution_resultsecond)) /\ exists ff_q_pvs_inverse_involution_resultsecondpositive. dst_positive_code_inverse_involution_resultsecond = ff_q_pvs_inverse_involution_resultsecondpositive * S ((S (dm_index_inverse_involution_result)) * dst_positive_scale_inverse_involution_resultsecond) + (dst_positive_inverse_involution_resultsecond))) /\ (((((exists ff_h_pvs_inverse_involution_resultsecondnegative. ff_h_pvs_inverse_involution_resultsecondnegative + S (dst_negative_inverse_involution_resultsecond) = S ((S (dm_index_inverse_involution_result)) * dst_negative_scale_inverse_involution_resultsecond)) /\ exists ff_q_pvs_inverse_involution_resultsecondnegative. dst_negative_code_inverse_involution_resultsecond = ff_q_pvs_inverse_involution_resultsecondnegative * S ((S (dm_index_inverse_involution_result)) * dst_negative_scale_inverse_involution_resultsecond) + (dst_negative_inverse_involution_resultsecond))) /\ (exists ge_balance_positive_inverse_involution_resultsecondvalue ge_balance_negative_inverse_involution_resultsecondvalue. (((((dm_second_value_inverse_involution_result) = 2 * (ge_balance_positive_inverse_involution_resultsecondvalue) /\ (ge_balance_negative_inverse_involution_resultsecondvalue) = 0) \/ exists ge_signed_half_inverse_involution_resultsecondvaluedecode. (((dm_second_value_inverse_involution_result) = 2 * ge_signed_half_inverse_involution_resultsecondvaluedecode + 1 /\ (ge_balance_positive_inverse_involution_resultsecondvalue) = 0) /\ (ge_balance_negative_inverse_involution_resultsecondvalue) = S ge_signed_half_inverse_involution_resultsecondvaluedecode))) /\ ((dst_positive_inverse_involution_resultsecond) + ge_balance_negative_inverse_involution_resultsecondvalue = (dst_negative_inverse_involution_resultsecond) + ge_balance_positive_inverse_involution_resultsecondvalue))))))))) -> dm_first_value_inverse_involution_result=dm_second_value_inverse_involution_result)Constructive proof overview
Generated structural guide
Taking an actual Dirichlet inverse twice recovers precisely the original positive represented values, with no encoding or zeroth-value uniqueness claim.
The unchanged tactic script uses 2 declared prerequisites and contains 17 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
none
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–6
02Use earlier factsL7–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L7
specialize dirichlet_inverse_positive_unique (N) - L8
specialize dirichlet_inverse_positive_unique (G) - L9
specialize dirichlet_inverse_positive_unique (F) - L10
specialize dirichlet_inverse_positive_unique (H) - L11
apply dirichlet_inverse_positive_unique - L12
specialize dirichlet_inverse_symmetric (N) - L13
specialize dirichlet_inverse_symmetric (F) - L14
specialize dirichlet_inverse_symmetric (G) - L15
apply dirichlet_inverse_symmetric - L16
exact hg
03Use earlier factsL17–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
exact hh
Original exact command ledger · 17 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro hg - 0006
intro hh - 0007
specialize dirichlet_inverse_positive_unique (N) - 0008
specialize dirichlet_inverse_positive_unique (G) - 0009
specialize dirichlet_inverse_positive_unique (F) - 0010
specialize dirichlet_inverse_positive_unique (H) - 0011
apply dirichlet_inverse_positive_unique - 0012
specialize dirichlet_inverse_symmetric (N) - 0013
specialize dirichlet_inverse_symmetric (F) - 0014
specialize dirichlet_inverse_symmetric (G) - 0015
apply dirichlet_inverse_symmetric - 0016
exact hg - 0017
exact hh