matrix_recursive_zero_extension

Exact expanded first-order arithmetic statement

forall mdr_pb_zero_extension mdr_pc_zero_extension mdr_nb_zero_extension mdr_nc_zero_extension mdr_b_zero_extension mdr_c_zero_extension mdr_l_zero_extension. (forall mdr_i_zero_extensionh. (exists mdr_gap_zero_extensionhi. mdr_gap_zero_extensionhi + S (mdr_i_zero_extensionh) = (mdr_l_zero_extension)) -> exists mdr_d_zero_extensionh mdr_pb_zero_extensionh mdr_pc_zero_extensionh mdr_nb_zero_extensionh mdr_nc_zero_extensionh mdr_p_zero_extensionh mdr_n_zero_extensionh. ((exists mdr_z_zero_extensionhr. ((exists mdr_a_zero_extensionhrc mdr_b_zero_extensionhrc mdr_c_zero_extensionhrc mdr_e_zero_extensionhrc mdr_f_zero_extensionhrc. ((mdr_a_zero_extensionhrc = ((mdr_d_zero_extensionh) + (mdr_pb_zero_extensionh)) * S ((mdr_d_zero_extensionh) + (mdr_pb_zero_extensionh)) + ((mdr_pb_zero_extensionh) + (mdr_pb_zero_extensionh))) /\ ((mdr_b_zero_extensionhrc = ((mdr_pc_zero_extensionh) + (mdr_nb_zero_extensionh)) * S ((mdr_pc_zero_extensionh) + (mdr_nb_zero_extensionh)) + ((mdr_nb_zero_extensionh) + (mdr_nb_zero_extensionh))) /\ ((mdr_c_zero_extensionhrc = ((mdr_a_zero_extensionhrc) + (mdr_b_zero_extensionhrc)) * S ((mdr_a_zero_extensionhrc) + (mdr_b_zero_extensionhrc)) + ((mdr_b_zero_extensionhrc) + (mdr_b_zero_extensionhrc))) /\ ((mdr_e_zero_extensionhrc = ((mdr_p_zero_extensionh) + (mdr_n_zero_extensionh)) * S ((mdr_p_zero_extensionh) + (mdr_n_zero_extensionh)) + ((mdr_n_zero_extensionh) + (mdr_n_zero_extensionh))) /\ ((mdr_f_zero_extensionhrc = ((mdr_nc_zero_extensionh) + (mdr_e_zero_extensionhrc)) * S ((mdr_nc_zero_extensionh) + (mdr_e_zero_extensionhrc)) + ((mdr_e_zero_extensionhrc) + (mdr_e_zero_extensionhrc))) /\ ((mdr_z_zero_extensionhr) = ((mdr_c_zero_extensionhrc) + (mdr_f_zero_extensionhrc)) * S ((mdr_c_zero_extensionhrc) + (mdr_f_zero_extensionhrc)) + ((mdr_f_zero_extensionhrc) + (mdr_f_zero_extensionhrc))))))))) /\ (((exists ff_h_mdr_zero_extensionhrb. ff_h_mdr_zero_extensionhrb + S (mdr_z_zero_extensionhr) = S ((S (mdr_i_zero_extensionh)) * mdr_c_zero_extension)) /\ exists ff_q_mdr_zero_extensionhrb. mdr_b_zero_extension = ff_q_mdr_zero_extensionhrb * S ((S (mdr_i_zero_extensionh)) * mdr_c_zero_extension) + (mdr_z_zero_extensionhr))))) /\ (((((mdr_d_zero_extensionh) = 0) /\ (((mdr_p_zero_extensionh) = 1) /\ ((mdr_n_zero_extensionh) = 0))) \/ exists mdr_q_zero_extensionhs mdr_eb_zero_extensionhs mdr_ec_zero_extensionhs mdr_fb_zero_extensionhs mdr_fc_zero_extensionhs. (((mdr_d_zero_extensionh) = S (mdr_q_zero_extensionhs)) /\ ((forall mdr_j_zero_extensionhsc. (exists mdr_gap_zero_extensionhscj. mdr_gap_zero_extensionhscj + S (mdr_j_zero_extensionhsc) = (S (mdr_q_zero_extensionhs))) -> exists mdr_i_zero_extensionhsc mdr_up_zero_extensionhsc mdr_us_zero_extensionhsc mdr_un_zero_extensionhsc mdr_ut_zero_extensionhsc mdr_p_zero_extensionhsc mdr_n_zero_extensionhsc. ((exists mdr_gap_zero_extensionhsci. mdr_gap_zero_extensionhsci + S (mdr_i_zero_extensionhsc) = (mdr_i_zero_extensionh)) /\ ((exists mdr_z_zero_extensionhscr. ((exists mdr_a_zero_extensionhscrc mdr_b_zero_extensionhscrc mdr_c_zero_extensionhscrc mdr_e_zero_extensionhscrc mdr_f_zero_extensionhscrc. ((mdr_a_zero_extensionhscrc = ((mdr_q_zero_extensionhs) + (mdr_up_zero_extensionhsc)) * S ((mdr_q_zero_extensionhs) + (mdr_up_zero_extensionhsc)) + ((mdr_up_zero_extensionhsc) + (mdr_up_zero_extensionhsc))) /\ ((mdr_b_zero_extensionhscrc = ((mdr_us_zero_extensionhsc) + (mdr_un_zero_extensionhsc)) * S ((mdr_us_zero_extensionhsc) + (mdr_un_zero_extensionhsc)) + ((mdr_un_zero_extensionhsc) + (mdr_un_zero_extensionhsc))) /\ ((mdr_c_zero_extensionhscrc = ((mdr_a_zero_extensionhscrc) + (mdr_b_zero_extensionhscrc)) * S ((mdr_a_zero_extensionhscrc) + (mdr_b_zero_extensionhscrc)) + ((mdr_b_zero_extensionhscrc) + (mdr_b_zero_extensionhscrc))) /\ ((mdr_e_zero_extensionhscrc = ((mdr_p_zero_extensionhsc) + (mdr_n_zero_extensionhsc)) * S ((mdr_p_zero_extensionhsc) + (mdr_n_zero_extensionhsc)) + ((mdr_n_zero_extensionhsc) + (mdr_n_zero_extensionhsc))) /\ ((mdr_f_zero_extensionhscrc = ((mdr_ut_zero_extensionhsc) + (mdr_e_zero_extensionhscrc)) * S ((mdr_ut_zero_extensionhsc) + (mdr_e_zero_extensionhscrc)) + ((mdr_e_zero_extensionhscrc) + (mdr_e_zero_extensionhscrc))) /\ ((mdr_z_zero_extensionhscr) = ((mdr_c_zero_extensionhscrc) + (mdr_f_zero_extensionhscrc)) * S ((mdr_c_zero_extensionhscrc) + (mdr_f_zero_extensionhscrc)) + ((mdr_f_zero_extensionhscrc) + (mdr_f_zero_extensionhscrc))))))))) /\ (((exists ff_h_mdr_zero_extensionhscrb. ff_h_mdr_zero_extensionhscrb + S (mdr_z_zero_extensionhscr) = S ((S (mdr_i_zero_extensionhsc)) * mdr_c_zero_extension)) /\ exists ff_q_mdr_zero_extensionhscrb. mdr_b_zero_extension = ff_q_mdr_zero_extensionhscrb * S ((S (mdr_i_zero_extensionhsc)) * mdr_c_zero_extension) + (mdr_z_zero_extensionhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_extensionhscm_positive. (exists ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_extensionhscm_positive) = ((mdr_q_zero_extensionhs) * (mdr_q_zero_extensionhs))) -> exists ff_row_mdm_prefix_mdr_zero_extensionhscm_positive ff_column_mdm_prefix_mdr_zero_extensionhscm_positive ff_value_mdm_prefix_mdr_zero_extensionhscm_positive. (ff_index_mdm_prefix_mdr_zero_extensionhscm_positive = (mdr_q_zero_extensionhs) * ff_row_mdm_prefix_mdr_zero_extensionhscm_positive + ff_column_mdm_prefix_mdr_zero_extensionhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_extensionhscm_positive) = (mdr_q_zero_extensionhs)) /\ ((exists ff_row_mdm_cell_mdr_zero_extensionhscm_positive_cell ff_column_mdm_cell_mdr_zero_extensionhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_extensionhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_extensionhscm_positive_cell = ff_row_mdm_prefix_mdr_zero_extensionhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_extensionhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_extensionhscm_positive)) /\ ff_row_mdm_cell_mdr_zero_extensionhscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_extensionhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_extensionhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_extensionhscm_positive) = (mdr_j_zero_extensionhsc)) /\ ff_column_mdm_cell_mdr_zero_extensionhscm_positive_cell = ff_column_mdm_prefix_mdr_zero_extensionhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_extensionhscm_positive_cell_column_after + (mdr_j_zero_extensionhsc) = (ff_column_mdm_prefix_mdr_zero_extensionhscm_positive)) /\ ff_column_mdm_cell_mdr_zero_extensionhscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_extensionhscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_extensionhscm_positive_cell_source. ff_h_mdm_mdr_zero_extensionhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_extensionhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_extensionhscm_positive_cell) * (S (mdr_q_zero_extensionhs)) + (ff_column_mdm_cell_mdr_zero_extensionhscm_positive_cell))) * mdr_pc_zero_extensionh)) /\ exists ff_q_mdm_mdr_zero_extensionhscm_positive_cell_source. mdr_pb_zero_extensionh = ff_q_mdm_mdr_zero_extensionhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_extensionhscm_positive_cell) * (S (mdr_q_zero_extensionhs)) + (ff_column_mdm_cell_mdr_zero_extensionhscm_positive_cell))) * mdr_pc_zero_extensionh) + (ff_value_mdm_prefix_mdr_zero_extensionhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_extensionhscm_positive_target. ff_h_mdm_mdr_zero_extensionhscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_extensionhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_extensionhscm_positive)) * mdr_us_zero_extensionhsc)) /\ exists ff_q_mdm_mdr_zero_extensionhscm_positive_target. mdr_up_zero_extensionhsc = ff_q_mdm_mdr_zero_extensionhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_extensionhscm_positive)) * mdr_us_zero_extensionhsc) + (ff_value_mdm_prefix_mdr_zero_extensionhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_extensionhscm_negative. (exists ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_extensionhscm_negative) = ((mdr_q_zero_extensionhs) * (mdr_q_zero_extensionhs))) -> exists ff_row_mdm_prefix_mdr_zero_extensionhscm_negative ff_column_mdm_prefix_mdr_zero_extensionhscm_negative ff_value_mdm_prefix_mdr_zero_extensionhscm_negative. (ff_index_mdm_prefix_mdr_zero_extensionhscm_negative = (mdr_q_zero_extensionhs) * ff_row_mdm_prefix_mdr_zero_extensionhscm_negative + ff_column_mdm_prefix_mdr_zero_extensionhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_extensionhscm_negative) = (mdr_q_zero_extensionhs)) /\ ((exists ff_row_mdm_cell_mdr_zero_extensionhscm_negative_cell ff_column_mdm_cell_mdr_zero_extensionhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_extensionhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_extensionhscm_negative_cell = ff_row_mdm_prefix_mdr_zero_extensionhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_extensionhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_extensionhscm_negative)) /\ ff_row_mdm_cell_mdr_zero_extensionhscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_extensionhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_extensionhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_extensionhscm_negative) = (mdr_j_zero_extensionhsc)) /\ ff_column_mdm_cell_mdr_zero_extensionhscm_negative_cell = ff_column_mdm_prefix_mdr_zero_extensionhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_extensionhscm_negative_cell_column_after + (mdr_j_zero_extensionhsc) = (ff_column_mdm_prefix_mdr_zero_extensionhscm_negative)) /\ ff_column_mdm_cell_mdr_zero_extensionhscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_extensionhscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_extensionhscm_negative_cell_source. ff_h_mdm_mdr_zero_extensionhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_extensionhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_extensionhscm_negative_cell) * (S (mdr_q_zero_extensionhs)) + (ff_column_mdm_cell_mdr_zero_extensionhscm_negative_cell))) * mdr_nc_zero_extensionh)) /\ exists ff_q_mdm_mdr_zero_extensionhscm_negative_cell_source. mdr_nb_zero_extensionh = ff_q_mdm_mdr_zero_extensionhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_extensionhscm_negative_cell) * (S (mdr_q_zero_extensionhs)) + (ff_column_mdm_cell_mdr_zero_extensionhscm_negative_cell))) * mdr_nc_zero_extensionh) + (ff_value_mdm_prefix_mdr_zero_extensionhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_extensionhscm_negative_target. ff_h_mdm_mdr_zero_extensionhscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_extensionhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_extensionhscm_negative)) * mdr_ut_zero_extensionhsc)) /\ exists ff_q_mdm_mdr_zero_extensionhscm_negative_target. mdr_un_zero_extensionhsc = ff_q_mdm_mdr_zero_extensionhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_extensionhscm_negative)) * mdr_ut_zero_extensionhsc) + (ff_value_mdm_prefix_mdr_zero_extensionhscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_extensionhscp. ff_h_mdr_zero_extensionhscp + S (mdr_p_zero_extensionhsc) = S ((S (mdr_j_zero_extensionhsc)) * mdr_ec_zero_extensionhs)) /\ exists ff_q_mdr_zero_extensionhscp. mdr_eb_zero_extensionhs = ff_q_mdr_zero_extensionhscp * S ((S (mdr_j_zero_extensionhsc)) * mdr_ec_zero_extensionhs) + (mdr_p_zero_extensionhsc))) /\ (((exists ff_h_mdr_zero_extensionhscn. ff_h_mdr_zero_extensionhscn + S (mdr_n_zero_extensionhsc) = S ((S (mdr_j_zero_extensionhsc)) * mdr_fc_zero_extensionhs)) /\ exists ff_q_mdr_zero_extensionhscn. mdr_fb_zero_extensionhs = ff_q_mdr_zero_extensionhscn * S ((S (mdr_j_zero_extensionhsc)) * mdr_fc_zero_extensionhs) + (mdr_n_zero_extensionhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_extensionhsf ff_uc_mce_fold_mdr_zero_extensionhsf ff_vb_mce_fold_mdr_zero_extensionhsf ff_vc_mce_fold_mdr_zero_extensionhsf. ((forall ff_index_mce_alternating_mdr_zero_extensionhsf_prefix. (exists ff_gap_mce_mdr_zero_extensionhsf_prefix_index. ff_gap_mce_mdr_zero_extensionhsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix) = (S (mdr_q_zero_extensionhs))) -> exists ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix ff_an_mce_alternating_mdr_zero_extensionhsf_prefix ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix ff_p_mce_alternating_mdr_zero_extensionhsf_prefix ff_n_mce_alternating_mdr_zero_extensionhsf_prefix. ((((exists ff_h_mce_mdr_zero_extensionhsf_prefix_ap. ff_h_mce_mdr_zero_extensionhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_pc_zero_extensionh)) /\ exists ff_q_mce_mdr_zero_extensionhsf_prefix_ap. mdr_pb_zero_extensionh = ff_q_mce_mdr_zero_extensionhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_pc_zero_extensionh) + (ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_prefix_an. ff_h_mce_mdr_zero_extensionhsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_extensionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_nc_zero_extensionh)) /\ exists ff_q_mce_mdr_zero_extensionhsf_prefix_an. mdr_nb_zero_extensionh = ff_q_mce_mdr_zero_extensionhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_nc_zero_extensionh) + (ff_an_mce_alternating_mdr_zero_extensionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_prefix_bp. ff_h_mce_mdr_zero_extensionhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_ec_zero_extensionhs)) /\ exists ff_q_mce_mdr_zero_extensionhsf_prefix_bp. mdr_eb_zero_extensionhs = ff_q_mce_mdr_zero_extensionhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_ec_zero_extensionhs) + (ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_prefix_bn. ff_h_mce_mdr_zero_extensionhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_fc_zero_extensionhs)) /\ exists ff_q_mce_mdr_zero_extensionhsf_prefix_bn. mdr_fb_zero_extensionhs = ff_q_mce_mdr_zero_extensionhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * mdr_fc_zero_extensionhs) + (ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_prefix_positive. ff_h_mce_mdr_zero_extensionhsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_extensionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * ff_uc_mce_fold_mdr_zero_extensionhsf)) /\ exists ff_q_mce_mdr_zero_extensionhsf_prefix_positive. ff_ub_mce_fold_mdr_zero_extensionhsf = ff_q_mce_mdr_zero_extensionhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * ff_uc_mce_fold_mdr_zero_extensionhsf) + (ff_p_mce_alternating_mdr_zero_extensionhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_prefix_negative. ff_h_mce_mdr_zero_extensionhsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_extensionhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * ff_vc_mce_fold_mdr_zero_extensionhsf)) /\ exists ff_q_mce_mdr_zero_extensionhsf_prefix_negative. ff_vb_mce_fold_mdr_zero_extensionhsf = ff_q_mce_mdr_zero_extensionhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_extensionhsf_prefix)) * ff_vc_mce_fold_mdr_zero_extensionhsf) + (ff_n_mce_alternating_mdr_zero_extensionhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_extensionhsf_prefix_term. ff_index_mce_alternating_mdr_zero_extensionhsf_prefix = 2 * ff_even_mce_term_mdr_zero_extensionhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_extensionhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix) /\ ff_n_mce_alternating_mdr_zero_extensionhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_extensionhsf_prefix_term. ff_index_mce_alternating_mdr_zero_extensionhsf_prefix = 2 * ff_odd_mce_term_mdr_zero_extensionhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_extensionhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix) /\ ff_n_mce_alternating_mdr_zero_extensionhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_extensionhsf_positive ff_v_mce_mdr_zero_extensionhsf_positive. ((((exists ff_h_mce_mdr_zero_extensionhsf_positive_start. ff_h_mce_mdr_zero_extensionhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_extensionhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionhsf_positive_start. ff_u_mce_mdr_zero_extensionhsf_positive = ff_q_mce_mdr_zero_extensionhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_extensionhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_positive_terminal. ff_h_mce_mdr_zero_extensionhsf_positive_terminal + S (mdr_p_zero_extensionh) = S ((S ((S (mdr_q_zero_extensionhs)))) * ff_v_mce_mdr_zero_extensionhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionhsf_positive_terminal. ff_u_mce_mdr_zero_extensionhsf_positive = ff_q_mce_mdr_zero_extensionhsf_positive_terminal * S ((S ((S (mdr_q_zero_extensionhs)))) * ff_v_mce_mdr_zero_extensionhsf_positive) + (mdr_p_zero_extensionh))) /\ forall ff_i_mce_mdr_zero_extensionhsf_positive. (exists ff_lt_mce_mdr_zero_extensionhsf_positive_bound. ff_lt_mce_mdr_zero_extensionhsf_positive_bound + S ff_i_mce_mdr_zero_extensionhsf_positive = (S (mdr_q_zero_extensionhs))) -> exists ff_a_mce_mdr_zero_extensionhsf_positive ff_r_mce_mdr_zero_extensionhsf_positive ff_s_mce_mdr_zero_extensionhsf_positive. ((((exists ff_h_mce_mdr_zero_extensionhsf_positive_summand. ff_h_mce_mdr_zero_extensionhsf_positive_summand + S (ff_a_mce_mdr_zero_extensionhsf_positive) = S ((S (ff_i_mce_mdr_zero_extensionhsf_positive)) * ff_uc_mce_fold_mdr_zero_extensionhsf)) /\ exists ff_q_mce_mdr_zero_extensionhsf_positive_summand. ff_ub_mce_fold_mdr_zero_extensionhsf = ff_q_mce_mdr_zero_extensionhsf_positive_summand * S ((S (ff_i_mce_mdr_zero_extensionhsf_positive)) * ff_uc_mce_fold_mdr_zero_extensionhsf) + (ff_a_mce_mdr_zero_extensionhsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_positive_partial. ff_h_mce_mdr_zero_extensionhsf_positive_partial + S (ff_r_mce_mdr_zero_extensionhsf_positive) = S ((S (ff_i_mce_mdr_zero_extensionhsf_positive)) * ff_v_mce_mdr_zero_extensionhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionhsf_positive_partial. ff_u_mce_mdr_zero_extensionhsf_positive = ff_q_mce_mdr_zero_extensionhsf_positive_partial * S ((S (ff_i_mce_mdr_zero_extensionhsf_positive)) * ff_v_mce_mdr_zero_extensionhsf_positive) + (ff_r_mce_mdr_zero_extensionhsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_positive_successor. ff_h_mce_mdr_zero_extensionhsf_positive_successor + S (ff_s_mce_mdr_zero_extensionhsf_positive) = S ((S (S ff_i_mce_mdr_zero_extensionhsf_positive)) * ff_v_mce_mdr_zero_extensionhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionhsf_positive_successor. ff_u_mce_mdr_zero_extensionhsf_positive = ff_q_mce_mdr_zero_extensionhsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_extensionhsf_positive)) * ff_v_mce_mdr_zero_extensionhsf_positive) + (ff_s_mce_mdr_zero_extensionhsf_positive))) /\ ff_s_mce_mdr_zero_extensionhsf_positive = ff_r_mce_mdr_zero_extensionhsf_positive + ff_a_mce_mdr_zero_extensionhsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_extensionhsf_negative ff_v_mce_mdr_zero_extensionhsf_negative. ((((exists ff_h_mce_mdr_zero_extensionhsf_negative_start. ff_h_mce_mdr_zero_extensionhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_extensionhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionhsf_negative_start. ff_u_mce_mdr_zero_extensionhsf_negative = ff_q_mce_mdr_zero_extensionhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_extensionhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_negative_terminal. ff_h_mce_mdr_zero_extensionhsf_negative_terminal + S (mdr_n_zero_extensionh) = S ((S ((S (mdr_q_zero_extensionhs)))) * ff_v_mce_mdr_zero_extensionhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionhsf_negative_terminal. ff_u_mce_mdr_zero_extensionhsf_negative = ff_q_mce_mdr_zero_extensionhsf_negative_terminal * S ((S ((S (mdr_q_zero_extensionhs)))) * ff_v_mce_mdr_zero_extensionhsf_negative) + (mdr_n_zero_extensionh))) /\ forall ff_i_mce_mdr_zero_extensionhsf_negative. (exists ff_lt_mce_mdr_zero_extensionhsf_negative_bound. ff_lt_mce_mdr_zero_extensionhsf_negative_bound + S ff_i_mce_mdr_zero_extensionhsf_negative = (S (mdr_q_zero_extensionhs))) -> exists ff_a_mce_mdr_zero_extensionhsf_negative ff_r_mce_mdr_zero_extensionhsf_negative ff_s_mce_mdr_zero_extensionhsf_negative. ((((exists ff_h_mce_mdr_zero_extensionhsf_negative_summand. ff_h_mce_mdr_zero_extensionhsf_negative_summand + S (ff_a_mce_mdr_zero_extensionhsf_negative) = S ((S (ff_i_mce_mdr_zero_extensionhsf_negative)) * ff_vc_mce_fold_mdr_zero_extensionhsf)) /\ exists ff_q_mce_mdr_zero_extensionhsf_negative_summand. ff_vb_mce_fold_mdr_zero_extensionhsf = ff_q_mce_mdr_zero_extensionhsf_negative_summand * S ((S (ff_i_mce_mdr_zero_extensionhsf_negative)) * ff_vc_mce_fold_mdr_zero_extensionhsf) + (ff_a_mce_mdr_zero_extensionhsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_negative_partial. ff_h_mce_mdr_zero_extensionhsf_negative_partial + S (ff_r_mce_mdr_zero_extensionhsf_negative) = S ((S (ff_i_mce_mdr_zero_extensionhsf_negative)) * ff_v_mce_mdr_zero_extensionhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionhsf_negative_partial. ff_u_mce_mdr_zero_extensionhsf_negative = ff_q_mce_mdr_zero_extensionhsf_negative_partial * S ((S (ff_i_mce_mdr_zero_extensionhsf_negative)) * ff_v_mce_mdr_zero_extensionhsf_negative) + (ff_r_mce_mdr_zero_extensionhsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_extensionhsf_negative_successor. ff_h_mce_mdr_zero_extensionhsf_negative_successor + S (ff_s_mce_mdr_zero_extensionhsf_negative) = S ((S (S ff_i_mce_mdr_zero_extensionhsf_negative)) * ff_v_mce_mdr_zero_extensionhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionhsf_negative_successor. ff_u_mce_mdr_zero_extensionhsf_negative = ff_q_mce_mdr_zero_extensionhsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_extensionhsf_negative)) * ff_v_mce_mdr_zero_extensionhsf_negative) + (ff_s_mce_mdr_zero_extensionhsf_negative))) /\ ff_s_mce_mdr_zero_extensionhsf_negative = ff_r_mce_mdr_zero_extensionhsf_negative + ff_a_mce_mdr_zero_extensionhsf_negative))))))))))))))) -> exists mdr_u_zero_extension mdr_v_zero_extension mdr_t_zero_extension mdr_p_zero_extension mdr_n_zero_extension. ((forall mdr_i_zero_extensionrp mdr_a_zero_extensionrp. (exists mdr_gap_zero_extensionrpb. mdr_gap_zero_extensionrpb + S (mdr_i_zero_extensionrp) = (mdr_l_zero_extension)) -> (((exists ff_h_mdr_zero_extensionrpo. ff_h_mdr_zero_extensionrpo + S (mdr_a_zero_extensionrp) = S ((S (mdr_i_zero_extensionrp)) * mdr_c_zero_extension)) /\ exists ff_q_mdr_zero_extensionrpo. mdr_b_zero_extension = ff_q_mdr_zero_extensionrpo * S ((S (mdr_i_zero_extensionrp)) * mdr_c_zero_extension) + (mdr_a_zero_extensionrp))) -> (((exists ff_h_mdr_zero_extensionrpn. ff_h_mdr_zero_extensionrpn + S (mdr_a_zero_extensionrp) = S ((S (mdr_i_zero_extensionrp)) * mdr_v_zero_extension)) /\ exists ff_q_mdr_zero_extensionrpn. mdr_u_zero_extension = ff_q_mdr_zero_extensionrpn * S ((S (mdr_i_zero_extensionrp)) * mdr_v_zero_extension) + (mdr_a_zero_extensionrp)))) /\ ((exists mdr_gap_zero_extensionrl. mdr_gap_zero_extensionrl + (mdr_l_zero_extension) = (mdr_t_zero_extension)) /\ ((forall mdr_i_zero_extensionrh. (exists mdr_gap_zero_extensionrhi. mdr_gap_zero_extensionrhi + S (mdr_i_zero_extensionrh) = (S (mdr_t_zero_extension))) -> exists mdr_d_zero_extensionrh mdr_pb_zero_extensionrh mdr_pc_zero_extensionrh mdr_nb_zero_extensionrh mdr_nc_zero_extensionrh mdr_p_zero_extensionrh mdr_n_zero_extensionrh. ((exists mdr_z_zero_extensionrhr. ((exists mdr_a_zero_extensionrhrc mdr_b_zero_extensionrhrc mdr_c_zero_extensionrhrc mdr_e_zero_extensionrhrc mdr_f_zero_extensionrhrc. ((mdr_a_zero_extensionrhrc = ((mdr_d_zero_extensionrh) + (mdr_pb_zero_extensionrh)) * S ((mdr_d_zero_extensionrh) + (mdr_pb_zero_extensionrh)) + ((mdr_pb_zero_extensionrh) + (mdr_pb_zero_extensionrh))) /\ ((mdr_b_zero_extensionrhrc = ((mdr_pc_zero_extensionrh) + (mdr_nb_zero_extensionrh)) * S ((mdr_pc_zero_extensionrh) + (mdr_nb_zero_extensionrh)) + ((mdr_nb_zero_extensionrh) + (mdr_nb_zero_extensionrh))) /\ ((mdr_c_zero_extensionrhrc = ((mdr_a_zero_extensionrhrc) + (mdr_b_zero_extensionrhrc)) * S ((mdr_a_zero_extensionrhrc) + (mdr_b_zero_extensionrhrc)) + ((mdr_b_zero_extensionrhrc) + (mdr_b_zero_extensionrhrc))) /\ ((mdr_e_zero_extensionrhrc = ((mdr_p_zero_extensionrh) + (mdr_n_zero_extensionrh)) * S ((mdr_p_zero_extensionrh) + (mdr_n_zero_extensionrh)) + ((mdr_n_zero_extensionrh) + (mdr_n_zero_extensionrh))) /\ ((mdr_f_zero_extensionrhrc = ((mdr_nc_zero_extensionrh) + (mdr_e_zero_extensionrhrc)) * S ((mdr_nc_zero_extensionrh) + (mdr_e_zero_extensionrhrc)) + ((mdr_e_zero_extensionrhrc) + (mdr_e_zero_extensionrhrc))) /\ ((mdr_z_zero_extensionrhr) = ((mdr_c_zero_extensionrhrc) + (mdr_f_zero_extensionrhrc)) * S ((mdr_c_zero_extensionrhrc) + (mdr_f_zero_extensionrhrc)) + ((mdr_f_zero_extensionrhrc) + (mdr_f_zero_extensionrhrc))))))))) /\ (((exists ff_h_mdr_zero_extensionrhrb. ff_h_mdr_zero_extensionrhrb + S (mdr_z_zero_extensionrhr) = S ((S (mdr_i_zero_extensionrh)) * mdr_v_zero_extension)) /\ exists ff_q_mdr_zero_extensionrhrb. mdr_u_zero_extension = ff_q_mdr_zero_extensionrhrb * S ((S (mdr_i_zero_extensionrh)) * mdr_v_zero_extension) + (mdr_z_zero_extensionrhr))))) /\ (((((mdr_d_zero_extensionrh) = 0) /\ (((mdr_p_zero_extensionrh) = 1) /\ ((mdr_n_zero_extensionrh) = 0))) \/ exists mdr_q_zero_extensionrhs mdr_eb_zero_extensionrhs mdr_ec_zero_extensionrhs mdr_fb_zero_extensionrhs mdr_fc_zero_extensionrhs. (((mdr_d_zero_extensionrh) = S (mdr_q_zero_extensionrhs)) /\ ((forall mdr_j_zero_extensionrhsc. (exists mdr_gap_zero_extensionrhscj. mdr_gap_zero_extensionrhscj + S (mdr_j_zero_extensionrhsc) = (S (mdr_q_zero_extensionrhs))) -> exists mdr_i_zero_extensionrhsc mdr_up_zero_extensionrhsc mdr_us_zero_extensionrhsc mdr_un_zero_extensionrhsc mdr_ut_zero_extensionrhsc mdr_p_zero_extensionrhsc mdr_n_zero_extensionrhsc. ((exists mdr_gap_zero_extensionrhsci. mdr_gap_zero_extensionrhsci + S (mdr_i_zero_extensionrhsc) = (mdr_i_zero_extensionrh)) /\ ((exists mdr_z_zero_extensionrhscr. ((exists mdr_a_zero_extensionrhscrc mdr_b_zero_extensionrhscrc mdr_c_zero_extensionrhscrc mdr_e_zero_extensionrhscrc mdr_f_zero_extensionrhscrc. ((mdr_a_zero_extensionrhscrc = ((mdr_q_zero_extensionrhs) + (mdr_up_zero_extensionrhsc)) * S ((mdr_q_zero_extensionrhs) + (mdr_up_zero_extensionrhsc)) + ((mdr_up_zero_extensionrhsc) + (mdr_up_zero_extensionrhsc))) /\ ((mdr_b_zero_extensionrhscrc = ((mdr_us_zero_extensionrhsc) + (mdr_un_zero_extensionrhsc)) * S ((mdr_us_zero_extensionrhsc) + (mdr_un_zero_extensionrhsc)) + ((mdr_un_zero_extensionrhsc) + (mdr_un_zero_extensionrhsc))) /\ ((mdr_c_zero_extensionrhscrc = ((mdr_a_zero_extensionrhscrc) + (mdr_b_zero_extensionrhscrc)) * S ((mdr_a_zero_extensionrhscrc) + (mdr_b_zero_extensionrhscrc)) + ((mdr_b_zero_extensionrhscrc) + (mdr_b_zero_extensionrhscrc))) /\ ((mdr_e_zero_extensionrhscrc = ((mdr_p_zero_extensionrhsc) + (mdr_n_zero_extensionrhsc)) * S ((mdr_p_zero_extensionrhsc) + (mdr_n_zero_extensionrhsc)) + ((mdr_n_zero_extensionrhsc) + (mdr_n_zero_extensionrhsc))) /\ ((mdr_f_zero_extensionrhscrc = ((mdr_ut_zero_extensionrhsc) + (mdr_e_zero_extensionrhscrc)) * S ((mdr_ut_zero_extensionrhsc) + (mdr_e_zero_extensionrhscrc)) + ((mdr_e_zero_extensionrhscrc) + (mdr_e_zero_extensionrhscrc))) /\ ((mdr_z_zero_extensionrhscr) = ((mdr_c_zero_extensionrhscrc) + (mdr_f_zero_extensionrhscrc)) * S ((mdr_c_zero_extensionrhscrc) + (mdr_f_zero_extensionrhscrc)) + ((mdr_f_zero_extensionrhscrc) + (mdr_f_zero_extensionrhscrc))))))))) /\ (((exists ff_h_mdr_zero_extensionrhscrb. ff_h_mdr_zero_extensionrhscrb + S (mdr_z_zero_extensionrhscr) = S ((S (mdr_i_zero_extensionrhsc)) * mdr_v_zero_extension)) /\ exists ff_q_mdr_zero_extensionrhscrb. mdr_u_zero_extension = ff_q_mdr_zero_extensionrhscrb * S ((S (mdr_i_zero_extensionrhsc)) * mdr_v_zero_extension) + (mdr_z_zero_extensionrhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_zero_extensionrhscm_positive. (exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_index_bound. ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_zero_extensionrhscm_positive) = ((mdr_q_zero_extensionrhs) * (mdr_q_zero_extensionrhs))) -> exists ff_row_mdm_prefix_mdr_zero_extensionrhscm_positive ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive ff_value_mdm_prefix_mdr_zero_extensionrhscm_positive. (ff_index_mdm_prefix_mdr_zero_extensionrhscm_positive = (mdr_q_zero_extensionrhs) * ff_row_mdm_prefix_mdr_zero_extensionrhscm_positive + ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_column_bound. ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive) = (mdr_q_zero_extensionrhs)) /\ ((exists ff_row_mdm_cell_mdr_zero_extensionrhscm_positive_cell ff_column_mdm_cell_mdr_zero_extensionrhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_extensionrhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_zero_extensionrhscm_positive_cell = ff_row_mdm_prefix_mdr_zero_extensionrhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionrhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_zero_extensionrhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_extensionrhscm_positive)) /\ ff_row_mdm_cell_mdr_zero_extensionrhscm_positive_cell = S ff_row_mdm_prefix_mdr_zero_extensionrhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_zero_extensionrhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive) = (mdr_j_zero_extensionrhsc)) /\ ff_column_mdm_cell_mdr_zero_extensionrhscm_positive_cell = ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionrhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_zero_extensionrhscm_positive_cell_column_after + (mdr_j_zero_extensionrhsc) = (ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive)) /\ ff_column_mdm_cell_mdr_zero_extensionrhscm_positive_cell = S ff_column_mdm_prefix_mdr_zero_extensionrhscm_positive))) /\ (((exists ff_h_mdm_mdr_zero_extensionrhscm_positive_cell_source. ff_h_mdm_mdr_zero_extensionrhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_zero_extensionrhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_zero_extensionrhscm_positive_cell) * (S (mdr_q_zero_extensionrhs)) + (ff_column_mdm_cell_mdr_zero_extensionrhscm_positive_cell))) * mdr_pc_zero_extensionrh)) /\ exists ff_q_mdm_mdr_zero_extensionrhscm_positive_cell_source. mdr_pb_zero_extensionrh = ff_q_mdm_mdr_zero_extensionrhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_extensionrhscm_positive_cell) * (S (mdr_q_zero_extensionrhs)) + (ff_column_mdm_cell_mdr_zero_extensionrhscm_positive_cell))) * mdr_pc_zero_extensionrh) + (ff_value_mdm_prefix_mdr_zero_extensionrhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_zero_extensionrhscm_positive_target. ff_h_mdm_mdr_zero_extensionrhscm_positive_target + S (ff_value_mdm_prefix_mdr_zero_extensionrhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_zero_extensionrhscm_positive)) * mdr_us_zero_extensionrhsc)) /\ exists ff_q_mdm_mdr_zero_extensionrhscm_positive_target. mdr_up_zero_extensionrhsc = ff_q_mdm_mdr_zero_extensionrhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_zero_extensionrhscm_positive)) * mdr_us_zero_extensionrhsc) + (ff_value_mdm_prefix_mdr_zero_extensionrhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_zero_extensionrhscm_negative. (exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_index_bound. ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_zero_extensionrhscm_negative) = ((mdr_q_zero_extensionrhs) * (mdr_q_zero_extensionrhs))) -> exists ff_row_mdm_prefix_mdr_zero_extensionrhscm_negative ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative ff_value_mdm_prefix_mdr_zero_extensionrhscm_negative. (ff_index_mdm_prefix_mdr_zero_extensionrhscm_negative = (mdr_q_zero_extensionrhs) * ff_row_mdm_prefix_mdr_zero_extensionrhscm_negative + ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_column_bound. ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative) = (mdr_q_zero_extensionrhs)) /\ ((exists ff_row_mdm_cell_mdr_zero_extensionrhscm_negative_cell ff_column_mdm_cell_mdr_zero_extensionrhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_zero_extensionrhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_zero_extensionrhscm_negative_cell = ff_row_mdm_prefix_mdr_zero_extensionrhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionrhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_zero_extensionrhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_zero_extensionrhscm_negative)) /\ ff_row_mdm_cell_mdr_zero_extensionrhscm_negative_cell = S ff_row_mdm_prefix_mdr_zero_extensionrhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_zero_extensionrhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative) = (mdr_j_zero_extensionrhsc)) /\ ff_column_mdm_cell_mdr_zero_extensionrhscm_negative_cell = ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_zero_extensionrhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_zero_extensionrhscm_negative_cell_column_after + (mdr_j_zero_extensionrhsc) = (ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative)) /\ ff_column_mdm_cell_mdr_zero_extensionrhscm_negative_cell = S ff_column_mdm_prefix_mdr_zero_extensionrhscm_negative))) /\ (((exists ff_h_mdm_mdr_zero_extensionrhscm_negative_cell_source. ff_h_mdm_mdr_zero_extensionrhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_zero_extensionrhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_zero_extensionrhscm_negative_cell) * (S (mdr_q_zero_extensionrhs)) + (ff_column_mdm_cell_mdr_zero_extensionrhscm_negative_cell))) * mdr_nc_zero_extensionrh)) /\ exists ff_q_mdm_mdr_zero_extensionrhscm_negative_cell_source. mdr_nb_zero_extensionrh = ff_q_mdm_mdr_zero_extensionrhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_zero_extensionrhscm_negative_cell) * (S (mdr_q_zero_extensionrhs)) + (ff_column_mdm_cell_mdr_zero_extensionrhscm_negative_cell))) * mdr_nc_zero_extensionrh) + (ff_value_mdm_prefix_mdr_zero_extensionrhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_zero_extensionrhscm_negative_target. ff_h_mdm_mdr_zero_extensionrhscm_negative_target + S (ff_value_mdm_prefix_mdr_zero_extensionrhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_zero_extensionrhscm_negative)) * mdr_ut_zero_extensionrhsc)) /\ exists ff_q_mdm_mdr_zero_extensionrhscm_negative_target. mdr_un_zero_extensionrhsc = ff_q_mdm_mdr_zero_extensionrhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_zero_extensionrhscm_negative)) * mdr_ut_zero_extensionrhsc) + (ff_value_mdm_prefix_mdr_zero_extensionrhscm_negative))))))))) /\ ((((exists ff_h_mdr_zero_extensionrhscp. ff_h_mdr_zero_extensionrhscp + S (mdr_p_zero_extensionrhsc) = S ((S (mdr_j_zero_extensionrhsc)) * mdr_ec_zero_extensionrhs)) /\ exists ff_q_mdr_zero_extensionrhscp. mdr_eb_zero_extensionrhs = ff_q_mdr_zero_extensionrhscp * S ((S (mdr_j_zero_extensionrhsc)) * mdr_ec_zero_extensionrhs) + (mdr_p_zero_extensionrhsc))) /\ (((exists ff_h_mdr_zero_extensionrhscn. ff_h_mdr_zero_extensionrhscn + S (mdr_n_zero_extensionrhsc) = S ((S (mdr_j_zero_extensionrhsc)) * mdr_fc_zero_extensionrhs)) /\ exists ff_q_mdr_zero_extensionrhscn. mdr_fb_zero_extensionrhs = ff_q_mdr_zero_extensionrhscn * S ((S (mdr_j_zero_extensionrhsc)) * mdr_fc_zero_extensionrhs) + (mdr_n_zero_extensionrhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_zero_extensionrhsf ff_uc_mce_fold_mdr_zero_extensionrhsf ff_vb_mce_fold_mdr_zero_extensionrhsf ff_vc_mce_fold_mdr_zero_extensionrhsf. ((forall ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix. (exists ff_gap_mce_mdr_zero_extensionrhsf_prefix_index. ff_gap_mce_mdr_zero_extensionrhsf_prefix_index + S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix) = (S (mdr_q_zero_extensionrhs))) -> exists ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix ff_p_mce_alternating_mdr_zero_extensionrhsf_prefix ff_n_mce_alternating_mdr_zero_extensionrhsf_prefix. ((((exists ff_h_mce_mdr_zero_extensionrhsf_prefix_ap. ff_h_mce_mdr_zero_extensionrhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_pc_zero_extensionrh)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_prefix_ap. mdr_pb_zero_extensionrh = ff_q_mce_mdr_zero_extensionrhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_pc_zero_extensionrh) + (ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_prefix_an. ff_h_mce_mdr_zero_extensionrhsf_prefix_an + S (ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_nc_zero_extensionrh)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_prefix_an. mdr_nb_zero_extensionrh = ff_q_mce_mdr_zero_extensionrhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_nc_zero_extensionrh) + (ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_prefix_bp. ff_h_mce_mdr_zero_extensionrhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_ec_zero_extensionrhs)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_prefix_bp. mdr_eb_zero_extensionrhs = ff_q_mce_mdr_zero_extensionrhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_ec_zero_extensionrhs) + (ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_prefix_bn. ff_h_mce_mdr_zero_extensionrhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_fc_zero_extensionrhs)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_prefix_bn. mdr_fb_zero_extensionrhs = ff_q_mce_mdr_zero_extensionrhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * mdr_fc_zero_extensionrhs) + (ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_prefix_positive. ff_h_mce_mdr_zero_extensionrhsf_prefix_positive + S (ff_p_mce_alternating_mdr_zero_extensionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * ff_uc_mce_fold_mdr_zero_extensionrhsf)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_prefix_positive. ff_ub_mce_fold_mdr_zero_extensionrhsf = ff_q_mce_mdr_zero_extensionrhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * ff_uc_mce_fold_mdr_zero_extensionrhsf) + (ff_p_mce_alternating_mdr_zero_extensionrhsf_prefix))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_prefix_negative. ff_h_mce_mdr_zero_extensionrhsf_prefix_negative + S (ff_n_mce_alternating_mdr_zero_extensionrhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * ff_vc_mce_fold_mdr_zero_extensionrhsf)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_prefix_negative. ff_vb_mce_fold_mdr_zero_extensionrhsf = ff_q_mce_mdr_zero_extensionrhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix)) * ff_vc_mce_fold_mdr_zero_extensionrhsf) + (ff_n_mce_alternating_mdr_zero_extensionrhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_zero_extensionrhsf_prefix_term. ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix = 2 * ff_even_mce_term_mdr_zero_extensionrhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_zero_extensionrhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix) /\ ff_n_mce_alternating_mdr_zero_extensionrhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_zero_extensionrhsf_prefix_term. ff_index_mce_alternating_mdr_zero_extensionrhsf_prefix = 2 * ff_odd_mce_term_mdr_zero_extensionrhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_zero_extensionrhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix) /\ ff_n_mce_alternating_mdr_zero_extensionrhsf_prefix = (ff_ap_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bp_mce_alternating_mdr_zero_extensionrhsf_prefix) + (ff_an_mce_alternating_mdr_zero_extensionrhsf_prefix) * (ff_bn_mce_alternating_mdr_zero_extensionrhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_zero_extensionrhsf_positive ff_v_mce_mdr_zero_extensionrhsf_positive. ((((exists ff_h_mce_mdr_zero_extensionrhsf_positive_start. ff_h_mce_mdr_zero_extensionrhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_extensionrhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_positive_start. ff_u_mce_mdr_zero_extensionrhsf_positive = ff_q_mce_mdr_zero_extensionrhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_zero_extensionrhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_positive_terminal. ff_h_mce_mdr_zero_extensionrhsf_positive_terminal + S (mdr_p_zero_extensionrh) = S ((S ((S (mdr_q_zero_extensionrhs)))) * ff_v_mce_mdr_zero_extensionrhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_positive_terminal. ff_u_mce_mdr_zero_extensionrhsf_positive = ff_q_mce_mdr_zero_extensionrhsf_positive_terminal * S ((S ((S (mdr_q_zero_extensionrhs)))) * ff_v_mce_mdr_zero_extensionrhsf_positive) + (mdr_p_zero_extensionrh))) /\ forall ff_i_mce_mdr_zero_extensionrhsf_positive. (exists ff_lt_mce_mdr_zero_extensionrhsf_positive_bound. ff_lt_mce_mdr_zero_extensionrhsf_positive_bound + S ff_i_mce_mdr_zero_extensionrhsf_positive = (S (mdr_q_zero_extensionrhs))) -> exists ff_a_mce_mdr_zero_extensionrhsf_positive ff_r_mce_mdr_zero_extensionrhsf_positive ff_s_mce_mdr_zero_extensionrhsf_positive. ((((exists ff_h_mce_mdr_zero_extensionrhsf_positive_summand. ff_h_mce_mdr_zero_extensionrhsf_positive_summand + S (ff_a_mce_mdr_zero_extensionrhsf_positive) = S ((S (ff_i_mce_mdr_zero_extensionrhsf_positive)) * ff_uc_mce_fold_mdr_zero_extensionrhsf)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_positive_summand. ff_ub_mce_fold_mdr_zero_extensionrhsf = ff_q_mce_mdr_zero_extensionrhsf_positive_summand * S ((S (ff_i_mce_mdr_zero_extensionrhsf_positive)) * ff_uc_mce_fold_mdr_zero_extensionrhsf) + (ff_a_mce_mdr_zero_extensionrhsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_positive_partial. ff_h_mce_mdr_zero_extensionrhsf_positive_partial + S (ff_r_mce_mdr_zero_extensionrhsf_positive) = S ((S (ff_i_mce_mdr_zero_extensionrhsf_positive)) * ff_v_mce_mdr_zero_extensionrhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_positive_partial. ff_u_mce_mdr_zero_extensionrhsf_positive = ff_q_mce_mdr_zero_extensionrhsf_positive_partial * S ((S (ff_i_mce_mdr_zero_extensionrhsf_positive)) * ff_v_mce_mdr_zero_extensionrhsf_positive) + (ff_r_mce_mdr_zero_extensionrhsf_positive))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_positive_successor. ff_h_mce_mdr_zero_extensionrhsf_positive_successor + S (ff_s_mce_mdr_zero_extensionrhsf_positive) = S ((S (S ff_i_mce_mdr_zero_extensionrhsf_positive)) * ff_v_mce_mdr_zero_extensionrhsf_positive)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_positive_successor. ff_u_mce_mdr_zero_extensionrhsf_positive = ff_q_mce_mdr_zero_extensionrhsf_positive_successor * S ((S (S ff_i_mce_mdr_zero_extensionrhsf_positive)) * ff_v_mce_mdr_zero_extensionrhsf_positive) + (ff_s_mce_mdr_zero_extensionrhsf_positive))) /\ ff_s_mce_mdr_zero_extensionrhsf_positive = ff_r_mce_mdr_zero_extensionrhsf_positive + ff_a_mce_mdr_zero_extensionrhsf_positive)))))) /\ (exists ff_u_mce_mdr_zero_extensionrhsf_negative ff_v_mce_mdr_zero_extensionrhsf_negative. ((((exists ff_h_mce_mdr_zero_extensionrhsf_negative_start. ff_h_mce_mdr_zero_extensionrhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_zero_extensionrhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_negative_start. ff_u_mce_mdr_zero_extensionrhsf_negative = ff_q_mce_mdr_zero_extensionrhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_zero_extensionrhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_negative_terminal. ff_h_mce_mdr_zero_extensionrhsf_negative_terminal + S (mdr_n_zero_extensionrh) = S ((S ((S (mdr_q_zero_extensionrhs)))) * ff_v_mce_mdr_zero_extensionrhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_negative_terminal. ff_u_mce_mdr_zero_extensionrhsf_negative = ff_q_mce_mdr_zero_extensionrhsf_negative_terminal * S ((S ((S (mdr_q_zero_extensionrhs)))) * ff_v_mce_mdr_zero_extensionrhsf_negative) + (mdr_n_zero_extensionrh))) /\ forall ff_i_mce_mdr_zero_extensionrhsf_negative. (exists ff_lt_mce_mdr_zero_extensionrhsf_negative_bound. ff_lt_mce_mdr_zero_extensionrhsf_negative_bound + S ff_i_mce_mdr_zero_extensionrhsf_negative = (S (mdr_q_zero_extensionrhs))) -> exists ff_a_mce_mdr_zero_extensionrhsf_negative ff_r_mce_mdr_zero_extensionrhsf_negative ff_s_mce_mdr_zero_extensionrhsf_negative. ((((exists ff_h_mce_mdr_zero_extensionrhsf_negative_summand. ff_h_mce_mdr_zero_extensionrhsf_negative_summand + S (ff_a_mce_mdr_zero_extensionrhsf_negative) = S ((S (ff_i_mce_mdr_zero_extensionrhsf_negative)) * ff_vc_mce_fold_mdr_zero_extensionrhsf)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_negative_summand. ff_vb_mce_fold_mdr_zero_extensionrhsf = ff_q_mce_mdr_zero_extensionrhsf_negative_summand * S ((S (ff_i_mce_mdr_zero_extensionrhsf_negative)) * ff_vc_mce_fold_mdr_zero_extensionrhsf) + (ff_a_mce_mdr_zero_extensionrhsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_negative_partial. ff_h_mce_mdr_zero_extensionrhsf_negative_partial + S (ff_r_mce_mdr_zero_extensionrhsf_negative) = S ((S (ff_i_mce_mdr_zero_extensionrhsf_negative)) * ff_v_mce_mdr_zero_extensionrhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_negative_partial. ff_u_mce_mdr_zero_extensionrhsf_negative = ff_q_mce_mdr_zero_extensionrhsf_negative_partial * S ((S (ff_i_mce_mdr_zero_extensionrhsf_negative)) * ff_v_mce_mdr_zero_extensionrhsf_negative) + (ff_r_mce_mdr_zero_extensionrhsf_negative))) /\ ((((exists ff_h_mce_mdr_zero_extensionrhsf_negative_successor. ff_h_mce_mdr_zero_extensionrhsf_negative_successor + S (ff_s_mce_mdr_zero_extensionrhsf_negative) = S ((S (S ff_i_mce_mdr_zero_extensionrhsf_negative)) * ff_v_mce_mdr_zero_extensionrhsf_negative)) /\ exists ff_q_mce_mdr_zero_extensionrhsf_negative_successor. ff_u_mce_mdr_zero_extensionrhsf_negative = ff_q_mce_mdr_zero_extensionrhsf_negative_successor * S ((S (S ff_i_mce_mdr_zero_extensionrhsf_negative)) * ff_v_mce_mdr_zero_extensionrhsf_negative) + (ff_s_mce_mdr_zero_extensionrhsf_negative))) /\ ff_s_mce_mdr_zero_extensionrhsf_negative = ff_r_mce_mdr_zero_extensionrhsf_negative + ff_a_mce_mdr_zero_extensionrhsf_negative))))))))))))))) /\ (exists mdr_z_zero_extensionrr. ((exists mdr_a_zero_extensionrrc mdr_b_zero_extensionrrc mdr_c_zero_extensionrrc mdr_e_zero_extensionrrc mdr_f_zero_extensionrrc. ((mdr_a_zero_extensionrrc = ((0) + (mdr_pb_zero_extension)) * S ((0) + (mdr_pb_zero_extension)) + ((mdr_pb_zero_extension) + (mdr_pb_zero_extension))) /\ ((mdr_b_zero_extensionrrc = ((mdr_pc_zero_extension) + (mdr_nb_zero_extension)) * S ((mdr_pc_zero_extension) + (mdr_nb_zero_extension)) + ((mdr_nb_zero_extension) + (mdr_nb_zero_extension))) /\ ((mdr_c_zero_extensionrrc = ((mdr_a_zero_extensionrrc) + (mdr_b_zero_extensionrrc)) * S ((mdr_a_zero_extensionrrc) + (mdr_b_zero_extensionrrc)) + ((mdr_b_zero_extensionrrc) + (mdr_b_zero_extensionrrc))) /\ ((mdr_e_zero_extensionrrc = ((mdr_p_zero_extension) + (mdr_n_zero_extension)) * S ((mdr_p_zero_extension) + (mdr_n_zero_extension)) + ((mdr_n_zero_extension) + (mdr_n_zero_extension))) /\ ((mdr_f_zero_extensionrrc = ((mdr_nc_zero_extension) + (mdr_e_zero_extensionrrc)) * S ((mdr_nc_zero_extension) + (mdr_e_zero_extensionrrc)) + ((mdr_e_zero_extensionrrc) + (mdr_e_zero_extensionrrc))) /\ ((mdr_z_zero_extensionrr) = ((mdr_c_zero_extensionrrc) + (mdr_f_zero_extensionrrc)) * S ((mdr_c_zero_extensionrrc) + (mdr_f_zero_extensionrrc)) + ((mdr_f_zero_extensionrrc) + (mdr_f_zero_extensionrrc))))))))) /\ (((exists ff_h_mdr_zero_extensionrrb. ff_h_mdr_zero_extensionrrb + S (mdr_z_zero_extensionrr) = S ((S (mdr_t_zero_extension)) * mdr_v_zero_extension)) /\ exists ff_q_mdr_zero_extensionrrb. mdr_u_zero_extension = ff_q_mdr_zero_extensionrrb * S ((S (mdr_t_zero_extension)) * mdr_v_zero_extension) + (mdr_z_zero_extensionrr))))))))