Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∃ pfh_coefficient_lowertier. ∃ pfh_before_lowertier. ∃ pfh_after_lowertier. ∃ pfh_product_lowertier. BetaAt(b,c,i,pfh_coefficient_lowertier) ∧ (BetaAt(u,v,i,pfh_before_lowertier) ∧ (BetaAt(u,v,S i,pfh_after_lowertier) ∧ (FpMul(p,pfh_before_lowertier,x,pfh_product_lowertier) ∧ FpAdd(p,pfh_product_lowertier,pfh_coefficient_lowertier,pfh_after_lowertier))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists pfh_coefficient_lowertier pfh_before_lowertier pfh_after_lowertier pfh_product_lowertier. ((((exists ff_h_pfp_lowertiercoefficient. ff_h_pfp_lowertiercoefficient + S (pfh_coefficient_lowertier) = S ((S ((i))) * (c))) /\ exists ff_q_pfp_lowertiercoefficient. (b) = ff_q_pfp_lowertiercoefficient * S ((S ((i))) * (c)) + (pfh_coefficient_lowertier))) /\ (((((exists ff_h_pfp_lowertierbefore. ff_h_pfp_lowertierbefore + S (pfh_before_lowertier) = S ((S ((i))) * (v))) /\ exists ff_q_pfp_lowertierbefore. (u) = ff_q_pfp_lowertierbefore * S ((S ((i))) * (v)) + (pfh_before_lowertier))) /\ (((((exists ff_h_pfp_lowertierafter. ff_h_pfp_lowertierafter + S (pfh_after_lowertier) = S ((S (S ((i)))) * (v))) /\ exists ff_q_pfp_lowertierafter. (u) = ff_q_pfp_lowertierafter * S ((S (S ((i)))) * (v)) + (pfh_after_lowertier))) /\ (((((exists pfa_gap_lowertiermultiplyleft. pfa_gap_lowertiermultiplyleft + S (pfh_before_lowertier) = ((p))) /\ (((exists pfa_gap_lowertiermultiplyright. pfa_gap_lowertiermultiplyright + S ((x)) = ((p))) /\ ((((exists pfa_gap_lowertiermultiplyresultbound. pfa_gap_lowertiermultiplyresultbound + S (pfh_product_lowertier) = ((p))) /\ ((exists pfa_offset_left_lowertiermultiplyresultcongruence pfa_offset_right_lowertiermultiplyresultcongruence. ((pfh_before_lowertier) * ((x))) + ((p)) * pfa_offset_left_lowertiermultiplyresultcongruence = (pfh_product_lowertier) + ((p)) * pfa_offset_right_lowertiermultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_lowertieraddleft. pfa_gap_lowertieraddleft + S (pfh_product_lowertier) = ((p))) /\ (((exists pfa_gap_lowertieraddright. pfa_gap_lowertieraddright + S (pfh_coefficient_lowertier) = ((p))) /\ ((((exists pfa_gap_lowertieraddresultbound. pfa_gap_lowertieraddresultbound + S (pfh_after_lowertier) = ((p))) /\ ((exists pfa_offset_left_lowertieraddresultcongruence pfa_offset_right_lowertieraddresultcongruence. ((pfh_product_lowertier) + (pfh_coefficient_lowertier)) + ((p)) * pfa_offset_left_lowertieraddresultcongruence = (pfh_after_lowertier) + ((p)) * pfa_offset_right_lowertieraddresultcongruence)))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
none directly; see definition consumers