prime_field_characteristic_exact

Exact expanded first-order arithmetic statement

forall p. (~((p) = 1) /\ forall pfa_factor_left_characteristic_domain pfa_factor_right_characteristic_domain. (p) = pfa_factor_left_characteristic_domain * pfa_factor_right_characteristic_domain -> pfa_factor_left_characteristic_domain = 1 \/ pfa_factor_right_characteristic_domain = 1) -> (((exists pff_history_code_characteristic_exactmodulus pff_history_scale_characteristic_exactmodulus. (((((exists ff_h_pft_characteristic_exactmodulushistorystart. ff_h_pft_characteristic_exactmodulushistorystart + S (0) = S ((S (0)) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistorystart. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistorystart * S ((S (0)) * pff_history_scale_characteristic_exactmodulus) + (0))) /\ (((((exists ff_h_pft_characteristic_exactmodulushistoryterminal. ff_h_pft_characteristic_exactmodulushistoryterminal + S (0) = S ((S (p)) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistoryterminal. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistoryterminal * S ((S (p)) * pff_history_scale_characteristic_exactmodulus) + (0))) /\ ((forall pff_trace_index_characteristic_exactmodulushistorysteps. (exists pfa_gap_characteristic_exactmodulushistorystepsindex. pfa_gap_characteristic_exactmodulushistorystepsindex + S (pff_trace_index_characteristic_exactmodulushistorysteps) = (p)) -> exists pff_trace_before_characteristic_exactmodulushistorysteps pff_trace_after_characteristic_exactmodulushistorysteps. ((((exists ff_h_pft_characteristic_exactmodulushistorystepsbefore. ff_h_pft_characteristic_exactmodulushistorystepsbefore + S (pff_trace_before_characteristic_exactmodulushistorysteps) = S ((S (pff_trace_index_characteristic_exactmodulushistorysteps)) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistorystepsbefore. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistorystepsbefore * S ((S (pff_trace_index_characteristic_exactmodulushistorysteps)) * pff_history_scale_characteristic_exactmodulus) + (pff_trace_before_characteristic_exactmodulushistorysteps))) /\ (((((exists ff_h_pft_characteristic_exactmodulushistorystepsafter. ff_h_pft_characteristic_exactmodulushistorystepsafter + S (pff_trace_after_characteristic_exactmodulushistorysteps) = S ((S (S (pff_trace_index_characteristic_exactmodulushistorysteps))) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistorystepsafter. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistorystepsafter * S ((S (S (pff_trace_index_characteristic_exactmodulushistorysteps))) * pff_history_scale_characteristic_exactmodulus) + (pff_trace_after_characteristic_exactmodulushistorysteps))) /\ ((((exists pfa_gap_characteristic_exactmodulushistorystepsadditionleft. pfa_gap_characteristic_exactmodulushistorystepsadditionleft + S (pff_trace_before_characteristic_exactmodulushistorysteps) = (p)) /\ (((exists pfa_gap_characteristic_exactmodulushistorystepsadditionright. pfa_gap_characteristic_exactmodulushistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_characteristic_exactmodulushistorystepsadditionresultbound. pfa_gap_characteristic_exactmodulushistorystepsadditionresultbound + S (pff_trace_after_characteristic_exactmodulushistorysteps) = (p)) /\ ((exists pfa_offset_left_characteristic_exactmodulushistorystepsadditionresultcongruence pfa_offset_right_characteristic_exactmodulushistorystepsadditionresultcongruence. ((pff_trace_before_characteristic_exactmodulushistorysteps) + (1)) + (p) * pfa_offset_left_characteristic_exactmodulushistorystepsadditionresultcongruence = (pff_trace_after_characteristic_exactmodulushistorysteps) + (p) * pfa_offset_right_characteristic_exactmodulushistorystepsadditionresultcongruence)))))))))))))))))))) /\ ((forall pff_smaller_positive_characteristic_exact. (exists pfa_gap_characteristic_exactstrict. pfa_gap_characteristic_exactstrict + S (pff_smaller_positive_characteristic_exact) = (p)) -> ~(pff_smaller_positive_characteristic_exact = 0) -> ~(exists pff_history_code_characteristic_exactsmaller pff_history_scale_characteristic_exactsmaller. (((((exists ff_h_pft_characteristic_exactsmallerhistorystart. ff_h_pft_characteristic_exactsmallerhistorystart + S (0) = S ((S (0)) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistorystart. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistorystart * S ((S (0)) * pff_history_scale_characteristic_exactsmaller) + (0))) /\ (((((exists ff_h_pft_characteristic_exactsmallerhistoryterminal. ff_h_pft_characteristic_exactsmallerhistoryterminal + S (0) = S ((S (pff_smaller_positive_characteristic_exact)) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistoryterminal. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistoryterminal * S ((S (pff_smaller_positive_characteristic_exact)) * pff_history_scale_characteristic_exactsmaller) + (0))) /\ ((forall pff_trace_index_characteristic_exactsmallerhistorysteps. (exists pfa_gap_characteristic_exactsmallerhistorystepsindex. pfa_gap_characteristic_exactsmallerhistorystepsindex + S (pff_trace_index_characteristic_exactsmallerhistorysteps) = (pff_smaller_positive_characteristic_exact)) -> exists pff_trace_before_characteristic_exactsmallerhistorysteps pff_trace_after_characteristic_exactsmallerhistorysteps. ((((exists ff_h_pft_characteristic_exactsmallerhistorystepsbefore. ff_h_pft_characteristic_exactsmallerhistorystepsbefore + S (pff_trace_before_characteristic_exactsmallerhistorysteps) = S ((S (pff_trace_index_characteristic_exactsmallerhistorysteps)) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistorystepsbefore. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistorystepsbefore * S ((S (pff_trace_index_characteristic_exactsmallerhistorysteps)) * pff_history_scale_characteristic_exactsmaller) + (pff_trace_before_characteristic_exactsmallerhistorysteps))) /\ (((((exists ff_h_pft_characteristic_exactsmallerhistorystepsafter. ff_h_pft_characteristic_exactsmallerhistorystepsafter + S (pff_trace_after_characteristic_exactsmallerhistorysteps) = S ((S (S (pff_trace_index_characteristic_exactsmallerhistorysteps))) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistorystepsafter. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistorystepsafter * S ((S (S (pff_trace_index_characteristic_exactsmallerhistorysteps))) * pff_history_scale_characteristic_exactsmaller) + (pff_trace_after_characteristic_exactsmallerhistorysteps))) /\ ((((exists pfa_gap_characteristic_exactsmallerhistorystepsadditionleft. pfa_gap_characteristic_exactsmallerhistorystepsadditionleft + S (pff_trace_before_characteristic_exactsmallerhistorysteps) = (p)) /\ (((exists pfa_gap_characteristic_exactsmallerhistorystepsadditionright. pfa_gap_characteristic_exactsmallerhistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_characteristic_exactsmallerhistorystepsadditionresultbound. pfa_gap_characteristic_exactsmallerhistorystepsadditionresultbound + S (pff_trace_after_characteristic_exactsmallerhistorysteps) = (p)) /\ ((exists pfa_offset_left_characteristic_exactsmallerhistorystepsadditionresultcongruence pfa_offset_right_characteristic_exactsmallerhistorystepsadditionresultcongruence. ((pff_trace_before_characteristic_exactsmallerhistorysteps) + (1)) + (p) * pfa_offset_left_characteristic_exactsmallerhistorystepsadditionresultcongruence = (pff_trace_after_characteristic_exactsmallerhistorysteps) + (p) * pfa_offset_right_characteristic_exactsmallerhistorystepsadditionresultcongruence))))))))))))))))))))))))