SignedMatrixMinor(pb,pc,nb,nc,w,r,d,q,up,us,un,ut)

Hygienic expanded first-order definition

((forall ff_index_mdm_prefix_research_positive. (exists ff_gap_mdm_lt_research_positive_index_bound. ff_gap_mdm_lt_research_positive_index_bound + S (ff_index_mdm_prefix_research_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_research_positive ff_column_mdm_prefix_research_positive ff_value_mdm_prefix_research_positive. (ff_index_mdm_prefix_research_positive = (q) * ff_row_mdm_prefix_research_positive + ff_column_mdm_prefix_research_positive /\ ((exists ff_gap_mdm_lt_research_positive_column_bound. ff_gap_mdm_lt_research_positive_column_bound + S (ff_column_mdm_prefix_research_positive) = (q)) /\ ((exists ff_row_mdm_cell_research_positive_cell ff_column_mdm_cell_research_positive_cell. (((((exists ff_gap_mdm_lt_research_positive_cell_row_before. ff_gap_mdm_lt_research_positive_cell_row_before + S (ff_row_mdm_prefix_research_positive) = (r)) /\ ff_row_mdm_cell_research_positive_cell = ff_row_mdm_prefix_research_positive) \/ ((exists ff_gap_mdm_le_research_positive_cell_row_after. ff_gap_mdm_le_research_positive_cell_row_after + (r) = (ff_row_mdm_prefix_research_positive)) /\ ff_row_mdm_cell_research_positive_cell = S ff_row_mdm_prefix_research_positive))) /\ (((((exists ff_gap_mdm_lt_research_positive_cell_column_before. ff_gap_mdm_lt_research_positive_cell_column_before + S (ff_column_mdm_prefix_research_positive) = (d)) /\ ff_column_mdm_cell_research_positive_cell = ff_column_mdm_prefix_research_positive) \/ ((exists ff_gap_mdm_le_research_positive_cell_column_after. ff_gap_mdm_le_research_positive_cell_column_after + (d) = (ff_column_mdm_prefix_research_positive)) /\ ff_column_mdm_cell_research_positive_cell = S ff_column_mdm_prefix_research_positive))) /\ (((exists ff_h_mdm_research_positive_cell_source. ff_h_mdm_research_positive_cell_source + S (ff_value_mdm_prefix_research_positive) = S ((S ((ff_row_mdm_cell_research_positive_cell) * (w) + (ff_column_mdm_cell_research_positive_cell))) * pc)) /\ exists ff_q_mdm_research_positive_cell_source. pb = ff_q_mdm_research_positive_cell_source * S ((S ((ff_row_mdm_cell_research_positive_cell) * (w) + (ff_column_mdm_cell_research_positive_cell))) * pc) + (ff_value_mdm_prefix_research_positive)))))) /\ (((exists ff_h_mdm_research_positive_target. ff_h_mdm_research_positive_target + S (ff_value_mdm_prefix_research_positive) = S ((S (ff_index_mdm_prefix_research_positive)) * us)) /\ exists ff_q_mdm_research_positive_target. up = ff_q_mdm_research_positive_target * S ((S (ff_index_mdm_prefix_research_positive)) * us) + (ff_value_mdm_prefix_research_positive))))))) /\ (forall ff_index_mdm_prefix_research_negative. (exists ff_gap_mdm_lt_research_negative_index_bound. ff_gap_mdm_lt_research_negative_index_bound + S (ff_index_mdm_prefix_research_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_research_negative ff_column_mdm_prefix_research_negative ff_value_mdm_prefix_research_negative. (ff_index_mdm_prefix_research_negative = (q) * ff_row_mdm_prefix_research_negative + ff_column_mdm_prefix_research_negative /\ ((exists ff_gap_mdm_lt_research_negative_column_bound. ff_gap_mdm_lt_research_negative_column_bound + S (ff_column_mdm_prefix_research_negative) = (q)) /\ ((exists ff_row_mdm_cell_research_negative_cell ff_column_mdm_cell_research_negative_cell. (((((exists ff_gap_mdm_lt_research_negative_cell_row_before. ff_gap_mdm_lt_research_negative_cell_row_before + S (ff_row_mdm_prefix_research_negative) = (r)) /\ ff_row_mdm_cell_research_negative_cell = ff_row_mdm_prefix_research_negative) \/ ((exists ff_gap_mdm_le_research_negative_cell_row_after. ff_gap_mdm_le_research_negative_cell_row_after + (r) = (ff_row_mdm_prefix_research_negative)) /\ ff_row_mdm_cell_research_negative_cell = S ff_row_mdm_prefix_research_negative))) /\ (((((exists ff_gap_mdm_lt_research_negative_cell_column_before. ff_gap_mdm_lt_research_negative_cell_column_before + S (ff_column_mdm_prefix_research_negative) = (d)) /\ ff_column_mdm_cell_research_negative_cell = ff_column_mdm_prefix_research_negative) \/ ((exists ff_gap_mdm_le_research_negative_cell_column_after. ff_gap_mdm_le_research_negative_cell_column_after + (d) = (ff_column_mdm_prefix_research_negative)) /\ ff_column_mdm_cell_research_negative_cell = S ff_column_mdm_prefix_research_negative))) /\ (((exists ff_h_mdm_research_negative_cell_source. ff_h_mdm_research_negative_cell_source + S (ff_value_mdm_prefix_research_negative) = S ((S ((ff_row_mdm_cell_research_negative_cell) * (w) + (ff_column_mdm_cell_research_negative_cell))) * nc)) /\ exists ff_q_mdm_research_negative_cell_source. nb = ff_q_mdm_research_negative_cell_source * S ((S ((ff_row_mdm_cell_research_negative_cell) * (w) + (ff_column_mdm_cell_research_negative_cell))) * nc) + (ff_value_mdm_prefix_research_negative)))))) /\ (((exists ff_h_mdm_research_negative_target. ff_h_mdm_research_negative_target + S (ff_value_mdm_prefix_research_negative) = S ((S (ff_index_mdm_prefix_research_negative)) * ut)) /\ exists ff_q_mdm_research_negative_target. un = ff_q_mdm_research_negative_target * S ((S (ff_index_mdm_prefix_research_negative)) * ut) + (ff_value_mdm_prefix_research_negative))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Definitions depending on this notation

Checked theorems using this definition