signed_cofactor_minor_family_entry_exists

Exact expanded first-order arithmetic statement

forall pb pc nb nc q u v j. (forall ff_index_mce_family_full. (exists ff_gap_mce_full_index. ff_gap_mce_full_index + S (ff_index_mce_family_full) = (S q)) -> exists ff_value_mce_family_full. ((((exists ff_h_mce_full_entry. ff_h_mce_full_entry + S (ff_value_mce_family_full) = S ((S (ff_index_mce_family_full)) * v)) /\ exists ff_q_mce_full_entry. u = ff_q_mce_full_entry * S ((S (ff_index_mce_family_full)) * v) + (ff_value_mce_family_full))) /\ (exists ff_up_mce_record_full_record ff_us_mce_record_full_record ff_un_mce_record_full_record ff_ut_mce_record_full_record. ((ff_value_mce_family_full = ((((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) * S ((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) + ((ff_us_mce_record_full_record) + (ff_us_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record)))) * S ((((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) * S ((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) + ((ff_us_mce_record_full_record) + (ff_us_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record)))) + ((((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record))))) /\ (((forall ff_index_mdm_prefix_mce_full_record_minor_positive. (exists ff_gap_mdm_lt_mce_full_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_full_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_full_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_full_record_minor_positive ff_column_mdm_prefix_mce_full_record_minor_positive ff_value_mdm_prefix_mce_full_record_minor_positive. (ff_index_mdm_prefix_mce_full_record_minor_positive = (q) * ff_row_mdm_prefix_mce_full_record_minor_positive + ff_column_mdm_prefix_mce_full_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_full_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_full_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_full_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_full_record_minor_positive_cell ff_column_mdm_cell_mce_full_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_full_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_full_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_full_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_full_record_minor_positive_cell = ff_row_mdm_prefix_mce_full_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_full_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_full_record_minor_positive)) /\ ff_row_mdm_cell_mce_full_record_minor_positive_cell = S ff_row_mdm_prefix_mce_full_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_full_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_full_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_full_record_minor_positive) = (ff_index_mce_family_full)) /\ ff_column_mdm_cell_mce_full_record_minor_positive_cell = ff_column_mdm_prefix_mce_full_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_full_record_minor_positive_cell_column_after + (ff_index_mce_family_full) = (ff_column_mdm_prefix_mce_full_record_minor_positive)) /\ ff_column_mdm_cell_mce_full_record_minor_positive_cell = S ff_column_mdm_prefix_mce_full_record_minor_positive))) /\ (((exists ff_h_mdm_mce_full_record_minor_positive_cell_source. ff_h_mdm_mce_full_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_full_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_full_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_full_record_minor_positive_cell_source. pb = ff_q_mdm_mce_full_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_full_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_full_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_full_record_minor_positive_target. ff_h_mdm_mce_full_record_minor_positive_target + S (ff_value_mdm_prefix_mce_full_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_full_record_minor_positive)) * ff_us_mce_record_full_record)) /\ exists ff_q_mdm_mce_full_record_minor_positive_target. ff_up_mce_record_full_record = ff_q_mdm_mce_full_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_full_record_minor_positive)) * ff_us_mce_record_full_record) + (ff_value_mdm_prefix_mce_full_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_full_record_minor_negative. (exists ff_gap_mdm_lt_mce_full_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_full_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_full_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_full_record_minor_negative ff_column_mdm_prefix_mce_full_record_minor_negative ff_value_mdm_prefix_mce_full_record_minor_negative. (ff_index_mdm_prefix_mce_full_record_minor_negative = (q) * ff_row_mdm_prefix_mce_full_record_minor_negative + ff_column_mdm_prefix_mce_full_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_full_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_full_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_full_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_full_record_minor_negative_cell ff_column_mdm_cell_mce_full_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_full_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_full_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_full_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_full_record_minor_negative_cell = ff_row_mdm_prefix_mce_full_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_full_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_full_record_minor_negative)) /\ ff_row_mdm_cell_mce_full_record_minor_negative_cell = S ff_row_mdm_prefix_mce_full_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_full_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_full_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_full_record_minor_negative) = (ff_index_mce_family_full)) /\ ff_column_mdm_cell_mce_full_record_minor_negative_cell = ff_column_mdm_prefix_mce_full_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_full_record_minor_negative_cell_column_after + (ff_index_mce_family_full) = (ff_column_mdm_prefix_mce_full_record_minor_negative)) /\ ff_column_mdm_cell_mce_full_record_minor_negative_cell = S ff_column_mdm_prefix_mce_full_record_minor_negative))) /\ (((exists ff_h_mdm_mce_full_record_minor_negative_cell_source. ff_h_mdm_mce_full_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_full_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_full_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_full_record_minor_negative_cell_source. nb = ff_q_mdm_mce_full_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_full_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_full_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_full_record_minor_negative_target. ff_h_mdm_mce_full_record_minor_negative_target + S (ff_value_mdm_prefix_mce_full_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_full_record_minor_negative)) * ff_ut_mce_record_full_record)) /\ exists ff_q_mdm_mce_full_record_minor_negative_target. ff_un_mce_record_full_record = ff_q_mdm_mce_full_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_full_record_minor_negative)) * ff_ut_mce_record_full_record) + (ff_value_mdm_prefix_mce_full_record_minor_negative))))))))))))) -> (exists ff_gap_mce_record_column. ff_gap_mce_record_column + S (j) = (S q)) -> exists z. ((((exists ff_h_mce_entry_result. ff_h_mce_entry_result + S (z) = S ((S (j)) * v)) /\ exists ff_q_mce_entry_result. u = ff_q_mce_entry_result * S ((S (j)) * v) + (z))) /\ (exists ff_up_mce_record_family_entry ff_us_mce_record_family_entry ff_un_mce_record_family_entry ff_ut_mce_record_family_entry. ((z = ((((ff_up_mce_record_family_entry) + (ff_us_mce_record_family_entry)) * S ((ff_up_mce_record_family_entry) + (ff_us_mce_record_family_entry)) + ((ff_us_mce_record_family_entry) + (ff_us_mce_record_family_entry))) + (((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) * S ((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) + ((ff_ut_mce_record_family_entry) + (ff_ut_mce_record_family_entry)))) * S ((((ff_up_mce_record_family_entry) + (ff_us_mce_record_family_entry)) * S ((ff_up_mce_record_family_entry) + (ff_us_mce_record_family_entry)) + ((ff_us_mce_record_family_entry) + (ff_us_mce_record_family_entry))) + (((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) * S ((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) + ((ff_ut_mce_record_family_entry) + (ff_ut_mce_record_family_entry)))) + ((((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) * S ((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) + ((ff_ut_mce_record_family_entry) + (ff_ut_mce_record_family_entry))) + (((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) * S ((ff_un_mce_record_family_entry) + (ff_ut_mce_record_family_entry)) + ((ff_ut_mce_record_family_entry) + (ff_ut_mce_record_family_entry))))) /\ (((forall ff_index_mdm_prefix_mce_family_entry_minor_positive. (exists ff_gap_mdm_lt_mce_family_entry_minor_positive_index_bound. ff_gap_mdm_lt_mce_family_entry_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_family_entry_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_family_entry_minor_positive ff_column_mdm_prefix_mce_family_entry_minor_positive ff_value_mdm_prefix_mce_family_entry_minor_positive. (ff_index_mdm_prefix_mce_family_entry_minor_positive = (q) * ff_row_mdm_prefix_mce_family_entry_minor_positive + ff_column_mdm_prefix_mce_family_entry_minor_positive /\ ((exists ff_gap_mdm_lt_mce_family_entry_minor_positive_column_bound. ff_gap_mdm_lt_mce_family_entry_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_family_entry_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_family_entry_minor_positive_cell ff_column_mdm_cell_mce_family_entry_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_family_entry_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_family_entry_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_family_entry_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_family_entry_minor_positive_cell = ff_row_mdm_prefix_mce_family_entry_minor_positive) \/ ((exists ff_gap_mdm_le_mce_family_entry_minor_positive_cell_row_after. ff_gap_mdm_le_mce_family_entry_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_family_entry_minor_positive)) /\ ff_row_mdm_cell_mce_family_entry_minor_positive_cell = S ff_row_mdm_prefix_mce_family_entry_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_family_entry_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_family_entry_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_family_entry_minor_positive) = (j)) /\ ff_column_mdm_cell_mce_family_entry_minor_positive_cell = ff_column_mdm_prefix_mce_family_entry_minor_positive) \/ ((exists ff_gap_mdm_le_mce_family_entry_minor_positive_cell_column_after. ff_gap_mdm_le_mce_family_entry_minor_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mce_family_entry_minor_positive)) /\ ff_column_mdm_cell_mce_family_entry_minor_positive_cell = S ff_column_mdm_prefix_mce_family_entry_minor_positive))) /\ (((exists ff_h_mdm_mce_family_entry_minor_positive_cell_source. ff_h_mdm_mce_family_entry_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_family_entry_minor_positive) = S ((S ((ff_row_mdm_cell_mce_family_entry_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_entry_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_family_entry_minor_positive_cell_source. pb = ff_q_mdm_mce_family_entry_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_family_entry_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_entry_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_family_entry_minor_positive)))))) /\ (((exists ff_h_mdm_mce_family_entry_minor_positive_target. ff_h_mdm_mce_family_entry_minor_positive_target + S (ff_value_mdm_prefix_mce_family_entry_minor_positive) = S ((S (ff_index_mdm_prefix_mce_family_entry_minor_positive)) * ff_us_mce_record_family_entry)) /\ exists ff_q_mdm_mce_family_entry_minor_positive_target. ff_up_mce_record_family_entry = ff_q_mdm_mce_family_entry_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_family_entry_minor_positive)) * ff_us_mce_record_family_entry) + (ff_value_mdm_prefix_mce_family_entry_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_family_entry_minor_negative. (exists ff_gap_mdm_lt_mce_family_entry_minor_negative_index_bound. ff_gap_mdm_lt_mce_family_entry_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_family_entry_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_family_entry_minor_negative ff_column_mdm_prefix_mce_family_entry_minor_negative ff_value_mdm_prefix_mce_family_entry_minor_negative. (ff_index_mdm_prefix_mce_family_entry_minor_negative = (q) * ff_row_mdm_prefix_mce_family_entry_minor_negative + ff_column_mdm_prefix_mce_family_entry_minor_negative /\ ((exists ff_gap_mdm_lt_mce_family_entry_minor_negative_column_bound. ff_gap_mdm_lt_mce_family_entry_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_family_entry_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_family_entry_minor_negative_cell ff_column_mdm_cell_mce_family_entry_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_family_entry_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_family_entry_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_family_entry_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_family_entry_minor_negative_cell = ff_row_mdm_prefix_mce_family_entry_minor_negative) \/ ((exists ff_gap_mdm_le_mce_family_entry_minor_negative_cell_row_after. ff_gap_mdm_le_mce_family_entry_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_family_entry_minor_negative)) /\ ff_row_mdm_cell_mce_family_entry_minor_negative_cell = S ff_row_mdm_prefix_mce_family_entry_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_family_entry_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_family_entry_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_family_entry_minor_negative) = (j)) /\ ff_column_mdm_cell_mce_family_entry_minor_negative_cell = ff_column_mdm_prefix_mce_family_entry_minor_negative) \/ ((exists ff_gap_mdm_le_mce_family_entry_minor_negative_cell_column_after. ff_gap_mdm_le_mce_family_entry_minor_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mce_family_entry_minor_negative)) /\ ff_column_mdm_cell_mce_family_entry_minor_negative_cell = S ff_column_mdm_prefix_mce_family_entry_minor_negative))) /\ (((exists ff_h_mdm_mce_family_entry_minor_negative_cell_source. ff_h_mdm_mce_family_entry_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_family_entry_minor_negative) = S ((S ((ff_row_mdm_cell_mce_family_entry_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_entry_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_family_entry_minor_negative_cell_source. nb = ff_q_mdm_mce_family_entry_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_family_entry_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_entry_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_family_entry_minor_negative)))))) /\ (((exists ff_h_mdm_mce_family_entry_minor_negative_target. ff_h_mdm_mce_family_entry_minor_negative_target + S (ff_value_mdm_prefix_mce_family_entry_minor_negative) = S ((S (ff_index_mdm_prefix_mce_family_entry_minor_negative)) * ff_ut_mce_record_family_entry)) /\ exists ff_q_mdm_mce_family_entry_minor_negative_target. ff_un_mce_record_family_entry = ff_q_mdm_mce_family_entry_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_family_entry_minor_negative)) * ff_ut_mce_record_family_entry) + (ff_value_mdm_prefix_mce_family_entry_minor_negative))))))))))))