matrix_recursive_prefix_trans

Exact expanded first-order arithmetic statement

forall b c u v w z l. (forall mdr_i_source mdr_a_source. (exists mdr_gap_sourceb. mdr_gap_sourceb + S (mdr_i_source) = (l)) -> (((exists ff_h_mdr_sourceo. ff_h_mdr_sourceo + S (mdr_a_source) = S ((S (mdr_i_source)) * c)) /\ exists ff_q_mdr_sourceo. b = ff_q_mdr_sourceo * S ((S (mdr_i_source)) * c) + (mdr_a_source))) -> (((exists ff_h_mdr_sourcen. ff_h_mdr_sourcen + S (mdr_a_source) = S ((S (mdr_i_source)) * v)) /\ exists ff_q_mdr_sourcen. u = ff_q_mdr_sourcen * S ((S (mdr_i_source)) * v) + (mdr_a_source)))) -> (forall mdr_i_middle mdr_a_middle. (exists mdr_gap_middleb. mdr_gap_middleb + S (mdr_i_middle) = (l)) -> (((exists ff_h_mdr_middleo. ff_h_mdr_middleo + S (mdr_a_middle) = S ((S (mdr_i_middle)) * v)) /\ exists ff_q_mdr_middleo. u = ff_q_mdr_middleo * S ((S (mdr_i_middle)) * v) + (mdr_a_middle))) -> (((exists ff_h_mdr_middlen. ff_h_mdr_middlen + S (mdr_a_middle) = S ((S (mdr_i_middle)) * z)) /\ exists ff_q_mdr_middlen. w = ff_q_mdr_middlen * S ((S (mdr_i_middle)) * z) + (mdr_a_middle)))) -> (forall mdr_i_result mdr_a_result. (exists mdr_gap_resultb. mdr_gap_resultb + S (mdr_i_result) = (l)) -> (((exists ff_h_mdr_resulto. ff_h_mdr_resulto + S (mdr_a_result) = S ((S (mdr_i_result)) * c)) /\ exists ff_q_mdr_resulto. b = ff_q_mdr_resulto * S ((S (mdr_i_result)) * c) + (mdr_a_result))) -> (((exists ff_h_mdr_resultn. ff_h_mdr_resultn + S (mdr_a_result) = S ((S (mdr_i_result)) * z)) /\ exists ff_q_mdr_resultn. w = ff_q_mdr_resultn * S ((S (mdr_i_result)) * z) + (mdr_a_result))))