prime_field_polynomial_division_quotient_data_functional

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d b k q qb qc B K Q QB QC. (((((exists ff_h_pfp_data_unique_firsthead. ff_h_pfp_data_unique_firsthead + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_data_unique_firsthead. bb = ff_q_pfp_data_unique_firsthead * S ((S (0)) * bc) + (b))) /\ (((((~((b) = 0)) /\ ((((exists pfa_gap_data_unique_firstinversemultiplicationleft. pfa_gap_data_unique_firstinversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_data_unique_firstinversemultiplicationright. pfa_gap_data_unique_firstinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_data_unique_firstinversemultiplicationresultbound. pfa_gap_data_unique_firstinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_data_unique_firstinversemultiplicationresultcongruence pfa_offset_right_data_unique_firstinversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_data_unique_firstinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_data_unique_firstinversemultiplicationresultcongruence)))))))))))) /\ (((((((q)=0) /\ ((exists pfc_gap_data_unique_firstlengthshort. pfc_gap_data_unique_firstlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((forall pfd_index_data_unique_firstexecution. (exists pfa_gap_data_unique_firstexecutionbound. pfa_gap_data_unique_firstexecutionbound + S (pfd_index_data_unique_firstexecution) = (q)) -> exists pfd_value_data_unique_firstexecution. ((((exists ff_h_pfp_data_unique_firstexecutionentry. ff_h_pfp_data_unique_firstexecutionentry + S (pfd_value_data_unique_firstexecution) = S ((S (pfd_index_data_unique_firstexecution)) * qc)) /\ exists ff_q_pfp_data_unique_firstexecutionentry. qb = ff_q_pfp_data_unique_firstexecutionentry * S ((S (pfd_index_data_unique_firstexecution)) * qc) + (pfd_value_data_unique_firstexecution))) /\ ((exists pfd_input_data_unique_firstexecutionstep pfd_previous_data_unique_firstexecutionstep pfd_difference_data_unique_firstexecutionstep. ((((exists ff_h_pfp_data_unique_firstexecutionstepinput. ff_h_pfp_data_unique_firstexecutionstepinput + S (pfd_input_data_unique_firstexecutionstep) = S ((S (pfd_index_data_unique_firstexecution)) * ac)) /\ exists ff_q_pfp_data_unique_firstexecutionstepinput. ab = ff_q_pfp_data_unique_firstexecutionstepinput * S ((S (pfd_index_data_unique_firstexecution)) * ac) + (pfd_input_data_unique_firstexecutionstep))) /\ (((exists pfc_terms_code_data_unique_firstexecutionstepprevious pfc_terms_scale_data_unique_firstexecutionstepprevious pfc_natural_sum_data_unique_firstexecutionstepprevious. ((forall pfc_index_data_unique_firstexecutionsteppreviousdiagonal. (exists pfa_gap_data_unique_firstexecutionsteppreviousdiagonalbound. pfa_gap_data_unique_firstexecutionsteppreviousdiagonalbound + S (pfc_index_data_unique_firstexecutionsteppreviousdiagonal) = (S (pfd_index_data_unique_firstexecution))) -> exists pfc_value_data_unique_firstexecutionsteppreviousdiagonal. ((((exists ff_h_pfp_data_unique_firstexecutionsteppreviousdiagonalentry. ff_h_pfp_data_unique_firstexecutionsteppreviousdiagonalentry + S (pfc_value_data_unique_firstexecutionsteppreviousdiagonal) = S ((S (pfc_index_data_unique_firstexecutionsteppreviousdiagonal)) * pfc_terms_scale_data_unique_firstexecutionstepprevious)) /\ exists ff_q_pfp_data_unique_firstexecutionsteppreviousdiagonalentry. pfc_terms_code_data_unique_firstexecutionstepprevious = ff_q_pfp_data_unique_firstexecutionsteppreviousdiagonalentry * S ((S (pfc_index_data_unique_firstexecutionsteppreviousdiagonal)) * pfc_terms_scale_data_unique_firstexecutionstepprevious) + (pfc_value_data_unique_firstexecutionsteppreviousdiagonal))) /\ ((exists pfc_complement_data_unique_firstexecutionsteppreviousdiagonalterm pfc_left_data_unique_firstexecutionsteppreviousdiagonalterm pfc_right_data_unique_firstexecutionsteppreviousdiagonalterm. (((pfc_index_data_unique_firstexecutionsteppreviousdiagonal)+pfc_complement_data_unique_firstexecutionsteppreviousdiagonalterm=(pfd_index_data_unique_firstexecution)) /\ ((((((exists pfa_gap_data_unique_firstexecutionsteppreviousdiagonaltermleftinside. pfa_gap_data_unique_firstexecutionsteppreviousdiagonaltermleftinside + S (pfc_index_data_unique_firstexecutionsteppreviousdiagonal) = (pfd_index_data_unique_firstexecution)) /\ ((((exists ff_h_pfp_data_unique_firstexecutionsteppreviousdiagonaltermleftentry. ff_h_pfp_data_unique_firstexecutionsteppreviousdiagonaltermleftentry + S (pfc_left_data_unique_firstexecutionsteppreviousdiagonalterm) = S ((S (pfc_index_data_unique_firstexecutionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_data_unique_firstexecutionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_data_unique_firstexecutionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_data_unique_firstexecutionsteppreviousdiagonal)) * qc) + (pfc_left_data_unique_firstexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_data_unique_firstexecutionsteppreviousdiagonaltermleftoutside. pfc_gap_data_unique_firstexecutionsteppreviousdiagonaltermleftoutside+(pfd_index_data_unique_firstexecution)=(pfc_index_data_unique_firstexecutionsteppreviousdiagonal)) /\ (((pfc_left_data_unique_firstexecutionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_data_unique_firstexecutionsteppreviousdiagonaltermrightinside. pfa_gap_data_unique_firstexecutionsteppreviousdiagonaltermrightinside + S (pfc_complement_data_unique_firstexecutionsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_data_unique_firstexecutionsteppreviousdiagonaltermrightentry. ff_h_pfp_data_unique_firstexecutionsteppreviousdiagonaltermrightentry + S (pfc_right_data_unique_firstexecutionsteppreviousdiagonalterm) = S ((S (pfc_complement_data_unique_firstexecutionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_data_unique_firstexecutionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_data_unique_firstexecutionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_data_unique_firstexecutionsteppreviousdiagonalterm)) * bc) + (pfc_right_data_unique_firstexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_data_unique_firstexecutionsteppreviousdiagonaltermrightoutside. pfc_gap_data_unique_firstexecutionsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_data_unique_firstexecutionsteppreviousdiagonalterm)) /\ (((pfc_right_data_unique_firstexecutionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_data_unique_firstexecutionsteppreviousdiagonal)=pfc_left_data_unique_firstexecutionsteppreviousdiagonalterm*pfc_right_data_unique_firstexecutionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_data_unique_firstexecutionstepprevioussum fs_v_pfc_data_unique_firstexecutionstepprevioussum. ((((exists fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_start. fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_data_unique_firstexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_start. fs_u_pfc_data_unique_firstexecutionstepprevioussum = fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_data_unique_firstexecutionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_terminal. fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_terminal + S (pfc_natural_sum_data_unique_firstexecutionstepprevious) = S ((S (S (pfd_index_data_unique_firstexecution))) * fs_v_pfc_data_unique_firstexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_terminal. fs_u_pfc_data_unique_firstexecutionstepprevioussum = fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_terminal * S ((S (S (pfd_index_data_unique_firstexecution))) * fs_v_pfc_data_unique_firstexecutionstepprevioussum) + (pfc_natural_sum_data_unique_firstexecutionstepprevious))) /\ forall fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps. (exists fs_lt_pfc_data_unique_firstexecutionstepprevioussum_body_steps_bound. fs_lt_pfc_data_unique_firstexecutionstepprevioussum_body_steps_bound + S fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps = S (pfd_index_data_unique_firstexecution)) -> exists fs_a_pfc_data_unique_firstexecutionstepprevioussum_body_steps fs_r_pfc_data_unique_firstexecutionstepprevioussum_body_steps fs_s_pfc_data_unique_firstexecutionstepprevioussum_body_steps. ((((exists fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_steps_summand. fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_steps_summand + S (fs_a_pfc_data_unique_firstexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps)) * pfc_terms_scale_data_unique_firstexecutionstepprevious)) /\ exists fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_steps_summand. pfc_terms_code_data_unique_firstexecutionstepprevious = fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps)) * pfc_terms_scale_data_unique_firstexecutionstepprevious) + (fs_a_pfc_data_unique_firstexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_steps_partial. fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_steps_partial + S (fs_r_pfc_data_unique_firstexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_firstexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_steps_partial. fs_u_pfc_data_unique_firstexecutionstepprevioussum = fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_firstexecutionstepprevioussum) + (fs_r_pfc_data_unique_firstexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_steps_successor. fs_h_pfc_data_unique_firstexecutionstepprevioussum_body_steps_successor + S (fs_s_pfc_data_unique_firstexecutionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_firstexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_steps_successor. fs_u_pfc_data_unique_firstexecutionstepprevioussum = fs_q_pfc_data_unique_firstexecutionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_data_unique_firstexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_firstexecutionstepprevioussum) + (fs_s_pfc_data_unique_firstexecutionstepprevioussum_body_steps))) /\ fs_s_pfc_data_unique_firstexecutionstepprevioussum_body_steps = fs_r_pfc_data_unique_firstexecutionstepprevioussum_body_steps + fs_a_pfc_data_unique_firstexecutionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_data_unique_firstexecutionsteppreviousresiduebound. pfa_gap_data_unique_firstexecutionsteppreviousresiduebound + S (pfd_previous_data_unique_firstexecutionstep) = (p)) /\ ((exists pfa_offset_left_data_unique_firstexecutionsteppreviousresiduecongruence pfa_offset_right_data_unique_firstexecutionsteppreviousresiduecongruence. (pfc_natural_sum_data_unique_firstexecutionstepprevious) + (p) * pfa_offset_left_data_unique_firstexecutionsteppreviousresiduecongruence = (pfd_previous_data_unique_firstexecutionstep) + (p) * pfa_offset_right_data_unique_firstexecutionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_data_unique_firstexecutionstepsubtractleft. pfa_gap_data_unique_firstexecutionstepsubtractleft + S (pfd_previous_data_unique_firstexecutionstep) = (p)) /\ (((exists pfa_gap_data_unique_firstexecutionstepsubtractright. pfa_gap_data_unique_firstexecutionstepsubtractright + S (pfd_difference_data_unique_firstexecutionstep) = (p)) /\ ((((exists pfa_gap_data_unique_firstexecutionstepsubtractresultbound. pfa_gap_data_unique_firstexecutionstepsubtractresultbound + S (pfd_input_data_unique_firstexecutionstep) = (p)) /\ ((exists pfa_offset_left_data_unique_firstexecutionstepsubtractresultcongruence pfa_offset_right_data_unique_firstexecutionstepsubtractresultcongruence. ((pfd_previous_data_unique_firstexecutionstep) + (pfd_difference_data_unique_firstexecutionstep)) + (p) * pfa_offset_left_data_unique_firstexecutionstepsubtractresultcongruence = (pfd_input_data_unique_firstexecutionstep) + (p) * pfa_offset_right_data_unique_firstexecutionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_data_unique_firstexecutionstepmultiplyleft. pfa_gap_data_unique_firstexecutionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_data_unique_firstexecutionstepmultiplyright. pfa_gap_data_unique_firstexecutionstepmultiplyright + S (pfd_difference_data_unique_firstexecutionstep) = (p)) /\ ((((exists pfa_gap_data_unique_firstexecutionstepmultiplyresultbound. pfa_gap_data_unique_firstexecutionstepmultiplyresultbound + S (pfd_value_data_unique_firstexecution) = (p)) /\ ((exists pfa_offset_left_data_unique_firstexecutionstepmultiplyresultcongruence pfa_offset_right_data_unique_firstexecutionstepmultiplyresultcongruence. ((k) * (pfd_difference_data_unique_firstexecutionstep)) + (p) * pfa_offset_left_data_unique_firstexecutionstepmultiplyresultcongruence = (pfd_value_data_unique_firstexecution) + (p) * pfa_offset_right_data_unique_firstexecutionstepmultiplyresultcongruence)))))))))))))))))))))))))) -> (((((exists ff_h_pfp_data_unique_secondhead. ff_h_pfp_data_unique_secondhead + S (B) = S ((S (0)) * bc)) /\ exists ff_q_pfp_data_unique_secondhead. bb = ff_q_pfp_data_unique_secondhead * S ((S (0)) * bc) + (B))) /\ (((((~((B) = 0)) /\ ((((exists pfa_gap_data_unique_secondinversemultiplicationleft. pfa_gap_data_unique_secondinversemultiplicationleft + S (B) = (p)) /\ (((exists pfa_gap_data_unique_secondinversemultiplicationright. pfa_gap_data_unique_secondinversemultiplicationright + S (K) = (p)) /\ ((((exists pfa_gap_data_unique_secondinversemultiplicationresultbound. pfa_gap_data_unique_secondinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_data_unique_secondinversemultiplicationresultcongruence pfa_offset_right_data_unique_secondinversemultiplicationresultcongruence. ((B) * (K)) + (p) * pfa_offset_left_data_unique_secondinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_data_unique_secondinversemultiplicationresultcongruence)))))))))))) /\ (((((((Q)=0) /\ ((exists pfc_gap_data_unique_secondlengthshort. pfc_gap_data_unique_secondlengthshort+(L)=(d))))) \/ (((~((Q)=0)) /\ (((Q)+(d)=(L)))))) /\ ((forall pfd_index_data_unique_secondexecution. (exists pfa_gap_data_unique_secondexecutionbound. pfa_gap_data_unique_secondexecutionbound + S (pfd_index_data_unique_secondexecution) = (Q)) -> exists pfd_value_data_unique_secondexecution. ((((exists ff_h_pfp_data_unique_secondexecutionentry. ff_h_pfp_data_unique_secondexecutionentry + S (pfd_value_data_unique_secondexecution) = S ((S (pfd_index_data_unique_secondexecution)) * QC)) /\ exists ff_q_pfp_data_unique_secondexecutionentry. QB = ff_q_pfp_data_unique_secondexecutionentry * S ((S (pfd_index_data_unique_secondexecution)) * QC) + (pfd_value_data_unique_secondexecution))) /\ ((exists pfd_input_data_unique_secondexecutionstep pfd_previous_data_unique_secondexecutionstep pfd_difference_data_unique_secondexecutionstep. ((((exists ff_h_pfp_data_unique_secondexecutionstepinput. ff_h_pfp_data_unique_secondexecutionstepinput + S (pfd_input_data_unique_secondexecutionstep) = S ((S (pfd_index_data_unique_secondexecution)) * ac)) /\ exists ff_q_pfp_data_unique_secondexecutionstepinput. ab = ff_q_pfp_data_unique_secondexecutionstepinput * S ((S (pfd_index_data_unique_secondexecution)) * ac) + (pfd_input_data_unique_secondexecutionstep))) /\ (((exists pfc_terms_code_data_unique_secondexecutionstepprevious pfc_terms_scale_data_unique_secondexecutionstepprevious pfc_natural_sum_data_unique_secondexecutionstepprevious. ((forall pfc_index_data_unique_secondexecutionsteppreviousdiagonal. (exists pfa_gap_data_unique_secondexecutionsteppreviousdiagonalbound. pfa_gap_data_unique_secondexecutionsteppreviousdiagonalbound + S (pfc_index_data_unique_secondexecutionsteppreviousdiagonal) = (S (pfd_index_data_unique_secondexecution))) -> exists pfc_value_data_unique_secondexecutionsteppreviousdiagonal. ((((exists ff_h_pfp_data_unique_secondexecutionsteppreviousdiagonalentry. ff_h_pfp_data_unique_secondexecutionsteppreviousdiagonalentry + S (pfc_value_data_unique_secondexecutionsteppreviousdiagonal) = S ((S (pfc_index_data_unique_secondexecutionsteppreviousdiagonal)) * pfc_terms_scale_data_unique_secondexecutionstepprevious)) /\ exists ff_q_pfp_data_unique_secondexecutionsteppreviousdiagonalentry. pfc_terms_code_data_unique_secondexecutionstepprevious = ff_q_pfp_data_unique_secondexecutionsteppreviousdiagonalentry * S ((S (pfc_index_data_unique_secondexecutionsteppreviousdiagonal)) * pfc_terms_scale_data_unique_secondexecutionstepprevious) + (pfc_value_data_unique_secondexecutionsteppreviousdiagonal))) /\ ((exists pfc_complement_data_unique_secondexecutionsteppreviousdiagonalterm pfc_left_data_unique_secondexecutionsteppreviousdiagonalterm pfc_right_data_unique_secondexecutionsteppreviousdiagonalterm. (((pfc_index_data_unique_secondexecutionsteppreviousdiagonal)+pfc_complement_data_unique_secondexecutionsteppreviousdiagonalterm=(pfd_index_data_unique_secondexecution)) /\ ((((((exists pfa_gap_data_unique_secondexecutionsteppreviousdiagonaltermleftinside. pfa_gap_data_unique_secondexecutionsteppreviousdiagonaltermleftinside + S (pfc_index_data_unique_secondexecutionsteppreviousdiagonal) = (pfd_index_data_unique_secondexecution)) /\ ((((exists ff_h_pfp_data_unique_secondexecutionsteppreviousdiagonaltermleftentry. ff_h_pfp_data_unique_secondexecutionsteppreviousdiagonaltermleftentry + S (pfc_left_data_unique_secondexecutionsteppreviousdiagonalterm) = S ((S (pfc_index_data_unique_secondexecutionsteppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_data_unique_secondexecutionsteppreviousdiagonaltermleftentry. QB = ff_q_pfp_data_unique_secondexecutionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_data_unique_secondexecutionsteppreviousdiagonal)) * QC) + (pfc_left_data_unique_secondexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_data_unique_secondexecutionsteppreviousdiagonaltermleftoutside. pfc_gap_data_unique_secondexecutionsteppreviousdiagonaltermleftoutside+(pfd_index_data_unique_secondexecution)=(pfc_index_data_unique_secondexecutionsteppreviousdiagonal)) /\ (((pfc_left_data_unique_secondexecutionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_data_unique_secondexecutionsteppreviousdiagonaltermrightinside. pfa_gap_data_unique_secondexecutionsteppreviousdiagonaltermrightinside + S (pfc_complement_data_unique_secondexecutionsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_data_unique_secondexecutionsteppreviousdiagonaltermrightentry. ff_h_pfp_data_unique_secondexecutionsteppreviousdiagonaltermrightentry + S (pfc_right_data_unique_secondexecutionsteppreviousdiagonalterm) = S ((S (pfc_complement_data_unique_secondexecutionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_data_unique_secondexecutionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_data_unique_secondexecutionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_data_unique_secondexecutionsteppreviousdiagonalterm)) * bc) + (pfc_right_data_unique_secondexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_data_unique_secondexecutionsteppreviousdiagonaltermrightoutside. pfc_gap_data_unique_secondexecutionsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_data_unique_secondexecutionsteppreviousdiagonalterm)) /\ (((pfc_right_data_unique_secondexecutionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_data_unique_secondexecutionsteppreviousdiagonal)=pfc_left_data_unique_secondexecutionsteppreviousdiagonalterm*pfc_right_data_unique_secondexecutionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_data_unique_secondexecutionstepprevioussum fs_v_pfc_data_unique_secondexecutionstepprevioussum. ((((exists fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_start. fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_data_unique_secondexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_start. fs_u_pfc_data_unique_secondexecutionstepprevioussum = fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_data_unique_secondexecutionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_terminal. fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_terminal + S (pfc_natural_sum_data_unique_secondexecutionstepprevious) = S ((S (S (pfd_index_data_unique_secondexecution))) * fs_v_pfc_data_unique_secondexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_terminal. fs_u_pfc_data_unique_secondexecutionstepprevioussum = fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_terminal * S ((S (S (pfd_index_data_unique_secondexecution))) * fs_v_pfc_data_unique_secondexecutionstepprevioussum) + (pfc_natural_sum_data_unique_secondexecutionstepprevious))) /\ forall fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps. (exists fs_lt_pfc_data_unique_secondexecutionstepprevioussum_body_steps_bound. fs_lt_pfc_data_unique_secondexecutionstepprevioussum_body_steps_bound + S fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps = S (pfd_index_data_unique_secondexecution)) -> exists fs_a_pfc_data_unique_secondexecutionstepprevioussum_body_steps fs_r_pfc_data_unique_secondexecutionstepprevioussum_body_steps fs_s_pfc_data_unique_secondexecutionstepprevioussum_body_steps. ((((exists fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_steps_summand. fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_steps_summand + S (fs_a_pfc_data_unique_secondexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps)) * pfc_terms_scale_data_unique_secondexecutionstepprevious)) /\ exists fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_steps_summand. pfc_terms_code_data_unique_secondexecutionstepprevious = fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps)) * pfc_terms_scale_data_unique_secondexecutionstepprevious) + (fs_a_pfc_data_unique_secondexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_steps_partial. fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_steps_partial + S (fs_r_pfc_data_unique_secondexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_secondexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_steps_partial. fs_u_pfc_data_unique_secondexecutionstepprevioussum = fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_secondexecutionstepprevioussum) + (fs_r_pfc_data_unique_secondexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_steps_successor. fs_h_pfc_data_unique_secondexecutionstepprevioussum_body_steps_successor + S (fs_s_pfc_data_unique_secondexecutionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_secondexecutionstepprevioussum)) /\ exists fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_steps_successor. fs_u_pfc_data_unique_secondexecutionstepprevioussum = fs_q_pfc_data_unique_secondexecutionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_data_unique_secondexecutionstepprevioussum_body_steps)) * fs_v_pfc_data_unique_secondexecutionstepprevioussum) + (fs_s_pfc_data_unique_secondexecutionstepprevioussum_body_steps))) /\ fs_s_pfc_data_unique_secondexecutionstepprevioussum_body_steps = fs_r_pfc_data_unique_secondexecutionstepprevioussum_body_steps + fs_a_pfc_data_unique_secondexecutionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_data_unique_secondexecutionsteppreviousresiduebound. pfa_gap_data_unique_secondexecutionsteppreviousresiduebound + S (pfd_previous_data_unique_secondexecutionstep) = (p)) /\ ((exists pfa_offset_left_data_unique_secondexecutionsteppreviousresiduecongruence pfa_offset_right_data_unique_secondexecutionsteppreviousresiduecongruence. (pfc_natural_sum_data_unique_secondexecutionstepprevious) + (p) * pfa_offset_left_data_unique_secondexecutionsteppreviousresiduecongruence = (pfd_previous_data_unique_secondexecutionstep) + (p) * pfa_offset_right_data_unique_secondexecutionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_data_unique_secondexecutionstepsubtractleft. pfa_gap_data_unique_secondexecutionstepsubtractleft + S (pfd_previous_data_unique_secondexecutionstep) = (p)) /\ (((exists pfa_gap_data_unique_secondexecutionstepsubtractright. pfa_gap_data_unique_secondexecutionstepsubtractright + S (pfd_difference_data_unique_secondexecutionstep) = (p)) /\ ((((exists pfa_gap_data_unique_secondexecutionstepsubtractresultbound. pfa_gap_data_unique_secondexecutionstepsubtractresultbound + S (pfd_input_data_unique_secondexecutionstep) = (p)) /\ ((exists pfa_offset_left_data_unique_secondexecutionstepsubtractresultcongruence pfa_offset_right_data_unique_secondexecutionstepsubtractresultcongruence. ((pfd_previous_data_unique_secondexecutionstep) + (pfd_difference_data_unique_secondexecutionstep)) + (p) * pfa_offset_left_data_unique_secondexecutionstepsubtractresultcongruence = (pfd_input_data_unique_secondexecutionstep) + (p) * pfa_offset_right_data_unique_secondexecutionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_data_unique_secondexecutionstepmultiplyleft. pfa_gap_data_unique_secondexecutionstepmultiplyleft + S (K) = (p)) /\ (((exists pfa_gap_data_unique_secondexecutionstepmultiplyright. pfa_gap_data_unique_secondexecutionstepmultiplyright + S (pfd_difference_data_unique_secondexecutionstep) = (p)) /\ ((((exists pfa_gap_data_unique_secondexecutionstepmultiplyresultbound. pfa_gap_data_unique_secondexecutionstepmultiplyresultbound + S (pfd_value_data_unique_secondexecution) = (p)) /\ ((exists pfa_offset_left_data_unique_secondexecutionstepmultiplyresultcongruence pfa_offset_right_data_unique_secondexecutionstepmultiplyresultcongruence. ((K) * (pfd_difference_data_unique_secondexecutionstep)) + (p) * pfa_offset_left_data_unique_secondexecutionstepmultiplyresultcongruence = (pfd_value_data_unique_secondexecution) + (p) * pfa_offset_right_data_unique_secondexecutionstepmultiplyresultcongruence)))))))))))))))))))))))))) -> (((b=B) /\ (((k=K) /\ (((q=Q) /\ ((forall mdr_i_pfp_data_unique_quotient mdr_a_pfp_data_unique_quotient. (exists mdr_gap_pfp_data_unique_quotientb. mdr_gap_pfp_data_unique_quotientb + S (mdr_i_pfp_data_unique_quotient) = (q)) -> (((exists ff_h_mdr_pfp_data_unique_quotiento. ff_h_mdr_pfp_data_unique_quotiento + S (mdr_a_pfp_data_unique_quotient) = S ((S (mdr_i_pfp_data_unique_quotient)) * qc)) /\ exists ff_q_mdr_pfp_data_unique_quotiento. qb = ff_q_mdr_pfp_data_unique_quotiento * S ((S (mdr_i_pfp_data_unique_quotient)) * qc) + (mdr_a_pfp_data_unique_quotient))) -> (((exists ff_h_mdr_pfp_data_unique_quotientn. ff_h_mdr_pfp_data_unique_quotientn + S (mdr_a_pfp_data_unique_quotient) = S ((S (mdr_i_pfp_data_unique_quotient)) * QC)) /\ exists ff_q_mdr_pfp_data_unique_quotientn. QB = ff_q_mdr_pfp_data_unique_quotientn * S ((S (mdr_i_pfp_data_unique_quotient)) * QC) + (mdr_a_pfp_data_unique_quotient)))))))))))