prime_field_polynomial_aligned_add_transport

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M rb rc N db dc J eb ec H fb fc I. (forall fom_index_pfp_aligned_transport_0. (exists fom_gap_pfp_aligned_transport_0_index_bound. fom_gap_pfp_aligned_transport_0_index_bound + S (fom_index_pfp_aligned_transport_0) = J) -> exists fom_value_pfp_aligned_transport_0. ((((exists fom_beta_height_pfp_aligned_transport_0_entry. fom_beta_height_pfp_aligned_transport_0_entry + S (fom_value_pfp_aligned_transport_0) = S ((S (fom_index_pfp_aligned_transport_0)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_transport_0_entry. db = fom_beta_quotient_pfp_aligned_transport_0_entry * S ((S (fom_index_pfp_aligned_transport_0)) * dc) + (fom_value_pfp_aligned_transport_0))) /\ (exists fom_gap_pfp_aligned_transport_0_value_bound. fom_gap_pfp_aligned_transport_0_value_bound + S (fom_value_pfp_aligned_transport_0) = p))) -> (forall fom_index_pfp_aligned_transport_1. (exists fom_gap_pfp_aligned_transport_1_index_bound. fom_gap_pfp_aligned_transport_1_index_bound + S (fom_index_pfp_aligned_transport_1) = H) -> exists fom_value_pfp_aligned_transport_1. ((((exists fom_beta_height_pfp_aligned_transport_1_entry. fom_beta_height_pfp_aligned_transport_1_entry + S (fom_value_pfp_aligned_transport_1) = S ((S (fom_index_pfp_aligned_transport_1)) * ec)) /\ exists fom_beta_quotient_pfp_aligned_transport_1_entry. eb = fom_beta_quotient_pfp_aligned_transport_1_entry * S ((S (fom_index_pfp_aligned_transport_1)) * ec) + (fom_value_pfp_aligned_transport_1))) /\ (exists fom_gap_pfp_aligned_transport_1_value_bound. fom_gap_pfp_aligned_transport_1_value_bound + S (fom_value_pfp_aligned_transport_1) = p))) -> (forall fom_index_pfp_aligned_transport_2. (exists fom_gap_pfp_aligned_transport_2_index_bound. fom_gap_pfp_aligned_transport_2_index_bound + S (fom_index_pfp_aligned_transport_2) = I) -> exists fom_value_pfp_aligned_transport_2. ((((exists fom_beta_height_pfp_aligned_transport_2_entry. fom_beta_height_pfp_aligned_transport_2_entry + S (fom_value_pfp_aligned_transport_2) = S ((S (fom_index_pfp_aligned_transport_2)) * fc)) /\ exists fom_beta_quotient_pfp_aligned_transport_2_entry. fb = fom_beta_quotient_pfp_aligned_transport_2_entry * S ((S (fom_index_pfp_aligned_transport_2)) * fc) + (fom_value_pfp_aligned_transport_2))) /\ (exists fom_gap_pfp_aligned_transport_2_value_bound. fom_gap_pfp_aligned_transport_2_value_bound + S (fom_value_pfp_aligned_transport_2) = p))) -> (forall pfrep_power_aligned_transport_left pfrep_left_aligned_transport_left pfrep_right_aligned_transport_left. ((exists pfrep_position_aligned_transport_leftfirst. ((pfrep_position_aligned_transport_leftfirst+S (pfrep_power_aligned_transport_left)=(J)) /\ ((((exists ff_h_pfp_aligned_transport_leftfirstentry. ff_h_pfp_aligned_transport_leftfirstentry + S (pfrep_left_aligned_transport_left) = S ((S (pfrep_position_aligned_transport_leftfirst)) * dc)) /\ exists ff_q_pfp_aligned_transport_leftfirstentry. db = ff_q_pfp_aligned_transport_leftfirstentry * S ((S (pfrep_position_aligned_transport_leftfirst)) * dc) + (pfrep_left_aligned_transport_left)))))) \/ (((exists pfrep_gap_aligned_transport_leftfirstoutside. pfrep_gap_aligned_transport_leftfirstoutside+(J)=(pfrep_power_aligned_transport_left)) /\ (((pfrep_left_aligned_transport_left)=0))))) -> ((exists pfrep_position_aligned_transport_leftsecond. ((pfrep_position_aligned_transport_leftsecond+S (pfrep_power_aligned_transport_left)=(L)) /\ ((((exists ff_h_pfp_aligned_transport_leftsecondentry. ff_h_pfp_aligned_transport_leftsecondentry + S (pfrep_right_aligned_transport_left) = S ((S (pfrep_position_aligned_transport_leftsecond)) * ac)) /\ exists ff_q_pfp_aligned_transport_leftsecondentry. ab = ff_q_pfp_aligned_transport_leftsecondentry * S ((S (pfrep_position_aligned_transport_leftsecond)) * ac) + (pfrep_right_aligned_transport_left)))))) \/ (((exists pfrep_gap_aligned_transport_leftsecondoutside. pfrep_gap_aligned_transport_leftsecondoutside+(L)=(pfrep_power_aligned_transport_left)) /\ (((pfrep_right_aligned_transport_left)=0))))) -> pfrep_left_aligned_transport_left=pfrep_right_aligned_transport_left) -> (forall pfrep_power_aligned_transport_right pfrep_left_aligned_transport_right pfrep_right_aligned_transport_right. ((exists pfrep_position_aligned_transport_rightfirst. ((pfrep_position_aligned_transport_rightfirst+S (pfrep_power_aligned_transport_right)=(H)) /\ ((((exists ff_h_pfp_aligned_transport_rightfirstentry. ff_h_pfp_aligned_transport_rightfirstentry + S (pfrep_left_aligned_transport_right) = S ((S (pfrep_position_aligned_transport_rightfirst)) * ec)) /\ exists ff_q_pfp_aligned_transport_rightfirstentry. eb = ff_q_pfp_aligned_transport_rightfirstentry * S ((S (pfrep_position_aligned_transport_rightfirst)) * ec) + (pfrep_left_aligned_transport_right)))))) \/ (((exists pfrep_gap_aligned_transport_rightfirstoutside. pfrep_gap_aligned_transport_rightfirstoutside+(H)=(pfrep_power_aligned_transport_right)) /\ (((pfrep_left_aligned_transport_right)=0))))) -> ((exists pfrep_position_aligned_transport_rightsecond. ((pfrep_position_aligned_transport_rightsecond+S (pfrep_power_aligned_transport_right)=(M)) /\ ((((exists ff_h_pfp_aligned_transport_rightsecondentry. ff_h_pfp_aligned_transport_rightsecondentry + S (pfrep_right_aligned_transport_right) = S ((S (pfrep_position_aligned_transport_rightsecond)) * bc)) /\ exists ff_q_pfp_aligned_transport_rightsecondentry. bb = ff_q_pfp_aligned_transport_rightsecondentry * S ((S (pfrep_position_aligned_transport_rightsecond)) * bc) + (pfrep_right_aligned_transport_right)))))) \/ (((exists pfrep_gap_aligned_transport_rightsecondoutside. pfrep_gap_aligned_transport_rightsecondoutside+(M)=(pfrep_power_aligned_transport_right)) /\ (((pfrep_right_aligned_transport_right)=0))))) -> pfrep_left_aligned_transport_right=pfrep_right_aligned_transport_right) -> (forall pfrep_power_aligned_transport_output pfrep_left_aligned_transport_output pfrep_right_aligned_transport_output. ((exists pfrep_position_aligned_transport_outputfirst. ((pfrep_position_aligned_transport_outputfirst+S (pfrep_power_aligned_transport_output)=(N)) /\ ((((exists ff_h_pfp_aligned_transport_outputfirstentry. ff_h_pfp_aligned_transport_outputfirstentry + S (pfrep_left_aligned_transport_output) = S ((S (pfrep_position_aligned_transport_outputfirst)) * rc)) /\ exists ff_q_pfp_aligned_transport_outputfirstentry. rb = ff_q_pfp_aligned_transport_outputfirstentry * S ((S (pfrep_position_aligned_transport_outputfirst)) * rc) + (pfrep_left_aligned_transport_output)))))) \/ (((exists pfrep_gap_aligned_transport_outputfirstoutside. pfrep_gap_aligned_transport_outputfirstoutside+(N)=(pfrep_power_aligned_transport_output)) /\ (((pfrep_left_aligned_transport_output)=0))))) -> ((exists pfrep_position_aligned_transport_outputsecond. ((pfrep_position_aligned_transport_outputsecond+S (pfrep_power_aligned_transport_output)=(I)) /\ ((((exists ff_h_pfp_aligned_transport_outputsecondentry. ff_h_pfp_aligned_transport_outputsecondentry + S (pfrep_right_aligned_transport_output) = S ((S (pfrep_position_aligned_transport_outputsecond)) * fc)) /\ exists ff_q_pfp_aligned_transport_outputsecondentry. fb = ff_q_pfp_aligned_transport_outputsecondentry * S ((S (pfrep_position_aligned_transport_outputsecond)) * fc) + (pfrep_right_aligned_transport_output)))))) \/ (((exists pfrep_gap_aligned_transport_outputsecondoutside. pfrep_gap_aligned_transport_outputsecondoutside+(I)=(pfrep_power_aligned_transport_output)) /\ (((pfrep_right_aligned_transport_output)=0))))) -> pfrep_left_aligned_transport_output=pfrep_right_aligned_transport_output) -> (((forall fom_index_pfp_aligned_transport_old_left_bounded. (exists fom_gap_pfp_aligned_transport_old_left_bounded_index_bound. fom_gap_pfp_aligned_transport_old_left_bounded_index_bound + S (fom_index_pfp_aligned_transport_old_left_bounded) = L) -> exists fom_value_pfp_aligned_transport_old_left_bounded. ((((exists fom_beta_height_pfp_aligned_transport_old_left_bounded_entry. fom_beta_height_pfp_aligned_transport_old_left_bounded_entry + S (fom_value_pfp_aligned_transport_old_left_bounded) = S ((S (fom_index_pfp_aligned_transport_old_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_transport_old_left_bounded_entry. ab = fom_beta_quotient_pfp_aligned_transport_old_left_bounded_entry * S ((S (fom_index_pfp_aligned_transport_old_left_bounded)) * ac) + (fom_value_pfp_aligned_transport_old_left_bounded))) /\ (exists fom_gap_pfp_aligned_transport_old_left_bounded_value_bound. fom_gap_pfp_aligned_transport_old_left_bounded_value_bound + S (fom_value_pfp_aligned_transport_old_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_transport_old_right_bounded. (exists fom_gap_pfp_aligned_transport_old_right_bounded_index_bound. fom_gap_pfp_aligned_transport_old_right_bounded_index_bound + S (fom_index_pfp_aligned_transport_old_right_bounded) = M) -> exists fom_value_pfp_aligned_transport_old_right_bounded. ((((exists fom_beta_height_pfp_aligned_transport_old_right_bounded_entry. fom_beta_height_pfp_aligned_transport_old_right_bounded_entry + S (fom_value_pfp_aligned_transport_old_right_bounded) = S ((S (fom_index_pfp_aligned_transport_old_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_transport_old_right_bounded_entry. bb = fom_beta_quotient_pfp_aligned_transport_old_right_bounded_entry * S ((S (fom_index_pfp_aligned_transport_old_right_bounded)) * bc) + (fom_value_pfp_aligned_transport_old_right_bounded))) /\ (exists fom_gap_pfp_aligned_transport_old_right_bounded_value_bound. fom_gap_pfp_aligned_transport_old_right_bounded_value_bound + S (fom_value_pfp_aligned_transport_old_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_transport_old_result_bounded. (exists fom_gap_pfp_aligned_transport_old_result_bounded_index_bound. fom_gap_pfp_aligned_transport_old_result_bounded_index_bound + S (fom_index_pfp_aligned_transport_old_result_bounded) = N) -> exists fom_value_pfp_aligned_transport_old_result_bounded. ((((exists fom_beta_height_pfp_aligned_transport_old_result_bounded_entry. fom_beta_height_pfp_aligned_transport_old_result_bounded_entry + S (fom_value_pfp_aligned_transport_old_result_bounded) = S ((S (fom_index_pfp_aligned_transport_old_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_transport_old_result_bounded_entry. rb = fom_beta_quotient_pfp_aligned_transport_old_result_bounded_entry * S ((S (fom_index_pfp_aligned_transport_old_result_bounded)) * rc) + (fom_value_pfp_aligned_transport_old_result_bounded))) /\ (exists fom_gap_pfp_aligned_transport_old_result_bounded_value_bound. fom_gap_pfp_aligned_transport_old_result_bounded_value_bound + S (fom_value_pfp_aligned_transport_old_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_transport_old pfaa_left_c_aligned_transport_old pfaa_right_b_aligned_transport_old pfaa_right_c_aligned_transport_old pfaa_sum_b_aligned_transport_old pfaa_sum_c_aligned_transport_old pfaa_length_aligned_transport_old. ((((forall pfrep_power_aligned_transport_old_witness_common_left pfrep_left_aligned_transport_old_witness_common_left pfrep_right_aligned_transport_old_witness_common_left. ((exists pfrep_position_aligned_transport_old_witness_common_leftfirst. ((pfrep_position_aligned_transport_old_witness_common_leftfirst+S (pfrep_power_aligned_transport_old_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_transport_old_witness_common_leftfirstentry. ff_h_pfp_aligned_transport_old_witness_common_leftfirstentry + S (pfrep_left_aligned_transport_old_witness_common_left) = S ((S (pfrep_position_aligned_transport_old_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_aligned_transport_old_witness_common_leftfirstentry. ab = ff_q_pfp_aligned_transport_old_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_transport_old_witness_common_leftfirst)) * ac) + (pfrep_left_aligned_transport_old_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_transport_old_witness_common_leftfirstoutside. pfrep_gap_aligned_transport_old_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_transport_old_witness_common_left)) /\ (((pfrep_left_aligned_transport_old_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_transport_old_witness_common_leftsecond. ((pfrep_position_aligned_transport_old_witness_common_leftsecond+S (pfrep_power_aligned_transport_old_witness_common_left)=(pfaa_length_aligned_transport_old)) /\ ((((exists ff_h_pfp_aligned_transport_old_witness_common_leftsecondentry. ff_h_pfp_aligned_transport_old_witness_common_leftsecondentry + S (pfrep_right_aligned_transport_old_witness_common_left) = S ((S (pfrep_position_aligned_transport_old_witness_common_leftsecond)) * pfaa_left_c_aligned_transport_old)) /\ exists ff_q_pfp_aligned_transport_old_witness_common_leftsecondentry. pfaa_left_b_aligned_transport_old = ff_q_pfp_aligned_transport_old_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_transport_old_witness_common_leftsecond)) * pfaa_left_c_aligned_transport_old) + (pfrep_right_aligned_transport_old_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_transport_old_witness_common_leftsecondoutside. pfrep_gap_aligned_transport_old_witness_common_leftsecondoutside+(pfaa_length_aligned_transport_old)=(pfrep_power_aligned_transport_old_witness_common_left)) /\ (((pfrep_right_aligned_transport_old_witness_common_left)=0))))) -> pfrep_left_aligned_transport_old_witness_common_left=pfrep_right_aligned_transport_old_witness_common_left) /\ ((forall pfrep_power_aligned_transport_old_witness_common_right pfrep_left_aligned_transport_old_witness_common_right pfrep_right_aligned_transport_old_witness_common_right. ((exists pfrep_position_aligned_transport_old_witness_common_rightfirst. ((pfrep_position_aligned_transport_old_witness_common_rightfirst+S (pfrep_power_aligned_transport_old_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_transport_old_witness_common_rightfirstentry. ff_h_pfp_aligned_transport_old_witness_common_rightfirstentry + S (pfrep_left_aligned_transport_old_witness_common_right) = S ((S (pfrep_position_aligned_transport_old_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_aligned_transport_old_witness_common_rightfirstentry. bb = ff_q_pfp_aligned_transport_old_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_transport_old_witness_common_rightfirst)) * bc) + (pfrep_left_aligned_transport_old_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_transport_old_witness_common_rightfirstoutside. pfrep_gap_aligned_transport_old_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_transport_old_witness_common_right)) /\ (((pfrep_left_aligned_transport_old_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_transport_old_witness_common_rightsecond. ((pfrep_position_aligned_transport_old_witness_common_rightsecond+S (pfrep_power_aligned_transport_old_witness_common_right)=(pfaa_length_aligned_transport_old)) /\ ((((exists ff_h_pfp_aligned_transport_old_witness_common_rightsecondentry. ff_h_pfp_aligned_transport_old_witness_common_rightsecondentry + S (pfrep_right_aligned_transport_old_witness_common_right) = S ((S (pfrep_position_aligned_transport_old_witness_common_rightsecond)) * pfaa_right_c_aligned_transport_old)) /\ exists ff_q_pfp_aligned_transport_old_witness_common_rightsecondentry. pfaa_right_b_aligned_transport_old = ff_q_pfp_aligned_transport_old_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_transport_old_witness_common_rightsecond)) * pfaa_right_c_aligned_transport_old) + (pfrep_right_aligned_transport_old_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_transport_old_witness_common_rightsecondoutside. pfrep_gap_aligned_transport_old_witness_common_rightsecondoutside+(pfaa_length_aligned_transport_old)=(pfrep_power_aligned_transport_old_witness_common_right)) /\ (((pfrep_right_aligned_transport_old_witness_common_right)=0))))) -> pfrep_left_aligned_transport_old_witness_common_right=pfrep_right_aligned_transport_old_witness_common_right)))) /\ (((forall pfp_index_aligned_transport_old_witness_operation. (exists pfa_gap_aligned_transport_old_witness_operationindex. pfa_gap_aligned_transport_old_witness_operationindex + S (pfp_index_aligned_transport_old_witness_operation) = (pfaa_length_aligned_transport_old)) -> exists pfp_left_aligned_transport_old_witness_operation pfp_right_aligned_transport_old_witness_operation pfp_value_aligned_transport_old_witness_operation. ((((exists ff_h_pfp_aligned_transport_old_witness_operationleft. ff_h_pfp_aligned_transport_old_witness_operationleft + S (pfp_left_aligned_transport_old_witness_operation) = S ((S (pfp_index_aligned_transport_old_witness_operation)) * pfaa_left_c_aligned_transport_old)) /\ exists ff_q_pfp_aligned_transport_old_witness_operationleft. pfaa_left_b_aligned_transport_old = ff_q_pfp_aligned_transport_old_witness_operationleft * S ((S (pfp_index_aligned_transport_old_witness_operation)) * pfaa_left_c_aligned_transport_old) + (pfp_left_aligned_transport_old_witness_operation))) /\ (((((exists ff_h_pfp_aligned_transport_old_witness_operationright. ff_h_pfp_aligned_transport_old_witness_operationright + S (pfp_right_aligned_transport_old_witness_operation) = S ((S (pfp_index_aligned_transport_old_witness_operation)) * pfaa_right_c_aligned_transport_old)) /\ exists ff_q_pfp_aligned_transport_old_witness_operationright. pfaa_right_b_aligned_transport_old = ff_q_pfp_aligned_transport_old_witness_operationright * S ((S (pfp_index_aligned_transport_old_witness_operation)) * pfaa_right_c_aligned_transport_old) + (pfp_right_aligned_transport_old_witness_operation))) /\ (((((exists ff_h_pfp_aligned_transport_old_witness_operationtarget. ff_h_pfp_aligned_transport_old_witness_operationtarget + S (pfp_value_aligned_transport_old_witness_operation) = S ((S (pfp_index_aligned_transport_old_witness_operation)) * pfaa_sum_c_aligned_transport_old)) /\ exists ff_q_pfp_aligned_transport_old_witness_operationtarget. pfaa_sum_b_aligned_transport_old = ff_q_pfp_aligned_transport_old_witness_operationtarget * S ((S (pfp_index_aligned_transport_old_witness_operation)) * pfaa_sum_c_aligned_transport_old) + (pfp_value_aligned_transport_old_witness_operation))) /\ ((((exists pfa_gap_aligned_transport_old_witness_operationoperationleft. pfa_gap_aligned_transport_old_witness_operationoperationleft + S (pfp_left_aligned_transport_old_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_transport_old_witness_operationoperationright. pfa_gap_aligned_transport_old_witness_operationoperationright + S (pfp_right_aligned_transport_old_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_transport_old_witness_operationoperationresultbound. pfa_gap_aligned_transport_old_witness_operationoperationresultbound + S (pfp_value_aligned_transport_old_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_transport_old_witness_operationoperationresultcongruence pfa_offset_right_aligned_transport_old_witness_operationoperationresultcongruence. ((pfp_left_aligned_transport_old_witness_operation) + (pfp_right_aligned_transport_old_witness_operation)) + (p) * pfa_offset_left_aligned_transport_old_witness_operationoperationresultcongruence = (pfp_value_aligned_transport_old_witness_operation) + (p) * pfa_offset_right_aligned_transport_old_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_transport_old_witness_output pfrep_left_aligned_transport_old_witness_output pfrep_right_aligned_transport_old_witness_output. ((exists pfrep_position_aligned_transport_old_witness_outputfirst. ((pfrep_position_aligned_transport_old_witness_outputfirst+S (pfrep_power_aligned_transport_old_witness_output)=(pfaa_length_aligned_transport_old)) /\ ((((exists ff_h_pfp_aligned_transport_old_witness_outputfirstentry. ff_h_pfp_aligned_transport_old_witness_outputfirstentry + S (pfrep_left_aligned_transport_old_witness_output) = S ((S (pfrep_position_aligned_transport_old_witness_outputfirst)) * pfaa_sum_c_aligned_transport_old)) /\ exists ff_q_pfp_aligned_transport_old_witness_outputfirstentry. pfaa_sum_b_aligned_transport_old = ff_q_pfp_aligned_transport_old_witness_outputfirstentry * S ((S (pfrep_position_aligned_transport_old_witness_outputfirst)) * pfaa_sum_c_aligned_transport_old) + (pfrep_left_aligned_transport_old_witness_output)))))) \/ (((exists pfrep_gap_aligned_transport_old_witness_outputfirstoutside. pfrep_gap_aligned_transport_old_witness_outputfirstoutside+(pfaa_length_aligned_transport_old)=(pfrep_power_aligned_transport_old_witness_output)) /\ (((pfrep_left_aligned_transport_old_witness_output)=0))))) -> ((exists pfrep_position_aligned_transport_old_witness_outputsecond. ((pfrep_position_aligned_transport_old_witness_outputsecond+S (pfrep_power_aligned_transport_old_witness_output)=(N)) /\ ((((exists ff_h_pfp_aligned_transport_old_witness_outputsecondentry. ff_h_pfp_aligned_transport_old_witness_outputsecondentry + S (pfrep_right_aligned_transport_old_witness_output) = S ((S (pfrep_position_aligned_transport_old_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_aligned_transport_old_witness_outputsecondentry. rb = ff_q_pfp_aligned_transport_old_witness_outputsecondentry * S ((S (pfrep_position_aligned_transport_old_witness_outputsecond)) * rc) + (pfrep_right_aligned_transport_old_witness_output)))))) \/ (((exists pfrep_gap_aligned_transport_old_witness_outputsecondoutside. pfrep_gap_aligned_transport_old_witness_outputsecondoutside+(N)=(pfrep_power_aligned_transport_old_witness_output)) /\ (((pfrep_right_aligned_transport_old_witness_output)=0))))) -> pfrep_left_aligned_transport_old_witness_output=pfrep_right_aligned_transport_old_witness_output))))))))))))) -> (((forall fom_index_pfp_aligned_transport_new_left_bounded. (exists fom_gap_pfp_aligned_transport_new_left_bounded_index_bound. fom_gap_pfp_aligned_transport_new_left_bounded_index_bound + S (fom_index_pfp_aligned_transport_new_left_bounded) = J) -> exists fom_value_pfp_aligned_transport_new_left_bounded. ((((exists fom_beta_height_pfp_aligned_transport_new_left_bounded_entry. fom_beta_height_pfp_aligned_transport_new_left_bounded_entry + S (fom_value_pfp_aligned_transport_new_left_bounded) = S ((S (fom_index_pfp_aligned_transport_new_left_bounded)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_transport_new_left_bounded_entry. db = fom_beta_quotient_pfp_aligned_transport_new_left_bounded_entry * S ((S (fom_index_pfp_aligned_transport_new_left_bounded)) * dc) + (fom_value_pfp_aligned_transport_new_left_bounded))) /\ (exists fom_gap_pfp_aligned_transport_new_left_bounded_value_bound. fom_gap_pfp_aligned_transport_new_left_bounded_value_bound + S (fom_value_pfp_aligned_transport_new_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_transport_new_right_bounded. (exists fom_gap_pfp_aligned_transport_new_right_bounded_index_bound. fom_gap_pfp_aligned_transport_new_right_bounded_index_bound + S (fom_index_pfp_aligned_transport_new_right_bounded) = H) -> exists fom_value_pfp_aligned_transport_new_right_bounded. ((((exists fom_beta_height_pfp_aligned_transport_new_right_bounded_entry. fom_beta_height_pfp_aligned_transport_new_right_bounded_entry + S (fom_value_pfp_aligned_transport_new_right_bounded) = S ((S (fom_index_pfp_aligned_transport_new_right_bounded)) * ec)) /\ exists fom_beta_quotient_pfp_aligned_transport_new_right_bounded_entry. eb = fom_beta_quotient_pfp_aligned_transport_new_right_bounded_entry * S ((S (fom_index_pfp_aligned_transport_new_right_bounded)) * ec) + (fom_value_pfp_aligned_transport_new_right_bounded))) /\ (exists fom_gap_pfp_aligned_transport_new_right_bounded_value_bound. fom_gap_pfp_aligned_transport_new_right_bounded_value_bound + S (fom_value_pfp_aligned_transport_new_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_transport_new_result_bounded. (exists fom_gap_pfp_aligned_transport_new_result_bounded_index_bound. fom_gap_pfp_aligned_transport_new_result_bounded_index_bound + S (fom_index_pfp_aligned_transport_new_result_bounded) = I) -> exists fom_value_pfp_aligned_transport_new_result_bounded. ((((exists fom_beta_height_pfp_aligned_transport_new_result_bounded_entry. fom_beta_height_pfp_aligned_transport_new_result_bounded_entry + S (fom_value_pfp_aligned_transport_new_result_bounded) = S ((S (fom_index_pfp_aligned_transport_new_result_bounded)) * fc)) /\ exists fom_beta_quotient_pfp_aligned_transport_new_result_bounded_entry. fb = fom_beta_quotient_pfp_aligned_transport_new_result_bounded_entry * S ((S (fom_index_pfp_aligned_transport_new_result_bounded)) * fc) + (fom_value_pfp_aligned_transport_new_result_bounded))) /\ (exists fom_gap_pfp_aligned_transport_new_result_bounded_value_bound. fom_gap_pfp_aligned_transport_new_result_bounded_value_bound + S (fom_value_pfp_aligned_transport_new_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_transport_new pfaa_left_c_aligned_transport_new pfaa_right_b_aligned_transport_new pfaa_right_c_aligned_transport_new pfaa_sum_b_aligned_transport_new pfaa_sum_c_aligned_transport_new pfaa_length_aligned_transport_new. ((((forall pfrep_power_aligned_transport_new_witness_common_left pfrep_left_aligned_transport_new_witness_common_left pfrep_right_aligned_transport_new_witness_common_left. ((exists pfrep_position_aligned_transport_new_witness_common_leftfirst. ((pfrep_position_aligned_transport_new_witness_common_leftfirst+S (pfrep_power_aligned_transport_new_witness_common_left)=(J)) /\ ((((exists ff_h_pfp_aligned_transport_new_witness_common_leftfirstentry. ff_h_pfp_aligned_transport_new_witness_common_leftfirstentry + S (pfrep_left_aligned_transport_new_witness_common_left) = S ((S (pfrep_position_aligned_transport_new_witness_common_leftfirst)) * dc)) /\ exists ff_q_pfp_aligned_transport_new_witness_common_leftfirstentry. db = ff_q_pfp_aligned_transport_new_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_transport_new_witness_common_leftfirst)) * dc) + (pfrep_left_aligned_transport_new_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_transport_new_witness_common_leftfirstoutside. pfrep_gap_aligned_transport_new_witness_common_leftfirstoutside+(J)=(pfrep_power_aligned_transport_new_witness_common_left)) /\ (((pfrep_left_aligned_transport_new_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_transport_new_witness_common_leftsecond. ((pfrep_position_aligned_transport_new_witness_common_leftsecond+S (pfrep_power_aligned_transport_new_witness_common_left)=(pfaa_length_aligned_transport_new)) /\ ((((exists ff_h_pfp_aligned_transport_new_witness_common_leftsecondentry. ff_h_pfp_aligned_transport_new_witness_common_leftsecondentry + S (pfrep_right_aligned_transport_new_witness_common_left) = S ((S (pfrep_position_aligned_transport_new_witness_common_leftsecond)) * pfaa_left_c_aligned_transport_new)) /\ exists ff_q_pfp_aligned_transport_new_witness_common_leftsecondentry. pfaa_left_b_aligned_transport_new = ff_q_pfp_aligned_transport_new_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_transport_new_witness_common_leftsecond)) * pfaa_left_c_aligned_transport_new) + (pfrep_right_aligned_transport_new_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_transport_new_witness_common_leftsecondoutside. pfrep_gap_aligned_transport_new_witness_common_leftsecondoutside+(pfaa_length_aligned_transport_new)=(pfrep_power_aligned_transport_new_witness_common_left)) /\ (((pfrep_right_aligned_transport_new_witness_common_left)=0))))) -> pfrep_left_aligned_transport_new_witness_common_left=pfrep_right_aligned_transport_new_witness_common_left) /\ ((forall pfrep_power_aligned_transport_new_witness_common_right pfrep_left_aligned_transport_new_witness_common_right pfrep_right_aligned_transport_new_witness_common_right. ((exists pfrep_position_aligned_transport_new_witness_common_rightfirst. ((pfrep_position_aligned_transport_new_witness_common_rightfirst+S (pfrep_power_aligned_transport_new_witness_common_right)=(H)) /\ ((((exists ff_h_pfp_aligned_transport_new_witness_common_rightfirstentry. ff_h_pfp_aligned_transport_new_witness_common_rightfirstentry + S (pfrep_left_aligned_transport_new_witness_common_right) = S ((S (pfrep_position_aligned_transport_new_witness_common_rightfirst)) * ec)) /\ exists ff_q_pfp_aligned_transport_new_witness_common_rightfirstentry. eb = ff_q_pfp_aligned_transport_new_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_transport_new_witness_common_rightfirst)) * ec) + (pfrep_left_aligned_transport_new_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_transport_new_witness_common_rightfirstoutside. pfrep_gap_aligned_transport_new_witness_common_rightfirstoutside+(H)=(pfrep_power_aligned_transport_new_witness_common_right)) /\ (((pfrep_left_aligned_transport_new_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_transport_new_witness_common_rightsecond. ((pfrep_position_aligned_transport_new_witness_common_rightsecond+S (pfrep_power_aligned_transport_new_witness_common_right)=(pfaa_length_aligned_transport_new)) /\ ((((exists ff_h_pfp_aligned_transport_new_witness_common_rightsecondentry. ff_h_pfp_aligned_transport_new_witness_common_rightsecondentry + S (pfrep_right_aligned_transport_new_witness_common_right) = S ((S (pfrep_position_aligned_transport_new_witness_common_rightsecond)) * pfaa_right_c_aligned_transport_new)) /\ exists ff_q_pfp_aligned_transport_new_witness_common_rightsecondentry. pfaa_right_b_aligned_transport_new = ff_q_pfp_aligned_transport_new_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_transport_new_witness_common_rightsecond)) * pfaa_right_c_aligned_transport_new) + (pfrep_right_aligned_transport_new_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_transport_new_witness_common_rightsecondoutside. pfrep_gap_aligned_transport_new_witness_common_rightsecondoutside+(pfaa_length_aligned_transport_new)=(pfrep_power_aligned_transport_new_witness_common_right)) /\ (((pfrep_right_aligned_transport_new_witness_common_right)=0))))) -> pfrep_left_aligned_transport_new_witness_common_right=pfrep_right_aligned_transport_new_witness_common_right)))) /\ (((forall pfp_index_aligned_transport_new_witness_operation. (exists pfa_gap_aligned_transport_new_witness_operationindex. pfa_gap_aligned_transport_new_witness_operationindex + S (pfp_index_aligned_transport_new_witness_operation) = (pfaa_length_aligned_transport_new)) -> exists pfp_left_aligned_transport_new_witness_operation pfp_right_aligned_transport_new_witness_operation pfp_value_aligned_transport_new_witness_operation. ((((exists ff_h_pfp_aligned_transport_new_witness_operationleft. ff_h_pfp_aligned_transport_new_witness_operationleft + S (pfp_left_aligned_transport_new_witness_operation) = S ((S (pfp_index_aligned_transport_new_witness_operation)) * pfaa_left_c_aligned_transport_new)) /\ exists ff_q_pfp_aligned_transport_new_witness_operationleft. pfaa_left_b_aligned_transport_new = ff_q_pfp_aligned_transport_new_witness_operationleft * S ((S (pfp_index_aligned_transport_new_witness_operation)) * pfaa_left_c_aligned_transport_new) + (pfp_left_aligned_transport_new_witness_operation))) /\ (((((exists ff_h_pfp_aligned_transport_new_witness_operationright. ff_h_pfp_aligned_transport_new_witness_operationright + S (pfp_right_aligned_transport_new_witness_operation) = S ((S (pfp_index_aligned_transport_new_witness_operation)) * pfaa_right_c_aligned_transport_new)) /\ exists ff_q_pfp_aligned_transport_new_witness_operationright. pfaa_right_b_aligned_transport_new = ff_q_pfp_aligned_transport_new_witness_operationright * S ((S (pfp_index_aligned_transport_new_witness_operation)) * pfaa_right_c_aligned_transport_new) + (pfp_right_aligned_transport_new_witness_operation))) /\ (((((exists ff_h_pfp_aligned_transport_new_witness_operationtarget. ff_h_pfp_aligned_transport_new_witness_operationtarget + S (pfp_value_aligned_transport_new_witness_operation) = S ((S (pfp_index_aligned_transport_new_witness_operation)) * pfaa_sum_c_aligned_transport_new)) /\ exists ff_q_pfp_aligned_transport_new_witness_operationtarget. pfaa_sum_b_aligned_transport_new = ff_q_pfp_aligned_transport_new_witness_operationtarget * S ((S (pfp_index_aligned_transport_new_witness_operation)) * pfaa_sum_c_aligned_transport_new) + (pfp_value_aligned_transport_new_witness_operation))) /\ ((((exists pfa_gap_aligned_transport_new_witness_operationoperationleft. pfa_gap_aligned_transport_new_witness_operationoperationleft + S (pfp_left_aligned_transport_new_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_transport_new_witness_operationoperationright. pfa_gap_aligned_transport_new_witness_operationoperationright + S (pfp_right_aligned_transport_new_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_transport_new_witness_operationoperationresultbound. pfa_gap_aligned_transport_new_witness_operationoperationresultbound + S (pfp_value_aligned_transport_new_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_transport_new_witness_operationoperationresultcongruence pfa_offset_right_aligned_transport_new_witness_operationoperationresultcongruence. ((pfp_left_aligned_transport_new_witness_operation) + (pfp_right_aligned_transport_new_witness_operation)) + (p) * pfa_offset_left_aligned_transport_new_witness_operationoperationresultcongruence = (pfp_value_aligned_transport_new_witness_operation) + (p) * pfa_offset_right_aligned_transport_new_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_transport_new_witness_output pfrep_left_aligned_transport_new_witness_output pfrep_right_aligned_transport_new_witness_output. ((exists pfrep_position_aligned_transport_new_witness_outputfirst. ((pfrep_position_aligned_transport_new_witness_outputfirst+S (pfrep_power_aligned_transport_new_witness_output)=(pfaa_length_aligned_transport_new)) /\ ((((exists ff_h_pfp_aligned_transport_new_witness_outputfirstentry. ff_h_pfp_aligned_transport_new_witness_outputfirstentry + S (pfrep_left_aligned_transport_new_witness_output) = S ((S (pfrep_position_aligned_transport_new_witness_outputfirst)) * pfaa_sum_c_aligned_transport_new)) /\ exists ff_q_pfp_aligned_transport_new_witness_outputfirstentry. pfaa_sum_b_aligned_transport_new = ff_q_pfp_aligned_transport_new_witness_outputfirstentry * S ((S (pfrep_position_aligned_transport_new_witness_outputfirst)) * pfaa_sum_c_aligned_transport_new) + (pfrep_left_aligned_transport_new_witness_output)))))) \/ (((exists pfrep_gap_aligned_transport_new_witness_outputfirstoutside. pfrep_gap_aligned_transport_new_witness_outputfirstoutside+(pfaa_length_aligned_transport_new)=(pfrep_power_aligned_transport_new_witness_output)) /\ (((pfrep_left_aligned_transport_new_witness_output)=0))))) -> ((exists pfrep_position_aligned_transport_new_witness_outputsecond. ((pfrep_position_aligned_transport_new_witness_outputsecond+S (pfrep_power_aligned_transport_new_witness_output)=(I)) /\ ((((exists ff_h_pfp_aligned_transport_new_witness_outputsecondentry. ff_h_pfp_aligned_transport_new_witness_outputsecondentry + S (pfrep_right_aligned_transport_new_witness_output) = S ((S (pfrep_position_aligned_transport_new_witness_outputsecond)) * fc)) /\ exists ff_q_pfp_aligned_transport_new_witness_outputsecondentry. fb = ff_q_pfp_aligned_transport_new_witness_outputsecondentry * S ((S (pfrep_position_aligned_transport_new_witness_outputsecond)) * fc) + (pfrep_right_aligned_transport_new_witness_output)))))) \/ (((exists pfrep_gap_aligned_transport_new_witness_outputsecondoutside. pfrep_gap_aligned_transport_new_witness_outputsecondoutside+(I)=(pfrep_power_aligned_transport_new_witness_output)) /\ (((pfrep_right_aligned_transport_new_witness_output)=0))))) -> pfrep_left_aligned_transport_new_witness_output=pfrep_right_aligned_transport_new_witness_output)))))))))))))