prime_field_polynomial_division_execution_aligned_identity

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d qb qc q rb rc R. (~((p) = 1) /\ forall pfa_factor_left_execution_aligned_prime pfa_factor_right_execution_aligned_prime. (p) = pfa_factor_left_execution_aligned_prime * pfa_factor_right_execution_aligned_prime -> pfa_factor_left_execution_aligned_prime = 1 \/ pfa_factor_right_execution_aligned_prime = 1) -> (((forall fom_index_pfp_execution_aligned_sourceinput. (exists fom_gap_pfp_execution_aligned_sourceinput_index_bound. fom_gap_pfp_execution_aligned_sourceinput_index_bound + S (fom_index_pfp_execution_aligned_sourceinput) = L) -> exists fom_value_pfp_execution_aligned_sourceinput. ((((exists fom_beta_height_pfp_execution_aligned_sourceinput_entry. fom_beta_height_pfp_execution_aligned_sourceinput_entry + S (fom_value_pfp_execution_aligned_sourceinput) = S ((S (fom_index_pfp_execution_aligned_sourceinput)) * ac)) /\ exists fom_beta_quotient_pfp_execution_aligned_sourceinput_entry. ab = fom_beta_quotient_pfp_execution_aligned_sourceinput_entry * S ((S (fom_index_pfp_execution_aligned_sourceinput)) * ac) + (fom_value_pfp_execution_aligned_sourceinput))) /\ (exists fom_gap_pfp_execution_aligned_sourceinput_value_bound. fom_gap_pfp_execution_aligned_sourceinput_value_bound + S (fom_value_pfp_execution_aligned_sourceinput) = p))) /\ (((forall fom_index_pfp_execution_aligned_sourcedivisor. (exists fom_gap_pfp_execution_aligned_sourcedivisor_index_bound. fom_gap_pfp_execution_aligned_sourcedivisor_index_bound + S (fom_index_pfp_execution_aligned_sourcedivisor) = S (d)) -> exists fom_value_pfp_execution_aligned_sourcedivisor. ((((exists fom_beta_height_pfp_execution_aligned_sourcedivisor_entry. fom_beta_height_pfp_execution_aligned_sourcedivisor_entry + S (fom_value_pfp_execution_aligned_sourcedivisor) = S ((S (fom_index_pfp_execution_aligned_sourcedivisor)) * bc)) /\ exists fom_beta_quotient_pfp_execution_aligned_sourcedivisor_entry. bb = fom_beta_quotient_pfp_execution_aligned_sourcedivisor_entry * S ((S (fom_index_pfp_execution_aligned_sourcedivisor)) * bc) + (fom_value_pfp_execution_aligned_sourcedivisor))) /\ (exists fom_gap_pfp_execution_aligned_sourcedivisor_value_bound. fom_gap_pfp_execution_aligned_sourcedivisor_value_bound + S (fom_value_pfp_execution_aligned_sourcedivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_execution_aligned_sourcelengthshort. pfc_gap_execution_aligned_sourcelengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_execution_aligned_source pfd_inverse_execution_aligned_source pfd_product_code_execution_aligned_source pfd_product_scale_execution_aligned_source pfd_residual_code_execution_aligned_source pfd_residual_scale_execution_aligned_source pfd_cut_execution_aligned_source. ((((exists ff_h_pfp_execution_aligned_sourcehead. ff_h_pfp_execution_aligned_sourcehead + S (pfd_head_execution_aligned_source) = S ((S (0)) * bc)) /\ exists ff_q_pfp_execution_aligned_sourcehead. bb = ff_q_pfp_execution_aligned_sourcehead * S ((S (0)) * bc) + (pfd_head_execution_aligned_source))) /\ (((((~((pfd_head_execution_aligned_source) = 0)) /\ ((((exists pfa_gap_execution_aligned_sourceinversemultiplicationleft. pfa_gap_execution_aligned_sourceinversemultiplicationleft + S (pfd_head_execution_aligned_source) = (p)) /\ (((exists pfa_gap_execution_aligned_sourceinversemultiplicationright. pfa_gap_execution_aligned_sourceinversemultiplicationright + S (pfd_inverse_execution_aligned_source) = (p)) /\ ((((exists pfa_gap_execution_aligned_sourceinversemultiplicationresultbound. pfa_gap_execution_aligned_sourceinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sourceinversemultiplicationresultcongruence pfa_offset_right_execution_aligned_sourceinversemultiplicationresultcongruence. ((pfd_head_execution_aligned_source) * (pfd_inverse_execution_aligned_source)) + (p) * pfa_offset_left_execution_aligned_sourceinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_execution_aligned_sourceinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_execution_aligned_sourcequotient. (exists pfa_gap_execution_aligned_sourcequotientbound. pfa_gap_execution_aligned_sourcequotientbound + S (pfd_index_execution_aligned_sourcequotient) = (q)) -> exists pfd_value_execution_aligned_sourcequotient. ((((exists ff_h_pfp_execution_aligned_sourcequotiententry. ff_h_pfp_execution_aligned_sourcequotiententry + S (pfd_value_execution_aligned_sourcequotient) = S ((S (pfd_index_execution_aligned_sourcequotient)) * qc)) /\ exists ff_q_pfp_execution_aligned_sourcequotiententry. qb = ff_q_pfp_execution_aligned_sourcequotiententry * S ((S (pfd_index_execution_aligned_sourcequotient)) * qc) + (pfd_value_execution_aligned_sourcequotient))) /\ ((exists pfd_input_execution_aligned_sourcequotientstep pfd_previous_execution_aligned_sourcequotientstep pfd_difference_execution_aligned_sourcequotientstep. ((((exists ff_h_pfp_execution_aligned_sourcequotientstepinput. ff_h_pfp_execution_aligned_sourcequotientstepinput + S (pfd_input_execution_aligned_sourcequotientstep) = S ((S (pfd_index_execution_aligned_sourcequotient)) * ac)) /\ exists ff_q_pfp_execution_aligned_sourcequotientstepinput. ab = ff_q_pfp_execution_aligned_sourcequotientstepinput * S ((S (pfd_index_execution_aligned_sourcequotient)) * ac) + (pfd_input_execution_aligned_sourcequotientstep))) /\ (((exists pfc_terms_code_execution_aligned_sourcequotientstepprevious pfc_terms_scale_execution_aligned_sourcequotientstepprevious pfc_natural_sum_execution_aligned_sourcequotientstepprevious. ((forall pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal. (exists pfa_gap_execution_aligned_sourcequotientsteppreviousdiagonalbound. pfa_gap_execution_aligned_sourcequotientsteppreviousdiagonalbound + S (pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal) = (S (pfd_index_execution_aligned_sourcequotient))) -> exists pfc_value_execution_aligned_sourcequotientsteppreviousdiagonal. ((((exists ff_h_pfp_execution_aligned_sourcequotientsteppreviousdiagonalentry. ff_h_pfp_execution_aligned_sourcequotientsteppreviousdiagonalentry + S (pfc_value_execution_aligned_sourcequotientsteppreviousdiagonal) = S ((S (pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal)) * pfc_terms_scale_execution_aligned_sourcequotientstepprevious)) /\ exists ff_q_pfp_execution_aligned_sourcequotientsteppreviousdiagonalentry. pfc_terms_code_execution_aligned_sourcequotientstepprevious = ff_q_pfp_execution_aligned_sourcequotientsteppreviousdiagonalentry * S ((S (pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal)) * pfc_terms_scale_execution_aligned_sourcequotientstepprevious) + (pfc_value_execution_aligned_sourcequotientsteppreviousdiagonal))) /\ ((exists pfc_complement_execution_aligned_sourcequotientsteppreviousdiagonalterm pfc_left_execution_aligned_sourcequotientsteppreviousdiagonalterm pfc_right_execution_aligned_sourcequotientsteppreviousdiagonalterm. (((pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal)+pfc_complement_execution_aligned_sourcequotientsteppreviousdiagonalterm=(pfd_index_execution_aligned_sourcequotient)) /\ ((((((exists pfa_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermleftinside. pfa_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermleftinside + S (pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal) = (pfd_index_execution_aligned_sourcequotient)) /\ ((((exists ff_h_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermleftentry. ff_h_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermleftentry + S (pfc_left_execution_aligned_sourcequotientsteppreviousdiagonalterm) = S ((S (pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal)) * qc) + (pfc_left_execution_aligned_sourcequotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermleftoutside. pfc_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermleftoutside+(pfd_index_execution_aligned_sourcequotient)=(pfc_index_execution_aligned_sourcequotientsteppreviousdiagonal)) /\ (((pfc_left_execution_aligned_sourcequotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermrightinside. pfa_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermrightinside + S (pfc_complement_execution_aligned_sourcequotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermrightentry. ff_h_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermrightentry + S (pfc_right_execution_aligned_sourcequotientsteppreviousdiagonalterm) = S ((S (pfc_complement_execution_aligned_sourcequotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_execution_aligned_sourcequotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_execution_aligned_sourcequotientsteppreviousdiagonalterm)) * bc) + (pfc_right_execution_aligned_sourcequotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermrightoutside. pfc_gap_execution_aligned_sourcequotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_aligned_sourcequotientsteppreviousdiagonalterm)) /\ (((pfc_right_execution_aligned_sourcequotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_execution_aligned_sourcequotientsteppreviousdiagonal)=pfc_left_execution_aligned_sourcequotientsteppreviousdiagonalterm*pfc_right_execution_aligned_sourcequotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_aligned_sourcequotientstepprevioussum fs_v_pfc_execution_aligned_sourcequotientstepprevioussum. ((((exists fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_start. fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum)) /\ exists fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_start. fs_u_pfc_execution_aligned_sourcequotientstepprevioussum = fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_terminal. fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_terminal + S (pfc_natural_sum_execution_aligned_sourcequotientstepprevious) = S ((S (S (pfd_index_execution_aligned_sourcequotient))) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum)) /\ exists fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_terminal. fs_u_pfc_execution_aligned_sourcequotientstepprevioussum = fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_terminal * S ((S (S (pfd_index_execution_aligned_sourcequotient))) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum) + (pfc_natural_sum_execution_aligned_sourcequotientstepprevious))) /\ forall fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps. (exists fs_lt_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_bound. fs_lt_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_bound + S fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps = S (pfd_index_execution_aligned_sourcequotient)) -> exists fs_a_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps fs_r_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps fs_s_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps. ((((exists fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_summand. fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_summand + S (fs_a_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_aligned_sourcequotientstepprevious)) /\ exists fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_summand. pfc_terms_code_execution_aligned_sourcequotientstepprevious = fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)) * pfc_terms_scale_execution_aligned_sourcequotientstepprevious) + (fs_a_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_partial. fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_partial + S (fs_r_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum)) /\ exists fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_partial. fs_u_pfc_execution_aligned_sourcequotientstepprevioussum = fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum) + (fs_r_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_successor. fs_h_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_successor + S (fs_s_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum)) /\ exists fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_successor. fs_u_pfc_execution_aligned_sourcequotientstepprevioussum = fs_q_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)) * fs_v_pfc_execution_aligned_sourcequotientstepprevioussum) + (fs_s_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps))) /\ fs_s_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps = fs_r_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps + fs_a_pfc_execution_aligned_sourcequotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_execution_aligned_sourcequotientsteppreviousresiduebound. pfa_gap_execution_aligned_sourcequotientsteppreviousresiduebound + S (pfd_previous_execution_aligned_sourcequotientstep) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sourcequotientsteppreviousresiduecongruence pfa_offset_right_execution_aligned_sourcequotientsteppreviousresiduecongruence. (pfc_natural_sum_execution_aligned_sourcequotientstepprevious) + (p) * pfa_offset_left_execution_aligned_sourcequotientsteppreviousresiduecongruence = (pfd_previous_execution_aligned_sourcequotientstep) + (p) * pfa_offset_right_execution_aligned_sourcequotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_execution_aligned_sourcequotientstepsubtractleft. pfa_gap_execution_aligned_sourcequotientstepsubtractleft + S (pfd_previous_execution_aligned_sourcequotientstep) = (p)) /\ (((exists pfa_gap_execution_aligned_sourcequotientstepsubtractright. pfa_gap_execution_aligned_sourcequotientstepsubtractright + S (pfd_difference_execution_aligned_sourcequotientstep) = (p)) /\ ((((exists pfa_gap_execution_aligned_sourcequotientstepsubtractresultbound. pfa_gap_execution_aligned_sourcequotientstepsubtractresultbound + S (pfd_input_execution_aligned_sourcequotientstep) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sourcequotientstepsubtractresultcongruence pfa_offset_right_execution_aligned_sourcequotientstepsubtractresultcongruence. ((pfd_previous_execution_aligned_sourcequotientstep) + (pfd_difference_execution_aligned_sourcequotientstep)) + (p) * pfa_offset_left_execution_aligned_sourcequotientstepsubtractresultcongruence = (pfd_input_execution_aligned_sourcequotientstep) + (p) * pfa_offset_right_execution_aligned_sourcequotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_execution_aligned_sourcequotientstepmultiplyleft. pfa_gap_execution_aligned_sourcequotientstepmultiplyleft + S (pfd_inverse_execution_aligned_source) = (p)) /\ (((exists pfa_gap_execution_aligned_sourcequotientstepmultiplyright. pfa_gap_execution_aligned_sourcequotientstepmultiplyright + S (pfd_difference_execution_aligned_sourcequotientstep) = (p)) /\ ((((exists pfa_gap_execution_aligned_sourcequotientstepmultiplyresultbound. pfa_gap_execution_aligned_sourcequotientstepmultiplyresultbound + S (pfd_value_execution_aligned_sourcequotient) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sourcequotientstepmultiplyresultcongruence pfa_offset_right_execution_aligned_sourcequotientstepmultiplyresultcongruence. ((pfd_inverse_execution_aligned_source) * (pfd_difference_execution_aligned_sourcequotientstep)) + (p) * pfa_offset_left_execution_aligned_sourcequotientstepmultiplyresultcongruence = (pfd_value_execution_aligned_sourcequotient) + (p) * pfa_offset_right_execution_aligned_sourcequotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_execution_aligned_sourceproduct. (exists pfa_gap_execution_aligned_sourceproductbound. pfa_gap_execution_aligned_sourceproductbound + S (pfc_index_execution_aligned_sourceproduct) = (L)) -> exists pfc_value_execution_aligned_sourceproduct. ((((exists ff_h_pfp_execution_aligned_sourceproductentry. ff_h_pfp_execution_aligned_sourceproductentry + S (pfc_value_execution_aligned_sourceproduct) = S ((S (pfc_index_execution_aligned_sourceproduct)) * pfd_product_scale_execution_aligned_source)) /\ exists ff_q_pfp_execution_aligned_sourceproductentry. pfd_product_code_execution_aligned_source = ff_q_pfp_execution_aligned_sourceproductentry * S ((S (pfc_index_execution_aligned_sourceproduct)) * pfd_product_scale_execution_aligned_source) + (pfc_value_execution_aligned_sourceproduct))) /\ ((exists pfc_terms_code_execution_aligned_sourceproductcoefficient pfc_terms_scale_execution_aligned_sourceproductcoefficient pfc_natural_sum_execution_aligned_sourceproductcoefficient. ((forall pfc_index_execution_aligned_sourceproductcoefficientdiagonal. (exists pfa_gap_execution_aligned_sourceproductcoefficientdiagonalbound. pfa_gap_execution_aligned_sourceproductcoefficientdiagonalbound + S (pfc_index_execution_aligned_sourceproductcoefficientdiagonal) = (S (pfc_index_execution_aligned_sourceproduct))) -> exists pfc_value_execution_aligned_sourceproductcoefficientdiagonal. ((((exists ff_h_pfp_execution_aligned_sourceproductcoefficientdiagonalentry. ff_h_pfp_execution_aligned_sourceproductcoefficientdiagonalentry + S (pfc_value_execution_aligned_sourceproductcoefficientdiagonal) = S ((S (pfc_index_execution_aligned_sourceproductcoefficientdiagonal)) * pfc_terms_scale_execution_aligned_sourceproductcoefficient)) /\ exists ff_q_pfp_execution_aligned_sourceproductcoefficientdiagonalentry. pfc_terms_code_execution_aligned_sourceproductcoefficient = ff_q_pfp_execution_aligned_sourceproductcoefficientdiagonalentry * S ((S (pfc_index_execution_aligned_sourceproductcoefficientdiagonal)) * pfc_terms_scale_execution_aligned_sourceproductcoefficient) + (pfc_value_execution_aligned_sourceproductcoefficientdiagonal))) /\ ((exists pfc_complement_execution_aligned_sourceproductcoefficientdiagonalterm pfc_left_execution_aligned_sourceproductcoefficientdiagonalterm pfc_right_execution_aligned_sourceproductcoefficientdiagonalterm. (((pfc_index_execution_aligned_sourceproductcoefficientdiagonal)+pfc_complement_execution_aligned_sourceproductcoefficientdiagonalterm=(pfc_index_execution_aligned_sourceproduct)) /\ ((((((exists pfa_gap_execution_aligned_sourceproductcoefficientdiagonaltermleftinside. pfa_gap_execution_aligned_sourceproductcoefficientdiagonaltermleftinside + S (pfc_index_execution_aligned_sourceproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_execution_aligned_sourceproductcoefficientdiagonaltermleftentry. ff_h_pfp_execution_aligned_sourceproductcoefficientdiagonaltermleftentry + S (pfc_left_execution_aligned_sourceproductcoefficientdiagonalterm) = S ((S (pfc_index_execution_aligned_sourceproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_execution_aligned_sourceproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_execution_aligned_sourceproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_aligned_sourceproductcoefficientdiagonal)) * qc) + (pfc_left_execution_aligned_sourceproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_aligned_sourceproductcoefficientdiagonaltermleftoutside. pfc_gap_execution_aligned_sourceproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_execution_aligned_sourceproductcoefficientdiagonal)) /\ (((pfc_left_execution_aligned_sourceproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_aligned_sourceproductcoefficientdiagonaltermrightinside. pfa_gap_execution_aligned_sourceproductcoefficientdiagonaltermrightinside + S (pfc_complement_execution_aligned_sourceproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_execution_aligned_sourceproductcoefficientdiagonaltermrightentry. ff_h_pfp_execution_aligned_sourceproductcoefficientdiagonaltermrightentry + S (pfc_right_execution_aligned_sourceproductcoefficientdiagonalterm) = S ((S (pfc_complement_execution_aligned_sourceproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_aligned_sourceproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_aligned_sourceproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_aligned_sourceproductcoefficientdiagonalterm)) * bc) + (pfc_right_execution_aligned_sourceproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_aligned_sourceproductcoefficientdiagonaltermrightoutside. pfc_gap_execution_aligned_sourceproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_execution_aligned_sourceproductcoefficientdiagonalterm)) /\ (((pfc_right_execution_aligned_sourceproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_aligned_sourceproductcoefficientdiagonal)=pfc_left_execution_aligned_sourceproductcoefficientdiagonalterm*pfc_right_execution_aligned_sourceproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_aligned_sourceproductcoefficientsum fs_v_pfc_execution_aligned_sourceproductcoefficientsum. ((((exists fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_start. fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum)) /\ exists fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_start. fs_u_pfc_execution_aligned_sourceproductcoefficientsum = fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_terminal. fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_terminal + S (pfc_natural_sum_execution_aligned_sourceproductcoefficient) = S ((S (S (pfc_index_execution_aligned_sourceproduct))) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum)) /\ exists fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_terminal. fs_u_pfc_execution_aligned_sourceproductcoefficientsum = fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_terminal * S ((S (S (pfc_index_execution_aligned_sourceproduct))) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum) + (pfc_natural_sum_execution_aligned_sourceproductcoefficient))) /\ forall fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps. (exists fs_lt_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_bound. fs_lt_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_bound + S fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps = S (pfc_index_execution_aligned_sourceproduct)) -> exists fs_a_pfc_execution_aligned_sourceproductcoefficientsum_body_steps fs_r_pfc_execution_aligned_sourceproductcoefficientsum_body_steps fs_s_pfc_execution_aligned_sourceproductcoefficientsum_body_steps. ((((exists fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_summand. fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_summand + S (fs_a_pfc_execution_aligned_sourceproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_aligned_sourceproductcoefficient)) /\ exists fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_summand. pfc_terms_code_execution_aligned_sourceproductcoefficient = fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)) * pfc_terms_scale_execution_aligned_sourceproductcoefficient) + (fs_a_pfc_execution_aligned_sourceproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_partial. fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_partial + S (fs_r_pfc_execution_aligned_sourceproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum)) /\ exists fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_partial. fs_u_pfc_execution_aligned_sourceproductcoefficientsum = fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum) + (fs_r_pfc_execution_aligned_sourceproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_successor. fs_h_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_successor + S (fs_s_pfc_execution_aligned_sourceproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum)) /\ exists fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_successor. fs_u_pfc_execution_aligned_sourceproductcoefficientsum = fs_q_pfc_execution_aligned_sourceproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_sourceproductcoefficientsum) + (fs_s_pfc_execution_aligned_sourceproductcoefficientsum_body_steps))) /\ fs_s_pfc_execution_aligned_sourceproductcoefficientsum_body_steps = fs_r_pfc_execution_aligned_sourceproductcoefficientsum_body_steps + fs_a_pfc_execution_aligned_sourceproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_aligned_sourceproductcoefficientresiduebound. pfa_gap_execution_aligned_sourceproductcoefficientresiduebound + S (pfc_value_execution_aligned_sourceproduct) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sourceproductcoefficientresiduecongruence pfa_offset_right_execution_aligned_sourceproductcoefficientresiduecongruence. (pfc_natural_sum_execution_aligned_sourceproductcoefficient) + (p) * pfa_offset_left_execution_aligned_sourceproductcoefficientresiduecongruence = (pfc_value_execution_aligned_sourceproduct) + (p) * pfa_offset_right_execution_aligned_sourceproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_execution_aligned_sourcedifference. (exists pfa_gap_execution_aligned_sourcedifferenceindex. pfa_gap_execution_aligned_sourcedifferenceindex + S (pfs_index_execution_aligned_sourcedifference) = (L)) -> exists pfs_left_execution_aligned_sourcedifference pfs_right_execution_aligned_sourcedifference pfs_result_execution_aligned_sourcedifference. ((((exists ff_h_pfp_execution_aligned_sourcedifferenceleft. ff_h_pfp_execution_aligned_sourcedifferenceleft + S (pfs_left_execution_aligned_sourcedifference) = S ((S (pfs_index_execution_aligned_sourcedifference)) * ac)) /\ exists ff_q_pfp_execution_aligned_sourcedifferenceleft. ab = ff_q_pfp_execution_aligned_sourcedifferenceleft * S ((S (pfs_index_execution_aligned_sourcedifference)) * ac) + (pfs_left_execution_aligned_sourcedifference))) /\ (((((exists ff_h_pfp_execution_aligned_sourcedifferenceright. ff_h_pfp_execution_aligned_sourcedifferenceright + S (pfs_right_execution_aligned_sourcedifference) = S ((S (pfs_index_execution_aligned_sourcedifference)) * pfd_product_scale_execution_aligned_source)) /\ exists ff_q_pfp_execution_aligned_sourcedifferenceright. pfd_product_code_execution_aligned_source = ff_q_pfp_execution_aligned_sourcedifferenceright * S ((S (pfs_index_execution_aligned_sourcedifference)) * pfd_product_scale_execution_aligned_source) + (pfs_right_execution_aligned_sourcedifference))) /\ (((((exists ff_h_pfp_execution_aligned_sourcedifferenceresult. ff_h_pfp_execution_aligned_sourcedifferenceresult + S (pfs_result_execution_aligned_sourcedifference) = S ((S (pfs_index_execution_aligned_sourcedifference)) * pfd_residual_scale_execution_aligned_source)) /\ exists ff_q_pfp_execution_aligned_sourcedifferenceresult. pfd_residual_code_execution_aligned_source = ff_q_pfp_execution_aligned_sourcedifferenceresult * S ((S (pfs_index_execution_aligned_sourcedifference)) * pfd_residual_scale_execution_aligned_source) + (pfs_result_execution_aligned_sourcedifference))) /\ ((((exists pfa_gap_execution_aligned_sourcedifferenceoperationleft. pfa_gap_execution_aligned_sourcedifferenceoperationleft + S (pfs_right_execution_aligned_sourcedifference) = (p)) /\ (((exists pfa_gap_execution_aligned_sourcedifferenceoperationright. pfa_gap_execution_aligned_sourcedifferenceoperationright + S (pfs_result_execution_aligned_sourcedifference) = (p)) /\ ((((exists pfa_gap_execution_aligned_sourcedifferenceoperationresultbound. pfa_gap_execution_aligned_sourcedifferenceoperationresultbound + S (pfs_left_execution_aligned_sourcedifference) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sourcedifferenceoperationresultcongruence pfa_offset_right_execution_aligned_sourcedifferenceoperationresultcongruence. ((pfs_right_execution_aligned_sourcedifference) + (pfs_result_execution_aligned_sourcedifference)) + (p) * pfa_offset_left_execution_aligned_sourcedifferenceoperationresultcongruence = (pfs_left_execution_aligned_sourcedifference) + (p) * pfa_offset_right_execution_aligned_sourcedifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_execution_aligned_source)+(R)) /\ (((forall fom_index_pfp_execution_aligned_sourcetriminput. (exists fom_gap_pfp_execution_aligned_sourcetriminput_index_bound. fom_gap_pfp_execution_aligned_sourcetriminput_index_bound + S (fom_index_pfp_execution_aligned_sourcetriminput) = L) -> exists fom_value_pfp_execution_aligned_sourcetriminput. ((((exists fom_beta_height_pfp_execution_aligned_sourcetriminput_entry. fom_beta_height_pfp_execution_aligned_sourcetriminput_entry + S (fom_value_pfp_execution_aligned_sourcetriminput) = S ((S (fom_index_pfp_execution_aligned_sourcetriminput)) * pfd_residual_scale_execution_aligned_source)) /\ exists fom_beta_quotient_pfp_execution_aligned_sourcetriminput_entry. pfd_residual_code_execution_aligned_source = fom_beta_quotient_pfp_execution_aligned_sourcetriminput_entry * S ((S (fom_index_pfp_execution_aligned_sourcetriminput)) * pfd_residual_scale_execution_aligned_source) + (fom_value_pfp_execution_aligned_sourcetriminput))) /\ (exists fom_gap_pfp_execution_aligned_sourcetriminput_value_bound. fom_gap_pfp_execution_aligned_sourcetriminput_value_bound + S (fom_value_pfp_execution_aligned_sourcetriminput) = p))) /\ (((forall pfp_repeat_index_execution_aligned_sourcetrimremoved. (exists pfa_gap_execution_aligned_sourcetrimremovedindex. pfa_gap_execution_aligned_sourcetrimremovedindex + S (pfp_repeat_index_execution_aligned_sourcetrimremoved) = (pfd_cut_execution_aligned_source)) -> (((exists ff_h_pfp_execution_aligned_sourcetrimremovedentry. ff_h_pfp_execution_aligned_sourcetrimremovedentry + S (0) = S ((S (pfp_repeat_index_execution_aligned_sourcetrimremoved)) * pfd_residual_scale_execution_aligned_source)) /\ exists ff_q_pfp_execution_aligned_sourcetrimremovedentry. pfd_residual_code_execution_aligned_source = ff_q_pfp_execution_aligned_sourcetrimremovedentry * S ((S (pfp_repeat_index_execution_aligned_sourcetrimremoved)) * pfd_residual_scale_execution_aligned_source) + (0)))) /\ (((forall pftrim_index_execution_aligned_sourcetrimsuffix pftrim_value_execution_aligned_sourcetrimsuffix. (exists pfa_gap_execution_aligned_sourcetrimsuffixbound. pfa_gap_execution_aligned_sourcetrimsuffixbound + S (pftrim_index_execution_aligned_sourcetrimsuffix) = (R)) -> (((exists ff_h_pfp_execution_aligned_sourcetrimsuffixsource. ff_h_pfp_execution_aligned_sourcetrimsuffixsource + S (pftrim_value_execution_aligned_sourcetrimsuffix) = S ((S ((pfd_cut_execution_aligned_source)+pftrim_index_execution_aligned_sourcetrimsuffix)) * pfd_residual_scale_execution_aligned_source)) /\ exists ff_q_pfp_execution_aligned_sourcetrimsuffixsource. pfd_residual_code_execution_aligned_source = ff_q_pfp_execution_aligned_sourcetrimsuffixsource * S ((S ((pfd_cut_execution_aligned_source)+pftrim_index_execution_aligned_sourcetrimsuffix)) * pfd_residual_scale_execution_aligned_source) + (pftrim_value_execution_aligned_sourcetrimsuffix))) -> (((exists ff_h_pfp_execution_aligned_sourcetrimsuffixoutput. ff_h_pfp_execution_aligned_sourcetrimsuffixoutput + S (pftrim_value_execution_aligned_sourcetrimsuffix) = S ((S (pftrim_index_execution_aligned_sourcetrimsuffix)) * rc)) /\ exists ff_q_pfp_execution_aligned_sourcetrimsuffixoutput. rb = ff_q_pfp_execution_aligned_sourcetrimsuffixoutput * S ((S (pftrim_index_execution_aligned_sourcetrimsuffix)) * rc) + (pftrim_value_execution_aligned_sourcetrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_execution_aligned_sourcetrimnormal. ((((exists ff_h_pfp_execution_aligned_sourcetrimnormalentry. ff_h_pfp_execution_aligned_sourcetrimnormalentry + S (pftrim_leading_execution_aligned_sourcetrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_execution_aligned_sourcetrimnormalentry. rb = ff_q_pfp_execution_aligned_sourcetrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_execution_aligned_sourcetrimnormal))) /\ ((~(pftrim_leading_execution_aligned_sourcetrimnormal=0))))))))))))))))))))))))))))))))) -> (exists pb pc N. ((((forall fom_index_pfp_execution_aligned_productleft. (exists fom_gap_pfp_execution_aligned_productleft_index_bound. fom_gap_pfp_execution_aligned_productleft_index_bound + S (fom_index_pfp_execution_aligned_productleft) = q) -> exists fom_value_pfp_execution_aligned_productleft. ((((exists fom_beta_height_pfp_execution_aligned_productleft_entry. fom_beta_height_pfp_execution_aligned_productleft_entry + S (fom_value_pfp_execution_aligned_productleft) = S ((S (fom_index_pfp_execution_aligned_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_execution_aligned_productleft_entry. qb = fom_beta_quotient_pfp_execution_aligned_productleft_entry * S ((S (fom_index_pfp_execution_aligned_productleft)) * qc) + (fom_value_pfp_execution_aligned_productleft))) /\ (exists fom_gap_pfp_execution_aligned_productleft_value_bound. fom_gap_pfp_execution_aligned_productleft_value_bound + S (fom_value_pfp_execution_aligned_productleft) = p))) /\ (((forall fom_index_pfp_execution_aligned_productright. (exists fom_gap_pfp_execution_aligned_productright_index_bound. fom_gap_pfp_execution_aligned_productright_index_bound + S (fom_index_pfp_execution_aligned_productright) = S d) -> exists fom_value_pfp_execution_aligned_productright. ((((exists fom_beta_height_pfp_execution_aligned_productright_entry. fom_beta_height_pfp_execution_aligned_productright_entry + S (fom_value_pfp_execution_aligned_productright) = S ((S (fom_index_pfp_execution_aligned_productright)) * bc)) /\ exists fom_beta_quotient_pfp_execution_aligned_productright_entry. bb = fom_beta_quotient_pfp_execution_aligned_productright_entry * S ((S (fom_index_pfp_execution_aligned_productright)) * bc) + (fom_value_pfp_execution_aligned_productright))) /\ (exists fom_gap_pfp_execution_aligned_productright_value_bound. fom_gap_pfp_execution_aligned_productright_value_bound + S (fom_value_pfp_execution_aligned_productright) = p))) /\ (((((((q)=0 \/ (S d)=0) /\ (((N)=0)))) \/ (((~((q)=0)) /\ (((~((S d)=0)) /\ (((q)+(S d)=S (N)))))))) /\ ((forall pfc_index_execution_aligned_productcoefficients. (exists pfa_gap_execution_aligned_productcoefficientsbound. pfa_gap_execution_aligned_productcoefficientsbound + S (pfc_index_execution_aligned_productcoefficients) = (N)) -> exists pfc_value_execution_aligned_productcoefficients. ((((exists ff_h_pfp_execution_aligned_productcoefficientsentry. ff_h_pfp_execution_aligned_productcoefficientsentry + S (pfc_value_execution_aligned_productcoefficients) = S ((S (pfc_index_execution_aligned_productcoefficients)) * pc)) /\ exists ff_q_pfp_execution_aligned_productcoefficientsentry. pb = ff_q_pfp_execution_aligned_productcoefficientsentry * S ((S (pfc_index_execution_aligned_productcoefficients)) * pc) + (pfc_value_execution_aligned_productcoefficients))) /\ ((exists pfc_terms_code_execution_aligned_productcoefficientscoefficient pfc_terms_scale_execution_aligned_productcoefficientscoefficient pfc_natural_sum_execution_aligned_productcoefficientscoefficient. ((forall pfc_index_execution_aligned_productcoefficientscoefficientdiagonal. (exists pfa_gap_execution_aligned_productcoefficientscoefficientdiagonalbound. pfa_gap_execution_aligned_productcoefficientscoefficientdiagonalbound + S (pfc_index_execution_aligned_productcoefficientscoefficientdiagonal) = (S (pfc_index_execution_aligned_productcoefficients))) -> exists pfc_value_execution_aligned_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_execution_aligned_productcoefficientscoefficientdiagonalentry. ff_h_pfp_execution_aligned_productcoefficientscoefficientdiagonalentry + S (pfc_value_execution_aligned_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_execution_aligned_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_aligned_productcoefficientscoefficient)) /\ exists ff_q_pfp_execution_aligned_productcoefficientscoefficientdiagonalentry. pfc_terms_code_execution_aligned_productcoefficientscoefficient = ff_q_pfp_execution_aligned_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_execution_aligned_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_execution_aligned_productcoefficientscoefficient) + (pfc_value_execution_aligned_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_execution_aligned_productcoefficientscoefficientdiagonalterm pfc_left_execution_aligned_productcoefficientscoefficientdiagonalterm pfc_right_execution_aligned_productcoefficientscoefficientdiagonalterm. (((pfc_index_execution_aligned_productcoefficientscoefficientdiagonal)+pfc_complement_execution_aligned_productcoefficientscoefficientdiagonalterm=(pfc_index_execution_aligned_productcoefficients)) /\ ((((((exists pfa_gap_execution_aligned_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_execution_aligned_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_execution_aligned_productcoefficientscoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_execution_aligned_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_execution_aligned_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_execution_aligned_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_execution_aligned_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_aligned_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_execution_aligned_productcoefficientscoefficientdiagonaltermleftoutside+(q)=(pfc_index_execution_aligned_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_execution_aligned_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_execution_aligned_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_execution_aligned_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_execution_aligned_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_execution_aligned_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_execution_aligned_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_execution_aligned_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_execution_aligned_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_execution_aligned_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_execution_aligned_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_execution_aligned_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_execution_aligned_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_execution_aligned_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_execution_aligned_productcoefficientscoefficientdiagonal)=pfc_left_execution_aligned_productcoefficientscoefficientdiagonalterm*pfc_right_execution_aligned_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_execution_aligned_productcoefficientscoefficientsum fs_v_pfc_execution_aligned_productcoefficientscoefficientsum. ((((exists fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_start. fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_start. fs_u_pfc_execution_aligned_productcoefficientscoefficientsum = fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_execution_aligned_productcoefficientscoefficient) = S ((S (S (pfc_index_execution_aligned_productcoefficients))) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_execution_aligned_productcoefficientscoefficientsum = fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_execution_aligned_productcoefficients))) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum) + (pfc_natural_sum_execution_aligned_productcoefficientscoefficient))) /\ forall fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps = S (pfc_index_execution_aligned_productcoefficients)) -> exists fs_a_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps fs_r_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps fs_s_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_aligned_productcoefficientscoefficient)) /\ exists fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_execution_aligned_productcoefficientscoefficient = fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_execution_aligned_productcoefficientscoefficient) + (fs_a_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_execution_aligned_productcoefficientscoefficientsum = fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum) + (fs_r_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_execution_aligned_productcoefficientscoefficientsum = fs_q_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_execution_aligned_productcoefficientscoefficientsum) + (fs_s_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps = fs_r_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps + fs_a_pfc_execution_aligned_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_execution_aligned_productcoefficientscoefficientresiduebound. pfa_gap_execution_aligned_productcoefficientscoefficientresiduebound + S (pfc_value_execution_aligned_productcoefficients) = (p)) /\ ((exists pfa_offset_left_execution_aligned_productcoefficientscoefficientresiduecongruence pfa_offset_right_execution_aligned_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_execution_aligned_productcoefficientscoefficient) + (p) * pfa_offset_left_execution_aligned_productcoefficientscoefficientresiduecongruence = (pfc_value_execution_aligned_productcoefficients) + (p) * pfa_offset_right_execution_aligned_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_execution_aligned_sum_left_bounded. (exists fom_gap_pfp_execution_aligned_sum_left_bounded_index_bound. fom_gap_pfp_execution_aligned_sum_left_bounded_index_bound + S (fom_index_pfp_execution_aligned_sum_left_bounded) = N) -> exists fom_value_pfp_execution_aligned_sum_left_bounded. ((((exists fom_beta_height_pfp_execution_aligned_sum_left_bounded_entry. fom_beta_height_pfp_execution_aligned_sum_left_bounded_entry + S (fom_value_pfp_execution_aligned_sum_left_bounded) = S ((S (fom_index_pfp_execution_aligned_sum_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_execution_aligned_sum_left_bounded_entry. pb = fom_beta_quotient_pfp_execution_aligned_sum_left_bounded_entry * S ((S (fom_index_pfp_execution_aligned_sum_left_bounded)) * pc) + (fom_value_pfp_execution_aligned_sum_left_bounded))) /\ (exists fom_gap_pfp_execution_aligned_sum_left_bounded_value_bound. fom_gap_pfp_execution_aligned_sum_left_bounded_value_bound + S (fom_value_pfp_execution_aligned_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_execution_aligned_sum_right_bounded. (exists fom_gap_pfp_execution_aligned_sum_right_bounded_index_bound. fom_gap_pfp_execution_aligned_sum_right_bounded_index_bound + S (fom_index_pfp_execution_aligned_sum_right_bounded) = R) -> exists fom_value_pfp_execution_aligned_sum_right_bounded. ((((exists fom_beta_height_pfp_execution_aligned_sum_right_bounded_entry. fom_beta_height_pfp_execution_aligned_sum_right_bounded_entry + S (fom_value_pfp_execution_aligned_sum_right_bounded) = S ((S (fom_index_pfp_execution_aligned_sum_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_execution_aligned_sum_right_bounded_entry. rb = fom_beta_quotient_pfp_execution_aligned_sum_right_bounded_entry * S ((S (fom_index_pfp_execution_aligned_sum_right_bounded)) * rc) + (fom_value_pfp_execution_aligned_sum_right_bounded))) /\ (exists fom_gap_pfp_execution_aligned_sum_right_bounded_value_bound. fom_gap_pfp_execution_aligned_sum_right_bounded_value_bound + S (fom_value_pfp_execution_aligned_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_execution_aligned_sum_result_bounded. (exists fom_gap_pfp_execution_aligned_sum_result_bounded_index_bound. fom_gap_pfp_execution_aligned_sum_result_bounded_index_bound + S (fom_index_pfp_execution_aligned_sum_result_bounded) = L) -> exists fom_value_pfp_execution_aligned_sum_result_bounded. ((((exists fom_beta_height_pfp_execution_aligned_sum_result_bounded_entry. fom_beta_height_pfp_execution_aligned_sum_result_bounded_entry + S (fom_value_pfp_execution_aligned_sum_result_bounded) = S ((S (fom_index_pfp_execution_aligned_sum_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_execution_aligned_sum_result_bounded_entry. ab = fom_beta_quotient_pfp_execution_aligned_sum_result_bounded_entry * S ((S (fom_index_pfp_execution_aligned_sum_result_bounded)) * ac) + (fom_value_pfp_execution_aligned_sum_result_bounded))) /\ (exists fom_gap_pfp_execution_aligned_sum_result_bounded_value_bound. fom_gap_pfp_execution_aligned_sum_result_bounded_value_bound + S (fom_value_pfp_execution_aligned_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_execution_aligned_sum pfaa_left_c_execution_aligned_sum pfaa_right_b_execution_aligned_sum pfaa_right_c_execution_aligned_sum pfaa_sum_b_execution_aligned_sum pfaa_sum_c_execution_aligned_sum pfaa_length_execution_aligned_sum. ((((forall pfrep_power_execution_aligned_sum_witness_common_left pfrep_left_execution_aligned_sum_witness_common_left pfrep_right_execution_aligned_sum_witness_common_left. ((exists pfrep_position_execution_aligned_sum_witness_common_leftfirst. ((pfrep_position_execution_aligned_sum_witness_common_leftfirst+S (pfrep_power_execution_aligned_sum_witness_common_left)=(N)) /\ ((((exists ff_h_pfp_execution_aligned_sum_witness_common_leftfirstentry. ff_h_pfp_execution_aligned_sum_witness_common_leftfirstentry + S (pfrep_left_execution_aligned_sum_witness_common_left) = S ((S (pfrep_position_execution_aligned_sum_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_execution_aligned_sum_witness_common_leftfirstentry. pb = ff_q_pfp_execution_aligned_sum_witness_common_leftfirstentry * S ((S (pfrep_position_execution_aligned_sum_witness_common_leftfirst)) * pc) + (pfrep_left_execution_aligned_sum_witness_common_left)))))) \/ (((exists pfrep_gap_execution_aligned_sum_witness_common_leftfirstoutside. pfrep_gap_execution_aligned_sum_witness_common_leftfirstoutside+(N)=(pfrep_power_execution_aligned_sum_witness_common_left)) /\ (((pfrep_left_execution_aligned_sum_witness_common_left)=0))))) -> ((exists pfrep_position_execution_aligned_sum_witness_common_leftsecond. ((pfrep_position_execution_aligned_sum_witness_common_leftsecond+S (pfrep_power_execution_aligned_sum_witness_common_left)=(pfaa_length_execution_aligned_sum)) /\ ((((exists ff_h_pfp_execution_aligned_sum_witness_common_leftsecondentry. ff_h_pfp_execution_aligned_sum_witness_common_leftsecondentry + S (pfrep_right_execution_aligned_sum_witness_common_left) = S ((S (pfrep_position_execution_aligned_sum_witness_common_leftsecond)) * pfaa_left_c_execution_aligned_sum)) /\ exists ff_q_pfp_execution_aligned_sum_witness_common_leftsecondentry. pfaa_left_b_execution_aligned_sum = ff_q_pfp_execution_aligned_sum_witness_common_leftsecondentry * S ((S (pfrep_position_execution_aligned_sum_witness_common_leftsecond)) * pfaa_left_c_execution_aligned_sum) + (pfrep_right_execution_aligned_sum_witness_common_left)))))) \/ (((exists pfrep_gap_execution_aligned_sum_witness_common_leftsecondoutside. pfrep_gap_execution_aligned_sum_witness_common_leftsecondoutside+(pfaa_length_execution_aligned_sum)=(pfrep_power_execution_aligned_sum_witness_common_left)) /\ (((pfrep_right_execution_aligned_sum_witness_common_left)=0))))) -> pfrep_left_execution_aligned_sum_witness_common_left=pfrep_right_execution_aligned_sum_witness_common_left) /\ ((forall pfrep_power_execution_aligned_sum_witness_common_right pfrep_left_execution_aligned_sum_witness_common_right pfrep_right_execution_aligned_sum_witness_common_right. ((exists pfrep_position_execution_aligned_sum_witness_common_rightfirst. ((pfrep_position_execution_aligned_sum_witness_common_rightfirst+S (pfrep_power_execution_aligned_sum_witness_common_right)=(R)) /\ ((((exists ff_h_pfp_execution_aligned_sum_witness_common_rightfirstentry. ff_h_pfp_execution_aligned_sum_witness_common_rightfirstentry + S (pfrep_left_execution_aligned_sum_witness_common_right) = S ((S (pfrep_position_execution_aligned_sum_witness_common_rightfirst)) * rc)) /\ exists ff_q_pfp_execution_aligned_sum_witness_common_rightfirstentry. rb = ff_q_pfp_execution_aligned_sum_witness_common_rightfirstentry * S ((S (pfrep_position_execution_aligned_sum_witness_common_rightfirst)) * rc) + (pfrep_left_execution_aligned_sum_witness_common_right)))))) \/ (((exists pfrep_gap_execution_aligned_sum_witness_common_rightfirstoutside. pfrep_gap_execution_aligned_sum_witness_common_rightfirstoutside+(R)=(pfrep_power_execution_aligned_sum_witness_common_right)) /\ (((pfrep_left_execution_aligned_sum_witness_common_right)=0))))) -> ((exists pfrep_position_execution_aligned_sum_witness_common_rightsecond. ((pfrep_position_execution_aligned_sum_witness_common_rightsecond+S (pfrep_power_execution_aligned_sum_witness_common_right)=(pfaa_length_execution_aligned_sum)) /\ ((((exists ff_h_pfp_execution_aligned_sum_witness_common_rightsecondentry. ff_h_pfp_execution_aligned_sum_witness_common_rightsecondentry + S (pfrep_right_execution_aligned_sum_witness_common_right) = S ((S (pfrep_position_execution_aligned_sum_witness_common_rightsecond)) * pfaa_right_c_execution_aligned_sum)) /\ exists ff_q_pfp_execution_aligned_sum_witness_common_rightsecondentry. pfaa_right_b_execution_aligned_sum = ff_q_pfp_execution_aligned_sum_witness_common_rightsecondentry * S ((S (pfrep_position_execution_aligned_sum_witness_common_rightsecond)) * pfaa_right_c_execution_aligned_sum) + (pfrep_right_execution_aligned_sum_witness_common_right)))))) \/ (((exists pfrep_gap_execution_aligned_sum_witness_common_rightsecondoutside. pfrep_gap_execution_aligned_sum_witness_common_rightsecondoutside+(pfaa_length_execution_aligned_sum)=(pfrep_power_execution_aligned_sum_witness_common_right)) /\ (((pfrep_right_execution_aligned_sum_witness_common_right)=0))))) -> pfrep_left_execution_aligned_sum_witness_common_right=pfrep_right_execution_aligned_sum_witness_common_right)))) /\ (((forall pfp_index_execution_aligned_sum_witness_operation. (exists pfa_gap_execution_aligned_sum_witness_operationindex. pfa_gap_execution_aligned_sum_witness_operationindex + S (pfp_index_execution_aligned_sum_witness_operation) = (pfaa_length_execution_aligned_sum)) -> exists pfp_left_execution_aligned_sum_witness_operation pfp_right_execution_aligned_sum_witness_operation pfp_value_execution_aligned_sum_witness_operation. ((((exists ff_h_pfp_execution_aligned_sum_witness_operationleft. ff_h_pfp_execution_aligned_sum_witness_operationleft + S (pfp_left_execution_aligned_sum_witness_operation) = S ((S (pfp_index_execution_aligned_sum_witness_operation)) * pfaa_left_c_execution_aligned_sum)) /\ exists ff_q_pfp_execution_aligned_sum_witness_operationleft. pfaa_left_b_execution_aligned_sum = ff_q_pfp_execution_aligned_sum_witness_operationleft * S ((S (pfp_index_execution_aligned_sum_witness_operation)) * pfaa_left_c_execution_aligned_sum) + (pfp_left_execution_aligned_sum_witness_operation))) /\ (((((exists ff_h_pfp_execution_aligned_sum_witness_operationright. ff_h_pfp_execution_aligned_sum_witness_operationright + S (pfp_right_execution_aligned_sum_witness_operation) = S ((S (pfp_index_execution_aligned_sum_witness_operation)) * pfaa_right_c_execution_aligned_sum)) /\ exists ff_q_pfp_execution_aligned_sum_witness_operationright. pfaa_right_b_execution_aligned_sum = ff_q_pfp_execution_aligned_sum_witness_operationright * S ((S (pfp_index_execution_aligned_sum_witness_operation)) * pfaa_right_c_execution_aligned_sum) + (pfp_right_execution_aligned_sum_witness_operation))) /\ (((((exists ff_h_pfp_execution_aligned_sum_witness_operationtarget. ff_h_pfp_execution_aligned_sum_witness_operationtarget + S (pfp_value_execution_aligned_sum_witness_operation) = S ((S (pfp_index_execution_aligned_sum_witness_operation)) * pfaa_sum_c_execution_aligned_sum)) /\ exists ff_q_pfp_execution_aligned_sum_witness_operationtarget. pfaa_sum_b_execution_aligned_sum = ff_q_pfp_execution_aligned_sum_witness_operationtarget * S ((S (pfp_index_execution_aligned_sum_witness_operation)) * pfaa_sum_c_execution_aligned_sum) + (pfp_value_execution_aligned_sum_witness_operation))) /\ ((((exists pfa_gap_execution_aligned_sum_witness_operationoperationleft. pfa_gap_execution_aligned_sum_witness_operationoperationleft + S (pfp_left_execution_aligned_sum_witness_operation) = (p)) /\ (((exists pfa_gap_execution_aligned_sum_witness_operationoperationright. pfa_gap_execution_aligned_sum_witness_operationoperationright + S (pfp_right_execution_aligned_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_execution_aligned_sum_witness_operationoperationresultbound. pfa_gap_execution_aligned_sum_witness_operationoperationresultbound + S (pfp_value_execution_aligned_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_execution_aligned_sum_witness_operationoperationresultcongruence pfa_offset_right_execution_aligned_sum_witness_operationoperationresultcongruence. ((pfp_left_execution_aligned_sum_witness_operation) + (pfp_right_execution_aligned_sum_witness_operation)) + (p) * pfa_offset_left_execution_aligned_sum_witness_operationoperationresultcongruence = (pfp_value_execution_aligned_sum_witness_operation) + (p) * pfa_offset_right_execution_aligned_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_execution_aligned_sum_witness_output pfrep_left_execution_aligned_sum_witness_output pfrep_right_execution_aligned_sum_witness_output. ((exists pfrep_position_execution_aligned_sum_witness_outputfirst. ((pfrep_position_execution_aligned_sum_witness_outputfirst+S (pfrep_power_execution_aligned_sum_witness_output)=(pfaa_length_execution_aligned_sum)) /\ ((((exists ff_h_pfp_execution_aligned_sum_witness_outputfirstentry. ff_h_pfp_execution_aligned_sum_witness_outputfirstentry + S (pfrep_left_execution_aligned_sum_witness_output) = S ((S (pfrep_position_execution_aligned_sum_witness_outputfirst)) * pfaa_sum_c_execution_aligned_sum)) /\ exists ff_q_pfp_execution_aligned_sum_witness_outputfirstentry. pfaa_sum_b_execution_aligned_sum = ff_q_pfp_execution_aligned_sum_witness_outputfirstentry * S ((S (pfrep_position_execution_aligned_sum_witness_outputfirst)) * pfaa_sum_c_execution_aligned_sum) + (pfrep_left_execution_aligned_sum_witness_output)))))) \/ (((exists pfrep_gap_execution_aligned_sum_witness_outputfirstoutside. pfrep_gap_execution_aligned_sum_witness_outputfirstoutside+(pfaa_length_execution_aligned_sum)=(pfrep_power_execution_aligned_sum_witness_output)) /\ (((pfrep_left_execution_aligned_sum_witness_output)=0))))) -> ((exists pfrep_position_execution_aligned_sum_witness_outputsecond. ((pfrep_position_execution_aligned_sum_witness_outputsecond+S (pfrep_power_execution_aligned_sum_witness_output)=(L)) /\ ((((exists ff_h_pfp_execution_aligned_sum_witness_outputsecondentry. ff_h_pfp_execution_aligned_sum_witness_outputsecondentry + S (pfrep_right_execution_aligned_sum_witness_output) = S ((S (pfrep_position_execution_aligned_sum_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_execution_aligned_sum_witness_outputsecondentry. ab = ff_q_pfp_execution_aligned_sum_witness_outputsecondentry * S ((S (pfrep_position_execution_aligned_sum_witness_outputsecond)) * ac) + (pfrep_right_execution_aligned_sum_witness_output)))))) \/ (((exists pfrep_gap_execution_aligned_sum_witness_outputsecondoutside. pfrep_gap_execution_aligned_sum_witness_outputsecondoutside+(L)=(pfrep_power_execution_aligned_sum_witness_output)) /\ (((pfrep_right_execution_aligned_sum_witness_output)=0))))) -> pfrep_left_execution_aligned_sum_witness_output=pfrep_right_execution_aligned_sum_witness_output))))))))))))))))