prime_field_polynomial_convolution_right_scale_equal

Exact expanded first-order arithmetic statement

forall p k ab ac L bb bc M sb sc cb cc N db dc K eb ec. (((exists pfa_gap_scalar_comparison_inputscalar. pfa_gap_scalar_comparison_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_comparison_input. (exists pfa_gap_scalar_comparison_inputindex. pfa_gap_scalar_comparison_inputindex + S (pfp_index_scalar_comparison_input) = (M)) -> exists pfp_source_scalar_comparison_input pfp_value_scalar_comparison_input. ((((exists ff_h_pfp_scalar_comparison_inputsource. ff_h_pfp_scalar_comparison_inputsource + S (pfp_source_scalar_comparison_input) = S ((S (pfp_index_scalar_comparison_input)) * bc)) /\ exists ff_q_pfp_scalar_comparison_inputsource. bb = ff_q_pfp_scalar_comparison_inputsource * S ((S (pfp_index_scalar_comparison_input)) * bc) + (pfp_source_scalar_comparison_input))) /\ (((((exists ff_h_pfp_scalar_comparison_inputtarget. ff_h_pfp_scalar_comparison_inputtarget + S (pfp_value_scalar_comparison_input) = S ((S (pfp_index_scalar_comparison_input)) * sc)) /\ exists ff_q_pfp_scalar_comparison_inputtarget. sb = ff_q_pfp_scalar_comparison_inputtarget * S ((S (pfp_index_scalar_comparison_input)) * sc) + (pfp_value_scalar_comparison_input))) /\ ((((exists pfa_gap_scalar_comparison_inputoperationleft. pfa_gap_scalar_comparison_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_comparison_inputoperationright. pfa_gap_scalar_comparison_inputoperationright + S (pfp_source_scalar_comparison_input) = (p)) /\ ((((exists pfa_gap_scalar_comparison_inputoperationresultbound. pfa_gap_scalar_comparison_inputoperationresultbound + S (pfp_value_scalar_comparison_input) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_inputoperationresultcongruence pfa_offset_right_scalar_comparison_inputoperationresultcongruence. ((k) * (pfp_source_scalar_comparison_input)) + (p) * pfa_offset_left_scalar_comparison_inputoperationresultcongruence = (pfp_value_scalar_comparison_input) + (p) * pfa_offset_right_scalar_comparison_inputoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_scalar_comparison_oldleft. (exists fom_gap_pfp_scalar_comparison_oldleft_index_bound. fom_gap_pfp_scalar_comparison_oldleft_index_bound + S (fom_index_pfp_scalar_comparison_oldleft) = L) -> exists fom_value_pfp_scalar_comparison_oldleft. ((((exists fom_beta_height_pfp_scalar_comparison_oldleft_entry. fom_beta_height_pfp_scalar_comparison_oldleft_entry + S (fom_value_pfp_scalar_comparison_oldleft) = S ((S (fom_index_pfp_scalar_comparison_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_comparison_oldleft_entry. ab = fom_beta_quotient_pfp_scalar_comparison_oldleft_entry * S ((S (fom_index_pfp_scalar_comparison_oldleft)) * ac) + (fom_value_pfp_scalar_comparison_oldleft))) /\ (exists fom_gap_pfp_scalar_comparison_oldleft_value_bound. fom_gap_pfp_scalar_comparison_oldleft_value_bound + S (fom_value_pfp_scalar_comparison_oldleft) = p))) /\ (((forall fom_index_pfp_scalar_comparison_oldright. (exists fom_gap_pfp_scalar_comparison_oldright_index_bound. fom_gap_pfp_scalar_comparison_oldright_index_bound + S (fom_index_pfp_scalar_comparison_oldright) = M) -> exists fom_value_pfp_scalar_comparison_oldright. ((((exists fom_beta_height_pfp_scalar_comparison_oldright_entry. fom_beta_height_pfp_scalar_comparison_oldright_entry + S (fom_value_pfp_scalar_comparison_oldright) = S ((S (fom_index_pfp_scalar_comparison_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_comparison_oldright_entry. bb = fom_beta_quotient_pfp_scalar_comparison_oldright_entry * S ((S (fom_index_pfp_scalar_comparison_oldright)) * bc) + (fom_value_pfp_scalar_comparison_oldright))) /\ (exists fom_gap_pfp_scalar_comparison_oldright_value_bound. fom_gap_pfp_scalar_comparison_oldright_value_bound + S (fom_value_pfp_scalar_comparison_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_comparison_oldcoefficients. (exists pfa_gap_scalar_comparison_oldcoefficientsbound. pfa_gap_scalar_comparison_oldcoefficientsbound + S (pfc_index_scalar_comparison_oldcoefficients) = (N)) -> exists pfc_value_scalar_comparison_oldcoefficients. ((((exists ff_h_pfp_scalar_comparison_oldcoefficientsentry. ff_h_pfp_scalar_comparison_oldcoefficientsentry + S (pfc_value_scalar_comparison_oldcoefficients) = S ((S (pfc_index_scalar_comparison_oldcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientsentry. cb = ff_q_pfp_scalar_comparison_oldcoefficientsentry * S ((S (pfc_index_scalar_comparison_oldcoefficients)) * cc) + (pfc_value_scalar_comparison_oldcoefficients))) /\ ((exists pfc_terms_code_scalar_comparison_oldcoefficientscoefficient pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient. ((forall pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonalbound. pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_comparison_oldcoefficients))) -> exists pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_comparison_oldcoefficientscoefficient = ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient) + (pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)+pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm=(pfc_index_scalar_comparison_oldcoefficients)) /\ ((((((exists pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal)=pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm*pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient) = S ((S (S (pfc_index_scalar_comparison_oldcoefficients))) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_comparison_oldcoefficients))) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_comparison_oldcoefficients)) -> exists fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_comparison_oldcoefficientscoefficient = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient) + (fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_comparison_oldcoefficientscoefficientresiduebound. pfa_gap_scalar_comparison_oldcoefficientscoefficientresiduebound + S (pfc_value_scalar_comparison_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_oldcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_comparison_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient) + (p) * pfa_offset_left_scalar_comparison_oldcoefficientscoefficientresiduecongruence = (pfc_value_scalar_comparison_oldcoefficients) + (p) * pfa_offset_right_scalar_comparison_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_scalar_comparison_scaledleft. (exists fom_gap_pfp_scalar_comparison_scaledleft_index_bound. fom_gap_pfp_scalar_comparison_scaledleft_index_bound + S (fom_index_pfp_scalar_comparison_scaledleft) = L) -> exists fom_value_pfp_scalar_comparison_scaledleft. ((((exists fom_beta_height_pfp_scalar_comparison_scaledleft_entry. fom_beta_height_pfp_scalar_comparison_scaledleft_entry + S (fom_value_pfp_scalar_comparison_scaledleft) = S ((S (fom_index_pfp_scalar_comparison_scaledleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_comparison_scaledleft_entry. ab = fom_beta_quotient_pfp_scalar_comparison_scaledleft_entry * S ((S (fom_index_pfp_scalar_comparison_scaledleft)) * ac) + (fom_value_pfp_scalar_comparison_scaledleft))) /\ (exists fom_gap_pfp_scalar_comparison_scaledleft_value_bound. fom_gap_pfp_scalar_comparison_scaledleft_value_bound + S (fom_value_pfp_scalar_comparison_scaledleft) = p))) /\ (((forall fom_index_pfp_scalar_comparison_scaledright. (exists fom_gap_pfp_scalar_comparison_scaledright_index_bound. fom_gap_pfp_scalar_comparison_scaledright_index_bound + S (fom_index_pfp_scalar_comparison_scaledright) = M) -> exists fom_value_pfp_scalar_comparison_scaledright. ((((exists fom_beta_height_pfp_scalar_comparison_scaledright_entry. fom_beta_height_pfp_scalar_comparison_scaledright_entry + S (fom_value_pfp_scalar_comparison_scaledright) = S ((S (fom_index_pfp_scalar_comparison_scaledright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_comparison_scaledright_entry. sb = fom_beta_quotient_pfp_scalar_comparison_scaledright_entry * S ((S (fom_index_pfp_scalar_comparison_scaledright)) * sc) + (fom_value_pfp_scalar_comparison_scaledright))) /\ (exists fom_gap_pfp_scalar_comparison_scaledright_value_bound. fom_gap_pfp_scalar_comparison_scaledright_value_bound + S (fom_value_pfp_scalar_comparison_scaledright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (K)))))))) /\ ((forall pfc_index_scalar_comparison_scaledcoefficients. (exists pfa_gap_scalar_comparison_scaledcoefficientsbound. pfa_gap_scalar_comparison_scaledcoefficientsbound + S (pfc_index_scalar_comparison_scaledcoefficients) = (K)) -> exists pfc_value_scalar_comparison_scaledcoefficients. ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientsentry. ff_h_pfp_scalar_comparison_scaledcoefficientsentry + S (pfc_value_scalar_comparison_scaledcoefficients) = S ((S (pfc_index_scalar_comparison_scaledcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientsentry. db = ff_q_pfp_scalar_comparison_scaledcoefficientsentry * S ((S (pfc_index_scalar_comparison_scaledcoefficients)) * dc) + (pfc_value_scalar_comparison_scaledcoefficients))) /\ ((exists pfc_terms_code_scalar_comparison_scaledcoefficientscoefficient pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient. ((forall pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonalbound. pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_comparison_scaledcoefficients))) -> exists pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_comparison_scaledcoefficientscoefficient = ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient) + (pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)+pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm=(pfc_index_scalar_comparison_scaledcoefficients)) /\ ((((((exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal)=pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm*pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient) = S ((S (S (pfc_index_scalar_comparison_scaledcoefficients))) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_comparison_scaledcoefficients))) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_comparison_scaledcoefficients)) -> exists fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_comparison_scaledcoefficientscoefficient = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient) + (fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientresiduebound. pfa_gap_scalar_comparison_scaledcoefficientscoefficientresiduebound + S (pfc_value_scalar_comparison_scaledcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_scaledcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_comparison_scaledcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient) + (p) * pfa_offset_left_scalar_comparison_scaledcoefficientscoefficientresiduecongruence = (pfc_value_scalar_comparison_scaledcoefficients) + (p) * pfa_offset_right_scalar_comparison_scaledcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((exists pfa_gap_scalar_comparison_outputscalar. pfa_gap_scalar_comparison_outputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_comparison_output. (exists pfa_gap_scalar_comparison_outputindex. pfa_gap_scalar_comparison_outputindex + S (pfp_index_scalar_comparison_output) = (N)) -> exists pfp_source_scalar_comparison_output pfp_value_scalar_comparison_output. ((((exists ff_h_pfp_scalar_comparison_outputsource. ff_h_pfp_scalar_comparison_outputsource + S (pfp_source_scalar_comparison_output) = S ((S (pfp_index_scalar_comparison_output)) * cc)) /\ exists ff_q_pfp_scalar_comparison_outputsource. cb = ff_q_pfp_scalar_comparison_outputsource * S ((S (pfp_index_scalar_comparison_output)) * cc) + (pfp_source_scalar_comparison_output))) /\ (((((exists ff_h_pfp_scalar_comparison_outputtarget. ff_h_pfp_scalar_comparison_outputtarget + S (pfp_value_scalar_comparison_output) = S ((S (pfp_index_scalar_comparison_output)) * ec)) /\ exists ff_q_pfp_scalar_comparison_outputtarget. eb = ff_q_pfp_scalar_comparison_outputtarget * S ((S (pfp_index_scalar_comparison_output)) * ec) + (pfp_value_scalar_comparison_output))) /\ ((((exists pfa_gap_scalar_comparison_outputoperationleft. pfa_gap_scalar_comparison_outputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_comparison_outputoperationright. pfa_gap_scalar_comparison_outputoperationright + S (pfp_source_scalar_comparison_output) = (p)) /\ ((((exists pfa_gap_scalar_comparison_outputoperationresultbound. pfa_gap_scalar_comparison_outputoperationresultbound + S (pfp_value_scalar_comparison_output) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_outputoperationresultcongruence pfa_offset_right_scalar_comparison_outputoperationresultcongruence. ((k) * (pfp_source_scalar_comparison_output)) + (p) * pfa_offset_left_scalar_comparison_outputoperationresultcongruence = (pfp_value_scalar_comparison_output) + (p) * pfa_offset_right_scalar_comparison_outputoperationresultcongruence))))))))))))))))) -> (((K=N) /\ ((forall mdr_i_pfp_scalar_comparison_result mdr_a_pfp_scalar_comparison_result. (exists mdr_gap_pfp_scalar_comparison_resultb. mdr_gap_pfp_scalar_comparison_resultb + S (mdr_i_pfp_scalar_comparison_result) = (N)) -> (((exists ff_h_mdr_pfp_scalar_comparison_resulto. ff_h_mdr_pfp_scalar_comparison_resulto + S (mdr_a_pfp_scalar_comparison_result) = S ((S (mdr_i_pfp_scalar_comparison_result)) * dc)) /\ exists ff_q_mdr_pfp_scalar_comparison_resulto. db = ff_q_mdr_pfp_scalar_comparison_resulto * S ((S (mdr_i_pfp_scalar_comparison_result)) * dc) + (mdr_a_pfp_scalar_comparison_result))) -> (((exists ff_h_mdr_pfp_scalar_comparison_resultn. ff_h_mdr_pfp_scalar_comparison_resultn + S (mdr_a_pfp_scalar_comparison_result) = S ((S (mdr_i_pfp_scalar_comparison_result)) * ec)) /\ exists ff_q_mdr_pfp_scalar_comparison_resultn. eb = ff_q_mdr_pfp_scalar_comparison_resultn * S ((S (mdr_i_pfp_scalar_comparison_result)) * ec) + (mdr_a_pfp_scalar_comparison_result)))))))