matrix_recursive_signed_minor_extensional

Exact expanded first-order arithmetic statement

forall pb pc nb nc qb qc rb rc q j up us un ut vp vs vn vt. (((forall mdr_i_parent_equalp mdr_a_parent_equalp. (exists mdr_gap_parent_equalpb. mdr_gap_parent_equalpb + S (mdr_i_parent_equalp) = ((S q) * (S q))) -> (((exists ff_h_mdr_parent_equalpo. ff_h_mdr_parent_equalpo + S (mdr_a_parent_equalp) = S ((S (mdr_i_parent_equalp)) * pc)) /\ exists ff_q_mdr_parent_equalpo. pb = ff_q_mdr_parent_equalpo * S ((S (mdr_i_parent_equalp)) * pc) + (mdr_a_parent_equalp))) -> (((exists ff_h_mdr_parent_equalpn. ff_h_mdr_parent_equalpn + S (mdr_a_parent_equalp) = S ((S (mdr_i_parent_equalp)) * qc)) /\ exists ff_q_mdr_parent_equalpn. qb = ff_q_mdr_parent_equalpn * S ((S (mdr_i_parent_equalp)) * qc) + (mdr_a_parent_equalp)))) /\ (forall mdr_i_parent_equaln mdr_a_parent_equaln. (exists mdr_gap_parent_equalnb. mdr_gap_parent_equalnb + S (mdr_i_parent_equaln) = ((S q) * (S q))) -> (((exists ff_h_mdr_parent_equalno. ff_h_mdr_parent_equalno + S (mdr_a_parent_equaln) = S ((S (mdr_i_parent_equaln)) * nc)) /\ exists ff_q_mdr_parent_equalno. nb = ff_q_mdr_parent_equalno * S ((S (mdr_i_parent_equaln)) * nc) + (mdr_a_parent_equaln))) -> (((exists ff_h_mdr_parent_equalnn. ff_h_mdr_parent_equalnn + S (mdr_a_parent_equaln) = S ((S (mdr_i_parent_equaln)) * rc)) /\ exists ff_q_mdr_parent_equalnn. rb = ff_q_mdr_parent_equalnn * S ((S (mdr_i_parent_equaln)) * rc) + (mdr_a_parent_equaln)))))) -> (((forall ff_index_mdm_prefix_mdr_left_signed_minor_positive. (exists ff_gap_mdm_lt_mdr_left_signed_minor_positive_index_bound. ff_gap_mdm_lt_mdr_left_signed_minor_positive_index_bound + S (ff_index_mdm_prefix_mdr_left_signed_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_left_signed_minor_positive ff_column_mdm_prefix_mdr_left_signed_minor_positive ff_value_mdm_prefix_mdr_left_signed_minor_positive. (ff_index_mdm_prefix_mdr_left_signed_minor_positive = (q) * ff_row_mdm_prefix_mdr_left_signed_minor_positive + ff_column_mdm_prefix_mdr_left_signed_minor_positive /\ ((exists ff_gap_mdm_lt_mdr_left_signed_minor_positive_column_bound. ff_gap_mdm_lt_mdr_left_signed_minor_positive_column_bound + S (ff_column_mdm_prefix_mdr_left_signed_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_left_signed_minor_positive_cell ff_column_mdm_cell_mdr_left_signed_minor_positive_cell. (((((exists ff_gap_mdm_lt_mdr_left_signed_minor_positive_cell_row_before. ff_gap_mdm_lt_mdr_left_signed_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_left_signed_minor_positive) = (0)) /\ ff_row_mdm_cell_mdr_left_signed_minor_positive_cell = ff_row_mdm_prefix_mdr_left_signed_minor_positive) \/ ((exists ff_gap_mdm_le_mdr_left_signed_minor_positive_cell_row_after. ff_gap_mdm_le_mdr_left_signed_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_left_signed_minor_positive)) /\ ff_row_mdm_cell_mdr_left_signed_minor_positive_cell = S ff_row_mdm_prefix_mdr_left_signed_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_left_signed_minor_positive_cell_column_before. ff_gap_mdm_lt_mdr_left_signed_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_left_signed_minor_positive) = (j)) /\ ff_column_mdm_cell_mdr_left_signed_minor_positive_cell = ff_column_mdm_prefix_mdr_left_signed_minor_positive) \/ ((exists ff_gap_mdm_le_mdr_left_signed_minor_positive_cell_column_after. ff_gap_mdm_le_mdr_left_signed_minor_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_left_signed_minor_positive)) /\ ff_column_mdm_cell_mdr_left_signed_minor_positive_cell = S ff_column_mdm_prefix_mdr_left_signed_minor_positive))) /\ (((exists ff_h_mdm_mdr_left_signed_minor_positive_cell_source. ff_h_mdm_mdr_left_signed_minor_positive_cell_source + S (ff_value_mdm_prefix_mdr_left_signed_minor_positive) = S ((S ((ff_row_mdm_cell_mdr_left_signed_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_left_signed_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mdr_left_signed_minor_positive_cell_source. pb = ff_q_mdm_mdr_left_signed_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_left_signed_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_left_signed_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mdr_left_signed_minor_positive)))))) /\ (((exists ff_h_mdm_mdr_left_signed_minor_positive_target. ff_h_mdm_mdr_left_signed_minor_positive_target + S (ff_value_mdm_prefix_mdr_left_signed_minor_positive) = S ((S (ff_index_mdm_prefix_mdr_left_signed_minor_positive)) * us)) /\ exists ff_q_mdm_mdr_left_signed_minor_positive_target. up = ff_q_mdm_mdr_left_signed_minor_positive_target * S ((S (ff_index_mdm_prefix_mdr_left_signed_minor_positive)) * us) + (ff_value_mdm_prefix_mdr_left_signed_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_left_signed_minor_negative. (exists ff_gap_mdm_lt_mdr_left_signed_minor_negative_index_bound. ff_gap_mdm_lt_mdr_left_signed_minor_negative_index_bound + S (ff_index_mdm_prefix_mdr_left_signed_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_left_signed_minor_negative ff_column_mdm_prefix_mdr_left_signed_minor_negative ff_value_mdm_prefix_mdr_left_signed_minor_negative. (ff_index_mdm_prefix_mdr_left_signed_minor_negative = (q) * ff_row_mdm_prefix_mdr_left_signed_minor_negative + ff_column_mdm_prefix_mdr_left_signed_minor_negative /\ ((exists ff_gap_mdm_lt_mdr_left_signed_minor_negative_column_bound. ff_gap_mdm_lt_mdr_left_signed_minor_negative_column_bound + S (ff_column_mdm_prefix_mdr_left_signed_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_left_signed_minor_negative_cell ff_column_mdm_cell_mdr_left_signed_minor_negative_cell. (((((exists ff_gap_mdm_lt_mdr_left_signed_minor_negative_cell_row_before. ff_gap_mdm_lt_mdr_left_signed_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_left_signed_minor_negative) = (0)) /\ ff_row_mdm_cell_mdr_left_signed_minor_negative_cell = ff_row_mdm_prefix_mdr_left_signed_minor_negative) \/ ((exists ff_gap_mdm_le_mdr_left_signed_minor_negative_cell_row_after. ff_gap_mdm_le_mdr_left_signed_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_left_signed_minor_negative)) /\ ff_row_mdm_cell_mdr_left_signed_minor_negative_cell = S ff_row_mdm_prefix_mdr_left_signed_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_left_signed_minor_negative_cell_column_before. ff_gap_mdm_lt_mdr_left_signed_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_left_signed_minor_negative) = (j)) /\ ff_column_mdm_cell_mdr_left_signed_minor_negative_cell = ff_column_mdm_prefix_mdr_left_signed_minor_negative) \/ ((exists ff_gap_mdm_le_mdr_left_signed_minor_negative_cell_column_after. ff_gap_mdm_le_mdr_left_signed_minor_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_left_signed_minor_negative)) /\ ff_column_mdm_cell_mdr_left_signed_minor_negative_cell = S ff_column_mdm_prefix_mdr_left_signed_minor_negative))) /\ (((exists ff_h_mdm_mdr_left_signed_minor_negative_cell_source. ff_h_mdm_mdr_left_signed_minor_negative_cell_source + S (ff_value_mdm_prefix_mdr_left_signed_minor_negative) = S ((S ((ff_row_mdm_cell_mdr_left_signed_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_left_signed_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mdr_left_signed_minor_negative_cell_source. nb = ff_q_mdm_mdr_left_signed_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_left_signed_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_left_signed_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mdr_left_signed_minor_negative)))))) /\ (((exists ff_h_mdm_mdr_left_signed_minor_negative_target. ff_h_mdm_mdr_left_signed_minor_negative_target + S (ff_value_mdm_prefix_mdr_left_signed_minor_negative) = S ((S (ff_index_mdm_prefix_mdr_left_signed_minor_negative)) * ut)) /\ exists ff_q_mdm_mdr_left_signed_minor_negative_target. un = ff_q_mdm_mdr_left_signed_minor_negative_target * S ((S (ff_index_mdm_prefix_mdr_left_signed_minor_negative)) * ut) + (ff_value_mdm_prefix_mdr_left_signed_minor_negative))))))))) -> (((forall ff_index_mdm_prefix_mdr_right_signed_minor_positive. (exists ff_gap_mdm_lt_mdr_right_signed_minor_positive_index_bound. ff_gap_mdm_lt_mdr_right_signed_minor_positive_index_bound + S (ff_index_mdm_prefix_mdr_right_signed_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_right_signed_minor_positive ff_column_mdm_prefix_mdr_right_signed_minor_positive ff_value_mdm_prefix_mdr_right_signed_minor_positive. (ff_index_mdm_prefix_mdr_right_signed_minor_positive = (q) * ff_row_mdm_prefix_mdr_right_signed_minor_positive + ff_column_mdm_prefix_mdr_right_signed_minor_positive /\ ((exists ff_gap_mdm_lt_mdr_right_signed_minor_positive_column_bound. ff_gap_mdm_lt_mdr_right_signed_minor_positive_column_bound + S (ff_column_mdm_prefix_mdr_right_signed_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_right_signed_minor_positive_cell ff_column_mdm_cell_mdr_right_signed_minor_positive_cell. (((((exists ff_gap_mdm_lt_mdr_right_signed_minor_positive_cell_row_before. ff_gap_mdm_lt_mdr_right_signed_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_right_signed_minor_positive) = (0)) /\ ff_row_mdm_cell_mdr_right_signed_minor_positive_cell = ff_row_mdm_prefix_mdr_right_signed_minor_positive) \/ ((exists ff_gap_mdm_le_mdr_right_signed_minor_positive_cell_row_after. ff_gap_mdm_le_mdr_right_signed_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_right_signed_minor_positive)) /\ ff_row_mdm_cell_mdr_right_signed_minor_positive_cell = S ff_row_mdm_prefix_mdr_right_signed_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_right_signed_minor_positive_cell_column_before. ff_gap_mdm_lt_mdr_right_signed_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_right_signed_minor_positive) = (j)) /\ ff_column_mdm_cell_mdr_right_signed_minor_positive_cell = ff_column_mdm_prefix_mdr_right_signed_minor_positive) \/ ((exists ff_gap_mdm_le_mdr_right_signed_minor_positive_cell_column_after. ff_gap_mdm_le_mdr_right_signed_minor_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_right_signed_minor_positive)) /\ ff_column_mdm_cell_mdr_right_signed_minor_positive_cell = S ff_column_mdm_prefix_mdr_right_signed_minor_positive))) /\ (((exists ff_h_mdm_mdr_right_signed_minor_positive_cell_source. ff_h_mdm_mdr_right_signed_minor_positive_cell_source + S (ff_value_mdm_prefix_mdr_right_signed_minor_positive) = S ((S ((ff_row_mdm_cell_mdr_right_signed_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_right_signed_minor_positive_cell))) * qc)) /\ exists ff_q_mdm_mdr_right_signed_minor_positive_cell_source. qb = ff_q_mdm_mdr_right_signed_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_right_signed_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_right_signed_minor_positive_cell))) * qc) + (ff_value_mdm_prefix_mdr_right_signed_minor_positive)))))) /\ (((exists ff_h_mdm_mdr_right_signed_minor_positive_target. ff_h_mdm_mdr_right_signed_minor_positive_target + S (ff_value_mdm_prefix_mdr_right_signed_minor_positive) = S ((S (ff_index_mdm_prefix_mdr_right_signed_minor_positive)) * vs)) /\ exists ff_q_mdm_mdr_right_signed_minor_positive_target. vp = ff_q_mdm_mdr_right_signed_minor_positive_target * S ((S (ff_index_mdm_prefix_mdr_right_signed_minor_positive)) * vs) + (ff_value_mdm_prefix_mdr_right_signed_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_right_signed_minor_negative. (exists ff_gap_mdm_lt_mdr_right_signed_minor_negative_index_bound. ff_gap_mdm_lt_mdr_right_signed_minor_negative_index_bound + S (ff_index_mdm_prefix_mdr_right_signed_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_right_signed_minor_negative ff_column_mdm_prefix_mdr_right_signed_minor_negative ff_value_mdm_prefix_mdr_right_signed_minor_negative. (ff_index_mdm_prefix_mdr_right_signed_minor_negative = (q) * ff_row_mdm_prefix_mdr_right_signed_minor_negative + ff_column_mdm_prefix_mdr_right_signed_minor_negative /\ ((exists ff_gap_mdm_lt_mdr_right_signed_minor_negative_column_bound. ff_gap_mdm_lt_mdr_right_signed_minor_negative_column_bound + S (ff_column_mdm_prefix_mdr_right_signed_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_right_signed_minor_negative_cell ff_column_mdm_cell_mdr_right_signed_minor_negative_cell. (((((exists ff_gap_mdm_lt_mdr_right_signed_minor_negative_cell_row_before. ff_gap_mdm_lt_mdr_right_signed_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_right_signed_minor_negative) = (0)) /\ ff_row_mdm_cell_mdr_right_signed_minor_negative_cell = ff_row_mdm_prefix_mdr_right_signed_minor_negative) \/ ((exists ff_gap_mdm_le_mdr_right_signed_minor_negative_cell_row_after. ff_gap_mdm_le_mdr_right_signed_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_right_signed_minor_negative)) /\ ff_row_mdm_cell_mdr_right_signed_minor_negative_cell = S ff_row_mdm_prefix_mdr_right_signed_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_right_signed_minor_negative_cell_column_before. ff_gap_mdm_lt_mdr_right_signed_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_right_signed_minor_negative) = (j)) /\ ff_column_mdm_cell_mdr_right_signed_minor_negative_cell = ff_column_mdm_prefix_mdr_right_signed_minor_negative) \/ ((exists ff_gap_mdm_le_mdr_right_signed_minor_negative_cell_column_after. ff_gap_mdm_le_mdr_right_signed_minor_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_right_signed_minor_negative)) /\ ff_column_mdm_cell_mdr_right_signed_minor_negative_cell = S ff_column_mdm_prefix_mdr_right_signed_minor_negative))) /\ (((exists ff_h_mdm_mdr_right_signed_minor_negative_cell_source. ff_h_mdm_mdr_right_signed_minor_negative_cell_source + S (ff_value_mdm_prefix_mdr_right_signed_minor_negative) = S ((S ((ff_row_mdm_cell_mdr_right_signed_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_right_signed_minor_negative_cell))) * rc)) /\ exists ff_q_mdm_mdr_right_signed_minor_negative_cell_source. rb = ff_q_mdm_mdr_right_signed_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_right_signed_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_right_signed_minor_negative_cell))) * rc) + (ff_value_mdm_prefix_mdr_right_signed_minor_negative)))))) /\ (((exists ff_h_mdm_mdr_right_signed_minor_negative_target. ff_h_mdm_mdr_right_signed_minor_negative_target + S (ff_value_mdm_prefix_mdr_right_signed_minor_negative) = S ((S (ff_index_mdm_prefix_mdr_right_signed_minor_negative)) * vt)) /\ exists ff_q_mdm_mdr_right_signed_minor_negative_target. vn = ff_q_mdm_mdr_right_signed_minor_negative_target * S ((S (ff_index_mdm_prefix_mdr_right_signed_minor_negative)) * vt) + (ff_value_mdm_prefix_mdr_right_signed_minor_negative))))))))) -> (((forall mdr_i_child_equalp mdr_a_child_equalp. (exists mdr_gap_child_equalpb. mdr_gap_child_equalpb + S (mdr_i_child_equalp) = ((q) * (q))) -> (((exists ff_h_mdr_child_equalpo. ff_h_mdr_child_equalpo + S (mdr_a_child_equalp) = S ((S (mdr_i_child_equalp)) * us)) /\ exists ff_q_mdr_child_equalpo. up = ff_q_mdr_child_equalpo * S ((S (mdr_i_child_equalp)) * us) + (mdr_a_child_equalp))) -> (((exists ff_h_mdr_child_equalpn. ff_h_mdr_child_equalpn + S (mdr_a_child_equalp) = S ((S (mdr_i_child_equalp)) * vs)) /\ exists ff_q_mdr_child_equalpn. vp = ff_q_mdr_child_equalpn * S ((S (mdr_i_child_equalp)) * vs) + (mdr_a_child_equalp)))) /\ (forall mdr_i_child_equaln mdr_a_child_equaln. (exists mdr_gap_child_equalnb. mdr_gap_child_equalnb + S (mdr_i_child_equaln) = ((q) * (q))) -> (((exists ff_h_mdr_child_equalno. ff_h_mdr_child_equalno + S (mdr_a_child_equaln) = S ((S (mdr_i_child_equaln)) * ut)) /\ exists ff_q_mdr_child_equalno. un = ff_q_mdr_child_equalno * S ((S (mdr_i_child_equaln)) * ut) + (mdr_a_child_equaln))) -> (((exists ff_h_mdr_child_equalnn. ff_h_mdr_child_equalnn + S (mdr_a_child_equaln) = S ((S (mdr_i_child_equaln)) * vt)) /\ exists ff_q_mdr_child_equalnn. vn = ff_q_mdr_child_equalnn * S ((S (mdr_i_child_equaln)) * vt) + (mdr_a_child_equaln))))))