prime_field_polynomial_division_execution_functional

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d qb qc q rb rc R QB QC Q RB RC K. (((forall fom_index_pfp_execution_unique_firstinput. (exists fom_gap_pfp_execution_unique_firstinput_index_bound. fom_gap_pfp_execution_unique_firstinput_index_bound + S (fom_index_pfp_execution_unique_firstinput) = L) -> exists fom_value_pfp_execution_unique_firstinput. ((((exists fom_beta_height_pfp_execution_unique_firstinput_entry. fom_beta_height_pfp_execution_unique_firstinput_entry + S (fom_value_pfp_execution_unique_firstinput) = S ((S (fom_index_pfp_execution_unique_firstinput)) * ac)) /\ exists fom_beta_quotient_pfp_execution_unique_firstinput_entry. ab = fom_beta_quotient_pfp_execution_unique_firstinput_entry * S ((S (fom_index_pfp_execution_unique_firstinput)) * ac) + (fom_value_pfp_execution_unique_firstinput))) /\ (exists fom_gap_pfp_execution_unique_firstinput_value_bound. fom_gap_pfp_execution_unique_firstinput_value_bound + S (fom_value_pfp_execution_unique_firstinput) = p))) /\ (((forall fom_index_pfp_execution_unique_firstdivisor. (exists fom_gap_pfp_execution_unique_firstdivisor_index_bound. fom_gap_pfp_execution_unique_firstdivisor_index_bound + S (fom_index_pfp_execution_unique_firstdivisor) = S (d)) -> exists fom_value_pfp_execution_unique_firstdivisor. ((((exists fom_beta_height_pfp_execution_unique_firstdivisor_entry. fom_beta_height_pfp_execution_unique_firstdivisor_entry + S (fom_value_pfp_execution_unique_firstdivisor) = S ((S (fom_index_pfp_execution_unique_firstdivisor)) * bc)) /\ exists fom_beta_quotient_pfp_execution_unique_firstdivisor_entry. bb = fom_beta_quotient_pfp_execution_unique_firstdivisor_entry * S ((S (fom_index_pfp_execution_unique_firstdivisor)) * bc) + (fom_value_pfp_execution_unique_firstdivisor))) /\ (exists fom_gap_pfp_execution_unique_firstdivisor_value_bound. fom_gap_pfp_execution_unique_firstdivisor_value_bound + S (fom_value_pfp_execution_unique_firstdivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_execution_unique_firstlengthshort. pfc_gap_execution_unique_firstlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_execution_unique_first pfd_inverse_execution_unique_first pfd_product_code_execution_unique_first pfd_product_scale_execution_unique_first pfd_residual_code_execution_unique_first pfd_residual_scale_execution_unique_first pfd_cut_execution_unique_first. ((((exists ff_h_pfp_execution_unique_firsthead. ff_h_pfp_execution_unique_firsthead + S (pfd_head_execution_unique_first) = S ((S (0)) * bc)) /\ exists ff_q_pfp_execution_unique_firsthead. bb = ff_q_pfp_execution_unique_firsthead * S ((S (0)) * bc) + (pfd_head_execution_unique_first))) /\ (((((~((pfd_head_execution_unique_first) = 0)) /\ ((((exists pfa_gap_execution_unique_firstinversemultiplicationleft. pfa_gap_execution_unique_firstinversemultiplicationleft + S (pfd_head_execution_unique_first) = (p)) /\ (((exists pfa_gap_execution_unique_firstinversemultiplicationright. pfa_gap_execution_unique_firstinversemultiplicationright + S (pfd_inverse_execution_unique_first) = (p)) /\ ((((exists pfa_gap_execution_unique_firstinversemultiplicationresultbound. pfa_gap_execution_unique_firstinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_execution_unique_firstinversemultiplicationresultcongruence pfa_offset_right_execution_unique_firstinversemultiplicationresultcongruence. ((pfd_head_execution_unique_first) * (pfd_inverse_execution_unique_first)) + (p) * pfa_offset_left_execution_unique_firstinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_execution_unique_firstinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_execution_unique_firstquotient. (exists pfa_gap_execution_unique_firstquotientbound. pfa_gap_execution_unique_firstquotientbound + S (pfd_index_execution_unique_firstquotient) = (q)) -> exists pfd_value_execution_unique_firstquotient. ((((exists ff_h_pfp_execution_unique_firstquotiententry. ff_h_pfp_execution_unique_firstquotiententry + S (pfd_value_execution_unique_firstquotient) = S ((S (pfd_index_execution_unique_firstquotient)) * qc)) /\ exists ff_q_pfp_execution_unique_firstquotiententry. qb = ff_q_pfp_execution_unique_firstquotiententry * S ((S (pfd_index_execution_unique_firstquotient)) * qc) + (pfd_value_execution_unique_firstquotient))) /\ ((exists pfd_input_execution_unique_firstquotientstep pfd_previous_execution_unique_firstquotientstep pfd_difference_execution_unique_firstquotientstep. ((((exists ff_h_pfp_execution_unique_firstquotientstepinput. ff_h_pfp_execution_unique_firstquotientstepinput + S (pfd_input_execution_unique_firstquotientstep) = S ((S (pfd_index_execution_unique_firstquotient)) * ac)) /\ exists ff_q_pfp_execution_unique_firstquotientstepinput. ab = ff_q_pfp_execution_unique_firstquotientstepinput * S ((S (pfd_index_execution_unique_firstquotient)) * ac) + (pfd_input_execution_unique_firstquotientstep))) /\ (((exists pfc_terms_code_execution_unique_firstquotientstepprevious pfc_terms_scale_execution_unique_firstquotientstepprevious pfc_natural_sum_execution_unique_firstquotientstepprevious. ((forall pfc_index_execution_unique_firstquotientsteppreviousdiagonal. (exists pfa_gap_execution_unique_firstquotientsteppreviousdiagonalbound. pfa_gap_execution_unique_firstquotientsteppreviousdiagonalbound + S (pfc_index_execution_unique_firstquotientsteppreviousdiagonal) = (S (pfd_index_execution_unique_firstquotient))) -> exists pfc_value_execution_unique_firstquotientsteppreviousdiagonal. ((((exists ff_h_pfp_execution_unique_firstquotientsteppreviousdiagonalentry. ff_h_pfp_execution_unique_firstquotientsteppreviousdiagonalentry + S (pfc_value_execution_unique_firstquotientsteppreviousdiagonal) = S ((S (pfc_index_execution_unique_firstquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_unique_firstquotientstepprevious)) /\ exists ff_q_pfp_execution_unique_firstquotientsteppreviousdiagonalentry. pfc_terms_code_execution_unique_firstquotientstepprevious = ff_q_pfp_execution_unique_firstquotientsteppreviousdiagonalentry * S ((S (pfc_index_execution_unique_firstquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_unique_firstquotientstepprevious) + (pfc_value_execution_unique_firstquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_execution_unique_firstquotientsteppreviousdiagonalterm pfc_left_execution_unique_firstquotientsteppreviousdiagonalterm pfc_right_execution_unique_firstquotientsteppreviousdiagonalterm. (((pfc_index_execution_unique_firstquotientsteppreviousdiagonal)+pfc_complement_execution_unique_firstquotientsteppreviousdiagonalterm=(pfd_index_execution_unique_firstquotient)) /\ ((((((exists pfa_gap_execution_unique_firstquotientsteppreviousdiagonaltermleftinside. pfa_gap_execution_unique_firstquotientsteppreviousdiagonaltermleftinside + S (pfc_index_execution_unique_firstquotientsteppreviousdiagonal) = (pfd_index_execution_unique_firstquotient)) /\ ((((exists ff_h_pfp_execution_unique_firstquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_execution_unique_firstquotientsteppreviousdiagonaltermleftentry + S (pfc_left_execution_unique_firstquotientsteppreviousdiagonalterm) = S ((S (pfc_index_execution_unique_firstquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_execution_unique_firstquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_execution_unique_firstquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_execution_unique_firstquotientsteppreviousdiagonal)) * qc) + (pfc_left_execution_unique_firstquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_firstquotientsteppreviousdiagonaltermleftoutside. pfc_gap_execution_unique_firstquotientsteppreviousdiagonaltermleftoutside+(pfd_index_execution_unique_firstquotient)=(pfc_index_execution_unique_firstquotientsteppreviousdiagonal)) /\ (((pfc_left_execution_unique_firstquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_unique_firstquotientsteppreviousdiagonaltermrightinside. pfa_gap_execution_unique_firstquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_execution_unique_firstquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_unique_firstquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_execution_unique_firstquotientsteppreviousdiagonaltermrightentry + S (pfc_right_execution_unique_firstquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_execution_unique_firstquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_unique_firstquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_execution_unique_firstquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_execution_unique_firstquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_execution_unique_firstquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_firstquotientsteppreviousdiagonaltermrightoutside. pfc_gap_execution_unique_firstquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_unique_firstquotientsteppreviousdiagonalterm)) /\ (((pfc_right_execution_unique_firstquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_execution_unique_firstquotientsteppreviousdiagonal)=pfc_left_execution_unique_firstquotientsteppreviousdiagonalterm*pfc_right_execution_unique_firstquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_unique_firstquotientstepprevioussum fs_v_pfc_execution_unique_firstquotientstepprevioussum. ((((exists fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_start. fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_unique_firstquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_start. fs_u_pfc_execution_unique_firstquotientstepprevioussum = fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_execution_unique_firstquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_terminal. fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_terminal + S (pfc_natural_sum_execution_unique_firstquotientstepprevious) = S ((S (S (pfd_index_execution_unique_firstquotient))) * fs_v_pfc_execution_unique_firstquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_terminal. fs_u_pfc_execution_unique_firstquotientstepprevioussum = fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_execution_unique_firstquotient))) * fs_v_pfc_execution_unique_firstquotientstepprevioussum) + (pfc_natural_sum_execution_unique_firstquotientstepprevious))) /\ forall fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps. (exists fs_lt_pfc_execution_unique_firstquotientstepprevioussum_body_steps_bound. fs_lt_pfc_execution_unique_firstquotientstepprevioussum_body_steps_bound + S fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps = S (pfd_index_execution_unique_firstquotient)) -> exists fs_a_pfc_execution_unique_firstquotientstepprevioussum_body_steps fs_r_pfc_execution_unique_firstquotientstepprevioussum_body_steps fs_s_pfc_execution_unique_firstquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_steps_summand. fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_execution_unique_firstquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_unique_firstquotientstepprevious)) /\ exists fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_steps_summand. pfc_terms_code_execution_unique_firstquotientstepprevious = fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_unique_firstquotientstepprevious) + (fs_a_pfc_execution_unique_firstquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_steps_partial. fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_execution_unique_firstquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_firstquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_steps_partial. fs_u_pfc_execution_unique_firstquotientstepprevioussum = fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_firstquotientstepprevioussum) + (fs_r_pfc_execution_unique_firstquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_steps_successor. fs_h_pfc_execution_unique_firstquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_execution_unique_firstquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_firstquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_steps_successor. fs_u_pfc_execution_unique_firstquotientstepprevioussum = fs_q_pfc_execution_unique_firstquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_execution_unique_firstquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_firstquotientstepprevioussum) + (fs_s_pfc_execution_unique_firstquotientstepprevioussum_body_steps))) /\ fs_s_pfc_execution_unique_firstquotientstepprevioussum_body_steps = fs_r_pfc_execution_unique_firstquotientstepprevioussum_body_steps + fs_a_pfc_execution_unique_firstquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_execution_unique_firstquotientsteppreviousresiduebound. pfa_gap_execution_unique_firstquotientsteppreviousresiduebound + S (pfd_previous_execution_unique_firstquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_unique_firstquotientsteppreviousresiduecongruence pfa_offset_right_execution_unique_firstquotientsteppreviousresiduecongruence. (pfc_natural_sum_execution_unique_firstquotientstepprevious) + (p) * pfa_offset_left_execution_unique_firstquotientsteppreviousresiduecongruence = (pfd_previous_execution_unique_firstquotientstep) + (p) * pfa_offset_right_execution_unique_firstquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_execution_unique_firstquotientstepsubtractleft. pfa_gap_execution_unique_firstquotientstepsubtractleft + S (pfd_previous_execution_unique_firstquotientstep) = (p)) /\ (((exists pfa_gap_execution_unique_firstquotientstepsubtractright. pfa_gap_execution_unique_firstquotientstepsubtractright + S (pfd_difference_execution_unique_firstquotientstep) = (p)) /\ ((((exists pfa_gap_execution_unique_firstquotientstepsubtractresultbound. pfa_gap_execution_unique_firstquotientstepsubtractresultbound + S (pfd_input_execution_unique_firstquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_unique_firstquotientstepsubtractresultcongruence pfa_offset_right_execution_unique_firstquotientstepsubtractresultcongruence. ((pfd_previous_execution_unique_firstquotientstep) + (pfd_difference_execution_unique_firstquotientstep)) + (p) * pfa_offset_left_execution_unique_firstquotientstepsubtractresultcongruence = (pfd_input_execution_unique_firstquotientstep) + (p) * pfa_offset_right_execution_unique_firstquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_execution_unique_firstquotientstepmultiplyleft. pfa_gap_execution_unique_firstquotientstepmultiplyleft + S (pfd_inverse_execution_unique_first) = (p)) /\ (((exists pfa_gap_execution_unique_firstquotientstepmultiplyright. pfa_gap_execution_unique_firstquotientstepmultiplyright + S (pfd_difference_execution_unique_firstquotientstep) = (p)) /\ ((((exists pfa_gap_execution_unique_firstquotientstepmultiplyresultbound. pfa_gap_execution_unique_firstquotientstepmultiplyresultbound + S (pfd_value_execution_unique_firstquotient) = (p)) /\ ((exists pfa_offset_left_execution_unique_firstquotientstepmultiplyresultcongruence pfa_offset_right_execution_unique_firstquotientstepmultiplyresultcongruence. ((pfd_inverse_execution_unique_first) * (pfd_difference_execution_unique_firstquotientstep)) + (p) * pfa_offset_left_execution_unique_firstquotientstepmultiplyresultcongruence = (pfd_value_execution_unique_firstquotient) + (p) * pfa_offset_right_execution_unique_firstquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_execution_unique_firstproduct. (exists pfa_gap_execution_unique_firstproductbound. pfa_gap_execution_unique_firstproductbound + S (pfc_index_execution_unique_firstproduct) = (L)) -> exists pfc_value_execution_unique_firstproduct. ((((exists ff_h_pfp_execution_unique_firstproductentry. ff_h_pfp_execution_unique_firstproductentry + S (pfc_value_execution_unique_firstproduct) = S ((S (pfc_index_execution_unique_firstproduct)) * pfd_product_scale_execution_unique_first)) /\ exists ff_q_pfp_execution_unique_firstproductentry. pfd_product_code_execution_unique_first = ff_q_pfp_execution_unique_firstproductentry * S ((S (pfc_index_execution_unique_firstproduct)) * pfd_product_scale_execution_unique_first) + (pfc_value_execution_unique_firstproduct))) /\ ((exists pfc_terms_code_execution_unique_firstproductcoefficient pfc_terms_scale_execution_unique_firstproductcoefficient pfc_natural_sum_execution_unique_firstproductcoefficient. ((forall pfc_index_execution_unique_firstproductcoefficientdiagonal. (exists pfa_gap_execution_unique_firstproductcoefficientdiagonalbound. pfa_gap_execution_unique_firstproductcoefficientdiagonalbound + S (pfc_index_execution_unique_firstproductcoefficientdiagonal) = (S (pfc_index_execution_unique_firstproduct))) -> exists pfc_value_execution_unique_firstproductcoefficientdiagonal. ((((exists ff_h_pfp_execution_unique_firstproductcoefficientdiagonalentry. ff_h_pfp_execution_unique_firstproductcoefficientdiagonalentry + S (pfc_value_execution_unique_firstproductcoefficientdiagonal) = S ((S (pfc_index_execution_unique_firstproductcoefficientdiagonal)) * pfc_terms_scale_execution_unique_firstproductcoefficient)) /\ exists ff_q_pfp_execution_unique_firstproductcoefficientdiagonalentry. pfc_terms_code_execution_unique_firstproductcoefficient = ff_q_pfp_execution_unique_firstproductcoefficientdiagonalentry * S ((S (pfc_index_execution_unique_firstproductcoefficientdiagonal)) * pfc_terms_scale_execution_unique_firstproductcoefficient) + (pfc_value_execution_unique_firstproductcoefficientdiagonal))) /\ ((exists pfc_complement_execution_unique_firstproductcoefficientdiagonalterm pfc_left_execution_unique_firstproductcoefficientdiagonalterm pfc_right_execution_unique_firstproductcoefficientdiagonalterm. (((pfc_index_execution_unique_firstproductcoefficientdiagonal)+pfc_complement_execution_unique_firstproductcoefficientdiagonalterm=(pfc_index_execution_unique_firstproduct)) /\ ((((((exists pfa_gap_execution_unique_firstproductcoefficientdiagonaltermleftinside. pfa_gap_execution_unique_firstproductcoefficientdiagonaltermleftinside + S (pfc_index_execution_unique_firstproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_execution_unique_firstproductcoefficientdiagonaltermleftentry. ff_h_pfp_execution_unique_firstproductcoefficientdiagonaltermleftentry + S (pfc_left_execution_unique_firstproductcoefficientdiagonalterm) = S ((S (pfc_index_execution_unique_firstproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_execution_unique_firstproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_execution_unique_firstproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_unique_firstproductcoefficientdiagonal)) * qc) + (pfc_left_execution_unique_firstproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_firstproductcoefficientdiagonaltermleftoutside. pfc_gap_execution_unique_firstproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_execution_unique_firstproductcoefficientdiagonal)) /\ (((pfc_left_execution_unique_firstproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_unique_firstproductcoefficientdiagonaltermrightinside. pfa_gap_execution_unique_firstproductcoefficientdiagonaltermrightinside + S (pfc_complement_execution_unique_firstproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_unique_firstproductcoefficientdiagonaltermrightentry. ff_h_pfp_execution_unique_firstproductcoefficientdiagonaltermrightentry + S (pfc_right_execution_unique_firstproductcoefficientdiagonalterm) = S ((S (pfc_complement_execution_unique_firstproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_unique_firstproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_unique_firstproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_unique_firstproductcoefficientdiagonalterm)) * bc) + (pfc_right_execution_unique_firstproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_firstproductcoefficientdiagonaltermrightoutside. pfc_gap_execution_unique_firstproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_unique_firstproductcoefficientdiagonalterm)) /\ (((pfc_right_execution_unique_firstproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_unique_firstproductcoefficientdiagonal)=pfc_left_execution_unique_firstproductcoefficientdiagonalterm*pfc_right_execution_unique_firstproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_unique_firstproductcoefficientsum fs_v_pfc_execution_unique_firstproductcoefficientsum. ((((exists fs_h_pfc_execution_unique_firstproductcoefficientsum_body_start. fs_h_pfc_execution_unique_firstproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_firstproductcoefficientsum_body_start. fs_u_pfc_execution_unique_firstproductcoefficientsum = fs_q_pfc_execution_unique_firstproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_unique_firstproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_unique_firstproductcoefficientsum_body_terminal. fs_h_pfc_execution_unique_firstproductcoefficientsum_body_terminal + S (pfc_natural_sum_execution_unique_firstproductcoefficient) = S ((S (S (pfc_index_execution_unique_firstproduct))) * fs_v_pfc_execution_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_firstproductcoefficientsum_body_terminal. fs_u_pfc_execution_unique_firstproductcoefficientsum = fs_q_pfc_execution_unique_firstproductcoefficientsum_body_terminal * S ((S (S (pfc_index_execution_unique_firstproduct))) * fs_v_pfc_execution_unique_firstproductcoefficientsum) + (pfc_natural_sum_execution_unique_firstproductcoefficient))) /\ forall fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps. (exists fs_lt_pfc_execution_unique_firstproductcoefficientsum_body_steps_bound. fs_lt_pfc_execution_unique_firstproductcoefficientsum_body_steps_bound + S fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps = S (pfc_index_execution_unique_firstproduct)) -> exists fs_a_pfc_execution_unique_firstproductcoefficientsum_body_steps fs_r_pfc_execution_unique_firstproductcoefficientsum_body_steps fs_s_pfc_execution_unique_firstproductcoefficientsum_body_steps. ((((exists fs_h_pfc_execution_unique_firstproductcoefficientsum_body_steps_summand. fs_h_pfc_execution_unique_firstproductcoefficientsum_body_steps_summand + S (fs_a_pfc_execution_unique_firstproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_unique_firstproductcoefficient)) /\ exists fs_q_pfc_execution_unique_firstproductcoefficientsum_body_steps_summand. pfc_terms_code_execution_unique_firstproductcoefficient = fs_q_pfc_execution_unique_firstproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_unique_firstproductcoefficient) + (fs_a_pfc_execution_unique_firstproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_firstproductcoefficientsum_body_steps_partial. fs_h_pfc_execution_unique_firstproductcoefficientsum_body_steps_partial + S (fs_r_pfc_execution_unique_firstproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_firstproductcoefficientsum_body_steps_partial. fs_u_pfc_execution_unique_firstproductcoefficientsum = fs_q_pfc_execution_unique_firstproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_firstproductcoefficientsum) + (fs_r_pfc_execution_unique_firstproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_firstproductcoefficientsum_body_steps_successor. fs_h_pfc_execution_unique_firstproductcoefficientsum_body_steps_successor + S (fs_s_pfc_execution_unique_firstproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_firstproductcoefficientsum_body_steps_successor. fs_u_pfc_execution_unique_firstproductcoefficientsum = fs_q_pfc_execution_unique_firstproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_firstproductcoefficientsum) + (fs_s_pfc_execution_unique_firstproductcoefficientsum_body_steps))) /\ fs_s_pfc_execution_unique_firstproductcoefficientsum_body_steps = fs_r_pfc_execution_unique_firstproductcoefficientsum_body_steps + fs_a_pfc_execution_unique_firstproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_unique_firstproductcoefficientresiduebound. pfa_gap_execution_unique_firstproductcoefficientresiduebound + S (pfc_value_execution_unique_firstproduct) = (p)) /\ ((exists pfa_offset_left_execution_unique_firstproductcoefficientresiduecongruence pfa_offset_right_execution_unique_firstproductcoefficientresiduecongruence. (pfc_natural_sum_execution_unique_firstproductcoefficient) + (p) * pfa_offset_left_execution_unique_firstproductcoefficientresiduecongruence = (pfc_value_execution_unique_firstproduct) + (p) * pfa_offset_right_execution_unique_firstproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_execution_unique_firstdifference. (exists pfa_gap_execution_unique_firstdifferenceindex. pfa_gap_execution_unique_firstdifferenceindex + S (pfs_index_execution_unique_firstdifference) = (L)) -> exists pfs_left_execution_unique_firstdifference pfs_right_execution_unique_firstdifference pfs_result_execution_unique_firstdifference. ((((exists ff_h_pfp_execution_unique_firstdifferenceleft. ff_h_pfp_execution_unique_firstdifferenceleft + S (pfs_left_execution_unique_firstdifference) = S ((S (pfs_index_execution_unique_firstdifference)) * ac)) /\ exists ff_q_pfp_execution_unique_firstdifferenceleft. ab = ff_q_pfp_execution_unique_firstdifferenceleft * S ((S (pfs_index_execution_unique_firstdifference)) * ac) + (pfs_left_execution_unique_firstdifference))) /\ (((((exists ff_h_pfp_execution_unique_firstdifferenceright. ff_h_pfp_execution_unique_firstdifferenceright + S (pfs_right_execution_unique_firstdifference) = S ((S (pfs_index_execution_unique_firstdifference)) * pfd_product_scale_execution_unique_first)) /\ exists ff_q_pfp_execution_unique_firstdifferenceright. pfd_product_code_execution_unique_first = ff_q_pfp_execution_unique_firstdifferenceright * S ((S (pfs_index_execution_unique_firstdifference)) * pfd_product_scale_execution_unique_first) + (pfs_right_execution_unique_firstdifference))) /\ (((((exists ff_h_pfp_execution_unique_firstdifferenceresult. ff_h_pfp_execution_unique_firstdifferenceresult + S (pfs_result_execution_unique_firstdifference) = S ((S (pfs_index_execution_unique_firstdifference)) * pfd_residual_scale_execution_unique_first)) /\ exists ff_q_pfp_execution_unique_firstdifferenceresult. pfd_residual_code_execution_unique_first = ff_q_pfp_execution_unique_firstdifferenceresult * S ((S (pfs_index_execution_unique_firstdifference)) * pfd_residual_scale_execution_unique_first) + (pfs_result_execution_unique_firstdifference))) /\ ((((exists pfa_gap_execution_unique_firstdifferenceoperationleft. pfa_gap_execution_unique_firstdifferenceoperationleft + S (pfs_right_execution_unique_firstdifference) = (p)) /\ (((exists pfa_gap_execution_unique_firstdifferenceoperationright. pfa_gap_execution_unique_firstdifferenceoperationright + S (pfs_result_execution_unique_firstdifference) = (p)) /\ ((((exists pfa_gap_execution_unique_firstdifferenceoperationresultbound. pfa_gap_execution_unique_firstdifferenceoperationresultbound + S (pfs_left_execution_unique_firstdifference) = (p)) /\ ((exists pfa_offset_left_execution_unique_firstdifferenceoperationresultcongruence pfa_offset_right_execution_unique_firstdifferenceoperationresultcongruence. ((pfs_right_execution_unique_firstdifference) + (pfs_result_execution_unique_firstdifference)) + (p) * pfa_offset_left_execution_unique_firstdifferenceoperationresultcongruence = (pfs_left_execution_unique_firstdifference) + (p) * pfa_offset_right_execution_unique_firstdifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_execution_unique_first)+(R)) /\ (((forall fom_index_pfp_execution_unique_firsttriminput. (exists fom_gap_pfp_execution_unique_firsttriminput_index_bound. fom_gap_pfp_execution_unique_firsttriminput_index_bound + S (fom_index_pfp_execution_unique_firsttriminput) = L) -> exists fom_value_pfp_execution_unique_firsttriminput. ((((exists fom_beta_height_pfp_execution_unique_firsttriminput_entry. fom_beta_height_pfp_execution_unique_firsttriminput_entry + S (fom_value_pfp_execution_unique_firsttriminput) = S ((S (fom_index_pfp_execution_unique_firsttriminput)) * pfd_residual_scale_execution_unique_first)) /\ exists fom_beta_quotient_pfp_execution_unique_firsttriminput_entry. pfd_residual_code_execution_unique_first = fom_beta_quotient_pfp_execution_unique_firsttriminput_entry * S ((S (fom_index_pfp_execution_unique_firsttriminput)) * pfd_residual_scale_execution_unique_first) + (fom_value_pfp_execution_unique_firsttriminput))) /\ (exists fom_gap_pfp_execution_unique_firsttriminput_value_bound. fom_gap_pfp_execution_unique_firsttriminput_value_bound + S (fom_value_pfp_execution_unique_firsttriminput) = p))) /\ (((forall pfp_repeat_index_execution_unique_firsttrimremoved. (exists pfa_gap_execution_unique_firsttrimremovedindex. pfa_gap_execution_unique_firsttrimremovedindex + S (pfp_repeat_index_execution_unique_firsttrimremoved) = (pfd_cut_execution_unique_first)) -> (((exists ff_h_pfp_execution_unique_firsttrimremovedentry. ff_h_pfp_execution_unique_firsttrimremovedentry + S (0) = S ((S (pfp_repeat_index_execution_unique_firsttrimremoved)) * pfd_residual_scale_execution_unique_first)) /\ exists ff_q_pfp_execution_unique_firsttrimremovedentry. pfd_residual_code_execution_unique_first = ff_q_pfp_execution_unique_firsttrimremovedentry * S ((S (pfp_repeat_index_execution_unique_firsttrimremoved)) * pfd_residual_scale_execution_unique_first) + (0)))) /\ (((forall pftrim_index_execution_unique_firsttrimsuffix pftrim_value_execution_unique_firsttrimsuffix. (exists pfa_gap_execution_unique_firsttrimsuffixbound. pfa_gap_execution_unique_firsttrimsuffixbound + S (pftrim_index_execution_unique_firsttrimsuffix) = (R)) -> (((exists ff_h_pfp_execution_unique_firsttrimsuffixsource. ff_h_pfp_execution_unique_firsttrimsuffixsource + S (pftrim_value_execution_unique_firsttrimsuffix) = S ((S ((pfd_cut_execution_unique_first)+pftrim_index_execution_unique_firsttrimsuffix)) * pfd_residual_scale_execution_unique_first)) /\ exists ff_q_pfp_execution_unique_firsttrimsuffixsource. pfd_residual_code_execution_unique_first = ff_q_pfp_execution_unique_firsttrimsuffixsource * S ((S ((pfd_cut_execution_unique_first)+pftrim_index_execution_unique_firsttrimsuffix)) * pfd_residual_scale_execution_unique_first) + (pftrim_value_execution_unique_firsttrimsuffix))) -> (((exists ff_h_pfp_execution_unique_firsttrimsuffixoutput. ff_h_pfp_execution_unique_firsttrimsuffixoutput + S (pftrim_value_execution_unique_firsttrimsuffix) = S ((S (pftrim_index_execution_unique_firsttrimsuffix)) * rc)) /\ exists ff_q_pfp_execution_unique_firsttrimsuffixoutput. rb = ff_q_pfp_execution_unique_firsttrimsuffixoutput * S ((S (pftrim_index_execution_unique_firsttrimsuffix)) * rc) + (pftrim_value_execution_unique_firsttrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_execution_unique_firsttrimnormal. ((((exists ff_h_pfp_execution_unique_firsttrimnormalentry. ff_h_pfp_execution_unique_firsttrimnormalentry + S (pftrim_leading_execution_unique_firsttrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_execution_unique_firsttrimnormalentry. rb = ff_q_pfp_execution_unique_firsttrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_execution_unique_firsttrimnormal))) /\ ((~(pftrim_leading_execution_unique_firsttrimnormal=0))))))))))))))))))))))))))))))))) -> (((forall fom_index_pfp_execution_unique_secondinput. (exists fom_gap_pfp_execution_unique_secondinput_index_bound. fom_gap_pfp_execution_unique_secondinput_index_bound + S (fom_index_pfp_execution_unique_secondinput) = L) -> exists fom_value_pfp_execution_unique_secondinput. ((((exists fom_beta_height_pfp_execution_unique_secondinput_entry. fom_beta_height_pfp_execution_unique_secondinput_entry + S (fom_value_pfp_execution_unique_secondinput) = S ((S (fom_index_pfp_execution_unique_secondinput)) * ac)) /\ exists fom_beta_quotient_pfp_execution_unique_secondinput_entry. ab = fom_beta_quotient_pfp_execution_unique_secondinput_entry * S ((S (fom_index_pfp_execution_unique_secondinput)) * ac) + (fom_value_pfp_execution_unique_secondinput))) /\ (exists fom_gap_pfp_execution_unique_secondinput_value_bound. fom_gap_pfp_execution_unique_secondinput_value_bound + S (fom_value_pfp_execution_unique_secondinput) = p))) /\ (((forall fom_index_pfp_execution_unique_seconddivisor. (exists fom_gap_pfp_execution_unique_seconddivisor_index_bound. fom_gap_pfp_execution_unique_seconddivisor_index_bound + S (fom_index_pfp_execution_unique_seconddivisor) = S (d)) -> exists fom_value_pfp_execution_unique_seconddivisor. ((((exists fom_beta_height_pfp_execution_unique_seconddivisor_entry. fom_beta_height_pfp_execution_unique_seconddivisor_entry + S (fom_value_pfp_execution_unique_seconddivisor) = S ((S (fom_index_pfp_execution_unique_seconddivisor)) * bc)) /\ exists fom_beta_quotient_pfp_execution_unique_seconddivisor_entry. bb = fom_beta_quotient_pfp_execution_unique_seconddivisor_entry * S ((S (fom_index_pfp_execution_unique_seconddivisor)) * bc) + (fom_value_pfp_execution_unique_seconddivisor))) /\ (exists fom_gap_pfp_execution_unique_seconddivisor_value_bound. fom_gap_pfp_execution_unique_seconddivisor_value_bound + S (fom_value_pfp_execution_unique_seconddivisor) = p))) /\ (((((((Q)=0) /\ ((exists pfc_gap_execution_unique_secondlengthshort. pfc_gap_execution_unique_secondlengthshort+(L)=(d))))) \/ (((~((Q)=0)) /\ (((Q)+(d)=(L)))))) /\ ((exists pfd_head_execution_unique_second pfd_inverse_execution_unique_second pfd_product_code_execution_unique_second pfd_product_scale_execution_unique_second pfd_residual_code_execution_unique_second pfd_residual_scale_execution_unique_second pfd_cut_execution_unique_second. ((((exists ff_h_pfp_execution_unique_secondhead. ff_h_pfp_execution_unique_secondhead + S (pfd_head_execution_unique_second) = S ((S (0)) * bc)) /\ exists ff_q_pfp_execution_unique_secondhead. bb = ff_q_pfp_execution_unique_secondhead * S ((S (0)) * bc) + (pfd_head_execution_unique_second))) /\ (((((~((pfd_head_execution_unique_second) = 0)) /\ ((((exists pfa_gap_execution_unique_secondinversemultiplicationleft. pfa_gap_execution_unique_secondinversemultiplicationleft + S (pfd_head_execution_unique_second) = (p)) /\ (((exists pfa_gap_execution_unique_secondinversemultiplicationright. pfa_gap_execution_unique_secondinversemultiplicationright + S (pfd_inverse_execution_unique_second) = (p)) /\ ((((exists pfa_gap_execution_unique_secondinversemultiplicationresultbound. pfa_gap_execution_unique_secondinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_execution_unique_secondinversemultiplicationresultcongruence pfa_offset_right_execution_unique_secondinversemultiplicationresultcongruence. ((pfd_head_execution_unique_second) * (pfd_inverse_execution_unique_second)) + (p) * pfa_offset_left_execution_unique_secondinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_execution_unique_secondinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_execution_unique_secondquotient. (exists pfa_gap_execution_unique_secondquotientbound. pfa_gap_execution_unique_secondquotientbound + S (pfd_index_execution_unique_secondquotient) = (Q)) -> exists pfd_value_execution_unique_secondquotient. ((((exists ff_h_pfp_execution_unique_secondquotiententry. ff_h_pfp_execution_unique_secondquotiententry + S (pfd_value_execution_unique_secondquotient) = S ((S (pfd_index_execution_unique_secondquotient)) * QC)) /\ exists ff_q_pfp_execution_unique_secondquotiententry. QB = ff_q_pfp_execution_unique_secondquotiententry * S ((S (pfd_index_execution_unique_secondquotient)) * QC) + (pfd_value_execution_unique_secondquotient))) /\ ((exists pfd_input_execution_unique_secondquotientstep pfd_previous_execution_unique_secondquotientstep pfd_difference_execution_unique_secondquotientstep. ((((exists ff_h_pfp_execution_unique_secondquotientstepinput. ff_h_pfp_execution_unique_secondquotientstepinput + S (pfd_input_execution_unique_secondquotientstep) = S ((S (pfd_index_execution_unique_secondquotient)) * ac)) /\ exists ff_q_pfp_execution_unique_secondquotientstepinput. ab = ff_q_pfp_execution_unique_secondquotientstepinput * S ((S (pfd_index_execution_unique_secondquotient)) * ac) + (pfd_input_execution_unique_secondquotientstep))) /\ (((exists pfc_terms_code_execution_unique_secondquotientstepprevious pfc_terms_scale_execution_unique_secondquotientstepprevious pfc_natural_sum_execution_unique_secondquotientstepprevious. ((forall pfc_index_execution_unique_secondquotientsteppreviousdiagonal. (exists pfa_gap_execution_unique_secondquotientsteppreviousdiagonalbound. pfa_gap_execution_unique_secondquotientsteppreviousdiagonalbound + S (pfc_index_execution_unique_secondquotientsteppreviousdiagonal) = (S (pfd_index_execution_unique_secondquotient))) -> exists pfc_value_execution_unique_secondquotientsteppreviousdiagonal. ((((exists ff_h_pfp_execution_unique_secondquotientsteppreviousdiagonalentry. ff_h_pfp_execution_unique_secondquotientsteppreviousdiagonalentry + S (pfc_value_execution_unique_secondquotientsteppreviousdiagonal) = S ((S (pfc_index_execution_unique_secondquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_unique_secondquotientstepprevious)) /\ exists ff_q_pfp_execution_unique_secondquotientsteppreviousdiagonalentry. pfc_terms_code_execution_unique_secondquotientstepprevious = ff_q_pfp_execution_unique_secondquotientsteppreviousdiagonalentry * S ((S (pfc_index_execution_unique_secondquotientsteppreviousdiagonal)) * pfc_terms_scale_execution_unique_secondquotientstepprevious) + (pfc_value_execution_unique_secondquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_execution_unique_secondquotientsteppreviousdiagonalterm pfc_left_execution_unique_secondquotientsteppreviousdiagonalterm pfc_right_execution_unique_secondquotientsteppreviousdiagonalterm. (((pfc_index_execution_unique_secondquotientsteppreviousdiagonal)+pfc_complement_execution_unique_secondquotientsteppreviousdiagonalterm=(pfd_index_execution_unique_secondquotient)) /\ ((((((exists pfa_gap_execution_unique_secondquotientsteppreviousdiagonaltermleftinside. pfa_gap_execution_unique_secondquotientsteppreviousdiagonaltermleftinside + S (pfc_index_execution_unique_secondquotientsteppreviousdiagonal) = (pfd_index_execution_unique_secondquotient)) /\ ((((exists ff_h_pfp_execution_unique_secondquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_execution_unique_secondquotientsteppreviousdiagonaltermleftentry + S (pfc_left_execution_unique_secondquotientsteppreviousdiagonalterm) = S ((S (pfc_index_execution_unique_secondquotientsteppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_execution_unique_secondquotientsteppreviousdiagonaltermleftentry. QB = ff_q_pfp_execution_unique_secondquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_execution_unique_secondquotientsteppreviousdiagonal)) * QC) + (pfc_left_execution_unique_secondquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_secondquotientsteppreviousdiagonaltermleftoutside. pfc_gap_execution_unique_secondquotientsteppreviousdiagonaltermleftoutside+(pfd_index_execution_unique_secondquotient)=(pfc_index_execution_unique_secondquotientsteppreviousdiagonal)) /\ (((pfc_left_execution_unique_secondquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_unique_secondquotientsteppreviousdiagonaltermrightinside. pfa_gap_execution_unique_secondquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_execution_unique_secondquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_unique_secondquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_execution_unique_secondquotientsteppreviousdiagonaltermrightentry + S (pfc_right_execution_unique_secondquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_execution_unique_secondquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_unique_secondquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_execution_unique_secondquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_execution_unique_secondquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_execution_unique_secondquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_secondquotientsteppreviousdiagonaltermrightoutside. pfc_gap_execution_unique_secondquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_unique_secondquotientsteppreviousdiagonalterm)) /\ (((pfc_right_execution_unique_secondquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_execution_unique_secondquotientsteppreviousdiagonal)=pfc_left_execution_unique_secondquotientsteppreviousdiagonalterm*pfc_right_execution_unique_secondquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_unique_secondquotientstepprevioussum fs_v_pfc_execution_unique_secondquotientstepprevioussum. ((((exists fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_start. fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_unique_secondquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_start. fs_u_pfc_execution_unique_secondquotientstepprevioussum = fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_execution_unique_secondquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_terminal. fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_terminal + S (pfc_natural_sum_execution_unique_secondquotientstepprevious) = S ((S (S (pfd_index_execution_unique_secondquotient))) * fs_v_pfc_execution_unique_secondquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_terminal. fs_u_pfc_execution_unique_secondquotientstepprevioussum = fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_execution_unique_secondquotient))) * fs_v_pfc_execution_unique_secondquotientstepprevioussum) + (pfc_natural_sum_execution_unique_secondquotientstepprevious))) /\ forall fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps. (exists fs_lt_pfc_execution_unique_secondquotientstepprevioussum_body_steps_bound. fs_lt_pfc_execution_unique_secondquotientstepprevioussum_body_steps_bound + S fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps = S (pfd_index_execution_unique_secondquotient)) -> exists fs_a_pfc_execution_unique_secondquotientstepprevioussum_body_steps fs_r_pfc_execution_unique_secondquotientstepprevioussum_body_steps fs_s_pfc_execution_unique_secondquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_steps_summand. fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_execution_unique_secondquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_unique_secondquotientstepprevious)) /\ exists fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_steps_summand. pfc_terms_code_execution_unique_secondquotientstepprevious = fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_unique_secondquotientstepprevious) + (fs_a_pfc_execution_unique_secondquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_steps_partial. fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_execution_unique_secondquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_secondquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_steps_partial. fs_u_pfc_execution_unique_secondquotientstepprevioussum = fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_secondquotientstepprevioussum) + (fs_r_pfc_execution_unique_secondquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_steps_successor. fs_h_pfc_execution_unique_secondquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_execution_unique_secondquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_secondquotientstepprevioussum)) /\ exists fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_steps_successor. fs_u_pfc_execution_unique_secondquotientstepprevioussum = fs_q_pfc_execution_unique_secondquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_execution_unique_secondquotientstepprevioussum_body_steps)) * fs_v_pfc_execution_unique_secondquotientstepprevioussum) + (fs_s_pfc_execution_unique_secondquotientstepprevioussum_body_steps))) /\ fs_s_pfc_execution_unique_secondquotientstepprevioussum_body_steps = fs_r_pfc_execution_unique_secondquotientstepprevioussum_body_steps + fs_a_pfc_execution_unique_secondquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_execution_unique_secondquotientsteppreviousresiduebound. pfa_gap_execution_unique_secondquotientsteppreviousresiduebound + S (pfd_previous_execution_unique_secondquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_unique_secondquotientsteppreviousresiduecongruence pfa_offset_right_execution_unique_secondquotientsteppreviousresiduecongruence. (pfc_natural_sum_execution_unique_secondquotientstepprevious) + (p) * pfa_offset_left_execution_unique_secondquotientsteppreviousresiduecongruence = (pfd_previous_execution_unique_secondquotientstep) + (p) * pfa_offset_right_execution_unique_secondquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_execution_unique_secondquotientstepsubtractleft. pfa_gap_execution_unique_secondquotientstepsubtractleft + S (pfd_previous_execution_unique_secondquotientstep) = (p)) /\ (((exists pfa_gap_execution_unique_secondquotientstepsubtractright. pfa_gap_execution_unique_secondquotientstepsubtractright + S (pfd_difference_execution_unique_secondquotientstep) = (p)) /\ ((((exists pfa_gap_execution_unique_secondquotientstepsubtractresultbound. pfa_gap_execution_unique_secondquotientstepsubtractresultbound + S (pfd_input_execution_unique_secondquotientstep) = (p)) /\ ((exists pfa_offset_left_execution_unique_secondquotientstepsubtractresultcongruence pfa_offset_right_execution_unique_secondquotientstepsubtractresultcongruence. ((pfd_previous_execution_unique_secondquotientstep) + (pfd_difference_execution_unique_secondquotientstep)) + (p) * pfa_offset_left_execution_unique_secondquotientstepsubtractresultcongruence = (pfd_input_execution_unique_secondquotientstep) + (p) * pfa_offset_right_execution_unique_secondquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_execution_unique_secondquotientstepmultiplyleft. pfa_gap_execution_unique_secondquotientstepmultiplyleft + S (pfd_inverse_execution_unique_second) = (p)) /\ (((exists pfa_gap_execution_unique_secondquotientstepmultiplyright. pfa_gap_execution_unique_secondquotientstepmultiplyright + S (pfd_difference_execution_unique_secondquotientstep) = (p)) /\ ((((exists pfa_gap_execution_unique_secondquotientstepmultiplyresultbound. pfa_gap_execution_unique_secondquotientstepmultiplyresultbound + S (pfd_value_execution_unique_secondquotient) = (p)) /\ ((exists pfa_offset_left_execution_unique_secondquotientstepmultiplyresultcongruence pfa_offset_right_execution_unique_secondquotientstepmultiplyresultcongruence. ((pfd_inverse_execution_unique_second) * (pfd_difference_execution_unique_secondquotientstep)) + (p) * pfa_offset_left_execution_unique_secondquotientstepmultiplyresultcongruence = (pfd_value_execution_unique_secondquotient) + (p) * pfa_offset_right_execution_unique_secondquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_execution_unique_secondproduct. (exists pfa_gap_execution_unique_secondproductbound. pfa_gap_execution_unique_secondproductbound + S (pfc_index_execution_unique_secondproduct) = (L)) -> exists pfc_value_execution_unique_secondproduct. ((((exists ff_h_pfp_execution_unique_secondproductentry. ff_h_pfp_execution_unique_secondproductentry + S (pfc_value_execution_unique_secondproduct) = S ((S (pfc_index_execution_unique_secondproduct)) * pfd_product_scale_execution_unique_second)) /\ exists ff_q_pfp_execution_unique_secondproductentry. pfd_product_code_execution_unique_second = ff_q_pfp_execution_unique_secondproductentry * S ((S (pfc_index_execution_unique_secondproduct)) * pfd_product_scale_execution_unique_second) + (pfc_value_execution_unique_secondproduct))) /\ ((exists pfc_terms_code_execution_unique_secondproductcoefficient pfc_terms_scale_execution_unique_secondproductcoefficient pfc_natural_sum_execution_unique_secondproductcoefficient. ((forall pfc_index_execution_unique_secondproductcoefficientdiagonal. (exists pfa_gap_execution_unique_secondproductcoefficientdiagonalbound. pfa_gap_execution_unique_secondproductcoefficientdiagonalbound + S (pfc_index_execution_unique_secondproductcoefficientdiagonal) = (S (pfc_index_execution_unique_secondproduct))) -> exists pfc_value_execution_unique_secondproductcoefficientdiagonal. ((((exists ff_h_pfp_execution_unique_secondproductcoefficientdiagonalentry. ff_h_pfp_execution_unique_secondproductcoefficientdiagonalentry + S (pfc_value_execution_unique_secondproductcoefficientdiagonal) = S ((S (pfc_index_execution_unique_secondproductcoefficientdiagonal)) * pfc_terms_scale_execution_unique_secondproductcoefficient)) /\ exists ff_q_pfp_execution_unique_secondproductcoefficientdiagonalentry. pfc_terms_code_execution_unique_secondproductcoefficient = ff_q_pfp_execution_unique_secondproductcoefficientdiagonalentry * S ((S (pfc_index_execution_unique_secondproductcoefficientdiagonal)) * pfc_terms_scale_execution_unique_secondproductcoefficient) + (pfc_value_execution_unique_secondproductcoefficientdiagonal))) /\ ((exists pfc_complement_execution_unique_secondproductcoefficientdiagonalterm pfc_left_execution_unique_secondproductcoefficientdiagonalterm pfc_right_execution_unique_secondproductcoefficientdiagonalterm. (((pfc_index_execution_unique_secondproductcoefficientdiagonal)+pfc_complement_execution_unique_secondproductcoefficientdiagonalterm=(pfc_index_execution_unique_secondproduct)) /\ ((((((exists pfa_gap_execution_unique_secondproductcoefficientdiagonaltermleftinside. pfa_gap_execution_unique_secondproductcoefficientdiagonaltermleftinside + S (pfc_index_execution_unique_secondproductcoefficientdiagonal) = (Q)) /\ ((((exists ff_h_pfp_execution_unique_secondproductcoefficientdiagonaltermleftentry. ff_h_pfp_execution_unique_secondproductcoefficientdiagonaltermleftentry + S (pfc_left_execution_unique_secondproductcoefficientdiagonalterm) = S ((S (pfc_index_execution_unique_secondproductcoefficientdiagonal)) * QC)) /\ exists ff_q_pfp_execution_unique_secondproductcoefficientdiagonaltermleftentry. QB = ff_q_pfp_execution_unique_secondproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_unique_secondproductcoefficientdiagonal)) * QC) + (pfc_left_execution_unique_secondproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_secondproductcoefficientdiagonaltermleftoutside. pfc_gap_execution_unique_secondproductcoefficientdiagonaltermleftoutside+(Q)=(pfc_index_execution_unique_secondproductcoefficientdiagonal)) /\ (((pfc_left_execution_unique_secondproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_unique_secondproductcoefficientdiagonaltermrightinside. pfa_gap_execution_unique_secondproductcoefficientdiagonaltermrightinside + S (pfc_complement_execution_unique_secondproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_unique_secondproductcoefficientdiagonaltermrightentry. ff_h_pfp_execution_unique_secondproductcoefficientdiagonaltermrightentry + S (pfc_right_execution_unique_secondproductcoefficientdiagonalterm) = S ((S (pfc_complement_execution_unique_secondproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_unique_secondproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_unique_secondproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_unique_secondproductcoefficientdiagonalterm)) * bc) + (pfc_right_execution_unique_secondproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_unique_secondproductcoefficientdiagonaltermrightoutside. pfc_gap_execution_unique_secondproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_unique_secondproductcoefficientdiagonalterm)) /\ (((pfc_right_execution_unique_secondproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_unique_secondproductcoefficientdiagonal)=pfc_left_execution_unique_secondproductcoefficientdiagonalterm*pfc_right_execution_unique_secondproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_unique_secondproductcoefficientsum fs_v_pfc_execution_unique_secondproductcoefficientsum. ((((exists fs_h_pfc_execution_unique_secondproductcoefficientsum_body_start. fs_h_pfc_execution_unique_secondproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_secondproductcoefficientsum_body_start. fs_u_pfc_execution_unique_secondproductcoefficientsum = fs_q_pfc_execution_unique_secondproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_unique_secondproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_unique_secondproductcoefficientsum_body_terminal. fs_h_pfc_execution_unique_secondproductcoefficientsum_body_terminal + S (pfc_natural_sum_execution_unique_secondproductcoefficient) = S ((S (S (pfc_index_execution_unique_secondproduct))) * fs_v_pfc_execution_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_secondproductcoefficientsum_body_terminal. fs_u_pfc_execution_unique_secondproductcoefficientsum = fs_q_pfc_execution_unique_secondproductcoefficientsum_body_terminal * S ((S (S (pfc_index_execution_unique_secondproduct))) * fs_v_pfc_execution_unique_secondproductcoefficientsum) + (pfc_natural_sum_execution_unique_secondproductcoefficient))) /\ forall fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps. (exists fs_lt_pfc_execution_unique_secondproductcoefficientsum_body_steps_bound. fs_lt_pfc_execution_unique_secondproductcoefficientsum_body_steps_bound + S fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps = S (pfc_index_execution_unique_secondproduct)) -> exists fs_a_pfc_execution_unique_secondproductcoefficientsum_body_steps fs_r_pfc_execution_unique_secondproductcoefficientsum_body_steps fs_s_pfc_execution_unique_secondproductcoefficientsum_body_steps. ((((exists fs_h_pfc_execution_unique_secondproductcoefficientsum_body_steps_summand. fs_h_pfc_execution_unique_secondproductcoefficientsum_body_steps_summand + S (fs_a_pfc_execution_unique_secondproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_unique_secondproductcoefficient)) /\ exists fs_q_pfc_execution_unique_secondproductcoefficientsum_body_steps_summand. pfc_terms_code_execution_unique_secondproductcoefficient = fs_q_pfc_execution_unique_secondproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_unique_secondproductcoefficient) + (fs_a_pfc_execution_unique_secondproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_secondproductcoefficientsum_body_steps_partial. fs_h_pfc_execution_unique_secondproductcoefficientsum_body_steps_partial + S (fs_r_pfc_execution_unique_secondproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_secondproductcoefficientsum_body_steps_partial. fs_u_pfc_execution_unique_secondproductcoefficientsum = fs_q_pfc_execution_unique_secondproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_secondproductcoefficientsum) + (fs_r_pfc_execution_unique_secondproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_unique_secondproductcoefficientsum_body_steps_successor. fs_h_pfc_execution_unique_secondproductcoefficientsum_body_steps_successor + S (fs_s_pfc_execution_unique_secondproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_execution_unique_secondproductcoefficientsum_body_steps_successor. fs_u_pfc_execution_unique_secondproductcoefficientsum = fs_q_pfc_execution_unique_secondproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_execution_unique_secondproductcoefficientsum) + (fs_s_pfc_execution_unique_secondproductcoefficientsum_body_steps))) /\ fs_s_pfc_execution_unique_secondproductcoefficientsum_body_steps = fs_r_pfc_execution_unique_secondproductcoefficientsum_body_steps + fs_a_pfc_execution_unique_secondproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_unique_secondproductcoefficientresiduebound. pfa_gap_execution_unique_secondproductcoefficientresiduebound + S (pfc_value_execution_unique_secondproduct) = (p)) /\ ((exists pfa_offset_left_execution_unique_secondproductcoefficientresiduecongruence pfa_offset_right_execution_unique_secondproductcoefficientresiduecongruence. (pfc_natural_sum_execution_unique_secondproductcoefficient) + (p) * pfa_offset_left_execution_unique_secondproductcoefficientresiduecongruence = (pfc_value_execution_unique_secondproduct) + (p) * pfa_offset_right_execution_unique_secondproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_execution_unique_seconddifference. (exists pfa_gap_execution_unique_seconddifferenceindex. pfa_gap_execution_unique_seconddifferenceindex + S (pfs_index_execution_unique_seconddifference) = (L)) -> exists pfs_left_execution_unique_seconddifference pfs_right_execution_unique_seconddifference pfs_result_execution_unique_seconddifference. ((((exists ff_h_pfp_execution_unique_seconddifferenceleft. ff_h_pfp_execution_unique_seconddifferenceleft + S (pfs_left_execution_unique_seconddifference) = S ((S (pfs_index_execution_unique_seconddifference)) * ac)) /\ exists ff_q_pfp_execution_unique_seconddifferenceleft. ab = ff_q_pfp_execution_unique_seconddifferenceleft * S ((S (pfs_index_execution_unique_seconddifference)) * ac) + (pfs_left_execution_unique_seconddifference))) /\ (((((exists ff_h_pfp_execution_unique_seconddifferenceright. ff_h_pfp_execution_unique_seconddifferenceright + S (pfs_right_execution_unique_seconddifference) = S ((S (pfs_index_execution_unique_seconddifference)) * pfd_product_scale_execution_unique_second)) /\ exists ff_q_pfp_execution_unique_seconddifferenceright. pfd_product_code_execution_unique_second = ff_q_pfp_execution_unique_seconddifferenceright * S ((S (pfs_index_execution_unique_seconddifference)) * pfd_product_scale_execution_unique_second) + (pfs_right_execution_unique_seconddifference))) /\ (((((exists ff_h_pfp_execution_unique_seconddifferenceresult. ff_h_pfp_execution_unique_seconddifferenceresult + S (pfs_result_execution_unique_seconddifference) = S ((S (pfs_index_execution_unique_seconddifference)) * pfd_residual_scale_execution_unique_second)) /\ exists ff_q_pfp_execution_unique_seconddifferenceresult. pfd_residual_code_execution_unique_second = ff_q_pfp_execution_unique_seconddifferenceresult * S ((S (pfs_index_execution_unique_seconddifference)) * pfd_residual_scale_execution_unique_second) + (pfs_result_execution_unique_seconddifference))) /\ ((((exists pfa_gap_execution_unique_seconddifferenceoperationleft. pfa_gap_execution_unique_seconddifferenceoperationleft + S (pfs_right_execution_unique_seconddifference) = (p)) /\ (((exists pfa_gap_execution_unique_seconddifferenceoperationright. pfa_gap_execution_unique_seconddifferenceoperationright + S (pfs_result_execution_unique_seconddifference) = (p)) /\ ((((exists pfa_gap_execution_unique_seconddifferenceoperationresultbound. pfa_gap_execution_unique_seconddifferenceoperationresultbound + S (pfs_left_execution_unique_seconddifference) = (p)) /\ ((exists pfa_offset_left_execution_unique_seconddifferenceoperationresultcongruence pfa_offset_right_execution_unique_seconddifferenceoperationresultcongruence. ((pfs_right_execution_unique_seconddifference) + (pfs_result_execution_unique_seconddifference)) + (p) * pfa_offset_left_execution_unique_seconddifferenceoperationresultcongruence = (pfs_left_execution_unique_seconddifference) + (p) * pfa_offset_right_execution_unique_seconddifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_execution_unique_second)+(K)) /\ (((forall fom_index_pfp_execution_unique_secondtriminput. (exists fom_gap_pfp_execution_unique_secondtriminput_index_bound. fom_gap_pfp_execution_unique_secondtriminput_index_bound + S (fom_index_pfp_execution_unique_secondtriminput) = L) -> exists fom_value_pfp_execution_unique_secondtriminput. ((((exists fom_beta_height_pfp_execution_unique_secondtriminput_entry. fom_beta_height_pfp_execution_unique_secondtriminput_entry + S (fom_value_pfp_execution_unique_secondtriminput) = S ((S (fom_index_pfp_execution_unique_secondtriminput)) * pfd_residual_scale_execution_unique_second)) /\ exists fom_beta_quotient_pfp_execution_unique_secondtriminput_entry. pfd_residual_code_execution_unique_second = fom_beta_quotient_pfp_execution_unique_secondtriminput_entry * S ((S (fom_index_pfp_execution_unique_secondtriminput)) * pfd_residual_scale_execution_unique_second) + (fom_value_pfp_execution_unique_secondtriminput))) /\ (exists fom_gap_pfp_execution_unique_secondtriminput_value_bound. fom_gap_pfp_execution_unique_secondtriminput_value_bound + S (fom_value_pfp_execution_unique_secondtriminput) = p))) /\ (((forall pfp_repeat_index_execution_unique_secondtrimremoved. (exists pfa_gap_execution_unique_secondtrimremovedindex. pfa_gap_execution_unique_secondtrimremovedindex + S (pfp_repeat_index_execution_unique_secondtrimremoved) = (pfd_cut_execution_unique_second)) -> (((exists ff_h_pfp_execution_unique_secondtrimremovedentry. ff_h_pfp_execution_unique_secondtrimremovedentry + S (0) = S ((S (pfp_repeat_index_execution_unique_secondtrimremoved)) * pfd_residual_scale_execution_unique_second)) /\ exists ff_q_pfp_execution_unique_secondtrimremovedentry. pfd_residual_code_execution_unique_second = ff_q_pfp_execution_unique_secondtrimremovedentry * S ((S (pfp_repeat_index_execution_unique_secondtrimremoved)) * pfd_residual_scale_execution_unique_second) + (0)))) /\ (((forall pftrim_index_execution_unique_secondtrimsuffix pftrim_value_execution_unique_secondtrimsuffix. (exists pfa_gap_execution_unique_secondtrimsuffixbound. pfa_gap_execution_unique_secondtrimsuffixbound + S (pftrim_index_execution_unique_secondtrimsuffix) = (K)) -> (((exists ff_h_pfp_execution_unique_secondtrimsuffixsource. ff_h_pfp_execution_unique_secondtrimsuffixsource + S (pftrim_value_execution_unique_secondtrimsuffix) = S ((S ((pfd_cut_execution_unique_second)+pftrim_index_execution_unique_secondtrimsuffix)) * pfd_residual_scale_execution_unique_second)) /\ exists ff_q_pfp_execution_unique_secondtrimsuffixsource. pfd_residual_code_execution_unique_second = ff_q_pfp_execution_unique_secondtrimsuffixsource * S ((S ((pfd_cut_execution_unique_second)+pftrim_index_execution_unique_secondtrimsuffix)) * pfd_residual_scale_execution_unique_second) + (pftrim_value_execution_unique_secondtrimsuffix))) -> (((exists ff_h_pfp_execution_unique_secondtrimsuffixoutput. ff_h_pfp_execution_unique_secondtrimsuffixoutput + S (pftrim_value_execution_unique_secondtrimsuffix) = S ((S (pftrim_index_execution_unique_secondtrimsuffix)) * RC)) /\ exists ff_q_pfp_execution_unique_secondtrimsuffixoutput. RB = ff_q_pfp_execution_unique_secondtrimsuffixoutput * S ((S (pftrim_index_execution_unique_secondtrimsuffix)) * RC) + (pftrim_value_execution_unique_secondtrimsuffix)))) /\ (((K)=0 \/ (exists pftrim_leading_execution_unique_secondtrimnormal. ((((exists ff_h_pfp_execution_unique_secondtrimnormalentry. ff_h_pfp_execution_unique_secondtrimnormalentry + S (pftrim_leading_execution_unique_secondtrimnormal) = S ((S (0)) * RC)) /\ exists ff_q_pfp_execution_unique_secondtrimnormalentry. RB = ff_q_pfp_execution_unique_secondtrimnormalentry * S ((S (0)) * RC) + (pftrim_leading_execution_unique_secondtrimnormal))) /\ ((~(pftrim_leading_execution_unique_secondtrimnormal=0))))))))))))))))))))))))))))))))) -> ((((q)=(Q)) /\ (((forall mdr_i_pfp_execution_unique_outputsquotient mdr_a_pfp_execution_unique_outputsquotient. (exists mdr_gap_pfp_execution_unique_outputsquotientb. mdr_gap_pfp_execution_unique_outputsquotientb + S (mdr_i_pfp_execution_unique_outputsquotient) = (q)) -> (((exists ff_h_mdr_pfp_execution_unique_outputsquotiento. ff_h_mdr_pfp_execution_unique_outputsquotiento + S (mdr_a_pfp_execution_unique_outputsquotient) = S ((S (mdr_i_pfp_execution_unique_outputsquotient)) * qc)) /\ exists ff_q_mdr_pfp_execution_unique_outputsquotiento. qb = ff_q_mdr_pfp_execution_unique_outputsquotiento * S ((S (mdr_i_pfp_execution_unique_outputsquotient)) * qc) + (mdr_a_pfp_execution_unique_outputsquotient))) -> (((exists ff_h_mdr_pfp_execution_unique_outputsquotientn. ff_h_mdr_pfp_execution_unique_outputsquotientn + S (mdr_a_pfp_execution_unique_outputsquotient) = S ((S (mdr_i_pfp_execution_unique_outputsquotient)) * QC)) /\ exists ff_q_mdr_pfp_execution_unique_outputsquotientn. QB = ff_q_mdr_pfp_execution_unique_outputsquotientn * S ((S (mdr_i_pfp_execution_unique_outputsquotient)) * QC) + (mdr_a_pfp_execution_unique_outputsquotient)))) /\ ((((R)=(K)) /\ ((forall mdr_i_pfp_execution_unique_outputsremainder mdr_a_pfp_execution_unique_outputsremainder. (exists mdr_gap_pfp_execution_unique_outputsremainderb. mdr_gap_pfp_execution_unique_outputsremainderb + S (mdr_i_pfp_execution_unique_outputsremainder) = (R)) -> (((exists ff_h_mdr_pfp_execution_unique_outputsremaindero. ff_h_mdr_pfp_execution_unique_outputsremaindero + S (mdr_a_pfp_execution_unique_outputsremainder) = S ((S (mdr_i_pfp_execution_unique_outputsremainder)) * rc)) /\ exists ff_q_mdr_pfp_execution_unique_outputsremaindero. rb = ff_q_mdr_pfp_execution_unique_outputsremaindero * S ((S (mdr_i_pfp_execution_unique_outputsremainder)) * rc) + (mdr_a_pfp_execution_unique_outputsremainder))) -> (((exists ff_h_mdr_pfp_execution_unique_outputsremaindern. ff_h_mdr_pfp_execution_unique_outputsremaindern + S (mdr_a_pfp_execution_unique_outputsremainder) = S ((S (mdr_i_pfp_execution_unique_outputsremainder)) * RC)) /\ exists ff_q_mdr_pfp_execution_unique_outputsremaindern. RB = ff_q_mdr_pfp_execution_unique_outputsremaindern * S ((S (mdr_i_pfp_execution_unique_outputsremainder)) * RC) + (mdr_a_pfp_execution_unique_outputsremainder)))))))))))