FpFiniteStructure(p,ab,ac,mb,mc,nb,nc,ib,ic,eb,ec)

((((forall pft_index_bottomlayertablesadd. (exists pfa_gap_bottomlayertablesaddprefix. pfa_gap_bottomlayertablesaddprefix + S (pft_index_bottomlayertablesadd) = (((p)) * ((p)))) -> exists pft_value_bottomlayertablesadd. (((((exists ff_h_pft_bottomlayertablesaddpointentry. ff_h_pft_bottomlayertablesaddpointentry + S (pft_value_bottomlayertablesadd) = S ((S (pft_index_bottomlayertablesadd)) * (ac))) /\ exists ff_q_pft_bottomlayertablesaddpointentry. (ab) = ff_q_pft_bottomlayertablesaddpointentry * S ((S (pft_index_bottomlayertablesadd)) * (ac)) + (pft_value_bottomlayertablesadd))) /\ ((exists pft_row_bottomlayertablesaddpointvalue pft_column_bottomlayertablesaddpointvalue. (((pft_index_bottomlayertablesadd) = pft_row_bottomlayertablesaddpointvalue * ((p)) + pft_column_bottomlayertablesaddpointvalue) /\ ((((exists pfa_gap_bottomlayertablesaddpointvalueoperationleft. pfa_gap_bottomlayertablesaddpointvalueoperationleft + S (pft_row_bottomlayertablesaddpointvalue) = ((p))) /\ (((exists pfa_gap_bottomlayertablesaddpointvalueoperationright. pfa_gap_bottomlayertablesaddpointvalueoperationright + S (pft_column_bottomlayertablesaddpointvalue) = ((p))) /\ ((((exists pfa_gap_bottomlayertablesaddpointvalueoperationresultbound. pfa_gap_bottomlayertablesaddpointvalueoperationresultbound + S (pft_value_bottomlayertablesadd) = ((p))) /\ ((exists pfa_offset_left_bottomlayertablesaddpointvalueoperationresultcongruence pfa_offset_right_bottomlayertablesaddpointvalueoperationresultcongruence. ((pft_row_bottomlayertablesaddpointvalue) + (pft_column_bottomlayertablesaddpointvalue)) + ((p)) * pfa_offset_left_bottomlayertablesaddpointvalueoperationresultcongruence = (pft_value_bottomlayertablesadd) + ((p)) * pfa_offset_right_bottomlayertablesaddpointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_bottomlayertablesmultiply. (exists pfa_gap_bottomlayertablesmultiplyprefix. pfa_gap_bottomlayertablesmultiplyprefix + S (pft_index_bottomlayertablesmultiply) = (((p)) * ((p)))) -> exists pft_value_bottomlayertablesmultiply. (((((exists ff_h_pft_bottomlayertablesmultiplypointentry. ff_h_pft_bottomlayertablesmultiplypointentry + S (pft_value_bottomlayertablesmultiply) = S ((S (pft_index_bottomlayertablesmultiply)) * (mc))) /\ exists ff_q_pft_bottomlayertablesmultiplypointentry. (mb) = ff_q_pft_bottomlayertablesmultiplypointentry * S ((S (pft_index_bottomlayertablesmultiply)) * (mc)) + (pft_value_bottomlayertablesmultiply))) /\ ((exists pft_row_bottomlayertablesmultiplypointvalue pft_column_bottomlayertablesmultiplypointvalue. (((pft_index_bottomlayertablesmultiply) = pft_row_bottomlayertablesmultiplypointvalue * ((p)) + pft_column_bottomlayertablesmultiplypointvalue) /\ ((((exists pfa_gap_bottomlayertablesmultiplypointvalueoperationleft. pfa_gap_bottomlayertablesmultiplypointvalueoperationleft + S (pft_row_bottomlayertablesmultiplypointvalue) = ((p))) /\ (((exists pfa_gap_bottomlayertablesmultiplypointvalueoperationright. pfa_gap_bottomlayertablesmultiplypointvalueoperationright + S (pft_column_bottomlayertablesmultiplypointvalue) = ((p))) /\ ((((exists pfa_gap_bottomlayertablesmultiplypointvalueoperationresultbound. pfa_gap_bottomlayertablesmultiplypointvalueoperationresultbound + S (pft_value_bottomlayertablesmultiply) = ((p))) /\ ((exists pfa_offset_left_bottomlayertablesmultiplypointvalueoperationresultcongruence pfa_offset_right_bottomlayertablesmultiplypointvalueoperationresultcongruence. ((pft_row_bottomlayertablesmultiplypointvalue) * (pft_column_bottomlayertablesmultiplypointvalue)) + ((p)) * pfa_offset_left_bottomlayertablesmultiplypointvalueoperationresultcongruence = (pft_value_bottomlayertablesmultiply) + ((p)) * pfa_offset_right_bottomlayertablesmultiplypointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_bottomlayertablesnegate. (exists pfa_gap_bottomlayertablesnegateprefix. pfa_gap_bottomlayertablesnegateprefix + S (pft_index_bottomlayertablesnegate) = ((p))) -> exists pft_value_bottomlayertablesnegate. (((((exists ff_h_pft_bottomlayertablesnegatepointentry. ff_h_pft_bottomlayertablesnegatepointentry + S (pft_value_bottomlayertablesnegate) = S ((S (pft_index_bottomlayertablesnegate)) * (nc))) /\ exists ff_q_pft_bottomlayertablesnegatepointentry. (nb) = ff_q_pft_bottomlayertablesnegatepointentry * S ((S (pft_index_bottomlayertablesnegate)) * (nc)) + (pft_value_bottomlayertablesnegate))) /\ ((((exists pfa_gap_bottomlayertablesnegatepointvalueadditionleft. pfa_gap_bottomlayertablesnegatepointvalueadditionleft + S (pft_index_bottomlayertablesnegate) = ((p))) /\ (((exists pfa_gap_bottomlayertablesnegatepointvalueadditionright. pfa_gap_bottomlayertablesnegatepointvalueadditionright + S (pft_value_bottomlayertablesnegate) = ((p))) /\ ((((exists pfa_gap_bottomlayertablesnegatepointvalueadditionresultbound. pfa_gap_bottomlayertablesnegatepointvalueadditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayertablesnegatepointvalueadditionresultcongruence pfa_offset_right_bottomlayertablesnegatepointvalueadditionresultcongruence. ((pft_index_bottomlayertablesnegate) + (pft_value_bottomlayertablesnegate)) + ((p)) * pfa_offset_left_bottomlayertablesnegatepointvalueadditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayertablesnegatepointvalueadditionresultcongruence))))))))))))) /\ ((forall pft_index_bottomlayertablesinverse. (exists pfa_gap_bottomlayertablesinverseprefix. pfa_gap_bottomlayertablesinverseprefix + S (pft_index_bottomlayertablesinverse) = ((p))) -> exists pft_value_bottomlayertablesinverse. (((((exists ff_h_pft_bottomlayertablesinversepointentry. ff_h_pft_bottomlayertablesinversepointentry + S (pft_value_bottomlayertablesinverse) = S ((S (pft_index_bottomlayertablesinverse)) * (ic))) /\ exists ff_q_pft_bottomlayertablesinversepointentry. (ib) = ff_q_pft_bottomlayertablesinversepointentry * S ((S (pft_index_bottomlayertablesinverse)) * (ic)) + (pft_value_bottomlayertablesinverse))) /\ ((((exists pfa_gap_bottomlayertablesinversepointvalueinput. pfa_gap_bottomlayertablesinversepointvalueinput + S (pft_index_bottomlayertablesinverse) = ((p))) /\ (((exists pfa_gap_bottomlayertablesinversepointvalueoutput. pfa_gap_bottomlayertablesinversepointvalueoutput + S (pft_value_bottomlayertablesinverse) = ((p))) /\ ((((pft_index_bottomlayertablesinverse) = 0 /\ (pft_value_bottomlayertablesinverse) = 0) \/ (((~((pft_index_bottomlayertablesinverse) = 0)) /\ ((((exists pfa_gap_bottomlayertablesinversepointvaluenonzeromultiplicationleft. pfa_gap_bottomlayertablesinversepointvaluenonzeromultiplicationleft + S (pft_index_bottomlayertablesinverse) = ((p))) /\ (((exists pfa_gap_bottomlayertablesinversepointvaluenonzeromultiplicationright. pfa_gap_bottomlayertablesinversepointvaluenonzeromultiplicationright + S (pft_value_bottomlayertablesinverse) = ((p))) /\ ((((exists pfa_gap_bottomlayertablesinversepointvaluenonzeromultiplicationresultbound. pfa_gap_bottomlayertablesinversepointvaluenonzeromultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayertablesinversepointvaluenonzeromultiplicationresultcongruence pfa_offset_right_bottomlayertablesinversepointvaluenonzeromultiplicationresultcongruence. ((pft_index_bottomlayertablesinverse) * (pft_value_bottomlayertablesinverse)) + ((p)) * pfa_offset_left_bottomlayertablesinversepointvaluenonzeromultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayertablesinversepointvaluenonzeromultiplicationresultcongruence))))))))))))))))))))))))))))) /\ (((((forall pff_enumeration_index_bottomlayercardinalityenumeration. (exists pfa_gap_bottomlayercardinalityenumerationbound. pfa_gap_bottomlayercardinalityenumerationbound + S (pff_enumeration_index_bottomlayercardinalityenumeration) = ((p))) -> (((exists ff_h_pft_bottomlayercardinalityenumerationentry. ff_h_pft_bottomlayercardinalityenumerationentry + S (pff_enumeration_index_bottomlayercardinalityenumeration) = S ((S (pff_enumeration_index_bottomlayercardinalityenumeration)) * (ec))) /\ exists ff_q_pft_bottomlayercardinalityenumerationentry. (eb) = ff_q_pft_bottomlayercardinalityenumerationentry * S ((S (pff_enumeration_index_bottomlayercardinalityenumeration)) * (ec)) + (pff_enumeration_index_bottomlayercardinalityenumeration)))) /\ (((forall pff_cardinality_i_bottomlayercardinality pff_cardinality_a_bottomlayercardinality. (exists pfa_gap_bottomlayercardinalitybounded_index. pfa_gap_bottomlayercardinalitybounded_index + S (pff_cardinality_i_bottomlayercardinality) = ((p))) -> (((exists ff_h_pft_bottomlayercardinalitybounded_entry. ff_h_pft_bottomlayercardinalitybounded_entry + S (pff_cardinality_a_bottomlayercardinality) = S ((S (pff_cardinality_i_bottomlayercardinality)) * (ec))) /\ exists ff_q_pft_bottomlayercardinalitybounded_entry. (eb) = ff_q_pft_bottomlayercardinalitybounded_entry * S ((S (pff_cardinality_i_bottomlayercardinality)) * (ec)) + (pff_cardinality_a_bottomlayercardinality))) -> (exists pfa_gap_bottomlayercardinalitybounded_value. pfa_gap_bottomlayercardinalitybounded_value + S (pff_cardinality_a_bottomlayercardinality) = ((p)))) /\ (((forall pff_cardinality_i_bottomlayercardinality pff_cardinality_j_bottomlayercardinality pff_cardinality_a_bottomlayercardinality. (exists pfa_gap_bottomlayercardinalityinjective_i. pfa_gap_bottomlayercardinalityinjective_i + S (pff_cardinality_i_bottomlayercardinality) = ((p))) -> (exists pfa_gap_bottomlayercardinalityinjective_j. pfa_gap_bottomlayercardinalityinjective_j + S (pff_cardinality_j_bottomlayercardinality) = ((p))) -> (((exists ff_h_pft_bottomlayercardinalityinjective_first. ff_h_pft_bottomlayercardinalityinjective_first + S (pff_cardinality_a_bottomlayercardinality) = S ((S (pff_cardinality_i_bottomlayercardinality)) * (ec))) /\ exists ff_q_pft_bottomlayercardinalityinjective_first. (eb) = ff_q_pft_bottomlayercardinalityinjective_first * S ((S (pff_cardinality_i_bottomlayercardinality)) * (ec)) + (pff_cardinality_a_bottomlayercardinality))) -> (((exists ff_h_pft_bottomlayercardinalityinjective_second. ff_h_pft_bottomlayercardinalityinjective_second + S (pff_cardinality_a_bottomlayercardinality) = S ((S (pff_cardinality_j_bottomlayercardinality)) * (ec))) /\ exists ff_q_pft_bottomlayercardinalityinjective_second. (eb) = ff_q_pft_bottomlayercardinalityinjective_second * S ((S (pff_cardinality_j_bottomlayercardinality)) * (ec)) + (pff_cardinality_a_bottomlayercardinality))) -> pff_cardinality_i_bottomlayercardinality = pff_cardinality_j_bottomlayercardinality) /\ ((forall pff_cardinality_a_bottomlayercardinality. (exists pfa_gap_bottomlayercardinalitysurjective_value. pfa_gap_bottomlayercardinalitysurjective_value + S (pff_cardinality_a_bottomlayercardinality) = ((p))) -> exists pff_cardinality_i_bottomlayercardinality. (exists pfa_gap_bottomlayercardinalitysurjective_index. pfa_gap_bottomlayercardinalitysurjective_index + S (pff_cardinality_i_bottomlayercardinality) = ((p))) /\ (((exists ff_h_pft_bottomlayercardinalitysurjective_entry. ff_h_pft_bottomlayercardinalitysurjective_entry + S (pff_cardinality_a_bottomlayercardinality) = S ((S (pff_cardinality_i_bottomlayercardinality)) * (ec))) /\ exists ff_q_pft_bottomlayercardinalitysurjective_entry. (eb) = ff_q_pft_bottomlayercardinalitysurjective_entry * S ((S (pff_cardinality_i_bottomlayercardinality)) * (ec)) + (pff_cardinality_a_bottomlayercardinality))))))))))) /\ (((((exists pfa_gap_bottomlayerlawszero. pfa_gap_bottomlayerlawszero + S (0) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsone. pfa_gap_bottomlayerlawsone + S (1) = ((p))) /\ (((~(0 = 1)) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsaddleft. pfa_gap_bottomlayerlawsaddleft + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (exists pfa_gap_bottomlayerlawsaddright. pfa_gap_bottomlayerlawsaddright + S (pfa_law_b_bottomlayerlaws) = ((p))) -> exists pfa_law_c_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsaddchosenleft. pfa_gap_bottomlayerlawsaddchosenleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddchosenright. pfa_gap_bottomlayerlawsaddchosenright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddchosenresultbound. pfa_gap_bottomlayerlawsaddchosenresultbound + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddchosenresultcongruence pfa_offset_right_bottomlayerlawsaddchosenresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddchosenresultcongruence = (pfa_law_c_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddchosenresultcongruence))))))))) /\ forall pfa_law_d_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsaddotherleft. pfa_gap_bottomlayerlawsaddotherleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddotherright. pfa_gap_bottomlayerlawsaddotherright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddotherresultbound. pfa_gap_bottomlayerlawsaddotherresultbound + S (pfa_law_d_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddotherresultcongruence pfa_offset_right_bottomlayerlawsaddotherresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddotherresultcongruence = (pfa_law_d_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddotherresultcongruence))))))))) -> pfa_law_d_bottomlayerlaws = pfa_law_c_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws pfa_law_c_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsaddcomm_firstleft. pfa_gap_bottomlayerlawsaddcomm_firstleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddcomm_firstright. pfa_gap_bottomlayerlawsaddcomm_firstright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddcomm_firstresultbound. pfa_gap_bottomlayerlawsaddcomm_firstresultbound + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddcomm_firstresultcongruence pfa_offset_right_bottomlayerlawsaddcomm_firstresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddcomm_firstresultcongruence = (pfa_law_c_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddcomm_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsaddcomm_secondleft. pfa_gap_bottomlayerlawsaddcomm_secondleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddcomm_secondright. pfa_gap_bottomlayerlawsaddcomm_secondright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddcomm_secondresultbound. pfa_gap_bottomlayerlawsaddcomm_secondresultbound + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddcomm_secondresultcongruence pfa_offset_right_bottomlayerlawsaddcomm_secondresultcongruence. ((pfa_law_b_bottomlayerlaws) + (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddcomm_secondresultcongruence = (pfa_law_c_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddcomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws pfa_law_c_bottomlayerlaws pfa_law_x_bottomlayerlaws pfa_law_y_bottomlayerlaws pfa_law_u_bottomlayerlaws pfa_law_v_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsaddassoc_firstleft. pfa_gap_bottomlayerlawsaddassoc_firstleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddassoc_firstright. pfa_gap_bottomlayerlawsaddassoc_firstright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddassoc_firstresultbound. pfa_gap_bottomlayerlawsaddassoc_firstresultbound + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddassoc_firstresultcongruence pfa_offset_right_bottomlayerlawsaddassoc_firstresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddassoc_firstresultcongruence = (pfa_law_x_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsaddassoc_leftleft. pfa_gap_bottomlayerlawsaddassoc_leftleft + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddassoc_leftright. pfa_gap_bottomlayerlawsaddassoc_leftright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddassoc_leftresultbound. pfa_gap_bottomlayerlawsaddassoc_leftresultbound + S (pfa_law_u_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddassoc_leftresultcongruence pfa_offset_right_bottomlayerlawsaddassoc_leftresultcongruence. ((pfa_law_x_bottomlayerlaws) + (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddassoc_leftresultcongruence = (pfa_law_u_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsaddassoc_secondleft. pfa_gap_bottomlayerlawsaddassoc_secondleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddassoc_secondright. pfa_gap_bottomlayerlawsaddassoc_secondright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddassoc_secondresultbound. pfa_gap_bottomlayerlawsaddassoc_secondresultbound + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddassoc_secondresultcongruence pfa_offset_right_bottomlayerlawsaddassoc_secondresultcongruence. ((pfa_law_b_bottomlayerlaws) + (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddassoc_secondresultcongruence = (pfa_law_y_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsaddassoc_rightleft. pfa_gap_bottomlayerlawsaddassoc_rightleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsaddassoc_rightright. pfa_gap_bottomlayerlawsaddassoc_rightright + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsaddassoc_rightresultbound. pfa_gap_bottomlayerlawsaddassoc_rightresultbound + S (pfa_law_v_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsaddassoc_rightresultcongruence pfa_offset_right_bottomlayerlawsaddassoc_rightresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_y_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsaddassoc_rightresultcongruence = (pfa_law_v_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsaddassoc_rightresultcongruence))))))))) -> pfa_law_u_bottomlayerlaws = pfa_law_v_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsmultiplyleft. pfa_gap_bottomlayerlawsmultiplyleft + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (exists pfa_gap_bottomlayerlawsmultiplyright. pfa_gap_bottomlayerlawsmultiplyright + S (pfa_law_b_bottomlayerlaws) = ((p))) -> exists pfa_law_c_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsmultiplychosenleft. pfa_gap_bottomlayerlawsmultiplychosenleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplychosenright. pfa_gap_bottomlayerlawsmultiplychosenright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplychosenresultbound. pfa_gap_bottomlayerlawsmultiplychosenresultbound + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplychosenresultcongruence pfa_offset_right_bottomlayerlawsmultiplychosenresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplychosenresultcongruence = (pfa_law_c_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplychosenresultcongruence))))))))) /\ forall pfa_law_d_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsmultiplyotherleft. pfa_gap_bottomlayerlawsmultiplyotherleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplyotherright. pfa_gap_bottomlayerlawsmultiplyotherright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplyotherresultbound. pfa_gap_bottomlayerlawsmultiplyotherresultbound + S (pfa_law_d_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplyotherresultcongruence pfa_offset_right_bottomlayerlawsmultiplyotherresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplyotherresultcongruence = (pfa_law_d_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplyotherresultcongruence))))))))) -> pfa_law_d_bottomlayerlaws = pfa_law_c_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws pfa_law_c_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsmultiplycomm_firstleft. pfa_gap_bottomlayerlawsmultiplycomm_firstleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplycomm_firstright. pfa_gap_bottomlayerlawsmultiplycomm_firstright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplycomm_firstresultbound. pfa_gap_bottomlayerlawsmultiplycomm_firstresultbound + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplycomm_firstresultcongruence pfa_offset_right_bottomlayerlawsmultiplycomm_firstresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplycomm_firstresultcongruence = (pfa_law_c_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplycomm_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsmultiplycomm_secondleft. pfa_gap_bottomlayerlawsmultiplycomm_secondleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplycomm_secondright. pfa_gap_bottomlayerlawsmultiplycomm_secondright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplycomm_secondresultbound. pfa_gap_bottomlayerlawsmultiplycomm_secondresultbound + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplycomm_secondresultcongruence pfa_offset_right_bottomlayerlawsmultiplycomm_secondresultcongruence. ((pfa_law_b_bottomlayerlaws) * (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplycomm_secondresultcongruence = (pfa_law_c_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplycomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws pfa_law_c_bottomlayerlaws pfa_law_x_bottomlayerlaws pfa_law_y_bottomlayerlaws pfa_law_u_bottomlayerlaws pfa_law_v_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsmultiplyassoc_firstleft. pfa_gap_bottomlayerlawsmultiplyassoc_firstleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplyassoc_firstright. pfa_gap_bottomlayerlawsmultiplyassoc_firstright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplyassoc_firstresultbound. pfa_gap_bottomlayerlawsmultiplyassoc_firstresultbound + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplyassoc_firstresultcongruence pfa_offset_right_bottomlayerlawsmultiplyassoc_firstresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplyassoc_firstresultcongruence = (pfa_law_x_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplyassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsmultiplyassoc_leftleft. pfa_gap_bottomlayerlawsmultiplyassoc_leftleft + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplyassoc_leftright. pfa_gap_bottomlayerlawsmultiplyassoc_leftright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplyassoc_leftresultbound. pfa_gap_bottomlayerlawsmultiplyassoc_leftresultbound + S (pfa_law_u_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplyassoc_leftresultcongruence pfa_offset_right_bottomlayerlawsmultiplyassoc_leftresultcongruence. ((pfa_law_x_bottomlayerlaws) * (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplyassoc_leftresultcongruence = (pfa_law_u_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplyassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsmultiplyassoc_secondleft. pfa_gap_bottomlayerlawsmultiplyassoc_secondleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplyassoc_secondright. pfa_gap_bottomlayerlawsmultiplyassoc_secondright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplyassoc_secondresultbound. pfa_gap_bottomlayerlawsmultiplyassoc_secondresultbound + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplyassoc_secondresultcongruence pfa_offset_right_bottomlayerlawsmultiplyassoc_secondresultcongruence. ((pfa_law_b_bottomlayerlaws) * (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplyassoc_secondresultcongruence = (pfa_law_y_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplyassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsmultiplyassoc_rightleft. pfa_gap_bottomlayerlawsmultiplyassoc_rightleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiplyassoc_rightright. pfa_gap_bottomlayerlawsmultiplyassoc_rightright + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiplyassoc_rightresultbound. pfa_gap_bottomlayerlawsmultiplyassoc_rightresultbound + S (pfa_law_v_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiplyassoc_rightresultcongruence pfa_offset_right_bottomlayerlawsmultiplyassoc_rightresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_y_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiplyassoc_rightresultcongruence = (pfa_law_v_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiplyassoc_rightresultcongruence))))))))) -> pfa_law_u_bottomlayerlaws = pfa_law_v_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws pfa_law_c_bottomlayerlaws pfa_law_s_bottomlayerlaws pfa_law_x_bottomlayerlaws pfa_law_y_bottomlayerlaws pfa_law_u_bottomlayerlaws pfa_law_v_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsleftdistribution_sumleft. pfa_gap_bottomlayerlawsleftdistribution_sumleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsleftdistribution_sumright. pfa_gap_bottomlayerlawsleftdistribution_sumright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsleftdistribution_sumresultbound. pfa_gap_bottomlayerlawsleftdistribution_sumresultbound + S (pfa_law_s_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsleftdistribution_sumresultcongruence pfa_offset_right_bottomlayerlawsleftdistribution_sumresultcongruence. ((pfa_law_b_bottomlayerlaws) + (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsleftdistribution_sumresultcongruence = (pfa_law_s_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsleftdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsleftdistribution_leftleft. pfa_gap_bottomlayerlawsleftdistribution_leftleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsleftdistribution_leftright. pfa_gap_bottomlayerlawsleftdistribution_leftright + S (pfa_law_s_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsleftdistribution_leftresultbound. pfa_gap_bottomlayerlawsleftdistribution_leftresultbound + S (pfa_law_u_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsleftdistribution_leftresultcongruence pfa_offset_right_bottomlayerlawsleftdistribution_leftresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_s_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsleftdistribution_leftresultcongruence = (pfa_law_u_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsleftdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsleftdistribution_firstleft. pfa_gap_bottomlayerlawsleftdistribution_firstleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsleftdistribution_firstright. pfa_gap_bottomlayerlawsleftdistribution_firstright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsleftdistribution_firstresultbound. pfa_gap_bottomlayerlawsleftdistribution_firstresultbound + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsleftdistribution_firstresultcongruence pfa_offset_right_bottomlayerlawsleftdistribution_firstresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsleftdistribution_firstresultcongruence = (pfa_law_x_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsleftdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsleftdistribution_secondleft. pfa_gap_bottomlayerlawsleftdistribution_secondleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsleftdistribution_secondright. pfa_gap_bottomlayerlawsleftdistribution_secondright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsleftdistribution_secondresultbound. pfa_gap_bottomlayerlawsleftdistribution_secondresultbound + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsleftdistribution_secondresultcongruence pfa_offset_right_bottomlayerlawsleftdistribution_secondresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsleftdistribution_secondresultcongruence = (pfa_law_y_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsleftdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsleftdistribution_rightleft. pfa_gap_bottomlayerlawsleftdistribution_rightleft + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsleftdistribution_rightright. pfa_gap_bottomlayerlawsleftdistribution_rightright + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsleftdistribution_rightresultbound. pfa_gap_bottomlayerlawsleftdistribution_rightresultbound + S (pfa_law_v_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsleftdistribution_rightresultcongruence pfa_offset_right_bottomlayerlawsleftdistribution_rightresultcongruence. ((pfa_law_x_bottomlayerlaws) + (pfa_law_y_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsleftdistribution_rightresultcongruence = (pfa_law_v_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsleftdistribution_rightresultcongruence))))))))) -> pfa_law_u_bottomlayerlaws = pfa_law_v_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws pfa_law_c_bottomlayerlaws pfa_law_s_bottomlayerlaws pfa_law_x_bottomlayerlaws pfa_law_y_bottomlayerlaws pfa_law_u_bottomlayerlaws pfa_law_v_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsrightdistribution_sumleft. pfa_gap_bottomlayerlawsrightdistribution_sumleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsrightdistribution_sumright. pfa_gap_bottomlayerlawsrightdistribution_sumright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsrightdistribution_sumresultbound. pfa_gap_bottomlayerlawsrightdistribution_sumresultbound + S (pfa_law_s_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsrightdistribution_sumresultcongruence pfa_offset_right_bottomlayerlawsrightdistribution_sumresultcongruence. ((pfa_law_b_bottomlayerlaws) + (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsrightdistribution_sumresultcongruence = (pfa_law_s_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsrightdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsrightdistribution_leftleft. pfa_gap_bottomlayerlawsrightdistribution_leftleft + S (pfa_law_s_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsrightdistribution_leftright. pfa_gap_bottomlayerlawsrightdistribution_leftright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsrightdistribution_leftresultbound. pfa_gap_bottomlayerlawsrightdistribution_leftresultbound + S (pfa_law_u_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsrightdistribution_leftresultcongruence pfa_offset_right_bottomlayerlawsrightdistribution_leftresultcongruence. ((pfa_law_s_bottomlayerlaws) * (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsrightdistribution_leftresultcongruence = (pfa_law_u_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsrightdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsrightdistribution_firstleft. pfa_gap_bottomlayerlawsrightdistribution_firstleft + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsrightdistribution_firstright. pfa_gap_bottomlayerlawsrightdistribution_firstright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsrightdistribution_firstresultbound. pfa_gap_bottomlayerlawsrightdistribution_firstresultbound + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsrightdistribution_firstresultcongruence pfa_offset_right_bottomlayerlawsrightdistribution_firstresultcongruence. ((pfa_law_b_bottomlayerlaws) * (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsrightdistribution_firstresultcongruence = (pfa_law_x_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsrightdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsrightdistribution_secondleft. pfa_gap_bottomlayerlawsrightdistribution_secondleft + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsrightdistribution_secondright. pfa_gap_bottomlayerlawsrightdistribution_secondright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsrightdistribution_secondresultbound. pfa_gap_bottomlayerlawsrightdistribution_secondresultbound + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsrightdistribution_secondresultcongruence pfa_offset_right_bottomlayerlawsrightdistribution_secondresultcongruence. ((pfa_law_c_bottomlayerlaws) * (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsrightdistribution_secondresultcongruence = (pfa_law_y_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsrightdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerlawsrightdistribution_rightleft. pfa_gap_bottomlayerlawsrightdistribution_rightleft + S (pfa_law_x_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsrightdistribution_rightright. pfa_gap_bottomlayerlawsrightdistribution_rightright + S (pfa_law_y_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsrightdistribution_rightresultbound. pfa_gap_bottomlayerlawsrightdistribution_rightresultbound + S (pfa_law_v_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsrightdistribution_rightresultcongruence pfa_offset_right_bottomlayerlawsrightdistribution_rightresultcongruence. ((pfa_law_x_bottomlayerlaws) + (pfa_law_y_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsrightdistribution_rightresultcongruence = (pfa_law_v_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsrightdistribution_rightresultcongruence))))))))) -> pfa_law_u_bottomlayerlaws = pfa_law_v_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsadd_zero_rightinput. pfa_gap_bottomlayerlawsadd_zero_rightinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (((exists pfa_gap_bottomlayerlawsadd_zero_rightleft. pfa_gap_bottomlayerlawsadd_zero_rightleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsadd_zero_rightright. pfa_gap_bottomlayerlawsadd_zero_rightright + S (0) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsadd_zero_rightresultbound. pfa_gap_bottomlayerlawsadd_zero_rightresultbound + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsadd_zero_rightresultcongruence pfa_offset_right_bottomlayerlawsadd_zero_rightresultcongruence. ((pfa_law_a_bottomlayerlaws) + (0)) + ((p)) * pfa_offset_left_bottomlayerlawsadd_zero_rightresultcongruence = (pfa_law_a_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsadd_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsadd_zero_leftinput. pfa_gap_bottomlayerlawsadd_zero_leftinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (((exists pfa_gap_bottomlayerlawsadd_zero_leftleft. pfa_gap_bottomlayerlawsadd_zero_leftleft + S (0) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsadd_zero_leftright. pfa_gap_bottomlayerlawsadd_zero_leftright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsadd_zero_leftresultbound. pfa_gap_bottomlayerlawsadd_zero_leftresultbound + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsadd_zero_leftresultcongruence pfa_offset_right_bottomlayerlawsadd_zero_leftresultcongruence. ((0) + (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsadd_zero_leftresultcongruence = (pfa_law_a_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsadd_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsmultiply_one_rightinput. pfa_gap_bottomlayerlawsmultiply_one_rightinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (((exists pfa_gap_bottomlayerlawsmultiply_one_rightleft. pfa_gap_bottomlayerlawsmultiply_one_rightleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiply_one_rightright. pfa_gap_bottomlayerlawsmultiply_one_rightright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiply_one_rightresultbound. pfa_gap_bottomlayerlawsmultiply_one_rightresultbound + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiply_one_rightresultcongruence pfa_offset_right_bottomlayerlawsmultiply_one_rightresultcongruence. ((pfa_law_a_bottomlayerlaws) * (1)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiply_one_rightresultcongruence = (pfa_law_a_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiply_one_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsmultiply_one_leftinput. pfa_gap_bottomlayerlawsmultiply_one_leftinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (((exists pfa_gap_bottomlayerlawsmultiply_one_leftleft. pfa_gap_bottomlayerlawsmultiply_one_leftleft + S (1) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiply_one_leftright. pfa_gap_bottomlayerlawsmultiply_one_leftright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiply_one_leftresultbound. pfa_gap_bottomlayerlawsmultiply_one_leftresultbound + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiply_one_leftresultcongruence pfa_offset_right_bottomlayerlawsmultiply_one_leftresultcongruence. ((1) * (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiply_one_leftresultcongruence = (pfa_law_a_bottomlayerlaws) + ((p)) * pfa_offset_right_bottomlayerlawsmultiply_one_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsmultiply_zero_rightinput. pfa_gap_bottomlayerlawsmultiply_zero_rightinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (((exists pfa_gap_bottomlayerlawsmultiply_zero_rightleft. pfa_gap_bottomlayerlawsmultiply_zero_rightleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiply_zero_rightright. pfa_gap_bottomlayerlawsmultiply_zero_rightright + S (0) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiply_zero_rightresultbound. pfa_gap_bottomlayerlawsmultiply_zero_rightresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiply_zero_rightresultcongruence pfa_offset_right_bottomlayerlawsmultiply_zero_rightresultcongruence. ((pfa_law_a_bottomlayerlaws) * (0)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiply_zero_rightresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayerlawsmultiply_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsmultiply_zero_leftinput. pfa_gap_bottomlayerlawsmultiply_zero_leftinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> (((exists pfa_gap_bottomlayerlawsmultiply_zero_leftleft. pfa_gap_bottomlayerlawsmultiply_zero_leftleft + S (0) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsmultiply_zero_leftright. pfa_gap_bottomlayerlawsmultiply_zero_leftright + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsmultiply_zero_leftresultbound. pfa_gap_bottomlayerlawsmultiply_zero_leftresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsmultiply_zero_leftresultcongruence pfa_offset_right_bottomlayerlawsmultiply_zero_leftresultcongruence. ((0) * (pfa_law_a_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsmultiply_zero_leftresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayerlawsmultiply_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsnegateinput. pfa_gap_bottomlayerlawsnegateinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> exists pfa_law_b_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsnegatechosenadditionleft. pfa_gap_bottomlayerlawsnegatechosenadditionleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsnegatechosenadditionright. pfa_gap_bottomlayerlawsnegatechosenadditionright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsnegatechosenadditionresultbound. pfa_gap_bottomlayerlawsnegatechosenadditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsnegatechosenadditionresultcongruence pfa_offset_right_bottomlayerlawsnegatechosenadditionresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsnegatechosenadditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayerlawsnegatechosenadditionresultcongruence))))))))) /\ forall pfa_law_c_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsnegateotheradditionleft. pfa_gap_bottomlayerlawsnegateotheradditionleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsnegateotheradditionright. pfa_gap_bottomlayerlawsnegateotheradditionright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsnegateotheradditionresultbound. pfa_gap_bottomlayerlawsnegateotheradditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsnegateotheradditionresultcongruence pfa_offset_right_bottomlayerlawsnegateotheradditionresultcongruence. ((pfa_law_a_bottomlayerlaws) + (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsnegateotheradditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayerlawsnegateotheradditionresultcongruence))))))))) -> pfa_law_c_bottomlayerlaws = pfa_law_b_bottomlayerlaws) /\ (((forall pfa_law_a_bottomlayerlaws. (exists pfa_gap_bottomlayerlawsinverseinput. pfa_gap_bottomlayerlawsinverseinput + S (pfa_law_a_bottomlayerlaws) = ((p))) -> ~(pfa_law_a_bottomlayerlaws = 0) -> exists pfa_law_b_bottomlayerlaws. (((~((pfa_law_a_bottomlayerlaws) = 0)) /\ ((((exists pfa_gap_bottomlayerlawsinversechosenmultiplicationleft. pfa_gap_bottomlayerlawsinversechosenmultiplicationleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsinversechosenmultiplicationright. pfa_gap_bottomlayerlawsinversechosenmultiplicationright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsinversechosenmultiplicationresultbound. pfa_gap_bottomlayerlawsinversechosenmultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsinversechosenmultiplicationresultcongruence pfa_offset_right_bottomlayerlawsinversechosenmultiplicationresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsinversechosenmultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayerlawsinversechosenmultiplicationresultcongruence)))))))))))) /\ forall pfa_law_c_bottomlayerlaws. (((~((pfa_law_a_bottomlayerlaws) = 0)) /\ ((((exists pfa_gap_bottomlayerlawsinverseothermultiplicationleft. pfa_gap_bottomlayerlawsinverseothermultiplicationleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsinverseothermultiplicationright. pfa_gap_bottomlayerlawsinverseothermultiplicationright + S (pfa_law_c_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsinverseothermultiplicationresultbound. pfa_gap_bottomlayerlawsinverseothermultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsinverseothermultiplicationresultcongruence pfa_offset_right_bottomlayerlawsinverseothermultiplicationresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_c_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsinverseothermultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayerlawsinverseothermultiplicationresultcongruence)))))))))))) -> pfa_law_c_bottomlayerlaws = pfa_law_b_bottomlayerlaws) /\ ((forall pfa_law_a_bottomlayerlaws pfa_law_b_bottomlayerlaws. (((exists pfa_gap_bottomlayerlawsnozeroleft. pfa_gap_bottomlayerlawsnozeroleft + S (pfa_law_a_bottomlayerlaws) = ((p))) /\ (((exists pfa_gap_bottomlayerlawsnozeroright. pfa_gap_bottomlayerlawsnozeroright + S (pfa_law_b_bottomlayerlaws) = ((p))) /\ ((((exists pfa_gap_bottomlayerlawsnozeroresultbound. pfa_gap_bottomlayerlawsnozeroresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayerlawsnozeroresultcongruence pfa_offset_right_bottomlayerlawsnozeroresultcongruence. ((pfa_law_a_bottomlayerlaws) * (pfa_law_b_bottomlayerlaws)) + ((p)) * pfa_offset_left_bottomlayerlawsnozeroresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayerlawsnozeroresultcongruence))))))))) -> pfa_law_a_bottomlayerlaws = 0 \/ pfa_law_b_bottomlayerlaws = 0)))))))))))))))))))))))))))))))))))))))) /\ ((((exists pff_history_code_bottomlayercharacteristicmodulus pff_history_scale_bottomlayercharacteristicmodulus. (((((exists ff_h_pft_bottomlayercharacteristicmodulushistorystart. ff_h_pft_bottomlayercharacteristicmodulushistorystart + S (0) = S ((S (0)) * pff_history_scale_bottomlayercharacteristicmodulus)) /\ exists ff_q_pft_bottomlayercharacteristicmodulushistorystart. pff_history_code_bottomlayercharacteristicmodulus = ff_q_pft_bottomlayercharacteristicmodulushistorystart * S ((S (0)) * pff_history_scale_bottomlayercharacteristicmodulus) + (0))) /\ (((((exists ff_h_pft_bottomlayercharacteristicmodulushistoryterminal. ff_h_pft_bottomlayercharacteristicmodulushistoryterminal + S (0) = S ((S ((p))) * pff_history_scale_bottomlayercharacteristicmodulus)) /\ exists ff_q_pft_bottomlayercharacteristicmodulushistoryterminal. pff_history_code_bottomlayercharacteristicmodulus = ff_q_pft_bottomlayercharacteristicmodulushistoryterminal * S ((S ((p))) * pff_history_scale_bottomlayercharacteristicmodulus) + (0))) /\ ((forall pff_trace_index_bottomlayercharacteristicmodulushistorysteps. (exists pfa_gap_bottomlayercharacteristicmodulushistorystepsindex. pfa_gap_bottomlayercharacteristicmodulushistorystepsindex + S (pff_trace_index_bottomlayercharacteristicmodulushistorysteps) = ((p))) -> exists pff_trace_before_bottomlayercharacteristicmodulushistorysteps pff_trace_after_bottomlayercharacteristicmodulushistorysteps. ((((exists ff_h_pft_bottomlayercharacteristicmodulushistorystepsbefore. ff_h_pft_bottomlayercharacteristicmodulushistorystepsbefore + S (pff_trace_before_bottomlayercharacteristicmodulushistorysteps) = S ((S (pff_trace_index_bottomlayercharacteristicmodulushistorysteps)) * pff_history_scale_bottomlayercharacteristicmodulus)) /\ exists ff_q_pft_bottomlayercharacteristicmodulushistorystepsbefore. pff_history_code_bottomlayercharacteristicmodulus = ff_q_pft_bottomlayercharacteristicmodulushistorystepsbefore * S ((S (pff_trace_index_bottomlayercharacteristicmodulushistorysteps)) * pff_history_scale_bottomlayercharacteristicmodulus) + (pff_trace_before_bottomlayercharacteristicmodulushistorysteps))) /\ (((((exists ff_h_pft_bottomlayercharacteristicmodulushistorystepsafter. ff_h_pft_bottomlayercharacteristicmodulushistorystepsafter + S (pff_trace_after_bottomlayercharacteristicmodulushistorysteps) = S ((S (S (pff_trace_index_bottomlayercharacteristicmodulushistorysteps))) * pff_history_scale_bottomlayercharacteristicmodulus)) /\ exists ff_q_pft_bottomlayercharacteristicmodulushistorystepsafter. pff_history_code_bottomlayercharacteristicmodulus = ff_q_pft_bottomlayercharacteristicmodulushistorystepsafter * S ((S (S (pff_trace_index_bottomlayercharacteristicmodulushistorysteps))) * pff_history_scale_bottomlayercharacteristicmodulus) + (pff_trace_after_bottomlayercharacteristicmodulushistorysteps))) /\ ((((exists pfa_gap_bottomlayercharacteristicmodulushistorystepsadditionleft. pfa_gap_bottomlayercharacteristicmodulushistorystepsadditionleft + S (pff_trace_before_bottomlayercharacteristicmodulushistorysteps) = ((p))) /\ (((exists pfa_gap_bottomlayercharacteristicmodulushistorystepsadditionright. pfa_gap_bottomlayercharacteristicmodulushistorystepsadditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayercharacteristicmodulushistorystepsadditionresultbound. pfa_gap_bottomlayercharacteristicmodulushistorystepsadditionresultbound + S (pff_trace_after_bottomlayercharacteristicmodulushistorysteps) = ((p))) /\ ((exists pfa_offset_left_bottomlayercharacteristicmodulushistorystepsadditionresultcongruence pfa_offset_right_bottomlayercharacteristicmodulushistorystepsadditionresultcongruence. ((pff_trace_before_bottomlayercharacteristicmodulushistorysteps) + (1)) + ((p)) * pfa_offset_left_bottomlayercharacteristicmodulushistorystepsadditionresultcongruence = (pff_trace_after_bottomlayercharacteristicmodulushistorysteps) + ((p)) * pfa_offset_right_bottomlayercharacteristicmodulushistorystepsadditionresultcongruence)))))))))))))))))))) /\ ((forall pff_smaller_positive_bottomlayercharacteristic. (exists pfa_gap_bottomlayercharacteristicstrict. pfa_gap_bottomlayercharacteristicstrict + S (pff_smaller_positive_bottomlayercharacteristic) = ((p))) -> ~(pff_smaller_positive_bottomlayercharacteristic = 0) -> ~(exists pff_history_code_bottomlayercharacteristicsmaller pff_history_scale_bottomlayercharacteristicsmaller. (((((exists ff_h_pft_bottomlayercharacteristicsmallerhistorystart. ff_h_pft_bottomlayercharacteristicsmallerhistorystart + S (0) = S ((S (0)) * pff_history_scale_bottomlayercharacteristicsmaller)) /\ exists ff_q_pft_bottomlayercharacteristicsmallerhistorystart. pff_history_code_bottomlayercharacteristicsmaller = ff_q_pft_bottomlayercharacteristicsmallerhistorystart * S ((S (0)) * pff_history_scale_bottomlayercharacteristicsmaller) + (0))) /\ (((((exists ff_h_pft_bottomlayercharacteristicsmallerhistoryterminal. ff_h_pft_bottomlayercharacteristicsmallerhistoryterminal + S (0) = S ((S (pff_smaller_positive_bottomlayercharacteristic)) * pff_history_scale_bottomlayercharacteristicsmaller)) /\ exists ff_q_pft_bottomlayercharacteristicsmallerhistoryterminal. pff_history_code_bottomlayercharacteristicsmaller = ff_q_pft_bottomlayercharacteristicsmallerhistoryterminal * S ((S (pff_smaller_positive_bottomlayercharacteristic)) * pff_history_scale_bottomlayercharacteristicsmaller) + (0))) /\ ((forall pff_trace_index_bottomlayercharacteristicsmallerhistorysteps. (exists pfa_gap_bottomlayercharacteristicsmallerhistorystepsindex. pfa_gap_bottomlayercharacteristicsmallerhistorystepsindex + S (pff_trace_index_bottomlayercharacteristicsmallerhistorysteps) = (pff_smaller_positive_bottomlayercharacteristic)) -> exists pff_trace_before_bottomlayercharacteristicsmallerhistorysteps pff_trace_after_bottomlayercharacteristicsmallerhistorysteps. ((((exists ff_h_pft_bottomlayercharacteristicsmallerhistorystepsbefore. ff_h_pft_bottomlayercharacteristicsmallerhistorystepsbefore + S (pff_trace_before_bottomlayercharacteristicsmallerhistorysteps) = S ((S (pff_trace_index_bottomlayercharacteristicsmallerhistorysteps)) * pff_history_scale_bottomlayercharacteristicsmaller)) /\ exists ff_q_pft_bottomlayercharacteristicsmallerhistorystepsbefore. pff_history_code_bottomlayercharacteristicsmaller = ff_q_pft_bottomlayercharacteristicsmallerhistorystepsbefore * S ((S (pff_trace_index_bottomlayercharacteristicsmallerhistorysteps)) * pff_history_scale_bottomlayercharacteristicsmaller) + (pff_trace_before_bottomlayercharacteristicsmallerhistorysteps))) /\ (((((exists ff_h_pft_bottomlayercharacteristicsmallerhistorystepsafter. ff_h_pft_bottomlayercharacteristicsmallerhistorystepsafter + S (pff_trace_after_bottomlayercharacteristicsmallerhistorysteps) = S ((S (S (pff_trace_index_bottomlayercharacteristicsmallerhistorysteps))) * pff_history_scale_bottomlayercharacteristicsmaller)) /\ exists ff_q_pft_bottomlayercharacteristicsmallerhistorystepsafter. pff_history_code_bottomlayercharacteristicsmaller = ff_q_pft_bottomlayercharacteristicsmallerhistorystepsafter * S ((S (S (pff_trace_index_bottomlayercharacteristicsmallerhistorysteps))) * pff_history_scale_bottomlayercharacteristicsmaller) + (pff_trace_after_bottomlayercharacteristicsmallerhistorysteps))) /\ ((((exists pfa_gap_bottomlayercharacteristicsmallerhistorystepsadditionleft. pfa_gap_bottomlayercharacteristicsmallerhistorystepsadditionleft + S (pff_trace_before_bottomlayercharacteristicsmallerhistorysteps) = ((p))) /\ (((exists pfa_gap_bottomlayercharacteristicsmallerhistorystepsadditionright. pfa_gap_bottomlayercharacteristicsmallerhistorystepsadditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayercharacteristicsmallerhistorystepsadditionresultbound. pfa_gap_bottomlayercharacteristicsmallerhistorystepsadditionresultbound + S (pff_trace_after_bottomlayercharacteristicsmallerhistorysteps) = ((p))) /\ ((exists pfa_offset_left_bottomlayercharacteristicsmallerhistorystepsadditionresultcongruence pfa_offset_right_bottomlayercharacteristicsmallerhistorystepsadditionresultcongruence. ((pff_trace_before_bottomlayercharacteristicsmallerhistorysteps) + (1)) + ((p)) * pfa_offset_left_bottomlayercharacteristicsmallerhistorystepsadditionresultcongruence = (pff_trace_after_bottomlayercharacteristicsmallerhistorysteps) + ((p)) * pfa_offset_right_bottomlayercharacteristicsmallerhistorystepsadditionresultcongruence))))))))))))))))))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.