ND0328 — FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,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

∀ pfs_index_polynomial_division_definition. Lt(pfs_index_polynomial_division_definition,L) → ∃ x. ∃ y. ∃ z. BetaAt(ab,ac,pfs_index_polynomial_division_definition,x) ∧ (BetaAt(bb,bc,pfs_index_polynomial_division_definition,y) ∧ (BetaAt(rb,rc,pfs_index_polynomial_division_definition,z) ∧ FpAdd(p,y,z,x)))

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

Hygienic expanded first-order definition

forall pfs_index_polynomial_division_definition. (exists pfa_gap_polynomial_division_definitionindex. pfa_gap_polynomial_division_definitionindex + S (pfs_index_polynomial_division_definition) = ((L))) -> exists pfs_left_polynomial_division_definition pfs_right_polynomial_division_definition pfs_result_polynomial_division_definition. ((((exists ff_h_pfp_polynomial_division_definitionleft. ff_h_pfp_polynomial_division_definitionleft + S (pfs_left_polynomial_division_definition) = S ((S (pfs_index_polynomial_division_definition)) * (ac))) /\ exists ff_q_pfp_polynomial_division_definitionleft. (ab) = ff_q_pfp_polynomial_division_definitionleft * S ((S (pfs_index_polynomial_division_definition)) * (ac)) + (pfs_left_polynomial_division_definition))) /\ (((((exists ff_h_pfp_polynomial_division_definitionright. ff_h_pfp_polynomial_division_definitionright + S (pfs_right_polynomial_division_definition) = S ((S (pfs_index_polynomial_division_definition)) * (bc))) /\ exists ff_q_pfp_polynomial_division_definitionright. (bb) = ff_q_pfp_polynomial_division_definitionright * S ((S (pfs_index_polynomial_division_definition)) * (bc)) + (pfs_right_polynomial_division_definition))) /\ (((((exists ff_h_pfp_polynomial_division_definitionresult. ff_h_pfp_polynomial_division_definitionresult + S (pfs_result_polynomial_division_definition) = S ((S (pfs_index_polynomial_division_definition)) * (rc))) /\ exists ff_q_pfp_polynomial_division_definitionresult. (rb) = ff_q_pfp_polynomial_division_definitionresult * S ((S (pfs_index_polynomial_division_definition)) * (rc)) + (pfs_result_polynomial_division_definition))) /\ ((((exists pfa_gap_polynomial_division_definitionoperationleft. pfa_gap_polynomial_division_definitionoperationleft + S (pfs_right_polynomial_division_definition) = ((p))) /\ (((exists pfa_gap_polynomial_division_definitionoperationright. pfa_gap_polynomial_division_definitionoperationright + S (pfs_result_polynomial_division_definition) = ((p))) /\ ((((exists pfa_gap_polynomial_division_definitionoperationresultbound. pfa_gap_polynomial_division_definitionoperationresultbound + S (pfs_left_polynomial_division_definition) = ((p))) /\ ((exists pfa_offset_left_polynomial_division_definitionoperationresultcongruence pfa_offset_right_polynomial_division_definitionoperationresultcongruence. ((pfs_right_polynomial_division_definition) + (pfs_result_polynomial_division_definition)) + ((p)) * pfa_offset_left_polynomial_division_definitionoperationresultcongruence = (pfs_left_polynomial_division_definition) + ((p)) * pfa_offset_right_polynomial_division_definitionoperationresultcongruence)))))))))))))))

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