prime_field_of_prime_order_exists

Exact expanded first-order arithmetic statement

forall p. (~((p) = 1) /\ forall pfa_factor_left_finite_structure_domain pfa_factor_right_finite_structure_domain. (p) = pfa_factor_left_finite_structure_domain * pfa_factor_right_finite_structure_domain -> pfa_factor_left_finite_structure_domain = 1 \/ pfa_factor_right_finite_structure_domain = 1) -> exists ab ac mb mc nb nc ib ic eb ec. (((((forall pft_index_finite_structuretablesadd. (exists pfa_gap_finite_structuretablesaddprefix. pfa_gap_finite_structuretablesaddprefix + S (pft_index_finite_structuretablesadd) = ((p) * (p))) -> exists pft_value_finite_structuretablesadd. (((((exists ff_h_pft_finite_structuretablesaddpointentry. ff_h_pft_finite_structuretablesaddpointentry + S (pft_value_finite_structuretablesadd) = S ((S (pft_index_finite_structuretablesadd)) * ac)) /\ exists ff_q_pft_finite_structuretablesaddpointentry. ab = ff_q_pft_finite_structuretablesaddpointentry * S ((S (pft_index_finite_structuretablesadd)) * ac) + (pft_value_finite_structuretablesadd))) /\ ((exists pft_row_finite_structuretablesaddpointvalue pft_column_finite_structuretablesaddpointvalue. (((pft_index_finite_structuretablesadd) = pft_row_finite_structuretablesaddpointvalue * (p) + pft_column_finite_structuretablesaddpointvalue) /\ ((((exists pfa_gap_finite_structuretablesaddpointvalueoperationleft. pfa_gap_finite_structuretablesaddpointvalueoperationleft + S (pft_row_finite_structuretablesaddpointvalue) = (p)) /\ (((exists pfa_gap_finite_structuretablesaddpointvalueoperationright. pfa_gap_finite_structuretablesaddpointvalueoperationright + S (pft_column_finite_structuretablesaddpointvalue) = (p)) /\ ((((exists pfa_gap_finite_structuretablesaddpointvalueoperationresultbound. pfa_gap_finite_structuretablesaddpointvalueoperationresultbound + S (pft_value_finite_structuretablesadd) = (p)) /\ ((exists pfa_offset_left_finite_structuretablesaddpointvalueoperationresultcongruence pfa_offset_right_finite_structuretablesaddpointvalueoperationresultcongruence. ((pft_row_finite_structuretablesaddpointvalue) + (pft_column_finite_structuretablesaddpointvalue)) + (p) * pfa_offset_left_finite_structuretablesaddpointvalueoperationresultcongruence = (pft_value_finite_structuretablesadd) + (p) * pfa_offset_right_finite_structuretablesaddpointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_finite_structuretablesmultiply. (exists pfa_gap_finite_structuretablesmultiplyprefix. pfa_gap_finite_structuretablesmultiplyprefix + S (pft_index_finite_structuretablesmultiply) = ((p) * (p))) -> exists pft_value_finite_structuretablesmultiply. (((((exists ff_h_pft_finite_structuretablesmultiplypointentry. ff_h_pft_finite_structuretablesmultiplypointentry + S (pft_value_finite_structuretablesmultiply) = S ((S (pft_index_finite_structuretablesmultiply)) * mc)) /\ exists ff_q_pft_finite_structuretablesmultiplypointentry. mb = ff_q_pft_finite_structuretablesmultiplypointentry * S ((S (pft_index_finite_structuretablesmultiply)) * mc) + (pft_value_finite_structuretablesmultiply))) /\ ((exists pft_row_finite_structuretablesmultiplypointvalue pft_column_finite_structuretablesmultiplypointvalue. (((pft_index_finite_structuretablesmultiply) = pft_row_finite_structuretablesmultiplypointvalue * (p) + pft_column_finite_structuretablesmultiplypointvalue) /\ ((((exists pfa_gap_finite_structuretablesmultiplypointvalueoperationleft. pfa_gap_finite_structuretablesmultiplypointvalueoperationleft + S (pft_row_finite_structuretablesmultiplypointvalue) = (p)) /\ (((exists pfa_gap_finite_structuretablesmultiplypointvalueoperationright. pfa_gap_finite_structuretablesmultiplypointvalueoperationright + S (pft_column_finite_structuretablesmultiplypointvalue) = (p)) /\ ((((exists pfa_gap_finite_structuretablesmultiplypointvalueoperationresultbound. pfa_gap_finite_structuretablesmultiplypointvalueoperationresultbound + S (pft_value_finite_structuretablesmultiply) = (p)) /\ ((exists pfa_offset_left_finite_structuretablesmultiplypointvalueoperationresultcongruence pfa_offset_right_finite_structuretablesmultiplypointvalueoperationresultcongruence. ((pft_row_finite_structuretablesmultiplypointvalue) * (pft_column_finite_structuretablesmultiplypointvalue)) + (p) * pfa_offset_left_finite_structuretablesmultiplypointvalueoperationresultcongruence = (pft_value_finite_structuretablesmultiply) + (p) * pfa_offset_right_finite_structuretablesmultiplypointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_finite_structuretablesnegate. (exists pfa_gap_finite_structuretablesnegateprefix. pfa_gap_finite_structuretablesnegateprefix + S (pft_index_finite_structuretablesnegate) = (p)) -> exists pft_value_finite_structuretablesnegate. (((((exists ff_h_pft_finite_structuretablesnegatepointentry. ff_h_pft_finite_structuretablesnegatepointentry + S (pft_value_finite_structuretablesnegate) = S ((S (pft_index_finite_structuretablesnegate)) * nc)) /\ exists ff_q_pft_finite_structuretablesnegatepointentry. nb = ff_q_pft_finite_structuretablesnegatepointentry * S ((S (pft_index_finite_structuretablesnegate)) * nc) + (pft_value_finite_structuretablesnegate))) /\ ((((exists pfa_gap_finite_structuretablesnegatepointvalueadditionleft. pfa_gap_finite_structuretablesnegatepointvalueadditionleft + S (pft_index_finite_structuretablesnegate) = (p)) /\ (((exists pfa_gap_finite_structuretablesnegatepointvalueadditionright. pfa_gap_finite_structuretablesnegatepointvalueadditionright + S (pft_value_finite_structuretablesnegate) = (p)) /\ ((((exists pfa_gap_finite_structuretablesnegatepointvalueadditionresultbound. pfa_gap_finite_structuretablesnegatepointvalueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_finite_structuretablesnegatepointvalueadditionresultcongruence pfa_offset_right_finite_structuretablesnegatepointvalueadditionresultcongruence. ((pft_index_finite_structuretablesnegate) + (pft_value_finite_structuretablesnegate)) + (p) * pfa_offset_left_finite_structuretablesnegatepointvalueadditionresultcongruence = (0) + (p) * pfa_offset_right_finite_structuretablesnegatepointvalueadditionresultcongruence))))))))))))) /\ ((forall pft_index_finite_structuretablesinverse. (exists pfa_gap_finite_structuretablesinverseprefix. pfa_gap_finite_structuretablesinverseprefix + S (pft_index_finite_structuretablesinverse) = (p)) -> exists pft_value_finite_structuretablesinverse. (((((exists ff_h_pft_finite_structuretablesinversepointentry. ff_h_pft_finite_structuretablesinversepointentry + S (pft_value_finite_structuretablesinverse) = S ((S (pft_index_finite_structuretablesinverse)) * ic)) /\ exists ff_q_pft_finite_structuretablesinversepointentry. ib = ff_q_pft_finite_structuretablesinversepointentry * S ((S (pft_index_finite_structuretablesinverse)) * ic) + (pft_value_finite_structuretablesinverse))) /\ ((((exists pfa_gap_finite_structuretablesinversepointvalueinput. pfa_gap_finite_structuretablesinversepointvalueinput + S (pft_index_finite_structuretablesinverse) = (p)) /\ (((exists pfa_gap_finite_structuretablesinversepointvalueoutput. pfa_gap_finite_structuretablesinversepointvalueoutput + S (pft_value_finite_structuretablesinverse) = (p)) /\ ((((pft_index_finite_structuretablesinverse) = 0 /\ (pft_value_finite_structuretablesinverse) = 0) \/ (((~((pft_index_finite_structuretablesinverse) = 0)) /\ ((((exists pfa_gap_finite_structuretablesinversepointvaluenonzeromultiplicationleft. pfa_gap_finite_structuretablesinversepointvaluenonzeromultiplicationleft + S (pft_index_finite_structuretablesinverse) = (p)) /\ (((exists pfa_gap_finite_structuretablesinversepointvaluenonzeromultiplicationright. pfa_gap_finite_structuretablesinversepointvaluenonzeromultiplicationright + S (pft_value_finite_structuretablesinverse) = (p)) /\ ((((exists pfa_gap_finite_structuretablesinversepointvaluenonzeromultiplicationresultbound. pfa_gap_finite_structuretablesinversepointvaluenonzeromultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_finite_structuretablesinversepointvaluenonzeromultiplicationresultcongruence pfa_offset_right_finite_structuretablesinversepointvaluenonzeromultiplicationresultcongruence. ((pft_index_finite_structuretablesinverse) * (pft_value_finite_structuretablesinverse)) + (p) * pfa_offset_left_finite_structuretablesinversepointvaluenonzeromultiplicationresultcongruence = (1) + (p) * pfa_offset_right_finite_structuretablesinversepointvaluenonzeromultiplicationresultcongruence))))))))))))))))))))))))))))) /\ (((((forall pff_enumeration_index_finite_structurecardinalityenumeration. (exists pfa_gap_finite_structurecardinalityenumerationbound. pfa_gap_finite_structurecardinalityenumerationbound + S (pff_enumeration_index_finite_structurecardinalityenumeration) = (p)) -> (((exists ff_h_pft_finite_structurecardinalityenumerationentry. ff_h_pft_finite_structurecardinalityenumerationentry + S (pff_enumeration_index_finite_structurecardinalityenumeration) = S ((S (pff_enumeration_index_finite_structurecardinalityenumeration)) * ec)) /\ exists ff_q_pft_finite_structurecardinalityenumerationentry. eb = ff_q_pft_finite_structurecardinalityenumerationentry * S ((S (pff_enumeration_index_finite_structurecardinalityenumeration)) * ec) + (pff_enumeration_index_finite_structurecardinalityenumeration)))) /\ (((forall pff_cardinality_i_finite_structurecardinality pff_cardinality_a_finite_structurecardinality. (exists pfa_gap_finite_structurecardinalitybounded_index. pfa_gap_finite_structurecardinalitybounded_index + S (pff_cardinality_i_finite_structurecardinality) = (p)) -> (((exists ff_h_pft_finite_structurecardinalitybounded_entry. ff_h_pft_finite_structurecardinalitybounded_entry + S (pff_cardinality_a_finite_structurecardinality) = S ((S (pff_cardinality_i_finite_structurecardinality)) * ec)) /\ exists ff_q_pft_finite_structurecardinalitybounded_entry. eb = ff_q_pft_finite_structurecardinalitybounded_entry * S ((S (pff_cardinality_i_finite_structurecardinality)) * ec) + (pff_cardinality_a_finite_structurecardinality))) -> (exists pfa_gap_finite_structurecardinalitybounded_value. pfa_gap_finite_structurecardinalitybounded_value + S (pff_cardinality_a_finite_structurecardinality) = (p))) /\ (((forall pff_cardinality_i_finite_structurecardinality pff_cardinality_j_finite_structurecardinality pff_cardinality_a_finite_structurecardinality. (exists pfa_gap_finite_structurecardinalityinjective_i. pfa_gap_finite_structurecardinalityinjective_i + S (pff_cardinality_i_finite_structurecardinality) = (p)) -> (exists pfa_gap_finite_structurecardinalityinjective_j. pfa_gap_finite_structurecardinalityinjective_j + S (pff_cardinality_j_finite_structurecardinality) = (p)) -> (((exists ff_h_pft_finite_structurecardinalityinjective_first. ff_h_pft_finite_structurecardinalityinjective_first + S (pff_cardinality_a_finite_structurecardinality) = S ((S (pff_cardinality_i_finite_structurecardinality)) * ec)) /\ exists ff_q_pft_finite_structurecardinalityinjective_first. eb = ff_q_pft_finite_structurecardinalityinjective_first * S ((S (pff_cardinality_i_finite_structurecardinality)) * ec) + (pff_cardinality_a_finite_structurecardinality))) -> (((exists ff_h_pft_finite_structurecardinalityinjective_second. ff_h_pft_finite_structurecardinalityinjective_second + S (pff_cardinality_a_finite_structurecardinality) = S ((S (pff_cardinality_j_finite_structurecardinality)) * ec)) /\ exists ff_q_pft_finite_structurecardinalityinjective_second. eb = ff_q_pft_finite_structurecardinalityinjective_second * S ((S (pff_cardinality_j_finite_structurecardinality)) * ec) + (pff_cardinality_a_finite_structurecardinality))) -> pff_cardinality_i_finite_structurecardinality = pff_cardinality_j_finite_structurecardinality) /\ ((forall pff_cardinality_a_finite_structurecardinality. (exists pfa_gap_finite_structurecardinalitysurjective_value. pfa_gap_finite_structurecardinalitysurjective_value + S (pff_cardinality_a_finite_structurecardinality) = (p)) -> exists pff_cardinality_i_finite_structurecardinality. (exists pfa_gap_finite_structurecardinalitysurjective_index. pfa_gap_finite_structurecardinalitysurjective_index + S (pff_cardinality_i_finite_structurecardinality) = (p)) /\ (((exists ff_h_pft_finite_structurecardinalitysurjective_entry. ff_h_pft_finite_structurecardinalitysurjective_entry + S (pff_cardinality_a_finite_structurecardinality) = S ((S (pff_cardinality_i_finite_structurecardinality)) * ec)) /\ exists ff_q_pft_finite_structurecardinalitysurjective_entry. eb = ff_q_pft_finite_structurecardinalitysurjective_entry * S ((S (pff_cardinality_i_finite_structurecardinality)) * ec) + (pff_cardinality_a_finite_structurecardinality))))))))))) /\ (((((exists pfa_gap_finite_structurelawszero. pfa_gap_finite_structurelawszero + S (0) = (p)) /\ (((exists pfa_gap_finite_structurelawsone. pfa_gap_finite_structurelawsone + S (1) = (p)) /\ (((~(0 = 1)) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws. (exists pfa_gap_finite_structurelawsaddleft. pfa_gap_finite_structurelawsaddleft + S (pfa_law_a_finite_structurelaws) = (p)) -> (exists pfa_gap_finite_structurelawsaddright. pfa_gap_finite_structurelawsaddright + S (pfa_law_b_finite_structurelaws) = (p)) -> exists pfa_law_c_finite_structurelaws. (((exists pfa_gap_finite_structurelawsaddchosenleft. pfa_gap_finite_structurelawsaddchosenleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddchosenright. pfa_gap_finite_structurelawsaddchosenright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddchosenresultbound. pfa_gap_finite_structurelawsaddchosenresultbound + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddchosenresultcongruence pfa_offset_right_finite_structurelawsaddchosenresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddchosenresultcongruence = (pfa_law_c_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddchosenresultcongruence))))))))) /\ forall pfa_law_d_finite_structurelaws. (((exists pfa_gap_finite_structurelawsaddotherleft. pfa_gap_finite_structurelawsaddotherleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddotherright. pfa_gap_finite_structurelawsaddotherright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddotherresultbound. pfa_gap_finite_structurelawsaddotherresultbound + S (pfa_law_d_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddotherresultcongruence pfa_offset_right_finite_structurelawsaddotherresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddotherresultcongruence = (pfa_law_d_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddotherresultcongruence))))))))) -> pfa_law_d_finite_structurelaws = pfa_law_c_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws pfa_law_c_finite_structurelaws. (((exists pfa_gap_finite_structurelawsaddcomm_firstleft. pfa_gap_finite_structurelawsaddcomm_firstleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddcomm_firstright. pfa_gap_finite_structurelawsaddcomm_firstright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddcomm_firstresultbound. pfa_gap_finite_structurelawsaddcomm_firstresultbound + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddcomm_firstresultcongruence pfa_offset_right_finite_structurelawsaddcomm_firstresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddcomm_firstresultcongruence = (pfa_law_c_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddcomm_firstresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsaddcomm_secondleft. pfa_gap_finite_structurelawsaddcomm_secondleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddcomm_secondright. pfa_gap_finite_structurelawsaddcomm_secondright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddcomm_secondresultbound. pfa_gap_finite_structurelawsaddcomm_secondresultbound + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddcomm_secondresultcongruence pfa_offset_right_finite_structurelawsaddcomm_secondresultcongruence. ((pfa_law_b_finite_structurelaws) + (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddcomm_secondresultcongruence = (pfa_law_c_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddcomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws pfa_law_c_finite_structurelaws pfa_law_x_finite_structurelaws pfa_law_y_finite_structurelaws pfa_law_u_finite_structurelaws pfa_law_v_finite_structurelaws. (((exists pfa_gap_finite_structurelawsaddassoc_firstleft. pfa_gap_finite_structurelawsaddassoc_firstleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddassoc_firstright. pfa_gap_finite_structurelawsaddassoc_firstright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddassoc_firstresultbound. pfa_gap_finite_structurelawsaddassoc_firstresultbound + S (pfa_law_x_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddassoc_firstresultcongruence pfa_offset_right_finite_structurelawsaddassoc_firstresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddassoc_firstresultcongruence = (pfa_law_x_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsaddassoc_leftleft. pfa_gap_finite_structurelawsaddassoc_leftleft + S (pfa_law_x_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddassoc_leftright. pfa_gap_finite_structurelawsaddassoc_leftright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddassoc_leftresultbound. pfa_gap_finite_structurelawsaddassoc_leftresultbound + S (pfa_law_u_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddassoc_leftresultcongruence pfa_offset_right_finite_structurelawsaddassoc_leftresultcongruence. ((pfa_law_x_finite_structurelaws) + (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddassoc_leftresultcongruence = (pfa_law_u_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsaddassoc_secondleft. pfa_gap_finite_structurelawsaddassoc_secondleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddassoc_secondright. pfa_gap_finite_structurelawsaddassoc_secondright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddassoc_secondresultbound. pfa_gap_finite_structurelawsaddassoc_secondresultbound + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddassoc_secondresultcongruence pfa_offset_right_finite_structurelawsaddassoc_secondresultcongruence. ((pfa_law_b_finite_structurelaws) + (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddassoc_secondresultcongruence = (pfa_law_y_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsaddassoc_rightleft. pfa_gap_finite_structurelawsaddassoc_rightleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsaddassoc_rightright. pfa_gap_finite_structurelawsaddassoc_rightright + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsaddassoc_rightresultbound. pfa_gap_finite_structurelawsaddassoc_rightresultbound + S (pfa_law_v_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsaddassoc_rightresultcongruence pfa_offset_right_finite_structurelawsaddassoc_rightresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_y_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsaddassoc_rightresultcongruence = (pfa_law_v_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsaddassoc_rightresultcongruence))))))))) -> pfa_law_u_finite_structurelaws = pfa_law_v_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws. (exists pfa_gap_finite_structurelawsmultiplyleft. pfa_gap_finite_structurelawsmultiplyleft + S (pfa_law_a_finite_structurelaws) = (p)) -> (exists pfa_gap_finite_structurelawsmultiplyright. pfa_gap_finite_structurelawsmultiplyright + S (pfa_law_b_finite_structurelaws) = (p)) -> exists pfa_law_c_finite_structurelaws. (((exists pfa_gap_finite_structurelawsmultiplychosenleft. pfa_gap_finite_structurelawsmultiplychosenleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplychosenright. pfa_gap_finite_structurelawsmultiplychosenright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplychosenresultbound. pfa_gap_finite_structurelawsmultiplychosenresultbound + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplychosenresultcongruence pfa_offset_right_finite_structurelawsmultiplychosenresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplychosenresultcongruence = (pfa_law_c_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplychosenresultcongruence))))))))) /\ forall pfa_law_d_finite_structurelaws. (((exists pfa_gap_finite_structurelawsmultiplyotherleft. pfa_gap_finite_structurelawsmultiplyotherleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplyotherright. pfa_gap_finite_structurelawsmultiplyotherright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplyotherresultbound. pfa_gap_finite_structurelawsmultiplyotherresultbound + S (pfa_law_d_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplyotherresultcongruence pfa_offset_right_finite_structurelawsmultiplyotherresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplyotherresultcongruence = (pfa_law_d_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplyotherresultcongruence))))))))) -> pfa_law_d_finite_structurelaws = pfa_law_c_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws pfa_law_c_finite_structurelaws. (((exists pfa_gap_finite_structurelawsmultiplycomm_firstleft. pfa_gap_finite_structurelawsmultiplycomm_firstleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplycomm_firstright. pfa_gap_finite_structurelawsmultiplycomm_firstright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplycomm_firstresultbound. pfa_gap_finite_structurelawsmultiplycomm_firstresultbound + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplycomm_firstresultcongruence pfa_offset_right_finite_structurelawsmultiplycomm_firstresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplycomm_firstresultcongruence = (pfa_law_c_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplycomm_firstresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsmultiplycomm_secondleft. pfa_gap_finite_structurelawsmultiplycomm_secondleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplycomm_secondright. pfa_gap_finite_structurelawsmultiplycomm_secondright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplycomm_secondresultbound. pfa_gap_finite_structurelawsmultiplycomm_secondresultbound + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplycomm_secondresultcongruence pfa_offset_right_finite_structurelawsmultiplycomm_secondresultcongruence. ((pfa_law_b_finite_structurelaws) * (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplycomm_secondresultcongruence = (pfa_law_c_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplycomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws pfa_law_c_finite_structurelaws pfa_law_x_finite_structurelaws pfa_law_y_finite_structurelaws pfa_law_u_finite_structurelaws pfa_law_v_finite_structurelaws. (((exists pfa_gap_finite_structurelawsmultiplyassoc_firstleft. pfa_gap_finite_structurelawsmultiplyassoc_firstleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplyassoc_firstright. pfa_gap_finite_structurelawsmultiplyassoc_firstright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplyassoc_firstresultbound. pfa_gap_finite_structurelawsmultiplyassoc_firstresultbound + S (pfa_law_x_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplyassoc_firstresultcongruence pfa_offset_right_finite_structurelawsmultiplyassoc_firstresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplyassoc_firstresultcongruence = (pfa_law_x_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplyassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsmultiplyassoc_leftleft. pfa_gap_finite_structurelawsmultiplyassoc_leftleft + S (pfa_law_x_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplyassoc_leftright. pfa_gap_finite_structurelawsmultiplyassoc_leftright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplyassoc_leftresultbound. pfa_gap_finite_structurelawsmultiplyassoc_leftresultbound + S (pfa_law_u_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplyassoc_leftresultcongruence pfa_offset_right_finite_structurelawsmultiplyassoc_leftresultcongruence. ((pfa_law_x_finite_structurelaws) * (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplyassoc_leftresultcongruence = (pfa_law_u_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplyassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsmultiplyassoc_secondleft. pfa_gap_finite_structurelawsmultiplyassoc_secondleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplyassoc_secondright. pfa_gap_finite_structurelawsmultiplyassoc_secondright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplyassoc_secondresultbound. pfa_gap_finite_structurelawsmultiplyassoc_secondresultbound + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplyassoc_secondresultcongruence pfa_offset_right_finite_structurelawsmultiplyassoc_secondresultcongruence. ((pfa_law_b_finite_structurelaws) * (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplyassoc_secondresultcongruence = (pfa_law_y_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplyassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsmultiplyassoc_rightleft. pfa_gap_finite_structurelawsmultiplyassoc_rightleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiplyassoc_rightright. pfa_gap_finite_structurelawsmultiplyassoc_rightright + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiplyassoc_rightresultbound. pfa_gap_finite_structurelawsmultiplyassoc_rightresultbound + S (pfa_law_v_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiplyassoc_rightresultcongruence pfa_offset_right_finite_structurelawsmultiplyassoc_rightresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_y_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiplyassoc_rightresultcongruence = (pfa_law_v_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiplyassoc_rightresultcongruence))))))))) -> pfa_law_u_finite_structurelaws = pfa_law_v_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws pfa_law_c_finite_structurelaws pfa_law_s_finite_structurelaws pfa_law_x_finite_structurelaws pfa_law_y_finite_structurelaws pfa_law_u_finite_structurelaws pfa_law_v_finite_structurelaws. (((exists pfa_gap_finite_structurelawsleftdistribution_sumleft. pfa_gap_finite_structurelawsleftdistribution_sumleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsleftdistribution_sumright. pfa_gap_finite_structurelawsleftdistribution_sumright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsleftdistribution_sumresultbound. pfa_gap_finite_structurelawsleftdistribution_sumresultbound + S (pfa_law_s_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsleftdistribution_sumresultcongruence pfa_offset_right_finite_structurelawsleftdistribution_sumresultcongruence. ((pfa_law_b_finite_structurelaws) + (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsleftdistribution_sumresultcongruence = (pfa_law_s_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsleftdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsleftdistribution_leftleft. pfa_gap_finite_structurelawsleftdistribution_leftleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsleftdistribution_leftright. pfa_gap_finite_structurelawsleftdistribution_leftright + S (pfa_law_s_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsleftdistribution_leftresultbound. pfa_gap_finite_structurelawsleftdistribution_leftresultbound + S (pfa_law_u_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsleftdistribution_leftresultcongruence pfa_offset_right_finite_structurelawsleftdistribution_leftresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_s_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsleftdistribution_leftresultcongruence = (pfa_law_u_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsleftdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsleftdistribution_firstleft. pfa_gap_finite_structurelawsleftdistribution_firstleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsleftdistribution_firstright. pfa_gap_finite_structurelawsleftdistribution_firstright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsleftdistribution_firstresultbound. pfa_gap_finite_structurelawsleftdistribution_firstresultbound + S (pfa_law_x_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsleftdistribution_firstresultcongruence pfa_offset_right_finite_structurelawsleftdistribution_firstresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsleftdistribution_firstresultcongruence = (pfa_law_x_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsleftdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsleftdistribution_secondleft. pfa_gap_finite_structurelawsleftdistribution_secondleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsleftdistribution_secondright. pfa_gap_finite_structurelawsleftdistribution_secondright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsleftdistribution_secondresultbound. pfa_gap_finite_structurelawsleftdistribution_secondresultbound + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsleftdistribution_secondresultcongruence pfa_offset_right_finite_structurelawsleftdistribution_secondresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsleftdistribution_secondresultcongruence = (pfa_law_y_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsleftdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsleftdistribution_rightleft. pfa_gap_finite_structurelawsleftdistribution_rightleft + S (pfa_law_x_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsleftdistribution_rightright. pfa_gap_finite_structurelawsleftdistribution_rightright + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsleftdistribution_rightresultbound. pfa_gap_finite_structurelawsleftdistribution_rightresultbound + S (pfa_law_v_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsleftdistribution_rightresultcongruence pfa_offset_right_finite_structurelawsleftdistribution_rightresultcongruence. ((pfa_law_x_finite_structurelaws) + (pfa_law_y_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsleftdistribution_rightresultcongruence = (pfa_law_v_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsleftdistribution_rightresultcongruence))))))))) -> pfa_law_u_finite_structurelaws = pfa_law_v_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws pfa_law_c_finite_structurelaws pfa_law_s_finite_structurelaws pfa_law_x_finite_structurelaws pfa_law_y_finite_structurelaws pfa_law_u_finite_structurelaws pfa_law_v_finite_structurelaws. (((exists pfa_gap_finite_structurelawsrightdistribution_sumleft. pfa_gap_finite_structurelawsrightdistribution_sumleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsrightdistribution_sumright. pfa_gap_finite_structurelawsrightdistribution_sumright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsrightdistribution_sumresultbound. pfa_gap_finite_structurelawsrightdistribution_sumresultbound + S (pfa_law_s_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsrightdistribution_sumresultcongruence pfa_offset_right_finite_structurelawsrightdistribution_sumresultcongruence. ((pfa_law_b_finite_structurelaws) + (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsrightdistribution_sumresultcongruence = (pfa_law_s_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsrightdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsrightdistribution_leftleft. pfa_gap_finite_structurelawsrightdistribution_leftleft + S (pfa_law_s_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsrightdistribution_leftright. pfa_gap_finite_structurelawsrightdistribution_leftright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsrightdistribution_leftresultbound. pfa_gap_finite_structurelawsrightdistribution_leftresultbound + S (pfa_law_u_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsrightdistribution_leftresultcongruence pfa_offset_right_finite_structurelawsrightdistribution_leftresultcongruence. ((pfa_law_s_finite_structurelaws) * (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsrightdistribution_leftresultcongruence = (pfa_law_u_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsrightdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsrightdistribution_firstleft. pfa_gap_finite_structurelawsrightdistribution_firstleft + S (pfa_law_b_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsrightdistribution_firstright. pfa_gap_finite_structurelawsrightdistribution_firstright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsrightdistribution_firstresultbound. pfa_gap_finite_structurelawsrightdistribution_firstresultbound + S (pfa_law_x_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsrightdistribution_firstresultcongruence pfa_offset_right_finite_structurelawsrightdistribution_firstresultcongruence. ((pfa_law_b_finite_structurelaws) * (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsrightdistribution_firstresultcongruence = (pfa_law_x_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsrightdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsrightdistribution_secondleft. pfa_gap_finite_structurelawsrightdistribution_secondleft + S (pfa_law_c_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsrightdistribution_secondright. pfa_gap_finite_structurelawsrightdistribution_secondright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsrightdistribution_secondresultbound. pfa_gap_finite_structurelawsrightdistribution_secondresultbound + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsrightdistribution_secondresultcongruence pfa_offset_right_finite_structurelawsrightdistribution_secondresultcongruence. ((pfa_law_c_finite_structurelaws) * (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsrightdistribution_secondresultcongruence = (pfa_law_y_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsrightdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_finite_structurelawsrightdistribution_rightleft. pfa_gap_finite_structurelawsrightdistribution_rightleft + S (pfa_law_x_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsrightdistribution_rightright. pfa_gap_finite_structurelawsrightdistribution_rightright + S (pfa_law_y_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsrightdistribution_rightresultbound. pfa_gap_finite_structurelawsrightdistribution_rightresultbound + S (pfa_law_v_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsrightdistribution_rightresultcongruence pfa_offset_right_finite_structurelawsrightdistribution_rightresultcongruence. ((pfa_law_x_finite_structurelaws) + (pfa_law_y_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsrightdistribution_rightresultcongruence = (pfa_law_v_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsrightdistribution_rightresultcongruence))))))))) -> pfa_law_u_finite_structurelaws = pfa_law_v_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsadd_zero_rightinput. pfa_gap_finite_structurelawsadd_zero_rightinput + S (pfa_law_a_finite_structurelaws) = (p)) -> (((exists pfa_gap_finite_structurelawsadd_zero_rightleft. pfa_gap_finite_structurelawsadd_zero_rightleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsadd_zero_rightright. pfa_gap_finite_structurelawsadd_zero_rightright + S (0) = (p)) /\ ((((exists pfa_gap_finite_structurelawsadd_zero_rightresultbound. pfa_gap_finite_structurelawsadd_zero_rightresultbound + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsadd_zero_rightresultcongruence pfa_offset_right_finite_structurelawsadd_zero_rightresultcongruence. ((pfa_law_a_finite_structurelaws) + (0)) + (p) * pfa_offset_left_finite_structurelawsadd_zero_rightresultcongruence = (pfa_law_a_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsadd_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsadd_zero_leftinput. pfa_gap_finite_structurelawsadd_zero_leftinput + S (pfa_law_a_finite_structurelaws) = (p)) -> (((exists pfa_gap_finite_structurelawsadd_zero_leftleft. pfa_gap_finite_structurelawsadd_zero_leftleft + S (0) = (p)) /\ (((exists pfa_gap_finite_structurelawsadd_zero_leftright. pfa_gap_finite_structurelawsadd_zero_leftright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsadd_zero_leftresultbound. pfa_gap_finite_structurelawsadd_zero_leftresultbound + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsadd_zero_leftresultcongruence pfa_offset_right_finite_structurelawsadd_zero_leftresultcongruence. ((0) + (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsadd_zero_leftresultcongruence = (pfa_law_a_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsadd_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsmultiply_one_rightinput. pfa_gap_finite_structurelawsmultiply_one_rightinput + S (pfa_law_a_finite_structurelaws) = (p)) -> (((exists pfa_gap_finite_structurelawsmultiply_one_rightleft. pfa_gap_finite_structurelawsmultiply_one_rightleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiply_one_rightright. pfa_gap_finite_structurelawsmultiply_one_rightright + S (1) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiply_one_rightresultbound. pfa_gap_finite_structurelawsmultiply_one_rightresultbound + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiply_one_rightresultcongruence pfa_offset_right_finite_structurelawsmultiply_one_rightresultcongruence. ((pfa_law_a_finite_structurelaws) * (1)) + (p) * pfa_offset_left_finite_structurelawsmultiply_one_rightresultcongruence = (pfa_law_a_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiply_one_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsmultiply_one_leftinput. pfa_gap_finite_structurelawsmultiply_one_leftinput + S (pfa_law_a_finite_structurelaws) = (p)) -> (((exists pfa_gap_finite_structurelawsmultiply_one_leftleft. pfa_gap_finite_structurelawsmultiply_one_leftleft + S (1) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiply_one_leftright. pfa_gap_finite_structurelawsmultiply_one_leftright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiply_one_leftresultbound. pfa_gap_finite_structurelawsmultiply_one_leftresultbound + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiply_one_leftresultcongruence pfa_offset_right_finite_structurelawsmultiply_one_leftresultcongruence. ((1) * (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiply_one_leftresultcongruence = (pfa_law_a_finite_structurelaws) + (p) * pfa_offset_right_finite_structurelawsmultiply_one_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsmultiply_zero_rightinput. pfa_gap_finite_structurelawsmultiply_zero_rightinput + S (pfa_law_a_finite_structurelaws) = (p)) -> (((exists pfa_gap_finite_structurelawsmultiply_zero_rightleft. pfa_gap_finite_structurelawsmultiply_zero_rightleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiply_zero_rightright. pfa_gap_finite_structurelawsmultiply_zero_rightright + S (0) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiply_zero_rightresultbound. pfa_gap_finite_structurelawsmultiply_zero_rightresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiply_zero_rightresultcongruence pfa_offset_right_finite_structurelawsmultiply_zero_rightresultcongruence. ((pfa_law_a_finite_structurelaws) * (0)) + (p) * pfa_offset_left_finite_structurelawsmultiply_zero_rightresultcongruence = (0) + (p) * pfa_offset_right_finite_structurelawsmultiply_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsmultiply_zero_leftinput. pfa_gap_finite_structurelawsmultiply_zero_leftinput + S (pfa_law_a_finite_structurelaws) = (p)) -> (((exists pfa_gap_finite_structurelawsmultiply_zero_leftleft. pfa_gap_finite_structurelawsmultiply_zero_leftleft + S (0) = (p)) /\ (((exists pfa_gap_finite_structurelawsmultiply_zero_leftright. pfa_gap_finite_structurelawsmultiply_zero_leftright + S (pfa_law_a_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsmultiply_zero_leftresultbound. pfa_gap_finite_structurelawsmultiply_zero_leftresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsmultiply_zero_leftresultcongruence pfa_offset_right_finite_structurelawsmultiply_zero_leftresultcongruence. ((0) * (pfa_law_a_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsmultiply_zero_leftresultcongruence = (0) + (p) * pfa_offset_right_finite_structurelawsmultiply_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsnegateinput. pfa_gap_finite_structurelawsnegateinput + S (pfa_law_a_finite_structurelaws) = (p)) -> exists pfa_law_b_finite_structurelaws. (((exists pfa_gap_finite_structurelawsnegatechosenadditionleft. pfa_gap_finite_structurelawsnegatechosenadditionleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsnegatechosenadditionright. pfa_gap_finite_structurelawsnegatechosenadditionright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsnegatechosenadditionresultbound. pfa_gap_finite_structurelawsnegatechosenadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsnegatechosenadditionresultcongruence pfa_offset_right_finite_structurelawsnegatechosenadditionresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsnegatechosenadditionresultcongruence = (0) + (p) * pfa_offset_right_finite_structurelawsnegatechosenadditionresultcongruence))))))))) /\ forall pfa_law_c_finite_structurelaws. (((exists pfa_gap_finite_structurelawsnegateotheradditionleft. pfa_gap_finite_structurelawsnegateotheradditionleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsnegateotheradditionright. pfa_gap_finite_structurelawsnegateotheradditionright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsnegateotheradditionresultbound. pfa_gap_finite_structurelawsnegateotheradditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsnegateotheradditionresultcongruence pfa_offset_right_finite_structurelawsnegateotheradditionresultcongruence. ((pfa_law_a_finite_structurelaws) + (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsnegateotheradditionresultcongruence = (0) + (p) * pfa_offset_right_finite_structurelawsnegateotheradditionresultcongruence))))))))) -> pfa_law_c_finite_structurelaws = pfa_law_b_finite_structurelaws) /\ (((forall pfa_law_a_finite_structurelaws. (exists pfa_gap_finite_structurelawsinverseinput. pfa_gap_finite_structurelawsinverseinput + S (pfa_law_a_finite_structurelaws) = (p)) -> ~(pfa_law_a_finite_structurelaws = 0) -> exists pfa_law_b_finite_structurelaws. (((~((pfa_law_a_finite_structurelaws) = 0)) /\ ((((exists pfa_gap_finite_structurelawsinversechosenmultiplicationleft. pfa_gap_finite_structurelawsinversechosenmultiplicationleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsinversechosenmultiplicationright. pfa_gap_finite_structurelawsinversechosenmultiplicationright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsinversechosenmultiplicationresultbound. pfa_gap_finite_structurelawsinversechosenmultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsinversechosenmultiplicationresultcongruence pfa_offset_right_finite_structurelawsinversechosenmultiplicationresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsinversechosenmultiplicationresultcongruence = (1) + (p) * pfa_offset_right_finite_structurelawsinversechosenmultiplicationresultcongruence)))))))))))) /\ forall pfa_law_c_finite_structurelaws. (((~((pfa_law_a_finite_structurelaws) = 0)) /\ ((((exists pfa_gap_finite_structurelawsinverseothermultiplicationleft. pfa_gap_finite_structurelawsinverseothermultiplicationleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsinverseothermultiplicationright. pfa_gap_finite_structurelawsinverseothermultiplicationright + S (pfa_law_c_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsinverseothermultiplicationresultbound. pfa_gap_finite_structurelawsinverseothermultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsinverseothermultiplicationresultcongruence pfa_offset_right_finite_structurelawsinverseothermultiplicationresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_c_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsinverseothermultiplicationresultcongruence = (1) + (p) * pfa_offset_right_finite_structurelawsinverseothermultiplicationresultcongruence)))))))))))) -> pfa_law_c_finite_structurelaws = pfa_law_b_finite_structurelaws) /\ ((forall pfa_law_a_finite_structurelaws pfa_law_b_finite_structurelaws. (((exists pfa_gap_finite_structurelawsnozeroleft. pfa_gap_finite_structurelawsnozeroleft + S (pfa_law_a_finite_structurelaws) = (p)) /\ (((exists pfa_gap_finite_structurelawsnozeroright. pfa_gap_finite_structurelawsnozeroright + S (pfa_law_b_finite_structurelaws) = (p)) /\ ((((exists pfa_gap_finite_structurelawsnozeroresultbound. pfa_gap_finite_structurelawsnozeroresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_finite_structurelawsnozeroresultcongruence pfa_offset_right_finite_structurelawsnozeroresultcongruence. ((pfa_law_a_finite_structurelaws) * (pfa_law_b_finite_structurelaws)) + (p) * pfa_offset_left_finite_structurelawsnozeroresultcongruence = (0) + (p) * pfa_offset_right_finite_structurelawsnozeroresultcongruence))))))))) -> pfa_law_a_finite_structurelaws = 0 \/ pfa_law_b_finite_structurelaws = 0)))))))))))))))))))))))))))))))))))))))) /\ ((((exists pff_history_code_finite_structurecharacteristicmodulus pff_history_scale_finite_structurecharacteristicmodulus. (((((exists ff_h_pft_finite_structurecharacteristicmodulushistorystart. ff_h_pft_finite_structurecharacteristicmodulushistorystart + S (0) = S ((S (0)) * pff_history_scale_finite_structurecharacteristicmodulus)) /\ exists ff_q_pft_finite_structurecharacteristicmodulushistorystart. pff_history_code_finite_structurecharacteristicmodulus = ff_q_pft_finite_structurecharacteristicmodulushistorystart * S ((S (0)) * pff_history_scale_finite_structurecharacteristicmodulus) + (0))) /\ (((((exists ff_h_pft_finite_structurecharacteristicmodulushistoryterminal. ff_h_pft_finite_structurecharacteristicmodulushistoryterminal + S (0) = S ((S (p)) * pff_history_scale_finite_structurecharacteristicmodulus)) /\ exists ff_q_pft_finite_structurecharacteristicmodulushistoryterminal. pff_history_code_finite_structurecharacteristicmodulus = ff_q_pft_finite_structurecharacteristicmodulushistoryterminal * S ((S (p)) * pff_history_scale_finite_structurecharacteristicmodulus) + (0))) /\ ((forall pff_trace_index_finite_structurecharacteristicmodulushistorysteps. (exists pfa_gap_finite_structurecharacteristicmodulushistorystepsindex. pfa_gap_finite_structurecharacteristicmodulushistorystepsindex + S (pff_trace_index_finite_structurecharacteristicmodulushistorysteps) = (p)) -> exists pff_trace_before_finite_structurecharacteristicmodulushistorysteps pff_trace_after_finite_structurecharacteristicmodulushistorysteps. ((((exists ff_h_pft_finite_structurecharacteristicmodulushistorystepsbefore. ff_h_pft_finite_structurecharacteristicmodulushistorystepsbefore + S (pff_trace_before_finite_structurecharacteristicmodulushistorysteps) = S ((S (pff_trace_index_finite_structurecharacteristicmodulushistorysteps)) * pff_history_scale_finite_structurecharacteristicmodulus)) /\ exists ff_q_pft_finite_structurecharacteristicmodulushistorystepsbefore. pff_history_code_finite_structurecharacteristicmodulus = ff_q_pft_finite_structurecharacteristicmodulushistorystepsbefore * S ((S (pff_trace_index_finite_structurecharacteristicmodulushistorysteps)) * pff_history_scale_finite_structurecharacteristicmodulus) + (pff_trace_before_finite_structurecharacteristicmodulushistorysteps))) /\ (((((exists ff_h_pft_finite_structurecharacteristicmodulushistorystepsafter. ff_h_pft_finite_structurecharacteristicmodulushistorystepsafter + S (pff_trace_after_finite_structurecharacteristicmodulushistorysteps) = S ((S (S (pff_trace_index_finite_structurecharacteristicmodulushistorysteps))) * pff_history_scale_finite_structurecharacteristicmodulus)) /\ exists ff_q_pft_finite_structurecharacteristicmodulushistorystepsafter. pff_history_code_finite_structurecharacteristicmodulus = ff_q_pft_finite_structurecharacteristicmodulushistorystepsafter * S ((S (S (pff_trace_index_finite_structurecharacteristicmodulushistorysteps))) * pff_history_scale_finite_structurecharacteristicmodulus) + (pff_trace_after_finite_structurecharacteristicmodulushistorysteps))) /\ ((((exists pfa_gap_finite_structurecharacteristicmodulushistorystepsadditionleft. pfa_gap_finite_structurecharacteristicmodulushistorystepsadditionleft + S (pff_trace_before_finite_structurecharacteristicmodulushistorysteps) = (p)) /\ (((exists pfa_gap_finite_structurecharacteristicmodulushistorystepsadditionright. pfa_gap_finite_structurecharacteristicmodulushistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_finite_structurecharacteristicmodulushistorystepsadditionresultbound. pfa_gap_finite_structurecharacteristicmodulushistorystepsadditionresultbound + S (pff_trace_after_finite_structurecharacteristicmodulushistorysteps) = (p)) /\ ((exists pfa_offset_left_finite_structurecharacteristicmodulushistorystepsadditionresultcongruence pfa_offset_right_finite_structurecharacteristicmodulushistorystepsadditionresultcongruence. ((pff_trace_before_finite_structurecharacteristicmodulushistorysteps) + (1)) + (p) * pfa_offset_left_finite_structurecharacteristicmodulushistorystepsadditionresultcongruence = (pff_trace_after_finite_structurecharacteristicmodulushistorysteps) + (p) * pfa_offset_right_finite_structurecharacteristicmodulushistorystepsadditionresultcongruence)))))))))))))))))))) /\ ((forall pff_smaller_positive_finite_structurecharacteristic. (exists pfa_gap_finite_structurecharacteristicstrict. pfa_gap_finite_structurecharacteristicstrict + S (pff_smaller_positive_finite_structurecharacteristic) = (p)) -> ~(pff_smaller_positive_finite_structurecharacteristic = 0) -> ~(exists pff_history_code_finite_structurecharacteristicsmaller pff_history_scale_finite_structurecharacteristicsmaller. (((((exists ff_h_pft_finite_structurecharacteristicsmallerhistorystart. ff_h_pft_finite_structurecharacteristicsmallerhistorystart + S (0) = S ((S (0)) * pff_history_scale_finite_structurecharacteristicsmaller)) /\ exists ff_q_pft_finite_structurecharacteristicsmallerhistorystart. pff_history_code_finite_structurecharacteristicsmaller = ff_q_pft_finite_structurecharacteristicsmallerhistorystart * S ((S (0)) * pff_history_scale_finite_structurecharacteristicsmaller) + (0))) /\ (((((exists ff_h_pft_finite_structurecharacteristicsmallerhistoryterminal. ff_h_pft_finite_structurecharacteristicsmallerhistoryterminal + S (0) = S ((S (pff_smaller_positive_finite_structurecharacteristic)) * pff_history_scale_finite_structurecharacteristicsmaller)) /\ exists ff_q_pft_finite_structurecharacteristicsmallerhistoryterminal. pff_history_code_finite_structurecharacteristicsmaller = ff_q_pft_finite_structurecharacteristicsmallerhistoryterminal * S ((S (pff_smaller_positive_finite_structurecharacteristic)) * pff_history_scale_finite_structurecharacteristicsmaller) + (0))) /\ ((forall pff_trace_index_finite_structurecharacteristicsmallerhistorysteps. (exists pfa_gap_finite_structurecharacteristicsmallerhistorystepsindex. pfa_gap_finite_structurecharacteristicsmallerhistorystepsindex + S (pff_trace_index_finite_structurecharacteristicsmallerhistorysteps) = (pff_smaller_positive_finite_structurecharacteristic)) -> exists pff_trace_before_finite_structurecharacteristicsmallerhistorysteps pff_trace_after_finite_structurecharacteristicsmallerhistorysteps. ((((exists ff_h_pft_finite_structurecharacteristicsmallerhistorystepsbefore. ff_h_pft_finite_structurecharacteristicsmallerhistorystepsbefore + S (pff_trace_before_finite_structurecharacteristicsmallerhistorysteps) = S ((S (pff_trace_index_finite_structurecharacteristicsmallerhistorysteps)) * pff_history_scale_finite_structurecharacteristicsmaller)) /\ exists ff_q_pft_finite_structurecharacteristicsmallerhistorystepsbefore. pff_history_code_finite_structurecharacteristicsmaller = ff_q_pft_finite_structurecharacteristicsmallerhistorystepsbefore * S ((S (pff_trace_index_finite_structurecharacteristicsmallerhistorysteps)) * pff_history_scale_finite_structurecharacteristicsmaller) + (pff_trace_before_finite_structurecharacteristicsmallerhistorysteps))) /\ (((((exists ff_h_pft_finite_structurecharacteristicsmallerhistorystepsafter. ff_h_pft_finite_structurecharacteristicsmallerhistorystepsafter + S (pff_trace_after_finite_structurecharacteristicsmallerhistorysteps) = S ((S (S (pff_trace_index_finite_structurecharacteristicsmallerhistorysteps))) * pff_history_scale_finite_structurecharacteristicsmaller)) /\ exists ff_q_pft_finite_structurecharacteristicsmallerhistorystepsafter. pff_history_code_finite_structurecharacteristicsmaller = ff_q_pft_finite_structurecharacteristicsmallerhistorystepsafter * S ((S (S (pff_trace_index_finite_structurecharacteristicsmallerhistorysteps))) * pff_history_scale_finite_structurecharacteristicsmaller) + (pff_trace_after_finite_structurecharacteristicsmallerhistorysteps))) /\ ((((exists pfa_gap_finite_structurecharacteristicsmallerhistorystepsadditionleft. pfa_gap_finite_structurecharacteristicsmallerhistorystepsadditionleft + S (pff_trace_before_finite_structurecharacteristicsmallerhistorysteps) = (p)) /\ (((exists pfa_gap_finite_structurecharacteristicsmallerhistorystepsadditionright. pfa_gap_finite_structurecharacteristicsmallerhistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_finite_structurecharacteristicsmallerhistorystepsadditionresultbound. pfa_gap_finite_structurecharacteristicsmallerhistorystepsadditionresultbound + S (pff_trace_after_finite_structurecharacteristicsmallerhistorysteps) = (p)) /\ ((exists pfa_offset_left_finite_structurecharacteristicsmallerhistorystepsadditionresultcongruence pfa_offset_right_finite_structurecharacteristicsmallerhistorystepsadditionresultcongruence. ((pff_trace_before_finite_structurecharacteristicsmallerhistorysteps) + (1)) + (p) * pfa_offset_left_finite_structurecharacteristicsmallerhistorystepsadditionresultcongruence = (pff_trace_after_finite_structurecharacteristicsmallerhistorysteps) + (p) * pfa_offset_right_finite_structurecharacteristicsmallerhistorystepsadditionresultcongruence)))))))))))))))))))))))))))))))