prime_field_unit_multiple_functional

Exact expanded first-order arithmetic statement

forall p n r s. (~((p) = 1) /\ forall pfa_factor_left_multiple_unique_domain pfa_factor_right_multiple_unique_domain. (p) = pfa_factor_left_multiple_unique_domain * pfa_factor_right_multiple_unique_domain -> pfa_factor_left_multiple_unique_domain = 1 \/ pfa_factor_right_multiple_unique_domain = 1) -> (exists pff_history_code_multiple_unique_first pff_history_scale_multiple_unique_first. (((((exists ff_h_pft_multiple_unique_firsthistorystart. ff_h_pft_multiple_unique_firsthistorystart + S (0) = S ((S (0)) * pff_history_scale_multiple_unique_first)) /\ exists ff_q_pft_multiple_unique_firsthistorystart. pff_history_code_multiple_unique_first = ff_q_pft_multiple_unique_firsthistorystart * S ((S (0)) * pff_history_scale_multiple_unique_first) + (0))) /\ (((((exists ff_h_pft_multiple_unique_firsthistoryterminal. ff_h_pft_multiple_unique_firsthistoryterminal + S (r) = S ((S (n)) * pff_history_scale_multiple_unique_first)) /\ exists ff_q_pft_multiple_unique_firsthistoryterminal. pff_history_code_multiple_unique_first = ff_q_pft_multiple_unique_firsthistoryterminal * S ((S (n)) * pff_history_scale_multiple_unique_first) + (r))) /\ ((forall pff_trace_index_multiple_unique_firsthistorysteps. (exists pfa_gap_multiple_unique_firsthistorystepsindex. pfa_gap_multiple_unique_firsthistorystepsindex + S (pff_trace_index_multiple_unique_firsthistorysteps) = (n)) -> exists pff_trace_before_multiple_unique_firsthistorysteps pff_trace_after_multiple_unique_firsthistorysteps. ((((exists ff_h_pft_multiple_unique_firsthistorystepsbefore. ff_h_pft_multiple_unique_firsthistorystepsbefore + S (pff_trace_before_multiple_unique_firsthistorysteps) = S ((S (pff_trace_index_multiple_unique_firsthistorysteps)) * pff_history_scale_multiple_unique_first)) /\ exists ff_q_pft_multiple_unique_firsthistorystepsbefore. pff_history_code_multiple_unique_first = ff_q_pft_multiple_unique_firsthistorystepsbefore * S ((S (pff_trace_index_multiple_unique_firsthistorysteps)) * pff_history_scale_multiple_unique_first) + (pff_trace_before_multiple_unique_firsthistorysteps))) /\ (((((exists ff_h_pft_multiple_unique_firsthistorystepsafter. ff_h_pft_multiple_unique_firsthistorystepsafter + S (pff_trace_after_multiple_unique_firsthistorysteps) = S ((S (S (pff_trace_index_multiple_unique_firsthistorysteps))) * pff_history_scale_multiple_unique_first)) /\ exists ff_q_pft_multiple_unique_firsthistorystepsafter. pff_history_code_multiple_unique_first = ff_q_pft_multiple_unique_firsthistorystepsafter * S ((S (S (pff_trace_index_multiple_unique_firsthistorysteps))) * pff_history_scale_multiple_unique_first) + (pff_trace_after_multiple_unique_firsthistorysteps))) /\ ((((exists pfa_gap_multiple_unique_firsthistorystepsadditionleft. pfa_gap_multiple_unique_firsthistorystepsadditionleft + S (pff_trace_before_multiple_unique_firsthistorysteps) = (p)) /\ (((exists pfa_gap_multiple_unique_firsthistorystepsadditionright. pfa_gap_multiple_unique_firsthistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_multiple_unique_firsthistorystepsadditionresultbound. pfa_gap_multiple_unique_firsthistorystepsadditionresultbound + S (pff_trace_after_multiple_unique_firsthistorysteps) = (p)) /\ ((exists pfa_offset_left_multiple_unique_firsthistorystepsadditionresultcongruence pfa_offset_right_multiple_unique_firsthistorystepsadditionresultcongruence. ((pff_trace_before_multiple_unique_firsthistorysteps) + (1)) + (p) * pfa_offset_left_multiple_unique_firsthistorystepsadditionresultcongruence = (pff_trace_after_multiple_unique_firsthistorysteps) + (p) * pfa_offset_right_multiple_unique_firsthistorystepsadditionresultcongruence)))))))))))))))))))) -> (exists pff_history_code_multiple_unique_second pff_history_scale_multiple_unique_second. (((((exists ff_h_pft_multiple_unique_secondhistorystart. ff_h_pft_multiple_unique_secondhistorystart + S (0) = S ((S (0)) * pff_history_scale_multiple_unique_second)) /\ exists ff_q_pft_multiple_unique_secondhistorystart. pff_history_code_multiple_unique_second = ff_q_pft_multiple_unique_secondhistorystart * S ((S (0)) * pff_history_scale_multiple_unique_second) + (0))) /\ (((((exists ff_h_pft_multiple_unique_secondhistoryterminal. ff_h_pft_multiple_unique_secondhistoryterminal + S (s) = S ((S (n)) * pff_history_scale_multiple_unique_second)) /\ exists ff_q_pft_multiple_unique_secondhistoryterminal. pff_history_code_multiple_unique_second = ff_q_pft_multiple_unique_secondhistoryterminal * S ((S (n)) * pff_history_scale_multiple_unique_second) + (s))) /\ ((forall pff_trace_index_multiple_unique_secondhistorysteps. (exists pfa_gap_multiple_unique_secondhistorystepsindex. pfa_gap_multiple_unique_secondhistorystepsindex + S (pff_trace_index_multiple_unique_secondhistorysteps) = (n)) -> exists pff_trace_before_multiple_unique_secondhistorysteps pff_trace_after_multiple_unique_secondhistorysteps. ((((exists ff_h_pft_multiple_unique_secondhistorystepsbefore. ff_h_pft_multiple_unique_secondhistorystepsbefore + S (pff_trace_before_multiple_unique_secondhistorysteps) = S ((S (pff_trace_index_multiple_unique_secondhistorysteps)) * pff_history_scale_multiple_unique_second)) /\ exists ff_q_pft_multiple_unique_secondhistorystepsbefore. pff_history_code_multiple_unique_second = ff_q_pft_multiple_unique_secondhistorystepsbefore * S ((S (pff_trace_index_multiple_unique_secondhistorysteps)) * pff_history_scale_multiple_unique_second) + (pff_trace_before_multiple_unique_secondhistorysteps))) /\ (((((exists ff_h_pft_multiple_unique_secondhistorystepsafter. ff_h_pft_multiple_unique_secondhistorystepsafter + S (pff_trace_after_multiple_unique_secondhistorysteps) = S ((S (S (pff_trace_index_multiple_unique_secondhistorysteps))) * pff_history_scale_multiple_unique_second)) /\ exists ff_q_pft_multiple_unique_secondhistorystepsafter. pff_history_code_multiple_unique_second = ff_q_pft_multiple_unique_secondhistorystepsafter * S ((S (S (pff_trace_index_multiple_unique_secondhistorysteps))) * pff_history_scale_multiple_unique_second) + (pff_trace_after_multiple_unique_secondhistorysteps))) /\ ((((exists pfa_gap_multiple_unique_secondhistorystepsadditionleft. pfa_gap_multiple_unique_secondhistorystepsadditionleft + S (pff_trace_before_multiple_unique_secondhistorysteps) = (p)) /\ (((exists pfa_gap_multiple_unique_secondhistorystepsadditionright. pfa_gap_multiple_unique_secondhistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_multiple_unique_secondhistorystepsadditionresultbound. pfa_gap_multiple_unique_secondhistorystepsadditionresultbound + S (pff_trace_after_multiple_unique_secondhistorysteps) = (p)) /\ ((exists pfa_offset_left_multiple_unique_secondhistorystepsadditionresultcongruence pfa_offset_right_multiple_unique_secondhistorystepsadditionresultcongruence. ((pff_trace_before_multiple_unique_secondhistorysteps) + (1)) + (p) * pfa_offset_left_multiple_unique_secondhistorystepsadditionresultcongruence = (pff_trace_after_multiple_unique_secondhistorysteps) + (p) * pfa_offset_right_multiple_unique_secondhistorystepsadditionresultcongruence)))))))))))))))))))) -> r = s