ND0229 — FpAdd(p,a,b,c)

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

Lt(a,p) ∧ (Lt(b,p) ∧ CanonicalModularResidue(p,a + b,c))

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition

((exists pfa_gap_bottomlayerleft. pfa_gap_bottomlayerleft + S ((a)) = ((p))) /\ (((exists pfa_gap_bottomlayerright. pfa_gap_bottomlayerright + S ((b)) = ((p))) /\ ((((exists pfa_gap_bottomlayerresultbound. pfa_gap_bottomlayerresultbound + S ((c)) = ((p))) /\ ((exists pfa_offset_left_bottomlayerresultcongruence pfa_offset_right_bottomlayerresultcongruence. (((a)) + ((b))) + ((p)) * pfa_offset_left_bottomlayerresultcongruence = ((c)) + ((p)) * pfa_offset_right_bottomlayerresultcongruence))))))))

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

Direct definition dependencies

Lt(a,b)CanonicalModularResidue(m,a,r)

Definitions depending on this notation

FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)FpHornerStep(p,b,c,x,u,v,i)FpNeg(p,a,b)FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L)

Checked theorems using this definition