Definition in prerequisite notation
Lt(0,p) ∧ (Lt(1,p) ∧ (¬0 = 1 ∧ ((∀ x. ∀ y. Lt(x,p) → Lt(y,p) → ∃ z. FpAdd(p,x,y,z) ∧ (∀ n. FpAdd(p,x,y,n) → n = z)) ∧ ((∀ x. ∀ y. ∀ z. FpAdd(p,x,y,z) → FpAdd(p,y,x,z)) ∧ ((∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. FpAdd(p,x,y,n) → FpAdd(p,n,z,k) → FpAdd(p,y,z,m) → FpAdd(p,x,m,i) → k = i) ∧ ((∀ x. ∀ y. Lt(x,p) → Lt(y,p) → ∃ z. FpMul(p,x,y,z) ∧ (∀ n. FpMul(p,x,y,n) → n = z)) ∧ ((∀ x. ∀ y. ∀ z. FpMul(p,x,y,z) → FpMul(p,y,x,z)) ∧ ((∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. FpMul(p,x,y,n) → FpMul(p,n,z,k) → FpMul(p,y,z,m) → FpMul(p,x,m,i) → k = i) ∧ ((∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. FpAdd(p,y,z,n) → FpMul(p,x,n,i) → FpMul(p,x,y,m) → FpMul(p,x,z,k) → FpAdd(p,m,k,j) → i = j) ∧ ((∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. FpAdd(p,y,z,n) → FpMul(p,n,x,i) → FpMul(p,y,x,m) → FpMul(p,z,x,k) → FpAdd(p,m,k,j) → i = j) ∧ ((∀ x. Lt(x,p) → FpAdd(p,x,0,x)) ∧ ((∀ x. Lt(x,p) → FpAdd(p,0,x,x)) ∧ ((∀ x. Lt(x,p) → FpMul(p,x,1,x)) ∧ ((∀ x. Lt(x,p) → FpMul(p,1,x,x)) ∧ ((∀ x. Lt(x,p) → FpMul(p,x,0,0)) ∧ ((∀ x. Lt(x,p) → FpMul(p,0,x,0)) ∧ ((∀ x. Lt(x,p) → ∃ y. FpAdd(p,x,y,0) ∧ (∀ z. FpAdd(p,x,z,0) → z = y)) ∧ ((∀ x. Lt(x,p) → ¬x = 0 → ∃ y. FpInv(p,x,y) ∧ (∀ z. FpInv(p,x,z) → z = y)) ∧ (∀ x. ∀ y. FpMul(p,x,y,0) → x = 0 ∨ y = 0)))))))))))))))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists pfa_gap_bottomlayerzero. pfa_gap_bottomlayerzero + S (0) = ((p))) /\ (((exists pfa_gap_bottomlayerone. pfa_gap_bottomlayerone + S (1) = ((p))) /\ (((~(0 = 1)) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer. (exists pfa_gap_bottomlayeraddleft. pfa_gap_bottomlayeraddleft + S (pfa_law_a_bottomlayer) = ((p))) -> (exists pfa_gap_bottomlayeraddright. pfa_gap_bottomlayeraddright + S (pfa_law_b_bottomlayer) = ((p))) -> exists pfa_law_c_bottomlayer. (((exists pfa_gap_bottomlayeraddchosenleft. pfa_gap_bottomlayeraddchosenleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddchosenright. pfa_gap_bottomlayeraddchosenright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddchosenresultbound. pfa_gap_bottomlayeraddchosenresultbound + S (pfa_law_c_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddchosenresultcongruence pfa_offset_right_bottomlayeraddchosenresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddchosenresultcongruence = (pfa_law_c_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddchosenresultcongruence))))))))) /\ forall pfa_law_d_bottomlayer. (((exists pfa_gap_bottomlayeraddotherleft. pfa_gap_bottomlayeraddotherleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddotherright. pfa_gap_bottomlayeraddotherright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddotherresultbound. pfa_gap_bottomlayeraddotherresultbound + S (pfa_law_d_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddotherresultcongruence pfa_offset_right_bottomlayeraddotherresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddotherresultcongruence = (pfa_law_d_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddotherresultcongruence))))))))) -> pfa_law_d_bottomlayer = pfa_law_c_bottomlayer) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer pfa_law_c_bottomlayer. (((exists pfa_gap_bottomlayeraddcomm_firstleft. pfa_gap_bottomlayeraddcomm_firstleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddcomm_firstright. pfa_gap_bottomlayeraddcomm_firstright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddcomm_firstresultbound. pfa_gap_bottomlayeraddcomm_firstresultbound + S (pfa_law_c_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddcomm_firstresultcongruence pfa_offset_right_bottomlayeraddcomm_firstresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddcomm_firstresultcongruence = (pfa_law_c_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddcomm_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayeraddcomm_secondleft. pfa_gap_bottomlayeraddcomm_secondleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddcomm_secondright. pfa_gap_bottomlayeraddcomm_secondright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddcomm_secondresultbound. pfa_gap_bottomlayeraddcomm_secondresultbound + S (pfa_law_c_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddcomm_secondresultcongruence pfa_offset_right_bottomlayeraddcomm_secondresultcongruence. ((pfa_law_b_bottomlayer) + (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddcomm_secondresultcongruence = (pfa_law_c_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddcomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer pfa_law_c_bottomlayer pfa_law_x_bottomlayer pfa_law_y_bottomlayer pfa_law_u_bottomlayer pfa_law_v_bottomlayer. (((exists pfa_gap_bottomlayeraddassoc_firstleft. pfa_gap_bottomlayeraddassoc_firstleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddassoc_firstright. pfa_gap_bottomlayeraddassoc_firstright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddassoc_firstresultbound. pfa_gap_bottomlayeraddassoc_firstresultbound + S (pfa_law_x_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddassoc_firstresultcongruence pfa_offset_right_bottomlayeraddassoc_firstresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddassoc_firstresultcongruence = (pfa_law_x_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayeraddassoc_leftleft. pfa_gap_bottomlayeraddassoc_leftleft + S (pfa_law_x_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddassoc_leftright. pfa_gap_bottomlayeraddassoc_leftright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddassoc_leftresultbound. pfa_gap_bottomlayeraddassoc_leftresultbound + S (pfa_law_u_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddassoc_leftresultcongruence pfa_offset_right_bottomlayeraddassoc_leftresultcongruence. ((pfa_law_x_bottomlayer) + (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddassoc_leftresultcongruence = (pfa_law_u_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayeraddassoc_secondleft. pfa_gap_bottomlayeraddassoc_secondleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddassoc_secondright. pfa_gap_bottomlayeraddassoc_secondright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddassoc_secondresultbound. pfa_gap_bottomlayeraddassoc_secondresultbound + S (pfa_law_y_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddassoc_secondresultcongruence pfa_offset_right_bottomlayeraddassoc_secondresultcongruence. ((pfa_law_b_bottomlayer) + (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddassoc_secondresultcongruence = (pfa_law_y_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayeraddassoc_rightleft. pfa_gap_bottomlayeraddassoc_rightleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeraddassoc_rightright. pfa_gap_bottomlayeraddassoc_rightright + S (pfa_law_y_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddassoc_rightresultbound. pfa_gap_bottomlayeraddassoc_rightresultbound + S (pfa_law_v_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddassoc_rightresultcongruence pfa_offset_right_bottomlayeraddassoc_rightresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_y_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeraddassoc_rightresultcongruence = (pfa_law_v_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeraddassoc_rightresultcongruence))))))))) -> pfa_law_u_bottomlayer = pfa_law_v_bottomlayer) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer. (exists pfa_gap_bottomlayermultiplyleft. pfa_gap_bottomlayermultiplyleft + S (pfa_law_a_bottomlayer) = ((p))) -> (exists pfa_gap_bottomlayermultiplyright. pfa_gap_bottomlayermultiplyright + S (pfa_law_b_bottomlayer) = ((p))) -> exists pfa_law_c_bottomlayer. (((exists pfa_gap_bottomlayermultiplychosenleft. pfa_gap_bottomlayermultiplychosenleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplychosenright. pfa_gap_bottomlayermultiplychosenright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplychosenresultbound. pfa_gap_bottomlayermultiplychosenresultbound + S (pfa_law_c_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplychosenresultcongruence pfa_offset_right_bottomlayermultiplychosenresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplychosenresultcongruence = (pfa_law_c_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplychosenresultcongruence))))))))) /\ forall pfa_law_d_bottomlayer. (((exists pfa_gap_bottomlayermultiplyotherleft. pfa_gap_bottomlayermultiplyotherleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplyotherright. pfa_gap_bottomlayermultiplyotherright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplyotherresultbound. pfa_gap_bottomlayermultiplyotherresultbound + S (pfa_law_d_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplyotherresultcongruence pfa_offset_right_bottomlayermultiplyotherresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplyotherresultcongruence = (pfa_law_d_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplyotherresultcongruence))))))))) -> pfa_law_d_bottomlayer = pfa_law_c_bottomlayer) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer pfa_law_c_bottomlayer. (((exists pfa_gap_bottomlayermultiplycomm_firstleft. pfa_gap_bottomlayermultiplycomm_firstleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplycomm_firstright. pfa_gap_bottomlayermultiplycomm_firstright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplycomm_firstresultbound. pfa_gap_bottomlayermultiplycomm_firstresultbound + S (pfa_law_c_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplycomm_firstresultcongruence pfa_offset_right_bottomlayermultiplycomm_firstresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplycomm_firstresultcongruence = (pfa_law_c_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplycomm_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayermultiplycomm_secondleft. pfa_gap_bottomlayermultiplycomm_secondleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplycomm_secondright. pfa_gap_bottomlayermultiplycomm_secondright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplycomm_secondresultbound. pfa_gap_bottomlayermultiplycomm_secondresultbound + S (pfa_law_c_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplycomm_secondresultcongruence pfa_offset_right_bottomlayermultiplycomm_secondresultcongruence. ((pfa_law_b_bottomlayer) * (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplycomm_secondresultcongruence = (pfa_law_c_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplycomm_secondresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer pfa_law_c_bottomlayer pfa_law_x_bottomlayer pfa_law_y_bottomlayer pfa_law_u_bottomlayer pfa_law_v_bottomlayer. (((exists pfa_gap_bottomlayermultiplyassoc_firstleft. pfa_gap_bottomlayermultiplyassoc_firstleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplyassoc_firstright. pfa_gap_bottomlayermultiplyassoc_firstright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplyassoc_firstresultbound. pfa_gap_bottomlayermultiplyassoc_firstresultbound + S (pfa_law_x_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplyassoc_firstresultcongruence pfa_offset_right_bottomlayermultiplyassoc_firstresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplyassoc_firstresultcongruence = (pfa_law_x_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplyassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayermultiplyassoc_leftleft. pfa_gap_bottomlayermultiplyassoc_leftleft + S (pfa_law_x_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplyassoc_leftright. pfa_gap_bottomlayermultiplyassoc_leftright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplyassoc_leftresultbound. pfa_gap_bottomlayermultiplyassoc_leftresultbound + S (pfa_law_u_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplyassoc_leftresultcongruence pfa_offset_right_bottomlayermultiplyassoc_leftresultcongruence. ((pfa_law_x_bottomlayer) * (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplyassoc_leftresultcongruence = (pfa_law_u_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplyassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayermultiplyassoc_secondleft. pfa_gap_bottomlayermultiplyassoc_secondleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplyassoc_secondright. pfa_gap_bottomlayermultiplyassoc_secondright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplyassoc_secondresultbound. pfa_gap_bottomlayermultiplyassoc_secondresultbound + S (pfa_law_y_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplyassoc_secondresultcongruence pfa_offset_right_bottomlayermultiplyassoc_secondresultcongruence. ((pfa_law_b_bottomlayer) * (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplyassoc_secondresultcongruence = (pfa_law_y_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplyassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayermultiplyassoc_rightleft. pfa_gap_bottomlayermultiplyassoc_rightleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplyassoc_rightright. pfa_gap_bottomlayermultiplyassoc_rightright + S (pfa_law_y_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplyassoc_rightresultbound. pfa_gap_bottomlayermultiplyassoc_rightresultbound + S (pfa_law_v_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplyassoc_rightresultcongruence pfa_offset_right_bottomlayermultiplyassoc_rightresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_y_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiplyassoc_rightresultcongruence = (pfa_law_v_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiplyassoc_rightresultcongruence))))))))) -> pfa_law_u_bottomlayer = pfa_law_v_bottomlayer) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer pfa_law_c_bottomlayer pfa_law_s_bottomlayer pfa_law_x_bottomlayer pfa_law_y_bottomlayer pfa_law_u_bottomlayer pfa_law_v_bottomlayer. (((exists pfa_gap_bottomlayerleftdistribution_sumleft. pfa_gap_bottomlayerleftdistribution_sumleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerleftdistribution_sumright. pfa_gap_bottomlayerleftdistribution_sumright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerleftdistribution_sumresultbound. pfa_gap_bottomlayerleftdistribution_sumresultbound + S (pfa_law_s_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerleftdistribution_sumresultcongruence pfa_offset_right_bottomlayerleftdistribution_sumresultcongruence. ((pfa_law_b_bottomlayer) + (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerleftdistribution_sumresultcongruence = (pfa_law_s_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerleftdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerleftdistribution_leftleft. pfa_gap_bottomlayerleftdistribution_leftleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerleftdistribution_leftright. pfa_gap_bottomlayerleftdistribution_leftright + S (pfa_law_s_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerleftdistribution_leftresultbound. pfa_gap_bottomlayerleftdistribution_leftresultbound + S (pfa_law_u_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerleftdistribution_leftresultcongruence pfa_offset_right_bottomlayerleftdistribution_leftresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_s_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerleftdistribution_leftresultcongruence = (pfa_law_u_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerleftdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerleftdistribution_firstleft. pfa_gap_bottomlayerleftdistribution_firstleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerleftdistribution_firstright. pfa_gap_bottomlayerleftdistribution_firstright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerleftdistribution_firstresultbound. pfa_gap_bottomlayerleftdistribution_firstresultbound + S (pfa_law_x_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerleftdistribution_firstresultcongruence pfa_offset_right_bottomlayerleftdistribution_firstresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerleftdistribution_firstresultcongruence = (pfa_law_x_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerleftdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerleftdistribution_secondleft. pfa_gap_bottomlayerleftdistribution_secondleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerleftdistribution_secondright. pfa_gap_bottomlayerleftdistribution_secondright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerleftdistribution_secondresultbound. pfa_gap_bottomlayerleftdistribution_secondresultbound + S (pfa_law_y_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerleftdistribution_secondresultcongruence pfa_offset_right_bottomlayerleftdistribution_secondresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerleftdistribution_secondresultcongruence = (pfa_law_y_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerleftdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerleftdistribution_rightleft. pfa_gap_bottomlayerleftdistribution_rightleft + S (pfa_law_x_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerleftdistribution_rightright. pfa_gap_bottomlayerleftdistribution_rightright + S (pfa_law_y_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerleftdistribution_rightresultbound. pfa_gap_bottomlayerleftdistribution_rightresultbound + S (pfa_law_v_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerleftdistribution_rightresultcongruence pfa_offset_right_bottomlayerleftdistribution_rightresultcongruence. ((pfa_law_x_bottomlayer) + (pfa_law_y_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerleftdistribution_rightresultcongruence = (pfa_law_v_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerleftdistribution_rightresultcongruence))))))))) -> pfa_law_u_bottomlayer = pfa_law_v_bottomlayer) /\ (((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer pfa_law_c_bottomlayer pfa_law_s_bottomlayer pfa_law_x_bottomlayer pfa_law_y_bottomlayer pfa_law_u_bottomlayer pfa_law_v_bottomlayer. (((exists pfa_gap_bottomlayerrightdistribution_sumleft. pfa_gap_bottomlayerrightdistribution_sumleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerrightdistribution_sumright. pfa_gap_bottomlayerrightdistribution_sumright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerrightdistribution_sumresultbound. pfa_gap_bottomlayerrightdistribution_sumresultbound + S (pfa_law_s_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerrightdistribution_sumresultcongruence pfa_offset_right_bottomlayerrightdistribution_sumresultcongruence. ((pfa_law_b_bottomlayer) + (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerrightdistribution_sumresultcongruence = (pfa_law_s_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerrightdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerrightdistribution_leftleft. pfa_gap_bottomlayerrightdistribution_leftleft + S (pfa_law_s_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerrightdistribution_leftright. pfa_gap_bottomlayerrightdistribution_leftright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerrightdistribution_leftresultbound. pfa_gap_bottomlayerrightdistribution_leftresultbound + S (pfa_law_u_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerrightdistribution_leftresultcongruence pfa_offset_right_bottomlayerrightdistribution_leftresultcongruence. ((pfa_law_s_bottomlayer) * (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerrightdistribution_leftresultcongruence = (pfa_law_u_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerrightdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerrightdistribution_firstleft. pfa_gap_bottomlayerrightdistribution_firstleft + S (pfa_law_b_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerrightdistribution_firstright. pfa_gap_bottomlayerrightdistribution_firstright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerrightdistribution_firstresultbound. pfa_gap_bottomlayerrightdistribution_firstresultbound + S (pfa_law_x_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerrightdistribution_firstresultcongruence pfa_offset_right_bottomlayerrightdistribution_firstresultcongruence. ((pfa_law_b_bottomlayer) * (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerrightdistribution_firstresultcongruence = (pfa_law_x_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerrightdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerrightdistribution_secondleft. pfa_gap_bottomlayerrightdistribution_secondleft + S (pfa_law_c_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerrightdistribution_secondright. pfa_gap_bottomlayerrightdistribution_secondright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerrightdistribution_secondresultbound. pfa_gap_bottomlayerrightdistribution_secondresultbound + S (pfa_law_y_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerrightdistribution_secondresultcongruence pfa_offset_right_bottomlayerrightdistribution_secondresultcongruence. ((pfa_law_c_bottomlayer) * (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerrightdistribution_secondresultcongruence = (pfa_law_y_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerrightdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_bottomlayerrightdistribution_rightleft. pfa_gap_bottomlayerrightdistribution_rightleft + S (pfa_law_x_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerrightdistribution_rightright. pfa_gap_bottomlayerrightdistribution_rightright + S (pfa_law_y_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerrightdistribution_rightresultbound. pfa_gap_bottomlayerrightdistribution_rightresultbound + S (pfa_law_v_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerrightdistribution_rightresultcongruence pfa_offset_right_bottomlayerrightdistribution_rightresultcongruence. ((pfa_law_x_bottomlayer) + (pfa_law_y_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerrightdistribution_rightresultcongruence = (pfa_law_v_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerrightdistribution_rightresultcongruence))))))))) -> pfa_law_u_bottomlayer = pfa_law_v_bottomlayer) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayeradd_zero_rightinput. pfa_gap_bottomlayeradd_zero_rightinput + S (pfa_law_a_bottomlayer) = ((p))) -> (((exists pfa_gap_bottomlayeradd_zero_rightleft. pfa_gap_bottomlayeradd_zero_rightleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeradd_zero_rightright. pfa_gap_bottomlayeradd_zero_rightright + S (0) = ((p))) /\ ((((exists pfa_gap_bottomlayeradd_zero_rightresultbound. pfa_gap_bottomlayeradd_zero_rightresultbound + S (pfa_law_a_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeradd_zero_rightresultcongruence pfa_offset_right_bottomlayeradd_zero_rightresultcongruence. ((pfa_law_a_bottomlayer) + (0)) + ((p)) * pfa_offset_left_bottomlayeradd_zero_rightresultcongruence = (pfa_law_a_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeradd_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayeradd_zero_leftinput. pfa_gap_bottomlayeradd_zero_leftinput + S (pfa_law_a_bottomlayer) = ((p))) -> (((exists pfa_gap_bottomlayeradd_zero_leftleft. pfa_gap_bottomlayeradd_zero_leftleft + S (0) = ((p))) /\ (((exists pfa_gap_bottomlayeradd_zero_leftright. pfa_gap_bottomlayeradd_zero_leftright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeradd_zero_leftresultbound. pfa_gap_bottomlayeradd_zero_leftresultbound + S (pfa_law_a_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeradd_zero_leftresultcongruence pfa_offset_right_bottomlayeradd_zero_leftresultcongruence. ((0) + (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeradd_zero_leftresultcongruence = (pfa_law_a_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeradd_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayermultiply_one_rightinput. pfa_gap_bottomlayermultiply_one_rightinput + S (pfa_law_a_bottomlayer) = ((p))) -> (((exists pfa_gap_bottomlayermultiply_one_rightleft. pfa_gap_bottomlayermultiply_one_rightleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiply_one_rightright. pfa_gap_bottomlayermultiply_one_rightright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiply_one_rightresultbound. pfa_gap_bottomlayermultiply_one_rightresultbound + S (pfa_law_a_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiply_one_rightresultcongruence pfa_offset_right_bottomlayermultiply_one_rightresultcongruence. ((pfa_law_a_bottomlayer) * (1)) + ((p)) * pfa_offset_left_bottomlayermultiply_one_rightresultcongruence = (pfa_law_a_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiply_one_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayermultiply_one_leftinput. pfa_gap_bottomlayermultiply_one_leftinput + S (pfa_law_a_bottomlayer) = ((p))) -> (((exists pfa_gap_bottomlayermultiply_one_leftleft. pfa_gap_bottomlayermultiply_one_leftleft + S (1) = ((p))) /\ (((exists pfa_gap_bottomlayermultiply_one_leftright. pfa_gap_bottomlayermultiply_one_leftright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiply_one_leftresultbound. pfa_gap_bottomlayermultiply_one_leftresultbound + S (pfa_law_a_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiply_one_leftresultcongruence pfa_offset_right_bottomlayermultiply_one_leftresultcongruence. ((1) * (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiply_one_leftresultcongruence = (pfa_law_a_bottomlayer) + ((p)) * pfa_offset_right_bottomlayermultiply_one_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayermultiply_zero_rightinput. pfa_gap_bottomlayermultiply_zero_rightinput + S (pfa_law_a_bottomlayer) = ((p))) -> (((exists pfa_gap_bottomlayermultiply_zero_rightleft. pfa_gap_bottomlayermultiply_zero_rightleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayermultiply_zero_rightright. pfa_gap_bottomlayermultiply_zero_rightright + S (0) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiply_zero_rightresultbound. pfa_gap_bottomlayermultiply_zero_rightresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiply_zero_rightresultcongruence pfa_offset_right_bottomlayermultiply_zero_rightresultcongruence. ((pfa_law_a_bottomlayer) * (0)) + ((p)) * pfa_offset_left_bottomlayermultiply_zero_rightresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayermultiply_zero_rightresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayermultiply_zero_leftinput. pfa_gap_bottomlayermultiply_zero_leftinput + S (pfa_law_a_bottomlayer) = ((p))) -> (((exists pfa_gap_bottomlayermultiply_zero_leftleft. pfa_gap_bottomlayermultiply_zero_leftleft + S (0) = ((p))) /\ (((exists pfa_gap_bottomlayermultiply_zero_leftright. pfa_gap_bottomlayermultiply_zero_leftright + S (pfa_law_a_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiply_zero_leftresultbound. pfa_gap_bottomlayermultiply_zero_leftresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiply_zero_leftresultcongruence pfa_offset_right_bottomlayermultiply_zero_leftresultcongruence. ((0) * (pfa_law_a_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayermultiply_zero_leftresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayermultiply_zero_leftresultcongruence)))))))))) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayernegateinput. pfa_gap_bottomlayernegateinput + S (pfa_law_a_bottomlayer) = ((p))) -> exists pfa_law_b_bottomlayer. (((exists pfa_gap_bottomlayernegatechosenadditionleft. pfa_gap_bottomlayernegatechosenadditionleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayernegatechosenadditionright. pfa_gap_bottomlayernegatechosenadditionright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayernegatechosenadditionresultbound. pfa_gap_bottomlayernegatechosenadditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayernegatechosenadditionresultcongruence pfa_offset_right_bottomlayernegatechosenadditionresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayernegatechosenadditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayernegatechosenadditionresultcongruence))))))))) /\ forall pfa_law_c_bottomlayer. (((exists pfa_gap_bottomlayernegateotheradditionleft. pfa_gap_bottomlayernegateotheradditionleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayernegateotheradditionright. pfa_gap_bottomlayernegateotheradditionright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayernegateotheradditionresultbound. pfa_gap_bottomlayernegateotheradditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayernegateotheradditionresultcongruence pfa_offset_right_bottomlayernegateotheradditionresultcongruence. ((pfa_law_a_bottomlayer) + (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayernegateotheradditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayernegateotheradditionresultcongruence))))))))) -> pfa_law_c_bottomlayer = pfa_law_b_bottomlayer) /\ (((forall pfa_law_a_bottomlayer. (exists pfa_gap_bottomlayerinverseinput. pfa_gap_bottomlayerinverseinput + S (pfa_law_a_bottomlayer) = ((p))) -> ~(pfa_law_a_bottomlayer = 0) -> exists pfa_law_b_bottomlayer. (((~((pfa_law_a_bottomlayer) = 0)) /\ ((((exists pfa_gap_bottomlayerinversechosenmultiplicationleft. pfa_gap_bottomlayerinversechosenmultiplicationleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerinversechosenmultiplicationright. pfa_gap_bottomlayerinversechosenmultiplicationright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerinversechosenmultiplicationresultbound. pfa_gap_bottomlayerinversechosenmultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayerinversechosenmultiplicationresultcongruence pfa_offset_right_bottomlayerinversechosenmultiplicationresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerinversechosenmultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayerinversechosenmultiplicationresultcongruence)))))))))))) /\ forall pfa_law_c_bottomlayer. (((~((pfa_law_a_bottomlayer) = 0)) /\ ((((exists pfa_gap_bottomlayerinverseothermultiplicationleft. pfa_gap_bottomlayerinverseothermultiplicationleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayerinverseothermultiplicationright. pfa_gap_bottomlayerinverseothermultiplicationright + S (pfa_law_c_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayerinverseothermultiplicationresultbound. pfa_gap_bottomlayerinverseothermultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayerinverseothermultiplicationresultcongruence pfa_offset_right_bottomlayerinverseothermultiplicationresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_c_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayerinverseothermultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayerinverseothermultiplicationresultcongruence)))))))))))) -> pfa_law_c_bottomlayer = pfa_law_b_bottomlayer) /\ ((forall pfa_law_a_bottomlayer pfa_law_b_bottomlayer. (((exists pfa_gap_bottomlayernozeroleft. pfa_gap_bottomlayernozeroleft + S (pfa_law_a_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayernozeroright. pfa_gap_bottomlayernozeroright + S (pfa_law_b_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayernozeroresultbound. pfa_gap_bottomlayernozeroresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayernozeroresultcongruence pfa_offset_right_bottomlayernozeroresultcongruence. ((pfa_law_a_bottomlayer) * (pfa_law_b_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayernozeroresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayernozeroresultcongruence))))))))) -> pfa_law_a_bottomlayer = 0 \/ pfa_law_b_bottomlayer = 0)))))))))))))))))))))))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.