prime_field_arithmetic_laws

Exact expanded first-order arithmetic statement

forall p. (~((p) = 1) /\ forall pfa_factor_left_complete_laws_domain pfa_factor_right_complete_laws_domain. (p) = pfa_factor_left_complete_laws_domain * pfa_factor_right_complete_laws_domain -> pfa_factor_left_complete_laws_domain = 1 \/ pfa_factor_right_complete_laws_domain = 1) -> (((exists pfa_gap_complete_lawszero. pfa_gap_complete_lawszero + S (0) = (p)) /\ (((exists pfa_gap_complete_lawsone. pfa_gap_complete_lawsone + S (1) = (p)) /\ (((~(0 = 1)) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws. (exists pfa_gap_complete_lawsaddleft. pfa_gap_complete_lawsaddleft + S (pfa_law_a_complete_laws) = (p)) -> (exists pfa_gap_complete_lawsaddright. pfa_gap_complete_lawsaddright + S (pfa_law_b_complete_laws) = (p)) -> exists pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsaddchosenleft. pfa_gap_complete_lawsaddchosenleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddchosenright. pfa_gap_complete_lawsaddchosenright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddchosenresultbound. pfa_gap_complete_lawsaddchosenresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddchosenresultcongruence pfa_offset_right_complete_lawsaddchosenresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddchosenresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsaddchosenresultcongruence))))))))) /\ forall pfa_law_d_complete_laws. (((exists pfa_gap_complete_lawsaddotherleft. pfa_gap_complete_lawsaddotherleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddotherright. pfa_gap_complete_lawsaddotherright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddotherresultbound. pfa_gap_complete_lawsaddotherresultbound + S (pfa_law_d_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddotherresultcongruence pfa_offset_right_complete_lawsaddotherresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddotherresultcongruence = (pfa_law_d_complete_laws) + (p) * pfa_offset_right_complete_lawsaddotherresultcongruence))))))))) -> pfa_law_d_complete_laws = pfa_law_c_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsaddcomm_firstleft. pfa_gap_complete_lawsaddcomm_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddcomm_firstright. pfa_gap_complete_lawsaddcomm_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddcomm_firstresultbound. pfa_gap_complete_lawsaddcomm_firstresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddcomm_firstresultcongruence pfa_offset_right_complete_lawsaddcomm_firstresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddcomm_firstresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsaddcomm_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddcomm_secondleft. pfa_gap_complete_lawsaddcomm_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddcomm_secondright. pfa_gap_complete_lawsaddcomm_secondright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddcomm_secondresultbound. pfa_gap_complete_lawsaddcomm_secondresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddcomm_secondresultcongruence pfa_offset_right_complete_lawsaddcomm_secondresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddcomm_secondresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsaddcomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsaddassoc_firstleft. pfa_gap_complete_lawsaddassoc_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_firstright. pfa_gap_complete_lawsaddassoc_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_firstresultbound. pfa_gap_complete_lawsaddassoc_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_firstresultcongruence pfa_offset_right_complete_lawsaddassoc_firstresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddassoc_leftleft. pfa_gap_complete_lawsaddassoc_leftleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_leftright. pfa_gap_complete_lawsaddassoc_leftright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_leftresultbound. pfa_gap_complete_lawsaddassoc_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_leftresultcongruence pfa_offset_right_complete_lawsaddassoc_leftresultcongruence. ((pfa_law_x_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddassoc_secondleft. pfa_gap_complete_lawsaddassoc_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_secondright. pfa_gap_complete_lawsaddassoc_secondright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_secondresultbound. pfa_gap_complete_lawsaddassoc_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_secondresultcongruence pfa_offset_right_complete_lawsaddassoc_secondresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsaddassoc_rightleft. pfa_gap_complete_lawsaddassoc_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsaddassoc_rightright. pfa_gap_complete_lawsaddassoc_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsaddassoc_rightresultbound. pfa_gap_complete_lawsaddassoc_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsaddassoc_rightresultcongruence pfa_offset_right_complete_lawsaddassoc_rightresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsaddassoc_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsaddassoc_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws. (exists pfa_gap_complete_lawsmultiplyleft. pfa_gap_complete_lawsmultiplyleft + S (pfa_law_a_complete_laws) = (p)) -> (exists pfa_gap_complete_lawsmultiplyright. pfa_gap_complete_lawsmultiplyright + S (pfa_law_b_complete_laws) = (p)) -> exists pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsmultiplychosenleft. pfa_gap_complete_lawsmultiplychosenleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplychosenright. pfa_gap_complete_lawsmultiplychosenright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplychosenresultbound. pfa_gap_complete_lawsmultiplychosenresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplychosenresultcongruence pfa_offset_right_complete_lawsmultiplychosenresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplychosenresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplychosenresultcongruence))))))))) /\ forall pfa_law_d_complete_laws. (((exists pfa_gap_complete_lawsmultiplyotherleft. pfa_gap_complete_lawsmultiplyotherleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyotherright. pfa_gap_complete_lawsmultiplyotherright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyotherresultbound. pfa_gap_complete_lawsmultiplyotherresultbound + S (pfa_law_d_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyotherresultcongruence pfa_offset_right_complete_lawsmultiplyotherresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyotherresultcongruence = (pfa_law_d_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyotherresultcongruence))))))))) -> pfa_law_d_complete_laws = pfa_law_c_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsmultiplycomm_firstleft. pfa_gap_complete_lawsmultiplycomm_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplycomm_firstright. pfa_gap_complete_lawsmultiplycomm_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplycomm_firstresultbound. pfa_gap_complete_lawsmultiplycomm_firstresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplycomm_firstresultcongruence pfa_offset_right_complete_lawsmultiplycomm_firstresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplycomm_firstresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplycomm_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplycomm_secondleft. pfa_gap_complete_lawsmultiplycomm_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplycomm_secondright. pfa_gap_complete_lawsmultiplycomm_secondright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplycomm_secondresultbound. pfa_gap_complete_lawsmultiplycomm_secondresultbound + S (pfa_law_c_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplycomm_secondresultcongruence pfa_offset_right_complete_lawsmultiplycomm_secondresultcongruence. ((pfa_law_b_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplycomm_secondresultcongruence = (pfa_law_c_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplycomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsmultiplyassoc_firstleft. pfa_gap_complete_lawsmultiplyassoc_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_firstright. pfa_gap_complete_lawsmultiplyassoc_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_firstresultbound. pfa_gap_complete_lawsmultiplyassoc_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_firstresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_firstresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplyassoc_leftleft. pfa_gap_complete_lawsmultiplyassoc_leftleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_leftright. pfa_gap_complete_lawsmultiplyassoc_leftright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_leftresultbound. pfa_gap_complete_lawsmultiplyassoc_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_leftresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_leftresultcongruence. ((pfa_law_x_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplyassoc_secondleft. pfa_gap_complete_lawsmultiplyassoc_secondleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_secondright. pfa_gap_complete_lawsmultiplyassoc_secondright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_secondresultbound. pfa_gap_complete_lawsmultiplyassoc_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_secondresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_secondresultcongruence. ((pfa_law_b_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsmultiplyassoc_rightleft. pfa_gap_complete_lawsmultiplyassoc_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiplyassoc_rightright. pfa_gap_complete_lawsmultiplyassoc_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiplyassoc_rightresultbound. pfa_gap_complete_lawsmultiplyassoc_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiplyassoc_rightresultcongruence pfa_offset_right_complete_lawsmultiplyassoc_rightresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiplyassoc_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiplyassoc_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_s_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsleftdistribution_sumleft. pfa_gap_complete_lawsleftdistribution_sumleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_sumright. pfa_gap_complete_lawsleftdistribution_sumright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_sumresultbound. pfa_gap_complete_lawsleftdistribution_sumresultbound + S (pfa_law_s_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_sumresultcongruence pfa_offset_right_complete_lawsleftdistribution_sumresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_sumresultcongruence = (pfa_law_s_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_leftleft. pfa_gap_complete_lawsleftdistribution_leftleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_leftright. pfa_gap_complete_lawsleftdistribution_leftright + S (pfa_law_s_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_leftresultbound. pfa_gap_complete_lawsleftdistribution_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_leftresultcongruence pfa_offset_right_complete_lawsleftdistribution_leftresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_s_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_firstleft. pfa_gap_complete_lawsleftdistribution_firstleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_firstright. pfa_gap_complete_lawsleftdistribution_firstright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_firstresultbound. pfa_gap_complete_lawsleftdistribution_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_firstresultcongruence pfa_offset_right_complete_lawsleftdistribution_firstresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_secondleft. pfa_gap_complete_lawsleftdistribution_secondleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_secondright. pfa_gap_complete_lawsleftdistribution_secondright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_secondresultbound. pfa_gap_complete_lawsleftdistribution_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_secondresultcongruence pfa_offset_right_complete_lawsleftdistribution_secondresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsleftdistribution_rightleft. pfa_gap_complete_lawsleftdistribution_rightleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsleftdistribution_rightright. pfa_gap_complete_lawsleftdistribution_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsleftdistribution_rightresultbound. pfa_gap_complete_lawsleftdistribution_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsleftdistribution_rightresultcongruence pfa_offset_right_complete_lawsleftdistribution_rightresultcongruence. ((pfa_law_x_complete_laws) + (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsleftdistribution_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsleftdistribution_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws pfa_law_b_complete_laws pfa_law_c_complete_laws pfa_law_s_complete_laws pfa_law_x_complete_laws pfa_law_y_complete_laws pfa_law_u_complete_laws pfa_law_v_complete_laws. (((exists pfa_gap_complete_lawsrightdistribution_sumleft. pfa_gap_complete_lawsrightdistribution_sumleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_sumright. pfa_gap_complete_lawsrightdistribution_sumright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_sumresultbound. pfa_gap_complete_lawsrightdistribution_sumresultbound + S (pfa_law_s_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_sumresultcongruence pfa_offset_right_complete_lawsrightdistribution_sumresultcongruence. ((pfa_law_b_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_sumresultcongruence = (pfa_law_s_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_leftleft. pfa_gap_complete_lawsrightdistribution_leftleft + S (pfa_law_s_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_leftright. pfa_gap_complete_lawsrightdistribution_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_leftresultbound. pfa_gap_complete_lawsrightdistribution_leftresultbound + S (pfa_law_u_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_leftresultcongruence pfa_offset_right_complete_lawsrightdistribution_leftresultcongruence. ((pfa_law_s_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_leftresultcongruence = (pfa_law_u_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_firstleft. pfa_gap_complete_lawsrightdistribution_firstleft + S (pfa_law_b_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_firstright. pfa_gap_complete_lawsrightdistribution_firstright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_firstresultbound. pfa_gap_complete_lawsrightdistribution_firstresultbound + S (pfa_law_x_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_firstresultcongruence pfa_offset_right_complete_lawsrightdistribution_firstresultcongruence. ((pfa_law_b_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_firstresultcongruence = (pfa_law_x_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_secondleft. pfa_gap_complete_lawsrightdistribution_secondleft + S (pfa_law_c_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_secondright. pfa_gap_complete_lawsrightdistribution_secondright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_secondresultbound. pfa_gap_complete_lawsrightdistribution_secondresultbound + S (pfa_law_y_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_secondresultcongruence pfa_offset_right_complete_lawsrightdistribution_secondresultcongruence. ((pfa_law_c_complete_laws) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_secondresultcongruence = (pfa_law_y_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_complete_lawsrightdistribution_rightleft. pfa_gap_complete_lawsrightdistribution_rightleft + S (pfa_law_x_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsrightdistribution_rightright. pfa_gap_complete_lawsrightdistribution_rightright + S (pfa_law_y_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsrightdistribution_rightresultbound. pfa_gap_complete_lawsrightdistribution_rightresultbound + S (pfa_law_v_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsrightdistribution_rightresultcongruence pfa_offset_right_complete_lawsrightdistribution_rightresultcongruence. ((pfa_law_x_complete_laws) + (pfa_law_y_complete_laws)) + (p) * pfa_offset_left_complete_lawsrightdistribution_rightresultcongruence = (pfa_law_v_complete_laws) + (p) * pfa_offset_right_complete_lawsrightdistribution_rightresultcongruence))))))))) -> pfa_law_u_complete_laws = pfa_law_v_complete_laws) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsadd_zero_rightinput. pfa_gap_complete_lawsadd_zero_rightinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsadd_zero_rightleft. pfa_gap_complete_lawsadd_zero_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsadd_zero_rightright. pfa_gap_complete_lawsadd_zero_rightright + S (0) = (p)) /\ ((((exists pfa_gap_complete_lawsadd_zero_rightresultbound. pfa_gap_complete_lawsadd_zero_rightresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsadd_zero_rightresultcongruence pfa_offset_right_complete_lawsadd_zero_rightresultcongruence. ((pfa_law_a_complete_laws) + (0)) + (p) * pfa_offset_left_complete_lawsadd_zero_rightresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsadd_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsadd_zero_leftinput. pfa_gap_complete_lawsadd_zero_leftinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsadd_zero_leftleft. pfa_gap_complete_lawsadd_zero_leftleft + S (0) = (p)) /\ (((exists pfa_gap_complete_lawsadd_zero_leftright. pfa_gap_complete_lawsadd_zero_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsadd_zero_leftresultbound. pfa_gap_complete_lawsadd_zero_leftresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsadd_zero_leftresultcongruence pfa_offset_right_complete_lawsadd_zero_leftresultcongruence. ((0) + (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsadd_zero_leftresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsadd_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_one_rightinput. pfa_gap_complete_lawsmultiply_one_rightinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_one_rightleft. pfa_gap_complete_lawsmultiply_one_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_one_rightright. pfa_gap_complete_lawsmultiply_one_rightright + S (1) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_one_rightresultbound. pfa_gap_complete_lawsmultiply_one_rightresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_one_rightresultcongruence pfa_offset_right_complete_lawsmultiply_one_rightresultcongruence. ((pfa_law_a_complete_laws) * (1)) + (p) * pfa_offset_left_complete_lawsmultiply_one_rightresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiply_one_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_one_leftinput. pfa_gap_complete_lawsmultiply_one_leftinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_one_leftleft. pfa_gap_complete_lawsmultiply_one_leftleft + S (1) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_one_leftright. pfa_gap_complete_lawsmultiply_one_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_one_leftresultbound. pfa_gap_complete_lawsmultiply_one_leftresultbound + S (pfa_law_a_complete_laws) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_one_leftresultcongruence pfa_offset_right_complete_lawsmultiply_one_leftresultcongruence. ((1) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiply_one_leftresultcongruence = (pfa_law_a_complete_laws) + (p) * pfa_offset_right_complete_lawsmultiply_one_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_zero_rightinput. pfa_gap_complete_lawsmultiply_zero_rightinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_zero_rightleft. pfa_gap_complete_lawsmultiply_zero_rightleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_zero_rightright. pfa_gap_complete_lawsmultiply_zero_rightright + S (0) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_zero_rightresultbound. pfa_gap_complete_lawsmultiply_zero_rightresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_zero_rightresultcongruence pfa_offset_right_complete_lawsmultiply_zero_rightresultcongruence. ((pfa_law_a_complete_laws) * (0)) + (p) * pfa_offset_left_complete_lawsmultiply_zero_rightresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsmultiply_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsmultiply_zero_leftinput. pfa_gap_complete_lawsmultiply_zero_leftinput + S (pfa_law_a_complete_laws) = (p)) -> (((exists pfa_gap_complete_lawsmultiply_zero_leftleft. pfa_gap_complete_lawsmultiply_zero_leftleft + S (0) = (p)) /\ (((exists pfa_gap_complete_lawsmultiply_zero_leftright. pfa_gap_complete_lawsmultiply_zero_leftright + S (pfa_law_a_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsmultiply_zero_leftresultbound. pfa_gap_complete_lawsmultiply_zero_leftresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsmultiply_zero_leftresultcongruence pfa_offset_right_complete_lawsmultiply_zero_leftresultcongruence. ((0) * (pfa_law_a_complete_laws)) + (p) * pfa_offset_left_complete_lawsmultiply_zero_leftresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsmultiply_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsnegateinput. pfa_gap_complete_lawsnegateinput + S (pfa_law_a_complete_laws) = (p)) -> exists pfa_law_b_complete_laws. (((exists pfa_gap_complete_lawsnegatechosenadditionleft. pfa_gap_complete_lawsnegatechosenadditionleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsnegatechosenadditionright. pfa_gap_complete_lawsnegatechosenadditionright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsnegatechosenadditionresultbound. pfa_gap_complete_lawsnegatechosenadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsnegatechosenadditionresultcongruence pfa_offset_right_complete_lawsnegatechosenadditionresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsnegatechosenadditionresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsnegatechosenadditionresultcongruence))))))))) /\ forall pfa_law_c_complete_laws. (((exists pfa_gap_complete_lawsnegateotheradditionleft. pfa_gap_complete_lawsnegateotheradditionleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsnegateotheradditionright. pfa_gap_complete_lawsnegateotheradditionright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsnegateotheradditionresultbound. pfa_gap_complete_lawsnegateotheradditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsnegateotheradditionresultcongruence pfa_offset_right_complete_lawsnegateotheradditionresultcongruence. ((pfa_law_a_complete_laws) + (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsnegateotheradditionresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsnegateotheradditionresultcongruence))))))))) -> pfa_law_c_complete_laws = pfa_law_b_complete_laws) /\ (((forall pfa_law_a_complete_laws. (exists pfa_gap_complete_lawsinverseinput. pfa_gap_complete_lawsinverseinput + S (pfa_law_a_complete_laws) = (p)) -> ~(pfa_law_a_complete_laws = 0) -> exists pfa_law_b_complete_laws. (((~((pfa_law_a_complete_laws) = 0)) /\ ((((exists pfa_gap_complete_lawsinversechosenmultiplicationleft. pfa_gap_complete_lawsinversechosenmultiplicationleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsinversechosenmultiplicationright. pfa_gap_complete_lawsinversechosenmultiplicationright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsinversechosenmultiplicationresultbound. pfa_gap_complete_lawsinversechosenmultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_complete_lawsinversechosenmultiplicationresultcongruence pfa_offset_right_complete_lawsinversechosenmultiplicationresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsinversechosenmultiplicationresultcongruence = (1) + (p) * pfa_offset_right_complete_lawsinversechosenmultiplicationresultcongruence)))))))))))) /\ forall pfa_law_c_complete_laws. (((~((pfa_law_a_complete_laws) = 0)) /\ ((((exists pfa_gap_complete_lawsinverseothermultiplicationleft. pfa_gap_complete_lawsinverseothermultiplicationleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsinverseothermultiplicationright. pfa_gap_complete_lawsinverseothermultiplicationright + S (pfa_law_c_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsinverseothermultiplicationresultbound. pfa_gap_complete_lawsinverseothermultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_complete_lawsinverseothermultiplicationresultcongruence pfa_offset_right_complete_lawsinverseothermultiplicationresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_c_complete_laws)) + (p) * pfa_offset_left_complete_lawsinverseothermultiplicationresultcongruence = (1) + (p) * pfa_offset_right_complete_lawsinverseothermultiplicationresultcongruence)))))))))))) -> pfa_law_c_complete_laws = pfa_law_b_complete_laws) /\ ((forall pfa_law_a_complete_laws pfa_law_b_complete_laws. (((exists pfa_gap_complete_lawsnozeroleft. pfa_gap_complete_lawsnozeroleft + S (pfa_law_a_complete_laws) = (p)) /\ (((exists pfa_gap_complete_lawsnozeroright. pfa_gap_complete_lawsnozeroright + S (pfa_law_b_complete_laws) = (p)) /\ ((((exists pfa_gap_complete_lawsnozeroresultbound. pfa_gap_complete_lawsnozeroresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_complete_lawsnozeroresultcongruence pfa_offset_right_complete_lawsnozeroresultcongruence. ((pfa_law_a_complete_laws) * (pfa_law_b_complete_laws)) + (p) * pfa_offset_left_complete_lawsnozeroresultcongruence = (0) + (p) * pfa_offset_right_complete_lawsnozeroresultcongruence))))))))) -> pfa_law_a_complete_laws = 0 \/ pfa_law_b_complete_laws = 0))))))))))))))))))))))))))))))))))))))))