matrix_rank_selector_transport

Exact expanded first-order arithmetic statement

forall b c u v l B. (forall mdr_i_selector_transport mdr_a_selector_transport. (exists mdr_gap_selector_transportb. mdr_gap_selector_transportb + S (mdr_i_selector_transport) = (l)) -> (((exists ff_h_mdr_selector_transporto. ff_h_mdr_selector_transporto + S (mdr_a_selector_transport) = S ((S (mdr_i_selector_transport)) * c)) /\ exists ff_q_mdr_selector_transporto. b = ff_q_mdr_selector_transporto * S ((S (mdr_i_selector_transport)) * c) + (mdr_a_selector_transport))) -> (((exists ff_h_mdr_selector_transportn. ff_h_mdr_selector_transportn + S (mdr_a_selector_transport) = S ((S (mdr_i_selector_transport)) * v)) /\ exists ff_q_mdr_selector_transportn. u = ff_q_mdr_selector_transportn * S ((S (mdr_i_selector_transport)) * v) + (mdr_a_selector_transport)))) -> (((forall fom_index_mrf_selector_sourcebound. (exists fom_gap_mrf_selector_sourcebound_index_bound. fom_gap_mrf_selector_sourcebound_index_bound + S (fom_index_mrf_selector_sourcebound) = l) -> exists fom_value_mrf_selector_sourcebound. ((((exists fom_beta_height_mrf_selector_sourcebound_entry. fom_beta_height_mrf_selector_sourcebound_entry + S (fom_value_mrf_selector_sourcebound) = S ((S (fom_index_mrf_selector_sourcebound)) * c)) /\ exists fom_beta_quotient_mrf_selector_sourcebound_entry. b = fom_beta_quotient_mrf_selector_sourcebound_entry * S ((S (fom_index_mrf_selector_sourcebound)) * c) + (fom_value_mrf_selector_sourcebound))) /\ (exists fom_gap_mrf_selector_sourcebound_value_bound. fom_gap_mrf_selector_sourcebound_value_bound + S (fom_value_mrf_selector_sourcebound) = B))) /\ (forall mdr_i_selector_sourcedistinct mdr_j_selector_sourcedistinct mdr_a_selector_sourcedistinct. (exists mdr_gap_selector_sourcedistincti. mdr_gap_selector_sourcedistincti + S (mdr_i_selector_sourcedistinct) = (l)) -> (exists mdr_gap_selector_sourcedistinctj. mdr_gap_selector_sourcedistinctj + S (mdr_j_selector_sourcedistinct) = (l)) -> (((exists ff_h_mdr_selector_sourcedistinctfirst. ff_h_mdr_selector_sourcedistinctfirst + S (mdr_a_selector_sourcedistinct) = S ((S (mdr_i_selector_sourcedistinct)) * c)) /\ exists ff_q_mdr_selector_sourcedistinctfirst. b = ff_q_mdr_selector_sourcedistinctfirst * S ((S (mdr_i_selector_sourcedistinct)) * c) + (mdr_a_selector_sourcedistinct))) -> (((exists ff_h_mdr_selector_sourcedistinctsecond. ff_h_mdr_selector_sourcedistinctsecond + S (mdr_a_selector_sourcedistinct) = S ((S (mdr_j_selector_sourcedistinct)) * c)) /\ exists ff_q_mdr_selector_sourcedistinctsecond. b = ff_q_mdr_selector_sourcedistinctsecond * S ((S (mdr_j_selector_sourcedistinct)) * c) + (mdr_a_selector_sourcedistinct))) -> mdr_i_selector_sourcedistinct = mdr_j_selector_sourcedistinct))) -> (((forall fom_index_mrf_selector_targetbound. (exists fom_gap_mrf_selector_targetbound_index_bound. fom_gap_mrf_selector_targetbound_index_bound + S (fom_index_mrf_selector_targetbound) = l) -> exists fom_value_mrf_selector_targetbound. ((((exists fom_beta_height_mrf_selector_targetbound_entry. fom_beta_height_mrf_selector_targetbound_entry + S (fom_value_mrf_selector_targetbound) = S ((S (fom_index_mrf_selector_targetbound)) * v)) /\ exists fom_beta_quotient_mrf_selector_targetbound_entry. u = fom_beta_quotient_mrf_selector_targetbound_entry * S ((S (fom_index_mrf_selector_targetbound)) * v) + (fom_value_mrf_selector_targetbound))) /\ (exists fom_gap_mrf_selector_targetbound_value_bound. fom_gap_mrf_selector_targetbound_value_bound + S (fom_value_mrf_selector_targetbound) = B))) /\ (forall mdr_i_selector_targetdistinct mdr_j_selector_targetdistinct mdr_a_selector_targetdistinct. (exists mdr_gap_selector_targetdistincti. mdr_gap_selector_targetdistincti + S (mdr_i_selector_targetdistinct) = (l)) -> (exists mdr_gap_selector_targetdistinctj. mdr_gap_selector_targetdistinctj + S (mdr_j_selector_targetdistinct) = (l)) -> (((exists ff_h_mdr_selector_targetdistinctfirst. ff_h_mdr_selector_targetdistinctfirst + S (mdr_a_selector_targetdistinct) = S ((S (mdr_i_selector_targetdistinct)) * v)) /\ exists ff_q_mdr_selector_targetdistinctfirst. u = ff_q_mdr_selector_targetdistinctfirst * S ((S (mdr_i_selector_targetdistinct)) * v) + (mdr_a_selector_targetdistinct))) -> (((exists ff_h_mdr_selector_targetdistinctsecond. ff_h_mdr_selector_targetdistinctsecond + S (mdr_a_selector_targetdistinct) = S ((S (mdr_j_selector_targetdistinct)) * v)) /\ exists ff_q_mdr_selector_targetdistinctsecond. u = ff_q_mdr_selector_targetdistinctsecond * S ((S (mdr_j_selector_targetdistinct)) * v) + (mdr_a_selector_targetdistinct))) -> mdr_i_selector_targetdistinct = mdr_j_selector_targetdistinct)))