dirichlet_multiplicative_function_invertible

Exact expanded first-order arithmetic statement

forall N F w. (((~((N)=0)) /\ (((exists dst_positive_code_invertible_inputtable dst_positive_scale_invertible_inputtable dst_negative_code_invertible_inputtable dst_negative_scale_invertible_inputtable. (((F) = (((((dst_positive_code_invertible_inputtable) + (dst_positive_scale_invertible_inputtable)) * S ((dst_positive_code_invertible_inputtable) + (dst_positive_scale_invertible_inputtable)) + ((dst_positive_scale_invertible_inputtable) + (dst_positive_scale_invertible_inputtable))) + (((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) * S ((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) + ((dst_negative_scale_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)))) * S ((((dst_positive_code_invertible_inputtable) + (dst_positive_scale_invertible_inputtable)) * S ((dst_positive_code_invertible_inputtable) + (dst_positive_scale_invertible_inputtable)) + ((dst_positive_scale_invertible_inputtable) + (dst_positive_scale_invertible_inputtable))) + (((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) * S ((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) + ((dst_negative_scale_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)))) + ((((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) * S ((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) + ((dst_negative_scale_invertible_inputtable) + (dst_negative_scale_invertible_inputtable))) + (((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) * S ((dst_negative_code_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)) + ((dst_negative_scale_invertible_inputtable) + (dst_negative_scale_invertible_inputtable)))))) /\ (forall dst_index_invertible_inputtable. (exists pvs_le_gap_invertible_inputtabledomain. pvs_le_gap_invertible_inputtabledomain + (dst_index_invertible_inputtable) = (N)) -> exists dst_positive_invertible_inputtable dst_negative_invertible_inputtable dst_value_invertible_inputtable. ((((exists ff_h_pvs_invertible_inputtableentrypositive. ff_h_pvs_invertible_inputtableentrypositive + S (dst_positive_invertible_inputtable) = S ((S (dst_index_invertible_inputtable)) * dst_positive_scale_invertible_inputtable)) /\ exists ff_q_pvs_invertible_inputtableentrypositive. dst_positive_code_invertible_inputtable = ff_q_pvs_invertible_inputtableentrypositive * S ((S (dst_index_invertible_inputtable)) * dst_positive_scale_invertible_inputtable) + (dst_positive_invertible_inputtable))) /\ (((((exists ff_h_pvs_invertible_inputtableentrynegative. ff_h_pvs_invertible_inputtableentrynegative + S (dst_negative_invertible_inputtable) = S ((S (dst_index_invertible_inputtable)) * dst_negative_scale_invertible_inputtable)) /\ exists ff_q_pvs_invertible_inputtableentrynegative. dst_negative_code_invertible_inputtable = ff_q_pvs_invertible_inputtableentrynegative * S ((S (dst_index_invertible_inputtable)) * dst_negative_scale_invertible_inputtable) + (dst_negative_invertible_inputtable))) /\ (exists ge_balance_positive_invertible_inputtableentryvalue ge_balance_negative_invertible_inputtableentryvalue. (((((dst_value_invertible_inputtable) = 2 * (ge_balance_positive_invertible_inputtableentryvalue) /\ (ge_balance_negative_invertible_inputtableentryvalue) = 0) \/ exists ge_signed_half_invertible_inputtableentryvaluedecode. (((dst_value_invertible_inputtable) = 2 * ge_signed_half_invertible_inputtableentryvaluedecode + 1 /\ (ge_balance_positive_invertible_inputtableentryvalue) = 0) /\ (ge_balance_negative_invertible_inputtableentryvalue) = S ge_signed_half_invertible_inputtableentryvaluedecode))) /\ ((dst_positive_invertible_inputtable) + ge_balance_negative_invertible_inputtableentryvalue = (dst_negative_invertible_inputtable) + ge_balance_positive_invertible_inputtableentryvalue))))))))) /\ (((exists dst_positive_code_invertible_inputone dst_positive_scale_invertible_inputone dst_negative_code_invertible_inputone dst_negative_scale_invertible_inputone dst_positive_invertible_inputone dst_negative_invertible_inputone. (((F) = (((((dst_positive_code_invertible_inputone) + (dst_positive_scale_invertible_inputone)) * S ((dst_positive_code_invertible_inputone) + (dst_positive_scale_invertible_inputone)) + ((dst_positive_scale_invertible_inputone) + (dst_positive_scale_invertible_inputone))) + (((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) * S ((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) + ((dst_negative_scale_invertible_inputone) + (dst_negative_scale_invertible_inputone)))) * S ((((dst_positive_code_invertible_inputone) + (dst_positive_scale_invertible_inputone)) * S ((dst_positive_code_invertible_inputone) + (dst_positive_scale_invertible_inputone)) + ((dst_positive_scale_invertible_inputone) + (dst_positive_scale_invertible_inputone))) + (((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) * S ((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) + ((dst_negative_scale_invertible_inputone) + (dst_negative_scale_invertible_inputone)))) + ((((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) * S ((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) + ((dst_negative_scale_invertible_inputone) + (dst_negative_scale_invertible_inputone))) + (((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) * S ((dst_negative_code_invertible_inputone) + (dst_negative_scale_invertible_inputone)) + ((dst_negative_scale_invertible_inputone) + (dst_negative_scale_invertible_inputone)))))) /\ (((((exists ff_h_pvs_invertible_inputonepositive. ff_h_pvs_invertible_inputonepositive + S (dst_positive_invertible_inputone) = S ((S (1)) * dst_positive_scale_invertible_inputone)) /\ exists ff_q_pvs_invertible_inputonepositive. dst_positive_code_invertible_inputone = ff_q_pvs_invertible_inputonepositive * S ((S (1)) * dst_positive_scale_invertible_inputone) + (dst_positive_invertible_inputone))) /\ (((((exists ff_h_pvs_invertible_inputonenegative. ff_h_pvs_invertible_inputonenegative + S (dst_negative_invertible_inputone) = S ((S (1)) * dst_negative_scale_invertible_inputone)) /\ exists ff_q_pvs_invertible_inputonenegative. dst_negative_code_invertible_inputone = ff_q_pvs_invertible_inputonenegative * S ((S (1)) * dst_negative_scale_invertible_inputone) + (dst_negative_invertible_inputone))) /\ (exists ge_balance_positive_invertible_inputonevalue ge_balance_negative_invertible_inputonevalue. (((((2) = 2 * (ge_balance_positive_invertible_inputonevalue) /\ (ge_balance_negative_invertible_inputonevalue) = 0) \/ exists ge_signed_half_invertible_inputonevaluedecode. (((2) = 2 * ge_signed_half_invertible_inputonevaluedecode + 1 /\ (ge_balance_positive_invertible_inputonevalue) = 0) /\ (ge_balance_negative_invertible_inputonevalue) = S ge_signed_half_invertible_inputonevaluedecode))) /\ ((dst_positive_invertible_inputone) + ge_balance_negative_invertible_inputonevalue = (dst_negative_invertible_inputone) + ge_balance_positive_invertible_inputonevalue))))))))) /\ (forall mp_a_invertible_input mp_b_invertible_input mp_x_invertible_input mp_y_invertible_input mp_z_invertible_input. ~(mp_a_invertible_input=0) -> ~(mp_b_invertible_input=0) -> (exists pvs_le_gap_invertible_inputbound. pvs_le_gap_invertible_inputbound + (mp_a_invertible_input*mp_b_invertible_input) = (N)) -> (forall frp_divisor_invertible_inputcoprime. (exists frp_left_factor_invertible_inputcoprime. mp_a_invertible_input = frp_divisor_invertible_inputcoprime * frp_left_factor_invertible_inputcoprime) -> (exists frp_right_factor_invertible_inputcoprime. mp_b_invertible_input = frp_divisor_invertible_inputcoprime * frp_right_factor_invertible_inputcoprime) -> frp_divisor_invertible_inputcoprime = 1) -> (exists dst_positive_code_invertible_inputfirst dst_positive_scale_invertible_inputfirst dst_negative_code_invertible_inputfirst dst_negative_scale_invertible_inputfirst dst_positive_invertible_inputfirst dst_negative_invertible_inputfirst. (((F) = (((((dst_positive_code_invertible_inputfirst) + (dst_positive_scale_invertible_inputfirst)) * S ((dst_positive_code_invertible_inputfirst) + (dst_positive_scale_invertible_inputfirst)) + ((dst_positive_scale_invertible_inputfirst) + (dst_positive_scale_invertible_inputfirst))) + (((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) * S ((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) + ((dst_negative_scale_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)))) * S ((((dst_positive_code_invertible_inputfirst) + (dst_positive_scale_invertible_inputfirst)) * S ((dst_positive_code_invertible_inputfirst) + (dst_positive_scale_invertible_inputfirst)) + ((dst_positive_scale_invertible_inputfirst) + (dst_positive_scale_invertible_inputfirst))) + (((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) * S ((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) + ((dst_negative_scale_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)))) + ((((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) * S ((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) + ((dst_negative_scale_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst))) + (((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) * S ((dst_negative_code_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)) + ((dst_negative_scale_invertible_inputfirst) + (dst_negative_scale_invertible_inputfirst)))))) /\ (((((exists ff_h_pvs_invertible_inputfirstpositive. ff_h_pvs_invertible_inputfirstpositive + S (dst_positive_invertible_inputfirst) = S ((S (mp_a_invertible_input)) * dst_positive_scale_invertible_inputfirst)) /\ exists ff_q_pvs_invertible_inputfirstpositive. dst_positive_code_invertible_inputfirst = ff_q_pvs_invertible_inputfirstpositive * S ((S (mp_a_invertible_input)) * dst_positive_scale_invertible_inputfirst) + (dst_positive_invertible_inputfirst))) /\ (((((exists ff_h_pvs_invertible_inputfirstnegative. ff_h_pvs_invertible_inputfirstnegative + S (dst_negative_invertible_inputfirst) = S ((S (mp_a_invertible_input)) * dst_negative_scale_invertible_inputfirst)) /\ exists ff_q_pvs_invertible_inputfirstnegative. dst_negative_code_invertible_inputfirst = ff_q_pvs_invertible_inputfirstnegative * S ((S (mp_a_invertible_input)) * dst_negative_scale_invertible_inputfirst) + (dst_negative_invertible_inputfirst))) /\ (exists ge_balance_positive_invertible_inputfirstvalue ge_balance_negative_invertible_inputfirstvalue. (((((mp_x_invertible_input) = 2 * (ge_balance_positive_invertible_inputfirstvalue) /\ (ge_balance_negative_invertible_inputfirstvalue) = 0) \/ exists ge_signed_half_invertible_inputfirstvaluedecode. (((mp_x_invertible_input) = 2 * ge_signed_half_invertible_inputfirstvaluedecode + 1 /\ (ge_balance_positive_invertible_inputfirstvalue) = 0) /\ (ge_balance_negative_invertible_inputfirstvalue) = S ge_signed_half_invertible_inputfirstvaluedecode))) /\ ((dst_positive_invertible_inputfirst) + ge_balance_negative_invertible_inputfirstvalue = (dst_negative_invertible_inputfirst) + ge_balance_positive_invertible_inputfirstvalue))))))))) -> (exists dst_positive_code_invertible_inputsecond dst_positive_scale_invertible_inputsecond dst_negative_code_invertible_inputsecond dst_negative_scale_invertible_inputsecond dst_positive_invertible_inputsecond dst_negative_invertible_inputsecond. (((F) = (((((dst_positive_code_invertible_inputsecond) + (dst_positive_scale_invertible_inputsecond)) * S ((dst_positive_code_invertible_inputsecond) + (dst_positive_scale_invertible_inputsecond)) + ((dst_positive_scale_invertible_inputsecond) + (dst_positive_scale_invertible_inputsecond))) + (((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) * S ((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) + ((dst_negative_scale_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)))) * S ((((dst_positive_code_invertible_inputsecond) + (dst_positive_scale_invertible_inputsecond)) * S ((dst_positive_code_invertible_inputsecond) + (dst_positive_scale_invertible_inputsecond)) + ((dst_positive_scale_invertible_inputsecond) + (dst_positive_scale_invertible_inputsecond))) + (((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) * S ((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) + ((dst_negative_scale_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)))) + ((((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) * S ((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) + ((dst_negative_scale_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond))) + (((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) * S ((dst_negative_code_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)) + ((dst_negative_scale_invertible_inputsecond) + (dst_negative_scale_invertible_inputsecond)))))) /\ (((((exists ff_h_pvs_invertible_inputsecondpositive. ff_h_pvs_invertible_inputsecondpositive + S (dst_positive_invertible_inputsecond) = S ((S (mp_b_invertible_input)) * dst_positive_scale_invertible_inputsecond)) /\ exists ff_q_pvs_invertible_inputsecondpositive. dst_positive_code_invertible_inputsecond = ff_q_pvs_invertible_inputsecondpositive * S ((S (mp_b_invertible_input)) * dst_positive_scale_invertible_inputsecond) + (dst_positive_invertible_inputsecond))) /\ (((((exists ff_h_pvs_invertible_inputsecondnegative. ff_h_pvs_invertible_inputsecondnegative + S (dst_negative_invertible_inputsecond) = S ((S (mp_b_invertible_input)) * dst_negative_scale_invertible_inputsecond)) /\ exists ff_q_pvs_invertible_inputsecondnegative. dst_negative_code_invertible_inputsecond = ff_q_pvs_invertible_inputsecondnegative * S ((S (mp_b_invertible_input)) * dst_negative_scale_invertible_inputsecond) + (dst_negative_invertible_inputsecond))) /\ (exists ge_balance_positive_invertible_inputsecondvalue ge_balance_negative_invertible_inputsecondvalue. (((((mp_y_invertible_input) = 2 * (ge_balance_positive_invertible_inputsecondvalue) /\ (ge_balance_negative_invertible_inputsecondvalue) = 0) \/ exists ge_signed_half_invertible_inputsecondvaluedecode. (((mp_y_invertible_input) = 2 * ge_signed_half_invertible_inputsecondvaluedecode + 1 /\ (ge_balance_positive_invertible_inputsecondvalue) = 0) /\ (ge_balance_negative_invertible_inputsecondvalue) = S ge_signed_half_invertible_inputsecondvaluedecode))) /\ ((dst_positive_invertible_inputsecond) + ge_balance_negative_invertible_inputsecondvalue = (dst_negative_invertible_inputsecond) + ge_balance_positive_invertible_inputsecondvalue))))))))) -> (exists dst_positive_code_invertible_inputproduct dst_positive_scale_invertible_inputproduct dst_negative_code_invertible_inputproduct dst_negative_scale_invertible_inputproduct dst_positive_invertible_inputproduct dst_negative_invertible_inputproduct. (((F) = (((((dst_positive_code_invertible_inputproduct) + (dst_positive_scale_invertible_inputproduct)) * S ((dst_positive_code_invertible_inputproduct) + (dst_positive_scale_invertible_inputproduct)) + ((dst_positive_scale_invertible_inputproduct) + (dst_positive_scale_invertible_inputproduct))) + (((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) * S ((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) + ((dst_negative_scale_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)))) * S ((((dst_positive_code_invertible_inputproduct) + (dst_positive_scale_invertible_inputproduct)) * S ((dst_positive_code_invertible_inputproduct) + (dst_positive_scale_invertible_inputproduct)) + ((dst_positive_scale_invertible_inputproduct) + (dst_positive_scale_invertible_inputproduct))) + (((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) * S ((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) + ((dst_negative_scale_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)))) + ((((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) * S ((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) + ((dst_negative_scale_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct))) + (((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) * S ((dst_negative_code_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)) + ((dst_negative_scale_invertible_inputproduct) + (dst_negative_scale_invertible_inputproduct)))))) /\ (((((exists ff_h_pvs_invertible_inputproductpositive. ff_h_pvs_invertible_inputproductpositive + S (dst_positive_invertible_inputproduct) = S ((S (mp_a_invertible_input*mp_b_invertible_input)) * dst_positive_scale_invertible_inputproduct)) /\ exists ff_q_pvs_invertible_inputproductpositive. dst_positive_code_invertible_inputproduct = ff_q_pvs_invertible_inputproductpositive * S ((S (mp_a_invertible_input*mp_b_invertible_input)) * dst_positive_scale_invertible_inputproduct) + (dst_positive_invertible_inputproduct))) /\ (((((exists ff_h_pvs_invertible_inputproductnegative. ff_h_pvs_invertible_inputproductnegative + S (dst_negative_invertible_inputproduct) = S ((S (mp_a_invertible_input*mp_b_invertible_input)) * dst_negative_scale_invertible_inputproduct)) /\ exists ff_q_pvs_invertible_inputproductnegative. dst_negative_code_invertible_inputproduct = ff_q_pvs_invertible_inputproductnegative * S ((S (mp_a_invertible_input*mp_b_invertible_input)) * dst_negative_scale_invertible_inputproduct) + (dst_negative_invertible_inputproduct))) /\ (exists ge_balance_positive_invertible_inputproductvalue ge_balance_negative_invertible_inputproductvalue. (((((mp_z_invertible_input) = 2 * (ge_balance_positive_invertible_inputproductvalue) /\ (ge_balance_negative_invertible_inputproductvalue) = 0) \/ exists ge_signed_half_invertible_inputproductvaluedecode. (((mp_z_invertible_input) = 2 * ge_signed_half_invertible_inputproductvaluedecode + 1 /\ (ge_balance_positive_invertible_inputproductvalue) = 0) /\ (ge_balance_negative_invertible_inputproductvalue) = S ge_signed_half_invertible_inputproductvaluedecode))) /\ ((dst_positive_invertible_inputproduct) + ge_balance_negative_invertible_inputproductvalue = (dst_negative_invertible_inputproduct) + ge_balance_positive_invertible_inputproductvalue))))))))) -> (exists sto_ap_invertible_inputlaw sto_an_invertible_inputlaw sto_bp_invertible_inputlaw sto_bn_invertible_inputlaw sto_cp_invertible_inputlaw sto_cn_invertible_inputlaw. (((((mp_x_invertible_input) = 2 * (sto_ap_invertible_inputlaw) /\ (sto_an_invertible_inputlaw) = 0) \/ exists ge_signed_half_invertible_inputlawleft. (((mp_x_invertible_input) = 2 * ge_signed_half_invertible_inputlawleft + 1 /\ (sto_ap_invertible_inputlaw) = 0) /\ (sto_an_invertible_inputlaw) = S ge_signed_half_invertible_inputlawleft))) /\ ((((((mp_y_invertible_input) = 2 * (sto_bp_invertible_inputlaw) /\ (sto_bn_invertible_inputlaw) = 0) \/ exists ge_signed_half_invertible_inputlawright. (((mp_y_invertible_input) = 2 * ge_signed_half_invertible_inputlawright + 1 /\ (sto_bp_invertible_inputlaw) = 0) /\ (sto_bn_invertible_inputlaw) = S ge_signed_half_invertible_inputlawright))) /\ ((((((mp_z_invertible_input) = 2 * (sto_cp_invertible_inputlaw) /\ (sto_cn_invertible_inputlaw) = 0) \/ exists ge_signed_half_invertible_inputlawoutput. (((mp_z_invertible_input) = 2 * ge_signed_half_invertible_inputlawoutput + 1 /\ (sto_cp_invertible_inputlaw) = 0) /\ (sto_cn_invertible_inputlaw) = S ge_signed_half_invertible_inputlawoutput))) /\ ((sto_ap_invertible_inputlaw * sto_bp_invertible_inputlaw + sto_an_invertible_inputlaw * sto_bn_invertible_inputlaw) + sto_cn_invertible_inputlaw = (sto_ap_invertible_inputlaw * sto_bn_invertible_inputlaw + sto_an_invertible_inputlaw * sto_bp_invertible_inputlaw) + sto_cp_invertible_inputlaw)))))))))))))) -> exists G. ((exists di_delta_invertible_result. ((((exists dst_positive_code_invertible_resultdeltatable dst_positive_scale_invertible_resultdeltatable dst_negative_code_invertible_resultdeltatable dst_negative_scale_invertible_resultdeltatable. (((di_delta_invertible_result) = (((((dst_positive_code_invertible_resultdeltatable) + (dst_positive_scale_invertible_resultdeltatable)) * S ((dst_positive_code_invertible_resultdeltatable) + (dst_positive_scale_invertible_resultdeltatable)) + ((dst_positive_scale_invertible_resultdeltatable) + (dst_positive_scale_invertible_resultdeltatable))) + (((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) * S ((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) + ((dst_negative_scale_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)))) * S ((((dst_positive_code_invertible_resultdeltatable) + (dst_positive_scale_invertible_resultdeltatable)) * S ((dst_positive_code_invertible_resultdeltatable) + (dst_positive_scale_invertible_resultdeltatable)) + ((dst_positive_scale_invertible_resultdeltatable) + (dst_positive_scale_invertible_resultdeltatable))) + (((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) * S ((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) + ((dst_negative_scale_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)))) + ((((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) * S ((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) + ((dst_negative_scale_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable))) + (((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) * S ((dst_negative_code_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)) + ((dst_negative_scale_invertible_resultdeltatable) + (dst_negative_scale_invertible_resultdeltatable)))))) /\ (forall dst_index_invertible_resultdeltatable. (exists pvs_le_gap_invertible_resultdeltatabledomain. pvs_le_gap_invertible_resultdeltatabledomain + (dst_index_invertible_resultdeltatable) = (N)) -> exists dst_positive_invertible_resultdeltatable dst_negative_invertible_resultdeltatable dst_value_invertible_resultdeltatable. ((((exists ff_h_pvs_invertible_resultdeltatableentrypositive. ff_h_pvs_invertible_resultdeltatableentrypositive + S (dst_positive_invertible_resultdeltatable) = S ((S (dst_index_invertible_resultdeltatable)) * dst_positive_scale_invertible_resultdeltatable)) /\ exists ff_q_pvs_invertible_resultdeltatableentrypositive. dst_positive_code_invertible_resultdeltatable = ff_q_pvs_invertible_resultdeltatableentrypositive * S ((S (dst_index_invertible_resultdeltatable)) * dst_positive_scale_invertible_resultdeltatable) + (dst_positive_invertible_resultdeltatable))) /\ (((((exists ff_h_pvs_invertible_resultdeltatableentrynegative. ff_h_pvs_invertible_resultdeltatableentrynegative + S (dst_negative_invertible_resultdeltatable) = S ((S (dst_index_invertible_resultdeltatable)) * dst_negative_scale_invertible_resultdeltatable)) /\ exists ff_q_pvs_invertible_resultdeltatableentrynegative. dst_negative_code_invertible_resultdeltatable = ff_q_pvs_invertible_resultdeltatableentrynegative * S ((S (dst_index_invertible_resultdeltatable)) * dst_negative_scale_invertible_resultdeltatable) + (dst_negative_invertible_resultdeltatable))) /\ (exists ge_balance_positive_invertible_resultdeltatableentryvalue ge_balance_negative_invertible_resultdeltatableentryvalue. (((((dst_value_invertible_resultdeltatable) = 2 * (ge_balance_positive_invertible_resultdeltatableentryvalue) /\ (ge_balance_negative_invertible_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_invertible_resultdeltatableentryvaluedecode. (((dst_value_invertible_resultdeltatable) = 2 * ge_signed_half_invertible_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_invertible_resultdeltatableentryvalue) = S ge_signed_half_invertible_resultdeltatableentryvaluedecode))) /\ ((dst_positive_invertible_resultdeltatable) + ge_balance_negative_invertible_resultdeltatableentryvalue = (dst_negative_invertible_resultdeltatable) + ge_balance_positive_invertible_resultdeltatableentryvalue))))))))) /\ (forall du_index_invertible_resultdelta du_value_invertible_resultdelta. ~(du_index_invertible_resultdelta=0) -> (exists pvs_le_gap_invertible_resultdeltabound. pvs_le_gap_invertible_resultdeltabound + (du_index_invertible_resultdelta) = (N)) -> (exists dst_positive_code_invertible_resultdeltaentry dst_positive_scale_invertible_resultdeltaentry dst_negative_code_invertible_resultdeltaentry dst_negative_scale_invertible_resultdeltaentry dst_positive_invertible_resultdeltaentry dst_negative_invertible_resultdeltaentry. (((di_delta_invertible_result) = (((((dst_positive_code_invertible_resultdeltaentry) + (dst_positive_scale_invertible_resultdeltaentry)) * S ((dst_positive_code_invertible_resultdeltaentry) + (dst_positive_scale_invertible_resultdeltaentry)) + ((dst_positive_scale_invertible_resultdeltaentry) + (dst_positive_scale_invertible_resultdeltaentry))) + (((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) * S ((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) + ((dst_negative_scale_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)))) * S ((((dst_positive_code_invertible_resultdeltaentry) + (dst_positive_scale_invertible_resultdeltaentry)) * S ((dst_positive_code_invertible_resultdeltaentry) + (dst_positive_scale_invertible_resultdeltaentry)) + ((dst_positive_scale_invertible_resultdeltaentry) + (dst_positive_scale_invertible_resultdeltaentry))) + (((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) * S ((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) + ((dst_negative_scale_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)))) + ((((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) * S ((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) + ((dst_negative_scale_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry))) + (((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) * S ((dst_negative_code_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)) + ((dst_negative_scale_invertible_resultdeltaentry) + (dst_negative_scale_invertible_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_invertible_resultdeltaentrypositive. ff_h_pvs_invertible_resultdeltaentrypositive + S (dst_positive_invertible_resultdeltaentry) = S ((S (du_index_invertible_resultdelta)) * dst_positive_scale_invertible_resultdeltaentry)) /\ exists ff_q_pvs_invertible_resultdeltaentrypositive. dst_positive_code_invertible_resultdeltaentry = ff_q_pvs_invertible_resultdeltaentrypositive * S ((S (du_index_invertible_resultdelta)) * dst_positive_scale_invertible_resultdeltaentry) + (dst_positive_invertible_resultdeltaentry))) /\ (((((exists ff_h_pvs_invertible_resultdeltaentrynegative. ff_h_pvs_invertible_resultdeltaentrynegative + S (dst_negative_invertible_resultdeltaentry) = S ((S (du_index_invertible_resultdelta)) * dst_negative_scale_invertible_resultdeltaentry)) /\ exists ff_q_pvs_invertible_resultdeltaentrynegative. dst_negative_code_invertible_resultdeltaentry = ff_q_pvs_invertible_resultdeltaentrynegative * S ((S (du_index_invertible_resultdelta)) * dst_negative_scale_invertible_resultdeltaentry) + (dst_negative_invertible_resultdeltaentry))) /\ (exists ge_balance_positive_invertible_resultdeltaentryvalue ge_balance_negative_invertible_resultdeltaentryvalue. (((((du_value_invertible_resultdelta) = 2 * (ge_balance_positive_invertible_resultdeltaentryvalue) /\ (ge_balance_negative_invertible_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_invertible_resultdeltaentryvaluedecode. (((du_value_invertible_resultdelta) = 2 * ge_signed_half_invertible_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_invertible_resultdeltaentryvalue) = S ge_signed_half_invertible_resultdeltaentryvaluedecode))) /\ ((dst_positive_invertible_resultdeltaentry) + ge_balance_negative_invertible_resultdeltaentryvalue = (dst_negative_invertible_resultdeltaentry) + ge_balance_positive_invertible_resultdeltaentryvalue))))))))) -> ((((du_index_invertible_resultdelta)=1 -> (du_value_invertible_resultdelta)=2) /\ (~((du_index_invertible_resultdelta)=1) -> (du_value_invertible_resultdelta)=0)))))) /\ (((((exists dst_positive_code_invertible_resultleftleft dst_positive_scale_invertible_resultleftleft dst_negative_code_invertible_resultleftleft dst_negative_scale_invertible_resultleftleft. (((F) = (((((dst_positive_code_invertible_resultleftleft) + (dst_positive_scale_invertible_resultleftleft)) * S ((dst_positive_code_invertible_resultleftleft) + (dst_positive_scale_invertible_resultleftleft)) + ((dst_positive_scale_invertible_resultleftleft) + (dst_positive_scale_invertible_resultleftleft))) + (((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) * S ((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) + ((dst_negative_scale_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)))) * S ((((dst_positive_code_invertible_resultleftleft) + (dst_positive_scale_invertible_resultleftleft)) * S ((dst_positive_code_invertible_resultleftleft) + (dst_positive_scale_invertible_resultleftleft)) + ((dst_positive_scale_invertible_resultleftleft) + (dst_positive_scale_invertible_resultleftleft))) + (((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) * S ((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) + ((dst_negative_scale_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)))) + ((((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) * S ((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) + ((dst_negative_scale_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft))) + (((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) * S ((dst_negative_code_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)) + ((dst_negative_scale_invertible_resultleftleft) + (dst_negative_scale_invertible_resultleftleft)))))) /\ (forall dst_index_invertible_resultleftleft. (exists pvs_le_gap_invertible_resultleftleftdomain. pvs_le_gap_invertible_resultleftleftdomain + (dst_index_invertible_resultleftleft) = (N)) -> exists dst_positive_invertible_resultleftleft dst_negative_invertible_resultleftleft dst_value_invertible_resultleftleft. ((((exists ff_h_pvs_invertible_resultleftleftentrypositive. ff_h_pvs_invertible_resultleftleftentrypositive + S (dst_positive_invertible_resultleftleft) = S ((S (dst_index_invertible_resultleftleft)) * dst_positive_scale_invertible_resultleftleft)) /\ exists ff_q_pvs_invertible_resultleftleftentrypositive. dst_positive_code_invertible_resultleftleft = ff_q_pvs_invertible_resultleftleftentrypositive * S ((S (dst_index_invertible_resultleftleft)) * dst_positive_scale_invertible_resultleftleft) + (dst_positive_invertible_resultleftleft))) /\ (((((exists ff_h_pvs_invertible_resultleftleftentrynegative. ff_h_pvs_invertible_resultleftleftentrynegative + S (dst_negative_invertible_resultleftleft) = S ((S (dst_index_invertible_resultleftleft)) * dst_negative_scale_invertible_resultleftleft)) /\ exists ff_q_pvs_invertible_resultleftleftentrynegative. dst_negative_code_invertible_resultleftleft = ff_q_pvs_invertible_resultleftleftentrynegative * S ((S (dst_index_invertible_resultleftleft)) * dst_negative_scale_invertible_resultleftleft) + (dst_negative_invertible_resultleftleft))) /\ (exists ge_balance_positive_invertible_resultleftleftentryvalue ge_balance_negative_invertible_resultleftleftentryvalue. (((((dst_value_invertible_resultleftleft) = 2 * (ge_balance_positive_invertible_resultleftleftentryvalue) /\ (ge_balance_negative_invertible_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_invertible_resultleftleftentryvaluedecode. (((dst_value_invertible_resultleftleft) = 2 * ge_signed_half_invertible_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_invertible_resultleftleftentryvalue) = S ge_signed_half_invertible_resultleftleftentryvaluedecode))) /\ ((dst_positive_invertible_resultleftleft) + ge_balance_negative_invertible_resultleftleftentryvalue = (dst_negative_invertible_resultleftleft) + ge_balance_positive_invertible_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_invertible_resultleftright dst_positive_scale_invertible_resultleftright dst_negative_code_invertible_resultleftright dst_negative_scale_invertible_resultleftright. (((G) = (((((dst_positive_code_invertible_resultleftright) + (dst_positive_scale_invertible_resultleftright)) * S ((dst_positive_code_invertible_resultleftright) + (dst_positive_scale_invertible_resultleftright)) + ((dst_positive_scale_invertible_resultleftright) + (dst_positive_scale_invertible_resultleftright))) + (((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) * S ((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) + ((dst_negative_scale_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)))) * S ((((dst_positive_code_invertible_resultleftright) + (dst_positive_scale_invertible_resultleftright)) * S ((dst_positive_code_invertible_resultleftright) + (dst_positive_scale_invertible_resultleftright)) + ((dst_positive_scale_invertible_resultleftright) + (dst_positive_scale_invertible_resultleftright))) + (((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) * S ((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) + ((dst_negative_scale_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)))) + ((((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) * S ((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) + ((dst_negative_scale_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright))) + (((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) * S ((dst_negative_code_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)) + ((dst_negative_scale_invertible_resultleftright) + (dst_negative_scale_invertible_resultleftright)))))) /\ (forall dst_index_invertible_resultleftright. (exists pvs_le_gap_invertible_resultleftrightdomain. pvs_le_gap_invertible_resultleftrightdomain + (dst_index_invertible_resultleftright) = (N)) -> exists dst_positive_invertible_resultleftright dst_negative_invertible_resultleftright dst_value_invertible_resultleftright. ((((exists ff_h_pvs_invertible_resultleftrightentrypositive. ff_h_pvs_invertible_resultleftrightentrypositive + S (dst_positive_invertible_resultleftright) = S ((S (dst_index_invertible_resultleftright)) * dst_positive_scale_invertible_resultleftright)) /\ exists ff_q_pvs_invertible_resultleftrightentrypositive. dst_positive_code_invertible_resultleftright = ff_q_pvs_invertible_resultleftrightentrypositive * S ((S (dst_index_invertible_resultleftright)) * dst_positive_scale_invertible_resultleftright) + (dst_positive_invertible_resultleftright))) /\ (((((exists ff_h_pvs_invertible_resultleftrightentrynegative. ff_h_pvs_invertible_resultleftrightentrynegative + S (dst_negative_invertible_resultleftright) = S ((S (dst_index_invertible_resultleftright)) * dst_negative_scale_invertible_resultleftright)) /\ exists ff_q_pvs_invertible_resultleftrightentrynegative. dst_negative_code_invertible_resultleftright = ff_q_pvs_invertible_resultleftrightentrynegative * S ((S (dst_index_invertible_resultleftright)) * dst_negative_scale_invertible_resultleftright) + (dst_negative_invertible_resultleftright))) /\ (exists ge_balance_positive_invertible_resultleftrightentryvalue ge_balance_negative_invertible_resultleftrightentryvalue. (((((dst_value_invertible_resultleftright) = 2 * (ge_balance_positive_invertible_resultleftrightentryvalue) /\ (ge_balance_negative_invertible_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_invertible_resultleftrightentryvaluedecode. (((dst_value_invertible_resultleftright) = 2 * ge_signed_half_invertible_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_invertible_resultleftrightentryvalue) = S ge_signed_half_invertible_resultleftrightentryvaluedecode))) /\ ((dst_positive_invertible_resultleftright) + ge_balance_negative_invertible_resultleftrightentryvalue = (dst_negative_invertible_resultleftright) + ge_balance_positive_invertible_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_invertible_resultlefttable dst_positive_scale_invertible_resultlefttable dst_negative_code_invertible_resultlefttable dst_negative_scale_invertible_resultlefttable. (((di_delta_invertible_result) = (((((dst_positive_code_invertible_resultlefttable) + (dst_positive_scale_invertible_resultlefttable)) * S ((dst_positive_code_invertible_resultlefttable) + (dst_positive_scale_invertible_resultlefttable)) + ((dst_positive_scale_invertible_resultlefttable) + (dst_positive_scale_invertible_resultlefttable))) + (((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) * S ((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) + ((dst_negative_scale_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)))) * S ((((dst_positive_code_invertible_resultlefttable) + (dst_positive_scale_invertible_resultlefttable)) * S ((dst_positive_code_invertible_resultlefttable) + (dst_positive_scale_invertible_resultlefttable)) + ((dst_positive_scale_invertible_resultlefttable) + (dst_positive_scale_invertible_resultlefttable))) + (((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) * S ((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) + ((dst_negative_scale_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)))) + ((((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) * S ((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) + ((dst_negative_scale_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable))) + (((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) * S ((dst_negative_code_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)) + ((dst_negative_scale_invertible_resultlefttable) + (dst_negative_scale_invertible_resultlefttable)))))) /\ (forall dst_index_invertible_resultlefttable. (exists pvs_le_gap_invertible_resultlefttabledomain. pvs_le_gap_invertible_resultlefttabledomain + (dst_index_invertible_resultlefttable) = (N)) -> exists dst_positive_invertible_resultlefttable dst_negative_invertible_resultlefttable dst_value_invertible_resultlefttable. ((((exists ff_h_pvs_invertible_resultlefttableentrypositive. ff_h_pvs_invertible_resultlefttableentrypositive + S (dst_positive_invertible_resultlefttable) = S ((S (dst_index_invertible_resultlefttable)) * dst_positive_scale_invertible_resultlefttable)) /\ exists ff_q_pvs_invertible_resultlefttableentrypositive. dst_positive_code_invertible_resultlefttable = ff_q_pvs_invertible_resultlefttableentrypositive * S ((S (dst_index_invertible_resultlefttable)) * dst_positive_scale_invertible_resultlefttable) + (dst_positive_invertible_resultlefttable))) /\ (((((exists ff_h_pvs_invertible_resultlefttableentrynegative. ff_h_pvs_invertible_resultlefttableentrynegative + S (dst_negative_invertible_resultlefttable) = S ((S (dst_index_invertible_resultlefttable)) * dst_negative_scale_invertible_resultlefttable)) /\ exists ff_q_pvs_invertible_resultlefttableentrynegative. dst_negative_code_invertible_resultlefttable = ff_q_pvs_invertible_resultlefttableentrynegative * S ((S (dst_index_invertible_resultlefttable)) * dst_negative_scale_invertible_resultlefttable) + (dst_negative_invertible_resultlefttable))) /\ (exists ge_balance_positive_invertible_resultlefttableentryvalue ge_balance_negative_invertible_resultlefttableentryvalue. (((((dst_value_invertible_resultlefttable) = 2 * (ge_balance_positive_invertible_resultlefttableentryvalue) /\ (ge_balance_negative_invertible_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_invertible_resultlefttableentryvaluedecode. (((dst_value_invertible_resultlefttable) = 2 * ge_signed_half_invertible_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_invertible_resultlefttableentryvalue) = S ge_signed_half_invertible_resultlefttableentryvaluedecode))) /\ ((dst_positive_invertible_resultlefttable) + ge_balance_negative_invertible_resultlefttableentryvalue = (dst_negative_invertible_resultlefttable) + ge_balance_positive_invertible_resultlefttableentryvalue))))))))) /\ (forall dc_input_invertible_resultleft dc_output_invertible_resultleft. ~(dc_input_invertible_resultleft=0) -> (exists pvs_le_gap_invertible_resultleftdomain. pvs_le_gap_invertible_resultleftdomain + (dc_input_invertible_resultleft) = (N)) -> (exists dst_positive_code_invertible_resultleftlookup dst_positive_scale_invertible_resultleftlookup dst_negative_code_invertible_resultleftlookup dst_negative_scale_invertible_resultleftlookup dst_positive_invertible_resultleftlookup dst_negative_invertible_resultleftlookup. (((di_delta_invertible_result) = (((((dst_positive_code_invertible_resultleftlookup) + (dst_positive_scale_invertible_resultleftlookup)) * S ((dst_positive_code_invertible_resultleftlookup) + (dst_positive_scale_invertible_resultleftlookup)) + ((dst_positive_scale_invertible_resultleftlookup) + (dst_positive_scale_invertible_resultleftlookup))) + (((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) * S ((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) + ((dst_negative_scale_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)))) * S ((((dst_positive_code_invertible_resultleftlookup) + (dst_positive_scale_invertible_resultleftlookup)) * S ((dst_positive_code_invertible_resultleftlookup) + (dst_positive_scale_invertible_resultleftlookup)) + ((dst_positive_scale_invertible_resultleftlookup) + (dst_positive_scale_invertible_resultleftlookup))) + (((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) * S ((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) + ((dst_negative_scale_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)))) + ((((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) * S ((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) + ((dst_negative_scale_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup))) + (((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) * S ((dst_negative_code_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)) + ((dst_negative_scale_invertible_resultleftlookup) + (dst_negative_scale_invertible_resultleftlookup)))))) /\ (((((exists ff_h_pvs_invertible_resultleftlookuppositive. ff_h_pvs_invertible_resultleftlookuppositive + S (dst_positive_invertible_resultleftlookup) = S ((S (dc_input_invertible_resultleft)) * dst_positive_scale_invertible_resultleftlookup)) /\ exists ff_q_pvs_invertible_resultleftlookuppositive. dst_positive_code_invertible_resultleftlookup = ff_q_pvs_invertible_resultleftlookuppositive * S ((S (dc_input_invertible_resultleft)) * dst_positive_scale_invertible_resultleftlookup) + (dst_positive_invertible_resultleftlookup))) /\ (((((exists ff_h_pvs_invertible_resultleftlookupnegative. ff_h_pvs_invertible_resultleftlookupnegative + S (dst_negative_invertible_resultleftlookup) = S ((S (dc_input_invertible_resultleft)) * dst_negative_scale_invertible_resultleftlookup)) /\ exists ff_q_pvs_invertible_resultleftlookupnegative. dst_negative_code_invertible_resultleftlookup = ff_q_pvs_invertible_resultleftlookupnegative * S ((S (dc_input_invertible_resultleft)) * dst_negative_scale_invertible_resultleftlookup) + (dst_negative_invertible_resultleftlookup))) /\ (exists ge_balance_positive_invertible_resultleftlookupvalue ge_balance_negative_invertible_resultleftlookupvalue. (((((dc_output_invertible_resultleft) = 2 * (ge_balance_positive_invertible_resultleftlookupvalue) /\ (ge_balance_negative_invertible_resultleftlookupvalue) = 0) \/ exists ge_signed_half_invertible_resultleftlookupvaluedecode. (((dc_output_invertible_resultleft) = 2 * ge_signed_half_invertible_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftlookupvalue) = 0) /\ (ge_balance_negative_invertible_resultleftlookupvalue) = S ge_signed_half_invertible_resultleftlookupvaluedecode))) /\ ((dst_positive_invertible_resultleftlookup) + ge_balance_negative_invertible_resultleftlookupvalue = (dst_negative_invertible_resultleftlookup) + ge_balance_positive_invertible_resultleftlookupvalue))))))))) -> (((~((dc_input_invertible_resultleft)=0)) /\ (exists dc_mask_invertible_resultleftvalue. ((((exists dst_positive_code_invertible_resultleftvaluemasktable dst_positive_scale_invertible_resultleftvaluemasktable dst_negative_code_invertible_resultleftvaluemasktable dst_negative_scale_invertible_resultleftvaluemasktable. (((dc_mask_invertible_resultleftvalue) = (((((dst_positive_code_invertible_resultleftvaluemasktable) + (dst_positive_scale_invertible_resultleftvaluemasktable)) * S ((dst_positive_code_invertible_resultleftvaluemasktable) + (dst_positive_scale_invertible_resultleftvaluemasktable)) + ((dst_positive_scale_invertible_resultleftvaluemasktable) + (dst_positive_scale_invertible_resultleftvaluemasktable))) + (((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) * S ((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) + ((dst_negative_scale_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)))) * S ((((dst_positive_code_invertible_resultleftvaluemasktable) + (dst_positive_scale_invertible_resultleftvaluemasktable)) * S ((dst_positive_code_invertible_resultleftvaluemasktable) + (dst_positive_scale_invertible_resultleftvaluemasktable)) + ((dst_positive_scale_invertible_resultleftvaluemasktable) + (dst_positive_scale_invertible_resultleftvaluemasktable))) + (((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) * S ((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) + ((dst_negative_scale_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)))) + ((((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) * S ((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) + ((dst_negative_scale_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable))) + (((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) * S ((dst_negative_code_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)) + ((dst_negative_scale_invertible_resultleftvaluemasktable) + (dst_negative_scale_invertible_resultleftvaluemasktable)))))) /\ (forall dst_index_invertible_resultleftvaluemasktable. (exists pvs_le_gap_invertible_resultleftvaluemasktabledomain. pvs_le_gap_invertible_resultleftvaluemasktabledomain + (dst_index_invertible_resultleftvaluemasktable) = (dc_input_invertible_resultleft)) -> exists dst_positive_invertible_resultleftvaluemasktable dst_negative_invertible_resultleftvaluemasktable dst_value_invertible_resultleftvaluemasktable. ((((exists ff_h_pvs_invertible_resultleftvaluemasktableentrypositive. ff_h_pvs_invertible_resultleftvaluemasktableentrypositive + S (dst_positive_invertible_resultleftvaluemasktable) = S ((S (dst_index_invertible_resultleftvaluemasktable)) * dst_positive_scale_invertible_resultleftvaluemasktable)) /\ exists ff_q_pvs_invertible_resultleftvaluemasktableentrypositive. dst_positive_code_invertible_resultleftvaluemasktable = ff_q_pvs_invertible_resultleftvaluemasktableentrypositive * S ((S (dst_index_invertible_resultleftvaluemasktable)) * dst_positive_scale_invertible_resultleftvaluemasktable) + (dst_positive_invertible_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemasktableentrynegative. ff_h_pvs_invertible_resultleftvaluemasktableentrynegative + S (dst_negative_invertible_resultleftvaluemasktable) = S ((S (dst_index_invertible_resultleftvaluemasktable)) * dst_negative_scale_invertible_resultleftvaluemasktable)) /\ exists ff_q_pvs_invertible_resultleftvaluemasktableentrynegative. dst_negative_code_invertible_resultleftvaluemasktable = ff_q_pvs_invertible_resultleftvaluemasktableentrynegative * S ((S (dst_index_invertible_resultleftvaluemasktable)) * dst_negative_scale_invertible_resultleftvaluemasktable) + (dst_negative_invertible_resultleftvaluemasktable))) /\ (exists ge_balance_positive_invertible_resultleftvaluemasktableentryvalue ge_balance_negative_invertible_resultleftvaluemasktableentryvalue. (((((dst_value_invertible_resultleftvaluemasktable) = 2 * (ge_balance_positive_invertible_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_invertible_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemasktableentryvaluedecode. (((dst_value_invertible_resultleftvaluemasktable) = 2 * ge_signed_half_invertible_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_invertible_resultleftvaluemasktableentryvalue) = S ge_signed_half_invertible_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_invertible_resultleftvaluemasktable) + ge_balance_negative_invertible_resultleftvaluemasktableentryvalue = (dst_negative_invertible_resultleftvaluemasktable) + ge_balance_positive_invertible_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_invertible_resultleftvaluemask dc_value_invertible_resultleftvaluemask. (exists pvs_le_gap_invertible_resultleftvaluemaskdomain. pvs_le_gap_invertible_resultleftvaluemaskdomain + (dc_index_invertible_resultleftvaluemask) = (dc_input_invertible_resultleft)) -> (exists dst_positive_code_invertible_resultleftvaluemasklookup dst_positive_scale_invertible_resultleftvaluemasklookup dst_negative_code_invertible_resultleftvaluemasklookup dst_negative_scale_invertible_resultleftvaluemasklookup dst_positive_invertible_resultleftvaluemasklookup dst_negative_invertible_resultleftvaluemasklookup. (((dc_mask_invertible_resultleftvalue) = (((((dst_positive_code_invertible_resultleftvaluemasklookup) + (dst_positive_scale_invertible_resultleftvaluemasklookup)) * S ((dst_positive_code_invertible_resultleftvaluemasklookup) + (dst_positive_scale_invertible_resultleftvaluemasklookup)) + ((dst_positive_scale_invertible_resultleftvaluemasklookup) + (dst_positive_scale_invertible_resultleftvaluemasklookup))) + (((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) * S ((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) + ((dst_negative_scale_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)))) * S ((((dst_positive_code_invertible_resultleftvaluemasklookup) + (dst_positive_scale_invertible_resultleftvaluemasklookup)) * S ((dst_positive_code_invertible_resultleftvaluemasklookup) + (dst_positive_scale_invertible_resultleftvaluemasklookup)) + ((dst_positive_scale_invertible_resultleftvaluemasklookup) + (dst_positive_scale_invertible_resultleftvaluemasklookup))) + (((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) * S ((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) + ((dst_negative_scale_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)))) + ((((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) * S ((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) + ((dst_negative_scale_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup))) + (((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) * S ((dst_negative_code_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)) + ((dst_negative_scale_invertible_resultleftvaluemasklookup) + (dst_negative_scale_invertible_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemasklookuppositive. ff_h_pvs_invertible_resultleftvaluemasklookuppositive + S (dst_positive_invertible_resultleftvaluemasklookup) = S ((S (dc_index_invertible_resultleftvaluemask)) * dst_positive_scale_invertible_resultleftvaluemasklookup)) /\ exists ff_q_pvs_invertible_resultleftvaluemasklookuppositive. dst_positive_code_invertible_resultleftvaluemasklookup = ff_q_pvs_invertible_resultleftvaluemasklookuppositive * S ((S (dc_index_invertible_resultleftvaluemask)) * dst_positive_scale_invertible_resultleftvaluemasklookup) + (dst_positive_invertible_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemasklookupnegative. ff_h_pvs_invertible_resultleftvaluemasklookupnegative + S (dst_negative_invertible_resultleftvaluemasklookup) = S ((S (dc_index_invertible_resultleftvaluemask)) * dst_negative_scale_invertible_resultleftvaluemasklookup)) /\ exists ff_q_pvs_invertible_resultleftvaluemasklookupnegative. dst_negative_code_invertible_resultleftvaluemasklookup = ff_q_pvs_invertible_resultleftvaluemasklookupnegative * S ((S (dc_index_invertible_resultleftvaluemask)) * dst_negative_scale_invertible_resultleftvaluemasklookup) + (dst_negative_invertible_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_invertible_resultleftvaluemasklookupvalue ge_balance_negative_invertible_resultleftvaluemasklookupvalue. (((((dc_value_invertible_resultleftvaluemask) = 2 * (ge_balance_positive_invertible_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_invertible_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemasklookupvaluedecode. (((dc_value_invertible_resultleftvaluemask) = 2 * ge_signed_half_invertible_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_invertible_resultleftvaluemasklookupvalue) = S ge_signed_half_invertible_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_invertible_resultleftvaluemasklookup) + ge_balance_negative_invertible_resultleftvaluemasklookupvalue = (dst_negative_invertible_resultleftvaluemasklookup) + ge_balance_positive_invertible_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_invertible_resultleftvaluemask)=0)) /\ (exists dc_quotient_invertible_resultleftvaluemaskentry dc_left_invertible_resultleftvaluemaskentry dc_right_invertible_resultleftvaluemaskentry. (((dc_input_invertible_resultleft)=(dc_index_invertible_resultleftvaluemask)*dc_quotient_invertible_resultleftvaluemaskentry) /\ (((exists dst_positive_code_invertible_resultleftvaluemaskentryleft dst_positive_scale_invertible_resultleftvaluemaskentryleft dst_negative_code_invertible_resultleftvaluemaskentryleft dst_negative_scale_invertible_resultleftvaluemaskentryleft dst_positive_invertible_resultleftvaluemaskentryleft dst_negative_invertible_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_invertible_resultleftvaluemaskentryleft) + (dst_positive_scale_invertible_resultleftvaluemaskentryleft)) * S ((dst_positive_code_invertible_resultleftvaluemaskentryleft) + (dst_positive_scale_invertible_resultleftvaluemaskentryleft)) + ((dst_positive_scale_invertible_resultleftvaluemaskentryleft) + (dst_positive_scale_invertible_resultleftvaluemaskentryleft))) + (((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_invertible_resultleftvaluemaskentryleft) + (dst_positive_scale_invertible_resultleftvaluemaskentryleft)) * S ((dst_positive_code_invertible_resultleftvaluemaskentryleft) + (dst_positive_scale_invertible_resultleftvaluemaskentryleft)) + ((dst_positive_scale_invertible_resultleftvaluemaskentryleft) + (dst_positive_scale_invertible_resultleftvaluemaskentryleft))) + (((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft))) + (((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryleft) + (dst_negative_scale_invertible_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemaskentryleftpositive. ff_h_pvs_invertible_resultleftvaluemaskentryleftpositive + S (dst_positive_invertible_resultleftvaluemaskentryleft) = S ((S (dc_index_invertible_resultleftvaluemask)) * dst_positive_scale_invertible_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_invertible_resultleftvaluemaskentryleftpositive. dst_positive_code_invertible_resultleftvaluemaskentryleft = ff_q_pvs_invertible_resultleftvaluemaskentryleftpositive * S ((S (dc_index_invertible_resultleftvaluemask)) * dst_positive_scale_invertible_resultleftvaluemaskentryleft) + (dst_positive_invertible_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemaskentryleftnegative. ff_h_pvs_invertible_resultleftvaluemaskentryleftnegative + S (dst_negative_invertible_resultleftvaluemaskentryleft) = S ((S (dc_index_invertible_resultleftvaluemask)) * dst_negative_scale_invertible_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_invertible_resultleftvaluemaskentryleftnegative. dst_negative_code_invertible_resultleftvaluemaskentryleft = ff_q_pvs_invertible_resultleftvaluemaskentryleftnegative * S ((S (dc_index_invertible_resultleftvaluemask)) * dst_negative_scale_invertible_resultleftvaluemaskentryleft) + (dst_negative_invertible_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_invertible_resultleftvaluemaskentryleftvalue ge_balance_negative_invertible_resultleftvaluemaskentryleftvalue. (((((dc_left_invertible_resultleftvaluemaskentry) = 2 * (ge_balance_positive_invertible_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_invertible_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemaskentryleftvaluedecode. (((dc_left_invertible_resultleftvaluemaskentry) = 2 * ge_signed_half_invertible_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_invertible_resultleftvaluemaskentryleftvalue) = S ge_signed_half_invertible_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_invertible_resultleftvaluemaskentryleft) + ge_balance_negative_invertible_resultleftvaluemaskentryleftvalue = (dst_negative_invertible_resultleftvaluemaskentryleft) + ge_balance_positive_invertible_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_invertible_resultleftvaluemaskentryright dst_positive_scale_invertible_resultleftvaluemaskentryright dst_negative_code_invertible_resultleftvaluemaskentryright dst_negative_scale_invertible_resultleftvaluemaskentryright dst_positive_invertible_resultleftvaluemaskentryright dst_negative_invertible_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_invertible_resultleftvaluemaskentryright) + (dst_positive_scale_invertible_resultleftvaluemaskentryright)) * S ((dst_positive_code_invertible_resultleftvaluemaskentryright) + (dst_positive_scale_invertible_resultleftvaluemaskentryright)) + ((dst_positive_scale_invertible_resultleftvaluemaskentryright) + (dst_positive_scale_invertible_resultleftvaluemaskentryright))) + (((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_invertible_resultleftvaluemaskentryright) + (dst_positive_scale_invertible_resultleftvaluemaskentryright)) * S ((dst_positive_code_invertible_resultleftvaluemaskentryright) + (dst_positive_scale_invertible_resultleftvaluemaskentryright)) + ((dst_positive_scale_invertible_resultleftvaluemaskentryright) + (dst_positive_scale_invertible_resultleftvaluemaskentryright))) + (((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)))) + ((((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright))) + (((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) * S ((dst_negative_code_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)) + ((dst_negative_scale_invertible_resultleftvaluemaskentryright) + (dst_negative_scale_invertible_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemaskentryrightpositive. ff_h_pvs_invertible_resultleftvaluemaskentryrightpositive + S (dst_positive_invertible_resultleftvaluemaskentryright) = S ((S (dc_quotient_invertible_resultleftvaluemaskentry)) * dst_positive_scale_invertible_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_invertible_resultleftvaluemaskentryrightpositive. dst_positive_code_invertible_resultleftvaluemaskentryright = ff_q_pvs_invertible_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_invertible_resultleftvaluemaskentry)) * dst_positive_scale_invertible_resultleftvaluemaskentryright) + (dst_positive_invertible_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_invertible_resultleftvaluemaskentryrightnegative. ff_h_pvs_invertible_resultleftvaluemaskentryrightnegative + S (dst_negative_invertible_resultleftvaluemaskentryright) = S ((S (dc_quotient_invertible_resultleftvaluemaskentry)) * dst_negative_scale_invertible_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_invertible_resultleftvaluemaskentryrightnegative. dst_negative_code_invertible_resultleftvaluemaskentryright = ff_q_pvs_invertible_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_invertible_resultleftvaluemaskentry)) * dst_negative_scale_invertible_resultleftvaluemaskentryright) + (dst_negative_invertible_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_invertible_resultleftvaluemaskentryrightvalue ge_balance_negative_invertible_resultleftvaluemaskentryrightvalue. (((((dc_right_invertible_resultleftvaluemaskentry) = 2 * (ge_balance_positive_invertible_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_invertible_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemaskentryrightvaluedecode. (((dc_right_invertible_resultleftvaluemaskentry) = 2 * ge_signed_half_invertible_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_invertible_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_invertible_resultleftvaluemaskentryrightvalue) = S ge_signed_half_invertible_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_invertible_resultleftvaluemaskentryright) + ge_balance_negative_invertible_resultleftvaluemaskentryrightvalue = (dst_negative_invertible_resultleftvaluemaskentryright) + ge_balance_positive_invertible_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_invertible_resultleftvaluemaskentryproduct sto_an_invertible_resultleftvaluemaskentryproduct sto_bp_invertible_resultleftvaluemaskentryproduct sto_bn_invertible_resultleftvaluemaskentryproduct sto_cp_invertible_resultleftvaluemaskentryproduct sto_cn_invertible_resultleftvaluemaskentryproduct. (((((dc_left_invertible_resultleftvaluemaskentry) = 2 * (sto_ap_invertible_resultleftvaluemaskentryproduct) /\ (sto_an_invertible_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemaskentryproductleft. (((dc_left_invertible_resultleftvaluemaskentry) = 2 * ge_signed_half_invertible_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_invertible_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_invertible_resultleftvaluemaskentryproduct) = S ge_signed_half_invertible_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_invertible_resultleftvaluemaskentry) = 2 * (sto_bp_invertible_resultleftvaluemaskentryproduct) /\ (sto_bn_invertible_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemaskentryproductright. (((dc_right_invertible_resultleftvaluemaskentry) = 2 * ge_signed_half_invertible_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_invertible_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_invertible_resultleftvaluemaskentryproduct) = S ge_signed_half_invertible_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_invertible_resultleftvaluemask) = 2 * (sto_cp_invertible_resultleftvaluemaskentryproduct) /\ (sto_cn_invertible_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_invertible_resultleftvaluemaskentryproductoutput. (((dc_value_invertible_resultleftvaluemask) = 2 * ge_signed_half_invertible_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_invertible_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_invertible_resultleftvaluemaskentryproduct) = S ge_signed_half_invertible_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_invertible_resultleftvaluemaskentryproduct * sto_bp_invertible_resultleftvaluemaskentryproduct + sto_an_invertible_resultleftvaluemaskentryproduct * sto_bn_invertible_resultleftvaluemaskentryproduct) + sto_cn_invertible_resultleftvaluemaskentryproduct = (sto_ap_invertible_resultleftvaluemaskentryproduct * sto_bn_invertible_resultleftvaluemaskentryproduct + sto_an_invertible_resultleftvaluemaskentryproduct * sto_bp_invertible_resultleftvaluemaskentryproduct) + sto_cp_invertible_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_invertible_resultleftvaluemask)=0 \/ ~(exists pvs_factor_invertible_resultleftvaluemaskentrynondivisor. (dc_input_invertible_resultleft) = (dc_index_invertible_resultleftvaluemask) * pvs_factor_invertible_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_invertible_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_invertible_resultleftvaluefold dst_positive_scale_invertible_resultleftvaluefold dst_negative_code_invertible_resultleftvaluefold dst_negative_scale_invertible_resultleftvaluefold dst_positive_sum_invertible_resultleftvaluefold dst_negative_sum_invertible_resultleftvaluefold. (((dc_mask_invertible_resultleftvalue) = (((((dst_positive_code_invertible_resultleftvaluefold) + (dst_positive_scale_invertible_resultleftvaluefold)) * S ((dst_positive_code_invertible_resultleftvaluefold) + (dst_positive_scale_invertible_resultleftvaluefold)) + ((dst_positive_scale_invertible_resultleftvaluefold) + (dst_positive_scale_invertible_resultleftvaluefold))) + (((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) * S ((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) + ((dst_negative_scale_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)))) * S ((((dst_positive_code_invertible_resultleftvaluefold) + (dst_positive_scale_invertible_resultleftvaluefold)) * S ((dst_positive_code_invertible_resultleftvaluefold) + (dst_positive_scale_invertible_resultleftvaluefold)) + ((dst_positive_scale_invertible_resultleftvaluefold) + (dst_positive_scale_invertible_resultleftvaluefold))) + (((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) * S ((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) + ((dst_negative_scale_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)))) + ((((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) * S ((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) + ((dst_negative_scale_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold))) + (((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) * S ((dst_negative_code_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)) + ((dst_negative_scale_invertible_resultleftvaluefold) + (dst_negative_scale_invertible_resultleftvaluefold)))))) /\ (((exists fs_u_dst_invertible_resultleftvaluefoldpositive fs_v_dst_invertible_resultleftvaluefoldpositive. ((((exists fs_h_dst_invertible_resultleftvaluefoldpositive_body_start. fs_h_dst_invertible_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_invertible_resultleftvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultleftvaluefoldpositive_body_start. fs_u_dst_invertible_resultleftvaluefoldpositive = fs_q_dst_invertible_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_invertible_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_invertible_resultleftvaluefoldpositive_body_terminal. fs_h_dst_invertible_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_invertible_resultleftvaluefold) = S ((S (S (dc_input_invertible_resultleft))) * fs_v_dst_invertible_resultleftvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultleftvaluefoldpositive_body_terminal. fs_u_dst_invertible_resultleftvaluefoldpositive = fs_q_dst_invertible_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_invertible_resultleft))) * fs_v_dst_invertible_resultleftvaluefoldpositive) + (dst_positive_sum_invertible_resultleftvaluefold))) /\ forall fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_invertible_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_invertible_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps = S (dc_input_invertible_resultleft)) -> exists fs_a_dst_invertible_resultleftvaluefoldpositive_body_steps fs_r_dst_invertible_resultleftvaluefoldpositive_body_steps fs_s_dst_invertible_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_invertible_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_invertible_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_invertible_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_invertible_resultleftvaluefold)) /\ exists fs_q_dst_invertible_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_invertible_resultleftvaluefold = fs_q_dst_invertible_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_invertible_resultleftvaluefold) + (fs_a_dst_invertible_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_invertible_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_invertible_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_invertible_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_invertible_resultleftvaluefoldpositive = fs_q_dst_invertible_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldpositive) + (fs_r_dst_invertible_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_invertible_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_invertible_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_invertible_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_invertible_resultleftvaluefoldpositive = fs_q_dst_invertible_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_invertible_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldpositive) + (fs_s_dst_invertible_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_invertible_resultleftvaluefoldpositive_body_steps = fs_r_dst_invertible_resultleftvaluefoldpositive_body_steps + fs_a_dst_invertible_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_invertible_resultleftvaluefoldnegative fs_v_dst_invertible_resultleftvaluefoldnegative. ((((exists fs_h_dst_invertible_resultleftvaluefoldnegative_body_start. fs_h_dst_invertible_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_invertible_resultleftvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultleftvaluefoldnegative_body_start. fs_u_dst_invertible_resultleftvaluefoldnegative = fs_q_dst_invertible_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_invertible_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_invertible_resultleftvaluefoldnegative_body_terminal. fs_h_dst_invertible_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_invertible_resultleftvaluefold) = S ((S (S (dc_input_invertible_resultleft))) * fs_v_dst_invertible_resultleftvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultleftvaluefoldnegative_body_terminal. fs_u_dst_invertible_resultleftvaluefoldnegative = fs_q_dst_invertible_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_invertible_resultleft))) * fs_v_dst_invertible_resultleftvaluefoldnegative) + (dst_negative_sum_invertible_resultleftvaluefold))) /\ forall fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_invertible_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_invertible_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps = S (dc_input_invertible_resultleft)) -> exists fs_a_dst_invertible_resultleftvaluefoldnegative_body_steps fs_r_dst_invertible_resultleftvaluefoldnegative_body_steps fs_s_dst_invertible_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_invertible_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_invertible_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_invertible_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_invertible_resultleftvaluefold)) /\ exists fs_q_dst_invertible_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_invertible_resultleftvaluefold = fs_q_dst_invertible_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_invertible_resultleftvaluefold) + (fs_a_dst_invertible_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_invertible_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_invertible_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_invertible_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_invertible_resultleftvaluefoldnegative = fs_q_dst_invertible_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldnegative) + (fs_r_dst_invertible_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_invertible_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_invertible_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_invertible_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_invertible_resultleftvaluefoldnegative = fs_q_dst_invertible_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_invertible_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultleftvaluefoldnegative) + (fs_s_dst_invertible_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_invertible_resultleftvaluefoldnegative_body_steps = fs_r_dst_invertible_resultleftvaluefoldnegative_body_steps + fs_a_dst_invertible_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_invertible_resultleftvaluefoldresult ge_balance_negative_invertible_resultleftvaluefoldresult. (((((dc_output_invertible_resultleft) = 2 * (ge_balance_positive_invertible_resultleftvaluefoldresult) /\ (ge_balance_negative_invertible_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_invertible_resultleftvaluefoldresultdecode. (((dc_output_invertible_resultleft) = 2 * ge_signed_half_invertible_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_invertible_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_invertible_resultleftvaluefoldresult) = S ge_signed_half_invertible_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_invertible_resultleftvaluefold) + ge_balance_negative_invertible_resultleftvaluefoldresult = (dst_negative_sum_invertible_resultleftvaluefold) + ge_balance_positive_invertible_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_invertible_resultrightleft dst_positive_scale_invertible_resultrightleft dst_negative_code_invertible_resultrightleft dst_negative_scale_invertible_resultrightleft. (((G) = (((((dst_positive_code_invertible_resultrightleft) + (dst_positive_scale_invertible_resultrightleft)) * S ((dst_positive_code_invertible_resultrightleft) + (dst_positive_scale_invertible_resultrightleft)) + ((dst_positive_scale_invertible_resultrightleft) + (dst_positive_scale_invertible_resultrightleft))) + (((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) * S ((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) + ((dst_negative_scale_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)))) * S ((((dst_positive_code_invertible_resultrightleft) + (dst_positive_scale_invertible_resultrightleft)) * S ((dst_positive_code_invertible_resultrightleft) + (dst_positive_scale_invertible_resultrightleft)) + ((dst_positive_scale_invertible_resultrightleft) + (dst_positive_scale_invertible_resultrightleft))) + (((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) * S ((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) + ((dst_negative_scale_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)))) + ((((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) * S ((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) + ((dst_negative_scale_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft))) + (((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) * S ((dst_negative_code_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)) + ((dst_negative_scale_invertible_resultrightleft) + (dst_negative_scale_invertible_resultrightleft)))))) /\ (forall dst_index_invertible_resultrightleft. (exists pvs_le_gap_invertible_resultrightleftdomain. pvs_le_gap_invertible_resultrightleftdomain + (dst_index_invertible_resultrightleft) = (N)) -> exists dst_positive_invertible_resultrightleft dst_negative_invertible_resultrightleft dst_value_invertible_resultrightleft. ((((exists ff_h_pvs_invertible_resultrightleftentrypositive. ff_h_pvs_invertible_resultrightleftentrypositive + S (dst_positive_invertible_resultrightleft) = S ((S (dst_index_invertible_resultrightleft)) * dst_positive_scale_invertible_resultrightleft)) /\ exists ff_q_pvs_invertible_resultrightleftentrypositive. dst_positive_code_invertible_resultrightleft = ff_q_pvs_invertible_resultrightleftentrypositive * S ((S (dst_index_invertible_resultrightleft)) * dst_positive_scale_invertible_resultrightleft) + (dst_positive_invertible_resultrightleft))) /\ (((((exists ff_h_pvs_invertible_resultrightleftentrynegative. ff_h_pvs_invertible_resultrightleftentrynegative + S (dst_negative_invertible_resultrightleft) = S ((S (dst_index_invertible_resultrightleft)) * dst_negative_scale_invertible_resultrightleft)) /\ exists ff_q_pvs_invertible_resultrightleftentrynegative. dst_negative_code_invertible_resultrightleft = ff_q_pvs_invertible_resultrightleftentrynegative * S ((S (dst_index_invertible_resultrightleft)) * dst_negative_scale_invertible_resultrightleft) + (dst_negative_invertible_resultrightleft))) /\ (exists ge_balance_positive_invertible_resultrightleftentryvalue ge_balance_negative_invertible_resultrightleftentryvalue. (((((dst_value_invertible_resultrightleft) = 2 * (ge_balance_positive_invertible_resultrightleftentryvalue) /\ (ge_balance_negative_invertible_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_invertible_resultrightleftentryvaluedecode. (((dst_value_invertible_resultrightleft) = 2 * ge_signed_half_invertible_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_invertible_resultrightleftentryvalue) = S ge_signed_half_invertible_resultrightleftentryvaluedecode))) /\ ((dst_positive_invertible_resultrightleft) + ge_balance_negative_invertible_resultrightleftentryvalue = (dst_negative_invertible_resultrightleft) + ge_balance_positive_invertible_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_invertible_resultrightright dst_positive_scale_invertible_resultrightright dst_negative_code_invertible_resultrightright dst_negative_scale_invertible_resultrightright. (((F) = (((((dst_positive_code_invertible_resultrightright) + (dst_positive_scale_invertible_resultrightright)) * S ((dst_positive_code_invertible_resultrightright) + (dst_positive_scale_invertible_resultrightright)) + ((dst_positive_scale_invertible_resultrightright) + (dst_positive_scale_invertible_resultrightright))) + (((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) * S ((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) + ((dst_negative_scale_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)))) * S ((((dst_positive_code_invertible_resultrightright) + (dst_positive_scale_invertible_resultrightright)) * S ((dst_positive_code_invertible_resultrightright) + (dst_positive_scale_invertible_resultrightright)) + ((dst_positive_scale_invertible_resultrightright) + (dst_positive_scale_invertible_resultrightright))) + (((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) * S ((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) + ((dst_negative_scale_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)))) + ((((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) * S ((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) + ((dst_negative_scale_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright))) + (((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) * S ((dst_negative_code_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)) + ((dst_negative_scale_invertible_resultrightright) + (dst_negative_scale_invertible_resultrightright)))))) /\ (forall dst_index_invertible_resultrightright. (exists pvs_le_gap_invertible_resultrightrightdomain. pvs_le_gap_invertible_resultrightrightdomain + (dst_index_invertible_resultrightright) = (N)) -> exists dst_positive_invertible_resultrightright dst_negative_invertible_resultrightright dst_value_invertible_resultrightright. ((((exists ff_h_pvs_invertible_resultrightrightentrypositive. ff_h_pvs_invertible_resultrightrightentrypositive + S (dst_positive_invertible_resultrightright) = S ((S (dst_index_invertible_resultrightright)) * dst_positive_scale_invertible_resultrightright)) /\ exists ff_q_pvs_invertible_resultrightrightentrypositive. dst_positive_code_invertible_resultrightright = ff_q_pvs_invertible_resultrightrightentrypositive * S ((S (dst_index_invertible_resultrightright)) * dst_positive_scale_invertible_resultrightright) + (dst_positive_invertible_resultrightright))) /\ (((((exists ff_h_pvs_invertible_resultrightrightentrynegative. ff_h_pvs_invertible_resultrightrightentrynegative + S (dst_negative_invertible_resultrightright) = S ((S (dst_index_invertible_resultrightright)) * dst_negative_scale_invertible_resultrightright)) /\ exists ff_q_pvs_invertible_resultrightrightentrynegative. dst_negative_code_invertible_resultrightright = ff_q_pvs_invertible_resultrightrightentrynegative * S ((S (dst_index_invertible_resultrightright)) * dst_negative_scale_invertible_resultrightright) + (dst_negative_invertible_resultrightright))) /\ (exists ge_balance_positive_invertible_resultrightrightentryvalue ge_balance_negative_invertible_resultrightrightentryvalue. (((((dst_value_invertible_resultrightright) = 2 * (ge_balance_positive_invertible_resultrightrightentryvalue) /\ (ge_balance_negative_invertible_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_invertible_resultrightrightentryvaluedecode. (((dst_value_invertible_resultrightright) = 2 * ge_signed_half_invertible_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_invertible_resultrightrightentryvalue) = S ge_signed_half_invertible_resultrightrightentryvaluedecode))) /\ ((dst_positive_invertible_resultrightright) + ge_balance_negative_invertible_resultrightrightentryvalue = (dst_negative_invertible_resultrightright) + ge_balance_positive_invertible_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_invertible_resultrighttable dst_positive_scale_invertible_resultrighttable dst_negative_code_invertible_resultrighttable dst_negative_scale_invertible_resultrighttable. (((di_delta_invertible_result) = (((((dst_positive_code_invertible_resultrighttable) + (dst_positive_scale_invertible_resultrighttable)) * S ((dst_positive_code_invertible_resultrighttable) + (dst_positive_scale_invertible_resultrighttable)) + ((dst_positive_scale_invertible_resultrighttable) + (dst_positive_scale_invertible_resultrighttable))) + (((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) * S ((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) + ((dst_negative_scale_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)))) * S ((((dst_positive_code_invertible_resultrighttable) + (dst_positive_scale_invertible_resultrighttable)) * S ((dst_positive_code_invertible_resultrighttable) + (dst_positive_scale_invertible_resultrighttable)) + ((dst_positive_scale_invertible_resultrighttable) + (dst_positive_scale_invertible_resultrighttable))) + (((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) * S ((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) + ((dst_negative_scale_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)))) + ((((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) * S ((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) + ((dst_negative_scale_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable))) + (((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) * S ((dst_negative_code_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)) + ((dst_negative_scale_invertible_resultrighttable) + (dst_negative_scale_invertible_resultrighttable)))))) /\ (forall dst_index_invertible_resultrighttable. (exists pvs_le_gap_invertible_resultrighttabledomain. pvs_le_gap_invertible_resultrighttabledomain + (dst_index_invertible_resultrighttable) = (N)) -> exists dst_positive_invertible_resultrighttable dst_negative_invertible_resultrighttable dst_value_invertible_resultrighttable. ((((exists ff_h_pvs_invertible_resultrighttableentrypositive. ff_h_pvs_invertible_resultrighttableentrypositive + S (dst_positive_invertible_resultrighttable) = S ((S (dst_index_invertible_resultrighttable)) * dst_positive_scale_invertible_resultrighttable)) /\ exists ff_q_pvs_invertible_resultrighttableentrypositive. dst_positive_code_invertible_resultrighttable = ff_q_pvs_invertible_resultrighttableentrypositive * S ((S (dst_index_invertible_resultrighttable)) * dst_positive_scale_invertible_resultrighttable) + (dst_positive_invertible_resultrighttable))) /\ (((((exists ff_h_pvs_invertible_resultrighttableentrynegative. ff_h_pvs_invertible_resultrighttableentrynegative + S (dst_negative_invertible_resultrighttable) = S ((S (dst_index_invertible_resultrighttable)) * dst_negative_scale_invertible_resultrighttable)) /\ exists ff_q_pvs_invertible_resultrighttableentrynegative. dst_negative_code_invertible_resultrighttable = ff_q_pvs_invertible_resultrighttableentrynegative * S ((S (dst_index_invertible_resultrighttable)) * dst_negative_scale_invertible_resultrighttable) + (dst_negative_invertible_resultrighttable))) /\ (exists ge_balance_positive_invertible_resultrighttableentryvalue ge_balance_negative_invertible_resultrighttableentryvalue. (((((dst_value_invertible_resultrighttable) = 2 * (ge_balance_positive_invertible_resultrighttableentryvalue) /\ (ge_balance_negative_invertible_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_invertible_resultrighttableentryvaluedecode. (((dst_value_invertible_resultrighttable) = 2 * ge_signed_half_invertible_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_invertible_resultrighttableentryvalue) = S ge_signed_half_invertible_resultrighttableentryvaluedecode))) /\ ((dst_positive_invertible_resultrighttable) + ge_balance_negative_invertible_resultrighttableentryvalue = (dst_negative_invertible_resultrighttable) + ge_balance_positive_invertible_resultrighttableentryvalue))))))))) /\ (forall dc_input_invertible_resultright dc_output_invertible_resultright. ~(dc_input_invertible_resultright=0) -> (exists pvs_le_gap_invertible_resultrightdomain. pvs_le_gap_invertible_resultrightdomain + (dc_input_invertible_resultright) = (N)) -> (exists dst_positive_code_invertible_resultrightlookup dst_positive_scale_invertible_resultrightlookup dst_negative_code_invertible_resultrightlookup dst_negative_scale_invertible_resultrightlookup dst_positive_invertible_resultrightlookup dst_negative_invertible_resultrightlookup. (((di_delta_invertible_result) = (((((dst_positive_code_invertible_resultrightlookup) + (dst_positive_scale_invertible_resultrightlookup)) * S ((dst_positive_code_invertible_resultrightlookup) + (dst_positive_scale_invertible_resultrightlookup)) + ((dst_positive_scale_invertible_resultrightlookup) + (dst_positive_scale_invertible_resultrightlookup))) + (((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) * S ((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) + ((dst_negative_scale_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)))) * S ((((dst_positive_code_invertible_resultrightlookup) + (dst_positive_scale_invertible_resultrightlookup)) * S ((dst_positive_code_invertible_resultrightlookup) + (dst_positive_scale_invertible_resultrightlookup)) + ((dst_positive_scale_invertible_resultrightlookup) + (dst_positive_scale_invertible_resultrightlookup))) + (((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) * S ((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) + ((dst_negative_scale_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)))) + ((((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) * S ((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) + ((dst_negative_scale_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup))) + (((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) * S ((dst_negative_code_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)) + ((dst_negative_scale_invertible_resultrightlookup) + (dst_negative_scale_invertible_resultrightlookup)))))) /\ (((((exists ff_h_pvs_invertible_resultrightlookuppositive. ff_h_pvs_invertible_resultrightlookuppositive + S (dst_positive_invertible_resultrightlookup) = S ((S (dc_input_invertible_resultright)) * dst_positive_scale_invertible_resultrightlookup)) /\ exists ff_q_pvs_invertible_resultrightlookuppositive. dst_positive_code_invertible_resultrightlookup = ff_q_pvs_invertible_resultrightlookuppositive * S ((S (dc_input_invertible_resultright)) * dst_positive_scale_invertible_resultrightlookup) + (dst_positive_invertible_resultrightlookup))) /\ (((((exists ff_h_pvs_invertible_resultrightlookupnegative. ff_h_pvs_invertible_resultrightlookupnegative + S (dst_negative_invertible_resultrightlookup) = S ((S (dc_input_invertible_resultright)) * dst_negative_scale_invertible_resultrightlookup)) /\ exists ff_q_pvs_invertible_resultrightlookupnegative. dst_negative_code_invertible_resultrightlookup = ff_q_pvs_invertible_resultrightlookupnegative * S ((S (dc_input_invertible_resultright)) * dst_negative_scale_invertible_resultrightlookup) + (dst_negative_invertible_resultrightlookup))) /\ (exists ge_balance_positive_invertible_resultrightlookupvalue ge_balance_negative_invertible_resultrightlookupvalue. (((((dc_output_invertible_resultright) = 2 * (ge_balance_positive_invertible_resultrightlookupvalue) /\ (ge_balance_negative_invertible_resultrightlookupvalue) = 0) \/ exists ge_signed_half_invertible_resultrightlookupvaluedecode. (((dc_output_invertible_resultright) = 2 * ge_signed_half_invertible_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightlookupvalue) = 0) /\ (ge_balance_negative_invertible_resultrightlookupvalue) = S ge_signed_half_invertible_resultrightlookupvaluedecode))) /\ ((dst_positive_invertible_resultrightlookup) + ge_balance_negative_invertible_resultrightlookupvalue = (dst_negative_invertible_resultrightlookup) + ge_balance_positive_invertible_resultrightlookupvalue))))))))) -> (((~((dc_input_invertible_resultright)=0)) /\ (exists dc_mask_invertible_resultrightvalue. ((((exists dst_positive_code_invertible_resultrightvaluemasktable dst_positive_scale_invertible_resultrightvaluemasktable dst_negative_code_invertible_resultrightvaluemasktable dst_negative_scale_invertible_resultrightvaluemasktable. (((dc_mask_invertible_resultrightvalue) = (((((dst_positive_code_invertible_resultrightvaluemasktable) + (dst_positive_scale_invertible_resultrightvaluemasktable)) * S ((dst_positive_code_invertible_resultrightvaluemasktable) + (dst_positive_scale_invertible_resultrightvaluemasktable)) + ((dst_positive_scale_invertible_resultrightvaluemasktable) + (dst_positive_scale_invertible_resultrightvaluemasktable))) + (((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) * S ((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) + ((dst_negative_scale_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)))) * S ((((dst_positive_code_invertible_resultrightvaluemasktable) + (dst_positive_scale_invertible_resultrightvaluemasktable)) * S ((dst_positive_code_invertible_resultrightvaluemasktable) + (dst_positive_scale_invertible_resultrightvaluemasktable)) + ((dst_positive_scale_invertible_resultrightvaluemasktable) + (dst_positive_scale_invertible_resultrightvaluemasktable))) + (((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) * S ((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) + ((dst_negative_scale_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)))) + ((((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) * S ((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) + ((dst_negative_scale_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable))) + (((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) * S ((dst_negative_code_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)) + ((dst_negative_scale_invertible_resultrightvaluemasktable) + (dst_negative_scale_invertible_resultrightvaluemasktable)))))) /\ (forall dst_index_invertible_resultrightvaluemasktable. (exists pvs_le_gap_invertible_resultrightvaluemasktabledomain. pvs_le_gap_invertible_resultrightvaluemasktabledomain + (dst_index_invertible_resultrightvaluemasktable) = (dc_input_invertible_resultright)) -> exists dst_positive_invertible_resultrightvaluemasktable dst_negative_invertible_resultrightvaluemasktable dst_value_invertible_resultrightvaluemasktable. ((((exists ff_h_pvs_invertible_resultrightvaluemasktableentrypositive. ff_h_pvs_invertible_resultrightvaluemasktableentrypositive + S (dst_positive_invertible_resultrightvaluemasktable) = S ((S (dst_index_invertible_resultrightvaluemasktable)) * dst_positive_scale_invertible_resultrightvaluemasktable)) /\ exists ff_q_pvs_invertible_resultrightvaluemasktableentrypositive. dst_positive_code_invertible_resultrightvaluemasktable = ff_q_pvs_invertible_resultrightvaluemasktableentrypositive * S ((S (dst_index_invertible_resultrightvaluemasktable)) * dst_positive_scale_invertible_resultrightvaluemasktable) + (dst_positive_invertible_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemasktableentrynegative. ff_h_pvs_invertible_resultrightvaluemasktableentrynegative + S (dst_negative_invertible_resultrightvaluemasktable) = S ((S (dst_index_invertible_resultrightvaluemasktable)) * dst_negative_scale_invertible_resultrightvaluemasktable)) /\ exists ff_q_pvs_invertible_resultrightvaluemasktableentrynegative. dst_negative_code_invertible_resultrightvaluemasktable = ff_q_pvs_invertible_resultrightvaluemasktableentrynegative * S ((S (dst_index_invertible_resultrightvaluemasktable)) * dst_negative_scale_invertible_resultrightvaluemasktable) + (dst_negative_invertible_resultrightvaluemasktable))) /\ (exists ge_balance_positive_invertible_resultrightvaluemasktableentryvalue ge_balance_negative_invertible_resultrightvaluemasktableentryvalue. (((((dst_value_invertible_resultrightvaluemasktable) = 2 * (ge_balance_positive_invertible_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_invertible_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemasktableentryvaluedecode. (((dst_value_invertible_resultrightvaluemasktable) = 2 * ge_signed_half_invertible_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_invertible_resultrightvaluemasktableentryvalue) = S ge_signed_half_invertible_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_invertible_resultrightvaluemasktable) + ge_balance_negative_invertible_resultrightvaluemasktableentryvalue = (dst_negative_invertible_resultrightvaluemasktable) + ge_balance_positive_invertible_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_invertible_resultrightvaluemask dc_value_invertible_resultrightvaluemask. (exists pvs_le_gap_invertible_resultrightvaluemaskdomain. pvs_le_gap_invertible_resultrightvaluemaskdomain + (dc_index_invertible_resultrightvaluemask) = (dc_input_invertible_resultright)) -> (exists dst_positive_code_invertible_resultrightvaluemasklookup dst_positive_scale_invertible_resultrightvaluemasklookup dst_negative_code_invertible_resultrightvaluemasklookup dst_negative_scale_invertible_resultrightvaluemasklookup dst_positive_invertible_resultrightvaluemasklookup dst_negative_invertible_resultrightvaluemasklookup. (((dc_mask_invertible_resultrightvalue) = (((((dst_positive_code_invertible_resultrightvaluemasklookup) + (dst_positive_scale_invertible_resultrightvaluemasklookup)) * S ((dst_positive_code_invertible_resultrightvaluemasklookup) + (dst_positive_scale_invertible_resultrightvaluemasklookup)) + ((dst_positive_scale_invertible_resultrightvaluemasklookup) + (dst_positive_scale_invertible_resultrightvaluemasklookup))) + (((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) * S ((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) + ((dst_negative_scale_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)))) * S ((((dst_positive_code_invertible_resultrightvaluemasklookup) + (dst_positive_scale_invertible_resultrightvaluemasklookup)) * S ((dst_positive_code_invertible_resultrightvaluemasklookup) + (dst_positive_scale_invertible_resultrightvaluemasklookup)) + ((dst_positive_scale_invertible_resultrightvaluemasklookup) + (dst_positive_scale_invertible_resultrightvaluemasklookup))) + (((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) * S ((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) + ((dst_negative_scale_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)))) + ((((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) * S ((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) + ((dst_negative_scale_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup))) + (((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) * S ((dst_negative_code_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)) + ((dst_negative_scale_invertible_resultrightvaluemasklookup) + (dst_negative_scale_invertible_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemasklookuppositive. ff_h_pvs_invertible_resultrightvaluemasklookuppositive + S (dst_positive_invertible_resultrightvaluemasklookup) = S ((S (dc_index_invertible_resultrightvaluemask)) * dst_positive_scale_invertible_resultrightvaluemasklookup)) /\ exists ff_q_pvs_invertible_resultrightvaluemasklookuppositive. dst_positive_code_invertible_resultrightvaluemasklookup = ff_q_pvs_invertible_resultrightvaluemasklookuppositive * S ((S (dc_index_invertible_resultrightvaluemask)) * dst_positive_scale_invertible_resultrightvaluemasklookup) + (dst_positive_invertible_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemasklookupnegative. ff_h_pvs_invertible_resultrightvaluemasklookupnegative + S (dst_negative_invertible_resultrightvaluemasklookup) = S ((S (dc_index_invertible_resultrightvaluemask)) * dst_negative_scale_invertible_resultrightvaluemasklookup)) /\ exists ff_q_pvs_invertible_resultrightvaluemasklookupnegative. dst_negative_code_invertible_resultrightvaluemasklookup = ff_q_pvs_invertible_resultrightvaluemasklookupnegative * S ((S (dc_index_invertible_resultrightvaluemask)) * dst_negative_scale_invertible_resultrightvaluemasklookup) + (dst_negative_invertible_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_invertible_resultrightvaluemasklookupvalue ge_balance_negative_invertible_resultrightvaluemasklookupvalue. (((((dc_value_invertible_resultrightvaluemask) = 2 * (ge_balance_positive_invertible_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_invertible_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemasklookupvaluedecode. (((dc_value_invertible_resultrightvaluemask) = 2 * ge_signed_half_invertible_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_invertible_resultrightvaluemasklookupvalue) = S ge_signed_half_invertible_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_invertible_resultrightvaluemasklookup) + ge_balance_negative_invertible_resultrightvaluemasklookupvalue = (dst_negative_invertible_resultrightvaluemasklookup) + ge_balance_positive_invertible_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_invertible_resultrightvaluemask)=0)) /\ (exists dc_quotient_invertible_resultrightvaluemaskentry dc_left_invertible_resultrightvaluemaskentry dc_right_invertible_resultrightvaluemaskentry. (((dc_input_invertible_resultright)=(dc_index_invertible_resultrightvaluemask)*dc_quotient_invertible_resultrightvaluemaskentry) /\ (((exists dst_positive_code_invertible_resultrightvaluemaskentryleft dst_positive_scale_invertible_resultrightvaluemaskentryleft dst_negative_code_invertible_resultrightvaluemaskentryleft dst_negative_scale_invertible_resultrightvaluemaskentryleft dst_positive_invertible_resultrightvaluemaskentryleft dst_negative_invertible_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_invertible_resultrightvaluemaskentryleft) + (dst_positive_scale_invertible_resultrightvaluemaskentryleft)) * S ((dst_positive_code_invertible_resultrightvaluemaskentryleft) + (dst_positive_scale_invertible_resultrightvaluemaskentryleft)) + ((dst_positive_scale_invertible_resultrightvaluemaskentryleft) + (dst_positive_scale_invertible_resultrightvaluemaskentryleft))) + (((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_invertible_resultrightvaluemaskentryleft) + (dst_positive_scale_invertible_resultrightvaluemaskentryleft)) * S ((dst_positive_code_invertible_resultrightvaluemaskentryleft) + (dst_positive_scale_invertible_resultrightvaluemaskentryleft)) + ((dst_positive_scale_invertible_resultrightvaluemaskentryleft) + (dst_positive_scale_invertible_resultrightvaluemaskentryleft))) + (((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft))) + (((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryleft) + (dst_negative_scale_invertible_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemaskentryleftpositive. ff_h_pvs_invertible_resultrightvaluemaskentryleftpositive + S (dst_positive_invertible_resultrightvaluemaskentryleft) = S ((S (dc_index_invertible_resultrightvaluemask)) * dst_positive_scale_invertible_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_invertible_resultrightvaluemaskentryleftpositive. dst_positive_code_invertible_resultrightvaluemaskentryleft = ff_q_pvs_invertible_resultrightvaluemaskentryleftpositive * S ((S (dc_index_invertible_resultrightvaluemask)) * dst_positive_scale_invertible_resultrightvaluemaskentryleft) + (dst_positive_invertible_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemaskentryleftnegative. ff_h_pvs_invertible_resultrightvaluemaskentryleftnegative + S (dst_negative_invertible_resultrightvaluemaskentryleft) = S ((S (dc_index_invertible_resultrightvaluemask)) * dst_negative_scale_invertible_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_invertible_resultrightvaluemaskentryleftnegative. dst_negative_code_invertible_resultrightvaluemaskentryleft = ff_q_pvs_invertible_resultrightvaluemaskentryleftnegative * S ((S (dc_index_invertible_resultrightvaluemask)) * dst_negative_scale_invertible_resultrightvaluemaskentryleft) + (dst_negative_invertible_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_invertible_resultrightvaluemaskentryleftvalue ge_balance_negative_invertible_resultrightvaluemaskentryleftvalue. (((((dc_left_invertible_resultrightvaluemaskentry) = 2 * (ge_balance_positive_invertible_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_invertible_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemaskentryleftvaluedecode. (((dc_left_invertible_resultrightvaluemaskentry) = 2 * ge_signed_half_invertible_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_invertible_resultrightvaluemaskentryleftvalue) = S ge_signed_half_invertible_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_invertible_resultrightvaluemaskentryleft) + ge_balance_negative_invertible_resultrightvaluemaskentryleftvalue = (dst_negative_invertible_resultrightvaluemaskentryleft) + ge_balance_positive_invertible_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_invertible_resultrightvaluemaskentryright dst_positive_scale_invertible_resultrightvaluemaskentryright dst_negative_code_invertible_resultrightvaluemaskentryright dst_negative_scale_invertible_resultrightvaluemaskentryright dst_positive_invertible_resultrightvaluemaskentryright dst_negative_invertible_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_invertible_resultrightvaluemaskentryright) + (dst_positive_scale_invertible_resultrightvaluemaskentryright)) * S ((dst_positive_code_invertible_resultrightvaluemaskentryright) + (dst_positive_scale_invertible_resultrightvaluemaskentryright)) + ((dst_positive_scale_invertible_resultrightvaluemaskentryright) + (dst_positive_scale_invertible_resultrightvaluemaskentryright))) + (((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_invertible_resultrightvaluemaskentryright) + (dst_positive_scale_invertible_resultrightvaluemaskentryright)) * S ((dst_positive_code_invertible_resultrightvaluemaskentryright) + (dst_positive_scale_invertible_resultrightvaluemaskentryright)) + ((dst_positive_scale_invertible_resultrightvaluemaskentryright) + (dst_positive_scale_invertible_resultrightvaluemaskentryright))) + (((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)))) + ((((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright))) + (((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) * S ((dst_negative_code_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)) + ((dst_negative_scale_invertible_resultrightvaluemaskentryright) + (dst_negative_scale_invertible_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemaskentryrightpositive. ff_h_pvs_invertible_resultrightvaluemaskentryrightpositive + S (dst_positive_invertible_resultrightvaluemaskentryright) = S ((S (dc_quotient_invertible_resultrightvaluemaskentry)) * dst_positive_scale_invertible_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_invertible_resultrightvaluemaskentryrightpositive. dst_positive_code_invertible_resultrightvaluemaskentryright = ff_q_pvs_invertible_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_invertible_resultrightvaluemaskentry)) * dst_positive_scale_invertible_resultrightvaluemaskentryright) + (dst_positive_invertible_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_invertible_resultrightvaluemaskentryrightnegative. ff_h_pvs_invertible_resultrightvaluemaskentryrightnegative + S (dst_negative_invertible_resultrightvaluemaskentryright) = S ((S (dc_quotient_invertible_resultrightvaluemaskentry)) * dst_negative_scale_invertible_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_invertible_resultrightvaluemaskentryrightnegative. dst_negative_code_invertible_resultrightvaluemaskentryright = ff_q_pvs_invertible_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_invertible_resultrightvaluemaskentry)) * dst_negative_scale_invertible_resultrightvaluemaskentryright) + (dst_negative_invertible_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_invertible_resultrightvaluemaskentryrightvalue ge_balance_negative_invertible_resultrightvaluemaskentryrightvalue. (((((dc_right_invertible_resultrightvaluemaskentry) = 2 * (ge_balance_positive_invertible_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_invertible_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemaskentryrightvaluedecode. (((dc_right_invertible_resultrightvaluemaskentry) = 2 * ge_signed_half_invertible_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_invertible_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_invertible_resultrightvaluemaskentryrightvalue) = S ge_signed_half_invertible_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_invertible_resultrightvaluemaskentryright) + ge_balance_negative_invertible_resultrightvaluemaskentryrightvalue = (dst_negative_invertible_resultrightvaluemaskentryright) + ge_balance_positive_invertible_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_invertible_resultrightvaluemaskentryproduct sto_an_invertible_resultrightvaluemaskentryproduct sto_bp_invertible_resultrightvaluemaskentryproduct sto_bn_invertible_resultrightvaluemaskentryproduct sto_cp_invertible_resultrightvaluemaskentryproduct sto_cn_invertible_resultrightvaluemaskentryproduct. (((((dc_left_invertible_resultrightvaluemaskentry) = 2 * (sto_ap_invertible_resultrightvaluemaskentryproduct) /\ (sto_an_invertible_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemaskentryproductleft. (((dc_left_invertible_resultrightvaluemaskentry) = 2 * ge_signed_half_invertible_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_invertible_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_invertible_resultrightvaluemaskentryproduct) = S ge_signed_half_invertible_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_invertible_resultrightvaluemaskentry) = 2 * (sto_bp_invertible_resultrightvaluemaskentryproduct) /\ (sto_bn_invertible_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemaskentryproductright. (((dc_right_invertible_resultrightvaluemaskentry) = 2 * ge_signed_half_invertible_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_invertible_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_invertible_resultrightvaluemaskentryproduct) = S ge_signed_half_invertible_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_invertible_resultrightvaluemask) = 2 * (sto_cp_invertible_resultrightvaluemaskentryproduct) /\ (sto_cn_invertible_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_invertible_resultrightvaluemaskentryproductoutput. (((dc_value_invertible_resultrightvaluemask) = 2 * ge_signed_half_invertible_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_invertible_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_invertible_resultrightvaluemaskentryproduct) = S ge_signed_half_invertible_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_invertible_resultrightvaluemaskentryproduct * sto_bp_invertible_resultrightvaluemaskentryproduct + sto_an_invertible_resultrightvaluemaskentryproduct * sto_bn_invertible_resultrightvaluemaskentryproduct) + sto_cn_invertible_resultrightvaluemaskentryproduct = (sto_ap_invertible_resultrightvaluemaskentryproduct * sto_bn_invertible_resultrightvaluemaskentryproduct + sto_an_invertible_resultrightvaluemaskentryproduct * sto_bp_invertible_resultrightvaluemaskentryproduct) + sto_cp_invertible_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_invertible_resultrightvaluemask)=0 \/ ~(exists pvs_factor_invertible_resultrightvaluemaskentrynondivisor. (dc_input_invertible_resultright) = (dc_index_invertible_resultrightvaluemask) * pvs_factor_invertible_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_invertible_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_invertible_resultrightvaluefold dst_positive_scale_invertible_resultrightvaluefold dst_negative_code_invertible_resultrightvaluefold dst_negative_scale_invertible_resultrightvaluefold dst_positive_sum_invertible_resultrightvaluefold dst_negative_sum_invertible_resultrightvaluefold. (((dc_mask_invertible_resultrightvalue) = (((((dst_positive_code_invertible_resultrightvaluefold) + (dst_positive_scale_invertible_resultrightvaluefold)) * S ((dst_positive_code_invertible_resultrightvaluefold) + (dst_positive_scale_invertible_resultrightvaluefold)) + ((dst_positive_scale_invertible_resultrightvaluefold) + (dst_positive_scale_invertible_resultrightvaluefold))) + (((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) * S ((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) + ((dst_negative_scale_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)))) * S ((((dst_positive_code_invertible_resultrightvaluefold) + (dst_positive_scale_invertible_resultrightvaluefold)) * S ((dst_positive_code_invertible_resultrightvaluefold) + (dst_positive_scale_invertible_resultrightvaluefold)) + ((dst_positive_scale_invertible_resultrightvaluefold) + (dst_positive_scale_invertible_resultrightvaluefold))) + (((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) * S ((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) + ((dst_negative_scale_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)))) + ((((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) * S ((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) + ((dst_negative_scale_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold))) + (((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) * S ((dst_negative_code_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)) + ((dst_negative_scale_invertible_resultrightvaluefold) + (dst_negative_scale_invertible_resultrightvaluefold)))))) /\ (((exists fs_u_dst_invertible_resultrightvaluefoldpositive fs_v_dst_invertible_resultrightvaluefoldpositive. ((((exists fs_h_dst_invertible_resultrightvaluefoldpositive_body_start. fs_h_dst_invertible_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_invertible_resultrightvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultrightvaluefoldpositive_body_start. fs_u_dst_invertible_resultrightvaluefoldpositive = fs_q_dst_invertible_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_invertible_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_invertible_resultrightvaluefoldpositive_body_terminal. fs_h_dst_invertible_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_invertible_resultrightvaluefold) = S ((S (S (dc_input_invertible_resultright))) * fs_v_dst_invertible_resultrightvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultrightvaluefoldpositive_body_terminal. fs_u_dst_invertible_resultrightvaluefoldpositive = fs_q_dst_invertible_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_invertible_resultright))) * fs_v_dst_invertible_resultrightvaluefoldpositive) + (dst_positive_sum_invertible_resultrightvaluefold))) /\ forall fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_invertible_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_invertible_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps = S (dc_input_invertible_resultright)) -> exists fs_a_dst_invertible_resultrightvaluefoldpositive_body_steps fs_r_dst_invertible_resultrightvaluefoldpositive_body_steps fs_s_dst_invertible_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_invertible_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_invertible_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_invertible_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_invertible_resultrightvaluefold)) /\ exists fs_q_dst_invertible_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_invertible_resultrightvaluefold = fs_q_dst_invertible_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_invertible_resultrightvaluefold) + (fs_a_dst_invertible_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_invertible_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_invertible_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_invertible_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_invertible_resultrightvaluefoldpositive = fs_q_dst_invertible_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldpositive) + (fs_r_dst_invertible_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_invertible_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_invertible_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_invertible_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldpositive)) /\ exists fs_q_dst_invertible_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_invertible_resultrightvaluefoldpositive = fs_q_dst_invertible_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_invertible_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldpositive) + (fs_s_dst_invertible_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_invertible_resultrightvaluefoldpositive_body_steps = fs_r_dst_invertible_resultrightvaluefoldpositive_body_steps + fs_a_dst_invertible_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_invertible_resultrightvaluefoldnegative fs_v_dst_invertible_resultrightvaluefoldnegative. ((((exists fs_h_dst_invertible_resultrightvaluefoldnegative_body_start. fs_h_dst_invertible_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_invertible_resultrightvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultrightvaluefoldnegative_body_start. fs_u_dst_invertible_resultrightvaluefoldnegative = fs_q_dst_invertible_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_invertible_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_invertible_resultrightvaluefoldnegative_body_terminal. fs_h_dst_invertible_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_invertible_resultrightvaluefold) = S ((S (S (dc_input_invertible_resultright))) * fs_v_dst_invertible_resultrightvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultrightvaluefoldnegative_body_terminal. fs_u_dst_invertible_resultrightvaluefoldnegative = fs_q_dst_invertible_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_invertible_resultright))) * fs_v_dst_invertible_resultrightvaluefoldnegative) + (dst_negative_sum_invertible_resultrightvaluefold))) /\ forall fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_invertible_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_invertible_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps = S (dc_input_invertible_resultright)) -> exists fs_a_dst_invertible_resultrightvaluefoldnegative_body_steps fs_r_dst_invertible_resultrightvaluefoldnegative_body_steps fs_s_dst_invertible_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_invertible_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_invertible_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_invertible_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_invertible_resultrightvaluefold)) /\ exists fs_q_dst_invertible_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_invertible_resultrightvaluefold = fs_q_dst_invertible_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_invertible_resultrightvaluefold) + (fs_a_dst_invertible_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_invertible_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_invertible_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_invertible_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_invertible_resultrightvaluefoldnegative = fs_q_dst_invertible_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldnegative) + (fs_r_dst_invertible_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_invertible_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_invertible_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_invertible_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldnegative)) /\ exists fs_q_dst_invertible_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_invertible_resultrightvaluefoldnegative = fs_q_dst_invertible_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_invertible_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_invertible_resultrightvaluefoldnegative) + (fs_s_dst_invertible_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_invertible_resultrightvaluefoldnegative_body_steps = fs_r_dst_invertible_resultrightvaluefoldnegative_body_steps + fs_a_dst_invertible_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_invertible_resultrightvaluefoldresult ge_balance_negative_invertible_resultrightvaluefoldresult. (((((dc_output_invertible_resultright) = 2 * (ge_balance_positive_invertible_resultrightvaluefoldresult) /\ (ge_balance_negative_invertible_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_invertible_resultrightvaluefoldresultdecode. (((dc_output_invertible_resultright) = 2 * ge_signed_half_invertible_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_invertible_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_invertible_resultrightvaluefoldresult) = S ge_signed_half_invertible_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_invertible_resultrightvaluefold) + ge_balance_negative_invertible_resultrightvaluefoldresult = (dst_negative_sum_invertible_resultrightvaluefold) + ge_balance_positive_invertible_resultrightvaluefoldresult)))))))))))))))))))))))) /\ (exists dst_positive_code_invertible_prescribed_zero dst_positive_scale_invertible_prescribed_zero dst_negative_code_invertible_prescribed_zero dst_negative_scale_invertible_prescribed_zero dst_positive_invertible_prescribed_zero dst_negative_invertible_prescribed_zero. (((G) = (((((dst_positive_code_invertible_prescribed_zero) + (dst_positive_scale_invertible_prescribed_zero)) * S ((dst_positive_code_invertible_prescribed_zero) + (dst_positive_scale_invertible_prescribed_zero)) + ((dst_positive_scale_invertible_prescribed_zero) + (dst_positive_scale_invertible_prescribed_zero))) + (((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) * S ((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) + ((dst_negative_scale_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)))) * S ((((dst_positive_code_invertible_prescribed_zero) + (dst_positive_scale_invertible_prescribed_zero)) * S ((dst_positive_code_invertible_prescribed_zero) + (dst_positive_scale_invertible_prescribed_zero)) + ((dst_positive_scale_invertible_prescribed_zero) + (dst_positive_scale_invertible_prescribed_zero))) + (((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) * S ((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) + ((dst_negative_scale_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)))) + ((((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) * S ((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) + ((dst_negative_scale_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero))) + (((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) * S ((dst_negative_code_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)) + ((dst_negative_scale_invertible_prescribed_zero) + (dst_negative_scale_invertible_prescribed_zero)))))) /\ (((((exists ff_h_pvs_invertible_prescribed_zeropositive. ff_h_pvs_invertible_prescribed_zeropositive + S (dst_positive_invertible_prescribed_zero) = S ((S (0)) * dst_positive_scale_invertible_prescribed_zero)) /\ exists ff_q_pvs_invertible_prescribed_zeropositive. dst_positive_code_invertible_prescribed_zero = ff_q_pvs_invertible_prescribed_zeropositive * S ((S (0)) * dst_positive_scale_invertible_prescribed_zero) + (dst_positive_invertible_prescribed_zero))) /\ (((((exists ff_h_pvs_invertible_prescribed_zeronegative. ff_h_pvs_invertible_prescribed_zeronegative + S (dst_negative_invertible_prescribed_zero) = S ((S (0)) * dst_negative_scale_invertible_prescribed_zero)) /\ exists ff_q_pvs_invertible_prescribed_zeronegative. dst_negative_code_invertible_prescribed_zero = ff_q_pvs_invertible_prescribed_zeronegative * S ((S (0)) * dst_negative_scale_invertible_prescribed_zero) + (dst_negative_invertible_prescribed_zero))) /\ (exists ge_balance_positive_invertible_prescribed_zerovalue ge_balance_negative_invertible_prescribed_zerovalue. (((((w) = 2 * (ge_balance_positive_invertible_prescribed_zerovalue) /\ (ge_balance_negative_invertible_prescribed_zerovalue) = 0) \/ exists ge_signed_half_invertible_prescribed_zerovaluedecode. (((w) = 2 * ge_signed_half_invertible_prescribed_zerovaluedecode + 1 /\ (ge_balance_positive_invertible_prescribed_zerovalue) = 0) /\ (ge_balance_negative_invertible_prescribed_zerovalue) = S ge_signed_half_invertible_prescribed_zerovaluedecode))) /\ ((dst_positive_invertible_prescribed_zero) + ge_balance_negative_invertible_prescribed_zerovalue = (dst_negative_invertible_prescribed_zero) + ge_balance_positive_invertible_prescribed_zerovalue))))))))))