prime_field_polynomial_division_execution_common_right_divisors

forall p ab ac L bb bc d qb qc q rb rc N db dc J. (~((p) = 1) /\ forall pfa_factor_left_execution_common_prime pfa_factor_right_execution_common_prime. (p) = pfa_factor_left_execution_common_prime * pfa_factor_right_execution_common_prime -> pfa_factor_left_execution_common_prime = 1 \/ pfa_factor_right_execution_common_prime = 1) -> (((forall fom_index_pfp_execution_common_actualinput. (exists fom_gap_pfp_execution_common_actualinput_index_bound. fom_gap_pfp_execution_common_actualinput_index_bound + S (fom_index_pfp_execution_common_actualinput) = L) -> exists fom_value_pfp_execution_common_actualinput. ((((exists fom_beta_height_pfp_execution_common_actualinput_entry. fom_beta_height_pfp_execution_common_actualinput_entry + S (fom_value_pfp_execution_common_actualinput) = S ((S (fom_index_pfp_execution_common_actualinput)) * ac)) /\ exists fom_beta_quotient_pfp_execution_common_actualinput_entry. ab = fom_beta_quotient_pfp_execution_common_actualinput_entry * S ((S (fom_index_pfp_execution_common_actualinput)) * ac) + (fom_value_pfp_execution_common_actualinput))) /\ (exists fom_gap_pfp_execution_common_actualinput_value_bound. fom_gap_pfp_execution_common_actualinput_value_bound + S (fom_value_pfp_execution_common_actualinput) = p))) /\ (((forall fom_index_pfp_execution_common_actualdivisor. (exists fom_gap_pfp_execution_common_actualdivisor_index_bound. fom_gap_pfp_execution_common_actualdivisor_index_bound + S (fom_index_pfp_execution_common_actualdivisor) = S (d)) -> exists fom_value_pfp_execution_common_actualdivisor. ((((exists fom_beta_height_pfp_execution_common_actualdivisor_entry. fom_beta_height_pfp_execution_common_actualdivisor_entry + S (fom_value_pfp_execution_common_actualdivisor) = S ((S (fom_index_pfp_execution_common_actualdivisor)) * bc)) /\ exists fom_beta_quotient_pfp_execution_common_actualdivisor_entry. bb = fom_beta_quotient_pfp_execution_common_actualdivisor_entry * S ((S (fom_index_pfp_execution_common_actualdivisor)) * bc) + (fom_value_pfp_execution_common_actualdivisor))) /\ (exists fom_gap_pfp_execution_common_actualdivisor_value_bound. fom_gap_pfp_execution_common_actualdivisor_value_bound + S (fom_value_pfp_execution_common_actualdivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_execution_common_actuallengthshort. pfc_gap_execution_common_actuallengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_execution_common_actual pfd_inverse_execution_common_actual pfd_product_code_execution_common_actual pfd_product_scale_execution_common_actual pfd_residual_code_execution_common_actual pfd_residual_scale_execution_common_actual pfd_cut_execution_common_actual. ((((exists ff_h_pfp_execution_common_actualhead. ff_h_pfp_execution_common_actualhead + S (pfd_head_execution_common_actual) = S ((S (0)) * bc)) /\ exists ff_q_pfp_execution_common_actualhead. bb = ff_q_pfp_execution_common_actualhead * S ((S (0)) * bc) + (pfd_head_execution_common_actual))) /\ (((((~((pfd_head_execution_common_actual) = 0)) /\ ((((exists pfa_gap_execution_common_actualinversemultiplicationleft. pfa_gap_execution_common_actualinversemultiplicationleft + S (pfd_head_execution_common_actual) = (p)) /\ (((exists pfa_gap_execution_common_actualinversemultiplicationright. pfa_gap_execution_common_actualinversemultiplicationright + S (pfd_inverse_execution_common_actual) = (p)) /\ ((((exists pfa_gap_execution_common_actualinversemultiplicationresultbound. pfa_gap_execution_common_actualinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_execution_common_actualinversemultiplicationresultcongruence pfa_offset_right_execution_common_actualinversemultiplicationresultcongruence. ((pfd_head_execution_common_actual) * (pfd_inverse_execution_common_actual)) + (p) * pfa_offset_left_execution_common_actualinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_execution_common_actualinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_execution_common_actualquotient. (exists pfa_gap_execution_common_actualquotientbound. pfa_gap_execution_common_actualquotientbound + S (pfd_index_execution_common_actualquotient) = (q)) -> exists pfd_value_execution_common_actualquotient. ((((exists ff_h_pfp_execution_common_actualquotiententry. ff_h_pfp_execution_common_actualquotiententry + S (pfd_value_execution_common_actualquotient) = S ((S (pfd_index_execution_common_actualquotient)) * qc)) /\ exists ff_q_pfp_execution_common_actualquotiententry. qb = ff_q_pfp_execution_common_actualquotiententry * S ((S (pfd_index_execution_common_actualquotient)) * qc) + (pfd_value_execution_common_actualquotient))) /\ ((exists pfd_input_execution_common_actualquotientstep pfd_previous_execution_common_actualquotientstep pfd_difference_execution_common_actualquotientstep. ((((exists ff_h_pfp_execution_common_actualquotientstepinput. ff_h_pfp_execution_common_actualquotientstepinput + S (pfd_input_execution_common_actualquotientstep) = S ((S (pfd_index_execution_common_actualquotient)) * ac)) /\ exists ff_q_pfp_execution_common_actualquotientstepinput. ab = ff_q_pfp_execution_common_actualquotientstepinput * S ((S (pfd_index_execution_common_actualquotient)) * ac) + (pfd_input_execution_common_actualquotientstep))) /\ (((exists pfc_terms_code_execution_common_actualquotientstepprevious pfc_terms_scale_execution_common_actualquotientstepprevious pfc_natural_sum_execution_common_actualquotientstepprevious. ((forall pfc_index_execution_common_actualquotientsteppreviousdiagonal. (exists pfa_gap_execution_common_actualquotientsteppreviousdiagonalbound. pfa_gap_execution_common_actualquotientsteppreviousdiagonalbound + S (pfc_index_execution_common_actualquotientsteppreviousdiagonal) = (S (pfd_index_execution_common_actualquotient))) -> exists pfc_value_execution_common_actualquotientsteppreviousdiagonal. ((((exists ff_h_pfp_execution_common_actualquotientsteppreviousdiagonalentry. ff_h_pfp_execution_common_actualquotientsteppreviousdiagonalentry + S (pfc_value_execution_common_actualquotientsteppreviousdiagonal) = S ((S (pfc_index_execution_common_actualquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_common_actualquotientstepprevious)) /\ exists ff_q_pfp_execution_common_actualquotientsteppreviousdiagonalentry. pfc_terms_code_execution_common_actualquotientstepprevious = ff_q_pfp_execution_common_actualquotientsteppreviousdiagonalentry * S ((S (pfc_index_execution_common_actualquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_common_actualquotientstepprevious) + (pfc_value_execution_common_actualquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_execution_common_actualquotientsteppreviousdiagonalterm pfc_left_execution_common_actualquotientsteppreviousdiagonalterm pfc_right_execution_common_actualquotientsteppreviousdiagonalterm. (((pfc_index_execution_common_actualquotientsteppreviousdiagonal)+pfc_complement_execution_common_actualquotientsteppreviousdiagonalterm=(pfd_index_execution_common_actualquotient)) /\ ((((((exists pfa_gap_execution_common_actualquotientsteppreviousdiagonaltermleftinside. pfa_gap_execution_common_actualquotientsteppreviousdiagonaltermleftinside + S (pfc_index_execution_common_actualquotientsteppreviousdiagonal) = (pfd_index_execution_common_actualquotient)) /\ ((((exists ff_h_pfp_execution_common_actualquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_execution_common_actualquotientsteppreviousdiagonaltermleftentry + S (pfc_left_execution_common_actualquotientsteppreviousdiagonalterm) = S ((S (pfc_index_execution_common_actualquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_execution_common_actualquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_execution_common_actualquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_execution_common_actualquotientsteppreviousdiagonal)) * qc) + (pfc_left_execution_common_actualquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_actualquotientsteppreviousdiagonaltermleftoutside. pfc_gap_execution_common_actualquotientsteppreviousdiagonaltermleftoutside+(pfd_index_execution_common_actualquotient)=(pfc_index_execution_common_actualquotientsteppreviousdiagonal)) /\ (((pfc_left_execution_common_actualquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_actualquotientsteppreviousdiagonaltermrightinside. pfa_gap_execution_common_actualquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_execution_common_actualquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_common_actualquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_execution_common_actualquotientsteppreviousdiagonaltermrightentry + S (pfc_right_execution_common_actualquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_execution_common_actualquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_common_actualquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_execution_common_actualquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_execution_common_actualquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_execution_common_actualquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_actualquotientsteppreviousdiagonaltermrightoutside. pfc_gap_execution_common_actualquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_common_actualquotientsteppreviousdiagonalterm)) /\ (((pfc_right_execution_common_actualquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_execution_common_actualquotientsteppreviousdiagonal)=pfc_left_execution_common_actualquotientsteppreviousdiagonalterm*pfc_right_execution_common_actualquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_actualquotientstepprevioussum fs_v_pfc_execution_common_actualquotientstepprevioussum. ((((exists fs_h_pfc_execution_common_actualquotientstepprevioussum_body_start. fs_h_pfc_execution_common_actualquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_common_actualquotientstepprevioussum_body_start. fs_u_pfc_execution_common_actualquotientstepprevioussum = fs_q_pfc_execution_common_actualquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_execution_common_actualquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_execution_common_actualquotientstepprevioussum_body_terminal. fs_h_pfc_execution_common_actualquotientstepprevioussum_body_terminal + S (pfc_natural_sum_execution_common_actualquotientstepprevious) = S ((S (S (pfd_index_execution_common_actualquotient))) * fs_v_pfc_execution_common_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_common_actualquotientstepprevioussum_body_terminal. fs_u_pfc_execution_common_actualquotientstepprevioussum = fs_q_pfc_execution_common_actualquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_execution_common_actualquotient))) * fs_v_pfc_execution_common_actualquotientstepprevioussum) + (pfc_natural_sum_execution_common_actualquotientstepprevious))) /\ forall fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps. (exists fs_lt_pfc_execution_common_actualquotientstepprevioussum_body_steps_bound. fs_lt_pfc_execution_common_actualquotientstepprevioussum_body_steps_bound + S fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps = S (pfd_index_execution_common_actualquotient)) -> exists fs_a_pfc_execution_common_actualquotientstepprevioussum_body_steps fs_r_pfc_execution_common_actualquotientstepprevioussum_body_steps fs_s_pfc_execution_common_actualquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_execution_common_actualquotientstepprevioussum_body_steps_summand. fs_h_pfc_execution_common_actualquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_execution_common_actualquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_common_actualquotientstepprevious)) /\ exists fs_q_pfc_execution_common_actualquotientstepprevioussum_body_steps_summand. pfc_terms_code_execution_common_actualquotientstepprevious = fs_q_pfc_execution_common_actualquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_common_actualquotientstepprevious) + (fs_a_pfc_execution_common_actualquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_actualquotientstepprevioussum_body_steps_partial. fs_h_pfc_execution_common_actualquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_execution_common_actualquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_common_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_common_actualquotientstepprevioussum_body_steps_partial. fs_u_pfc_execution_common_actualquotientstepprevioussum = fs_q_pfc_execution_common_actualquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_common_actualquotientstepprevioussum) + (fs_r_pfc_execution_common_actualquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_actualquotientstepprevioussum_body_steps_successor. fs_h_pfc_execution_common_actualquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_execution_common_actualquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_common_actualquotientstepprevioussum)) /\ exists fs_q_pfc_execution_common_actualquotientstepprevioussum_body_steps_successor. fs_u_pfc_execution_common_actualquotientstepprevioussum = fs_q_pfc_execution_common_actualquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_actualquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_common_actualquotientstepprevioussum) + (fs_s_pfc_execution_common_actualquotientstepprevioussum_body_steps))) /\ fs_s_pfc_execution_common_actualquotientstepprevioussum_body_steps = fs_r_pfc_execution_common_actualquotientstepprevioussum_body_steps + fs_a_pfc_execution_common_actualquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_actualquotientsteppreviousresiduebound. pfa_gap_execution_common_actualquotientsteppreviousresiduebound + S (pfd_previous_execution_common_actualquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_common_actualquotientsteppreviousresiduecongruence pfa_offset_right_execution_common_actualquotientsteppreviousresiduecongruence. (pfc_natural_sum_execution_common_actualquotientstepprevious) + (p) * pfa_offset_left_execution_common_actualquotientsteppreviousresiduecongruence = (pfd_previous_execution_common_actualquotientstep) + (p) * pfa_offset_right_execution_common_actualquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_execution_common_actualquotientstepsubtractleft. pfa_gap_execution_common_actualquotientstepsubtractleft + S (pfd_previous_execution_common_actualquotientstep) = (p)) /\ (((exists pfa_gap_execution_common_actualquotientstepsubtractright. pfa_gap_execution_common_actualquotientstepsubtractright + S (pfd_difference_execution_common_actualquotientstep) = (p)) /\ ((((exists pfa_gap_execution_common_actualquotientstepsubtractresultbound. pfa_gap_execution_common_actualquotientstepsubtractresultbound + S (pfd_input_execution_common_actualquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_common_actualquotientstepsubtractresultcongruence pfa_offset_right_execution_common_actualquotientstepsubtractresultcongruence. ((pfd_previous_execution_common_actualquotientstep) + (pfd_difference_execution_common_actualquotientstep)) + (p) * pfa_offset_left_execution_common_actualquotientstepsubtractresultcongruence = (pfd_input_execution_common_actualquotientstep) + (p) * pfa_offset_right_execution_common_actualquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_execution_common_actualquotientstepmultiplyleft. pfa_gap_execution_common_actualquotientstepmultiplyleft + S (pfd_inverse_execution_common_actual) = (p)) /\ (((exists pfa_gap_execution_common_actualquotientstepmultiplyright. pfa_gap_execution_common_actualquotientstepmultiplyright + S (pfd_difference_execution_common_actualquotientstep) = (p)) /\ ((((exists pfa_gap_execution_common_actualquotientstepmultiplyresultbound. pfa_gap_execution_common_actualquotientstepmultiplyresultbound + S (pfd_value_execution_common_actualquotient) = (p)) /\ ((exists pfa_offset_left_execution_common_actualquotientstepmultiplyresultcongruence pfa_offset_right_execution_common_actualquotientstepmultiplyresultcongruence. ((pfd_inverse_execution_common_actual) * (pfd_difference_execution_common_actualquotientstep)) + (p) * pfa_offset_left_execution_common_actualquotientstepmultiplyresultcongruence = (pfd_value_execution_common_actualquotient) + (p) * pfa_offset_right_execution_common_actualquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_execution_common_actualproduct. (exists pfa_gap_execution_common_actualproductbound. pfa_gap_execution_common_actualproductbound + S (pfc_index_execution_common_actualproduct) = (L)) -> exists pfc_value_execution_common_actualproduct. ((((exists ff_h_pfp_execution_common_actualproductentry. ff_h_pfp_execution_common_actualproductentry + S (pfc_value_execution_common_actualproduct) = S ((S (pfc_index_execution_common_actualproduct)) * pfd_product_scale_execution_common_actual)) /\ exists ff_q_pfp_execution_common_actualproductentry. pfd_product_code_execution_common_actual = ff_q_pfp_execution_common_actualproductentry * S ((S (pfc_index_execution_common_actualproduct)) * pfd_product_scale_execution_common_actual) + (pfc_value_execution_common_actualproduct))) /\ ((exists pfc_terms_code_execution_common_actualproductcoefficient pfc_terms_scale_execution_common_actualproductcoefficient pfc_natural_sum_execution_common_actualproductcoefficient. ((forall pfc_index_execution_common_actualproductcoefficientdiagonal. (exists pfa_gap_execution_common_actualproductcoefficientdiagonalbound. pfa_gap_execution_common_actualproductcoefficientdiagonalbound + S (pfc_index_execution_common_actualproductcoefficientdiagonal) = (S (pfc_index_execution_common_actualproduct))) -> exists pfc_value_execution_common_actualproductcoefficientdiagonal. ((((exists ff_h_pfp_execution_common_actualproductcoefficientdiagonalentry. ff_h_pfp_execution_common_actualproductcoefficientdiagonalentry + S (pfc_value_execution_common_actualproductcoefficientdiagonal) = S ((S (pfc_index_execution_common_actualproductcoefficientdiagonal)) * pfc_terms_scale_execution_common_actualproductcoefficient)) /\ exists ff_q_pfp_execution_common_actualproductcoefficientdiagonalentry. pfc_terms_code_execution_common_actualproductcoefficient = ff_q_pfp_execution_common_actualproductcoefficientdiagonalentry * S ((S (pfc_index_execution_common_actualproductcoefficientdiagonal)) * pfc_terms_scale_execution_common_actualproductcoefficient) + (pfc_value_execution_common_actualproductcoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_actualproductcoefficientdiagonalterm pfc_left_execution_common_actualproductcoefficientdiagonalterm pfc_right_execution_common_actualproductcoefficientdiagonalterm. (((pfc_index_execution_common_actualproductcoefficientdiagonal)+pfc_complement_execution_common_actualproductcoefficientdiagonalterm=(pfc_index_execution_common_actualproduct)) /\ ((((((exists pfa_gap_execution_common_actualproductcoefficientdiagonaltermleftinside. pfa_gap_execution_common_actualproductcoefficientdiagonaltermleftinside + S (pfc_index_execution_common_actualproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_execution_common_actualproductcoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_actualproductcoefficientdiagonaltermleftentry + S (pfc_left_execution_common_actualproductcoefficientdiagonalterm) = S ((S (pfc_index_execution_common_actualproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_execution_common_actualproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_execution_common_actualproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_actualproductcoefficientdiagonal)) * qc) + (pfc_left_execution_common_actualproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_actualproductcoefficientdiagonaltermleftoutside. pfc_gap_execution_common_actualproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_execution_common_actualproductcoefficientdiagonal)) /\ (((pfc_left_execution_common_actualproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_actualproductcoefficientdiagonaltermrightinside. pfa_gap_execution_common_actualproductcoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_actualproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_common_actualproductcoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_actualproductcoefficientdiagonaltermrightentry + S (pfc_right_execution_common_actualproductcoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_actualproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_common_actualproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_common_actualproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_actualproductcoefficientdiagonalterm)) * bc) + (pfc_right_execution_common_actualproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_actualproductcoefficientdiagonaltermrightoutside. pfc_gap_execution_common_actualproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_common_actualproductcoefficientdiagonalterm)) /\ (((pfc_right_execution_common_actualproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_actualproductcoefficientdiagonal)=pfc_left_execution_common_actualproductcoefficientdiagonalterm*pfc_right_execution_common_actualproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_actualproductcoefficientsum fs_v_pfc_execution_common_actualproductcoefficientsum. ((((exists fs_h_pfc_execution_common_actualproductcoefficientsum_body_start. fs_h_pfc_execution_common_actualproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_common_actualproductcoefficientsum_body_start. fs_u_pfc_execution_common_actualproductcoefficientsum = fs_q_pfc_execution_common_actualproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_actualproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_actualproductcoefficientsum_body_terminal. fs_h_pfc_execution_common_actualproductcoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_actualproductcoefficient) = S ((S (S (pfc_index_execution_common_actualproduct))) * fs_v_pfc_execution_common_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_common_actualproductcoefficientsum_body_terminal. fs_u_pfc_execution_common_actualproductcoefficientsum = fs_q_pfc_execution_common_actualproductcoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_actualproduct))) * fs_v_pfc_execution_common_actualproductcoefficientsum) + (pfc_natural_sum_execution_common_actualproductcoefficient))) /\ forall fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_actualproductcoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_actualproductcoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps = S (pfc_index_execution_common_actualproduct)) -> exists fs_a_pfc_execution_common_actualproductcoefficientsum_body_steps fs_r_pfc_execution_common_actualproductcoefficientsum_body_steps fs_s_pfc_execution_common_actualproductcoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_actualproductcoefficientsum_body_steps_summand. fs_h_pfc_execution_common_actualproductcoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_actualproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_common_actualproductcoefficient)) /\ exists fs_q_pfc_execution_common_actualproductcoefficientsum_body_steps_summand. pfc_terms_code_execution_common_actualproductcoefficient = fs_q_pfc_execution_common_actualproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_common_actualproductcoefficient) + (fs_a_pfc_execution_common_actualproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_actualproductcoefficientsum_body_steps_partial. fs_h_pfc_execution_common_actualproductcoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_actualproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_common_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_common_actualproductcoefficientsum_body_steps_partial. fs_u_pfc_execution_common_actualproductcoefficientsum = fs_q_pfc_execution_common_actualproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_common_actualproductcoefficientsum) + (fs_r_pfc_execution_common_actualproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_actualproductcoefficientsum_body_steps_successor. fs_h_pfc_execution_common_actualproductcoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_actualproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_common_actualproductcoefficientsum)) /\ exists fs_q_pfc_execution_common_actualproductcoefficientsum_body_steps_successor. fs_u_pfc_execution_common_actualproductcoefficientsum = fs_q_pfc_execution_common_actualproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_actualproductcoefficientsum_body_steps)) * fs_v_pfc_execution_common_actualproductcoefficientsum) + (fs_s_pfc_execution_common_actualproductcoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_actualproductcoefficientsum_body_steps = fs_r_pfc_execution_common_actualproductcoefficientsum_body_steps + fs_a_pfc_execution_common_actualproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_actualproductcoefficientresiduebound. pfa_gap_execution_common_actualproductcoefficientresiduebound + S (pfc_value_execution_common_actualproduct) = (p)) /\ ((exists pfa_offset_left_execution_common_actualproductcoefficientresiduecongruence pfa_offset_right_execution_common_actualproductcoefficientresiduecongruence. (pfc_natural_sum_execution_common_actualproductcoefficient) + (p) * pfa_offset_left_execution_common_actualproductcoefficientresiduecongruence = (pfc_value_execution_common_actualproduct) + (p) * pfa_offset_right_execution_common_actualproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_execution_common_actualdifference. (exists pfa_gap_execution_common_actualdifferenceindex. pfa_gap_execution_common_actualdifferenceindex + S (pfs_index_execution_common_actualdifference) = (L)) -> exists pfs_left_execution_common_actualdifference pfs_right_execution_common_actualdifference pfs_result_execution_common_actualdifference. ((((exists ff_h_pfp_execution_common_actualdifferenceleft. ff_h_pfp_execution_common_actualdifferenceleft + S (pfs_left_execution_common_actualdifference) = S ((S (pfs_index_execution_common_actualdifference)) * ac)) /\ exists ff_q_pfp_execution_common_actualdifferenceleft. ab = ff_q_pfp_execution_common_actualdifferenceleft * S ((S (pfs_index_execution_common_actualdifference)) * ac) + (pfs_left_execution_common_actualdifference))) /\ (((((exists ff_h_pfp_execution_common_actualdifferenceright. ff_h_pfp_execution_common_actualdifferenceright + S (pfs_right_execution_common_actualdifference) = S ((S (pfs_index_execution_common_actualdifference)) * pfd_product_scale_execution_common_actual)) /\ exists ff_q_pfp_execution_common_actualdifferenceright. pfd_product_code_execution_common_actual = ff_q_pfp_execution_common_actualdifferenceright * S ((S (pfs_index_execution_common_actualdifference)) * pfd_product_scale_execution_common_actual) + (pfs_right_execution_common_actualdifference))) /\ (((((exists ff_h_pfp_execution_common_actualdifferenceresult. ff_h_pfp_execution_common_actualdifferenceresult + S (pfs_result_execution_common_actualdifference) = S ((S (pfs_index_execution_common_actualdifference)) * pfd_residual_scale_execution_common_actual)) /\ exists ff_q_pfp_execution_common_actualdifferenceresult. pfd_residual_code_execution_common_actual = ff_q_pfp_execution_common_actualdifferenceresult * S ((S (pfs_index_execution_common_actualdifference)) * pfd_residual_scale_execution_common_actual) + (pfs_result_execution_common_actualdifference))) /\ ((((exists pfa_gap_execution_common_actualdifferenceoperationleft. pfa_gap_execution_common_actualdifferenceoperationleft + S (pfs_right_execution_common_actualdifference) = (p)) /\ (((exists pfa_gap_execution_common_actualdifferenceoperationright. pfa_gap_execution_common_actualdifferenceoperationright + S (pfs_result_execution_common_actualdifference) = (p)) /\ ((((exists pfa_gap_execution_common_actualdifferenceoperationresultbound. pfa_gap_execution_common_actualdifferenceoperationresultbound + S (pfs_left_execution_common_actualdifference) = (p)) /\ ((exists pfa_offset_left_execution_common_actualdifferenceoperationresultcongruence pfa_offset_right_execution_common_actualdifferenceoperationresultcongruence. ((pfs_right_execution_common_actualdifference) + (pfs_result_execution_common_actualdifference)) + (p) * pfa_offset_left_execution_common_actualdifferenceoperationresultcongruence = (pfs_left_execution_common_actualdifference) + (p) * pfa_offset_right_execution_common_actualdifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_execution_common_actual)+(N)) /\ (((forall fom_index_pfp_execution_common_actualtriminput. (exists fom_gap_pfp_execution_common_actualtriminput_index_bound. fom_gap_pfp_execution_common_actualtriminput_index_bound + S (fom_index_pfp_execution_common_actualtriminput) = L) -> exists fom_value_pfp_execution_common_actualtriminput. ((((exists fom_beta_height_pfp_execution_common_actualtriminput_entry. fom_beta_height_pfp_execution_common_actualtriminput_entry + S (fom_value_pfp_execution_common_actualtriminput) = S ((S (fom_index_pfp_execution_common_actualtriminput)) * pfd_residual_scale_execution_common_actual)) /\ exists fom_beta_quotient_pfp_execution_common_actualtriminput_entry. pfd_residual_code_execution_common_actual = fom_beta_quotient_pfp_execution_common_actualtriminput_entry * S ((S (fom_index_pfp_execution_common_actualtriminput)) * pfd_residual_scale_execution_common_actual) + (fom_value_pfp_execution_common_actualtriminput))) /\ (exists fom_gap_pfp_execution_common_actualtriminput_value_bound. fom_gap_pfp_execution_common_actualtriminput_value_bound + S (fom_value_pfp_execution_common_actualtriminput) = p))) /\ (((forall pfp_repeat_index_execution_common_actualtrimremoved. (exists pfa_gap_execution_common_actualtrimremovedindex. pfa_gap_execution_common_actualtrimremovedindex + S (pfp_repeat_index_execution_common_actualtrimremoved) = (pfd_cut_execution_common_actual)) -> (((exists ff_h_pfp_execution_common_actualtrimremovedentry. ff_h_pfp_execution_common_actualtrimremovedentry + S (0) = S ((S (pfp_repeat_index_execution_common_actualtrimremoved)) * pfd_residual_scale_execution_common_actual)) /\ exists ff_q_pfp_execution_common_actualtrimremovedentry. pfd_residual_code_execution_common_actual = ff_q_pfp_execution_common_actualtrimremovedentry * S ((S (pfp_repeat_index_execution_common_actualtrimremoved)) * pfd_residual_scale_execution_common_actual) + (0)))) /\ (((forall pftrim_index_execution_common_actualtrimsuffix pftrim_value_execution_common_actualtrimsuffix. (exists pfa_gap_execution_common_actualtrimsuffixbound. pfa_gap_execution_common_actualtrimsuffixbound + S (pftrim_index_execution_common_actualtrimsuffix) = (N)) -> (((exists ff_h_pfp_execution_common_actualtrimsuffixsource. ff_h_pfp_execution_common_actualtrimsuffixsource + S (pftrim_value_execution_common_actualtrimsuffix) = S ((S ((pfd_cut_execution_common_actual)+pftrim_index_execution_common_actualtrimsuffix)) * pfd_residual_scale_execution_common_actual)) /\ exists ff_q_pfp_execution_common_actualtrimsuffixsource. pfd_residual_code_execution_common_actual = ff_q_pfp_execution_common_actualtrimsuffixsource * S ((S ((pfd_cut_execution_common_actual)+pftrim_index_execution_common_actualtrimsuffix)) * pfd_residual_scale_execution_common_actual) + (pftrim_value_execution_common_actualtrimsuffix))) -> (((exists ff_h_pfp_execution_common_actualtrimsuffixoutput. ff_h_pfp_execution_common_actualtrimsuffixoutput + S (pftrim_value_execution_common_actualtrimsuffix) = S ((S (pftrim_index_execution_common_actualtrimsuffix)) * rc)) /\ exists ff_q_pfp_execution_common_actualtrimsuffixoutput. rb = ff_q_pfp_execution_common_actualtrimsuffixoutput * S ((S (pftrim_index_execution_common_actualtrimsuffix)) * rc) + (pftrim_value_execution_common_actualtrimsuffix)))) /\ (((N)=0 \/ (exists pftrim_leading_execution_common_actualtrimnormal. ((((exists ff_h_pfp_execution_common_actualtrimnormalentry. ff_h_pfp_execution_common_actualtrimnormalentry + S (pftrim_leading_execution_common_actualtrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_execution_common_actualtrimnormalentry. rb = ff_q_pfp_execution_common_actualtrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_execution_common_actualtrimnormal))) /\ ((~(pftrim_leading_execution_common_actualtrimnormal=0))))))))))))))))))))))))))))))))) -> ((((((((forall fom_index_pfp_execution_common_source_left_canonical. (exists fom_gap_pfp_execution_common_source_left_canonical_index_bound. fom_gap_pfp_execution_common_source_left_canonical_index_bound + S (fom_index_pfp_execution_common_source_left_canonical) = L) -> exists fom_value_pfp_execution_common_source_left_canonical. ((((exists fom_beta_height_pfp_execution_common_source_left_canonical_entry. fom_beta_height_pfp_execution_common_source_left_canonical_entry + S (fom_value_pfp_execution_common_source_left_canonical) = S ((S (fom_index_pfp_execution_common_source_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_execution_common_source_left_canonical_entry. ab = fom_beta_quotient_pfp_execution_common_source_left_canonical_entry * S ((S (fom_index_pfp_execution_common_source_left_canonical)) * ac) + (fom_value_pfp_execution_common_source_left_canonical))) /\ (exists fom_gap_pfp_execution_common_source_left_canonical_value_bound. fom_gap_pfp_execution_common_source_left_canonical_value_bound + S (fom_value_pfp_execution_common_source_left_canonical) = p))) /\ ((exists pfrd_qb_execution_common_source_left pfrd_qc_execution_common_source_left pfrd_qlen_execution_common_source_left pfrd_pb_execution_common_source_left pfrd_pc_execution_common_source_left pfrd_plen_execution_common_source_left. ((((forall fom_index_pfp_execution_common_source_left_productleft. (exists fom_gap_pfp_execution_common_source_left_productleft_index_bound. fom_gap_pfp_execution_common_source_left_productleft_index_bound + S (fom_index_pfp_execution_common_source_left_productleft) = pfrd_qlen_execution_common_source_left) -> exists fom_value_pfp_execution_common_source_left_productleft. ((((exists fom_beta_height_pfp_execution_common_source_left_productleft_entry. fom_beta_height_pfp_execution_common_source_left_productleft_entry + S (fom_value_pfp_execution_common_source_left_productleft) = S ((S (fom_index_pfp_execution_common_source_left_productleft)) * pfrd_qc_execution_common_source_left)) /\ exists fom_beta_quotient_pfp_execution_common_source_left_productleft_entry. pfrd_qb_execution_common_source_left = fom_beta_quotient_pfp_execution_common_source_left_productleft_entry * S ((S (fom_index_pfp_execution_common_source_left_productleft)) * pfrd_qc_execution_common_source_left) + (fom_value_pfp_execution_common_source_left_productleft))) /\ (exists fom_gap_pfp_execution_common_source_left_productleft_value_bound. fom_gap_pfp_execution_common_source_left_productleft_value_bound + S (fom_value_pfp_execution_common_source_left_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_source_left_productright. (exists fom_gap_pfp_execution_common_source_left_productright_index_bound. fom_gap_pfp_execution_common_source_left_productright_index_bound + S (fom_index_pfp_execution_common_source_left_productright) = J) -> exists fom_value_pfp_execution_common_source_left_productright. ((((exists fom_beta_height_pfp_execution_common_source_left_productright_entry. fom_beta_height_pfp_execution_common_source_left_productright_entry + S (fom_value_pfp_execution_common_source_left_productright) = S ((S (fom_index_pfp_execution_common_source_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_source_left_productright_entry. db = fom_beta_quotient_pfp_execution_common_source_left_productright_entry * S ((S (fom_index_pfp_execution_common_source_left_productright)) * dc) + (fom_value_pfp_execution_common_source_left_productright))) /\ (exists fom_gap_pfp_execution_common_source_left_productright_value_bound. fom_gap_pfp_execution_common_source_left_productright_value_bound + S (fom_value_pfp_execution_common_source_left_productright) = p))) /\ (((((((pfrd_qlen_execution_common_source_left)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_source_left)=0)))) \/ (((~((pfrd_qlen_execution_common_source_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_source_left)+(J)=S (pfrd_plen_execution_common_source_left)))))))) /\ ((forall pfc_index_execution_common_source_left_productcoefficients. (exists pfa_gap_execution_common_source_left_productcoefficientsbound. pfa_gap_execution_common_source_left_productcoefficientsbound + S (pfc_index_execution_common_source_left_productcoefficients) = (pfrd_plen_execution_common_source_left)) -> exists pfc_value_execution_common_source_left_productcoefficients. ((((exists ff_h_pfp_execution_common_source_left_productcoefficientsentry. ff_h_pfp_execution_common_source_left_productcoefficientsentry + S (pfc_value_execution_common_source_left_productcoefficients) = S ((S (pfc_index_execution_common_source_left_productcoefficients)) * pfrd_pc_execution_common_source_left)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientsentry. pfrd_pb_execution_common_source_left = ff_q_pfp_execution_common_source_left_productcoefficientsentry * S ((S (pfc_index_execution_common_source_left_productcoefficients)) * pfrd_pc_execution_common_source_left) + (pfc_value_execution_common_source_left_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_source_left_productcoefficientscoefficient pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient. ((forall pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_source_left_productcoefficients))) -> exists pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_source_left_productcoefficientscoefficient = ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient) + (pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_source_left_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_source_left)) /\ ((((exists ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_left)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_source_left = ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_left) + (pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_source_left)=(pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_source_left_productcoefficients))) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_source_left_productcoefficients))) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_source_left_productcoefficients)) -> exists fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_source_left_productcoefficientscoefficient = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient) + (fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_source_left_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_source_left_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_source_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_source_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_source_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_source_left_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_source_left_productcoefficients) + (p) * pfa_offset_right_execution_common_source_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_source_left_target pfrep_left_execution_common_source_left_target pfrep_right_execution_common_source_left_target. ((exists pfrep_position_execution_common_source_left_targetfirst. ((pfrep_position_execution_common_source_left_targetfirst+S (pfrep_power_execution_common_source_left_target)=(pfrd_plen_execution_common_source_left)) /\ ((((exists ff_h_pfp_execution_common_source_left_targetfirstentry. ff_h_pfp_execution_common_source_left_targetfirstentry + S (pfrep_left_execution_common_source_left_target) = S ((S (pfrep_position_execution_common_source_left_targetfirst)) * pfrd_pc_execution_common_source_left)) /\ exists ff_q_pfp_execution_common_source_left_targetfirstentry. pfrd_pb_execution_common_source_left = ff_q_pfp_execution_common_source_left_targetfirstentry * S ((S (pfrep_position_execution_common_source_left_targetfirst)) * pfrd_pc_execution_common_source_left) + (pfrep_left_execution_common_source_left_target)))))) \/ (((exists pfrep_gap_execution_common_source_left_targetfirstoutside. pfrep_gap_execution_common_source_left_targetfirstoutside+(pfrd_plen_execution_common_source_left)=(pfrep_power_execution_common_source_left_target)) /\ (((pfrep_left_execution_common_source_left_target)=0))))) -> ((exists pfrep_position_execution_common_source_left_targetsecond. ((pfrep_position_execution_common_source_left_targetsecond+S (pfrep_power_execution_common_source_left_target)=(L)) /\ ((((exists ff_h_pfp_execution_common_source_left_targetsecondentry. ff_h_pfp_execution_common_source_left_targetsecondentry + S (pfrep_right_execution_common_source_left_target) = S ((S (pfrep_position_execution_common_source_left_targetsecond)) * ac)) /\ exists ff_q_pfp_execution_common_source_left_targetsecondentry. ab = ff_q_pfp_execution_common_source_left_targetsecondentry * S ((S (pfrep_position_execution_common_source_left_targetsecond)) * ac) + (pfrep_right_execution_common_source_left_target)))))) \/ (((exists pfrep_gap_execution_common_source_left_targetsecondoutside. pfrep_gap_execution_common_source_left_targetsecondoutside+(L)=(pfrep_power_execution_common_source_left_target)) /\ (((pfrep_right_execution_common_source_left_target)=0))))) -> pfrep_left_execution_common_source_left_target=pfrep_right_execution_common_source_left_target))))))) /\ ((((forall fom_index_pfp_execution_common_source_right_canonical. (exists fom_gap_pfp_execution_common_source_right_canonical_index_bound. fom_gap_pfp_execution_common_source_right_canonical_index_bound + S (fom_index_pfp_execution_common_source_right_canonical) = S d) -> exists fom_value_pfp_execution_common_source_right_canonical. ((((exists fom_beta_height_pfp_execution_common_source_right_canonical_entry. fom_beta_height_pfp_execution_common_source_right_canonical_entry + S (fom_value_pfp_execution_common_source_right_canonical) = S ((S (fom_index_pfp_execution_common_source_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_execution_common_source_right_canonical_entry. bb = fom_beta_quotient_pfp_execution_common_source_right_canonical_entry * S ((S (fom_index_pfp_execution_common_source_right_canonical)) * bc) + (fom_value_pfp_execution_common_source_right_canonical))) /\ (exists fom_gap_pfp_execution_common_source_right_canonical_value_bound. fom_gap_pfp_execution_common_source_right_canonical_value_bound + S (fom_value_pfp_execution_common_source_right_canonical) = p))) /\ ((exists pfrd_qb_execution_common_source_right pfrd_qc_execution_common_source_right pfrd_qlen_execution_common_source_right pfrd_pb_execution_common_source_right pfrd_pc_execution_common_source_right pfrd_plen_execution_common_source_right. ((((forall fom_index_pfp_execution_common_source_right_productleft. (exists fom_gap_pfp_execution_common_source_right_productleft_index_bound. fom_gap_pfp_execution_common_source_right_productleft_index_bound + S (fom_index_pfp_execution_common_source_right_productleft) = pfrd_qlen_execution_common_source_right) -> exists fom_value_pfp_execution_common_source_right_productleft. ((((exists fom_beta_height_pfp_execution_common_source_right_productleft_entry. fom_beta_height_pfp_execution_common_source_right_productleft_entry + S (fom_value_pfp_execution_common_source_right_productleft) = S ((S (fom_index_pfp_execution_common_source_right_productleft)) * pfrd_qc_execution_common_source_right)) /\ exists fom_beta_quotient_pfp_execution_common_source_right_productleft_entry. pfrd_qb_execution_common_source_right = fom_beta_quotient_pfp_execution_common_source_right_productleft_entry * S ((S (fom_index_pfp_execution_common_source_right_productleft)) * pfrd_qc_execution_common_source_right) + (fom_value_pfp_execution_common_source_right_productleft))) /\ (exists fom_gap_pfp_execution_common_source_right_productleft_value_bound. fom_gap_pfp_execution_common_source_right_productleft_value_bound + S (fom_value_pfp_execution_common_source_right_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_source_right_productright. (exists fom_gap_pfp_execution_common_source_right_productright_index_bound. fom_gap_pfp_execution_common_source_right_productright_index_bound + S (fom_index_pfp_execution_common_source_right_productright) = J) -> exists fom_value_pfp_execution_common_source_right_productright. ((((exists fom_beta_height_pfp_execution_common_source_right_productright_entry. fom_beta_height_pfp_execution_common_source_right_productright_entry + S (fom_value_pfp_execution_common_source_right_productright) = S ((S (fom_index_pfp_execution_common_source_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_source_right_productright_entry. db = fom_beta_quotient_pfp_execution_common_source_right_productright_entry * S ((S (fom_index_pfp_execution_common_source_right_productright)) * dc) + (fom_value_pfp_execution_common_source_right_productright))) /\ (exists fom_gap_pfp_execution_common_source_right_productright_value_bound. fom_gap_pfp_execution_common_source_right_productright_value_bound + S (fom_value_pfp_execution_common_source_right_productright) = p))) /\ (((((((pfrd_qlen_execution_common_source_right)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_source_right)=0)))) \/ (((~((pfrd_qlen_execution_common_source_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_source_right)+(J)=S (pfrd_plen_execution_common_source_right)))))))) /\ ((forall pfc_index_execution_common_source_right_productcoefficients. (exists pfa_gap_execution_common_source_right_productcoefficientsbound. pfa_gap_execution_common_source_right_productcoefficientsbound + S (pfc_index_execution_common_source_right_productcoefficients) = (pfrd_plen_execution_common_source_right)) -> exists pfc_value_execution_common_source_right_productcoefficients. ((((exists ff_h_pfp_execution_common_source_right_productcoefficientsentry. ff_h_pfp_execution_common_source_right_productcoefficientsentry + S (pfc_value_execution_common_source_right_productcoefficients) = S ((S (pfc_index_execution_common_source_right_productcoefficients)) * pfrd_pc_execution_common_source_right)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientsentry. pfrd_pb_execution_common_source_right = ff_q_pfp_execution_common_source_right_productcoefficientsentry * S ((S (pfc_index_execution_common_source_right_productcoefficients)) * pfrd_pc_execution_common_source_right) + (pfc_value_execution_common_source_right_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_source_right_productcoefficientscoefficient pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient. ((forall pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_source_right_productcoefficients))) -> exists pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_source_right_productcoefficientscoefficient = ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient) + (pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_source_right_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_source_right)) /\ ((((exists ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_right)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_source_right = ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_right) + (pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_source_right)=(pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_source_right_productcoefficients))) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_source_right_productcoefficients))) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_source_right_productcoefficients)) -> exists fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_source_right_productcoefficientscoefficient = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient) + (fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_source_right_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_source_right_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_source_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_source_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_source_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_source_right_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_source_right_productcoefficients) + (p) * pfa_offset_right_execution_common_source_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_source_right_target pfrep_left_execution_common_source_right_target pfrep_right_execution_common_source_right_target. ((exists pfrep_position_execution_common_source_right_targetfirst. ((pfrep_position_execution_common_source_right_targetfirst+S (pfrep_power_execution_common_source_right_target)=(pfrd_plen_execution_common_source_right)) /\ ((((exists ff_h_pfp_execution_common_source_right_targetfirstentry. ff_h_pfp_execution_common_source_right_targetfirstentry + S (pfrep_left_execution_common_source_right_target) = S ((S (pfrep_position_execution_common_source_right_targetfirst)) * pfrd_pc_execution_common_source_right)) /\ exists ff_q_pfp_execution_common_source_right_targetfirstentry. pfrd_pb_execution_common_source_right = ff_q_pfp_execution_common_source_right_targetfirstentry * S ((S (pfrep_position_execution_common_source_right_targetfirst)) * pfrd_pc_execution_common_source_right) + (pfrep_left_execution_common_source_right_target)))))) \/ (((exists pfrep_gap_execution_common_source_right_targetfirstoutside. pfrep_gap_execution_common_source_right_targetfirstoutside+(pfrd_plen_execution_common_source_right)=(pfrep_power_execution_common_source_right_target)) /\ (((pfrep_left_execution_common_source_right_target)=0))))) -> ((exists pfrep_position_execution_common_source_right_targetsecond. ((pfrep_position_execution_common_source_right_targetsecond+S (pfrep_power_execution_common_source_right_target)=(S d)) /\ ((((exists ff_h_pfp_execution_common_source_right_targetsecondentry. ff_h_pfp_execution_common_source_right_targetsecondentry + S (pfrep_right_execution_common_source_right_target) = S ((S (pfrep_position_execution_common_source_right_targetsecond)) * bc)) /\ exists ff_q_pfp_execution_common_source_right_targetsecondentry. bb = ff_q_pfp_execution_common_source_right_targetsecondentry * S ((S (pfrep_position_execution_common_source_right_targetsecond)) * bc) + (pfrep_right_execution_common_source_right_target)))))) \/ (((exists pfrep_gap_execution_common_source_right_targetsecondoutside. pfrep_gap_execution_common_source_right_targetsecondoutside+(S d)=(pfrep_power_execution_common_source_right_target)) /\ (((pfrep_right_execution_common_source_right_target)=0))))) -> pfrep_left_execution_common_source_right_target=pfrep_right_execution_common_source_right_target)))))))))) -> (((((forall fom_index_pfp_execution_common_target_left_canonical. (exists fom_gap_pfp_execution_common_target_left_canonical_index_bound. fom_gap_pfp_execution_common_target_left_canonical_index_bound + S (fom_index_pfp_execution_common_target_left_canonical) = S d) -> exists fom_value_pfp_execution_common_target_left_canonical. ((((exists fom_beta_height_pfp_execution_common_target_left_canonical_entry. fom_beta_height_pfp_execution_common_target_left_canonical_entry + S (fom_value_pfp_execution_common_target_left_canonical) = S ((S (fom_index_pfp_execution_common_target_left_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_execution_common_target_left_canonical_entry. bb = fom_beta_quotient_pfp_execution_common_target_left_canonical_entry * S ((S (fom_index_pfp_execution_common_target_left_canonical)) * bc) + (fom_value_pfp_execution_common_target_left_canonical))) /\ (exists fom_gap_pfp_execution_common_target_left_canonical_value_bound. fom_gap_pfp_execution_common_target_left_canonical_value_bound + S (fom_value_pfp_execution_common_target_left_canonical) = p))) /\ ((exists pfrd_qb_execution_common_target_left pfrd_qc_execution_common_target_left pfrd_qlen_execution_common_target_left pfrd_pb_execution_common_target_left pfrd_pc_execution_common_target_left pfrd_plen_execution_common_target_left. ((((forall fom_index_pfp_execution_common_target_left_productleft. (exists fom_gap_pfp_execution_common_target_left_productleft_index_bound. fom_gap_pfp_execution_common_target_left_productleft_index_bound + S (fom_index_pfp_execution_common_target_left_productleft) = pfrd_qlen_execution_common_target_left) -> exists fom_value_pfp_execution_common_target_left_productleft. ((((exists fom_beta_height_pfp_execution_common_target_left_productleft_entry. fom_beta_height_pfp_execution_common_target_left_productleft_entry + S (fom_value_pfp_execution_common_target_left_productleft) = S ((S (fom_index_pfp_execution_common_target_left_productleft)) * pfrd_qc_execution_common_target_left)) /\ exists fom_beta_quotient_pfp_execution_common_target_left_productleft_entry. pfrd_qb_execution_common_target_left = fom_beta_quotient_pfp_execution_common_target_left_productleft_entry * S ((S (fom_index_pfp_execution_common_target_left_productleft)) * pfrd_qc_execution_common_target_left) + (fom_value_pfp_execution_common_target_left_productleft))) /\ (exists fom_gap_pfp_execution_common_target_left_productleft_value_bound. fom_gap_pfp_execution_common_target_left_productleft_value_bound + S (fom_value_pfp_execution_common_target_left_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_target_left_productright. (exists fom_gap_pfp_execution_common_target_left_productright_index_bound. fom_gap_pfp_execution_common_target_left_productright_index_bound + S (fom_index_pfp_execution_common_target_left_productright) = J) -> exists fom_value_pfp_execution_common_target_left_productright. ((((exists fom_beta_height_pfp_execution_common_target_left_productright_entry. fom_beta_height_pfp_execution_common_target_left_productright_entry + S (fom_value_pfp_execution_common_target_left_productright) = S ((S (fom_index_pfp_execution_common_target_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_target_left_productright_entry. db = fom_beta_quotient_pfp_execution_common_target_left_productright_entry * S ((S (fom_index_pfp_execution_common_target_left_productright)) * dc) + (fom_value_pfp_execution_common_target_left_productright))) /\ (exists fom_gap_pfp_execution_common_target_left_productright_value_bound. fom_gap_pfp_execution_common_target_left_productright_value_bound + S (fom_value_pfp_execution_common_target_left_productright) = p))) /\ (((((((pfrd_qlen_execution_common_target_left)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_target_left)=0)))) \/ (((~((pfrd_qlen_execution_common_target_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_target_left)+(J)=S (pfrd_plen_execution_common_target_left)))))))) /\ ((forall pfc_index_execution_common_target_left_productcoefficients. (exists pfa_gap_execution_common_target_left_productcoefficientsbound. pfa_gap_execution_common_target_left_productcoefficientsbound + S (pfc_index_execution_common_target_left_productcoefficients) = (pfrd_plen_execution_common_target_left)) -> exists pfc_value_execution_common_target_left_productcoefficients. ((((exists ff_h_pfp_execution_common_target_left_productcoefficientsentry. ff_h_pfp_execution_common_target_left_productcoefficientsentry + S (pfc_value_execution_common_target_left_productcoefficients) = S ((S (pfc_index_execution_common_target_left_productcoefficients)) * pfrd_pc_execution_common_target_left)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientsentry. pfrd_pb_execution_common_target_left = ff_q_pfp_execution_common_target_left_productcoefficientsentry * S ((S (pfc_index_execution_common_target_left_productcoefficients)) * pfrd_pc_execution_common_target_left) + (pfc_value_execution_common_target_left_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_target_left_productcoefficientscoefficient pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient. ((forall pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_target_left_productcoefficients))) -> exists pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_target_left_productcoefficientscoefficient = ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient) + (pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_target_left_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_target_left)) /\ ((((exists ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_left)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_target_left = ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_left) + (pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_target_left)=(pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_target_left_productcoefficients))) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_target_left_productcoefficients))) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_target_left_productcoefficients)) -> exists fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_target_left_productcoefficientscoefficient = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient) + (fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_target_left_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_target_left_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_target_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_target_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_target_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_target_left_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_target_left_productcoefficients) + (p) * pfa_offset_right_execution_common_target_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_target_left_target pfrep_left_execution_common_target_left_target pfrep_right_execution_common_target_left_target. ((exists pfrep_position_execution_common_target_left_targetfirst. ((pfrep_position_execution_common_target_left_targetfirst+S (pfrep_power_execution_common_target_left_target)=(pfrd_plen_execution_common_target_left)) /\ ((((exists ff_h_pfp_execution_common_target_left_targetfirstentry. ff_h_pfp_execution_common_target_left_targetfirstentry + S (pfrep_left_execution_common_target_left_target) = S ((S (pfrep_position_execution_common_target_left_targetfirst)) * pfrd_pc_execution_common_target_left)) /\ exists ff_q_pfp_execution_common_target_left_targetfirstentry. pfrd_pb_execution_common_target_left = ff_q_pfp_execution_common_target_left_targetfirstentry * S ((S (pfrep_position_execution_common_target_left_targetfirst)) * pfrd_pc_execution_common_target_left) + (pfrep_left_execution_common_target_left_target)))))) \/ (((exists pfrep_gap_execution_common_target_left_targetfirstoutside. pfrep_gap_execution_common_target_left_targetfirstoutside+(pfrd_plen_execution_common_target_left)=(pfrep_power_execution_common_target_left_target)) /\ (((pfrep_left_execution_common_target_left_target)=0))))) -> ((exists pfrep_position_execution_common_target_left_targetsecond. ((pfrep_position_execution_common_target_left_targetsecond+S (pfrep_power_execution_common_target_left_target)=(S d)) /\ ((((exists ff_h_pfp_execution_common_target_left_targetsecondentry. ff_h_pfp_execution_common_target_left_targetsecondentry + S (pfrep_right_execution_common_target_left_target) = S ((S (pfrep_position_execution_common_target_left_targetsecond)) * bc)) /\ exists ff_q_pfp_execution_common_target_left_targetsecondentry. bb = ff_q_pfp_execution_common_target_left_targetsecondentry * S ((S (pfrep_position_execution_common_target_left_targetsecond)) * bc) + (pfrep_right_execution_common_target_left_target)))))) \/ (((exists pfrep_gap_execution_common_target_left_targetsecondoutside. pfrep_gap_execution_common_target_left_targetsecondoutside+(S d)=(pfrep_power_execution_common_target_left_target)) /\ (((pfrep_right_execution_common_target_left_target)=0))))) -> pfrep_left_execution_common_target_left_target=pfrep_right_execution_common_target_left_target))))))) /\ ((((forall fom_index_pfp_execution_common_target_right_canonical. (exists fom_gap_pfp_execution_common_target_right_canonical_index_bound. fom_gap_pfp_execution_common_target_right_canonical_index_bound + S (fom_index_pfp_execution_common_target_right_canonical) = N) -> exists fom_value_pfp_execution_common_target_right_canonical. ((((exists fom_beta_height_pfp_execution_common_target_right_canonical_entry. fom_beta_height_pfp_execution_common_target_right_canonical_entry + S (fom_value_pfp_execution_common_target_right_canonical) = S ((S (fom_index_pfp_execution_common_target_right_canonical)) * rc)) /\ exists fom_beta_quotient_pfp_execution_common_target_right_canonical_entry. rb = fom_beta_quotient_pfp_execution_common_target_right_canonical_entry * S ((S (fom_index_pfp_execution_common_target_right_canonical)) * rc) + (fom_value_pfp_execution_common_target_right_canonical))) /\ (exists fom_gap_pfp_execution_common_target_right_canonical_value_bound. fom_gap_pfp_execution_common_target_right_canonical_value_bound + S (fom_value_pfp_execution_common_target_right_canonical) = p))) /\ ((exists pfrd_qb_execution_common_target_right pfrd_qc_execution_common_target_right pfrd_qlen_execution_common_target_right pfrd_pb_execution_common_target_right pfrd_pc_execution_common_target_right pfrd_plen_execution_common_target_right. ((((forall fom_index_pfp_execution_common_target_right_productleft. (exists fom_gap_pfp_execution_common_target_right_productleft_index_bound. fom_gap_pfp_execution_common_target_right_productleft_index_bound + S (fom_index_pfp_execution_common_target_right_productleft) = pfrd_qlen_execution_common_target_right) -> exists fom_value_pfp_execution_common_target_right_productleft. ((((exists fom_beta_height_pfp_execution_common_target_right_productleft_entry. fom_beta_height_pfp_execution_common_target_right_productleft_entry + S (fom_value_pfp_execution_common_target_right_productleft) = S ((S (fom_index_pfp_execution_common_target_right_productleft)) * pfrd_qc_execution_common_target_right)) /\ exists fom_beta_quotient_pfp_execution_common_target_right_productleft_entry. pfrd_qb_execution_common_target_right = fom_beta_quotient_pfp_execution_common_target_right_productleft_entry * S ((S (fom_index_pfp_execution_common_target_right_productleft)) * pfrd_qc_execution_common_target_right) + (fom_value_pfp_execution_common_target_right_productleft))) /\ (exists fom_gap_pfp_execution_common_target_right_productleft_value_bound. fom_gap_pfp_execution_common_target_right_productleft_value_bound + S (fom_value_pfp_execution_common_target_right_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_target_right_productright. (exists fom_gap_pfp_execution_common_target_right_productright_index_bound. fom_gap_pfp_execution_common_target_right_productright_index_bound + S (fom_index_pfp_execution_common_target_right_productright) = J) -> exists fom_value_pfp_execution_common_target_right_productright. ((((exists fom_beta_height_pfp_execution_common_target_right_productright_entry. fom_beta_height_pfp_execution_common_target_right_productright_entry + S (fom_value_pfp_execution_common_target_right_productright) = S ((S (fom_index_pfp_execution_common_target_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_target_right_productright_entry. db = fom_beta_quotient_pfp_execution_common_target_right_productright_entry * S ((S (fom_index_pfp_execution_common_target_right_productright)) * dc) + (fom_value_pfp_execution_common_target_right_productright))) /\ (exists fom_gap_pfp_execution_common_target_right_productright_value_bound. fom_gap_pfp_execution_common_target_right_productright_value_bound + S (fom_value_pfp_execution_common_target_right_productright) = p))) /\ (((((((pfrd_qlen_execution_common_target_right)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_target_right)=0)))) \/ (((~((pfrd_qlen_execution_common_target_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_target_right)+(J)=S (pfrd_plen_execution_common_target_right)))))))) /\ ((forall pfc_index_execution_common_target_right_productcoefficients. (exists pfa_gap_execution_common_target_right_productcoefficientsbound. pfa_gap_execution_common_target_right_productcoefficientsbound + S (pfc_index_execution_common_target_right_productcoefficients) = (pfrd_plen_execution_common_target_right)) -> exists pfc_value_execution_common_target_right_productcoefficients. ((((exists ff_h_pfp_execution_common_target_right_productcoefficientsentry. ff_h_pfp_execution_common_target_right_productcoefficientsentry + S (pfc_value_execution_common_target_right_productcoefficients) = S ((S (pfc_index_execution_common_target_right_productcoefficients)) * pfrd_pc_execution_common_target_right)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientsentry. pfrd_pb_execution_common_target_right = ff_q_pfp_execution_common_target_right_productcoefficientsentry * S ((S (pfc_index_execution_common_target_right_productcoefficients)) * pfrd_pc_execution_common_target_right) + (pfc_value_execution_common_target_right_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_target_right_productcoefficientscoefficient pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient. ((forall pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_target_right_productcoefficients))) -> exists pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_target_right_productcoefficientscoefficient = ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient) + (pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_target_right_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_target_right)) /\ ((((exists ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_right)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_target_right = ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_right) + (pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_target_right)=(pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_target_right_productcoefficients))) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_target_right_productcoefficients))) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_target_right_productcoefficients)) -> exists fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_target_right_productcoefficientscoefficient = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient) + (fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_target_right_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_target_right_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_target_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_target_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_target_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_target_right_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_target_right_productcoefficients) + (p) * pfa_offset_right_execution_common_target_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_target_right_target pfrep_left_execution_common_target_right_target pfrep_right_execution_common_target_right_target. ((exists pfrep_position_execution_common_target_right_targetfirst. ((pfrep_position_execution_common_target_right_targetfirst+S (pfrep_power_execution_common_target_right_target)=(pfrd_plen_execution_common_target_right)) /\ ((((exists ff_h_pfp_execution_common_target_right_targetfirstentry. ff_h_pfp_execution_common_target_right_targetfirstentry + S (pfrep_left_execution_common_target_right_target) = S ((S (pfrep_position_execution_common_target_right_targetfirst)) * pfrd_pc_execution_common_target_right)) /\ exists ff_q_pfp_execution_common_target_right_targetfirstentry. pfrd_pb_execution_common_target_right = ff_q_pfp_execution_common_target_right_targetfirstentry * S ((S (pfrep_position_execution_common_target_right_targetfirst)) * pfrd_pc_execution_common_target_right) + (pfrep_left_execution_common_target_right_target)))))) \/ (((exists pfrep_gap_execution_common_target_right_targetfirstoutside. pfrep_gap_execution_common_target_right_targetfirstoutside+(pfrd_plen_execution_common_target_right)=(pfrep_power_execution_common_target_right_target)) /\ (((pfrep_left_execution_common_target_right_target)=0))))) -> ((exists pfrep_position_execution_common_target_right_targetsecond. ((pfrep_position_execution_common_target_right_targetsecond+S (pfrep_power_execution_common_target_right_target)=(N)) /\ ((((exists ff_h_pfp_execution_common_target_right_targetsecondentry. ff_h_pfp_execution_common_target_right_targetsecondentry + S (pfrep_right_execution_common_target_right_target) = S ((S (pfrep_position_execution_common_target_right_targetsecond)) * rc)) /\ exists ff_q_pfp_execution_common_target_right_targetsecondentry. rb = ff_q_pfp_execution_common_target_right_targetsecondentry * S ((S (pfrep_position_execution_common_target_right_targetsecond)) * rc) + (pfrep_right_execution_common_target_right_target)))))) \/ (((exists pfrep_gap_execution_common_target_right_targetsecondoutside. pfrep_gap_execution_common_target_right_targetsecondoutside+(N)=(pfrep_power_execution_common_target_right_target)) /\ (((pfrep_right_execution_common_target_right_target)=0))))) -> pfrep_left_execution_common_target_right_target=pfrep_right_execution_common_target_right_target))))))))))) /\ (((((((forall fom_index_pfp_execution_common_target_left_canonical. (exists fom_gap_pfp_execution_common_target_left_canonical_index_bound. fom_gap_pfp_execution_common_target_left_canonical_index_bound + S (fom_index_pfp_execution_common_target_left_canonical) = S d) -> exists fom_value_pfp_execution_common_target_left_canonical. ((((exists fom_beta_height_pfp_execution_common_target_left_canonical_entry. fom_beta_height_pfp_execution_common_target_left_canonical_entry + S (fom_value_pfp_execution_common_target_left_canonical) = S ((S (fom_index_pfp_execution_common_target_left_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_execution_common_target_left_canonical_entry. bb = fom_beta_quotient_pfp_execution_common_target_left_canonical_entry * S ((S (fom_index_pfp_execution_common_target_left_canonical)) * bc) + (fom_value_pfp_execution_common_target_left_canonical))) /\ (exists fom_gap_pfp_execution_common_target_left_canonical_value_bound. fom_gap_pfp_execution_common_target_left_canonical_value_bound + S (fom_value_pfp_execution_common_target_left_canonical) = p))) /\ ((exists pfrd_qb_execution_common_target_left pfrd_qc_execution_common_target_left pfrd_qlen_execution_common_target_left pfrd_pb_execution_common_target_left pfrd_pc_execution_common_target_left pfrd_plen_execution_common_target_left. ((((forall fom_index_pfp_execution_common_target_left_productleft. (exists fom_gap_pfp_execution_common_target_left_productleft_index_bound. fom_gap_pfp_execution_common_target_left_productleft_index_bound + S (fom_index_pfp_execution_common_target_left_productleft) = pfrd_qlen_execution_common_target_left) -> exists fom_value_pfp_execution_common_target_left_productleft. ((((exists fom_beta_height_pfp_execution_common_target_left_productleft_entry. fom_beta_height_pfp_execution_common_target_left_productleft_entry + S (fom_value_pfp_execution_common_target_left_productleft) = S ((S (fom_index_pfp_execution_common_target_left_productleft)) * pfrd_qc_execution_common_target_left)) /\ exists fom_beta_quotient_pfp_execution_common_target_left_productleft_entry. pfrd_qb_execution_common_target_left = fom_beta_quotient_pfp_execution_common_target_left_productleft_entry * S ((S (fom_index_pfp_execution_common_target_left_productleft)) * pfrd_qc_execution_common_target_left) + (fom_value_pfp_execution_common_target_left_productleft))) /\ (exists fom_gap_pfp_execution_common_target_left_productleft_value_bound. fom_gap_pfp_execution_common_target_left_productleft_value_bound + S (fom_value_pfp_execution_common_target_left_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_target_left_productright. (exists fom_gap_pfp_execution_common_target_left_productright_index_bound. fom_gap_pfp_execution_common_target_left_productright_index_bound + S (fom_index_pfp_execution_common_target_left_productright) = J) -> exists fom_value_pfp_execution_common_target_left_productright. ((((exists fom_beta_height_pfp_execution_common_target_left_productright_entry. fom_beta_height_pfp_execution_common_target_left_productright_entry + S (fom_value_pfp_execution_common_target_left_productright) = S ((S (fom_index_pfp_execution_common_target_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_target_left_productright_entry. db = fom_beta_quotient_pfp_execution_common_target_left_productright_entry * S ((S (fom_index_pfp_execution_common_target_left_productright)) * dc) + (fom_value_pfp_execution_common_target_left_productright))) /\ (exists fom_gap_pfp_execution_common_target_left_productright_value_bound. fom_gap_pfp_execution_common_target_left_productright_value_bound + S (fom_value_pfp_execution_common_target_left_productright) = p))) /\ (((((((pfrd_qlen_execution_common_target_left)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_target_left)=0)))) \/ (((~((pfrd_qlen_execution_common_target_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_target_left)+(J)=S (pfrd_plen_execution_common_target_left)))))))) /\ ((forall pfc_index_execution_common_target_left_productcoefficients. (exists pfa_gap_execution_common_target_left_productcoefficientsbound. pfa_gap_execution_common_target_left_productcoefficientsbound + S (pfc_index_execution_common_target_left_productcoefficients) = (pfrd_plen_execution_common_target_left)) -> exists pfc_value_execution_common_target_left_productcoefficients. ((((exists ff_h_pfp_execution_common_target_left_productcoefficientsentry. ff_h_pfp_execution_common_target_left_productcoefficientsentry + S (pfc_value_execution_common_target_left_productcoefficients) = S ((S (pfc_index_execution_common_target_left_productcoefficients)) * pfrd_pc_execution_common_target_left)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientsentry. pfrd_pb_execution_common_target_left = ff_q_pfp_execution_common_target_left_productcoefficientsentry * S ((S (pfc_index_execution_common_target_left_productcoefficients)) * pfrd_pc_execution_common_target_left) + (pfc_value_execution_common_target_left_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_target_left_productcoefficientscoefficient pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient. ((forall pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_target_left_productcoefficients))) -> exists pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_target_left_productcoefficientscoefficient = ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient) + (pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_target_left_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_target_left)) /\ ((((exists ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_left)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_target_left = ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_left) + (pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_target_left)=(pfc_index_execution_common_target_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_target_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_target_left_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_target_left_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_target_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_target_left_productcoefficients))) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_target_left_productcoefficients))) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_target_left_productcoefficients)) -> exists fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_target_left_productcoefficientscoefficient = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_left_productcoefficientscoefficient) + (fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_left_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_target_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_target_left_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_target_left_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_target_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_target_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_target_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_target_left_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_target_left_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_target_left_productcoefficients) + (p) * pfa_offset_right_execution_common_target_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_target_left_target pfrep_left_execution_common_target_left_target pfrep_right_execution_common_target_left_target. ((exists pfrep_position_execution_common_target_left_targetfirst. ((pfrep_position_execution_common_target_left_targetfirst+S (pfrep_power_execution_common_target_left_target)=(pfrd_plen_execution_common_target_left)) /\ ((((exists ff_h_pfp_execution_common_target_left_targetfirstentry. ff_h_pfp_execution_common_target_left_targetfirstentry + S (pfrep_left_execution_common_target_left_target) = S ((S (pfrep_position_execution_common_target_left_targetfirst)) * pfrd_pc_execution_common_target_left)) /\ exists ff_q_pfp_execution_common_target_left_targetfirstentry. pfrd_pb_execution_common_target_left = ff_q_pfp_execution_common_target_left_targetfirstentry * S ((S (pfrep_position_execution_common_target_left_targetfirst)) * pfrd_pc_execution_common_target_left) + (pfrep_left_execution_common_target_left_target)))))) \/ (((exists pfrep_gap_execution_common_target_left_targetfirstoutside. pfrep_gap_execution_common_target_left_targetfirstoutside+(pfrd_plen_execution_common_target_left)=(pfrep_power_execution_common_target_left_target)) /\ (((pfrep_left_execution_common_target_left_target)=0))))) -> ((exists pfrep_position_execution_common_target_left_targetsecond. ((pfrep_position_execution_common_target_left_targetsecond+S (pfrep_power_execution_common_target_left_target)=(S d)) /\ ((((exists ff_h_pfp_execution_common_target_left_targetsecondentry. ff_h_pfp_execution_common_target_left_targetsecondentry + S (pfrep_right_execution_common_target_left_target) = S ((S (pfrep_position_execution_common_target_left_targetsecond)) * bc)) /\ exists ff_q_pfp_execution_common_target_left_targetsecondentry. bb = ff_q_pfp_execution_common_target_left_targetsecondentry * S ((S (pfrep_position_execution_common_target_left_targetsecond)) * bc) + (pfrep_right_execution_common_target_left_target)))))) \/ (((exists pfrep_gap_execution_common_target_left_targetsecondoutside. pfrep_gap_execution_common_target_left_targetsecondoutside+(S d)=(pfrep_power_execution_common_target_left_target)) /\ (((pfrep_right_execution_common_target_left_target)=0))))) -> pfrep_left_execution_common_target_left_target=pfrep_right_execution_common_target_left_target))))))) /\ ((((forall fom_index_pfp_execution_common_target_right_canonical. (exists fom_gap_pfp_execution_common_target_right_canonical_index_bound. fom_gap_pfp_execution_common_target_right_canonical_index_bound + S (fom_index_pfp_execution_common_target_right_canonical) = N) -> exists fom_value_pfp_execution_common_target_right_canonical. ((((exists fom_beta_height_pfp_execution_common_target_right_canonical_entry. fom_beta_height_pfp_execution_common_target_right_canonical_entry + S (fom_value_pfp_execution_common_target_right_canonical) = S ((S (fom_index_pfp_execution_common_target_right_canonical)) * rc)) /\ exists fom_beta_quotient_pfp_execution_common_target_right_canonical_entry. rb = fom_beta_quotient_pfp_execution_common_target_right_canonical_entry * S ((S (fom_index_pfp_execution_common_target_right_canonical)) * rc) + (fom_value_pfp_execution_common_target_right_canonical))) /\ (exists fom_gap_pfp_execution_common_target_right_canonical_value_bound. fom_gap_pfp_execution_common_target_right_canonical_value_bound + S (fom_value_pfp_execution_common_target_right_canonical) = p))) /\ ((exists pfrd_qb_execution_common_target_right pfrd_qc_execution_common_target_right pfrd_qlen_execution_common_target_right pfrd_pb_execution_common_target_right pfrd_pc_execution_common_target_right pfrd_plen_execution_common_target_right. ((((forall fom_index_pfp_execution_common_target_right_productleft. (exists fom_gap_pfp_execution_common_target_right_productleft_index_bound. fom_gap_pfp_execution_common_target_right_productleft_index_bound + S (fom_index_pfp_execution_common_target_right_productleft) = pfrd_qlen_execution_common_target_right) -> exists fom_value_pfp_execution_common_target_right_productleft. ((((exists fom_beta_height_pfp_execution_common_target_right_productleft_entry. fom_beta_height_pfp_execution_common_target_right_productleft_entry + S (fom_value_pfp_execution_common_target_right_productleft) = S ((S (fom_index_pfp_execution_common_target_right_productleft)) * pfrd_qc_execution_common_target_right)) /\ exists fom_beta_quotient_pfp_execution_common_target_right_productleft_entry. pfrd_qb_execution_common_target_right = fom_beta_quotient_pfp_execution_common_target_right_productleft_entry * S ((S (fom_index_pfp_execution_common_target_right_productleft)) * pfrd_qc_execution_common_target_right) + (fom_value_pfp_execution_common_target_right_productleft))) /\ (exists fom_gap_pfp_execution_common_target_right_productleft_value_bound. fom_gap_pfp_execution_common_target_right_productleft_value_bound + S (fom_value_pfp_execution_common_target_right_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_target_right_productright. (exists fom_gap_pfp_execution_common_target_right_productright_index_bound. fom_gap_pfp_execution_common_target_right_productright_index_bound + S (fom_index_pfp_execution_common_target_right_productright) = J) -> exists fom_value_pfp_execution_common_target_right_productright. ((((exists fom_beta_height_pfp_execution_common_target_right_productright_entry. fom_beta_height_pfp_execution_common_target_right_productright_entry + S (fom_value_pfp_execution_common_target_right_productright) = S ((S (fom_index_pfp_execution_common_target_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_target_right_productright_entry. db = fom_beta_quotient_pfp_execution_common_target_right_productright_entry * S ((S (fom_index_pfp_execution_common_target_right_productright)) * dc) + (fom_value_pfp_execution_common_target_right_productright))) /\ (exists fom_gap_pfp_execution_common_target_right_productright_value_bound. fom_gap_pfp_execution_common_target_right_productright_value_bound + S (fom_value_pfp_execution_common_target_right_productright) = p))) /\ (((((((pfrd_qlen_execution_common_target_right)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_target_right)=0)))) \/ (((~((pfrd_qlen_execution_common_target_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_target_right)+(J)=S (pfrd_plen_execution_common_target_right)))))))) /\ ((forall pfc_index_execution_common_target_right_productcoefficients. (exists pfa_gap_execution_common_target_right_productcoefficientsbound. pfa_gap_execution_common_target_right_productcoefficientsbound + S (pfc_index_execution_common_target_right_productcoefficients) = (pfrd_plen_execution_common_target_right)) -> exists pfc_value_execution_common_target_right_productcoefficients. ((((exists ff_h_pfp_execution_common_target_right_productcoefficientsentry. ff_h_pfp_execution_common_target_right_productcoefficientsentry + S (pfc_value_execution_common_target_right_productcoefficients) = S ((S (pfc_index_execution_common_target_right_productcoefficients)) * pfrd_pc_execution_common_target_right)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientsentry. pfrd_pb_execution_common_target_right = ff_q_pfp_execution_common_target_right_productcoefficientsentry * S ((S (pfc_index_execution_common_target_right_productcoefficients)) * pfrd_pc_execution_common_target_right) + (pfc_value_execution_common_target_right_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_target_right_productcoefficientscoefficient pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient. ((forall pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_target_right_productcoefficients))) -> exists pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_target_right_productcoefficientscoefficient = ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient) + (pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_target_right_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_target_right)) /\ ((((exists ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_right)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_target_right = ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_target_right) + (pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_target_right)=(pfc_index_execution_common_target_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_target_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_target_right_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_target_right_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_target_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_target_right_productcoefficients))) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_target_right_productcoefficients))) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_target_right_productcoefficients)) -> exists fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_target_right_productcoefficientscoefficient = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_target_right_productcoefficientscoefficient) + (fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_target_right_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_target_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_target_right_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_target_right_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_target_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_target_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_target_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_target_right_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_target_right_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_target_right_productcoefficients) + (p) * pfa_offset_right_execution_common_target_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_target_right_target pfrep_left_execution_common_target_right_target pfrep_right_execution_common_target_right_target. ((exists pfrep_position_execution_common_target_right_targetfirst. ((pfrep_position_execution_common_target_right_targetfirst+S (pfrep_power_execution_common_target_right_target)=(pfrd_plen_execution_common_target_right)) /\ ((((exists ff_h_pfp_execution_common_target_right_targetfirstentry. ff_h_pfp_execution_common_target_right_targetfirstentry + S (pfrep_left_execution_common_target_right_target) = S ((S (pfrep_position_execution_common_target_right_targetfirst)) * pfrd_pc_execution_common_target_right)) /\ exists ff_q_pfp_execution_common_target_right_targetfirstentry. pfrd_pb_execution_common_target_right = ff_q_pfp_execution_common_target_right_targetfirstentry * S ((S (pfrep_position_execution_common_target_right_targetfirst)) * pfrd_pc_execution_common_target_right) + (pfrep_left_execution_common_target_right_target)))))) \/ (((exists pfrep_gap_execution_common_target_right_targetfirstoutside. pfrep_gap_execution_common_target_right_targetfirstoutside+(pfrd_plen_execution_common_target_right)=(pfrep_power_execution_common_target_right_target)) /\ (((pfrep_left_execution_common_target_right_target)=0))))) -> ((exists pfrep_position_execution_common_target_right_targetsecond. ((pfrep_position_execution_common_target_right_targetsecond+S (pfrep_power_execution_common_target_right_target)=(N)) /\ ((((exists ff_h_pfp_execution_common_target_right_targetsecondentry. ff_h_pfp_execution_common_target_right_targetsecondentry + S (pfrep_right_execution_common_target_right_target) = S ((S (pfrep_position_execution_common_target_right_targetsecond)) * rc)) /\ exists ff_q_pfp_execution_common_target_right_targetsecondentry. rb = ff_q_pfp_execution_common_target_right_targetsecondentry * S ((S (pfrep_position_execution_common_target_right_targetsecond)) * rc) + (pfrep_right_execution_common_target_right_target)))))) \/ (((exists pfrep_gap_execution_common_target_right_targetsecondoutside. pfrep_gap_execution_common_target_right_targetsecondoutside+(N)=(pfrep_power_execution_common_target_right_target)) /\ (((pfrep_right_execution_common_target_right_target)=0))))) -> pfrep_left_execution_common_target_right_target=pfrep_right_execution_common_target_right_target)))))))))) -> (((((forall fom_index_pfp_execution_common_source_left_canonical. (exists fom_gap_pfp_execution_common_source_left_canonical_index_bound. fom_gap_pfp_execution_common_source_left_canonical_index_bound + S (fom_index_pfp_execution_common_source_left_canonical) = L) -> exists fom_value_pfp_execution_common_source_left_canonical. ((((exists fom_beta_height_pfp_execution_common_source_left_canonical_entry. fom_beta_height_pfp_execution_common_source_left_canonical_entry + S (fom_value_pfp_execution_common_source_left_canonical) = S ((S (fom_index_pfp_execution_common_source_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_execution_common_source_left_canonical_entry. ab = fom_beta_quotient_pfp_execution_common_source_left_canonical_entry * S ((S (fom_index_pfp_execution_common_source_left_canonical)) * ac) + (fom_value_pfp_execution_common_source_left_canonical))) /\ (exists fom_gap_pfp_execution_common_source_left_canonical_value_bound. fom_gap_pfp_execution_common_source_left_canonical_value_bound + S (fom_value_pfp_execution_common_source_left_canonical) = p))) /\ ((exists pfrd_qb_execution_common_source_left pfrd_qc_execution_common_source_left pfrd_qlen_execution_common_source_left pfrd_pb_execution_common_source_left pfrd_pc_execution_common_source_left pfrd_plen_execution_common_source_left. ((((forall fom_index_pfp_execution_common_source_left_productleft. (exists fom_gap_pfp_execution_common_source_left_productleft_index_bound. fom_gap_pfp_execution_common_source_left_productleft_index_bound + S (fom_index_pfp_execution_common_source_left_productleft) = pfrd_qlen_execution_common_source_left) -> exists fom_value_pfp_execution_common_source_left_productleft. ((((exists fom_beta_height_pfp_execution_common_source_left_productleft_entry. fom_beta_height_pfp_execution_common_source_left_productleft_entry + S (fom_value_pfp_execution_common_source_left_productleft) = S ((S (fom_index_pfp_execution_common_source_left_productleft)) * pfrd_qc_execution_common_source_left)) /\ exists fom_beta_quotient_pfp_execution_common_source_left_productleft_entry. pfrd_qb_execution_common_source_left = fom_beta_quotient_pfp_execution_common_source_left_productleft_entry * S ((S (fom_index_pfp_execution_common_source_left_productleft)) * pfrd_qc_execution_common_source_left) + (fom_value_pfp_execution_common_source_left_productleft))) /\ (exists fom_gap_pfp_execution_common_source_left_productleft_value_bound. fom_gap_pfp_execution_common_source_left_productleft_value_bound + S (fom_value_pfp_execution_common_source_left_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_source_left_productright. (exists fom_gap_pfp_execution_common_source_left_productright_index_bound. fom_gap_pfp_execution_common_source_left_productright_index_bound + S (fom_index_pfp_execution_common_source_left_productright) = J) -> exists fom_value_pfp_execution_common_source_left_productright. ((((exists fom_beta_height_pfp_execution_common_source_left_productright_entry. fom_beta_height_pfp_execution_common_source_left_productright_entry + S (fom_value_pfp_execution_common_source_left_productright) = S ((S (fom_index_pfp_execution_common_source_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_source_left_productright_entry. db = fom_beta_quotient_pfp_execution_common_source_left_productright_entry * S ((S (fom_index_pfp_execution_common_source_left_productright)) * dc) + (fom_value_pfp_execution_common_source_left_productright))) /\ (exists fom_gap_pfp_execution_common_source_left_productright_value_bound. fom_gap_pfp_execution_common_source_left_productright_value_bound + S (fom_value_pfp_execution_common_source_left_productright) = p))) /\ (((((((pfrd_qlen_execution_common_source_left)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_source_left)=0)))) \/ (((~((pfrd_qlen_execution_common_source_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_source_left)+(J)=S (pfrd_plen_execution_common_source_left)))))))) /\ ((forall pfc_index_execution_common_source_left_productcoefficients. (exists pfa_gap_execution_common_source_left_productcoefficientsbound. pfa_gap_execution_common_source_left_productcoefficientsbound + S (pfc_index_execution_common_source_left_productcoefficients) = (pfrd_plen_execution_common_source_left)) -> exists pfc_value_execution_common_source_left_productcoefficients. ((((exists ff_h_pfp_execution_common_source_left_productcoefficientsentry. ff_h_pfp_execution_common_source_left_productcoefficientsentry + S (pfc_value_execution_common_source_left_productcoefficients) = S ((S (pfc_index_execution_common_source_left_productcoefficients)) * pfrd_pc_execution_common_source_left)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientsentry. pfrd_pb_execution_common_source_left = ff_q_pfp_execution_common_source_left_productcoefficientsentry * S ((S (pfc_index_execution_common_source_left_productcoefficients)) * pfrd_pc_execution_common_source_left) + (pfc_value_execution_common_source_left_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_source_left_productcoefficientscoefficient pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient. ((forall pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_source_left_productcoefficients))) -> exists pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_source_left_productcoefficientscoefficient = ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient) + (pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_source_left_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_source_left)) /\ ((((exists ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_left)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_source_left = ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_left) + (pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_source_left)=(pfc_index_execution_common_source_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_source_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_source_left_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_source_left_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_source_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_source_left_productcoefficients))) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_source_left_productcoefficients))) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_source_left_productcoefficients)) -> exists fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_source_left_productcoefficientscoefficient = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_left_productcoefficientscoefficient) + (fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_left_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_source_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_source_left_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_source_left_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_source_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_source_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_source_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_source_left_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_source_left_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_source_left_productcoefficients) + (p) * pfa_offset_right_execution_common_source_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_source_left_target pfrep_left_execution_common_source_left_target pfrep_right_execution_common_source_left_target. ((exists pfrep_position_execution_common_source_left_targetfirst. ((pfrep_position_execution_common_source_left_targetfirst+S (pfrep_power_execution_common_source_left_target)=(pfrd_plen_execution_common_source_left)) /\ ((((exists ff_h_pfp_execution_common_source_left_targetfirstentry. ff_h_pfp_execution_common_source_left_targetfirstentry + S (pfrep_left_execution_common_source_left_target) = S ((S (pfrep_position_execution_common_source_left_targetfirst)) * pfrd_pc_execution_common_source_left)) /\ exists ff_q_pfp_execution_common_source_left_targetfirstentry. pfrd_pb_execution_common_source_left = ff_q_pfp_execution_common_source_left_targetfirstentry * S ((S (pfrep_position_execution_common_source_left_targetfirst)) * pfrd_pc_execution_common_source_left) + (pfrep_left_execution_common_source_left_target)))))) \/ (((exists pfrep_gap_execution_common_source_left_targetfirstoutside. pfrep_gap_execution_common_source_left_targetfirstoutside+(pfrd_plen_execution_common_source_left)=(pfrep_power_execution_common_source_left_target)) /\ (((pfrep_left_execution_common_source_left_target)=0))))) -> ((exists pfrep_position_execution_common_source_left_targetsecond. ((pfrep_position_execution_common_source_left_targetsecond+S (pfrep_power_execution_common_source_left_target)=(L)) /\ ((((exists ff_h_pfp_execution_common_source_left_targetsecondentry. ff_h_pfp_execution_common_source_left_targetsecondentry + S (pfrep_right_execution_common_source_left_target) = S ((S (pfrep_position_execution_common_source_left_targetsecond)) * ac)) /\ exists ff_q_pfp_execution_common_source_left_targetsecondentry. ab = ff_q_pfp_execution_common_source_left_targetsecondentry * S ((S (pfrep_position_execution_common_source_left_targetsecond)) * ac) + (pfrep_right_execution_common_source_left_target)))))) \/ (((exists pfrep_gap_execution_common_source_left_targetsecondoutside. pfrep_gap_execution_common_source_left_targetsecondoutside+(L)=(pfrep_power_execution_common_source_left_target)) /\ (((pfrep_right_execution_common_source_left_target)=0))))) -> pfrep_left_execution_common_source_left_target=pfrep_right_execution_common_source_left_target))))))) /\ ((((forall fom_index_pfp_execution_common_source_right_canonical. (exists fom_gap_pfp_execution_common_source_right_canonical_index_bound. fom_gap_pfp_execution_common_source_right_canonical_index_bound + S (fom_index_pfp_execution_common_source_right_canonical) = S d) -> exists fom_value_pfp_execution_common_source_right_canonical. ((((exists fom_beta_height_pfp_execution_common_source_right_canonical_entry. fom_beta_height_pfp_execution_common_source_right_canonical_entry + S (fom_value_pfp_execution_common_source_right_canonical) = S ((S (fom_index_pfp_execution_common_source_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_execution_common_source_right_canonical_entry. bb = fom_beta_quotient_pfp_execution_common_source_right_canonical_entry * S ((S (fom_index_pfp_execution_common_source_right_canonical)) * bc) + (fom_value_pfp_execution_common_source_right_canonical))) /\ (exists fom_gap_pfp_execution_common_source_right_canonical_value_bound. fom_gap_pfp_execution_common_source_right_canonical_value_bound + S (fom_value_pfp_execution_common_source_right_canonical) = p))) /\ ((exists pfrd_qb_execution_common_source_right pfrd_qc_execution_common_source_right pfrd_qlen_execution_common_source_right pfrd_pb_execution_common_source_right pfrd_pc_execution_common_source_right pfrd_plen_execution_common_source_right. ((((forall fom_index_pfp_execution_common_source_right_productleft. (exists fom_gap_pfp_execution_common_source_right_productleft_index_bound. fom_gap_pfp_execution_common_source_right_productleft_index_bound + S (fom_index_pfp_execution_common_source_right_productleft) = pfrd_qlen_execution_common_source_right) -> exists fom_value_pfp_execution_common_source_right_productleft. ((((exists fom_beta_height_pfp_execution_common_source_right_productleft_entry. fom_beta_height_pfp_execution_common_source_right_productleft_entry + S (fom_value_pfp_execution_common_source_right_productleft) = S ((S (fom_index_pfp_execution_common_source_right_productleft)) * pfrd_qc_execution_common_source_right)) /\ exists fom_beta_quotient_pfp_execution_common_source_right_productleft_entry. pfrd_qb_execution_common_source_right = fom_beta_quotient_pfp_execution_common_source_right_productleft_entry * S ((S (fom_index_pfp_execution_common_source_right_productleft)) * pfrd_qc_execution_common_source_right) + (fom_value_pfp_execution_common_source_right_productleft))) /\ (exists fom_gap_pfp_execution_common_source_right_productleft_value_bound. fom_gap_pfp_execution_common_source_right_productleft_value_bound + S (fom_value_pfp_execution_common_source_right_productleft) = p))) /\ (((forall fom_index_pfp_execution_common_source_right_productright. (exists fom_gap_pfp_execution_common_source_right_productright_index_bound. fom_gap_pfp_execution_common_source_right_productright_index_bound + S (fom_index_pfp_execution_common_source_right_productright) = J) -> exists fom_value_pfp_execution_common_source_right_productright. ((((exists fom_beta_height_pfp_execution_common_source_right_productright_entry. fom_beta_height_pfp_execution_common_source_right_productright_entry + S (fom_value_pfp_execution_common_source_right_productright) = S ((S (fom_index_pfp_execution_common_source_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_execution_common_source_right_productright_entry. db = fom_beta_quotient_pfp_execution_common_source_right_productright_entry * S ((S (fom_index_pfp_execution_common_source_right_productright)) * dc) + (fom_value_pfp_execution_common_source_right_productright))) /\ (exists fom_gap_pfp_execution_common_source_right_productright_value_bound. fom_gap_pfp_execution_common_source_right_productright_value_bound + S (fom_value_pfp_execution_common_source_right_productright) = p))) /\ (((((((pfrd_qlen_execution_common_source_right)=0 \/ (J)=0) /\ (((pfrd_plen_execution_common_source_right)=0)))) \/ (((~((pfrd_qlen_execution_common_source_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_execution_common_source_right)+(J)=S (pfrd_plen_execution_common_source_right)))))))) /\ ((forall pfc_index_execution_common_source_right_productcoefficients. (exists pfa_gap_execution_common_source_right_productcoefficientsbound. pfa_gap_execution_common_source_right_productcoefficientsbound + S (pfc_index_execution_common_source_right_productcoefficients) = (pfrd_plen_execution_common_source_right)) -> exists pfc_value_execution_common_source_right_productcoefficients. ((((exists ff_h_pfp_execution_common_source_right_productcoefficientsentry. ff_h_pfp_execution_common_source_right_productcoefficientsentry + S (pfc_value_execution_common_source_right_productcoefficients) = S ((S (pfc_index_execution_common_source_right_productcoefficients)) * pfrd_pc_execution_common_source_right)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientsentry. pfrd_pb_execution_common_source_right = ff_q_pfp_execution_common_source_right_productcoefficientsentry * S ((S (pfc_index_execution_common_source_right_productcoefficients)) * pfrd_pc_execution_common_source_right) + (pfc_value_execution_common_source_right_productcoefficients))) /\ ((exists pfc_terms_code_execution_common_source_right_productcoefficientscoefficient pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient. ((forall pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_common_source_right_productcoefficients))) -> exists pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_common_source_right_productcoefficientscoefficient = ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient) + (pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)+pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_common_source_right_productcoefficients)) /\ ((((((exists pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_execution_common_source_right)) /\ ((((exists ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_right)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_execution_common_source_right = ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_execution_common_source_right) + (pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_execution_common_source_right)=(pfc_index_execution_common_source_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_execution_common_source_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_common_source_right_productcoefficientscoefficientdiagonal)=pfc_left_execution_common_source_right_productcoefficientscoefficientdiagonalterm*pfc_right_execution_common_source_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_common_source_right_productcoefficients))) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_common_source_right_productcoefficients))) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_common_source_right_productcoefficients)) -> exists fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_common_source_right_productcoefficientscoefficient = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_common_source_right_productcoefficientscoefficient) + (fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_common_source_right_productcoefficientscoefficientsum) + (fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_common_source_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_common_source_right_productcoefficientscoefficientresiduebound. pfa_gap_execution_common_source_right_productcoefficientscoefficientresiduebound + S (pfc_value_execution_common_source_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_common_source_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_common_source_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_common_source_right_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_common_source_right_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_common_source_right_productcoefficients) + (p) * pfa_offset_right_execution_common_source_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_execution_common_source_right_target pfrep_left_execution_common_source_right_target pfrep_right_execution_common_source_right_target. ((exists pfrep_position_execution_common_source_right_targetfirst. ((pfrep_position_execution_common_source_right_targetfirst+S (pfrep_power_execution_common_source_right_target)=(pfrd_plen_execution_common_source_right)) /\ ((((exists ff_h_pfp_execution_common_source_right_targetfirstentry. ff_h_pfp_execution_common_source_right_targetfirstentry + S (pfrep_left_execution_common_source_right_target) = S ((S (pfrep_position_execution_common_source_right_targetfirst)) * pfrd_pc_execution_common_source_right)) /\ exists ff_q_pfp_execution_common_source_right_targetfirstentry. pfrd_pb_execution_common_source_right = ff_q_pfp_execution_common_source_right_targetfirstentry * S ((S (pfrep_position_execution_common_source_right_targetfirst)) * pfrd_pc_execution_common_source_right) + (pfrep_left_execution_common_source_right_target)))))) \/ (((exists pfrep_gap_execution_common_source_right_targetfirstoutside. pfrep_gap_execution_common_source_right_targetfirstoutside+(pfrd_plen_execution_common_source_right)=(pfrep_power_execution_common_source_right_target)) /\ (((pfrep_left_execution_common_source_right_target)=0))))) -> ((exists pfrep_position_execution_common_source_right_targetsecond. ((pfrep_position_execution_common_source_right_targetsecond+S (pfrep_power_execution_common_source_right_target)=(S d)) /\ ((((exists ff_h_pfp_execution_common_source_right_targetsecondentry. ff_h_pfp_execution_common_source_right_targetsecondentry + S (pfrep_right_execution_common_source_right_target) = S ((S (pfrep_position_execution_common_source_right_targetsecond)) * bc)) /\ exists ff_q_pfp_execution_common_source_right_targetsecondentry. bb = ff_q_pfp_execution_common_source_right_targetsecondentry * S ((S (pfrep_position_execution_common_source_right_targetsecond)) * bc) + (pfrep_right_execution_common_source_right_target)))))) \/ (((exists pfrep_gap_execution_common_source_right_targetsecondoutside. pfrep_gap_execution_common_source_right_targetsecondoutside+(S d)=(pfrep_power_execution_common_source_right_target)) /\ (((pfrep_right_execution_common_source_right_target)=0))))) -> pfrep_left_execution_common_source_right_target=pfrep_right_execution_common_source_right_target))))))))))))))