ND0270 — FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)

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

∀ pfp_index_lowertier. Lt(pfp_index_lowertier,l) → ∃ x. ∃ y. ∃ z. BetaAt(ab,ac,pfp_index_lowertier,x) ∧ (BetaAt(bb,bc,pfp_index_lowertier,y) ∧ (BetaAt(cb,cc,pfp_index_lowertier,z) ∧ FpAdd(p,x,y,z)))

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

Hygienic expanded first-order definition

forall pfp_index_lowertier. (exists pfa_gap_lowertierindex. pfa_gap_lowertierindex + S (pfp_index_lowertier) = ((l))) -> exists pfp_left_lowertier pfp_right_lowertier pfp_value_lowertier. ((((exists ff_h_pfp_lowertierleft. ff_h_pfp_lowertierleft + S (pfp_left_lowertier) = S ((S (pfp_index_lowertier)) * (ac))) /\ exists ff_q_pfp_lowertierleft. (ab) = ff_q_pfp_lowertierleft * S ((S (pfp_index_lowertier)) * (ac)) + (pfp_left_lowertier))) /\ (((((exists ff_h_pfp_lowertierright. ff_h_pfp_lowertierright + S (pfp_right_lowertier) = S ((S (pfp_index_lowertier)) * (bc))) /\ exists ff_q_pfp_lowertierright. (bb) = ff_q_pfp_lowertierright * S ((S (pfp_index_lowertier)) * (bc)) + (pfp_right_lowertier))) /\ (((((exists ff_h_pfp_lowertiertarget. ff_h_pfp_lowertiertarget + S (pfp_value_lowertier) = S ((S (pfp_index_lowertier)) * (cc))) /\ exists ff_q_pfp_lowertiertarget. (cb) = ff_q_pfp_lowertiertarget * S ((S (pfp_index_lowertier)) * (cc)) + (pfp_value_lowertier))) /\ ((((exists pfa_gap_lowertieroperationleft. pfa_gap_lowertieroperationleft + S (pfp_left_lowertier) = ((p))) /\ (((exists pfa_gap_lowertieroperationright. pfa_gap_lowertieroperationright + S (pfp_right_lowertier) = ((p))) /\ ((((exists pfa_gap_lowertieroperationresultbound. pfa_gap_lowertieroperationresultbound + S (pfp_value_lowertier) = ((p))) /\ ((exists pfa_offset_left_lowertieroperationresultcongruence pfa_offset_right_lowertieroperationresultcongruence. ((pfp_left_lowertier) + (pfp_right_lowertier)) + ((p)) * pfa_offset_left_lowertieroperationresultcongruence = (pfp_value_lowertier) + ((p)) * pfa_offset_right_lowertieroperationresultcongruence)))))))))))))))

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)BetaAt(b,c,i,x)FpAdd(p,a,b,c)

Definitions depending on this notation

none

Checked theorems using this definition