PX0054

prime_field_polynomial_quotient_prefix_functional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Finite induction proves coefficientwise uniqueness of the actual quotient recursion, with no claim about beta code identity or unused entries.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc M qb qc QB QC N. (forall pfd_index_prefix_unique_first. (exists pfa_gap_prefix_unique_firstbound. pfa_gap_prefix_unique_firstbound + S (pfd_index_prefix_unique_first) = (N)) -> exists pfd_value_prefix_unique_first. ((((exists ff_h_pfp_prefix_unique_firstentry. ff_h_pfp_prefix_unique_firstentry + S (pfd_value_prefix_unique_first) = S ((S (pfd_index_prefix_unique_first)) * qc)) /\ exists ff_q_pfp_prefix_unique_firstentry. qb = ff_q_pfp_prefix_unique_firstentry * S ((S (pfd_index_prefix_unique_first)) * qc) + (pfd_value_prefix_unique_first))) /\ ((exists pfd_input_prefix_unique_firststep pfd_previous_prefix_unique_firststep pfd_difference_prefix_unique_firststep. ((((exists ff_h_pfp_prefix_unique_firststepinput. ff_h_pfp_prefix_unique_firststepinput + S (pfd_input_prefix_unique_firststep) = S ((S (pfd_index_prefix_unique_first)) * ac)) /\ exists ff_q_pfp_prefix_unique_firststepinput. ab = ff_q_pfp_prefix_unique_firststepinput * S ((S (pfd_index_prefix_unique_first)) * ac) + (pfd_input_prefix_unique_firststep))) /\ (((exists pfc_terms_code_prefix_unique_firststepprevious pfc_terms_scale_prefix_unique_firststepprevious pfc_natural_sum_prefix_unique_firststepprevious. ((forall pfc_index_prefix_unique_firststeppreviousdiagonal. (exists pfa_gap_prefix_unique_firststeppreviousdiagonalbound. pfa_gap_prefix_unique_firststeppreviousdiagonalbound + S (pfc_index_prefix_unique_firststeppreviousdiagonal) = (S (pfd_index_prefix_unique_first))) -> exists pfc_value_prefix_unique_firststeppreviousdiagonal. ((((exists ff_h_pfp_prefix_unique_firststeppreviousdiagonalentry. ff_h_pfp_prefix_unique_firststeppreviousdiagonalentry + S (pfc_value_prefix_unique_firststeppreviousdiagonal) = S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * pfc_terms_scale_prefix_unique_firststepprevious)) /\ exists ff_q_pfp_prefix_unique_firststeppreviousdiagonalentry. pfc_terms_code_prefix_unique_firststepprevious = ff_q_pfp_prefix_unique_firststeppreviousdiagonalentry * S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * pfc_terms_scale_prefix_unique_firststepprevious) + (pfc_value_prefix_unique_firststeppreviousdiagonal))) /\ ((exists pfc_complement_prefix_unique_firststeppreviousdiagonalterm pfc_left_prefix_unique_firststeppreviousdiagonalterm pfc_right_prefix_unique_firststeppreviousdiagonalterm. (((pfc_index_prefix_unique_firststeppreviousdiagonal)+pfc_complement_prefix_unique_firststeppreviousdiagonalterm=(pfd_index_prefix_unique_first)) /\ ((((((exists pfa_gap_prefix_unique_firststeppreviousdiagonaltermleftinside. pfa_gap_prefix_unique_firststeppreviousdiagonaltermleftinside + S (pfc_index_prefix_unique_firststeppreviousdiagonal) = (pfd_index_prefix_unique_first)) /\ ((((exists ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry. ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry + S (pfc_left_prefix_unique_firststeppreviousdiagonalterm) = S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry. qb = ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry * S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * qc) + (pfc_left_prefix_unique_firststeppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_firststeppreviousdiagonaltermleftoutside. pfc_gap_prefix_unique_firststeppreviousdiagonaltermleftoutside+(pfd_index_prefix_unique_first)=(pfc_index_prefix_unique_firststeppreviousdiagonal)) /\ (((pfc_left_prefix_unique_firststeppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_unique_firststeppreviousdiagonaltermrightinside. pfa_gap_prefix_unique_firststeppreviousdiagonaltermrightinside + S (pfc_complement_prefix_unique_firststeppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry. ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry + S (pfc_right_prefix_unique_firststeppreviousdiagonalterm) = S ((S (pfc_complement_prefix_unique_firststeppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry. bb = ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry * S ((S (pfc_complement_prefix_unique_firststeppreviousdiagonalterm)) * bc) + (pfc_right_prefix_unique_firststeppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_firststeppreviousdiagonaltermrightoutside. pfc_gap_prefix_unique_firststeppreviousdiagonaltermrightoutside+(M)=(pfc_complement_prefix_unique_firststeppreviousdiagonalterm)) /\ (((pfc_right_prefix_unique_firststeppreviousdiagonalterm)=0))))) /\ (((pfc_value_prefix_unique_firststeppreviousdiagonal)=pfc_left_prefix_unique_firststeppreviousdiagonalterm*pfc_right_prefix_unique_firststeppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_unique_firststepprevioussum fs_v_pfc_prefix_unique_firststepprevioussum. ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_start. fs_h_pfc_prefix_unique_firststepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_start. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_start * S ((S (0)) * fs_v_pfc_prefix_unique_firststepprevioussum) + (0))) /\ ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_terminal. fs_h_pfc_prefix_unique_firststepprevioussum_body_terminal + S (pfc_natural_sum_prefix_unique_firststepprevious) = S ((S (S (pfd_index_prefix_unique_first))) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_terminal. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_terminal * S ((S (S (pfd_index_prefix_unique_first))) * fs_v_pfc_prefix_unique_firststepprevioussum) + (pfc_natural_sum_prefix_unique_firststepprevious))) /\ forall fs_i_pfc_prefix_unique_firststepprevioussum_body_steps. (exists fs_lt_pfc_prefix_unique_firststepprevioussum_body_steps_bound. fs_lt_pfc_prefix_unique_firststepprevioussum_body_steps_bound + S fs_i_pfc_prefix_unique_firststepprevioussum_body_steps = S (pfd_index_prefix_unique_first)) -> exists fs_a_pfc_prefix_unique_firststepprevioussum_body_steps fs_r_pfc_prefix_unique_firststepprevioussum_body_steps fs_s_pfc_prefix_unique_firststepprevioussum_body_steps. ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_summand. fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_summand + S (fs_a_pfc_prefix_unique_firststepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_firststepprevious)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_summand. pfc_terms_code_prefix_unique_firststepprevious = fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_summand * S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_firststepprevious) + (fs_a_pfc_prefix_unique_firststepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_partial. fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_partial + S (fs_r_pfc_prefix_unique_firststepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_partial. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_partial * S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum) + (fs_r_pfc_prefix_unique_firststepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_successor. fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_successor + S (fs_s_pfc_prefix_unique_firststepprevioussum_body_steps) = S ((S (S fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_successor. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum) + (fs_s_pfc_prefix_unique_firststepprevioussum_body_steps))) /\ fs_s_pfc_prefix_unique_firststepprevioussum_body_steps = fs_r_pfc_prefix_unique_firststepprevioussum_body_steps + fs_a_pfc_prefix_unique_firststepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_prefix_unique_firststeppreviousresiduebound. pfa_gap_prefix_unique_firststeppreviousresiduebound + S (pfd_previous_prefix_unique_firststep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_firststeppreviousresiduecongruence pfa_offset_right_prefix_unique_firststeppreviousresiduecongruence. (pfc_natural_sum_prefix_unique_firststepprevious) + (p) * pfa_offset_left_prefix_unique_firststeppreviousresiduecongruence = (pfd_previous_prefix_unique_firststep) + (p) * pfa_offset_right_prefix_unique_firststeppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_prefix_unique_firststepsubtractleft. pfa_gap_prefix_unique_firststepsubtractleft + S (pfd_previous_prefix_unique_firststep) = (p)) /\ (((exists pfa_gap_prefix_unique_firststepsubtractright. pfa_gap_prefix_unique_firststepsubtractright + S (pfd_difference_prefix_unique_firststep) = (p)) /\ ((((exists pfa_gap_prefix_unique_firststepsubtractresultbound. pfa_gap_prefix_unique_firststepsubtractresultbound + S (pfd_input_prefix_unique_firststep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_firststepsubtractresultcongruence pfa_offset_right_prefix_unique_firststepsubtractresultcongruence. ((pfd_previous_prefix_unique_firststep) + (pfd_difference_prefix_unique_firststep)) + (p) * pfa_offset_left_prefix_unique_firststepsubtractresultcongruence = (pfd_input_prefix_unique_firststep) + (p) * pfa_offset_right_prefix_unique_firststepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_prefix_unique_firststepmultiplyleft. pfa_gap_prefix_unique_firststepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_prefix_unique_firststepmultiplyright. pfa_gap_prefix_unique_firststepmultiplyright + S (pfd_difference_prefix_unique_firststep) = (p)) /\ ((((exists pfa_gap_prefix_unique_firststepmultiplyresultbound. pfa_gap_prefix_unique_firststepmultiplyresultbound + S (pfd_value_prefix_unique_first) = (p)) /\ ((exists pfa_offset_left_prefix_unique_firststepmultiplyresultcongruence pfa_offset_right_prefix_unique_firststepmultiplyresultcongruence. ((k) * (pfd_difference_prefix_unique_firststep)) + (p) * pfa_offset_left_prefix_unique_firststepmultiplyresultcongruence = (pfd_value_prefix_unique_first) + (p) * pfa_offset_right_prefix_unique_firststepmultiplyresultcongruence))))))))))))))))))) -> (forall pfd_index_prefix_unique_second. (exists pfa_gap_prefix_unique_secondbound. pfa_gap_prefix_unique_secondbound + S (pfd_index_prefix_unique_second) = (N)) -> exists pfd_value_prefix_unique_second. ((((exists ff_h_pfp_prefix_unique_secondentry. ff_h_pfp_prefix_unique_secondentry + S (pfd_value_prefix_unique_second) = S ((S (pfd_index_prefix_unique_second)) * QC)) /\ exists ff_q_pfp_prefix_unique_secondentry. QB = ff_q_pfp_prefix_unique_secondentry * S ((S (pfd_index_prefix_unique_second)) * QC) + (pfd_value_prefix_unique_second))) /\ ((exists pfd_input_prefix_unique_secondstep pfd_previous_prefix_unique_secondstep pfd_difference_prefix_unique_secondstep. ((((exists ff_h_pfp_prefix_unique_secondstepinput. ff_h_pfp_prefix_unique_secondstepinput + S (pfd_input_prefix_unique_secondstep) = S ((S (pfd_index_prefix_unique_second)) * ac)) /\ exists ff_q_pfp_prefix_unique_secondstepinput. ab = ff_q_pfp_prefix_unique_secondstepinput * S ((S (pfd_index_prefix_unique_second)) * ac) + (pfd_input_prefix_unique_secondstep))) /\ (((exists pfc_terms_code_prefix_unique_secondstepprevious pfc_terms_scale_prefix_unique_secondstepprevious pfc_natural_sum_prefix_unique_secondstepprevious. ((forall pfc_index_prefix_unique_secondsteppreviousdiagonal. (exists pfa_gap_prefix_unique_secondsteppreviousdiagonalbound. pfa_gap_prefix_unique_secondsteppreviousdiagonalbound + S (pfc_index_prefix_unique_secondsteppreviousdiagonal) = (S (pfd_index_prefix_unique_second))) -> exists pfc_value_prefix_unique_secondsteppreviousdiagonal. ((((exists ff_h_pfp_prefix_unique_secondsteppreviousdiagonalentry. ff_h_pfp_prefix_unique_secondsteppreviousdiagonalentry + S (pfc_value_prefix_unique_secondsteppreviousdiagonal) = S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * pfc_terms_scale_prefix_unique_secondstepprevious)) /\ exists ff_q_pfp_prefix_unique_secondsteppreviousdiagonalentry. pfc_terms_code_prefix_unique_secondstepprevious = ff_q_pfp_prefix_unique_secondsteppreviousdiagonalentry * S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * pfc_terms_scale_prefix_unique_secondstepprevious) + (pfc_value_prefix_unique_secondsteppreviousdiagonal))) /\ ((exists pfc_complement_prefix_unique_secondsteppreviousdiagonalterm pfc_left_prefix_unique_secondsteppreviousdiagonalterm pfc_right_prefix_unique_secondsteppreviousdiagonalterm. (((pfc_index_prefix_unique_secondsteppreviousdiagonal)+pfc_complement_prefix_unique_secondsteppreviousdiagonalterm=(pfd_index_prefix_unique_second)) /\ ((((((exists pfa_gap_prefix_unique_secondsteppreviousdiagonaltermleftinside. pfa_gap_prefix_unique_secondsteppreviousdiagonaltermleftinside + S (pfc_index_prefix_unique_secondsteppreviousdiagonal) = (pfd_index_prefix_unique_second)) /\ ((((exists ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry. ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry + S (pfc_left_prefix_unique_secondsteppreviousdiagonalterm) = S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry. QB = ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry * S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * QC) + (pfc_left_prefix_unique_secondsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_secondsteppreviousdiagonaltermleftoutside. pfc_gap_prefix_unique_secondsteppreviousdiagonaltermleftoutside+(pfd_index_prefix_unique_second)=(pfc_index_prefix_unique_secondsteppreviousdiagonal)) /\ (((pfc_left_prefix_unique_secondsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_unique_secondsteppreviousdiagonaltermrightinside. pfa_gap_prefix_unique_secondsteppreviousdiagonaltermrightinside + S (pfc_complement_prefix_unique_secondsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry. ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry + S (pfc_right_prefix_unique_secondsteppreviousdiagonalterm) = S ((S (pfc_complement_prefix_unique_secondsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_prefix_unique_secondsteppreviousdiagonalterm)) * bc) + (pfc_right_prefix_unique_secondsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_secondsteppreviousdiagonaltermrightoutside. pfc_gap_prefix_unique_secondsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_prefix_unique_secondsteppreviousdiagonalterm)) /\ (((pfc_right_prefix_unique_secondsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_prefix_unique_secondsteppreviousdiagonal)=pfc_left_prefix_unique_secondsteppreviousdiagonalterm*pfc_right_prefix_unique_secondsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_unique_secondstepprevioussum fs_v_pfc_prefix_unique_secondstepprevioussum. ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_start. fs_h_pfc_prefix_unique_secondstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_start. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_terminal. fs_h_pfc_prefix_unique_secondstepprevioussum_body_terminal + S (pfc_natural_sum_prefix_unique_secondstepprevious) = S ((S (S (pfd_index_prefix_unique_second))) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_terminal. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_terminal * S ((S (S (pfd_index_prefix_unique_second))) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (pfc_natural_sum_prefix_unique_secondstepprevious))) /\ forall fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps. (exists fs_lt_pfc_prefix_unique_secondstepprevioussum_body_steps_bound. fs_lt_pfc_prefix_unique_secondstepprevioussum_body_steps_bound + S fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps = S (pfd_index_prefix_unique_second)) -> exists fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps. ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_summand. fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_summand + S (fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_secondstepprevious)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_summand. pfc_terms_code_prefix_unique_secondstepprevious = fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_secondstepprevious) + (fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_partial. fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_partial + S (fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_partial. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_successor. fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_successor + S (fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps) = S ((S (S fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_successor. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps))) /\ fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps = fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps + fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_prefix_unique_secondsteppreviousresiduebound. pfa_gap_prefix_unique_secondsteppreviousresiduebound + S (pfd_previous_prefix_unique_secondstep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_secondsteppreviousresiduecongruence pfa_offset_right_prefix_unique_secondsteppreviousresiduecongruence. (pfc_natural_sum_prefix_unique_secondstepprevious) + (p) * pfa_offset_left_prefix_unique_secondsteppreviousresiduecongruence = (pfd_previous_prefix_unique_secondstep) + (p) * pfa_offset_right_prefix_unique_secondsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_prefix_unique_secondstepsubtractleft. pfa_gap_prefix_unique_secondstepsubtractleft + S (pfd_previous_prefix_unique_secondstep) = (p)) /\ (((exists pfa_gap_prefix_unique_secondstepsubtractright. pfa_gap_prefix_unique_secondstepsubtractright + S (pfd_difference_prefix_unique_secondstep) = (p)) /\ ((((exists pfa_gap_prefix_unique_secondstepsubtractresultbound. pfa_gap_prefix_unique_secondstepsubtractresultbound + S (pfd_input_prefix_unique_secondstep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_secondstepsubtractresultcongruence pfa_offset_right_prefix_unique_secondstepsubtractresultcongruence. ((pfd_previous_prefix_unique_secondstep) + (pfd_difference_prefix_unique_secondstep)) + (p) * pfa_offset_left_prefix_unique_secondstepsubtractresultcongruence = (pfd_input_prefix_unique_secondstep) + (p) * pfa_offset_right_prefix_unique_secondstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_prefix_unique_secondstepmultiplyleft. pfa_gap_prefix_unique_secondstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_prefix_unique_secondstepmultiplyright. pfa_gap_prefix_unique_secondstepmultiplyright + S (pfd_difference_prefix_unique_secondstep) = (p)) /\ ((((exists pfa_gap_prefix_unique_secondstepmultiplyresultbound. pfa_gap_prefix_unique_secondstepmultiplyresultbound + S (pfd_value_prefix_unique_second) = (p)) /\ ((exists pfa_offset_left_prefix_unique_secondstepmultiplyresultcongruence pfa_offset_right_prefix_unique_secondstepmultiplyresultcongruence. ((k) * (pfd_difference_prefix_unique_secondstep)) + (p) * pfa_offset_left_prefix_unique_secondstepmultiplyresultcongruence = (pfd_value_prefix_unique_second) + (p) * pfa_offset_right_prefix_unique_secondstepmultiplyresultcongruence))))))))))))))))))) -> (forall mdr_i_pfp_prefix_unique_result mdr_a_pfp_prefix_unique_result. (exists mdr_gap_pfp_prefix_unique_resultb. mdr_gap_pfp_prefix_unique_resultb + S (mdr_i_pfp_prefix_unique_result) = (N)) -> (((exists ff_h_mdr_pfp_prefix_unique_resulto. ff_h_mdr_pfp_prefix_unique_resulto + S (mdr_a_pfp_prefix_unique_result) = S ((S (mdr_i_pfp_prefix_unique_result)) * qc)) /\ exists ff_q_mdr_pfp_prefix_unique_resulto. qb = ff_q_mdr_pfp_prefix_unique_resulto * S ((S (mdr_i_pfp_prefix_unique_result)) * qc) + (mdr_a_pfp_prefix_unique_result))) -> (((exists ff_h_mdr_pfp_prefix_unique_resultn. ff_h_mdr_pfp_prefix_unique_resultn + S (mdr_a_pfp_prefix_unique_result) = S ((S (mdr_i_pfp_prefix_unique_result)) * QC)) /\ exists ff_q_mdr_pfp_prefix_unique_resultn. QB = ff_q_mdr_pfp_prefix_unique_resultn * S ((S (mdr_i_pfp_prefix_unique_result)) * QC) + (mdr_a_pfp_prefix_unique_result))))

Constructive proof overview

Generated structural guide

Finite induction proves coefficientwise uniqueness of the actual quotient recursion, with no claim about beta code identity or unused entries.

The unchanged tactic script uses 8 declared prerequisites and contains 130 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

lt_not_le Alpha theorem; checked-use authorized zero_le Alpha theorem; checked-use authorized PX002A prime_field_polynomial_quotient_prefix_restrict le_succ Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized PX0053 prime_field_polynomial_quotient_step_prefix_functional PX002B prime_field_polynomial_quotient_prefix_entry

Direct dependents

PX0057 prime_field_polynomial_division_quotient_data_functional

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

130 script commands · 22 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
prime field polynomial quotient prefix restrictprime field polynomial quotient step prefix functionalprime field polynomial quotient prefix entry

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro qb
  9. L9
    intro qc
  10. L10
    intro QB
02Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro QC
  2. L12
    intro N
03Induction on NL13–19

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L13
    induction N
  2. L14
    intro hfirst
  3. L15
    intro hsecond
  4. L16
    intro i
  5. L17
    intro a
  6. L18
    intro hindex
  7. L19
    intro hvalue
04Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    exfalso
05Use earlier factsL21–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    specialize lt_not_le (i)
  2. L22
    specialize lt_not_le (0)
  3. L23
    apply lt_not_le
  4. L24
    exact hindex
  5. L25
    specialize zero_le (i)
  6. L26
    apply zero_le
06Fix variables and assumptionsL27–28

Work with arbitrary variables or the premises of the current implication.

  1. L27
    intro hfirst
  2. L28
    intro hsecond
07Establish hequalL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L29
    have hequal : BetaPrefixEqual(qb,qc,QB,QC,N)Definitions: BetaPrefixEqual
  2. L30
    apply IH
  3. L31
    specialize prime_field_polynomial_quotient_prefix_restrict (p)
  4. L32
    specialize prime_field_polynomial_quotient_prefix_restrict (k)
  5. L33
    specialize prime_field_polynomial_quotient_prefix_restrict (ab)
  6. L34
    specialize prime_field_polynomial_quotient_prefix_restrict (ac)
  7. L35
    specialize prime_field_polynomial_quotient_prefix_restrict (bb)
  8. L36
    specialize prime_field_polynomial_quotient_prefix_restrict (bc)
  9. L37
    specialize prime_field_polynomial_quotient_prefix_restrict (M)
  10. L38
    specialize prime_field_polynomial_quotient_prefix_restrict (qb)
08Use earlier factsL39–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    specialize prime_field_polynomial_quotient_prefix_restrict (qc)
  2. L40
    specialize prime_field_polynomial_quotient_prefix_restrict (S N)
  3. L41
    specialize prime_field_polynomial_quotient_prefix_restrict (N)
  4. L42
    apply prime_field_polynomial_quotient_prefix_restrict
  5. L43
    specialize le_succ (N)
  6. L44
    specialize le_succ (N)
  7. L45
    apply le_succ
  8. L46
    specialize le_refl (N)
  9. L47
    apply le_refl
  10. L48
    exact hfirst
09Use earlier factsL49–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize prime_field_polynomial_quotient_prefix_restrict (p)
  2. L50
    specialize prime_field_polynomial_quotient_prefix_restrict (k)
  3. L51
    specialize prime_field_polynomial_quotient_prefix_restrict (ab)
  4. L52
    specialize prime_field_polynomial_quotient_prefix_restrict (ac)
  5. L53
    specialize prime_field_polynomial_quotient_prefix_restrict (bb)
  6. L54
    specialize prime_field_polynomial_quotient_prefix_restrict (bc)
  7. L55
    specialize prime_field_polynomial_quotient_prefix_restrict (M)
  8. L56
    specialize prime_field_polynomial_quotient_prefix_restrict (QB)
  9. L57
    specialize prime_field_polynomial_quotient_prefix_restrict (QC)
  10. L58
    specialize prime_field_polynomial_quotient_prefix_restrict (S N)
10Use earlier factsL59–66

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    specialize prime_field_polynomial_quotient_prefix_restrict (N)
  2. L60
    apply prime_field_polynomial_quotient_prefix_restrict
  3. L61
    specialize le_succ (N)
  4. L62
    specialize le_succ (N)
  5. L63
    apply le_succ
  6. L64
    specialize le_refl (N)
  7. L65
    apply le_refl
  8. L66
    exact hsecond
11Fix variables and assumptionsL67–70

Work with arbitrary variables or the premises of the current implication.

  1. L67
    intro i
  2. L68
    intro a
  3. L69
    intro hindex
  4. L70
    intro hvalue
12Establish hcaseL71–75

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L71
    have hcase : i=N \/ (exists pfa_gap_prefix_unique_earlier. pfa_gap_prefix_unique_earlier + S (i) = (N))
  2. L72
    specialize finite_lt_succ_eq_or_lt (N)
  3. L73
    specialize finite_lt_succ_eq_or_lt (i)
  4. L74
    apply finite_lt_succ_eq_or_lt
  5. L75
    exact hindex
13Separate the logical casesL76–76

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    cases hcase
14Calculate and transport equalitiesL77–80

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L77
    rewrite hcase_left at hvalue
  2. L78
    rewrite hcase_left at hvalue
  3. L79
    rewrite hcase_left
  4. L80
    rewrite hcase_left
15Establish hchosenL81–85

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsecond.

  1. L81
    have hchosen : ∃ r. BetaAt(QB,QC,N,r) ∧ FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,QB,QC,N,r)Definitions: FpPolynomialQuotientStepBetaAt
  2. L82
    specialize hsecond (N)
  3. L83
    apply hsecond
  4. L84
    specialize le_refl (S N)
  5. L85
    apply le_refl
16Separate the logical casesL86–87

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L86
    cases hchosen
  2. L87
    cases hchosen_witness
17Establish hlastL88–97

Establish this local claim before using it. It is not an additional assumption.

  1. L88
    have hlast : a=x
  2. L89
    specialize prime_field_polynomial_quotient_step_prefix_functional (p)
  3. L90
    specialize prime_field_polynomial_quotient_step_prefix_functional (k)
  4. L91
    specialize prime_field_polynomial_quotient_step_prefix_functional (ab)
  5. L92
    specialize prime_field_polynomial_quotient_step_prefix_functional (ac)
  6. L93
    specialize prime_field_polynomial_quotient_step_prefix_functional (bb)
  7. L94
    specialize prime_field_polynomial_quotient_step_prefix_functional (bc)
  8. L95
    specialize prime_field_polynomial_quotient_step_prefix_functional (M)
  9. L96
    specialize prime_field_polynomial_quotient_step_prefix_functional (qb)
  10. L97
    specialize prime_field_polynomial_quotient_step_prefix_functional (qc)
18Use earlier factsL98–107

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L98
    specialize prime_field_polynomial_quotient_step_prefix_functional (QB)
  2. L99
    specialize prime_field_polynomial_quotient_step_prefix_functional (QC)
  3. L100
    specialize prime_field_polynomial_quotient_step_prefix_functional (N)
  4. L101
    specialize prime_field_polynomial_quotient_step_prefix_functional (a)
  5. L102
    specialize prime_field_polynomial_quotient_step_prefix_functional (x)
  6. L103
    apply prime_field_polynomial_quotient_step_prefix_functional
  7. L104
    exact hequal
  8. L105
    specialize prime_field_polynomial_quotient_prefix_entry (p)
  9. L106
    specialize prime_field_polynomial_quotient_prefix_entry (k)
  10. L107
    specialize prime_field_polynomial_quotient_prefix_entry (ab)
19Use earlier factsL108–117

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L108
    specialize prime_field_polynomial_quotient_prefix_entry (ac)
  2. L109
    specialize prime_field_polynomial_quotient_prefix_entry (bb)
  3. L110
    specialize prime_field_polynomial_quotient_prefix_entry (bc)
  4. L111
    specialize prime_field_polynomial_quotient_prefix_entry (M)
  5. L112
    specialize prime_field_polynomial_quotient_prefix_entry (qb)
  6. L113
    specialize prime_field_polynomial_quotient_prefix_entry (qc)
  7. L114
    specialize prime_field_polynomial_quotient_prefix_entry (S N)
  8. L115
    specialize prime_field_polynomial_quotient_prefix_entry (N)
  9. L116
    specialize prime_field_polynomial_quotient_prefix_entry (a)
  10. L117
    apply prime_field_polynomial_quotient_prefix_entry
20Use earlier factsL118–122

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L118
    exact hfirst
  2. L119
    specialize le_refl (S N)
  3. L120
    apply le_refl
  4. L121
    exact hvalue
  5. L122
    exact hchosen_witness_right
21Calculate and transport equalitiesL123–124

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L123
    rewrite hlast
  2. L124
    rewrite hlast
22Use earlier factsL125–130

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L125
    exact hchosen_witness_left
  2. L126
    specialize hequal (i)
  3. L127
    specialize hequal (a)
  4. L128
    apply hequal
  5. L129
    exact hcase_right
  6. L130
    exact hvalue

Library-wide reading audit

Original exact command ledger · 130 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro QB
  11. 0011intro QC
  12. 0012intro N
  13. 0013induction N
  14. 0014intro hfirst
  15. 0015intro hsecond
  16. 0016intro i
  17. 0017intro a
  18. 0018intro hindex
  19. 0019intro hvalue
  20. 0020exfalso
  21. 0021specialize lt_not_le (i)
  22. 0022specialize lt_not_le (0)
  23. 0023apply lt_not_le
  24. 0024exact hindex
  25. 0025specialize zero_le (i)
  26. 0026apply zero_le
  27. 0027intro hfirst
  28. 0028intro hsecond
  29. 0029have hequal : forall mdr_i_pfp_prefix_unique_induction mdr_a_pfp_prefix_unique_induction. (exists mdr_gap_pfp_prefix_unique_inductionb. mdr_gap_pfp_prefix_unique_inductionb + S (mdr_i_pfp_prefix_unique_induction) = (N)) -> (((exists ff_h_mdr_pfp_prefix_unique_inductiono. ff_h_mdr_pfp_prefix_unique_inductiono + S (mdr_a_pfp_prefix_unique_induction) = S ((S (mdr_i_pfp_prefix_unique_induction)) * qc)) /\ exists ff_q_mdr_pfp_prefix_unique_inductiono. qb = ff_q_mdr_pfp_prefix_unique_inductiono * S ((S (mdr_i_pfp_prefix_unique_induction)) * qc) + (mdr_a_pfp_prefix_unique_induction))) -> (((exists ff_h_mdr_pfp_prefix_unique_inductionn. ff_h_mdr_pfp_prefix_unique_inductionn + S (mdr_a_pfp_prefix_unique_induction) = S ((S (mdr_i_pfp_prefix_unique_induction)) * QC)) /\ exists ff_q_mdr_pfp_prefix_unique_inductionn. QB = ff_q_mdr_pfp_prefix_unique_inductionn * S ((S (mdr_i_pfp_prefix_unique_induction)) * QC) + (mdr_a_pfp_prefix_unique_induction)))
  30. 0030apply IH
  31. 0031specialize prime_field_polynomial_quotient_prefix_restrict (p)
  32. 0032specialize prime_field_polynomial_quotient_prefix_restrict (k)
  33. 0033specialize prime_field_polynomial_quotient_prefix_restrict (ab)
  34. 0034specialize prime_field_polynomial_quotient_prefix_restrict (ac)
  35. 0035specialize prime_field_polynomial_quotient_prefix_restrict (bb)
  36. 0036specialize prime_field_polynomial_quotient_prefix_restrict (bc)
  37. 0037specialize prime_field_polynomial_quotient_prefix_restrict (M)
  38. 0038specialize prime_field_polynomial_quotient_prefix_restrict (qb)
  39. 0039specialize prime_field_polynomial_quotient_prefix_restrict (qc)
  40. 0040specialize prime_field_polynomial_quotient_prefix_restrict (S N)
  41. 0041specialize prime_field_polynomial_quotient_prefix_restrict (N)
  42. 0042apply prime_field_polynomial_quotient_prefix_restrict
  43. 0043specialize le_succ (N)
  44. 0044specialize le_succ (N)
  45. 0045apply le_succ
  46. 0046specialize le_refl (N)
  47. 0047apply le_refl
  48. 0048exact hfirst
  49. 0049specialize prime_field_polynomial_quotient_prefix_restrict (p)
  50. 0050specialize prime_field_polynomial_quotient_prefix_restrict (k)
  51. 0051specialize prime_field_polynomial_quotient_prefix_restrict (ab)
  52. 0052specialize prime_field_polynomial_quotient_prefix_restrict (ac)
  53. 0053specialize prime_field_polynomial_quotient_prefix_restrict (bb)
  54. 0054specialize prime_field_polynomial_quotient_prefix_restrict (bc)
  55. 0055specialize prime_field_polynomial_quotient_prefix_restrict (M)
  56. 0056specialize prime_field_polynomial_quotient_prefix_restrict (QB)
  57. 0057specialize prime_field_polynomial_quotient_prefix_restrict (QC)
  58. 0058specialize prime_field_polynomial_quotient_prefix_restrict (S N)
  59. 0059specialize prime_field_polynomial_quotient_prefix_restrict (N)
  60. 0060apply prime_field_polynomial_quotient_prefix_restrict
  61. 0061specialize le_succ (N)
  62. 0062specialize le_succ (N)
  63. 0063apply le_succ
  64. 0064specialize le_refl (N)
  65. 0065apply le_refl
  66. 0066exact hsecond
  67. 0067intro i
  68. 0068intro a
  69. 0069intro hindex
  70. 0070intro hvalue
  71. 0071have hcase : i=N \/ (exists pfa_gap_prefix_unique_earlier. pfa_gap_prefix_unique_earlier + S (i) = (N))
  72. 0072specialize finite_lt_succ_eq_or_lt (N)
  73. 0073specialize finite_lt_succ_eq_or_lt (i)
  74. 0074apply finite_lt_succ_eq_or_lt
  75. 0075exact hindex
  76. 0076cases hcase
  77. 0077rewrite hcase_left at hvalue
  78. 0078rewrite hcase_left at hvalue
  79. 0079rewrite hcase_left
  80. 0080rewrite hcase_left
  81. 0081have hchosen : exists r. (((((exists ff_h_pfp_prefix_unique_other_value. ff_h_pfp_prefix_unique_other_value + S (r) = S ((S (N)) * QC)) /\ exists ff_q_pfp_prefix_unique_other_value. QB = ff_q_pfp_prefix_unique_other_value * S ((S (N)) * QC) + (r))) /\ ((exists pfd_input_prefix_unique_other_step pfd_previous_prefix_unique_other_step pfd_difference_prefix_unique_other_step. ((((exists ff_h_pfp_prefix_unique_other_stepinput. ff_h_pfp_prefix_unique_other_stepinput + S (pfd_input_prefix_unique_other_step) = S ((S (N)) * ac)) /\ exists ff_q_pfp_prefix_unique_other_stepinput. ab = ff_q_pfp_prefix_unique_other_stepinput * S ((S (N)) * ac) + (pfd_input_prefix_unique_other_step))) /\ (((exists pfc_terms_code_prefix_unique_other_stepprevious pfc_terms_scale_prefix_unique_other_stepprevious pfc_natural_sum_prefix_unique_other_stepprevious. ((forall pfc_index_prefix_unique_other_steppreviousdiagonal. (exists pfa_gap_prefix_unique_other_steppreviousdiagonalbound. pfa_gap_prefix_unique_other_steppreviousdiagonalbound + S (pfc_index_prefix_unique_other_steppreviousdiagonal) = (S (N))) -> exists pfc_value_prefix_unique_other_steppreviousdiagonal. ((((exists ff_h_pfp_prefix_unique_other_steppreviousdiagonalentry. ff_h_pfp_prefix_unique_other_steppreviousdiagonalentry + S (pfc_value_prefix_unique_other_steppreviousdiagonal) = S ((S (pfc_index_prefix_unique_other_steppreviousdiagonal)) * pfc_terms_scale_prefix_unique_other_stepprevious)) /\ exists ff_q_pfp_prefix_unique_other_steppreviousdiagonalentry. pfc_terms_code_prefix_unique_other_stepprevious = ff_q_pfp_prefix_unique_other_steppreviousdiagonalentry * S ((S (pfc_index_prefix_unique_other_steppreviousdiagonal)) * pfc_terms_scale_prefix_unique_other_stepprevious) + (pfc_value_prefix_unique_other_steppreviousdiagonal))) /\ ((exists pfc_complement_prefix_unique_other_steppreviousdiagonalterm pfc_left_prefix_unique_other_steppreviousdiagonalterm pfc_right_prefix_unique_other_steppreviousdiagonalterm. (((pfc_index_prefix_unique_other_steppreviousdiagonal)+pfc_complement_prefix_unique_other_steppreviousdiagonalterm=(N)) /\ ((((((exists pfa_gap_prefix_unique_other_steppreviousdiagonaltermleftinside. pfa_gap_prefix_unique_other_steppreviousdiagonaltermleftinside + S (pfc_index_prefix_unique_other_steppreviousdiagonal) = (N)) /\ ((((exists ff_h_pfp_prefix_unique_other_steppreviousdiagonaltermleftentry. ff_h_pfp_prefix_unique_other_steppreviousdiagonaltermleftentry + S (pfc_left_prefix_unique_other_steppreviousdiagonalterm) = S ((S (pfc_index_prefix_unique_other_steppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_prefix_unique_other_steppreviousdiagonaltermleftentry. QB = ff_q_pfp_prefix_unique_other_steppreviousdiagonaltermleftentry * S ((S (pfc_index_prefix_unique_other_steppreviousdiagonal)) * QC) + (pfc_left_prefix_unique_other_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_other_steppreviousdiagonaltermleftoutside. pfc_gap_prefix_unique_other_steppreviousdiagonaltermleftoutside+(N)=(pfc_index_prefix_unique_other_steppreviousdiagonal)) /\ (((pfc_left_prefix_unique_other_steppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_unique_other_steppreviousdiagonaltermrightinside. pfa_gap_prefix_unique_other_steppreviousdiagonaltermrightinside + S (pfc_complement_prefix_unique_other_steppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_prefix_unique_other_steppreviousdiagonaltermrightentry. ff_h_pfp_prefix_unique_other_steppreviousdiagonaltermrightentry + S (pfc_right_prefix_unique_other_steppreviousdiagonalterm) = S ((S (pfc_complement_prefix_unique_other_steppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_prefix_unique_other_steppreviousdiagonaltermrightentry. bb = ff_q_pfp_prefix_unique_other_steppreviousdiagonaltermrightentry * S ((S (pfc_complement_prefix_unique_other_steppreviousdiagonalterm)) * bc) + (pfc_right_prefix_unique_other_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_other_steppreviousdiagonaltermrightoutside. pfc_gap_prefix_unique_other_steppreviousdiagonaltermrightoutside+(M)=(pfc_complement_prefix_unique_other_steppreviousdiagonalterm)) /\ (((pfc_right_prefix_unique_other_steppreviousdiagonalterm)=0))))) /\ (((pfc_value_prefix_unique_other_steppreviousdiagonal)=pfc_left_prefix_unique_other_steppreviousdiagonalterm*pfc_right_prefix_unique_other_steppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_unique_other_stepprevioussum fs_v_pfc_prefix_unique_other_stepprevioussum. ((((exists fs_h_pfc_prefix_unique_other_stepprevioussum_body_start. fs_h_pfc_prefix_unique_other_stepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_unique_other_stepprevioussum)) /\ exists fs_q_pfc_prefix_unique_other_stepprevioussum_body_start. fs_u_pfc_prefix_unique_other_stepprevioussum = fs_q_pfc_prefix_unique_other_stepprevioussum_body_start * S ((S (0)) * fs_v_pfc_prefix_unique_other_stepprevioussum) + (0))) /\ ((((exists fs_h_pfc_prefix_unique_other_stepprevioussum_body_terminal. fs_h_pfc_prefix_unique_other_stepprevioussum_body_terminal + S (pfc_natural_sum_prefix_unique_other_stepprevious) = S ((S (S (N))) * fs_v_pfc_prefix_unique_other_stepprevioussum)) /\ exists fs_q_pfc_prefix_unique_other_stepprevioussum_body_terminal. fs_u_pfc_prefix_unique_other_stepprevioussum = fs_q_pfc_prefix_unique_other_stepprevioussum_body_terminal * S ((S (S (N))) * fs_v_pfc_prefix_unique_other_stepprevioussum) + (pfc_natural_sum_prefix_unique_other_stepprevious))) /\ forall fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps. (exists fs_lt_pfc_prefix_unique_other_stepprevioussum_body_steps_bound. fs_lt_pfc_prefix_unique_other_stepprevioussum_body_steps_bound + S fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps = S (N)) -> exists fs_a_pfc_prefix_unique_other_stepprevioussum_body_steps fs_r_pfc_prefix_unique_other_stepprevioussum_body_steps fs_s_pfc_prefix_unique_other_stepprevioussum_body_steps. ((((exists fs_h_pfc_prefix_unique_other_stepprevioussum_body_steps_summand. fs_h_pfc_prefix_unique_other_stepprevioussum_body_steps_summand + S (fs_a_pfc_prefix_unique_other_stepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_other_stepprevious)) /\ exists fs_q_pfc_prefix_unique_other_stepprevioussum_body_steps_summand. pfc_terms_code_prefix_unique_other_stepprevious = fs_q_pfc_prefix_unique_other_stepprevioussum_body_steps_summand * S ((S (fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_other_stepprevious) + (fs_a_pfc_prefix_unique_other_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_other_stepprevioussum_body_steps_partial. fs_h_pfc_prefix_unique_other_stepprevioussum_body_steps_partial + S (fs_r_pfc_prefix_unique_other_stepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_other_stepprevioussum)) /\ exists fs_q_pfc_prefix_unique_other_stepprevioussum_body_steps_partial. fs_u_pfc_prefix_unique_other_stepprevioussum = fs_q_pfc_prefix_unique_other_stepprevioussum_body_steps_partial * S ((S (fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_other_stepprevioussum) + (fs_r_pfc_prefix_unique_other_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_other_stepprevioussum_body_steps_successor. fs_h_pfc_prefix_unique_other_stepprevioussum_body_steps_successor + S (fs_s_pfc_prefix_unique_other_stepprevioussum_body_steps) = S ((S (S fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_other_stepprevioussum)) /\ exists fs_q_pfc_prefix_unique_other_stepprevioussum_body_steps_successor. fs_u_pfc_prefix_unique_other_stepprevioussum = fs_q_pfc_prefix_unique_other_stepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_prefix_unique_other_stepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_other_stepprevioussum) + (fs_s_pfc_prefix_unique_other_stepprevioussum_body_steps))) /\ fs_s_pfc_prefix_unique_other_stepprevioussum_body_steps = fs_r_pfc_prefix_unique_other_stepprevioussum_body_steps + fs_a_pfc_prefix_unique_other_stepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_prefix_unique_other_steppreviousresiduebound. pfa_gap_prefix_unique_other_steppreviousresiduebound + S (pfd_previous_prefix_unique_other_step) = (p)) /\ ((exists pfa_offset_left_prefix_unique_other_steppreviousresiduecongruence pfa_offset_right_prefix_unique_other_steppreviousresiduecongruence. (pfc_natural_sum_prefix_unique_other_stepprevious) + (p) * pfa_offset_left_prefix_unique_other_steppreviousresiduecongruence = (pfd_previous_prefix_unique_other_step) + (p) * pfa_offset_right_prefix_unique_other_steppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_prefix_unique_other_stepsubtractleft. pfa_gap_prefix_unique_other_stepsubtractleft + S (pfd_previous_prefix_unique_other_step) = (p)) /\ (((exists pfa_gap_prefix_unique_other_stepsubtractright. pfa_gap_prefix_unique_other_stepsubtractright + S (pfd_difference_prefix_unique_other_step) = (p)) /\ ((((exists pfa_gap_prefix_unique_other_stepsubtractresultbound. pfa_gap_prefix_unique_other_stepsubtractresultbound + S (pfd_input_prefix_unique_other_step) = (p)) /\ ((exists pfa_offset_left_prefix_unique_other_stepsubtractresultcongruence pfa_offset_right_prefix_unique_other_stepsubtractresultcongruence. ((pfd_previous_prefix_unique_other_step) + (pfd_difference_prefix_unique_other_step)) + (p) * pfa_offset_left_prefix_unique_other_stepsubtractresultcongruence = (pfd_input_prefix_unique_other_step) + (p) * pfa_offset_right_prefix_unique_other_stepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_prefix_unique_other_stepmultiplyleft. pfa_gap_prefix_unique_other_stepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_prefix_unique_other_stepmultiplyright. pfa_gap_prefix_unique_other_stepmultiplyright + S (pfd_difference_prefix_unique_other_step) = (p)) /\ ((((exists pfa_gap_prefix_unique_other_stepmultiplyresultbound. pfa_gap_prefix_unique_other_stepmultiplyresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_prefix_unique_other_stepmultiplyresultcongruence pfa_offset_right_prefix_unique_other_stepmultiplyresultcongruence. ((k) * (pfd_difference_prefix_unique_other_step)) + (p) * pfa_offset_left_prefix_unique_other_stepmultiplyresultcongruence = (r) + (p) * pfa_offset_right_prefix_unique_other_stepmultiplyresultcongruence)))))))))))))))))))
  82. 0082specialize hsecond (N)
  83. 0083apply hsecond
  84. 0084specialize le_refl (S N)
  85. 0085apply le_refl
  86. 0086cases hchosen
  87. 0087cases hchosen_witness
  88. 0088have hlast : a=x
  89. 0089specialize prime_field_polynomial_quotient_step_prefix_functional (p)
  90. 0090specialize prime_field_polynomial_quotient_step_prefix_functional (k)
  91. 0091specialize prime_field_polynomial_quotient_step_prefix_functional (ab)
  92. 0092specialize prime_field_polynomial_quotient_step_prefix_functional (ac)
  93. 0093specialize prime_field_polynomial_quotient_step_prefix_functional (bb)
  94. 0094specialize prime_field_polynomial_quotient_step_prefix_functional (bc)
  95. 0095specialize prime_field_polynomial_quotient_step_prefix_functional (M)
  96. 0096specialize prime_field_polynomial_quotient_step_prefix_functional (qb)
  97. 0097specialize prime_field_polynomial_quotient_step_prefix_functional (qc)
  98. 0098specialize prime_field_polynomial_quotient_step_prefix_functional (QB)
  99. 0099specialize prime_field_polynomial_quotient_step_prefix_functional (QC)
  100. 0100specialize prime_field_polynomial_quotient_step_prefix_functional (N)
  101. 0101specialize prime_field_polynomial_quotient_step_prefix_functional (a)
  102. 0102specialize prime_field_polynomial_quotient_step_prefix_functional (x)
  103. 0103apply prime_field_polynomial_quotient_step_prefix_functional
  104. 0104exact hequal
  105. 0105specialize prime_field_polynomial_quotient_prefix_entry (p)
  106. 0106specialize prime_field_polynomial_quotient_prefix_entry (k)
  107. 0107specialize prime_field_polynomial_quotient_prefix_entry (ab)
  108. 0108specialize prime_field_polynomial_quotient_prefix_entry (ac)
  109. 0109specialize prime_field_polynomial_quotient_prefix_entry (bb)
  110. 0110specialize prime_field_polynomial_quotient_prefix_entry (bc)
  111. 0111specialize prime_field_polynomial_quotient_prefix_entry (M)
  112. 0112specialize prime_field_polynomial_quotient_prefix_entry (qb)
  113. 0113specialize prime_field_polynomial_quotient_prefix_entry (qc)
  114. 0114specialize prime_field_polynomial_quotient_prefix_entry (S N)
  115. 0115specialize prime_field_polynomial_quotient_prefix_entry (N)
  116. 0116specialize prime_field_polynomial_quotient_prefix_entry (a)
  117. 0117apply prime_field_polynomial_quotient_prefix_entry
  118. 0118exact hfirst
  119. 0119specialize le_refl (S N)
  120. 0120apply le_refl
  121. 0121exact hvalue
  122. 0122exact hchosen_witness_right
  123. 0123rewrite hlast
  124. 0124rewrite hlast
  125. 0125exact hchosen_witness_left
  126. 0126specialize hequal (i)
  127. 0127specialize hequal (a)
  128. 0128apply hequal
  129. 0129exact hcase_right
  130. 0130exact hvalue