prime_field_polynomial_division_execution_bezout_backward

forall p ab ac La bb bc d qb qc Lq rb rc Lr gb gc Lg ub uc Lu vb vc Lv. (~((p) = 1) /\ forall pfa_factor_left_execution_backward_prime pfa_factor_right_execution_backward_prime. (p) = pfa_factor_left_execution_backward_prime * pfa_factor_right_execution_backward_prime -> pfa_factor_left_execution_backward_prime = 1 \/ pfa_factor_right_execution_backward_prime = 1) -> (((forall fom_index_pfp_execution_backward_actualinput. (exists fom_gap_pfp_execution_backward_actualinput_index_bound. fom_gap_pfp_execution_backward_actualinput_index_bound + S (fom_index_pfp_execution_backward_actualinput) = La) -> exists fom_value_pfp_execution_backward_actualinput. ((((exists fom_beta_height_pfp_execution_backward_actualinput_entry. fom_beta_height_pfp_execution_backward_actualinput_entry + S (fom_value_pfp_execution_backward_actualinput) = S ((S (fom_index_pfp_execution_backward_actualinput)) * ac)) /\ exists fom_beta_quotient_pfp_execution_backward_actualinput_entry. ab = fom_beta_quotient_pfp_execution_backward_actualinput_entry * S ((S (fom_index_pfp_execution_backward_actualinput)) * ac) + (fom_value_pfp_execution_backward_actualinput))) /\ (exists fom_gap_pfp_execution_backward_actualinput_value_bound. fom_gap_pfp_execution_backward_actualinput_value_bound + S (fom_value_pfp_execution_backward_actualinput) = p))) /\ (((forall fom_index_pfp_execution_backward_actualdivisor. (exists fom_gap_pfp_execution_backward_actualdivisor_index_bound. fom_gap_pfp_execution_backward_actualdivisor_index_bound + S (fom_index_pfp_execution_backward_actualdivisor) = S (d)) -> exists fom_value_pfp_execution_backward_actualdivisor. ((((exists fom_beta_height_pfp_execution_backward_actualdivisor_entry. fom_beta_height_pfp_execution_backward_actualdivisor_entry + S (fom_value_pfp_execution_backward_actualdivisor) = S ((S (fom_index_pfp_execution_backward_actualdivisor)) * bc)) /\ exists fom_beta_quotient_pfp_execution_backward_actualdivisor_entry. bb = fom_beta_quotient_pfp_execution_backward_actualdivisor_entry * S ((S (fom_index_pfp_execution_backward_actualdivisor)) * bc) + (fom_value_pfp_execution_backward_actualdivisor))) /\ (exists fom_gap_pfp_execution_backward_actualdivisor_value_bound. fom_gap_pfp_execution_backward_actualdivisor_value_bound + S (fom_value_pfp_execution_backward_actualdivisor) = p))) /\ (((((((Lq)=0) /\ ((exists pfc_gap_execution_backward_actuallengthshort. pfc_gap_execution_backward_actuallengthshort+(La)=(d))))) \/ (((~((Lq)=0)) /\ (((Lq)+(d)=(La)))))) /\ ((exists pfd_head_execution_backward_actual pfd_inverse_execution_backward_actual pfd_product_code_execution_backward_actual pfd_product_scale_execution_backward_actual pfd_residual_code_execution_backward_actual pfd_residual_scale_execution_backward_actual pfd_cut_execution_backward_actual. ((((exists ff_h_pfp_execution_backward_actualhead. ff_h_pfp_execution_backward_actualhead + S (pfd_head_execution_backward_actual) = S ((S (0)) * bc)) /\ exists ff_q_pfp_execution_backward_actualhead. bb = ff_q_pfp_execution_backward_actualhead * S ((S (0)) * bc) + (pfd_head_execution_backward_actual))) /\ (((((~((pfd_head_execution_backward_actual) = 0)) /\ ((((exists pfa_gap_execution_backward_actualinversemultiplicationleft. pfa_gap_execution_backward_actualinversemultiplicationleft + S (pfd_head_execution_backward_actual) = (p)) /\ (((exists pfa_gap_execution_backward_actualinversemultiplicationright. pfa_gap_execution_backward_actualinversemultiplicationright + S (pfd_inverse_execution_backward_actual) = (p)) /\ ((((exists pfa_gap_execution_backward_actualinversemultiplicationresultbound. pfa_gap_execution_backward_actualinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_execution_backward_actualinversemultiplicationresultcongruence pfa_offset_right_execution_backward_actualinversemultiplicationresultcongruence. ((pfd_head_execution_backward_actual) * (pfd_inverse_execution_backward_actual)) + (p) * pfa_offset_left_execution_backward_actualinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_execution_backward_actualinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_execution_backward_actualquotient. (exists pfa_gap_execution_backward_actualquotientbound. pfa_gap_execution_backward_actualquotientbound + S (pfd_index_execution_backward_actualquotient) = (Lq)) -> exists pfd_value_execution_backward_actualquotient. ((((exists ff_h_pfp_execution_backward_actualquotiententry. ff_h_pfp_execution_backward_actualquotiententry + S (pfd_value_execution_backward_actualquotient) = S ((S (pfd_index_execution_backward_actualquotient)) * qc)) /\ exists ff_q_pfp_execution_backward_actualquotiententry. qb = ff_q_pfp_execution_backward_actualquotiententry * S ((S (pfd_index_execution_backward_actualquotient)) * qc) + (pfd_value_execution_backward_actualquotient))) /\ ((exists pfd_input_execution_backward_actualquotientstep pfd_previous_execution_backward_actualquotientstep pfd_difference_execution_backward_actualquotientstep. ((((exists ff_h_pfp_execution_backward_actualquotientstepinput. ff_h_pfp_execution_backward_actualquotientstepinput + S (pfd_input_execution_backward_actualquotientstep) = S ((S (pfd_index_execution_backward_actualquotient)) * ac)) /\ exists ff_q_pfp_execution_backward_actualquotientstepinput. ab = ff_q_pfp_execution_backward_actualquotientstepinput * S ((S (pfd_index_execution_backward_actualquotient)) * ac) + (pfd_input_execution_backward_actualquotientstep))) /\ (((exists pfc_terms_code_execution_backward_actualquotientstepprevious pfc_terms_scale_execution_backward_actualquotientstepprevious pfc_natural_sum_execution_backward_actualquotientstepprevious. ((forall pfc_index_execution_backward_actualquotientsteppreviousdiagonal. (exists pfa_gap_execution_backward_actualquotientsteppreviousdiagonalbound. pfa_gap_execution_backward_actualquotientsteppreviousdiagonalbound + S (pfc_index_execution_backward_actualquotientsteppreviousdiagonal) = (S (pfd_index_execution_backward_actualquotient))) -> exists pfc_value_execution_backward_actualquotientsteppreviousdiagonal. ((((exists ff_h_pfp_execution_backward_actualquotientsteppreviousdiagonalentry. ff_h_pfp_execution_backward_actualquotientsteppreviousdiagonalentry + S (pfc_value_execution_backward_actualquotientsteppreviousdiagonal) = S ((S (pfc_index_execution_backward_actualquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_backward_actualquotientstepprevious)) /\ exists ff_q_pfp_execution_backward_actualquotientsteppreviousdiagonalentry. pfc_terms_code_execution_backward_actualquotientstepprevious = ff_q_pfp_execution_backward_actualquotientsteppreviousdiagonalentry * S ((S (pfc_index_execution_backward_actualquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_backward_actualquotientstepprevious) + (pfc_value_execution_backward_actualquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_execution_backward_actualquotientsteppreviousdiagonalterm pfc_left_execution_backward_actualquotientsteppreviousdiagonalterm pfc_right_execution_backward_actualquotientsteppreviousdiagonalterm. (((pfc_index_execution_backward_actualquotientsteppreviousdiagonal)+pfc_complement_execution_backward_actualquotientsteppreviousdiagonalterm=(pfd_index_execution_backward_actualquotient)) /\ ((((((exists pfa_gap_execution_backward_actualquotientsteppreviousdiagonaltermleftinside. pfa_gap_execution_backward_actualquotientsteppreviousdiagonaltermleftinside + S (pfc_index_execution_backward_actualquotientsteppreviousdiagonal) = (pfd_index_execution_backward_actualquotient)) /\ ((((exists ff_h_pfp_execution_backward_actualquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_execution_backward_actualquotientsteppreviousdiagonaltermleftentry + S (pfc_left_execution_backward_actualquotientsteppreviousdiagonalterm) = S ((S (pfc_index_execution_backward_actualquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_execution_backward_actualquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_execution_backward_actualquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_execution_backward_actualquotientsteppreviousdiagonal)) * qc) + (pfc_left_execution_backward_actualquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_actualquotientsteppreviousdiagonaltermleftoutside. pfc_gap_execution_backward_actualquotientsteppreviousdiagonaltermleftoutside+(pfd_index_execution_backward_actualquotient)=(pfc_index_execution_backward_actualquotientsteppreviousdiagonal)) /\ (((pfc_left_execution_backward_actualquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_actualquotientsteppreviousdiagonaltermrightinside. pfa_gap_execution_backward_actualquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_execution_backward_actualquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_backward_actualquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_execution_backward_actualquotientsteppreviousdiagonaltermrightentry + S (pfc_right_execution_backward_actualquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_execution_backward_actualquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_backward_actualquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_execution_backward_actualquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_actualquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_execution_backward_actualquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_actualquotientsteppreviousdiagonaltermrightoutside. pfc_gap_execution_backward_actualquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_backward_actualquotientsteppreviousdiagonalterm)) /\ (((pfc_right_execution_backward_actualquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_actualquotientsteppreviousdiagonal)=pfc_left_execution_backward_actualquotientsteppreviousdiagonalterm*pfc_right_execution_backward_actualquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_actualquotientstepprevioussum fs_v_pfc_execution_backward_actualquotientstepprevioussum. ((((exists fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_start. fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_start. fs_u_pfc_execution_backward_actualquotientstepprevioussum = fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_actualquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_terminal. fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_terminal + S (pfc_natural_sum_execution_backward_actualquotientstepprevious) = S ((S (S (pfd_index_execution_backward_actualquotient))) * fs_v_pfc_execution_backward_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_terminal. fs_u_pfc_execution_backward_actualquotientstepprevioussum = fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_execution_backward_actualquotient))) * fs_v_pfc_execution_backward_actualquotientstepprevioussum) + (pfc_natural_sum_execution_backward_actualquotientstepprevious))) /\ forall fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps. (exists fs_lt_pfc_execution_backward_actualquotientstepprevioussum_body_steps_bound. fs_lt_pfc_execution_backward_actualquotientstepprevioussum_body_steps_bound + S fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps = S (pfd_index_execution_backward_actualquotient)) -> exists fs_a_pfc_execution_backward_actualquotientstepprevioussum_body_steps fs_r_pfc_execution_backward_actualquotientstepprevioussum_body_steps fs_s_pfc_execution_backward_actualquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_steps_summand. fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_execution_backward_actualquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_backward_actualquotientstepprevious)) /\ exists fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_steps_summand. pfc_terms_code_execution_backward_actualquotientstepprevious = fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_backward_actualquotientstepprevious) + (fs_a_pfc_execution_backward_actualquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_steps_partial. fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_execution_backward_actualquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_backward_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_steps_partial. fs_u_pfc_execution_backward_actualquotientstepprevioussum = fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_backward_actualquotientstepprevioussum) + (fs_r_pfc_execution_backward_actualquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_steps_successor. fs_h_pfc_execution_backward_actualquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_execution_backward_actualquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_backward_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_steps_successor. fs_u_pfc_execution_backward_actualquotientstepprevioussum = fs_q_pfc_execution_backward_actualquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_backward_actualquotientstepprevioussum) + (fs_s_pfc_execution_backward_actualquotientstepprevioussum_body_steps))) /\ fs_s_pfc_execution_backward_actualquotientstepprevioussum_body_steps = fs_r_pfc_execution_backward_actualquotientstepprevioussum_body_steps + fs_a_pfc_execution_backward_actualquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_actualquotientsteppreviousresiduebound. pfa_gap_execution_backward_actualquotientsteppreviousresiduebound + S (pfd_previous_execution_backward_actualquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_backward_actualquotientsteppreviousresiduecongruence pfa_offset_right_execution_backward_actualquotientsteppreviousresiduecongruence. (pfc_natural_sum_execution_backward_actualquotientstepprevious) + (p) * pfa_offset_left_execution_backward_actualquotientsteppreviousresiduecongruence = (pfd_previous_execution_backward_actualquotientstep) + (p) * pfa_offset_right_execution_backward_actualquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_execution_backward_actualquotientstepsubtractleft. pfa_gap_execution_backward_actualquotientstepsubtractleft + S (pfd_previous_execution_backward_actualquotientstep) = (p)) /\ (((exists pfa_gap_execution_backward_actualquotientstepsubtractright. pfa_gap_execution_backward_actualquotientstepsubtractright + S (pfd_difference_execution_backward_actualquotientstep) = (p)) /\ ((((exists pfa_gap_execution_backward_actualquotientstepsubtractresultbound. pfa_gap_execution_backward_actualquotientstepsubtractresultbound + S (pfd_input_execution_backward_actualquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_backward_actualquotientstepsubtractresultcongruence pfa_offset_right_execution_backward_actualquotientstepsubtractresultcongruence. ((pfd_previous_execution_backward_actualquotientstep) + (pfd_difference_execution_backward_actualquotientstep)) + (p) * pfa_offset_left_execution_backward_actualquotientstepsubtractresultcongruence = (pfd_input_execution_backward_actualquotientstep) + (p) * pfa_offset_right_execution_backward_actualquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_execution_backward_actualquotientstepmultiplyleft. pfa_gap_execution_backward_actualquotientstepmultiplyleft + S (pfd_inverse_execution_backward_actual) = (p)) /\ (((exists pfa_gap_execution_backward_actualquotientstepmultiplyright. pfa_gap_execution_backward_actualquotientstepmultiplyright + S (pfd_difference_execution_backward_actualquotientstep) = (p)) /\ ((((exists pfa_gap_execution_backward_actualquotientstepmultiplyresultbound. pfa_gap_execution_backward_actualquotientstepmultiplyresultbound + S (pfd_value_execution_backward_actualquotient) = (p)) /\ ((exists pfa_offset_left_execution_backward_actualquotientstepmultiplyresultcongruence pfa_offset_right_execution_backward_actualquotientstepmultiplyresultcongruence. ((pfd_inverse_execution_backward_actual) * (pfd_difference_execution_backward_actualquotientstep)) + (p) * pfa_offset_left_execution_backward_actualquotientstepmultiplyresultcongruence = (pfd_value_execution_backward_actualquotient) + (p) * pfa_offset_right_execution_backward_actualquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_execution_backward_actualproduct. (exists pfa_gap_execution_backward_actualproductbound. pfa_gap_execution_backward_actualproductbound + S (pfc_index_execution_backward_actualproduct) = (La)) -> exists pfc_value_execution_backward_actualproduct. ((((exists ff_h_pfp_execution_backward_actualproductentry. ff_h_pfp_execution_backward_actualproductentry + S (pfc_value_execution_backward_actualproduct) = S ((S (pfc_index_execution_backward_actualproduct)) * pfd_product_scale_execution_backward_actual)) /\ exists ff_q_pfp_execution_backward_actualproductentry. pfd_product_code_execution_backward_actual = ff_q_pfp_execution_backward_actualproductentry * S ((S (pfc_index_execution_backward_actualproduct)) * pfd_product_scale_execution_backward_actual) + (pfc_value_execution_backward_actualproduct))) /\ ((exists pfc_terms_code_execution_backward_actualproductcoefficient pfc_terms_scale_execution_backward_actualproductcoefficient pfc_natural_sum_execution_backward_actualproductcoefficient. ((forall pfc_index_execution_backward_actualproductcoefficientdiagonal. (exists pfa_gap_execution_backward_actualproductcoefficientdiagonalbound. pfa_gap_execution_backward_actualproductcoefficientdiagonalbound + S (pfc_index_execution_backward_actualproductcoefficientdiagonal) = (S (pfc_index_execution_backward_actualproduct))) -> exists pfc_value_execution_backward_actualproductcoefficientdiagonal. ((((exists ff_h_pfp_execution_backward_actualproductcoefficientdiagonalentry. ff_h_pfp_execution_backward_actualproductcoefficientdiagonalentry + S (pfc_value_execution_backward_actualproductcoefficientdiagonal) = S ((S (pfc_index_execution_backward_actualproductcoefficientdiagonal)) * pfc_terms_scale_execution_backward_actualproductcoefficient)) /\ exists ff_q_pfp_execution_backward_actualproductcoefficientdiagonalentry. pfc_terms_code_execution_backward_actualproductcoefficient = ff_q_pfp_execution_backward_actualproductcoefficientdiagonalentry * S ((S (pfc_index_execution_backward_actualproductcoefficientdiagonal)) * pfc_terms_scale_execution_backward_actualproductcoefficient) + (pfc_value_execution_backward_actualproductcoefficientdiagonal))) /\ ((exists pfc_complement_execution_backward_actualproductcoefficientdiagonalterm pfc_left_execution_backward_actualproductcoefficientdiagonalterm pfc_right_execution_backward_actualproductcoefficientdiagonalterm. (((pfc_index_execution_backward_actualproductcoefficientdiagonal)+pfc_complement_execution_backward_actualproductcoefficientdiagonalterm=(pfc_index_execution_backward_actualproduct)) /\ ((((((exists pfa_gap_execution_backward_actualproductcoefficientdiagonaltermleftinside. pfa_gap_execution_backward_actualproductcoefficientdiagonaltermleftinside + S (pfc_index_execution_backward_actualproductcoefficientdiagonal) = (Lq)) /\ ((((exists ff_h_pfp_execution_backward_actualproductcoefficientdiagonaltermleftentry. ff_h_pfp_execution_backward_actualproductcoefficientdiagonaltermleftentry + S (pfc_left_execution_backward_actualproductcoefficientdiagonalterm) = S ((S (pfc_index_execution_backward_actualproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_execution_backward_actualproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_execution_backward_actualproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_backward_actualproductcoefficientdiagonal)) * qc) + (pfc_left_execution_backward_actualproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_actualproductcoefficientdiagonaltermleftoutside. pfc_gap_execution_backward_actualproductcoefficientdiagonaltermleftoutside+(Lq)=(pfc_index_execution_backward_actualproductcoefficientdiagonal)) /\ (((pfc_left_execution_backward_actualproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_actualproductcoefficientdiagonaltermrightinside. pfa_gap_execution_backward_actualproductcoefficientdiagonaltermrightinside + S (pfc_complement_execution_backward_actualproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_backward_actualproductcoefficientdiagonaltermrightentry. ff_h_pfp_execution_backward_actualproductcoefficientdiagonaltermrightentry + S (pfc_right_execution_backward_actualproductcoefficientdiagonalterm) = S ((S (pfc_complement_execution_backward_actualproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_backward_actualproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_backward_actualproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_actualproductcoefficientdiagonalterm)) * bc) + (pfc_right_execution_backward_actualproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_actualproductcoefficientdiagonaltermrightoutside. pfc_gap_execution_backward_actualproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_backward_actualproductcoefficientdiagonalterm)) /\ (((pfc_right_execution_backward_actualproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_actualproductcoefficientdiagonal)=pfc_left_execution_backward_actualproductcoefficientdiagonalterm*pfc_right_execution_backward_actualproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_actualproductcoefficientsum fs_v_pfc_execution_backward_actualproductcoefficientsum. ((((exists fs_h_pfc_execution_backward_actualproductcoefficientsum_body_start. fs_h_pfc_execution_backward_actualproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_backward_actualproductcoefficientsum_body_start. fs_u_pfc_execution_backward_actualproductcoefficientsum = fs_q_pfc_execution_backward_actualproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_actualproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_actualproductcoefficientsum_body_terminal. fs_h_pfc_execution_backward_actualproductcoefficientsum_body_terminal + S (pfc_natural_sum_execution_backward_actualproductcoefficient) = S ((S (S (pfc_index_execution_backward_actualproduct))) * fs_v_pfc_execution_backward_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_backward_actualproductcoefficientsum_body_terminal. fs_u_pfc_execution_backward_actualproductcoefficientsum = fs_q_pfc_execution_backward_actualproductcoefficientsum_body_terminal * S ((S (S (pfc_index_execution_backward_actualproduct))) * fs_v_pfc_execution_backward_actualproductcoefficientsum) + (pfc_natural_sum_execution_backward_actualproductcoefficient))) /\ forall fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps. (exists fs_lt_pfc_execution_backward_actualproductcoefficientsum_body_steps_bound. fs_lt_pfc_execution_backward_actualproductcoefficientsum_body_steps_bound + S fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps = S (pfc_index_execution_backward_actualproduct)) -> exists fs_a_pfc_execution_backward_actualproductcoefficientsum_body_steps fs_r_pfc_execution_backward_actualproductcoefficientsum_body_steps fs_s_pfc_execution_backward_actualproductcoefficientsum_body_steps. ((((exists fs_h_pfc_execution_backward_actualproductcoefficientsum_body_steps_summand. fs_h_pfc_execution_backward_actualproductcoefficientsum_body_steps_summand + S (fs_a_pfc_execution_backward_actualproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_actualproductcoefficient)) /\ exists fs_q_pfc_execution_backward_actualproductcoefficientsum_body_steps_summand. pfc_terms_code_execution_backward_actualproductcoefficient = fs_q_pfc_execution_backward_actualproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_actualproductcoefficient) + (fs_a_pfc_execution_backward_actualproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_actualproductcoefficientsum_body_steps_partial. fs_h_pfc_execution_backward_actualproductcoefficientsum_body_steps_partial + S (fs_r_pfc_execution_backward_actualproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_backward_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_backward_actualproductcoefficientsum_body_steps_partial. fs_u_pfc_execution_backward_actualproductcoefficientsum = fs_q_pfc_execution_backward_actualproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_backward_actualproductcoefficientsum) + (fs_r_pfc_execution_backward_actualproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_actualproductcoefficientsum_body_steps_successor. fs_h_pfc_execution_backward_actualproductcoefficientsum_body_steps_successor + S (fs_s_pfc_execution_backward_actualproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_backward_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_backward_actualproductcoefficientsum_body_steps_successor. fs_u_pfc_execution_backward_actualproductcoefficientsum = fs_q_pfc_execution_backward_actualproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_backward_actualproductcoefficientsum) + (fs_s_pfc_execution_backward_actualproductcoefficientsum_body_steps))) /\ fs_s_pfc_execution_backward_actualproductcoefficientsum_body_steps = fs_r_pfc_execution_backward_actualproductcoefficientsum_body_steps + fs_a_pfc_execution_backward_actualproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_actualproductcoefficientresiduebound. pfa_gap_execution_backward_actualproductcoefficientresiduebound + S (pfc_value_execution_backward_actualproduct) = (p)) /\ ((exists pfa_offset_left_execution_backward_actualproductcoefficientresiduecongruence pfa_offset_right_execution_backward_actualproductcoefficientresiduecongruence. (pfc_natural_sum_execution_backward_actualproductcoefficient) + (p) * pfa_offset_left_execution_backward_actualproductcoefficientresiduecongruence = (pfc_value_execution_backward_actualproduct) + (p) * pfa_offset_right_execution_backward_actualproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_execution_backward_actualdifference. (exists pfa_gap_execution_backward_actualdifferenceindex. pfa_gap_execution_backward_actualdifferenceindex + S (pfs_index_execution_backward_actualdifference) = (La)) -> exists pfs_left_execution_backward_actualdifference pfs_right_execution_backward_actualdifference pfs_result_execution_backward_actualdifference. ((((exists ff_h_pfp_execution_backward_actualdifferenceleft. ff_h_pfp_execution_backward_actualdifferenceleft + S (pfs_left_execution_backward_actualdifference) = S ((S (pfs_index_execution_backward_actualdifference)) * ac)) /\ exists ff_q_pfp_execution_backward_actualdifferenceleft. ab = ff_q_pfp_execution_backward_actualdifferenceleft * S ((S (pfs_index_execution_backward_actualdifference)) * ac) + (pfs_left_execution_backward_actualdifference))) /\ (((((exists ff_h_pfp_execution_backward_actualdifferenceright. ff_h_pfp_execution_backward_actualdifferenceright + S (pfs_right_execution_backward_actualdifference) = S ((S (pfs_index_execution_backward_actualdifference)) * pfd_product_scale_execution_backward_actual)) /\ exists ff_q_pfp_execution_backward_actualdifferenceright. pfd_product_code_execution_backward_actual = ff_q_pfp_execution_backward_actualdifferenceright * S ((S (pfs_index_execution_backward_actualdifference)) * pfd_product_scale_execution_backward_actual) + (pfs_right_execution_backward_actualdifference))) /\ (((((exists ff_h_pfp_execution_backward_actualdifferenceresult. ff_h_pfp_execution_backward_actualdifferenceresult + S (pfs_result_execution_backward_actualdifference) = S ((S (pfs_index_execution_backward_actualdifference)) * pfd_residual_scale_execution_backward_actual)) /\ exists ff_q_pfp_execution_backward_actualdifferenceresult. pfd_residual_code_execution_backward_actual = ff_q_pfp_execution_backward_actualdifferenceresult * S ((S (pfs_index_execution_backward_actualdifference)) * pfd_residual_scale_execution_backward_actual) + (pfs_result_execution_backward_actualdifference))) /\ ((((exists pfa_gap_execution_backward_actualdifferenceoperationleft. pfa_gap_execution_backward_actualdifferenceoperationleft + S (pfs_right_execution_backward_actualdifference) = (p)) /\ (((exists pfa_gap_execution_backward_actualdifferenceoperationright. pfa_gap_execution_backward_actualdifferenceoperationright + S (pfs_result_execution_backward_actualdifference) = (p)) /\ ((((exists pfa_gap_execution_backward_actualdifferenceoperationresultbound. pfa_gap_execution_backward_actualdifferenceoperationresultbound + S (pfs_left_execution_backward_actualdifference) = (p)) /\ ((exists pfa_offset_left_execution_backward_actualdifferenceoperationresultcongruence pfa_offset_right_execution_backward_actualdifferenceoperationresultcongruence. ((pfs_right_execution_backward_actualdifference) + (pfs_result_execution_backward_actualdifference)) + (p) * pfa_offset_left_execution_backward_actualdifferenceoperationresultcongruence = (pfs_left_execution_backward_actualdifference) + (p) * pfa_offset_right_execution_backward_actualdifferenceoperationresultcongruence)))))))))))))))) /\ (((((La)=(pfd_cut_execution_backward_actual)+(Lr)) /\ (((forall fom_index_pfp_execution_backward_actualtriminput. (exists fom_gap_pfp_execution_backward_actualtriminput_index_bound. fom_gap_pfp_execution_backward_actualtriminput_index_bound + S (fom_index_pfp_execution_backward_actualtriminput) = La) -> exists fom_value_pfp_execution_backward_actualtriminput. ((((exists fom_beta_height_pfp_execution_backward_actualtriminput_entry. fom_beta_height_pfp_execution_backward_actualtriminput_entry + S (fom_value_pfp_execution_backward_actualtriminput) = S ((S (fom_index_pfp_execution_backward_actualtriminput)) * pfd_residual_scale_execution_backward_actual)) /\ exists fom_beta_quotient_pfp_execution_backward_actualtriminput_entry. pfd_residual_code_execution_backward_actual = fom_beta_quotient_pfp_execution_backward_actualtriminput_entry * S ((S (fom_index_pfp_execution_backward_actualtriminput)) * pfd_residual_scale_execution_backward_actual) + (fom_value_pfp_execution_backward_actualtriminput))) /\ (exists fom_gap_pfp_execution_backward_actualtriminput_value_bound. fom_gap_pfp_execution_backward_actualtriminput_value_bound + S (fom_value_pfp_execution_backward_actualtriminput) = p))) /\ (((forall pfp_repeat_index_execution_backward_actualtrimremoved. (exists pfa_gap_execution_backward_actualtrimremovedindex. pfa_gap_execution_backward_actualtrimremovedindex + S (pfp_repeat_index_execution_backward_actualtrimremoved) = (pfd_cut_execution_backward_actual)) -> (((exists ff_h_pfp_execution_backward_actualtrimremovedentry. ff_h_pfp_execution_backward_actualtrimremovedentry + S (0) = S ((S (pfp_repeat_index_execution_backward_actualtrimremoved)) * pfd_residual_scale_execution_backward_actual)) /\ exists ff_q_pfp_execution_backward_actualtrimremovedentry. pfd_residual_code_execution_backward_actual = ff_q_pfp_execution_backward_actualtrimremovedentry * S ((S (pfp_repeat_index_execution_backward_actualtrimremoved)) * pfd_residual_scale_execution_backward_actual) + (0)))) /\ (((forall pftrim_index_execution_backward_actualtrimsuffix pftrim_value_execution_backward_actualtrimsuffix. (exists pfa_gap_execution_backward_actualtrimsuffixbound. pfa_gap_execution_backward_actualtrimsuffixbound + S (pftrim_index_execution_backward_actualtrimsuffix) = (Lr)) -> (((exists ff_h_pfp_execution_backward_actualtrimsuffixsource. ff_h_pfp_execution_backward_actualtrimsuffixsource + S (pftrim_value_execution_backward_actualtrimsuffix) = S ((S ((pfd_cut_execution_backward_actual)+pftrim_index_execution_backward_actualtrimsuffix)) * pfd_residual_scale_execution_backward_actual)) /\ exists ff_q_pfp_execution_backward_actualtrimsuffixsource. pfd_residual_code_execution_backward_actual = ff_q_pfp_execution_backward_actualtrimsuffixsource * S ((S ((pfd_cut_execution_backward_actual)+pftrim_index_execution_backward_actualtrimsuffix)) * pfd_residual_scale_execution_backward_actual) + (pftrim_value_execution_backward_actualtrimsuffix))) -> (((exists ff_h_pfp_execution_backward_actualtrimsuffixoutput. ff_h_pfp_execution_backward_actualtrimsuffixoutput + S (pftrim_value_execution_backward_actualtrimsuffix) = S ((S (pftrim_index_execution_backward_actualtrimsuffix)) * rc)) /\ exists ff_q_pfp_execution_backward_actualtrimsuffixoutput. rb = ff_q_pfp_execution_backward_actualtrimsuffixoutput * S ((S (pftrim_index_execution_backward_actualtrimsuffix)) * rc) + (pftrim_value_execution_backward_actualtrimsuffix)))) /\ (((Lr)=0 \/ (exists pftrim_leading_execution_backward_actualtrimnormal. ((((exists ff_h_pfp_execution_backward_actualtrimnormalentry. ff_h_pfp_execution_backward_actualtrimnormalentry + S (pftrim_leading_execution_backward_actualtrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_execution_backward_actualtrimnormalentry. rb = ff_q_pfp_execution_backward_actualtrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_execution_backward_actualtrimnormal))) /\ ((~(pftrim_leading_execution_backward_actualtrimnormal=0))))))))))))))))))))))))))))))))) -> (exists pfbz_left_code_execution_backward_original pfbz_left_scale_execution_backward_original pfbz_left_length_execution_backward_original pfbz_right_code_execution_backward_original pfbz_right_scale_execution_backward_original pfbz_right_length_execution_backward_original. ((((forall fom_index_pfp_execution_backward_original_left_productleft. (exists fom_gap_pfp_execution_backward_original_left_productleft_index_bound. fom_gap_pfp_execution_backward_original_left_productleft_index_bound + S (fom_index_pfp_execution_backward_original_left_productleft) = Lu) -> exists fom_value_pfp_execution_backward_original_left_productleft. ((((exists fom_beta_height_pfp_execution_backward_original_left_productleft_entry. fom_beta_height_pfp_execution_backward_original_left_productleft_entry + S (fom_value_pfp_execution_backward_original_left_productleft) = S ((S (fom_index_pfp_execution_backward_original_left_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_execution_backward_original_left_productleft_entry. ub = fom_beta_quotient_pfp_execution_backward_original_left_productleft_entry * S ((S (fom_index_pfp_execution_backward_original_left_productleft)) * uc) + (fom_value_pfp_execution_backward_original_left_productleft))) /\ (exists fom_gap_pfp_execution_backward_original_left_productleft_value_bound. fom_gap_pfp_execution_backward_original_left_productleft_value_bound + S (fom_value_pfp_execution_backward_original_left_productleft) = p))) /\ (((forall fom_index_pfp_execution_backward_original_left_productright. (exists fom_gap_pfp_execution_backward_original_left_productright_index_bound. fom_gap_pfp_execution_backward_original_left_productright_index_bound + S (fom_index_pfp_execution_backward_original_left_productright) = S d) -> exists fom_value_pfp_execution_backward_original_left_productright. ((((exists fom_beta_height_pfp_execution_backward_original_left_productright_entry. fom_beta_height_pfp_execution_backward_original_left_productright_entry + S (fom_value_pfp_execution_backward_original_left_productright) = S ((S (fom_index_pfp_execution_backward_original_left_productright)) * bc)) /\ exists fom_beta_quotient_pfp_execution_backward_original_left_productright_entry. bb = fom_beta_quotient_pfp_execution_backward_original_left_productright_entry * S ((S (fom_index_pfp_execution_backward_original_left_productright)) * bc) + (fom_value_pfp_execution_backward_original_left_productright))) /\ (exists fom_gap_pfp_execution_backward_original_left_productright_value_bound. fom_gap_pfp_execution_backward_original_left_productright_value_bound + S (fom_value_pfp_execution_backward_original_left_productright) = p))) /\ (((((((Lu)=0 \/ (S d)=0) /\ (((pfbz_left_length_execution_backward_original)=0)))) \/ (((~((Lu)=0)) /\ (((~((S d)=0)) /\ (((Lu)+(S d)=S (pfbz_left_length_execution_backward_original)))))))) /\ ((forall pfc_index_execution_backward_original_left_productcoefficients. (exists pfa_gap_execution_backward_original_left_productcoefficientsbound. pfa_gap_execution_backward_original_left_productcoefficientsbound + S (pfc_index_execution_backward_original_left_productcoefficients) = (pfbz_left_length_execution_backward_original)) -> exists pfc_value_execution_backward_original_left_productcoefficients. ((((exists ff_h_pfp_execution_backward_original_left_productcoefficientsentry. ff_h_pfp_execution_backward_original_left_productcoefficientsentry + S (pfc_value_execution_backward_original_left_productcoefficients) = S ((S (pfc_index_execution_backward_original_left_productcoefficients)) * pfbz_left_scale_execution_backward_original)) /\ exists ff_q_pfp_execution_backward_original_left_productcoefficientsentry. pfbz_left_code_execution_backward_original = ff_q_pfp_execution_backward_original_left_productcoefficientsentry * S ((S (pfc_index_execution_backward_original_left_productcoefficients)) * pfbz_left_scale_execution_backward_original) + (pfc_value_execution_backward_original_left_productcoefficients))) /\ ((exists pfc_terms_code_execution_backward_original_left_productcoefficientscoefficient pfc_terms_scale_execution_backward_original_left_productcoefficientscoefficient pfc_natural_sum_execution_backward_original_left_productcoefficientscoefficient. ((forall pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_backward_original_left_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_backward_original_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_backward_original_left_productcoefficients))) -> exists pfc_value_execution_backward_original_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_backward_original_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_original_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_backward_original_left_productcoefficientscoefficient = ff_q_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_original_left_productcoefficientscoefficient) + (pfc_value_execution_backward_original_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_backward_original_left_productcoefficientscoefficientdiagonalterm pfc_left_execution_backward_original_left_productcoefficientscoefficientdiagonalterm pfc_right_execution_backward_original_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal)+pfc_complement_execution_backward_original_left_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_backward_original_left_productcoefficients)) /\ ((((((exists pfa_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal) = (Lu)) /\ ((((exists ff_h_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_backward_original_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermleftoutside+(Lu)=(pfc_index_execution_backward_original_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_backward_original_left_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_backward_original_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_backward_original_left_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_backward_original_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_original_left_productcoefficientscoefficientdiagonal)=pfc_left_execution_backward_original_left_productcoefficientscoefficientdiagonalterm*pfc_right_execution_backward_original_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_original_left_productcoefficientscoefficientsum fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_backward_original_left_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_backward_original_left_productcoefficients))) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_backward_original_left_productcoefficients))) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_backward_original_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_backward_original_left_productcoefficients)) -> exists fs_a_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_original_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_backward_original_left_productcoefficientscoefficient = fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_original_left_productcoefficientscoefficient) + (fs_a_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum) + (fs_r_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_left_productcoefficientscoefficientsum) + (fs_s_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_backward_original_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_original_left_productcoefficientscoefficientresiduebound. pfa_gap_execution_backward_original_left_productcoefficientscoefficientresiduebound + S (pfc_value_execution_backward_original_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_backward_original_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_backward_original_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_backward_original_left_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_backward_original_left_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_backward_original_left_productcoefficients) + (p) * pfa_offset_right_execution_backward_original_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_execution_backward_original_right_productleft. (exists fom_gap_pfp_execution_backward_original_right_productleft_index_bound. fom_gap_pfp_execution_backward_original_right_productleft_index_bound + S (fom_index_pfp_execution_backward_original_right_productleft) = Lv) -> exists fom_value_pfp_execution_backward_original_right_productleft. ((((exists fom_beta_height_pfp_execution_backward_original_right_productleft_entry. fom_beta_height_pfp_execution_backward_original_right_productleft_entry + S (fom_value_pfp_execution_backward_original_right_productleft) = S ((S (fom_index_pfp_execution_backward_original_right_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_execution_backward_original_right_productleft_entry. vb = fom_beta_quotient_pfp_execution_backward_original_right_productleft_entry * S ((S (fom_index_pfp_execution_backward_original_right_productleft)) * vc) + (fom_value_pfp_execution_backward_original_right_productleft))) /\ (exists fom_gap_pfp_execution_backward_original_right_productleft_value_bound. fom_gap_pfp_execution_backward_original_right_productleft_value_bound + S (fom_value_pfp_execution_backward_original_right_productleft) = p))) /\ (((forall fom_index_pfp_execution_backward_original_right_productright. (exists fom_gap_pfp_execution_backward_original_right_productright_index_bound. fom_gap_pfp_execution_backward_original_right_productright_index_bound + S (fom_index_pfp_execution_backward_original_right_productright) = Lr) -> exists fom_value_pfp_execution_backward_original_right_productright. ((((exists fom_beta_height_pfp_execution_backward_original_right_productright_entry. fom_beta_height_pfp_execution_backward_original_right_productright_entry + S (fom_value_pfp_execution_backward_original_right_productright) = S ((S (fom_index_pfp_execution_backward_original_right_productright)) * rc)) /\ exists fom_beta_quotient_pfp_execution_backward_original_right_productright_entry. rb = fom_beta_quotient_pfp_execution_backward_original_right_productright_entry * S ((S (fom_index_pfp_execution_backward_original_right_productright)) * rc) + (fom_value_pfp_execution_backward_original_right_productright))) /\ (exists fom_gap_pfp_execution_backward_original_right_productright_value_bound. fom_gap_pfp_execution_backward_original_right_productright_value_bound + S (fom_value_pfp_execution_backward_original_right_productright) = p))) /\ (((((((Lv)=0 \/ (Lr)=0) /\ (((pfbz_right_length_execution_backward_original)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lr)=0)) /\ (((Lv)+(Lr)=S (pfbz_right_length_execution_backward_original)))))))) /\ ((forall pfc_index_execution_backward_original_right_productcoefficients. (exists pfa_gap_execution_backward_original_right_productcoefficientsbound. pfa_gap_execution_backward_original_right_productcoefficientsbound + S (pfc_index_execution_backward_original_right_productcoefficients) = (pfbz_right_length_execution_backward_original)) -> exists pfc_value_execution_backward_original_right_productcoefficients. ((((exists ff_h_pfp_execution_backward_original_right_productcoefficientsentry. ff_h_pfp_execution_backward_original_right_productcoefficientsentry + S (pfc_value_execution_backward_original_right_productcoefficients) = S ((S (pfc_index_execution_backward_original_right_productcoefficients)) * pfbz_right_scale_execution_backward_original)) /\ exists ff_q_pfp_execution_backward_original_right_productcoefficientsentry. pfbz_right_code_execution_backward_original = ff_q_pfp_execution_backward_original_right_productcoefficientsentry * S ((S (pfc_index_execution_backward_original_right_productcoefficients)) * pfbz_right_scale_execution_backward_original) + (pfc_value_execution_backward_original_right_productcoefficients))) /\ ((exists pfc_terms_code_execution_backward_original_right_productcoefficientscoefficient pfc_terms_scale_execution_backward_original_right_productcoefficientscoefficient pfc_natural_sum_execution_backward_original_right_productcoefficientscoefficient. ((forall pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_backward_original_right_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_backward_original_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_backward_original_right_productcoefficients))) -> exists pfc_value_execution_backward_original_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_backward_original_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_original_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_backward_original_right_productcoefficientscoefficient = ff_q_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_original_right_productcoefficientscoefficient) + (pfc_value_execution_backward_original_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_backward_original_right_productcoefficientscoefficientdiagonalterm pfc_left_execution_backward_original_right_productcoefficientscoefficientdiagonalterm pfc_right_execution_backward_original_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal)+pfc_complement_execution_backward_original_right_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_backward_original_right_productcoefficients)) /\ ((((((exists pfa_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_backward_original_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_execution_backward_original_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_backward_original_right_productcoefficientscoefficientdiagonalterm) = (Lr)) /\ ((((exists ff_h_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_backward_original_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)) * rc)) /\ exists ff_q_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry. rb = ff_q_pfp_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)) * rc) + (pfc_right_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_backward_original_right_productcoefficientscoefficientdiagonaltermrightoutside+(Lr)=(pfc_complement_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_backward_original_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_original_right_productcoefficientscoefficientdiagonal)=pfc_left_execution_backward_original_right_productcoefficientscoefficientdiagonalterm*pfc_right_execution_backward_original_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_original_right_productcoefficientscoefficientsum fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_backward_original_right_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_backward_original_right_productcoefficients))) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_backward_original_right_productcoefficients))) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_backward_original_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_backward_original_right_productcoefficients)) -> exists fs_a_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_original_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_backward_original_right_productcoefficientscoefficient = fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_original_right_productcoefficientscoefficient) + (fs_a_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum) + (fs_r_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_original_right_productcoefficientscoefficientsum) + (fs_s_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_backward_original_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_original_right_productcoefficientscoefficientresiduebound. pfa_gap_execution_backward_original_right_productcoefficientscoefficientresiduebound + S (pfc_value_execution_backward_original_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_backward_original_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_backward_original_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_backward_original_right_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_backward_original_right_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_backward_original_right_productcoefficients) + (p) * pfa_offset_right_execution_backward_original_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_execution_backward_original_sum_left_bounded. (exists fom_gap_pfp_execution_backward_original_sum_left_bounded_index_bound. fom_gap_pfp_execution_backward_original_sum_left_bounded_index_bound + S (fom_index_pfp_execution_backward_original_sum_left_bounded) = pfbz_left_length_execution_backward_original) -> exists fom_value_pfp_execution_backward_original_sum_left_bounded. ((((exists fom_beta_height_pfp_execution_backward_original_sum_left_bounded_entry. fom_beta_height_pfp_execution_backward_original_sum_left_bounded_entry + S (fom_value_pfp_execution_backward_original_sum_left_bounded) = S ((S (fom_index_pfp_execution_backward_original_sum_left_bounded)) * pfbz_left_scale_execution_backward_original)) /\ exists fom_beta_quotient_pfp_execution_backward_original_sum_left_bounded_entry. pfbz_left_code_execution_backward_original = fom_beta_quotient_pfp_execution_backward_original_sum_left_bounded_entry * S ((S (fom_index_pfp_execution_backward_original_sum_left_bounded)) * pfbz_left_scale_execution_backward_original) + (fom_value_pfp_execution_backward_original_sum_left_bounded))) /\ (exists fom_gap_pfp_execution_backward_original_sum_left_bounded_value_bound. fom_gap_pfp_execution_backward_original_sum_left_bounded_value_bound + S (fom_value_pfp_execution_backward_original_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_execution_backward_original_sum_right_bounded. (exists fom_gap_pfp_execution_backward_original_sum_right_bounded_index_bound. fom_gap_pfp_execution_backward_original_sum_right_bounded_index_bound + S (fom_index_pfp_execution_backward_original_sum_right_bounded) = pfbz_right_length_execution_backward_original) -> exists fom_value_pfp_execution_backward_original_sum_right_bounded. ((((exists fom_beta_height_pfp_execution_backward_original_sum_right_bounded_entry. fom_beta_height_pfp_execution_backward_original_sum_right_bounded_entry + S (fom_value_pfp_execution_backward_original_sum_right_bounded) = S ((S (fom_index_pfp_execution_backward_original_sum_right_bounded)) * pfbz_right_scale_execution_backward_original)) /\ exists fom_beta_quotient_pfp_execution_backward_original_sum_right_bounded_entry. pfbz_right_code_execution_backward_original = fom_beta_quotient_pfp_execution_backward_original_sum_right_bounded_entry * S ((S (fom_index_pfp_execution_backward_original_sum_right_bounded)) * pfbz_right_scale_execution_backward_original) + (fom_value_pfp_execution_backward_original_sum_right_bounded))) /\ (exists fom_gap_pfp_execution_backward_original_sum_right_bounded_value_bound. fom_gap_pfp_execution_backward_original_sum_right_bounded_value_bound + S (fom_value_pfp_execution_backward_original_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_execution_backward_original_sum_result_bounded. (exists fom_gap_pfp_execution_backward_original_sum_result_bounded_index_bound. fom_gap_pfp_execution_backward_original_sum_result_bounded_index_bound + S (fom_index_pfp_execution_backward_original_sum_result_bounded) = Lg) -> exists fom_value_pfp_execution_backward_original_sum_result_bounded. ((((exists fom_beta_height_pfp_execution_backward_original_sum_result_bounded_entry. fom_beta_height_pfp_execution_backward_original_sum_result_bounded_entry + S (fom_value_pfp_execution_backward_original_sum_result_bounded) = S ((S (fom_index_pfp_execution_backward_original_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_execution_backward_original_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_execution_backward_original_sum_result_bounded_entry * S ((S (fom_index_pfp_execution_backward_original_sum_result_bounded)) * gc) + (fom_value_pfp_execution_backward_original_sum_result_bounded))) /\ (exists fom_gap_pfp_execution_backward_original_sum_result_bounded_value_bound. fom_gap_pfp_execution_backward_original_sum_result_bounded_value_bound + S (fom_value_pfp_execution_backward_original_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_execution_backward_original_sum pfaa_left_c_execution_backward_original_sum pfaa_right_b_execution_backward_original_sum pfaa_right_c_execution_backward_original_sum pfaa_sum_b_execution_backward_original_sum pfaa_sum_c_execution_backward_original_sum pfaa_length_execution_backward_original_sum. ((((forall pfrep_power_execution_backward_original_sum_witness_common_left pfrep_left_execution_backward_original_sum_witness_common_left pfrep_right_execution_backward_original_sum_witness_common_left. ((exists pfrep_position_execution_backward_original_sum_witness_common_leftfirst. ((pfrep_position_execution_backward_original_sum_witness_common_leftfirst+S (pfrep_power_execution_backward_original_sum_witness_common_left)=(pfbz_left_length_execution_backward_original)) /\ ((((exists ff_h_pfp_execution_backward_original_sum_witness_common_leftfirstentry. ff_h_pfp_execution_backward_original_sum_witness_common_leftfirstentry + S (pfrep_left_execution_backward_original_sum_witness_common_left) = S ((S (pfrep_position_execution_backward_original_sum_witness_common_leftfirst)) * pfbz_left_scale_execution_backward_original)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_common_leftfirstentry. pfbz_left_code_execution_backward_original = ff_q_pfp_execution_backward_original_sum_witness_common_leftfirstentry * S ((S (pfrep_position_execution_backward_original_sum_witness_common_leftfirst)) * pfbz_left_scale_execution_backward_original) + (pfrep_left_execution_backward_original_sum_witness_common_left)))))) \/ (((exists pfrep_gap_execution_backward_original_sum_witness_common_leftfirstoutside. pfrep_gap_execution_backward_original_sum_witness_common_leftfirstoutside+(pfbz_left_length_execution_backward_original)=(pfrep_power_execution_backward_original_sum_witness_common_left)) /\ (((pfrep_left_execution_backward_original_sum_witness_common_left)=0))))) -> ((exists pfrep_position_execution_backward_original_sum_witness_common_leftsecond. ((pfrep_position_execution_backward_original_sum_witness_common_leftsecond+S (pfrep_power_execution_backward_original_sum_witness_common_left)=(pfaa_length_execution_backward_original_sum)) /\ ((((exists ff_h_pfp_execution_backward_original_sum_witness_common_leftsecondentry. ff_h_pfp_execution_backward_original_sum_witness_common_leftsecondentry + S (pfrep_right_execution_backward_original_sum_witness_common_left) = S ((S (pfrep_position_execution_backward_original_sum_witness_common_leftsecond)) * pfaa_left_c_execution_backward_original_sum)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_common_leftsecondentry. pfaa_left_b_execution_backward_original_sum = ff_q_pfp_execution_backward_original_sum_witness_common_leftsecondentry * S ((S (pfrep_position_execution_backward_original_sum_witness_common_leftsecond)) * pfaa_left_c_execution_backward_original_sum) + (pfrep_right_execution_backward_original_sum_witness_common_left)))))) \/ (((exists pfrep_gap_execution_backward_original_sum_witness_common_leftsecondoutside. pfrep_gap_execution_backward_original_sum_witness_common_leftsecondoutside+(pfaa_length_execution_backward_original_sum)=(pfrep_power_execution_backward_original_sum_witness_common_left)) /\ (((pfrep_right_execution_backward_original_sum_witness_common_left)=0))))) -> pfrep_left_execution_backward_original_sum_witness_common_left=pfrep_right_execution_backward_original_sum_witness_common_left) /\ ((forall pfrep_power_execution_backward_original_sum_witness_common_right pfrep_left_execution_backward_original_sum_witness_common_right pfrep_right_execution_backward_original_sum_witness_common_right. ((exists pfrep_position_execution_backward_original_sum_witness_common_rightfirst. ((pfrep_position_execution_backward_original_sum_witness_common_rightfirst+S (pfrep_power_execution_backward_original_sum_witness_common_right)=(pfbz_right_length_execution_backward_original)) /\ ((((exists ff_h_pfp_execution_backward_original_sum_witness_common_rightfirstentry. ff_h_pfp_execution_backward_original_sum_witness_common_rightfirstentry + S (pfrep_left_execution_backward_original_sum_witness_common_right) = S ((S (pfrep_position_execution_backward_original_sum_witness_common_rightfirst)) * pfbz_right_scale_execution_backward_original)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_common_rightfirstentry. pfbz_right_code_execution_backward_original = ff_q_pfp_execution_backward_original_sum_witness_common_rightfirstentry * S ((S (pfrep_position_execution_backward_original_sum_witness_common_rightfirst)) * pfbz_right_scale_execution_backward_original) + (pfrep_left_execution_backward_original_sum_witness_common_right)))))) \/ (((exists pfrep_gap_execution_backward_original_sum_witness_common_rightfirstoutside. pfrep_gap_execution_backward_original_sum_witness_common_rightfirstoutside+(pfbz_right_length_execution_backward_original)=(pfrep_power_execution_backward_original_sum_witness_common_right)) /\ (((pfrep_left_execution_backward_original_sum_witness_common_right)=0))))) -> ((exists pfrep_position_execution_backward_original_sum_witness_common_rightsecond. ((pfrep_position_execution_backward_original_sum_witness_common_rightsecond+S (pfrep_power_execution_backward_original_sum_witness_common_right)=(pfaa_length_execution_backward_original_sum)) /\ ((((exists ff_h_pfp_execution_backward_original_sum_witness_common_rightsecondentry. ff_h_pfp_execution_backward_original_sum_witness_common_rightsecondentry + S (pfrep_right_execution_backward_original_sum_witness_common_right) = S ((S (pfrep_position_execution_backward_original_sum_witness_common_rightsecond)) * pfaa_right_c_execution_backward_original_sum)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_common_rightsecondentry. pfaa_right_b_execution_backward_original_sum = ff_q_pfp_execution_backward_original_sum_witness_common_rightsecondentry * S ((S (pfrep_position_execution_backward_original_sum_witness_common_rightsecond)) * pfaa_right_c_execution_backward_original_sum) + (pfrep_right_execution_backward_original_sum_witness_common_right)))))) \/ (((exists pfrep_gap_execution_backward_original_sum_witness_common_rightsecondoutside. pfrep_gap_execution_backward_original_sum_witness_common_rightsecondoutside+(pfaa_length_execution_backward_original_sum)=(pfrep_power_execution_backward_original_sum_witness_common_right)) /\ (((pfrep_right_execution_backward_original_sum_witness_common_right)=0))))) -> pfrep_left_execution_backward_original_sum_witness_common_right=pfrep_right_execution_backward_original_sum_witness_common_right)))) /\ (((forall pfp_index_execution_backward_original_sum_witness_operation. (exists pfa_gap_execution_backward_original_sum_witness_operationindex. pfa_gap_execution_backward_original_sum_witness_operationindex + S (pfp_index_execution_backward_original_sum_witness_operation) = (pfaa_length_execution_backward_original_sum)) -> exists pfp_left_execution_backward_original_sum_witness_operation pfp_right_execution_backward_original_sum_witness_operation pfp_value_execution_backward_original_sum_witness_operation. ((((exists ff_h_pfp_execution_backward_original_sum_witness_operationleft. ff_h_pfp_execution_backward_original_sum_witness_operationleft + S (pfp_left_execution_backward_original_sum_witness_operation) = S ((S (pfp_index_execution_backward_original_sum_witness_operation)) * pfaa_left_c_execution_backward_original_sum)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_operationleft. pfaa_left_b_execution_backward_original_sum = ff_q_pfp_execution_backward_original_sum_witness_operationleft * S ((S (pfp_index_execution_backward_original_sum_witness_operation)) * pfaa_left_c_execution_backward_original_sum) + (pfp_left_execution_backward_original_sum_witness_operation))) /\ (((((exists ff_h_pfp_execution_backward_original_sum_witness_operationright. ff_h_pfp_execution_backward_original_sum_witness_operationright + S (pfp_right_execution_backward_original_sum_witness_operation) = S ((S (pfp_index_execution_backward_original_sum_witness_operation)) * pfaa_right_c_execution_backward_original_sum)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_operationright. pfaa_right_b_execution_backward_original_sum = ff_q_pfp_execution_backward_original_sum_witness_operationright * S ((S (pfp_index_execution_backward_original_sum_witness_operation)) * pfaa_right_c_execution_backward_original_sum) + (pfp_right_execution_backward_original_sum_witness_operation))) /\ (((((exists ff_h_pfp_execution_backward_original_sum_witness_operationtarget. ff_h_pfp_execution_backward_original_sum_witness_operationtarget + S (pfp_value_execution_backward_original_sum_witness_operation) = S ((S (pfp_index_execution_backward_original_sum_witness_operation)) * pfaa_sum_c_execution_backward_original_sum)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_operationtarget. pfaa_sum_b_execution_backward_original_sum = ff_q_pfp_execution_backward_original_sum_witness_operationtarget * S ((S (pfp_index_execution_backward_original_sum_witness_operation)) * pfaa_sum_c_execution_backward_original_sum) + (pfp_value_execution_backward_original_sum_witness_operation))) /\ ((((exists pfa_gap_execution_backward_original_sum_witness_operationoperationleft. pfa_gap_execution_backward_original_sum_witness_operationoperationleft + S (pfp_left_execution_backward_original_sum_witness_operation) = (p)) /\ (((exists pfa_gap_execution_backward_original_sum_witness_operationoperationright. pfa_gap_execution_backward_original_sum_witness_operationoperationright + S (pfp_right_execution_backward_original_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_execution_backward_original_sum_witness_operationoperationresultbound. pfa_gap_execution_backward_original_sum_witness_operationoperationresultbound + S (pfp_value_execution_backward_original_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_execution_backward_original_sum_witness_operationoperationresultcongruence pfa_offset_right_execution_backward_original_sum_witness_operationoperationresultcongruence. ((pfp_left_execution_backward_original_sum_witness_operation) + (pfp_right_execution_backward_original_sum_witness_operation)) + (p) * pfa_offset_left_execution_backward_original_sum_witness_operationoperationresultcongruence = (pfp_value_execution_backward_original_sum_witness_operation) + (p) * pfa_offset_right_execution_backward_original_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_execution_backward_original_sum_witness_output pfrep_left_execution_backward_original_sum_witness_output pfrep_right_execution_backward_original_sum_witness_output. ((exists pfrep_position_execution_backward_original_sum_witness_outputfirst. ((pfrep_position_execution_backward_original_sum_witness_outputfirst+S (pfrep_power_execution_backward_original_sum_witness_output)=(pfaa_length_execution_backward_original_sum)) /\ ((((exists ff_h_pfp_execution_backward_original_sum_witness_outputfirstentry. ff_h_pfp_execution_backward_original_sum_witness_outputfirstentry + S (pfrep_left_execution_backward_original_sum_witness_output) = S ((S (pfrep_position_execution_backward_original_sum_witness_outputfirst)) * pfaa_sum_c_execution_backward_original_sum)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_outputfirstentry. pfaa_sum_b_execution_backward_original_sum = ff_q_pfp_execution_backward_original_sum_witness_outputfirstentry * S ((S (pfrep_position_execution_backward_original_sum_witness_outputfirst)) * pfaa_sum_c_execution_backward_original_sum) + (pfrep_left_execution_backward_original_sum_witness_output)))))) \/ (((exists pfrep_gap_execution_backward_original_sum_witness_outputfirstoutside. pfrep_gap_execution_backward_original_sum_witness_outputfirstoutside+(pfaa_length_execution_backward_original_sum)=(pfrep_power_execution_backward_original_sum_witness_output)) /\ (((pfrep_left_execution_backward_original_sum_witness_output)=0))))) -> ((exists pfrep_position_execution_backward_original_sum_witness_outputsecond. ((pfrep_position_execution_backward_original_sum_witness_outputsecond+S (pfrep_power_execution_backward_original_sum_witness_output)=(Lg)) /\ ((((exists ff_h_pfp_execution_backward_original_sum_witness_outputsecondentry. ff_h_pfp_execution_backward_original_sum_witness_outputsecondentry + S (pfrep_right_execution_backward_original_sum_witness_output) = S ((S (pfrep_position_execution_backward_original_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_execution_backward_original_sum_witness_outputsecondentry. gb = ff_q_pfp_execution_backward_original_sum_witness_outputsecondentry * S ((S (pfrep_position_execution_backward_original_sum_witness_outputsecond)) * gc) + (pfrep_right_execution_backward_original_sum_witness_output)))))) \/ (((exists pfrep_gap_execution_backward_original_sum_witness_outputsecondoutside. pfrep_gap_execution_backward_original_sum_witness_outputsecondoutside+(Lg)=(pfrep_power_execution_backward_original_sum_witness_output)) /\ (((pfrep_right_execution_backward_original_sum_witness_output)=0))))) -> pfrep_left_execution_backward_original_sum_witness_output=pfrep_right_execution_backward_original_sum_witness_output)))))))))))))))))) -> (exists pfbz_update_wb_execution_backward_result pfbz_update_wc_execution_backward_result pfbz_update_W_execution_backward_result pfbz_update_tb_execution_backward_result pfbz_update_tc_execution_backward_result pfbz_update_T_execution_backward_result. ((((forall fom_index_pfp_execution_backward_result_coefficient_productleft. (exists fom_gap_pfp_execution_backward_result_coefficient_productleft_index_bound. fom_gap_pfp_execution_backward_result_coefficient_productleft_index_bound + S (fom_index_pfp_execution_backward_result_coefficient_productleft) = Lv) -> exists fom_value_pfp_execution_backward_result_coefficient_productleft. ((((exists fom_beta_height_pfp_execution_backward_result_coefficient_productleft_entry. fom_beta_height_pfp_execution_backward_result_coefficient_productleft_entry + S (fom_value_pfp_execution_backward_result_coefficient_productleft) = S ((S (fom_index_pfp_execution_backward_result_coefficient_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_execution_backward_result_coefficient_productleft_entry. vb = fom_beta_quotient_pfp_execution_backward_result_coefficient_productleft_entry * S ((S (fom_index_pfp_execution_backward_result_coefficient_productleft)) * vc) + (fom_value_pfp_execution_backward_result_coefficient_productleft))) /\ (exists fom_gap_pfp_execution_backward_result_coefficient_productleft_value_bound. fom_gap_pfp_execution_backward_result_coefficient_productleft_value_bound + S (fom_value_pfp_execution_backward_result_coefficient_productleft) = p))) /\ (((forall fom_index_pfp_execution_backward_result_coefficient_productright. (exists fom_gap_pfp_execution_backward_result_coefficient_productright_index_bound. fom_gap_pfp_execution_backward_result_coefficient_productright_index_bound + S (fom_index_pfp_execution_backward_result_coefficient_productright) = Lq) -> exists fom_value_pfp_execution_backward_result_coefficient_productright. ((((exists fom_beta_height_pfp_execution_backward_result_coefficient_productright_entry. fom_beta_height_pfp_execution_backward_result_coefficient_productright_entry + S (fom_value_pfp_execution_backward_result_coefficient_productright) = S ((S (fom_index_pfp_execution_backward_result_coefficient_productright)) * qc)) /\ exists fom_beta_quotient_pfp_execution_backward_result_coefficient_productright_entry. qb = fom_beta_quotient_pfp_execution_backward_result_coefficient_productright_entry * S ((S (fom_index_pfp_execution_backward_result_coefficient_productright)) * qc) + (fom_value_pfp_execution_backward_result_coefficient_productright))) /\ (exists fom_gap_pfp_execution_backward_result_coefficient_productright_value_bound. fom_gap_pfp_execution_backward_result_coefficient_productright_value_bound + S (fom_value_pfp_execution_backward_result_coefficient_productright) = p))) /\ (((((((Lv)=0 \/ (Lq)=0) /\ (((pfbz_update_W_execution_backward_result)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lq)=0)) /\ (((Lv)+(Lq)=S (pfbz_update_W_execution_backward_result)))))))) /\ ((forall pfc_index_execution_backward_result_coefficient_productcoefficients. (exists pfa_gap_execution_backward_result_coefficient_productcoefficientsbound. pfa_gap_execution_backward_result_coefficient_productcoefficientsbound + S (pfc_index_execution_backward_result_coefficient_productcoefficients) = (pfbz_update_W_execution_backward_result)) -> exists pfc_value_execution_backward_result_coefficient_productcoefficients. ((((exists ff_h_pfp_execution_backward_result_coefficient_productcoefficientsentry. ff_h_pfp_execution_backward_result_coefficient_productcoefficientsentry + S (pfc_value_execution_backward_result_coefficient_productcoefficients) = S ((S (pfc_index_execution_backward_result_coefficient_productcoefficients)) * pfbz_update_wc_execution_backward_result)) /\ exists ff_q_pfp_execution_backward_result_coefficient_productcoefficientsentry. pfbz_update_wb_execution_backward_result = ff_q_pfp_execution_backward_result_coefficient_productcoefficientsentry * S ((S (pfc_index_execution_backward_result_coefficient_productcoefficients)) * pfbz_update_wc_execution_backward_result) + (pfc_value_execution_backward_result_coefficient_productcoefficients))) /\ ((exists pfc_terms_code_execution_backward_result_coefficient_productcoefficientscoefficient pfc_terms_scale_execution_backward_result_coefficient_productcoefficientscoefficient pfc_natural_sum_execution_backward_result_coefficient_productcoefficientscoefficient. ((forall pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_backward_result_coefficient_productcoefficients))) -> exists pfc_value_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_result_coefficient_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_backward_result_coefficient_productcoefficientscoefficient = ff_q_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_result_coefficient_productcoefficientscoefficient) + (pfc_value_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm pfc_left_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm pfc_right_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)+pfc_complement_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_backward_result_coefficient_productcoefficients)) /\ ((((((exists pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm) = (Lq)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)) * qc)) /\ exists ff_q_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry. qb = ff_q_pfp_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)) * qc) + (pfc_right_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightoutside+(Lq)=(pfc_complement_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_result_coefficient_productcoefficientscoefficientdiagonal)=pfc_left_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm*pfc_right_execution_backward_result_coefficient_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_backward_result_coefficient_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_backward_result_coefficient_productcoefficients))) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_backward_result_coefficient_productcoefficients))) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_backward_result_coefficient_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_backward_result_coefficient_productcoefficients)) -> exists fs_a_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_result_coefficient_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_backward_result_coefficient_productcoefficientscoefficient = fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_result_coefficient_productcoefficientscoefficient) + (fs_a_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum) + (fs_r_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum) + (fs_s_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientresiduebound. pfa_gap_execution_backward_result_coefficient_productcoefficientscoefficientresiduebound + S (pfc_value_execution_backward_result_coefficient_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_backward_result_coefficient_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_backward_result_coefficient_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_backward_result_coefficient_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_backward_result_coefficient_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_backward_result_coefficient_productcoefficients) + (p) * pfa_offset_right_execution_backward_result_coefficient_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_execution_backward_result_coefficient_difference_left_bounded. (exists fom_gap_pfp_execution_backward_result_coefficient_difference_left_bounded_index_bound. fom_gap_pfp_execution_backward_result_coefficient_difference_left_bounded_index_bound + S (fom_index_pfp_execution_backward_result_coefficient_difference_left_bounded) = pfbz_update_W_execution_backward_result) -> exists fom_value_pfp_execution_backward_result_coefficient_difference_left_bounded. ((((exists fom_beta_height_pfp_execution_backward_result_coefficient_difference_left_bounded_entry. fom_beta_height_pfp_execution_backward_result_coefficient_difference_left_bounded_entry + S (fom_value_pfp_execution_backward_result_coefficient_difference_left_bounded) = S ((S (fom_index_pfp_execution_backward_result_coefficient_difference_left_bounded)) * pfbz_update_wc_execution_backward_result)) /\ exists fom_beta_quotient_pfp_execution_backward_result_coefficient_difference_left_bounded_entry. pfbz_update_wb_execution_backward_result = fom_beta_quotient_pfp_execution_backward_result_coefficient_difference_left_bounded_entry * S ((S (fom_index_pfp_execution_backward_result_coefficient_difference_left_bounded)) * pfbz_update_wc_execution_backward_result) + (fom_value_pfp_execution_backward_result_coefficient_difference_left_bounded))) /\ (exists fom_gap_pfp_execution_backward_result_coefficient_difference_left_bounded_value_bound. fom_gap_pfp_execution_backward_result_coefficient_difference_left_bounded_value_bound + S (fom_value_pfp_execution_backward_result_coefficient_difference_left_bounded) = p))) /\ (((forall fom_index_pfp_execution_backward_result_coefficient_difference_right_bounded. (exists fom_gap_pfp_execution_backward_result_coefficient_difference_right_bounded_index_bound. fom_gap_pfp_execution_backward_result_coefficient_difference_right_bounded_index_bound + S (fom_index_pfp_execution_backward_result_coefficient_difference_right_bounded) = pfbz_update_T_execution_backward_result) -> exists fom_value_pfp_execution_backward_result_coefficient_difference_right_bounded. ((((exists fom_beta_height_pfp_execution_backward_result_coefficient_difference_right_bounded_entry. fom_beta_height_pfp_execution_backward_result_coefficient_difference_right_bounded_entry + S (fom_value_pfp_execution_backward_result_coefficient_difference_right_bounded) = S ((S (fom_index_pfp_execution_backward_result_coefficient_difference_right_bounded)) * pfbz_update_tc_execution_backward_result)) /\ exists fom_beta_quotient_pfp_execution_backward_result_coefficient_difference_right_bounded_entry. pfbz_update_tb_execution_backward_result = fom_beta_quotient_pfp_execution_backward_result_coefficient_difference_right_bounded_entry * S ((S (fom_index_pfp_execution_backward_result_coefficient_difference_right_bounded)) * pfbz_update_tc_execution_backward_result) + (fom_value_pfp_execution_backward_result_coefficient_difference_right_bounded))) /\ (exists fom_gap_pfp_execution_backward_result_coefficient_difference_right_bounded_value_bound. fom_gap_pfp_execution_backward_result_coefficient_difference_right_bounded_value_bound + S (fom_value_pfp_execution_backward_result_coefficient_difference_right_bounded) = p))) /\ (((forall fom_index_pfp_execution_backward_result_coefficient_difference_result_bounded. (exists fom_gap_pfp_execution_backward_result_coefficient_difference_result_bounded_index_bound. fom_gap_pfp_execution_backward_result_coefficient_difference_result_bounded_index_bound + S (fom_index_pfp_execution_backward_result_coefficient_difference_result_bounded) = Lu) -> exists fom_value_pfp_execution_backward_result_coefficient_difference_result_bounded. ((((exists fom_beta_height_pfp_execution_backward_result_coefficient_difference_result_bounded_entry. fom_beta_height_pfp_execution_backward_result_coefficient_difference_result_bounded_entry + S (fom_value_pfp_execution_backward_result_coefficient_difference_result_bounded) = S ((S (fom_index_pfp_execution_backward_result_coefficient_difference_result_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_execution_backward_result_coefficient_difference_result_bounded_entry. ub = fom_beta_quotient_pfp_execution_backward_result_coefficient_difference_result_bounded_entry * S ((S (fom_index_pfp_execution_backward_result_coefficient_difference_result_bounded)) * uc) + (fom_value_pfp_execution_backward_result_coefficient_difference_result_bounded))) /\ (exists fom_gap_pfp_execution_backward_result_coefficient_difference_result_bounded_value_bound. fom_gap_pfp_execution_backward_result_coefficient_difference_result_bounded_value_bound + S (fom_value_pfp_execution_backward_result_coefficient_difference_result_bounded) = p))) /\ ((exists pfaa_left_b_execution_backward_result_coefficient_difference pfaa_left_c_execution_backward_result_coefficient_difference pfaa_right_b_execution_backward_result_coefficient_difference pfaa_right_c_execution_backward_result_coefficient_difference pfaa_sum_b_execution_backward_result_coefficient_difference pfaa_sum_c_execution_backward_result_coefficient_difference pfaa_length_execution_backward_result_coefficient_difference. ((((forall pfrep_power_execution_backward_result_coefficient_difference_witness_common_left pfrep_left_execution_backward_result_coefficient_difference_witness_common_left pfrep_right_execution_backward_result_coefficient_difference_witness_common_left. ((exists pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftfirst. ((pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftfirst+S (pfrep_power_execution_backward_result_coefficient_difference_witness_common_left)=(pfbz_update_W_execution_backward_result)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_leftfirstentry. ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_leftfirstentry + S (pfrep_left_execution_backward_result_coefficient_difference_witness_common_left) = S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftfirst)) * pfbz_update_wc_execution_backward_result)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_leftfirstentry. pfbz_update_wb_execution_backward_result = ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_leftfirstentry * S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftfirst)) * pfbz_update_wc_execution_backward_result) + (pfrep_left_execution_backward_result_coefficient_difference_witness_common_left)))))) \/ (((exists pfrep_gap_execution_backward_result_coefficient_difference_witness_common_leftfirstoutside. pfrep_gap_execution_backward_result_coefficient_difference_witness_common_leftfirstoutside+(pfbz_update_W_execution_backward_result)=(pfrep_power_execution_backward_result_coefficient_difference_witness_common_left)) /\ (((pfrep_left_execution_backward_result_coefficient_difference_witness_common_left)=0))))) -> ((exists pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftsecond. ((pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftsecond+S (pfrep_power_execution_backward_result_coefficient_difference_witness_common_left)=(pfaa_length_execution_backward_result_coefficient_difference)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_leftsecondentry. ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_leftsecondentry + S (pfrep_right_execution_backward_result_coefficient_difference_witness_common_left) = S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftsecond)) * pfaa_left_c_execution_backward_result_coefficient_difference)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_leftsecondentry. pfaa_left_b_execution_backward_result_coefficient_difference = ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_leftsecondentry * S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_leftsecond)) * pfaa_left_c_execution_backward_result_coefficient_difference) + (pfrep_right_execution_backward_result_coefficient_difference_witness_common_left)))))) \/ (((exists pfrep_gap_execution_backward_result_coefficient_difference_witness_common_leftsecondoutside. pfrep_gap_execution_backward_result_coefficient_difference_witness_common_leftsecondoutside+(pfaa_length_execution_backward_result_coefficient_difference)=(pfrep_power_execution_backward_result_coefficient_difference_witness_common_left)) /\ (((pfrep_right_execution_backward_result_coefficient_difference_witness_common_left)=0))))) -> pfrep_left_execution_backward_result_coefficient_difference_witness_common_left=pfrep_right_execution_backward_result_coefficient_difference_witness_common_left) /\ ((forall pfrep_power_execution_backward_result_coefficient_difference_witness_common_right pfrep_left_execution_backward_result_coefficient_difference_witness_common_right pfrep_right_execution_backward_result_coefficient_difference_witness_common_right. ((exists pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightfirst. ((pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightfirst+S (pfrep_power_execution_backward_result_coefficient_difference_witness_common_right)=(pfbz_update_T_execution_backward_result)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_rightfirstentry. ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_rightfirstentry + S (pfrep_left_execution_backward_result_coefficient_difference_witness_common_right) = S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightfirst)) * pfbz_update_tc_execution_backward_result)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_rightfirstentry. pfbz_update_tb_execution_backward_result = ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_rightfirstentry * S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightfirst)) * pfbz_update_tc_execution_backward_result) + (pfrep_left_execution_backward_result_coefficient_difference_witness_common_right)))))) \/ (((exists pfrep_gap_execution_backward_result_coefficient_difference_witness_common_rightfirstoutside. pfrep_gap_execution_backward_result_coefficient_difference_witness_common_rightfirstoutside+(pfbz_update_T_execution_backward_result)=(pfrep_power_execution_backward_result_coefficient_difference_witness_common_right)) /\ (((pfrep_left_execution_backward_result_coefficient_difference_witness_common_right)=0))))) -> ((exists pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightsecond. ((pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightsecond+S (pfrep_power_execution_backward_result_coefficient_difference_witness_common_right)=(pfaa_length_execution_backward_result_coefficient_difference)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_rightsecondentry. ff_h_pfp_execution_backward_result_coefficient_difference_witness_common_rightsecondentry + S (pfrep_right_execution_backward_result_coefficient_difference_witness_common_right) = S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightsecond)) * pfaa_right_c_execution_backward_result_coefficient_difference)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_rightsecondentry. pfaa_right_b_execution_backward_result_coefficient_difference = ff_q_pfp_execution_backward_result_coefficient_difference_witness_common_rightsecondentry * S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_common_rightsecond)) * pfaa_right_c_execution_backward_result_coefficient_difference) + (pfrep_right_execution_backward_result_coefficient_difference_witness_common_right)))))) \/ (((exists pfrep_gap_execution_backward_result_coefficient_difference_witness_common_rightsecondoutside. pfrep_gap_execution_backward_result_coefficient_difference_witness_common_rightsecondoutside+(pfaa_length_execution_backward_result_coefficient_difference)=(pfrep_power_execution_backward_result_coefficient_difference_witness_common_right)) /\ (((pfrep_right_execution_backward_result_coefficient_difference_witness_common_right)=0))))) -> pfrep_left_execution_backward_result_coefficient_difference_witness_common_right=pfrep_right_execution_backward_result_coefficient_difference_witness_common_right)))) /\ (((forall pfp_index_execution_backward_result_coefficient_difference_witness_operation. (exists pfa_gap_execution_backward_result_coefficient_difference_witness_operationindex. pfa_gap_execution_backward_result_coefficient_difference_witness_operationindex + S (pfp_index_execution_backward_result_coefficient_difference_witness_operation) = (pfaa_length_execution_backward_result_coefficient_difference)) -> exists pfp_left_execution_backward_result_coefficient_difference_witness_operation pfp_right_execution_backward_result_coefficient_difference_witness_operation pfp_value_execution_backward_result_coefficient_difference_witness_operation. ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_operationleft. ff_h_pfp_execution_backward_result_coefficient_difference_witness_operationleft + S (pfp_left_execution_backward_result_coefficient_difference_witness_operation) = S ((S (pfp_index_execution_backward_result_coefficient_difference_witness_operation)) * pfaa_left_c_execution_backward_result_coefficient_difference)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_operationleft. pfaa_left_b_execution_backward_result_coefficient_difference = ff_q_pfp_execution_backward_result_coefficient_difference_witness_operationleft * S ((S (pfp_index_execution_backward_result_coefficient_difference_witness_operation)) * pfaa_left_c_execution_backward_result_coefficient_difference) + (pfp_left_execution_backward_result_coefficient_difference_witness_operation))) /\ (((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_operationright. ff_h_pfp_execution_backward_result_coefficient_difference_witness_operationright + S (pfp_right_execution_backward_result_coefficient_difference_witness_operation) = S ((S (pfp_index_execution_backward_result_coefficient_difference_witness_operation)) * pfaa_right_c_execution_backward_result_coefficient_difference)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_operationright. pfaa_right_b_execution_backward_result_coefficient_difference = ff_q_pfp_execution_backward_result_coefficient_difference_witness_operationright * S ((S (pfp_index_execution_backward_result_coefficient_difference_witness_operation)) * pfaa_right_c_execution_backward_result_coefficient_difference) + (pfp_right_execution_backward_result_coefficient_difference_witness_operation))) /\ (((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_operationtarget. ff_h_pfp_execution_backward_result_coefficient_difference_witness_operationtarget + S (pfp_value_execution_backward_result_coefficient_difference_witness_operation) = S ((S (pfp_index_execution_backward_result_coefficient_difference_witness_operation)) * pfaa_sum_c_execution_backward_result_coefficient_difference)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_operationtarget. pfaa_sum_b_execution_backward_result_coefficient_difference = ff_q_pfp_execution_backward_result_coefficient_difference_witness_operationtarget * S ((S (pfp_index_execution_backward_result_coefficient_difference_witness_operation)) * pfaa_sum_c_execution_backward_result_coefficient_difference) + (pfp_value_execution_backward_result_coefficient_difference_witness_operation))) /\ ((((exists pfa_gap_execution_backward_result_coefficient_difference_witness_operationoperationleft. pfa_gap_execution_backward_result_coefficient_difference_witness_operationoperationleft + S (pfp_left_execution_backward_result_coefficient_difference_witness_operation) = (p)) /\ (((exists pfa_gap_execution_backward_result_coefficient_difference_witness_operationoperationright. pfa_gap_execution_backward_result_coefficient_difference_witness_operationoperationright + S (pfp_right_execution_backward_result_coefficient_difference_witness_operation) = (p)) /\ ((((exists pfa_gap_execution_backward_result_coefficient_difference_witness_operationoperationresultbound. pfa_gap_execution_backward_result_coefficient_difference_witness_operationoperationresultbound + S (pfp_value_execution_backward_result_coefficient_difference_witness_operation) = (p)) /\ ((exists pfa_offset_left_execution_backward_result_coefficient_difference_witness_operationoperationresultcongruence pfa_offset_right_execution_backward_result_coefficient_difference_witness_operationoperationresultcongruence. ((pfp_left_execution_backward_result_coefficient_difference_witness_operation) + (pfp_right_execution_backward_result_coefficient_difference_witness_operation)) + (p) * pfa_offset_left_execution_backward_result_coefficient_difference_witness_operationoperationresultcongruence = (pfp_value_execution_backward_result_coefficient_difference_witness_operation) + (p) * pfa_offset_right_execution_backward_result_coefficient_difference_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_execution_backward_result_coefficient_difference_witness_output pfrep_left_execution_backward_result_coefficient_difference_witness_output pfrep_right_execution_backward_result_coefficient_difference_witness_output. ((exists pfrep_position_execution_backward_result_coefficient_difference_witness_outputfirst. ((pfrep_position_execution_backward_result_coefficient_difference_witness_outputfirst+S (pfrep_power_execution_backward_result_coefficient_difference_witness_output)=(pfaa_length_execution_backward_result_coefficient_difference)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_outputfirstentry. ff_h_pfp_execution_backward_result_coefficient_difference_witness_outputfirstentry + S (pfrep_left_execution_backward_result_coefficient_difference_witness_output) = S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_outputfirst)) * pfaa_sum_c_execution_backward_result_coefficient_difference)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_outputfirstentry. pfaa_sum_b_execution_backward_result_coefficient_difference = ff_q_pfp_execution_backward_result_coefficient_difference_witness_outputfirstentry * S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_outputfirst)) * pfaa_sum_c_execution_backward_result_coefficient_difference) + (pfrep_left_execution_backward_result_coefficient_difference_witness_output)))))) \/ (((exists pfrep_gap_execution_backward_result_coefficient_difference_witness_outputfirstoutside. pfrep_gap_execution_backward_result_coefficient_difference_witness_outputfirstoutside+(pfaa_length_execution_backward_result_coefficient_difference)=(pfrep_power_execution_backward_result_coefficient_difference_witness_output)) /\ (((pfrep_left_execution_backward_result_coefficient_difference_witness_output)=0))))) -> ((exists pfrep_position_execution_backward_result_coefficient_difference_witness_outputsecond. ((pfrep_position_execution_backward_result_coefficient_difference_witness_outputsecond+S (pfrep_power_execution_backward_result_coefficient_difference_witness_output)=(Lu)) /\ ((((exists ff_h_pfp_execution_backward_result_coefficient_difference_witness_outputsecondentry. ff_h_pfp_execution_backward_result_coefficient_difference_witness_outputsecondentry + S (pfrep_right_execution_backward_result_coefficient_difference_witness_output) = S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_outputsecond)) * uc)) /\ exists ff_q_pfp_execution_backward_result_coefficient_difference_witness_outputsecondentry. ub = ff_q_pfp_execution_backward_result_coefficient_difference_witness_outputsecondentry * S ((S (pfrep_position_execution_backward_result_coefficient_difference_witness_outputsecond)) * uc) + (pfrep_right_execution_backward_result_coefficient_difference_witness_output)))))) \/ (((exists pfrep_gap_execution_backward_result_coefficient_difference_witness_outputsecondoutside. pfrep_gap_execution_backward_result_coefficient_difference_witness_outputsecondoutside+(Lu)=(pfrep_power_execution_backward_result_coefficient_difference_witness_output)) /\ (((pfrep_right_execution_backward_result_coefficient_difference_witness_output)=0))))) -> pfrep_left_execution_backward_result_coefficient_difference_witness_output=pfrep_right_execution_backward_result_coefficient_difference_witness_output))))))))))))) /\ ((exists pfbz_left_code_execution_backward_result_bezout pfbz_left_scale_execution_backward_result_bezout pfbz_left_length_execution_backward_result_bezout pfbz_right_code_execution_backward_result_bezout pfbz_right_scale_execution_backward_result_bezout pfbz_right_length_execution_backward_result_bezout. ((((forall fom_index_pfp_execution_backward_result_bezout_left_productleft. (exists fom_gap_pfp_execution_backward_result_bezout_left_productleft_index_bound. fom_gap_pfp_execution_backward_result_bezout_left_productleft_index_bound + S (fom_index_pfp_execution_backward_result_bezout_left_productleft) = Lv) -> exists fom_value_pfp_execution_backward_result_bezout_left_productleft. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_left_productleft_entry. fom_beta_height_pfp_execution_backward_result_bezout_left_productleft_entry + S (fom_value_pfp_execution_backward_result_bezout_left_productleft) = S ((S (fom_index_pfp_execution_backward_result_bezout_left_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_left_productleft_entry. vb = fom_beta_quotient_pfp_execution_backward_result_bezout_left_productleft_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_left_productleft)) * vc) + (fom_value_pfp_execution_backward_result_bezout_left_productleft))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_left_productleft_value_bound. fom_gap_pfp_execution_backward_result_bezout_left_productleft_value_bound + S (fom_value_pfp_execution_backward_result_bezout_left_productleft) = p))) /\ (((forall fom_index_pfp_execution_backward_result_bezout_left_productright. (exists fom_gap_pfp_execution_backward_result_bezout_left_productright_index_bound. fom_gap_pfp_execution_backward_result_bezout_left_productright_index_bound + S (fom_index_pfp_execution_backward_result_bezout_left_productright) = La) -> exists fom_value_pfp_execution_backward_result_bezout_left_productright. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_left_productright_entry. fom_beta_height_pfp_execution_backward_result_bezout_left_productright_entry + S (fom_value_pfp_execution_backward_result_bezout_left_productright) = S ((S (fom_index_pfp_execution_backward_result_bezout_left_productright)) * ac)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_left_productright_entry. ab = fom_beta_quotient_pfp_execution_backward_result_bezout_left_productright_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_left_productright)) * ac) + (fom_value_pfp_execution_backward_result_bezout_left_productright))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_left_productright_value_bound. fom_gap_pfp_execution_backward_result_bezout_left_productright_value_bound + S (fom_value_pfp_execution_backward_result_bezout_left_productright) = p))) /\ (((((((Lv)=0 \/ (La)=0) /\ (((pfbz_left_length_execution_backward_result_bezout)=0)))) \/ (((~((Lv)=0)) /\ (((~((La)=0)) /\ (((Lv)+(La)=S (pfbz_left_length_execution_backward_result_bezout)))))))) /\ ((forall pfc_index_execution_backward_result_bezout_left_productcoefficients. (exists pfa_gap_execution_backward_result_bezout_left_productcoefficientsbound. pfa_gap_execution_backward_result_bezout_left_productcoefficientsbound + S (pfc_index_execution_backward_result_bezout_left_productcoefficients) = (pfbz_left_length_execution_backward_result_bezout)) -> exists pfc_value_execution_backward_result_bezout_left_productcoefficients. ((((exists ff_h_pfp_execution_backward_result_bezout_left_productcoefficientsentry. ff_h_pfp_execution_backward_result_bezout_left_productcoefficientsentry + S (pfc_value_execution_backward_result_bezout_left_productcoefficients) = S ((S (pfc_index_execution_backward_result_bezout_left_productcoefficients)) * pfbz_left_scale_execution_backward_result_bezout)) /\ exists ff_q_pfp_execution_backward_result_bezout_left_productcoefficientsentry. pfbz_left_code_execution_backward_result_bezout = ff_q_pfp_execution_backward_result_bezout_left_productcoefficientsentry * S ((S (pfc_index_execution_backward_result_bezout_left_productcoefficients)) * pfbz_left_scale_execution_backward_result_bezout) + (pfc_value_execution_backward_result_bezout_left_productcoefficients))) /\ ((exists pfc_terms_code_execution_backward_result_bezout_left_productcoefficientscoefficient pfc_terms_scale_execution_backward_result_bezout_left_productcoefficientscoefficient pfc_natural_sum_execution_backward_result_bezout_left_productcoefficientscoefficient. ((forall pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_backward_result_bezout_left_productcoefficients))) -> exists pfc_value_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_result_bezout_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_backward_result_bezout_left_productcoefficientscoefficient = ff_q_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_result_bezout_left_productcoefficientscoefficient) + (pfc_value_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm pfc_left_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm pfc_right_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)+pfc_complement_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_backward_result_bezout_left_productcoefficients)) /\ ((((((exists pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm) = (La)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightoutside+(La)=(pfc_complement_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonal)=pfc_left_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm*pfc_right_execution_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_backward_result_bezout_left_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_backward_result_bezout_left_productcoefficients))) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_backward_result_bezout_left_productcoefficients))) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_backward_result_bezout_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_backward_result_bezout_left_productcoefficients)) -> exists fs_a_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_result_bezout_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_backward_result_bezout_left_productcoefficientscoefficient = fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_result_bezout_left_productcoefficientscoefficient) + (fs_a_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum) + (fs_r_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum) + (fs_s_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientresiduebound. pfa_gap_execution_backward_result_bezout_left_productcoefficientscoefficientresiduebound + S (pfc_value_execution_backward_result_bezout_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_backward_result_bezout_left_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_backward_result_bezout_left_productcoefficients) + (p) * pfa_offset_right_execution_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_execution_backward_result_bezout_right_productleft. (exists fom_gap_pfp_execution_backward_result_bezout_right_productleft_index_bound. fom_gap_pfp_execution_backward_result_bezout_right_productleft_index_bound + S (fom_index_pfp_execution_backward_result_bezout_right_productleft) = pfbz_update_T_execution_backward_result) -> exists fom_value_pfp_execution_backward_result_bezout_right_productleft. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_right_productleft_entry. fom_beta_height_pfp_execution_backward_result_bezout_right_productleft_entry + S (fom_value_pfp_execution_backward_result_bezout_right_productleft) = S ((S (fom_index_pfp_execution_backward_result_bezout_right_productleft)) * pfbz_update_tc_execution_backward_result)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_right_productleft_entry. pfbz_update_tb_execution_backward_result = fom_beta_quotient_pfp_execution_backward_result_bezout_right_productleft_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_right_productleft)) * pfbz_update_tc_execution_backward_result) + (fom_value_pfp_execution_backward_result_bezout_right_productleft))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_right_productleft_value_bound. fom_gap_pfp_execution_backward_result_bezout_right_productleft_value_bound + S (fom_value_pfp_execution_backward_result_bezout_right_productleft) = p))) /\ (((forall fom_index_pfp_execution_backward_result_bezout_right_productright. (exists fom_gap_pfp_execution_backward_result_bezout_right_productright_index_bound. fom_gap_pfp_execution_backward_result_bezout_right_productright_index_bound + S (fom_index_pfp_execution_backward_result_bezout_right_productright) = S d) -> exists fom_value_pfp_execution_backward_result_bezout_right_productright. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_right_productright_entry. fom_beta_height_pfp_execution_backward_result_bezout_right_productright_entry + S (fom_value_pfp_execution_backward_result_bezout_right_productright) = S ((S (fom_index_pfp_execution_backward_result_bezout_right_productright)) * bc)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_right_productright_entry. bb = fom_beta_quotient_pfp_execution_backward_result_bezout_right_productright_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_right_productright)) * bc) + (fom_value_pfp_execution_backward_result_bezout_right_productright))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_right_productright_value_bound. fom_gap_pfp_execution_backward_result_bezout_right_productright_value_bound + S (fom_value_pfp_execution_backward_result_bezout_right_productright) = p))) /\ (((((((pfbz_update_T_execution_backward_result)=0 \/ (S d)=0) /\ (((pfbz_right_length_execution_backward_result_bezout)=0)))) \/ (((~((pfbz_update_T_execution_backward_result)=0)) /\ (((~((S d)=0)) /\ (((pfbz_update_T_execution_backward_result)+(S d)=S (pfbz_right_length_execution_backward_result_bezout)))))))) /\ ((forall pfc_index_execution_backward_result_bezout_right_productcoefficients. (exists pfa_gap_execution_backward_result_bezout_right_productcoefficientsbound. pfa_gap_execution_backward_result_bezout_right_productcoefficientsbound + S (pfc_index_execution_backward_result_bezout_right_productcoefficients) = (pfbz_right_length_execution_backward_result_bezout)) -> exists pfc_value_execution_backward_result_bezout_right_productcoefficients. ((((exists ff_h_pfp_execution_backward_result_bezout_right_productcoefficientsentry. ff_h_pfp_execution_backward_result_bezout_right_productcoefficientsentry + S (pfc_value_execution_backward_result_bezout_right_productcoefficients) = S ((S (pfc_index_execution_backward_result_bezout_right_productcoefficients)) * pfbz_right_scale_execution_backward_result_bezout)) /\ exists ff_q_pfp_execution_backward_result_bezout_right_productcoefficientsentry. pfbz_right_code_execution_backward_result_bezout = ff_q_pfp_execution_backward_result_bezout_right_productcoefficientsentry * S ((S (pfc_index_execution_backward_result_bezout_right_productcoefficients)) * pfbz_right_scale_execution_backward_result_bezout) + (pfc_value_execution_backward_result_bezout_right_productcoefficients))) /\ ((exists pfc_terms_code_execution_backward_result_bezout_right_productcoefficientscoefficient pfc_terms_scale_execution_backward_result_bezout_right_productcoefficientscoefficient pfc_natural_sum_execution_backward_result_bezout_right_productcoefficientscoefficient. ((forall pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_backward_result_bezout_right_productcoefficients))) -> exists pfc_value_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_result_bezout_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_backward_result_bezout_right_productcoefficientscoefficient = ff_q_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_backward_result_bezout_right_productcoefficientscoefficient) + (pfc_value_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm pfc_left_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm pfc_right_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)+pfc_complement_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_backward_result_bezout_right_productcoefficients)) /\ ((((((exists pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal) = (pfbz_update_T_execution_backward_result)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfbz_update_tc_execution_backward_result)) /\ exists ff_q_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry. pfbz_update_tb_execution_backward_result = ff_q_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfbz_update_tc_execution_backward_result) + (pfc_left_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfbz_update_T_execution_backward_result)=(pfc_index_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonal)=pfc_left_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm*pfc_right_execution_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_backward_result_bezout_right_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_backward_result_bezout_right_productcoefficients))) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_backward_result_bezout_right_productcoefficients))) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_backward_result_bezout_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_backward_result_bezout_right_productcoefficients)) -> exists fs_a_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_result_bezout_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_backward_result_bezout_right_productcoefficientscoefficient = fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_backward_result_bezout_right_productcoefficientscoefficient) + (fs_a_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum) + (fs_r_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum) + (fs_s_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientresiduebound. pfa_gap_execution_backward_result_bezout_right_productcoefficientscoefficientresiduebound + S (pfc_value_execution_backward_result_bezout_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_backward_result_bezout_right_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_backward_result_bezout_right_productcoefficients) + (p) * pfa_offset_right_execution_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_execution_backward_result_bezout_sum_left_bounded. (exists fom_gap_pfp_execution_backward_result_bezout_sum_left_bounded_index_bound. fom_gap_pfp_execution_backward_result_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_execution_backward_result_bezout_sum_left_bounded) = pfbz_left_length_execution_backward_result_bezout) -> exists fom_value_pfp_execution_backward_result_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_sum_left_bounded_entry. fom_beta_height_pfp_execution_backward_result_bezout_sum_left_bounded_entry + S (fom_value_pfp_execution_backward_result_bezout_sum_left_bounded) = S ((S (fom_index_pfp_execution_backward_result_bezout_sum_left_bounded)) * pfbz_left_scale_execution_backward_result_bezout)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_sum_left_bounded_entry. pfbz_left_code_execution_backward_result_bezout = fom_beta_quotient_pfp_execution_backward_result_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_sum_left_bounded)) * pfbz_left_scale_execution_backward_result_bezout) + (fom_value_pfp_execution_backward_result_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_sum_left_bounded_value_bound. fom_gap_pfp_execution_backward_result_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_execution_backward_result_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_execution_backward_result_bezout_sum_right_bounded. (exists fom_gap_pfp_execution_backward_result_bezout_sum_right_bounded_index_bound. fom_gap_pfp_execution_backward_result_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_execution_backward_result_bezout_sum_right_bounded) = pfbz_right_length_execution_backward_result_bezout) -> exists fom_value_pfp_execution_backward_result_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_sum_right_bounded_entry. fom_beta_height_pfp_execution_backward_result_bezout_sum_right_bounded_entry + S (fom_value_pfp_execution_backward_result_bezout_sum_right_bounded) = S ((S (fom_index_pfp_execution_backward_result_bezout_sum_right_bounded)) * pfbz_right_scale_execution_backward_result_bezout)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_sum_right_bounded_entry. pfbz_right_code_execution_backward_result_bezout = fom_beta_quotient_pfp_execution_backward_result_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_sum_right_bounded)) * pfbz_right_scale_execution_backward_result_bezout) + (fom_value_pfp_execution_backward_result_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_sum_right_bounded_value_bound. fom_gap_pfp_execution_backward_result_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_execution_backward_result_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_execution_backward_result_bezout_sum_result_bounded. (exists fom_gap_pfp_execution_backward_result_bezout_sum_result_bounded_index_bound. fom_gap_pfp_execution_backward_result_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_execution_backward_result_bezout_sum_result_bounded) = Lg) -> exists fom_value_pfp_execution_backward_result_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_execution_backward_result_bezout_sum_result_bounded_entry. fom_beta_height_pfp_execution_backward_result_bezout_sum_result_bounded_entry + S (fom_value_pfp_execution_backward_result_bezout_sum_result_bounded) = S ((S (fom_index_pfp_execution_backward_result_bezout_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_execution_backward_result_bezout_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_execution_backward_result_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_execution_backward_result_bezout_sum_result_bounded)) * gc) + (fom_value_pfp_execution_backward_result_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_execution_backward_result_bezout_sum_result_bounded_value_bound. fom_gap_pfp_execution_backward_result_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_execution_backward_result_bezout_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_execution_backward_result_bezout_sum pfaa_left_c_execution_backward_result_bezout_sum pfaa_right_b_execution_backward_result_bezout_sum pfaa_right_c_execution_backward_result_bezout_sum pfaa_sum_b_execution_backward_result_bezout_sum pfaa_sum_c_execution_backward_result_bezout_sum pfaa_length_execution_backward_result_bezout_sum. ((((forall pfrep_power_execution_backward_result_bezout_sum_witness_common_left pfrep_left_execution_backward_result_bezout_sum_witness_common_left pfrep_right_execution_backward_result_bezout_sum_witness_common_left. ((exists pfrep_position_execution_backward_result_bezout_sum_witness_common_leftfirst. ((pfrep_position_execution_backward_result_bezout_sum_witness_common_leftfirst+S (pfrep_power_execution_backward_result_bezout_sum_witness_common_left)=(pfbz_left_length_execution_backward_result_bezout)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_common_leftfirstentry. ff_h_pfp_execution_backward_result_bezout_sum_witness_common_leftfirstentry + S (pfrep_left_execution_backward_result_bezout_sum_witness_common_left) = S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_leftfirst)) * pfbz_left_scale_execution_backward_result_bezout)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_common_leftfirstentry. pfbz_left_code_execution_backward_result_bezout = ff_q_pfp_execution_backward_result_bezout_sum_witness_common_leftfirstentry * S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_leftfirst)) * pfbz_left_scale_execution_backward_result_bezout) + (pfrep_left_execution_backward_result_bezout_sum_witness_common_left)))))) \/ (((exists pfrep_gap_execution_backward_result_bezout_sum_witness_common_leftfirstoutside. pfrep_gap_execution_backward_result_bezout_sum_witness_common_leftfirstoutside+(pfbz_left_length_execution_backward_result_bezout)=(pfrep_power_execution_backward_result_bezout_sum_witness_common_left)) /\ (((pfrep_left_execution_backward_result_bezout_sum_witness_common_left)=0))))) -> ((exists pfrep_position_execution_backward_result_bezout_sum_witness_common_leftsecond. ((pfrep_position_execution_backward_result_bezout_sum_witness_common_leftsecond+S (pfrep_power_execution_backward_result_bezout_sum_witness_common_left)=(pfaa_length_execution_backward_result_bezout_sum)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_common_leftsecondentry. ff_h_pfp_execution_backward_result_bezout_sum_witness_common_leftsecondentry + S (pfrep_right_execution_backward_result_bezout_sum_witness_common_left) = S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_leftsecond)) * pfaa_left_c_execution_backward_result_bezout_sum)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_common_leftsecondentry. pfaa_left_b_execution_backward_result_bezout_sum = ff_q_pfp_execution_backward_result_bezout_sum_witness_common_leftsecondentry * S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_leftsecond)) * pfaa_left_c_execution_backward_result_bezout_sum) + (pfrep_right_execution_backward_result_bezout_sum_witness_common_left)))))) \/ (((exists pfrep_gap_execution_backward_result_bezout_sum_witness_common_leftsecondoutside. pfrep_gap_execution_backward_result_bezout_sum_witness_common_leftsecondoutside+(pfaa_length_execution_backward_result_bezout_sum)=(pfrep_power_execution_backward_result_bezout_sum_witness_common_left)) /\ (((pfrep_right_execution_backward_result_bezout_sum_witness_common_left)=0))))) -> pfrep_left_execution_backward_result_bezout_sum_witness_common_left=pfrep_right_execution_backward_result_bezout_sum_witness_common_left) /\ ((forall pfrep_power_execution_backward_result_bezout_sum_witness_common_right pfrep_left_execution_backward_result_bezout_sum_witness_common_right pfrep_right_execution_backward_result_bezout_sum_witness_common_right. ((exists pfrep_position_execution_backward_result_bezout_sum_witness_common_rightfirst. ((pfrep_position_execution_backward_result_bezout_sum_witness_common_rightfirst+S (pfrep_power_execution_backward_result_bezout_sum_witness_common_right)=(pfbz_right_length_execution_backward_result_bezout)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_common_rightfirstentry. ff_h_pfp_execution_backward_result_bezout_sum_witness_common_rightfirstentry + S (pfrep_left_execution_backward_result_bezout_sum_witness_common_right) = S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_rightfirst)) * pfbz_right_scale_execution_backward_result_bezout)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_common_rightfirstentry. pfbz_right_code_execution_backward_result_bezout = ff_q_pfp_execution_backward_result_bezout_sum_witness_common_rightfirstentry * S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_rightfirst)) * pfbz_right_scale_execution_backward_result_bezout) + (pfrep_left_execution_backward_result_bezout_sum_witness_common_right)))))) \/ (((exists pfrep_gap_execution_backward_result_bezout_sum_witness_common_rightfirstoutside. pfrep_gap_execution_backward_result_bezout_sum_witness_common_rightfirstoutside+(pfbz_right_length_execution_backward_result_bezout)=(pfrep_power_execution_backward_result_bezout_sum_witness_common_right)) /\ (((pfrep_left_execution_backward_result_bezout_sum_witness_common_right)=0))))) -> ((exists pfrep_position_execution_backward_result_bezout_sum_witness_common_rightsecond. ((pfrep_position_execution_backward_result_bezout_sum_witness_common_rightsecond+S (pfrep_power_execution_backward_result_bezout_sum_witness_common_right)=(pfaa_length_execution_backward_result_bezout_sum)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_common_rightsecondentry. ff_h_pfp_execution_backward_result_bezout_sum_witness_common_rightsecondentry + S (pfrep_right_execution_backward_result_bezout_sum_witness_common_right) = S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_rightsecond)) * pfaa_right_c_execution_backward_result_bezout_sum)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_common_rightsecondentry. pfaa_right_b_execution_backward_result_bezout_sum = ff_q_pfp_execution_backward_result_bezout_sum_witness_common_rightsecondentry * S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_common_rightsecond)) * pfaa_right_c_execution_backward_result_bezout_sum) + (pfrep_right_execution_backward_result_bezout_sum_witness_common_right)))))) \/ (((exists pfrep_gap_execution_backward_result_bezout_sum_witness_common_rightsecondoutside. pfrep_gap_execution_backward_result_bezout_sum_witness_common_rightsecondoutside+(pfaa_length_execution_backward_result_bezout_sum)=(pfrep_power_execution_backward_result_bezout_sum_witness_common_right)) /\ (((pfrep_right_execution_backward_result_bezout_sum_witness_common_right)=0))))) -> pfrep_left_execution_backward_result_bezout_sum_witness_common_right=pfrep_right_execution_backward_result_bezout_sum_witness_common_right)))) /\ (((forall pfp_index_execution_backward_result_bezout_sum_witness_operation. (exists pfa_gap_execution_backward_result_bezout_sum_witness_operationindex. pfa_gap_execution_backward_result_bezout_sum_witness_operationindex + S (pfp_index_execution_backward_result_bezout_sum_witness_operation) = (pfaa_length_execution_backward_result_bezout_sum)) -> exists pfp_left_execution_backward_result_bezout_sum_witness_operation pfp_right_execution_backward_result_bezout_sum_witness_operation pfp_value_execution_backward_result_bezout_sum_witness_operation. ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_operationleft. ff_h_pfp_execution_backward_result_bezout_sum_witness_operationleft + S (pfp_left_execution_backward_result_bezout_sum_witness_operation) = S ((S (pfp_index_execution_backward_result_bezout_sum_witness_operation)) * pfaa_left_c_execution_backward_result_bezout_sum)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_operationleft. pfaa_left_b_execution_backward_result_bezout_sum = ff_q_pfp_execution_backward_result_bezout_sum_witness_operationleft * S ((S (pfp_index_execution_backward_result_bezout_sum_witness_operation)) * pfaa_left_c_execution_backward_result_bezout_sum) + (pfp_left_execution_backward_result_bezout_sum_witness_operation))) /\ (((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_operationright. ff_h_pfp_execution_backward_result_bezout_sum_witness_operationright + S (pfp_right_execution_backward_result_bezout_sum_witness_operation) = S ((S (pfp_index_execution_backward_result_bezout_sum_witness_operation)) * pfaa_right_c_execution_backward_result_bezout_sum)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_operationright. pfaa_right_b_execution_backward_result_bezout_sum = ff_q_pfp_execution_backward_result_bezout_sum_witness_operationright * S ((S (pfp_index_execution_backward_result_bezout_sum_witness_operation)) * pfaa_right_c_execution_backward_result_bezout_sum) + (pfp_right_execution_backward_result_bezout_sum_witness_operation))) /\ (((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_operationtarget. ff_h_pfp_execution_backward_result_bezout_sum_witness_operationtarget + S (pfp_value_execution_backward_result_bezout_sum_witness_operation) = S ((S (pfp_index_execution_backward_result_bezout_sum_witness_operation)) * pfaa_sum_c_execution_backward_result_bezout_sum)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_operationtarget. pfaa_sum_b_execution_backward_result_bezout_sum = ff_q_pfp_execution_backward_result_bezout_sum_witness_operationtarget * S ((S (pfp_index_execution_backward_result_bezout_sum_witness_operation)) * pfaa_sum_c_execution_backward_result_bezout_sum) + (pfp_value_execution_backward_result_bezout_sum_witness_operation))) /\ ((((exists pfa_gap_execution_backward_result_bezout_sum_witness_operationoperationleft. pfa_gap_execution_backward_result_bezout_sum_witness_operationoperationleft + S (pfp_left_execution_backward_result_bezout_sum_witness_operation) = (p)) /\ (((exists pfa_gap_execution_backward_result_bezout_sum_witness_operationoperationright. pfa_gap_execution_backward_result_bezout_sum_witness_operationoperationright + S (pfp_right_execution_backward_result_bezout_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_execution_backward_result_bezout_sum_witness_operationoperationresultbound. pfa_gap_execution_backward_result_bezout_sum_witness_operationoperationresultbound + S (pfp_value_execution_backward_result_bezout_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_execution_backward_result_bezout_sum_witness_operationoperationresultcongruence pfa_offset_right_execution_backward_result_bezout_sum_witness_operationoperationresultcongruence. ((pfp_left_execution_backward_result_bezout_sum_witness_operation) + (pfp_right_execution_backward_result_bezout_sum_witness_operation)) + (p) * pfa_offset_left_execution_backward_result_bezout_sum_witness_operationoperationresultcongruence = (pfp_value_execution_backward_result_bezout_sum_witness_operation) + (p) * pfa_offset_right_execution_backward_result_bezout_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_execution_backward_result_bezout_sum_witness_output pfrep_left_execution_backward_result_bezout_sum_witness_output pfrep_right_execution_backward_result_bezout_sum_witness_output. ((exists pfrep_position_execution_backward_result_bezout_sum_witness_outputfirst. ((pfrep_position_execution_backward_result_bezout_sum_witness_outputfirst+S (pfrep_power_execution_backward_result_bezout_sum_witness_output)=(pfaa_length_execution_backward_result_bezout_sum)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_outputfirstentry. ff_h_pfp_execution_backward_result_bezout_sum_witness_outputfirstentry + S (pfrep_left_execution_backward_result_bezout_sum_witness_output) = S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_outputfirst)) * pfaa_sum_c_execution_backward_result_bezout_sum)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_outputfirstentry. pfaa_sum_b_execution_backward_result_bezout_sum = ff_q_pfp_execution_backward_result_bezout_sum_witness_outputfirstentry * S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_outputfirst)) * pfaa_sum_c_execution_backward_result_bezout_sum) + (pfrep_left_execution_backward_result_bezout_sum_witness_output)))))) \/ (((exists pfrep_gap_execution_backward_result_bezout_sum_witness_outputfirstoutside. pfrep_gap_execution_backward_result_bezout_sum_witness_outputfirstoutside+(pfaa_length_execution_backward_result_bezout_sum)=(pfrep_power_execution_backward_result_bezout_sum_witness_output)) /\ (((pfrep_left_execution_backward_result_bezout_sum_witness_output)=0))))) -> ((exists pfrep_position_execution_backward_result_bezout_sum_witness_outputsecond. ((pfrep_position_execution_backward_result_bezout_sum_witness_outputsecond+S (pfrep_power_execution_backward_result_bezout_sum_witness_output)=(Lg)) /\ ((((exists ff_h_pfp_execution_backward_result_bezout_sum_witness_outputsecondentry. ff_h_pfp_execution_backward_result_bezout_sum_witness_outputsecondentry + S (pfrep_right_execution_backward_result_bezout_sum_witness_output) = S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_execution_backward_result_bezout_sum_witness_outputsecondentry. gb = ff_q_pfp_execution_backward_result_bezout_sum_witness_outputsecondentry * S ((S (pfrep_position_execution_backward_result_bezout_sum_witness_outputsecond)) * gc) + (pfrep_right_execution_backward_result_bezout_sum_witness_output)))))) \/ (((exists pfrep_gap_execution_backward_result_bezout_sum_witness_outputsecondoutside. pfrep_gap_execution_backward_result_bezout_sum_witness_outputsecondoutside+(Lg)=(pfrep_power_execution_backward_result_bezout_sum_witness_output)) /\ (((pfrep_right_execution_backward_result_bezout_sum_witness_output)=0))))) -> pfrep_left_execution_backward_result_bezout_sum_witness_output=pfrep_right_execution_backward_result_bezout_sum_witness_output)))))))))))))))))))))))