prime_field_polynomial_bezout_equivalent_transport

Exact expanded first-order arithmetic statement

forall p ab ac A bb bc B gb gc G ub uc U vb vc V ab2 ac2 A2 bb2 bc2 B2 gb2 gc2 G2. (~(p=0)) -> (forall fom_index_pfp_transport_a_bound. (exists fom_gap_pfp_transport_a_bound_index_bound. fom_gap_pfp_transport_a_bound_index_bound + S (fom_index_pfp_transport_a_bound) = A2) -> exists fom_value_pfp_transport_a_bound. ((((exists fom_beta_height_pfp_transport_a_bound_entry. fom_beta_height_pfp_transport_a_bound_entry + S (fom_value_pfp_transport_a_bound) = S ((S (fom_index_pfp_transport_a_bound)) * ac2)) /\ exists fom_beta_quotient_pfp_transport_a_bound_entry. ab2 = fom_beta_quotient_pfp_transport_a_bound_entry * S ((S (fom_index_pfp_transport_a_bound)) * ac2) + (fom_value_pfp_transport_a_bound))) /\ (exists fom_gap_pfp_transport_a_bound_value_bound. fom_gap_pfp_transport_a_bound_value_bound + S (fom_value_pfp_transport_a_bound) = p))) -> (forall fom_index_pfp_transport_b_bound. (exists fom_gap_pfp_transport_b_bound_index_bound. fom_gap_pfp_transport_b_bound_index_bound + S (fom_index_pfp_transport_b_bound) = B2) -> exists fom_value_pfp_transport_b_bound. ((((exists fom_beta_height_pfp_transport_b_bound_entry. fom_beta_height_pfp_transport_b_bound_entry + S (fom_value_pfp_transport_b_bound) = S ((S (fom_index_pfp_transport_b_bound)) * bc2)) /\ exists fom_beta_quotient_pfp_transport_b_bound_entry. bb2 = fom_beta_quotient_pfp_transport_b_bound_entry * S ((S (fom_index_pfp_transport_b_bound)) * bc2) + (fom_value_pfp_transport_b_bound))) /\ (exists fom_gap_pfp_transport_b_bound_value_bound. fom_gap_pfp_transport_b_bound_value_bound + S (fom_value_pfp_transport_b_bound) = p))) -> (forall fom_index_pfp_transport_g_bound. (exists fom_gap_pfp_transport_g_bound_index_bound. fom_gap_pfp_transport_g_bound_index_bound + S (fom_index_pfp_transport_g_bound) = G2) -> exists fom_value_pfp_transport_g_bound. ((((exists fom_beta_height_pfp_transport_g_bound_entry. fom_beta_height_pfp_transport_g_bound_entry + S (fom_value_pfp_transport_g_bound) = S ((S (fom_index_pfp_transport_g_bound)) * gc2)) /\ exists fom_beta_quotient_pfp_transport_g_bound_entry. gb2 = fom_beta_quotient_pfp_transport_g_bound_entry * S ((S (fom_index_pfp_transport_g_bound)) * gc2) + (fom_value_pfp_transport_g_bound))) /\ (exists fom_gap_pfp_transport_g_bound_value_bound. fom_gap_pfp_transport_g_bound_value_bound + S (fom_value_pfp_transport_g_bound) = p))) -> (forall pfrep_power_transport_a_equivalent pfrep_left_transport_a_equivalent pfrep_right_transport_a_equivalent. ((exists pfrep_position_transport_a_equivalentfirst. ((pfrep_position_transport_a_equivalentfirst+S (pfrep_power_transport_a_equivalent)=(A)) /\ ((((exists ff_h_pfp_transport_a_equivalentfirstentry. ff_h_pfp_transport_a_equivalentfirstentry + S (pfrep_left_transport_a_equivalent) = S ((S (pfrep_position_transport_a_equivalentfirst)) * ac)) /\ exists ff_q_pfp_transport_a_equivalentfirstentry. ab = ff_q_pfp_transport_a_equivalentfirstentry * S ((S (pfrep_position_transport_a_equivalentfirst)) * ac) + (pfrep_left_transport_a_equivalent)))))) \/ (((exists pfrep_gap_transport_a_equivalentfirstoutside. pfrep_gap_transport_a_equivalentfirstoutside+(A)=(pfrep_power_transport_a_equivalent)) /\ (((pfrep_left_transport_a_equivalent)=0))))) -> ((exists pfrep_position_transport_a_equivalentsecond. ((pfrep_position_transport_a_equivalentsecond+S (pfrep_power_transport_a_equivalent)=(A2)) /\ ((((exists ff_h_pfp_transport_a_equivalentsecondentry. ff_h_pfp_transport_a_equivalentsecondentry + S (pfrep_right_transport_a_equivalent) = S ((S (pfrep_position_transport_a_equivalentsecond)) * ac2)) /\ exists ff_q_pfp_transport_a_equivalentsecondentry. ab2 = ff_q_pfp_transport_a_equivalentsecondentry * S ((S (pfrep_position_transport_a_equivalentsecond)) * ac2) + (pfrep_right_transport_a_equivalent)))))) \/ (((exists pfrep_gap_transport_a_equivalentsecondoutside. pfrep_gap_transport_a_equivalentsecondoutside+(A2)=(pfrep_power_transport_a_equivalent)) /\ (((pfrep_right_transport_a_equivalent)=0))))) -> pfrep_left_transport_a_equivalent=pfrep_right_transport_a_equivalent) -> (forall pfrep_power_transport_b_equivalent pfrep_left_transport_b_equivalent pfrep_right_transport_b_equivalent. ((exists pfrep_position_transport_b_equivalentfirst. ((pfrep_position_transport_b_equivalentfirst+S (pfrep_power_transport_b_equivalent)=(B)) /\ ((((exists ff_h_pfp_transport_b_equivalentfirstentry. ff_h_pfp_transport_b_equivalentfirstentry + S (pfrep_left_transport_b_equivalent) = S ((S (pfrep_position_transport_b_equivalentfirst)) * bc)) /\ exists ff_q_pfp_transport_b_equivalentfirstentry. bb = ff_q_pfp_transport_b_equivalentfirstentry * S ((S (pfrep_position_transport_b_equivalentfirst)) * bc) + (pfrep_left_transport_b_equivalent)))))) \/ (((exists pfrep_gap_transport_b_equivalentfirstoutside. pfrep_gap_transport_b_equivalentfirstoutside+(B)=(pfrep_power_transport_b_equivalent)) /\ (((pfrep_left_transport_b_equivalent)=0))))) -> ((exists pfrep_position_transport_b_equivalentsecond. ((pfrep_position_transport_b_equivalentsecond+S (pfrep_power_transport_b_equivalent)=(B2)) /\ ((((exists ff_h_pfp_transport_b_equivalentsecondentry. ff_h_pfp_transport_b_equivalentsecondentry + S (pfrep_right_transport_b_equivalent) = S ((S (pfrep_position_transport_b_equivalentsecond)) * bc2)) /\ exists ff_q_pfp_transport_b_equivalentsecondentry. bb2 = ff_q_pfp_transport_b_equivalentsecondentry * S ((S (pfrep_position_transport_b_equivalentsecond)) * bc2) + (pfrep_right_transport_b_equivalent)))))) \/ (((exists pfrep_gap_transport_b_equivalentsecondoutside. pfrep_gap_transport_b_equivalentsecondoutside+(B2)=(pfrep_power_transport_b_equivalent)) /\ (((pfrep_right_transport_b_equivalent)=0))))) -> pfrep_left_transport_b_equivalent=pfrep_right_transport_b_equivalent) -> (forall pfrep_power_transport_g_equivalent pfrep_left_transport_g_equivalent pfrep_right_transport_g_equivalent. ((exists pfrep_position_transport_g_equivalentfirst. ((pfrep_position_transport_g_equivalentfirst+S (pfrep_power_transport_g_equivalent)=(G)) /\ ((((exists ff_h_pfp_transport_g_equivalentfirstentry. ff_h_pfp_transport_g_equivalentfirstentry + S (pfrep_left_transport_g_equivalent) = S ((S (pfrep_position_transport_g_equivalentfirst)) * gc)) /\ exists ff_q_pfp_transport_g_equivalentfirstentry. gb = ff_q_pfp_transport_g_equivalentfirstentry * S ((S (pfrep_position_transport_g_equivalentfirst)) * gc) + (pfrep_left_transport_g_equivalent)))))) \/ (((exists pfrep_gap_transport_g_equivalentfirstoutside. pfrep_gap_transport_g_equivalentfirstoutside+(G)=(pfrep_power_transport_g_equivalent)) /\ (((pfrep_left_transport_g_equivalent)=0))))) -> ((exists pfrep_position_transport_g_equivalentsecond. ((pfrep_position_transport_g_equivalentsecond+S (pfrep_power_transport_g_equivalent)=(G2)) /\ ((((exists ff_h_pfp_transport_g_equivalentsecondentry. ff_h_pfp_transport_g_equivalentsecondentry + S (pfrep_right_transport_g_equivalent) = S ((S (pfrep_position_transport_g_equivalentsecond)) * gc2)) /\ exists ff_q_pfp_transport_g_equivalentsecondentry. gb2 = ff_q_pfp_transport_g_equivalentsecondentry * S ((S (pfrep_position_transport_g_equivalentsecond)) * gc2) + (pfrep_right_transport_g_equivalent)))))) \/ (((exists pfrep_gap_transport_g_equivalentsecondoutside. pfrep_gap_transport_g_equivalentsecondoutside+(G2)=(pfrep_power_transport_g_equivalent)) /\ (((pfrep_right_transport_g_equivalent)=0))))) -> pfrep_left_transport_g_equivalent=pfrep_right_transport_g_equivalent) -> (exists pfbz_left_code_transport_old pfbz_left_scale_transport_old pfbz_left_length_transport_old pfbz_right_code_transport_old pfbz_right_scale_transport_old pfbz_right_length_transport_old. ((((forall fom_index_pfp_transport_old_left_productleft. (exists fom_gap_pfp_transport_old_left_productleft_index_bound. fom_gap_pfp_transport_old_left_productleft_index_bound + S (fom_index_pfp_transport_old_left_productleft) = U) -> exists fom_value_pfp_transport_old_left_productleft. ((((exists fom_beta_height_pfp_transport_old_left_productleft_entry. fom_beta_height_pfp_transport_old_left_productleft_entry + S (fom_value_pfp_transport_old_left_productleft) = S ((S (fom_index_pfp_transport_old_left_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_transport_old_left_productleft_entry. ub = fom_beta_quotient_pfp_transport_old_left_productleft_entry * S ((S (fom_index_pfp_transport_old_left_productleft)) * uc) + (fom_value_pfp_transport_old_left_productleft))) /\ (exists fom_gap_pfp_transport_old_left_productleft_value_bound. fom_gap_pfp_transport_old_left_productleft_value_bound + S (fom_value_pfp_transport_old_left_productleft) = p))) /\ (((forall fom_index_pfp_transport_old_left_productright. (exists fom_gap_pfp_transport_old_left_productright_index_bound. fom_gap_pfp_transport_old_left_productright_index_bound + S (fom_index_pfp_transport_old_left_productright) = A) -> exists fom_value_pfp_transport_old_left_productright. ((((exists fom_beta_height_pfp_transport_old_left_productright_entry. fom_beta_height_pfp_transport_old_left_productright_entry + S (fom_value_pfp_transport_old_left_productright) = S ((S (fom_index_pfp_transport_old_left_productright)) * ac)) /\ exists fom_beta_quotient_pfp_transport_old_left_productright_entry. ab = fom_beta_quotient_pfp_transport_old_left_productright_entry * S ((S (fom_index_pfp_transport_old_left_productright)) * ac) + (fom_value_pfp_transport_old_left_productright))) /\ (exists fom_gap_pfp_transport_old_left_productright_value_bound. fom_gap_pfp_transport_old_left_productright_value_bound + S (fom_value_pfp_transport_old_left_productright) = p))) /\ (((((((U)=0 \/ (A)=0) /\ (((pfbz_left_length_transport_old)=0)))) \/ (((~((U)=0)) /\ (((~((A)=0)) /\ (((U)+(A)=S (pfbz_left_length_transport_old)))))))) /\ ((forall pfc_index_transport_old_left_productcoefficients. (exists pfa_gap_transport_old_left_productcoefficientsbound. pfa_gap_transport_old_left_productcoefficientsbound + S (pfc_index_transport_old_left_productcoefficients) = (pfbz_left_length_transport_old)) -> exists pfc_value_transport_old_left_productcoefficients. ((((exists ff_h_pfp_transport_old_left_productcoefficientsentry. ff_h_pfp_transport_old_left_productcoefficientsentry + S (pfc_value_transport_old_left_productcoefficients) = S ((S (pfc_index_transport_old_left_productcoefficients)) * pfbz_left_scale_transport_old)) /\ exists ff_q_pfp_transport_old_left_productcoefficientsentry. pfbz_left_code_transport_old = ff_q_pfp_transport_old_left_productcoefficientsentry * S ((S (pfc_index_transport_old_left_productcoefficients)) * pfbz_left_scale_transport_old) + (pfc_value_transport_old_left_productcoefficients))) /\ ((exists pfc_terms_code_transport_old_left_productcoefficientscoefficient pfc_terms_scale_transport_old_left_productcoefficientscoefficient pfc_natural_sum_transport_old_left_productcoefficientscoefficient. ((forall pfc_index_transport_old_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_old_left_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_old_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_old_left_productcoefficients))) -> exists pfc_value_transport_old_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_old_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_old_left_productcoefficientscoefficient = ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient) + (pfc_value_transport_old_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)+pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_old_left_productcoefficients)) /\ ((((((exists pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal) = (U)) /\ ((((exists ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftoutside+(U)=(pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm) = (A)) /\ ((((exists ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightoutside+(A)=(pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_old_left_productcoefficientscoefficientdiagonal)=pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm*pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_old_left_productcoefficientscoefficientsum fs_v_pfc_transport_old_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_old_left_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_old_left_productcoefficients))) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_old_left_productcoefficients))) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_old_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_old_left_productcoefficients)) -> exists fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_old_left_productcoefficientscoefficient = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient) + (fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_old_left_productcoefficientscoefficientresiduebound. pfa_gap_transport_old_left_productcoefficientscoefficientresiduebound + S (pfc_value_transport_old_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_old_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_old_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_old_left_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_old_left_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_old_left_productcoefficients) + (p) * pfa_offset_right_transport_old_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_transport_old_right_productleft. (exists fom_gap_pfp_transport_old_right_productleft_index_bound. fom_gap_pfp_transport_old_right_productleft_index_bound + S (fom_index_pfp_transport_old_right_productleft) = V) -> exists fom_value_pfp_transport_old_right_productleft. ((((exists fom_beta_height_pfp_transport_old_right_productleft_entry. fom_beta_height_pfp_transport_old_right_productleft_entry + S (fom_value_pfp_transport_old_right_productleft) = S ((S (fom_index_pfp_transport_old_right_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_transport_old_right_productleft_entry. vb = fom_beta_quotient_pfp_transport_old_right_productleft_entry * S ((S (fom_index_pfp_transport_old_right_productleft)) * vc) + (fom_value_pfp_transport_old_right_productleft))) /\ (exists fom_gap_pfp_transport_old_right_productleft_value_bound. fom_gap_pfp_transport_old_right_productleft_value_bound + S (fom_value_pfp_transport_old_right_productleft) = p))) /\ (((forall fom_index_pfp_transport_old_right_productright. (exists fom_gap_pfp_transport_old_right_productright_index_bound. fom_gap_pfp_transport_old_right_productright_index_bound + S (fom_index_pfp_transport_old_right_productright) = B) -> exists fom_value_pfp_transport_old_right_productright. ((((exists fom_beta_height_pfp_transport_old_right_productright_entry. fom_beta_height_pfp_transport_old_right_productright_entry + S (fom_value_pfp_transport_old_right_productright) = S ((S (fom_index_pfp_transport_old_right_productright)) * bc)) /\ exists fom_beta_quotient_pfp_transport_old_right_productright_entry. bb = fom_beta_quotient_pfp_transport_old_right_productright_entry * S ((S (fom_index_pfp_transport_old_right_productright)) * bc) + (fom_value_pfp_transport_old_right_productright))) /\ (exists fom_gap_pfp_transport_old_right_productright_value_bound. fom_gap_pfp_transport_old_right_productright_value_bound + S (fom_value_pfp_transport_old_right_productright) = p))) /\ (((((((V)=0 \/ (B)=0) /\ (((pfbz_right_length_transport_old)=0)))) \/ (((~((V)=0)) /\ (((~((B)=0)) /\ (((V)+(B)=S (pfbz_right_length_transport_old)))))))) /\ ((forall pfc_index_transport_old_right_productcoefficients. (exists pfa_gap_transport_old_right_productcoefficientsbound. pfa_gap_transport_old_right_productcoefficientsbound + S (pfc_index_transport_old_right_productcoefficients) = (pfbz_right_length_transport_old)) -> exists pfc_value_transport_old_right_productcoefficients. ((((exists ff_h_pfp_transport_old_right_productcoefficientsentry. ff_h_pfp_transport_old_right_productcoefficientsentry + S (pfc_value_transport_old_right_productcoefficients) = S ((S (pfc_index_transport_old_right_productcoefficients)) * pfbz_right_scale_transport_old)) /\ exists ff_q_pfp_transport_old_right_productcoefficientsentry. pfbz_right_code_transport_old = ff_q_pfp_transport_old_right_productcoefficientsentry * S ((S (pfc_index_transport_old_right_productcoefficients)) * pfbz_right_scale_transport_old) + (pfc_value_transport_old_right_productcoefficients))) /\ ((exists pfc_terms_code_transport_old_right_productcoefficientscoefficient pfc_terms_scale_transport_old_right_productcoefficientscoefficient pfc_natural_sum_transport_old_right_productcoefficientscoefficient. ((forall pfc_index_transport_old_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_old_right_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_old_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_old_right_productcoefficients))) -> exists pfc_value_transport_old_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_old_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_old_right_productcoefficientscoefficient = ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient) + (pfc_value_transport_old_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)+pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_old_right_productcoefficients)) /\ ((((((exists pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal) = (V)) /\ ((((exists ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftoutside+(V)=(pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm) = (B)) /\ ((((exists ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightoutside+(B)=(pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_old_right_productcoefficientscoefficientdiagonal)=pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm*pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_old_right_productcoefficientscoefficientsum fs_v_pfc_transport_old_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_old_right_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_old_right_productcoefficients))) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_old_right_productcoefficients))) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_old_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_old_right_productcoefficients)) -> exists fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_old_right_productcoefficientscoefficient = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient) + (fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_old_right_productcoefficientscoefficientresiduebound. pfa_gap_transport_old_right_productcoefficientscoefficientresiduebound + S (pfc_value_transport_old_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_old_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_old_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_old_right_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_old_right_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_old_right_productcoefficients) + (p) * pfa_offset_right_transport_old_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_transport_old_sum_left_bounded. (exists fom_gap_pfp_transport_old_sum_left_bounded_index_bound. fom_gap_pfp_transport_old_sum_left_bounded_index_bound + S (fom_index_pfp_transport_old_sum_left_bounded) = pfbz_left_length_transport_old) -> exists fom_value_pfp_transport_old_sum_left_bounded. ((((exists fom_beta_height_pfp_transport_old_sum_left_bounded_entry. fom_beta_height_pfp_transport_old_sum_left_bounded_entry + S (fom_value_pfp_transport_old_sum_left_bounded) = S ((S (fom_index_pfp_transport_old_sum_left_bounded)) * pfbz_left_scale_transport_old)) /\ exists fom_beta_quotient_pfp_transport_old_sum_left_bounded_entry. pfbz_left_code_transport_old = fom_beta_quotient_pfp_transport_old_sum_left_bounded_entry * S ((S (fom_index_pfp_transport_old_sum_left_bounded)) * pfbz_left_scale_transport_old) + (fom_value_pfp_transport_old_sum_left_bounded))) /\ (exists fom_gap_pfp_transport_old_sum_left_bounded_value_bound. fom_gap_pfp_transport_old_sum_left_bounded_value_bound + S (fom_value_pfp_transport_old_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_transport_old_sum_right_bounded. (exists fom_gap_pfp_transport_old_sum_right_bounded_index_bound. fom_gap_pfp_transport_old_sum_right_bounded_index_bound + S (fom_index_pfp_transport_old_sum_right_bounded) = pfbz_right_length_transport_old) -> exists fom_value_pfp_transport_old_sum_right_bounded. ((((exists fom_beta_height_pfp_transport_old_sum_right_bounded_entry. fom_beta_height_pfp_transport_old_sum_right_bounded_entry + S (fom_value_pfp_transport_old_sum_right_bounded) = S ((S (fom_index_pfp_transport_old_sum_right_bounded)) * pfbz_right_scale_transport_old)) /\ exists fom_beta_quotient_pfp_transport_old_sum_right_bounded_entry. pfbz_right_code_transport_old = fom_beta_quotient_pfp_transport_old_sum_right_bounded_entry * S ((S (fom_index_pfp_transport_old_sum_right_bounded)) * pfbz_right_scale_transport_old) + (fom_value_pfp_transport_old_sum_right_bounded))) /\ (exists fom_gap_pfp_transport_old_sum_right_bounded_value_bound. fom_gap_pfp_transport_old_sum_right_bounded_value_bound + S (fom_value_pfp_transport_old_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_transport_old_sum_result_bounded. (exists fom_gap_pfp_transport_old_sum_result_bounded_index_bound. fom_gap_pfp_transport_old_sum_result_bounded_index_bound + S (fom_index_pfp_transport_old_sum_result_bounded) = G) -> exists fom_value_pfp_transport_old_sum_result_bounded. ((((exists fom_beta_height_pfp_transport_old_sum_result_bounded_entry. fom_beta_height_pfp_transport_old_sum_result_bounded_entry + S (fom_value_pfp_transport_old_sum_result_bounded) = S ((S (fom_index_pfp_transport_old_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_transport_old_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_transport_old_sum_result_bounded_entry * S ((S (fom_index_pfp_transport_old_sum_result_bounded)) * gc) + (fom_value_pfp_transport_old_sum_result_bounded))) /\ (exists fom_gap_pfp_transport_old_sum_result_bounded_value_bound. fom_gap_pfp_transport_old_sum_result_bounded_value_bound + S (fom_value_pfp_transport_old_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_transport_old_sum pfaa_left_c_transport_old_sum pfaa_right_b_transport_old_sum pfaa_right_c_transport_old_sum pfaa_sum_b_transport_old_sum pfaa_sum_c_transport_old_sum pfaa_length_transport_old_sum. ((((forall pfrep_power_transport_old_sum_witness_common_left pfrep_left_transport_old_sum_witness_common_left pfrep_right_transport_old_sum_witness_common_left. ((exists pfrep_position_transport_old_sum_witness_common_leftfirst. ((pfrep_position_transport_old_sum_witness_common_leftfirst+S (pfrep_power_transport_old_sum_witness_common_left)=(pfbz_left_length_transport_old)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_leftfirstentry. ff_h_pfp_transport_old_sum_witness_common_leftfirstentry + S (pfrep_left_transport_old_sum_witness_common_left) = S ((S (pfrep_position_transport_old_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_old)) /\ exists ff_q_pfp_transport_old_sum_witness_common_leftfirstentry. pfbz_left_code_transport_old = ff_q_pfp_transport_old_sum_witness_common_leftfirstentry * S ((S (pfrep_position_transport_old_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_old) + (pfrep_left_transport_old_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_leftfirstoutside. pfrep_gap_transport_old_sum_witness_common_leftfirstoutside+(pfbz_left_length_transport_old)=(pfrep_power_transport_old_sum_witness_common_left)) /\ (((pfrep_left_transport_old_sum_witness_common_left)=0))))) -> ((exists pfrep_position_transport_old_sum_witness_common_leftsecond. ((pfrep_position_transport_old_sum_witness_common_leftsecond+S (pfrep_power_transport_old_sum_witness_common_left)=(pfaa_length_transport_old_sum)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_leftsecondentry. ff_h_pfp_transport_old_sum_witness_common_leftsecondentry + S (pfrep_right_transport_old_sum_witness_common_left) = S ((S (pfrep_position_transport_old_sum_witness_common_leftsecond)) * pfaa_left_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_common_leftsecondentry. pfaa_left_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_common_leftsecondentry * S ((S (pfrep_position_transport_old_sum_witness_common_leftsecond)) * pfaa_left_c_transport_old_sum) + (pfrep_right_transport_old_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_leftsecondoutside. pfrep_gap_transport_old_sum_witness_common_leftsecondoutside+(pfaa_length_transport_old_sum)=(pfrep_power_transport_old_sum_witness_common_left)) /\ (((pfrep_right_transport_old_sum_witness_common_left)=0))))) -> pfrep_left_transport_old_sum_witness_common_left=pfrep_right_transport_old_sum_witness_common_left) /\ ((forall pfrep_power_transport_old_sum_witness_common_right pfrep_left_transport_old_sum_witness_common_right pfrep_right_transport_old_sum_witness_common_right. ((exists pfrep_position_transport_old_sum_witness_common_rightfirst. ((pfrep_position_transport_old_sum_witness_common_rightfirst+S (pfrep_power_transport_old_sum_witness_common_right)=(pfbz_right_length_transport_old)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_rightfirstentry. ff_h_pfp_transport_old_sum_witness_common_rightfirstentry + S (pfrep_left_transport_old_sum_witness_common_right) = S ((S (pfrep_position_transport_old_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_old)) /\ exists ff_q_pfp_transport_old_sum_witness_common_rightfirstentry. pfbz_right_code_transport_old = ff_q_pfp_transport_old_sum_witness_common_rightfirstentry * S ((S (pfrep_position_transport_old_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_old) + (pfrep_left_transport_old_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_rightfirstoutside. pfrep_gap_transport_old_sum_witness_common_rightfirstoutside+(pfbz_right_length_transport_old)=(pfrep_power_transport_old_sum_witness_common_right)) /\ (((pfrep_left_transport_old_sum_witness_common_right)=0))))) -> ((exists pfrep_position_transport_old_sum_witness_common_rightsecond. ((pfrep_position_transport_old_sum_witness_common_rightsecond+S (pfrep_power_transport_old_sum_witness_common_right)=(pfaa_length_transport_old_sum)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_rightsecondentry. ff_h_pfp_transport_old_sum_witness_common_rightsecondentry + S (pfrep_right_transport_old_sum_witness_common_right) = S ((S (pfrep_position_transport_old_sum_witness_common_rightsecond)) * pfaa_right_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_common_rightsecondentry. pfaa_right_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_common_rightsecondentry * S ((S (pfrep_position_transport_old_sum_witness_common_rightsecond)) * pfaa_right_c_transport_old_sum) + (pfrep_right_transport_old_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_rightsecondoutside. pfrep_gap_transport_old_sum_witness_common_rightsecondoutside+(pfaa_length_transport_old_sum)=(pfrep_power_transport_old_sum_witness_common_right)) /\ (((pfrep_right_transport_old_sum_witness_common_right)=0))))) -> pfrep_left_transport_old_sum_witness_common_right=pfrep_right_transport_old_sum_witness_common_right)))) /\ (((forall pfp_index_transport_old_sum_witness_operation. (exists pfa_gap_transport_old_sum_witness_operationindex. pfa_gap_transport_old_sum_witness_operationindex + S (pfp_index_transport_old_sum_witness_operation) = (pfaa_length_transport_old_sum)) -> exists pfp_left_transport_old_sum_witness_operation pfp_right_transport_old_sum_witness_operation pfp_value_transport_old_sum_witness_operation. ((((exists ff_h_pfp_transport_old_sum_witness_operationleft. ff_h_pfp_transport_old_sum_witness_operationleft + S (pfp_left_transport_old_sum_witness_operation) = S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_left_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_operationleft. pfaa_left_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_operationleft * S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_left_c_transport_old_sum) + (pfp_left_transport_old_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_old_sum_witness_operationright. ff_h_pfp_transport_old_sum_witness_operationright + S (pfp_right_transport_old_sum_witness_operation) = S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_right_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_operationright. pfaa_right_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_operationright * S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_right_c_transport_old_sum) + (pfp_right_transport_old_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_old_sum_witness_operationtarget. ff_h_pfp_transport_old_sum_witness_operationtarget + S (pfp_value_transport_old_sum_witness_operation) = S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_sum_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_operationtarget. pfaa_sum_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_operationtarget * S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_sum_c_transport_old_sum) + (pfp_value_transport_old_sum_witness_operation))) /\ ((((exists pfa_gap_transport_old_sum_witness_operationoperationleft. pfa_gap_transport_old_sum_witness_operationoperationleft + S (pfp_left_transport_old_sum_witness_operation) = (p)) /\ (((exists pfa_gap_transport_old_sum_witness_operationoperationright. pfa_gap_transport_old_sum_witness_operationoperationright + S (pfp_right_transport_old_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_transport_old_sum_witness_operationoperationresultbound. pfa_gap_transport_old_sum_witness_operationoperationresultbound + S (pfp_value_transport_old_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_transport_old_sum_witness_operationoperationresultcongruence pfa_offset_right_transport_old_sum_witness_operationoperationresultcongruence. ((pfp_left_transport_old_sum_witness_operation) + (pfp_right_transport_old_sum_witness_operation)) + (p) * pfa_offset_left_transport_old_sum_witness_operationoperationresultcongruence = (pfp_value_transport_old_sum_witness_operation) + (p) * pfa_offset_right_transport_old_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_transport_old_sum_witness_output pfrep_left_transport_old_sum_witness_output pfrep_right_transport_old_sum_witness_output. ((exists pfrep_position_transport_old_sum_witness_outputfirst. ((pfrep_position_transport_old_sum_witness_outputfirst+S (pfrep_power_transport_old_sum_witness_output)=(pfaa_length_transport_old_sum)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_outputfirstentry. ff_h_pfp_transport_old_sum_witness_outputfirstentry + S (pfrep_left_transport_old_sum_witness_output) = S ((S (pfrep_position_transport_old_sum_witness_outputfirst)) * pfaa_sum_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_outputfirstentry. pfaa_sum_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_outputfirstentry * S ((S (pfrep_position_transport_old_sum_witness_outputfirst)) * pfaa_sum_c_transport_old_sum) + (pfrep_left_transport_old_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_outputfirstoutside. pfrep_gap_transport_old_sum_witness_outputfirstoutside+(pfaa_length_transport_old_sum)=(pfrep_power_transport_old_sum_witness_output)) /\ (((pfrep_left_transport_old_sum_witness_output)=0))))) -> ((exists pfrep_position_transport_old_sum_witness_outputsecond. ((pfrep_position_transport_old_sum_witness_outputsecond+S (pfrep_power_transport_old_sum_witness_output)=(G)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_outputsecondentry. ff_h_pfp_transport_old_sum_witness_outputsecondentry + S (pfrep_right_transport_old_sum_witness_output) = S ((S (pfrep_position_transport_old_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_transport_old_sum_witness_outputsecondentry. gb = ff_q_pfp_transport_old_sum_witness_outputsecondentry * S ((S (pfrep_position_transport_old_sum_witness_outputsecond)) * gc) + (pfrep_right_transport_old_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_outputsecondoutside. pfrep_gap_transport_old_sum_witness_outputsecondoutside+(G)=(pfrep_power_transport_old_sum_witness_output)) /\ (((pfrep_right_transport_old_sum_witness_output)=0))))) -> pfrep_left_transport_old_sum_witness_output=pfrep_right_transport_old_sum_witness_output)))))))))))))))))) -> (exists pfbz_left_code_transport_result pfbz_left_scale_transport_result pfbz_left_length_transport_result pfbz_right_code_transport_result pfbz_right_scale_transport_result pfbz_right_length_transport_result. ((((forall fom_index_pfp_transport_result_left_productleft. (exists fom_gap_pfp_transport_result_left_productleft_index_bound. fom_gap_pfp_transport_result_left_productleft_index_bound + S (fom_index_pfp_transport_result_left_productleft) = U) -> exists fom_value_pfp_transport_result_left_productleft. ((((exists fom_beta_height_pfp_transport_result_left_productleft_entry. fom_beta_height_pfp_transport_result_left_productleft_entry + S (fom_value_pfp_transport_result_left_productleft) = S ((S (fom_index_pfp_transport_result_left_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_transport_result_left_productleft_entry. ub = fom_beta_quotient_pfp_transport_result_left_productleft_entry * S ((S (fom_index_pfp_transport_result_left_productleft)) * uc) + (fom_value_pfp_transport_result_left_productleft))) /\ (exists fom_gap_pfp_transport_result_left_productleft_value_bound. fom_gap_pfp_transport_result_left_productleft_value_bound + S (fom_value_pfp_transport_result_left_productleft) = p))) /\ (((forall fom_index_pfp_transport_result_left_productright. (exists fom_gap_pfp_transport_result_left_productright_index_bound. fom_gap_pfp_transport_result_left_productright_index_bound + S (fom_index_pfp_transport_result_left_productright) = A2) -> exists fom_value_pfp_transport_result_left_productright. ((((exists fom_beta_height_pfp_transport_result_left_productright_entry. fom_beta_height_pfp_transport_result_left_productright_entry + S (fom_value_pfp_transport_result_left_productright) = S ((S (fom_index_pfp_transport_result_left_productright)) * ac2)) /\ exists fom_beta_quotient_pfp_transport_result_left_productright_entry. ab2 = fom_beta_quotient_pfp_transport_result_left_productright_entry * S ((S (fom_index_pfp_transport_result_left_productright)) * ac2) + (fom_value_pfp_transport_result_left_productright))) /\ (exists fom_gap_pfp_transport_result_left_productright_value_bound. fom_gap_pfp_transport_result_left_productright_value_bound + S (fom_value_pfp_transport_result_left_productright) = p))) /\ (((((((U)=0 \/ (A2)=0) /\ (((pfbz_left_length_transport_result)=0)))) \/ (((~((U)=0)) /\ (((~((A2)=0)) /\ (((U)+(A2)=S (pfbz_left_length_transport_result)))))))) /\ ((forall pfc_index_transport_result_left_productcoefficients. (exists pfa_gap_transport_result_left_productcoefficientsbound. pfa_gap_transport_result_left_productcoefficientsbound + S (pfc_index_transport_result_left_productcoefficients) = (pfbz_left_length_transport_result)) -> exists pfc_value_transport_result_left_productcoefficients. ((((exists ff_h_pfp_transport_result_left_productcoefficientsentry. ff_h_pfp_transport_result_left_productcoefficientsentry + S (pfc_value_transport_result_left_productcoefficients) = S ((S (pfc_index_transport_result_left_productcoefficients)) * pfbz_left_scale_transport_result)) /\ exists ff_q_pfp_transport_result_left_productcoefficientsentry. pfbz_left_code_transport_result = ff_q_pfp_transport_result_left_productcoefficientsentry * S ((S (pfc_index_transport_result_left_productcoefficients)) * pfbz_left_scale_transport_result) + (pfc_value_transport_result_left_productcoefficients))) /\ ((exists pfc_terms_code_transport_result_left_productcoefficientscoefficient pfc_terms_scale_transport_result_left_productcoefficientscoefficient pfc_natural_sum_transport_result_left_productcoefficientscoefficient. ((forall pfc_index_transport_result_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_result_left_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_result_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_result_left_productcoefficients))) -> exists pfc_value_transport_result_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_result_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_result_left_productcoefficientscoefficient = ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient) + (pfc_value_transport_result_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)+pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_result_left_productcoefficients)) /\ ((((((exists pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal) = (U)) /\ ((((exists ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftoutside+(U)=(pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm) = (A2)) /\ ((((exists ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm)) * ac2)) /\ exists ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry. ab2 = ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm)) * ac2) + (pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightoutside+(A2)=(pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_result_left_productcoefficientscoefficientdiagonal)=pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm*pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_result_left_productcoefficientscoefficientsum fs_v_pfc_transport_result_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_result_left_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_result_left_productcoefficients))) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_result_left_productcoefficients))) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_result_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_result_left_productcoefficients)) -> exists fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_result_left_productcoefficientscoefficient = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient) + (fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_result_left_productcoefficientscoefficientresiduebound. pfa_gap_transport_result_left_productcoefficientscoefficientresiduebound + S (pfc_value_transport_result_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_result_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_result_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_result_left_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_result_left_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_result_left_productcoefficients) + (p) * pfa_offset_right_transport_result_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_transport_result_right_productleft. (exists fom_gap_pfp_transport_result_right_productleft_index_bound. fom_gap_pfp_transport_result_right_productleft_index_bound + S (fom_index_pfp_transport_result_right_productleft) = V) -> exists fom_value_pfp_transport_result_right_productleft. ((((exists fom_beta_height_pfp_transport_result_right_productleft_entry. fom_beta_height_pfp_transport_result_right_productleft_entry + S (fom_value_pfp_transport_result_right_productleft) = S ((S (fom_index_pfp_transport_result_right_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_transport_result_right_productleft_entry. vb = fom_beta_quotient_pfp_transport_result_right_productleft_entry * S ((S (fom_index_pfp_transport_result_right_productleft)) * vc) + (fom_value_pfp_transport_result_right_productleft))) /\ (exists fom_gap_pfp_transport_result_right_productleft_value_bound. fom_gap_pfp_transport_result_right_productleft_value_bound + S (fom_value_pfp_transport_result_right_productleft) = p))) /\ (((forall fom_index_pfp_transport_result_right_productright. (exists fom_gap_pfp_transport_result_right_productright_index_bound. fom_gap_pfp_transport_result_right_productright_index_bound + S (fom_index_pfp_transport_result_right_productright) = B2) -> exists fom_value_pfp_transport_result_right_productright. ((((exists fom_beta_height_pfp_transport_result_right_productright_entry. fom_beta_height_pfp_transport_result_right_productright_entry + S (fom_value_pfp_transport_result_right_productright) = S ((S (fom_index_pfp_transport_result_right_productright)) * bc2)) /\ exists fom_beta_quotient_pfp_transport_result_right_productright_entry. bb2 = fom_beta_quotient_pfp_transport_result_right_productright_entry * S ((S (fom_index_pfp_transport_result_right_productright)) * bc2) + (fom_value_pfp_transport_result_right_productright))) /\ (exists fom_gap_pfp_transport_result_right_productright_value_bound. fom_gap_pfp_transport_result_right_productright_value_bound + S (fom_value_pfp_transport_result_right_productright) = p))) /\ (((((((V)=0 \/ (B2)=0) /\ (((pfbz_right_length_transport_result)=0)))) \/ (((~((V)=0)) /\ (((~((B2)=0)) /\ (((V)+(B2)=S (pfbz_right_length_transport_result)))))))) /\ ((forall pfc_index_transport_result_right_productcoefficients. (exists pfa_gap_transport_result_right_productcoefficientsbound. pfa_gap_transport_result_right_productcoefficientsbound + S (pfc_index_transport_result_right_productcoefficients) = (pfbz_right_length_transport_result)) -> exists pfc_value_transport_result_right_productcoefficients. ((((exists ff_h_pfp_transport_result_right_productcoefficientsentry. ff_h_pfp_transport_result_right_productcoefficientsentry + S (pfc_value_transport_result_right_productcoefficients) = S ((S (pfc_index_transport_result_right_productcoefficients)) * pfbz_right_scale_transport_result)) /\ exists ff_q_pfp_transport_result_right_productcoefficientsentry. pfbz_right_code_transport_result = ff_q_pfp_transport_result_right_productcoefficientsentry * S ((S (pfc_index_transport_result_right_productcoefficients)) * pfbz_right_scale_transport_result) + (pfc_value_transport_result_right_productcoefficients))) /\ ((exists pfc_terms_code_transport_result_right_productcoefficientscoefficient pfc_terms_scale_transport_result_right_productcoefficientscoefficient pfc_natural_sum_transport_result_right_productcoefficientscoefficient. ((forall pfc_index_transport_result_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_result_right_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_result_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_result_right_productcoefficients))) -> exists pfc_value_transport_result_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_result_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_result_right_productcoefficientscoefficient = ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient) + (pfc_value_transport_result_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)+pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_result_right_productcoefficients)) /\ ((((((exists pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal) = (V)) /\ ((((exists ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftoutside+(V)=(pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm) = (B2)) /\ ((((exists ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm)) * bc2)) /\ exists ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry. bb2 = ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm)) * bc2) + (pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightoutside+(B2)=(pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_result_right_productcoefficientscoefficientdiagonal)=pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm*pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_result_right_productcoefficientscoefficientsum fs_v_pfc_transport_result_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_result_right_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_result_right_productcoefficients))) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_result_right_productcoefficients))) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_result_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_result_right_productcoefficients)) -> exists fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_result_right_productcoefficientscoefficient = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient) + (fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_result_right_productcoefficientscoefficientresiduebound. pfa_gap_transport_result_right_productcoefficientscoefficientresiduebound + S (pfc_value_transport_result_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_result_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_result_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_result_right_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_result_right_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_result_right_productcoefficients) + (p) * pfa_offset_right_transport_result_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_transport_result_sum_left_bounded. (exists fom_gap_pfp_transport_result_sum_left_bounded_index_bound. fom_gap_pfp_transport_result_sum_left_bounded_index_bound + S (fom_index_pfp_transport_result_sum_left_bounded) = pfbz_left_length_transport_result) -> exists fom_value_pfp_transport_result_sum_left_bounded. ((((exists fom_beta_height_pfp_transport_result_sum_left_bounded_entry. fom_beta_height_pfp_transport_result_sum_left_bounded_entry + S (fom_value_pfp_transport_result_sum_left_bounded) = S ((S (fom_index_pfp_transport_result_sum_left_bounded)) * pfbz_left_scale_transport_result)) /\ exists fom_beta_quotient_pfp_transport_result_sum_left_bounded_entry. pfbz_left_code_transport_result = fom_beta_quotient_pfp_transport_result_sum_left_bounded_entry * S ((S (fom_index_pfp_transport_result_sum_left_bounded)) * pfbz_left_scale_transport_result) + (fom_value_pfp_transport_result_sum_left_bounded))) /\ (exists fom_gap_pfp_transport_result_sum_left_bounded_value_bound. fom_gap_pfp_transport_result_sum_left_bounded_value_bound + S (fom_value_pfp_transport_result_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_transport_result_sum_right_bounded. (exists fom_gap_pfp_transport_result_sum_right_bounded_index_bound. fom_gap_pfp_transport_result_sum_right_bounded_index_bound + S (fom_index_pfp_transport_result_sum_right_bounded) = pfbz_right_length_transport_result) -> exists fom_value_pfp_transport_result_sum_right_bounded. ((((exists fom_beta_height_pfp_transport_result_sum_right_bounded_entry. fom_beta_height_pfp_transport_result_sum_right_bounded_entry + S (fom_value_pfp_transport_result_sum_right_bounded) = S ((S (fom_index_pfp_transport_result_sum_right_bounded)) * pfbz_right_scale_transport_result)) /\ exists fom_beta_quotient_pfp_transport_result_sum_right_bounded_entry. pfbz_right_code_transport_result = fom_beta_quotient_pfp_transport_result_sum_right_bounded_entry * S ((S (fom_index_pfp_transport_result_sum_right_bounded)) * pfbz_right_scale_transport_result) + (fom_value_pfp_transport_result_sum_right_bounded))) /\ (exists fom_gap_pfp_transport_result_sum_right_bounded_value_bound. fom_gap_pfp_transport_result_sum_right_bounded_value_bound + S (fom_value_pfp_transport_result_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_transport_result_sum_result_bounded. (exists fom_gap_pfp_transport_result_sum_result_bounded_index_bound. fom_gap_pfp_transport_result_sum_result_bounded_index_bound + S (fom_index_pfp_transport_result_sum_result_bounded) = G2) -> exists fom_value_pfp_transport_result_sum_result_bounded. ((((exists fom_beta_height_pfp_transport_result_sum_result_bounded_entry. fom_beta_height_pfp_transport_result_sum_result_bounded_entry + S (fom_value_pfp_transport_result_sum_result_bounded) = S ((S (fom_index_pfp_transport_result_sum_result_bounded)) * gc2)) /\ exists fom_beta_quotient_pfp_transport_result_sum_result_bounded_entry. gb2 = fom_beta_quotient_pfp_transport_result_sum_result_bounded_entry * S ((S (fom_index_pfp_transport_result_sum_result_bounded)) * gc2) + (fom_value_pfp_transport_result_sum_result_bounded))) /\ (exists fom_gap_pfp_transport_result_sum_result_bounded_value_bound. fom_gap_pfp_transport_result_sum_result_bounded_value_bound + S (fom_value_pfp_transport_result_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_transport_result_sum pfaa_left_c_transport_result_sum pfaa_right_b_transport_result_sum pfaa_right_c_transport_result_sum pfaa_sum_b_transport_result_sum pfaa_sum_c_transport_result_sum pfaa_length_transport_result_sum. ((((forall pfrep_power_transport_result_sum_witness_common_left pfrep_left_transport_result_sum_witness_common_left pfrep_right_transport_result_sum_witness_common_left. ((exists pfrep_position_transport_result_sum_witness_common_leftfirst. ((pfrep_position_transport_result_sum_witness_common_leftfirst+S (pfrep_power_transport_result_sum_witness_common_left)=(pfbz_left_length_transport_result)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_leftfirstentry. ff_h_pfp_transport_result_sum_witness_common_leftfirstentry + S (pfrep_left_transport_result_sum_witness_common_left) = S ((S (pfrep_position_transport_result_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_result)) /\ exists ff_q_pfp_transport_result_sum_witness_common_leftfirstentry. pfbz_left_code_transport_result = ff_q_pfp_transport_result_sum_witness_common_leftfirstentry * S ((S (pfrep_position_transport_result_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_result) + (pfrep_left_transport_result_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_leftfirstoutside. pfrep_gap_transport_result_sum_witness_common_leftfirstoutside+(pfbz_left_length_transport_result)=(pfrep_power_transport_result_sum_witness_common_left)) /\ (((pfrep_left_transport_result_sum_witness_common_left)=0))))) -> ((exists pfrep_position_transport_result_sum_witness_common_leftsecond. ((pfrep_position_transport_result_sum_witness_common_leftsecond+S (pfrep_power_transport_result_sum_witness_common_left)=(pfaa_length_transport_result_sum)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_leftsecondentry. ff_h_pfp_transport_result_sum_witness_common_leftsecondentry + S (pfrep_right_transport_result_sum_witness_common_left) = S ((S (pfrep_position_transport_result_sum_witness_common_leftsecond)) * pfaa_left_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_common_leftsecondentry. pfaa_left_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_common_leftsecondentry * S ((S (pfrep_position_transport_result_sum_witness_common_leftsecond)) * pfaa_left_c_transport_result_sum) + (pfrep_right_transport_result_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_leftsecondoutside. pfrep_gap_transport_result_sum_witness_common_leftsecondoutside+(pfaa_length_transport_result_sum)=(pfrep_power_transport_result_sum_witness_common_left)) /\ (((pfrep_right_transport_result_sum_witness_common_left)=0))))) -> pfrep_left_transport_result_sum_witness_common_left=pfrep_right_transport_result_sum_witness_common_left) /\ ((forall pfrep_power_transport_result_sum_witness_common_right pfrep_left_transport_result_sum_witness_common_right pfrep_right_transport_result_sum_witness_common_right. ((exists pfrep_position_transport_result_sum_witness_common_rightfirst. ((pfrep_position_transport_result_sum_witness_common_rightfirst+S (pfrep_power_transport_result_sum_witness_common_right)=(pfbz_right_length_transport_result)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_rightfirstentry. ff_h_pfp_transport_result_sum_witness_common_rightfirstentry + S (pfrep_left_transport_result_sum_witness_common_right) = S ((S (pfrep_position_transport_result_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_result)) /\ exists ff_q_pfp_transport_result_sum_witness_common_rightfirstentry. pfbz_right_code_transport_result = ff_q_pfp_transport_result_sum_witness_common_rightfirstentry * S ((S (pfrep_position_transport_result_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_result) + (pfrep_left_transport_result_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_rightfirstoutside. pfrep_gap_transport_result_sum_witness_common_rightfirstoutside+(pfbz_right_length_transport_result)=(pfrep_power_transport_result_sum_witness_common_right)) /\ (((pfrep_left_transport_result_sum_witness_common_right)=0))))) -> ((exists pfrep_position_transport_result_sum_witness_common_rightsecond. ((pfrep_position_transport_result_sum_witness_common_rightsecond+S (pfrep_power_transport_result_sum_witness_common_right)=(pfaa_length_transport_result_sum)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_rightsecondentry. ff_h_pfp_transport_result_sum_witness_common_rightsecondentry + S (pfrep_right_transport_result_sum_witness_common_right) = S ((S (pfrep_position_transport_result_sum_witness_common_rightsecond)) * pfaa_right_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_common_rightsecondentry. pfaa_right_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_common_rightsecondentry * S ((S (pfrep_position_transport_result_sum_witness_common_rightsecond)) * pfaa_right_c_transport_result_sum) + (pfrep_right_transport_result_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_rightsecondoutside. pfrep_gap_transport_result_sum_witness_common_rightsecondoutside+(pfaa_length_transport_result_sum)=(pfrep_power_transport_result_sum_witness_common_right)) /\ (((pfrep_right_transport_result_sum_witness_common_right)=0))))) -> pfrep_left_transport_result_sum_witness_common_right=pfrep_right_transport_result_sum_witness_common_right)))) /\ (((forall pfp_index_transport_result_sum_witness_operation. (exists pfa_gap_transport_result_sum_witness_operationindex. pfa_gap_transport_result_sum_witness_operationindex + S (pfp_index_transport_result_sum_witness_operation) = (pfaa_length_transport_result_sum)) -> exists pfp_left_transport_result_sum_witness_operation pfp_right_transport_result_sum_witness_operation pfp_value_transport_result_sum_witness_operation. ((((exists ff_h_pfp_transport_result_sum_witness_operationleft. ff_h_pfp_transport_result_sum_witness_operationleft + S (pfp_left_transport_result_sum_witness_operation) = S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_left_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_operationleft. pfaa_left_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_operationleft * S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_left_c_transport_result_sum) + (pfp_left_transport_result_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_result_sum_witness_operationright. ff_h_pfp_transport_result_sum_witness_operationright + S (pfp_right_transport_result_sum_witness_operation) = S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_right_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_operationright. pfaa_right_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_operationright * S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_right_c_transport_result_sum) + (pfp_right_transport_result_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_result_sum_witness_operationtarget. ff_h_pfp_transport_result_sum_witness_operationtarget + S (pfp_value_transport_result_sum_witness_operation) = S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_sum_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_operationtarget. pfaa_sum_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_operationtarget * S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_sum_c_transport_result_sum) + (pfp_value_transport_result_sum_witness_operation))) /\ ((((exists pfa_gap_transport_result_sum_witness_operationoperationleft. pfa_gap_transport_result_sum_witness_operationoperationleft + S (pfp_left_transport_result_sum_witness_operation) = (p)) /\ (((exists pfa_gap_transport_result_sum_witness_operationoperationright. pfa_gap_transport_result_sum_witness_operationoperationright + S (pfp_right_transport_result_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_transport_result_sum_witness_operationoperationresultbound. pfa_gap_transport_result_sum_witness_operationoperationresultbound + S (pfp_value_transport_result_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_transport_result_sum_witness_operationoperationresultcongruence pfa_offset_right_transport_result_sum_witness_operationoperationresultcongruence. ((pfp_left_transport_result_sum_witness_operation) + (pfp_right_transport_result_sum_witness_operation)) + (p) * pfa_offset_left_transport_result_sum_witness_operationoperationresultcongruence = (pfp_value_transport_result_sum_witness_operation) + (p) * pfa_offset_right_transport_result_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_transport_result_sum_witness_output pfrep_left_transport_result_sum_witness_output pfrep_right_transport_result_sum_witness_output. ((exists pfrep_position_transport_result_sum_witness_outputfirst. ((pfrep_position_transport_result_sum_witness_outputfirst+S (pfrep_power_transport_result_sum_witness_output)=(pfaa_length_transport_result_sum)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_outputfirstentry. ff_h_pfp_transport_result_sum_witness_outputfirstentry + S (pfrep_left_transport_result_sum_witness_output) = S ((S (pfrep_position_transport_result_sum_witness_outputfirst)) * pfaa_sum_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_outputfirstentry. pfaa_sum_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_outputfirstentry * S ((S (pfrep_position_transport_result_sum_witness_outputfirst)) * pfaa_sum_c_transport_result_sum) + (pfrep_left_transport_result_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_outputfirstoutside. pfrep_gap_transport_result_sum_witness_outputfirstoutside+(pfaa_length_transport_result_sum)=(pfrep_power_transport_result_sum_witness_output)) /\ (((pfrep_left_transport_result_sum_witness_output)=0))))) -> ((exists pfrep_position_transport_result_sum_witness_outputsecond. ((pfrep_position_transport_result_sum_witness_outputsecond+S (pfrep_power_transport_result_sum_witness_output)=(G2)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_outputsecondentry. ff_h_pfp_transport_result_sum_witness_outputsecondentry + S (pfrep_right_transport_result_sum_witness_output) = S ((S (pfrep_position_transport_result_sum_witness_outputsecond)) * gc2)) /\ exists ff_q_pfp_transport_result_sum_witness_outputsecondentry. gb2 = ff_q_pfp_transport_result_sum_witness_outputsecondentry * S ((S (pfrep_position_transport_result_sum_witness_outputsecond)) * gc2) + (pfrep_right_transport_result_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_outputsecondoutside. pfrep_gap_transport_result_sum_witness_outputsecondoutside+(G2)=(pfrep_power_transport_result_sum_witness_output)) /\ (((pfrep_right_transport_result_sum_witness_output)=0))))) -> pfrep_left_transport_result_sum_witness_output=pfrep_right_transport_result_sum_witness_output))))))))))))))))))