MatrixMinorPrefix(b,c,w,r,d,u,v,q,l)

Hygienic expanded first-order definition

forall ff_index_mdm_prefix_research. (exists ff_gap_mdm_lt_research_index_bound. ff_gap_mdm_lt_research_index_bound + S (ff_index_mdm_prefix_research) = (l)) -> exists ff_row_mdm_prefix_research ff_column_mdm_prefix_research ff_value_mdm_prefix_research. (ff_index_mdm_prefix_research = (q) * ff_row_mdm_prefix_research + ff_column_mdm_prefix_research /\ ((exists ff_gap_mdm_lt_research_column_bound. ff_gap_mdm_lt_research_column_bound + S (ff_column_mdm_prefix_research) = (q)) /\ ((exists ff_row_mdm_cell_research_cell ff_column_mdm_cell_research_cell. (((((exists ff_gap_mdm_lt_research_cell_row_before. ff_gap_mdm_lt_research_cell_row_before + S (ff_row_mdm_prefix_research) = (r)) /\ ff_row_mdm_cell_research_cell = ff_row_mdm_prefix_research) \/ ((exists ff_gap_mdm_le_research_cell_row_after. ff_gap_mdm_le_research_cell_row_after + (r) = (ff_row_mdm_prefix_research)) /\ ff_row_mdm_cell_research_cell = S ff_row_mdm_prefix_research))) /\ (((((exists ff_gap_mdm_lt_research_cell_column_before. ff_gap_mdm_lt_research_cell_column_before + S (ff_column_mdm_prefix_research) = (d)) /\ ff_column_mdm_cell_research_cell = ff_column_mdm_prefix_research) \/ ((exists ff_gap_mdm_le_research_cell_column_after. ff_gap_mdm_le_research_cell_column_after + (d) = (ff_column_mdm_prefix_research)) /\ ff_column_mdm_cell_research_cell = S ff_column_mdm_prefix_research))) /\ (((exists ff_h_mdm_research_cell_source. ff_h_mdm_research_cell_source + S (ff_value_mdm_prefix_research) = S ((S ((ff_row_mdm_cell_research_cell) * (w) + (ff_column_mdm_cell_research_cell))) * c)) /\ exists ff_q_mdm_research_cell_source. b = ff_q_mdm_research_cell_source * S ((S ((ff_row_mdm_cell_research_cell) * (w) + (ff_column_mdm_cell_research_cell))) * c) + (ff_value_mdm_prefix_research)))))) /\ (((exists ff_h_mdm_research_target. ff_h_mdm_research_target + S (ff_value_mdm_prefix_research) = S ((S (ff_index_mdm_prefix_research)) * v)) /\ exists ff_q_mdm_research_target. u = ff_q_mdm_research_target * S ((S (ff_index_mdm_prefix_research)) * v) + (ff_value_mdm_prefix_research))))))

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