| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1986 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (368 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (668 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (622 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (129 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Global Index
A
addEnd [definition, in Buchberger.BuchAux]addEnd_incl [lemma, in Buchberger.Buch]
addEnd_app [lemma, in Buchberger.BuchAux]
addEnd_id2 [lemma, in Buchberger.BuchAux]
addEnd_id1 [lemma, in Buchberger.BuchAux]
addEnd_cons [lemma, in Buchberger.BuchAux]
addEnd1 [abbreviation, in Buchberger.WfR0]
addEnd1 [abbreviation, in Buchberger.Buch]
addEnd1 [abbreviation, in Buchberger.BuchRed]
addRes [definition, in Buchberger.Buch]
app2_inv [lemma, in Buchberger.POrder]
A_sep [lemma, in Buchberger.moreCoefStructure]
A1_diff_A0 [projection, in Buchberger.CoefStructure]
B
Bad [definition, in Buchberger.Bar]BadM [definition, in Buchberger.WfR0]
Bar [inductive, in Buchberger.Bar]
Bar [library]
Base [constructor, in Buchberger.Bar]
buch [definition, in Buchberger.Buch]
Buch [section, in Buchberger.Buch]
Buch [library]
BuchAux [section, in Buchberger.BuchAux]
BuchAux [library]
BuchAux.A [variable, in Buchberger.BuchAux]
BuchAux.A0 [variable, in Buchberger.BuchAux]
BuchAux.A1 [variable, in Buchberger.BuchAux]
BuchAux.cs [variable, in Buchberger.BuchAux]
BuchAux.divA [variable, in Buchberger.BuchAux]
BuchAux.eqA [variable, in Buchberger.BuchAux]
BuchAux.eqA_dec [variable, in Buchberger.BuchAux]
BuchAux.invA [variable, in Buchberger.BuchAux]
BuchAux.ltM [variable, in Buchberger.BuchAux]
BuchAux.ltM_dec [variable, in Buchberger.BuchAux]
BuchAux.minusA [variable, in Buchberger.BuchAux]
BuchAux.multA [variable, in Buchberger.BuchAux]
BuchAux.n [variable, in Buchberger.BuchAux]
BuchAux.os [variable, in Buchberger.BuchAux]
BuchAux.plusA [variable, in Buchberger.BuchAux]
BuchRed [section, in Buchberger.BuchRed]
BuchRed [library]
BuchRed.A [variable, in Buchberger.BuchRed]
BuchRed.A0 [variable, in Buchberger.BuchRed]
BuchRed.A1 [variable, in Buchberger.BuchRed]
BuchRed.cs [variable, in Buchberger.BuchRed]
BuchRed.divA [variable, in Buchberger.BuchRed]
BuchRed.eqA [variable, in Buchberger.BuchRed]
BuchRed.eqA_dec [variable, in Buchberger.BuchRed]
BuchRed.invA [variable, in Buchberger.BuchRed]
BuchRed.ltM [variable, in Buchberger.BuchRed]
BuchRed.ltM_dec [variable, in Buchberger.BuchRed]
BuchRed.minusA [variable, in Buchberger.BuchRed]
BuchRed.multA [variable, in Buchberger.BuchRed]
BuchRed.n [variable, in Buchberger.BuchRed]
BuchRed.os [variable, in Buchberger.BuchRed]
BuchRed.plusA [variable, in Buchberger.BuchRed]
buch_Grobner [lemma, in Buchberger.Buch]
buch_spolyQ [lemma, in Buchberger.Buch]
buch_reds [lemma, in Buchberger.Buch]
buch_Stable [lemma, in Buchberger.Buch]
Buch.A [variable, in Buchberger.Buch]
Buch.A0 [variable, in Buchberger.Buch]
Buch.A1 [variable, in Buchberger.Buch]
Buch.Co [variable, in Buchberger.Buch]
Buch.cs [variable, in Buchberger.Buch]
Buch.divA [variable, in Buchberger.Buch]
Buch.eqA [variable, in Buchberger.Buch]
Buch.eqA_dec [variable, in Buchberger.Buch]
Buch.FPset [variable, in Buchberger.Buch]
Buch.invA [variable, in Buchberger.Buch]
Buch.ltM [variable, in Buchberger.Buch]
Buch.ltM_dec [variable, in Buchberger.Buch]
Buch.minusA [variable, in Buchberger.Buch]
Buch.multA [variable, in Buchberger.Buch]
Buch.n [variable, in Buchberger.Buch]
Buch.os [variable, in Buchberger.Buch]
Buch.plusA [variable, in Buchberger.Buch]
buch1 [abbreviation, in Buchberger.BuchRed]
C
canonical [definition, in Buchberger.POrder]canonicalpO [lemma, in Buchberger.Peq]
canonicalp1 [lemma, in Buchberger.Peq]
canonical_reduce [lemma, in Buchberger.Preduce]
canonical_imp_in_nzero [lemma, in Buchberger.POrder]
canonical_pX_ltP [lemma, in Buchberger.POrder]
canonical_skip_fst [lemma, in Buchberger.POrder]
canonical_imp_canonical [lemma, in Buchberger.POrder]
canonical_pX_order [lemma, in Buchberger.POrder]
canonical_pX_eqT [lemma, in Buchberger.POrder]
canonical_cons [lemma, in Buchberger.POrder]
canonical_nzeroP [lemma, in Buchberger.POrder]
canonical_ltT [lemma, in Buchberger.POrder]
canonical_imp_olist [lemma, in Buchberger.POrder]
canonical_s2p [lemma, in Buchberger.BuchAux]
canonical_reduceplus [lemma, in Buchberger.Preduceplus]
canonical_mults_inv [lemma, in Buchberger.Pmults]
canonical_mults [lemma, in Buchberger.Pmults]
canonical_minuspf [lemma, in Buchberger.Pminus]
canonical_minusP [lemma, in Buchberger.Pminus]
canonical_Dmult [lemma, in Buchberger.Pcrit]
canonical_Rminus [lemma, in Buchberger.Pcrit]
canonical_spminusf_full_t [lemma, in Buchberger.Pspminus]
canonical_spminusf_full [lemma, in Buchberger.Pspminus]
canonical_spminusf [lemma, in Buchberger.Pspminus]
canonical_pluspf [lemma, in Buchberger.Pplus]
canonical_plusP [lemma, in Buchberger.Pplus]
canonical_multpf [lemma, in Buchberger.Pmult]
canonical0 [lemma, in Buchberger.POrder]
canonical1 [abbreviation, in Buchberger.Preduce]
canonical1 [abbreviation, in Buchberger.Peq]
canonical1 [abbreviation, in Buchberger.WfR0]
canonical1 [abbreviation, in Buchberger.Buch]
canonical1 [abbreviation, in Buchberger.BuchAux]
canonical1 [abbreviation, in Buchberger.Preduceplus]
canonical1 [abbreviation, in Buchberger.Pmults]
canonical1 [abbreviation, in Buchberger.Preducestar]
canonical1 [abbreviation, in Buchberger.Preducestar]
canonical1 [abbreviation, in Buchberger.BuchRed]
canonical1 [abbreviation, in Buchberger.Pminus]
canonical1 [abbreviation, in Buchberger.Pspoly]
canonical1 [abbreviation, in Buchberger.Pcrit]
canonical1 [abbreviation, in Buchberger.Pcomb]
canonical1 [abbreviation, in Buchberger.Pspminus]
canonical1 [abbreviation, in Buchberger.Pplus]
canonical1 [abbreviation, in Buchberger.Pmult]
Cb [definition, in Buchberger.BuchAux]
Cb_genPcPf [lemma, in Buchberger.Buch]
Cb_genPcP [lemma, in Buchberger.Buch]
Cb_stable [lemma, in Buchberger.Buch]
Cb_sp [lemma, in Buchberger.BuchAux]
Cb_in [lemma, in Buchberger.BuchAux]
Cb_in1 [lemma, in Buchberger.BuchAux]
Cb_incl [lemma, in Buchberger.BuchAux]
Cb_trans [lemma, in Buchberger.BuchAux]
Cb_id [lemma, in Buchberger.BuchAux]
cb_Red_cb2 [lemma, in Buchberger.BuchRed]
cb_Red_cb1 [lemma, in Buchberger.BuchRed]
Cb_Red [lemma, in Buchberger.BuchRed]
cb_redacc [lemma, in Buchberger.BuchRed]
Cb_compo [lemma, in Buchberger.BuchRed]
Cb_nf [lemma, in Buchberger.BuchRed]
Cb_comp [lemma, in Buchberger.BuchRed]
Cb_cons [lemma, in Buchberger.BuchRed]
Cb_trans_cons [lemma, in Buchberger.BuchRed]
Cb_cons_addEnd [lemma, in Buchberger.BuchRed]
Cb_addEnd_cons [lemma, in Buchberger.BuchRed]
cb_red_cb2 [lemma, in Buchberger.Fred]
cb_red_cb1 [lemma, in Buchberger.Fred]
cb_red [lemma, in Buchberger.Fred]
cb_redacc [lemma, in Buchberger.Fred]
Cb1 [abbreviation, in Buchberger.WfR0]
Cb1 [abbreviation, in Buchberger.Buch]
Cb1 [abbreviation, in Buchberger.BuchRed]
cmin [constructor, in Buchberger.OpenIndGoodRel]
CoefStructure [record, in Buchberger.CoefStructure]
CoefStructure [library]
CombLinear [inductive, in Buchberger.Pcomb]
CombLinear_trans1 [lemma, in Buchberger.BuchAux]
CombLinear_compo [lemma, in Buchberger.Pcomb]
CombLinear_trans_cons_lem [lemma, in Buchberger.Pcomb]
CombLinear_incl [lemma, in Buchberger.Pcomb]
CombLinear_reducestar [lemma, in Buchberger.Pcomb]
CombLinear_reduceplus [lemma, in Buchberger.Pcomb]
CombLinear_reduce [lemma, in Buchberger.Pcomb]
CombLinear_spoly [lemma, in Buchberger.Pcomb]
CombLinear_id [lemma, in Buchberger.Pcomb]
CombLinear_minuspf [lemma, in Buchberger.Pcomb]
CombLinear_mults1 [lemma, in Buchberger.Pcomb]
CombLinear_pluspf [lemma, in Buchberger.Pcomb]
CombLinear_comp [lemma, in Buchberger.Pcomb]
CombLinear_canonical [lemma, in Buchberger.Pcomb]
CombLinear_1 [constructor, in Buchberger.Pcomb]
CombLinear_0 [constructor, in Buchberger.Pcomb]
CombLinear1 [abbreviation, in Buchberger.WfR0]
CombLinear1 [abbreviation, in Buchberger.Buch]
CombLinear1 [abbreviation, in Buchberger.BuchAux]
CombLinear1 [abbreviation, in Buchberger.BuchRed]
Confluent [inductive, in Buchberger.Pspoly]
ConfluentReduce [inductive, in Buchberger.Pcomb]
ConfluentReduce_imp_Grobner [lemma, in Buchberger.Pcomb]
ConfluentReduce0 [constructor, in Buchberger.Pcomb]
Confluent0 [constructor, in Buchberger.Pspoly]
confl_reducestar [lemma, in Buchberger.Pspoly]
confl_restar [lemma, in Buchberger.Pspoly]
confl_mix [lemma, in Buchberger.Pspoly]
confl_top [lemma, in Buchberger.Pspoly]
confl_top_simpl [lemma, in Buchberger.Pspoly]
confl_under [lemma, in Buchberger.Pspoly]
Conf_trans [lemma, in Buchberger.Pspoly]
Conf_inv1 [lemma, in Buchberger.Pspoly]
consGRBar [lemma, in Buchberger.Bar]
cpRes [inductive, in Buchberger.Buch]
crit [section, in Buchberger.Pcrit]
crit.A [variable, in Buchberger.Pcrit]
crit.A0 [variable, in Buchberger.Pcrit]
crit.A1 [variable, in Buchberger.Pcrit]
crit.cs [variable, in Buchberger.Pcrit]
crit.divA [variable, in Buchberger.Pcrit]
crit.eqA [variable, in Buchberger.Pcrit]
crit.eqA_dec [variable, in Buchberger.Pcrit]
crit.invA [variable, in Buchberger.Pcrit]
crit.ltM [variable, in Buchberger.Pcrit]
crit.ltM_dec [variable, in Buchberger.Pcrit]
crit.minusA [variable, in Buchberger.Pcrit]
crit.multA [variable, in Buchberger.Pcrit]
crit.n [variable, in Buchberger.Pcrit]
crit.os [variable, in Buchberger.Pcrit]
crit.plusA [variable, in Buchberger.Pcrit]
c_n [constructor, in Buchberger.Monomials]
D
DecRel [definition, in Buchberger.Dickson]dec_lt [lemma, in Buchberger.Dickson]
def_grobner [lemma, in Buchberger.BuchRed]
degc [definition, in Buchberger.LexiOrder]
descA_subst [lemma, in Buchberger.POrder]
Dickson [section, in Buchberger.Dickson]
Dickson [library]
dicksonL [lemma, in Buchberger.Dickson]
Dickson.A [variable, in Buchberger.Dickson]
Dickson.B [variable, in Buchberger.Dickson]
Dickson.declt [variable, in Buchberger.Dickson]
Dickson.lt [variable, in Buchberger.Dickson]
Dickson.R [variable, in Buchberger.Dickson]
Dickson.wfgt [variable, in Buchberger.Dickson]
Dickson.wR [variable, in Buchberger.Dickson]
divA_invA_r [projection, in Buchberger.CoefStructure]
divA_multA_comp_r [projection, in Buchberger.CoefStructure]
divA_eqA_comp [projection, in Buchberger.CoefStructure]
divA_is_multA [projection, in Buchberger.CoefStructure]
divA_rew [projection, in Buchberger.CoefStructure]
divA_nZ [lemma, in Buchberger.BuchAux]
divA_nZ [lemma, in Buchberger.moreCoefStructure]
divA_A1 [lemma, in Buchberger.moreCoefStructure]
divA_A0_l [lemma, in Buchberger.moreCoefStructure]
divA_multA_comp_l [lemma, in Buchberger.moreCoefStructure]
divp [definition, in Buchberger.BuchAux]
divP [inductive, in Buchberger.DivTerm]
divpf [definition, in Buchberger.Pcrit]
divpf_comp [lemma, in Buchberger.Pcrit]
divpf_canonical [lemma, in Buchberger.Pcrit]
divPp [definition, in Buchberger.Pcrit]
divPp_mults1 [lemma, in Buchberger.Pcrit]
divPp_divpf [lemma, in Buchberger.Pcrit]
divp_trans1 [abbreviation, in Buchberger.WfR0]
divp_dec1 [abbreviation, in Buchberger.WfR0]
divp_trans1 [abbreviation, in Buchberger.Buch]
divp_dec1 [abbreviation, in Buchberger.Buch]
divP_ppc [lemma, in Buchberger.BuchAux]
divp_nzeropr [lemma, in Buchberger.BuchAux]
divp_nzeropl [lemma, in Buchberger.BuchAux]
divp_ppc [lemma, in Buchberger.BuchAux]
divp_dec [lemma, in Buchberger.BuchAux]
divp_trans [lemma, in Buchberger.BuchAux]
divp_id [lemma, in Buchberger.BuchRed]
divp_reduce1 [lemma, in Buchberger.BuchRed]
divp_trans1 [abbreviation, in Buchberger.BuchRed]
divp_dec1 [abbreviation, in Buchberger.BuchRed]
divp_is_multTerm [lemma, in Buchberger.Pcrit]
divP_minusTerm_comp [lemma, in Buchberger.Pspminus]
divP_ltT_comp [lemma, in Buchberger.Pspminus]
divP_is_not_order [lemma, in Buchberger.Pspminus]
divP_eqT [lemma, in Buchberger.DivTerm]
divP_dec [lemma, in Buchberger.DivTerm]
divP_comp_ppc1 [lemma, in Buchberger.DivTerm]
divP_comp_ppc0 [lemma, in Buchberger.DivTerm]
divP_ppcr [lemma, in Buchberger.DivTerm]
divP_ppcl [lemma, in Buchberger.DivTerm]
divP_multTerm_r [lemma, in Buchberger.DivTerm]
divP_multTerm_l [lemma, in Buchberger.DivTerm]
divP_comp [lemma, in Buchberger.DivTerm]
divP_on_eqT_eqT [lemma, in Buchberger.DivTerm]
divP_on_eqT [lemma, in Buchberger.DivTerm]
divP_eqTerm_comp [lemma, in Buchberger.DivTerm]
divP_nZero [lemma, in Buchberger.DivTerm]
divP_trans [lemma, in Buchberger.DivTerm]
divP_invTerm_r [lemma, in Buchberger.DivTerm]
divP_invTerm_l [lemma, in Buchberger.DivTerm]
divP_plusTerm [lemma, in Buchberger.DivTerm]
divP_inv3 [lemma, in Buchberger.DivTerm]
divP_inv2 [lemma, in Buchberger.DivTerm]
divP_inv1 [lemma, in Buchberger.DivTerm]
divP1 [abbreviation, in Buchberger.Preduce]
divp1 [abbreviation, in Buchberger.WfR0]
divP1 [abbreviation, in Buchberger.WfR0]
divp1 [abbreviation, in Buchberger.Buch]
divP1 [abbreviation, in Buchberger.Buch]
divP1 [abbreviation, in Buchberger.BuchAux]
divP1 [abbreviation, in Buchberger.Preduceplus]
divP1 [abbreviation, in Buchberger.Preducestar]
divP1 [abbreviation, in Buchberger.Preducestar]
divp1 [abbreviation, in Buchberger.BuchRed]
divP1 [abbreviation, in Buchberger.BuchRed]
divP1 [abbreviation, in Buchberger.Pspoly]
divP1 [abbreviation, in Buchberger.Pcrit]
divP1 [abbreviation, in Buchberger.Pcomb]
divP1 [abbreviation, in Buchberger.Pspminus]
divTerm [definition, in Buchberger.DivTerm]
DivTerm [section, in Buchberger.DivTerm]
DivTerm [library]
divTerm_compo [lemma, in Buchberger.DivTerm]
divTerm_multTermr [lemma, in Buchberger.DivTerm]
divTerm_multTerml [lemma, in Buchberger.DivTerm]
divTerm_def [constructor, in Buchberger.DivTerm]
divTerm_rew [lemma, in Buchberger.DivTerm]
divTerm_ppcr [lemma, in Buchberger.DivTerm]
divTerm_ppcl [lemma, in Buchberger.DivTerm]
divTerm_ppc [lemma, in Buchberger.DivTerm]
divTerm_on_plusM_minusM [lemma, in Buchberger.DivTerm]
divTerm_on_eqT_eqT [lemma, in Buchberger.DivTerm]
divTerm_on_eqT [lemma, in Buchberger.DivTerm]
divTerm_dec [lemma, in Buchberger.DivTerm]
divTerm_eqT [lemma, in Buchberger.DivTerm]
divTerm_nZ [lemma, in Buchberger.DivTerm]
divTerm_multTerm_r [lemma, in Buchberger.DivTerm]
divTerm_multTerm_l [lemma, in Buchberger.DivTerm]
divTerm_invTerm_r [lemma, in Buchberger.DivTerm]
divTerm_invTerm_l [lemma, in Buchberger.DivTerm]
DivTerm.A [variable, in Buchberger.DivTerm]
DivTerm.A0 [variable, in Buchberger.DivTerm]
DivTerm.A1 [variable, in Buchberger.DivTerm]
DivTerm.cs [variable, in Buchberger.DivTerm]
DivTerm.divA [variable, in Buchberger.DivTerm]
DivTerm.eqA [variable, in Buchberger.DivTerm]
DivTerm.eqA_dec [variable, in Buchberger.DivTerm]
DivTerm.gb [variable, in Buchberger.DivTerm]
DivTerm.gm [variable, in Buchberger.DivTerm]
DivTerm.invA [variable, in Buchberger.DivTerm]
DivTerm.ltM [variable, in Buchberger.DivTerm]
DivTerm.ltM_dec [variable, in Buchberger.DivTerm]
DivTerm.minusA [variable, in Buchberger.DivTerm]
DivTerm.multA [variable, in Buchberger.DivTerm]
DivTerm.n [variable, in Buchberger.DivTerm]
DivTerm.os [variable, in Buchberger.DivTerm]
DivTerm.plusA [variable, in Buchberger.DivTerm]
divTerm1 [abbreviation, in Buchberger.Preduce]
divTerm1 [abbreviation, in Buchberger.WfR0]
divTerm1 [abbreviation, in Buchberger.Buch]
divTerm1 [abbreviation, in Buchberger.BuchAux]
divTerm1 [abbreviation, in Buchberger.Preduceplus]
divTerm1 [abbreviation, in Buchberger.Preducestar]
divTerm1 [abbreviation, in Buchberger.Preducestar]
divTerm1 [abbreviation, in Buchberger.BuchRed]
divTerm1 [abbreviation, in Buchberger.Pspoly]
divTerm1 [abbreviation, in Buchberger.Pcrit]
divTerm1 [abbreviation, in Buchberger.Pcomb]
divTerm1 [abbreviation, in Buchberger.Pspminus]
div_clean_dec1 [lemma, in Buchberger.Monomials]
div_clean_dec2 [lemma, in Buchberger.Monomials]
div_mon_clean [definition, in Buchberger.Monomials]
div_mon [definition, in Buchberger.Monomials]
div_is_T1 [lemma, in Buchberger.DivTerm]
Dmult [definition, in Buchberger.Pcrit]
Dmult_is_mulpf [lemma, in Buchberger.Pcrit]
DontKeep [constructor, in Buchberger.Buch]
E
eqA_trans [projection, in Buchberger.CoefStructure]eqA_sym [projection, in Buchberger.CoefStructure]
eqA_ref [projection, in Buchberger.CoefStructure]
eqA_A0 [lemma, in Buchberger.moreCoefStructure]
eqA0_right [lemma, in Buchberger.moreCoefStructure]
eqA0_left [lemma, in Buchberger.moreCoefStructure]
eqmon_dec [lemma, in Buchberger.Monomials]
eqP [inductive, in Buchberger.Peq]
eqPf [definition, in Buchberger.Peq]
eqpP1 [constructor, in Buchberger.Peq]
eqptail_spminusf_com [lemma, in Buchberger.Pspminus]
eqp_sym1 [abbreviation, in Buchberger.Preduce]
eqp_trans1 [abbreviation, in Buchberger.Preduce]
eqp_imp_canonical [lemma, in Buchberger.Peq]
eqp_eqTerm [lemma, in Buchberger.Peq]
eqp_trans [lemma, in Buchberger.Peq]
eqp_inv3r [lemma, in Buchberger.Peq]
eqp_inv3l [lemma, in Buchberger.Peq]
eqp_inv2 [lemma, in Buchberger.Peq]
eqp_inv1 [lemma, in Buchberger.Peq]
eqp_sym [lemma, in Buchberger.Peq]
eqp_refl [lemma, in Buchberger.Peq]
eqp_sym1 [abbreviation, in Buchberger.WfR0]
eqp_trans1 [abbreviation, in Buchberger.WfR0]
eqp_sym1 [abbreviation, in Buchberger.Buch]
eqp_trans1 [abbreviation, in Buchberger.Buch]
eqp_sym1 [abbreviation, in Buchberger.BuchAux]
eqp_trans1 [abbreviation, in Buchberger.BuchAux]
eqp_sym1 [abbreviation, in Buchberger.Preduceplus]
eqp_trans1 [abbreviation, in Buchberger.Preduceplus]
eqp_invT1_pO_is_pO [lemma, in Buchberger.Pmults]
eqp_sym1 [abbreviation, in Buchberger.Pmults]
eqp_trans1 [abbreviation, in Buchberger.Pmults]
eqp_sym1 [abbreviation, in Buchberger.Preducestar]
eqp_trans1 [abbreviation, in Buchberger.Preducestar]
eqp_sym1 [abbreviation, in Buchberger.Preducestar]
eqp_trans1 [abbreviation, in Buchberger.Preducestar]
eqp_sym1 [abbreviation, in Buchberger.BuchRed]
eqp_trans1 [abbreviation, in Buchberger.BuchRed]
eqp_sym1 [abbreviation, in Buchberger.Pminus]
eqp_trans1 [abbreviation, in Buchberger.Pminus]
eqp_sym1 [abbreviation, in Buchberger.Pspoly]
eqp_trans1 [abbreviation, in Buchberger.Pspoly]
eqp_sym1 [abbreviation, in Buchberger.Pcrit]
eqp_trans1 [abbreviation, in Buchberger.Pcrit]
eqp_sym1 [abbreviation, in Buchberger.Pcomb]
eqp_trans1 [abbreviation, in Buchberger.Pcomb]
eqp_spminusf_com [lemma, in Buchberger.Pspminus]
eqp_sym1 [abbreviation, in Buchberger.Pspminus]
eqp_trans1 [abbreviation, in Buchberger.Pspminus]
eqp_pluspf_com [lemma, in Buchberger.Pplus]
eqp_pluspf_com_r [lemma, in Buchberger.Pplus]
eqp_pluspf_com_l [lemma, in Buchberger.Pplus]
eqp_sym1 [abbreviation, in Buchberger.Pplus]
eqp_trans1 [abbreviation, in Buchberger.Pplus]
eqp_sym1 [abbreviation, in Buchberger.Pmult]
eqp_trans1 [abbreviation, in Buchberger.Pmult]
eqP0 [constructor, in Buchberger.Peq]
eqP1 [abbreviation, in Buchberger.Preduce]
eqP1 [abbreviation, in Buchberger.WfR0]
eqP1 [abbreviation, in Buchberger.Buch]
eqP1 [abbreviation, in Buchberger.BuchAux]
eqP1 [abbreviation, in Buchberger.Preduceplus]
eqP1 [abbreviation, in Buchberger.Pmults]
eqP1 [abbreviation, in Buchberger.Preducestar]
eqP1 [abbreviation, in Buchberger.Preducestar]
eqP1 [abbreviation, in Buchberger.BuchRed]
eqP1 [abbreviation, in Buchberger.Pminus]
eqP1 [abbreviation, in Buchberger.Pspoly]
eqP1 [abbreviation, in Buchberger.Pcrit]
eqP1 [abbreviation, in Buchberger.Pcomb]
eqP1 [abbreviation, in Buchberger.Pspminus]
eqP1 [abbreviation, in Buchberger.Pplus]
eqP1 [abbreviation, in Buchberger.Pmult]
eqT [definition, in Buchberger.Term]
eqTerm [definition, in Buchberger.Term]
eqTerm_dec1 [abbreviation, in Buchberger.Preduce]
eqTerm_trans1 [abbreviation, in Buchberger.Preduce]
eqTerm_sym1 [abbreviation, in Buchberger.Preduce]
eqTerm_dec1 [abbreviation, in Buchberger.Peq]
eqTerm_trans1 [abbreviation, in Buchberger.Peq]
eqTerm_sym1 [abbreviation, in Buchberger.Peq]
eqTerm_dec1 [abbreviation, in Buchberger.POrder]
eqTerm_trans1 [abbreviation, in Buchberger.POrder]
eqTerm_sym1 [abbreviation, in Buchberger.POrder]
eqTerm_dec1 [abbreviation, in Buchberger.WfR0]
eqTerm_trans1 [abbreviation, in Buchberger.WfR0]
eqTerm_sym1 [abbreviation, in Buchberger.WfR0]
eqTerm_dec1 [abbreviation, in Buchberger.Buch]
eqTerm_trans1 [abbreviation, in Buchberger.Buch]
eqTerm_sym1 [abbreviation, in Buchberger.Buch]
eqTerm_dec1 [abbreviation, in Buchberger.BuchAux]
eqTerm_trans1 [abbreviation, in Buchberger.BuchAux]
eqTerm_sym1 [abbreviation, in Buchberger.BuchAux]
eqTerm_dec1 [abbreviation, in Buchberger.Preduceplus]
eqTerm_trans1 [abbreviation, in Buchberger.Preduceplus]
eqTerm_sym1 [abbreviation, in Buchberger.Preduceplus]
eqTerm_dec1 [abbreviation, in Buchberger.Pmults]
eqTerm_trans1 [abbreviation, in Buchberger.Pmults]
eqTerm_sym1 [abbreviation, in Buchberger.Pmults]
eqTerm_dec1 [abbreviation, in Buchberger.Preducestar]
eqTerm_trans1 [abbreviation, in Buchberger.Preducestar]
eqTerm_sym1 [abbreviation, in Buchberger.Preducestar]
eqTerm_dec1 [abbreviation, in Buchberger.Preducestar]
eqTerm_trans1 [abbreviation, in Buchberger.Preducestar]
eqTerm_sym1 [abbreviation, in Buchberger.Preducestar]
eqTerm_dec1 [abbreviation, in Buchberger.BuchRed]
eqTerm_trans1 [abbreviation, in Buchberger.BuchRed]
eqTerm_sym1 [abbreviation, in Buchberger.BuchRed]
eqTerm_dec1 [abbreviation, in Buchberger.Pminus]
eqTerm_trans1 [abbreviation, in Buchberger.Pminus]
eqTerm_sym1 [abbreviation, in Buchberger.Pminus]
eqTerm_minusTerm_plusTerm_invTerm [lemma, in Buchberger.Term]
eqTerm_T1_eqT [lemma, in Buchberger.Term]
eqTerm_invTerm_comp [lemma, in Buchberger.Term]
eqTerm_multTerm_comp [lemma, in Buchberger.Term]
eqTerm_plusTerm_comp [lemma, in Buchberger.Term]
eqTerm_dec [lemma, in Buchberger.Term]
eqTerm_imp_eqT [lemma, in Buchberger.Term]
eqTerm_trans [lemma, in Buchberger.Term]
eqTerm_sym [lemma, in Buchberger.Term]
eqTerm_refl [lemma, in Buchberger.Term]
eqTerm_spolyf_red3 [lemma, in Buchberger.Pspoly]
eqTerm_spolyf_red2 [lemma, in Buchberger.Pspoly]
eqTerm_dec1 [abbreviation, in Buchberger.Pspoly]
eqTerm_trans1 [abbreviation, in Buchberger.Pspoly]
eqTerm_sym1 [abbreviation, in Buchberger.Pspoly]
eqTerm_dec1 [abbreviation, in Buchberger.Pcrit]
eqTerm_trans1 [abbreviation, in Buchberger.Pcrit]
eqTerm_sym1 [abbreviation, in Buchberger.Pcrit]
eqTerm_dec1 [abbreviation, in Buchberger.Pcomb]
eqTerm_trans1 [abbreviation, in Buchberger.Pcomb]
eqTerm_sym1 [abbreviation, in Buchberger.Pcomb]
eqTerm_spminusf_com [lemma, in Buchberger.Pspminus]
eqTerm_dec1 [abbreviation, in Buchberger.Pspminus]
eqTerm_trans1 [abbreviation, in Buchberger.Pspminus]
eqTerm_sym1 [abbreviation, in Buchberger.Pspminus]
eqTerm_multTerm_imp_eqTerm [lemma, in Buchberger.DivTerm]
eqTerm_divTerm_comp [lemma, in Buchberger.DivTerm]
eqTerm_dec1 [abbreviation, in Buchberger.DivTerm]
eqTerm_trans1 [abbreviation, in Buchberger.DivTerm]
eqTerm_sym1 [abbreviation, in Buchberger.DivTerm]
eqTerm_dec1 [abbreviation, in Buchberger.Pplus]
eqTerm_trans1 [abbreviation, in Buchberger.Pplus]
eqTerm_sym1 [abbreviation, in Buchberger.Pplus]
eqTerm_dec1 [abbreviation, in Buchberger.Pmult]
eqTerm_trans1 [abbreviation, in Buchberger.Pmult]
eqTerm_sym1 [abbreviation, in Buchberger.Pmult]
eqTerm1 [abbreviation, in Buchberger.Preduce]
eqTerm1 [abbreviation, in Buchberger.Peq]
eqTerm1 [abbreviation, in Buchberger.POrder]
eqTerm1 [abbreviation, in Buchberger.WfR0]
eqTerm1 [abbreviation, in Buchberger.Buch]
eqTerm1 [abbreviation, in Buchberger.BuchAux]
eqTerm1 [abbreviation, in Buchberger.Preduceplus]
eqTerm1 [abbreviation, in Buchberger.Pmults]
eqTerm1 [abbreviation, in Buchberger.Preducestar]
eqTerm1 [abbreviation, in Buchberger.Preducestar]
eqTerm1 [abbreviation, in Buchberger.BuchRed]
eqTerm1 [abbreviation, in Buchberger.Pminus]
eqTerm1 [abbreviation, in Buchberger.Pspoly]
eqTerm1 [abbreviation, in Buchberger.Pcrit]
eqTerm1 [abbreviation, in Buchberger.Pcomb]
eqTerm1 [abbreviation, in Buchberger.Pspminus]
eqTerm1 [abbreviation, in Buchberger.DivTerm]
eqTerm1 [abbreviation, in Buchberger.Pplus]
eqTerm1 [abbreviation, in Buchberger.Pmult]
eqT_not_ltT [lemma, in Buchberger.POrder]
eqT_dec [lemma, in Buchberger.POrder]
eqT_compat_ltTl [lemma, in Buchberger.POrder]
eqT_compat_ltTr [lemma, in Buchberger.POrder]
eqT_zerop_is_eqTerm [lemma, in Buchberger.Term]
eqT_trans [lemma, in Buchberger.Term]
eqT_sym [lemma, in Buchberger.Term]
eqT_refl [lemma, in Buchberger.Term]
eqT_nzero_eqT_divP [lemma, in Buchberger.DivTerm]
eqT_nzero_divP [lemma, in Buchberger.DivTerm]
eqT_divTerm [lemma, in Buchberger.DivTerm]
eqT_divTerm_plusTerm [lemma, in Buchberger.DivTerm]
ExistsL [inductive, in Buchberger.Bar]
Extract [library]
F
fconfl_top [lemma, in Buchberger.Pspoly]Fl [definition, in Buchberger.Buch]
fltP [lemma, in Buchberger.POrder]
foreigner [definition, in Buchberger.BuchAux]
foreigner_dec1 [abbreviation, in Buchberger.WfR0]
foreigner_dec1 [abbreviation, in Buchberger.Buch]
foreigner_red [lemma, in Buchberger.BuchAux]
foreigner_dec [definition, in Buchberger.BuchAux]
foreigner_dec1 [abbreviation, in Buchberger.BuchRed]
foreigner1 [abbreviation, in Buchberger.WfR0]
foreigner1 [abbreviation, in Buchberger.Buch]
foreigner1 [abbreviation, in Buchberger.BuchRed]
FoundE [constructor, in Buchberger.Bar]
FoundG [constructor, in Buchberger.Bar]
fP [definition, in Buchberger.POrder]
fp_tail [lemma, in Buchberger.POrder]
fP_app [lemma, in Buchberger.POrder]
Fred [library]
fsltP [lemma, in Buchberger.POrder]
fspoly [definition, in Buchberger.POrder]
fspoly_Reduceplus_pO [lemma, in Buchberger.Pcrit]
G
GBarlR [definition, in Buchberger.Dickson]genOCPf [definition, in Buchberger.Buch]
genOCPf_stable [lemma, in Buchberger.Buch]
genOCp_redln [lemma, in Buchberger.Buch]
genPcP [inductive, in Buchberger.Buch]
genPcPf [definition, in Buchberger.Buch]
genPcPf_incl [lemma, in Buchberger.Buch]
genPcPf0 [definition, in Buchberger.Buch]
genPcP_incl [lemma, in Buchberger.Buch]
genPcP_spolyp1 [lemma, in Buchberger.Buch]
genPcP0 [constructor, in Buchberger.Buch]
genPcP1 [constructor, in Buchberger.Buch]
genPcP2 [constructor, in Buchberger.Buch]
gen_mon [definition, in Buchberger.Monomials]
getRes [definition, in Buchberger.Buch]
get_monL [definition, in Buchberger.WfR0]
get_is_correct [lemma, in Buchberger.WfR0]
get_mon [definition, in Buchberger.WfR0]
GoodR [inductive, in Buchberger.Bar]
GRBar [definition, in Buchberger.Bar]
Grobner [inductive, in Buchberger.Pcomb]
grobner_def [lemma, in Buchberger.BuchRed]
Grobner_imp_SpolyQ [lemma, in Buchberger.Pcomb]
Grobner0 [constructor, in Buchberger.Pcomb]
Grobner1 [abbreviation, in Buchberger.WfR0]
Grobner1 [abbreviation, in Buchberger.Buch]
Grobner1 [abbreviation, in Buchberger.BuchAux]
Grobner1 [abbreviation, in Buchberger.BuchRed]
I
imp_in [lemma, in Buchberger.Buch]Incl_inp_inPolySet [lemma, in Buchberger.Preduce]
incl_addEnd1 [lemma, in Buchberger.Buch]
incons [constructor, in Buchberger.Preduce]
Ind [constructor, in Buchberger.Bar]
inPolySet [inductive, in Buchberger.Preduce]
inPolySet_inv1 [lemma, in Buchberger.Preduce]
inPolySet_inv0 [lemma, in Buchberger.Preduce]
inPolySet_is_pX [lemma, in Buchberger.Preduce]
inPolySet_imp_canonical [lemma, in Buchberger.Preduce]
inPolySet_addEnd [lemma, in Buchberger.BuchAux]
inPolySet1 [abbreviation, in Buchberger.WfR0]
inPolySet1 [abbreviation, in Buchberger.Buch]
inPolySet1 [abbreviation, in Buchberger.BuchAux]
inPolySet1 [abbreviation, in Buchberger.Preduceplus]
inPolySet1 [abbreviation, in Buchberger.Preducestar]
inPolySet1 [abbreviation, in Buchberger.Preducestar]
inPolySet1 [abbreviation, in Buchberger.BuchRed]
inPolySet1 [abbreviation, in Buchberger.Pspoly]
inPolySet1 [abbreviation, in Buchberger.Pcrit]
inPolySet1 [abbreviation, in Buchberger.Pcomb]
inP_reducestar [lemma, in Buchberger.BuchAux]
inP_reduceplus [lemma, in Buchberger.BuchAux]
inP_reduce [lemma, in Buchberger.BuchAux]
inskip [constructor, in Buchberger.Preduce]
inv [definition, in Buchberger.Pminus]
invA_eqA_comp [projection, in Buchberger.CoefStructure]
invA_plusA [projection, in Buchberger.CoefStructure]
invA_is_invA1 [lemma, in Buchberger.moreCoefStructure]
invA0 [lemma, in Buchberger.moreCoefStructure]
invA0_inv [lemma, in Buchberger.moreCoefStructure]
invA0_comp [lemma, in Buchberger.moreCoefStructure]
invTerm [definition, in Buchberger.Term]
invTerm_ltT_l [lemma, in Buchberger.POrder]
invTerm_T1_multTerm_T1 [lemma, in Buchberger.Pminus]
invTerm_T1_eqT_comp [lemma, in Buchberger.Pminus]
invTerm_eqT_comp [lemma, in Buchberger.Pminus]
invTerm_eqT [lemma, in Buchberger.Term]
invTerm_invol [lemma, in Buchberger.Term]
invTerm1 [abbreviation, in Buchberger.Preduce]
invTerm1 [abbreviation, in Buchberger.Peq]
invTerm1 [abbreviation, in Buchberger.POrder]
invTerm1 [abbreviation, in Buchberger.WfR0]
invTerm1 [abbreviation, in Buchberger.Buch]
invTerm1 [abbreviation, in Buchberger.BuchAux]
invTerm1 [abbreviation, in Buchberger.Preduceplus]
invTerm1 [abbreviation, in Buchberger.Pmults]
invTerm1 [abbreviation, in Buchberger.Preducestar]
invTerm1 [abbreviation, in Buchberger.Preducestar]
invTerm1 [abbreviation, in Buchberger.BuchRed]
invTerm1 [abbreviation, in Buchberger.Pminus]
invTerm1 [abbreviation, in Buchberger.Pspoly]
invTerm1 [abbreviation, in Buchberger.Pcrit]
invTerm1 [abbreviation, in Buchberger.Pcomb]
invTerm1 [abbreviation, in Buchberger.Pspminus]
invTerm1 [abbreviation, in Buchberger.DivTerm]
invTerm1 [abbreviation, in Buchberger.Pplus]
invTerm1 [abbreviation, in Buchberger.Pmult]
inv_prop [lemma, in Buchberger.Pminus]
in_inPolySet [lemma, in Buchberger.Preduce]
In_inp_inPolySet [lemma, in Buchberger.Preduce]
in_incl [lemma, in Buchberger.Buch]
in_minuspf_spoly_in [lemma, in Buchberger.Pcrit]
in_rev [lemma, in Buchberger.ListProps]
in_multpf_head [lemma, in Buchberger.Pmult]
irreducible [definition, in Buchberger.Preduce]
irreducible_eqp_com [lemma, in Buchberger.Preduce]
irreducible_inv_px_l [lemma, in Buchberger.Preduce]
irreducible1 [abbreviation, in Buchberger.WfR0]
irreducible1 [abbreviation, in Buchberger.Buch]
irreducible1 [abbreviation, in Buchberger.BuchAux]
irreducible1 [abbreviation, in Buchberger.Preduceplus]
irreducible1 [abbreviation, in Buchberger.Preducestar]
irreducible1 [abbreviation, in Buchberger.Preducestar]
irreducible1 [abbreviation, in Buchberger.BuchRed]
irreducible1 [abbreviation, in Buchberger.Pspoly]
irreducible1 [abbreviation, in Buchberger.Pcrit]
irreducible1 [abbreviation, in Buchberger.Pcomb]
is_nil_id [lemma, in Buchberger.Monomials]
is_nil [definition, in Buchberger.Monomials]
J
jj [definition, in Buchberger.Dickson]jjProp1 [lemma, in Buchberger.Dickson]
jjProp2 [lemma, in Buchberger.Dickson]
K
Keep [constructor, in Buchberger.Buch]keylem [lemma, in Buchberger.Dickson]
keylem_cor [lemma, in Buchberger.Dickson]
L
lems [section, in Buchberger.Bar]lems.tdiv [variable, in Buchberger.Bar]
lems.trm [variable, in Buchberger.Bar]
lem_redln_cons_gen [lemma, in Buchberger.Buch]
lem_redln_cons [lemma, in Buchberger.Buch]
lem_redIn_nil [lemma, in Buchberger.Buch]
lem0 [lemma, in Buchberger.Dickson]
lem1 [lemma, in Buchberger.Dickson]
lem1aux [lemma, in Buchberger.Dickson]
leq [definition, in Buchberger.Dickson]
leq2le [lemma, in Buchberger.Dickson]
lessP [definition, in Buchberger.Peq]
lessP3 [definition, in Buchberger.Peq]
LetP [definition, in Buchberger.LetP]
LetP [library]
LexiOrder [library]
lexi_order [section, in Buchberger.LexiOrder]
ListProps [library]
lo1 [constructor, in Buchberger.LexiOrder]
lo2 [constructor, in Buchberger.LexiOrder]
ltM_plusl [projection, in Buchberger.OrderStructure]
ltM_plusr [projection, in Buchberger.OrderStructure]
ltM_wf [projection, in Buchberger.OrderStructure]
ltM_trans [projection, in Buchberger.OrderStructure]
ltM_nonrefl [projection, in Buchberger.OrderStructure]
ltP [inductive, in Buchberger.POrder]
ltPO [constructor, in Buchberger.POrder]
ltP_reduce [lemma, in Buchberger.Preduce]
ltp_eqp_comp [lemma, in Buchberger.Peq]
ltP_refl_pX [lemma, in Buchberger.Peq]
ltP_pX_canonical [lemma, in Buchberger.POrder]
ltP_order_comp [lemma, in Buchberger.POrder]
ltP_pX_olist [lemma, in Buchberger.POrder]
ltP_trans [lemma, in Buchberger.POrder]
ltp_not_refl [lemma, in Buchberger.POrder]
ltP_tl [constructor, in Buchberger.POrder]
ltP_hd [constructor, in Buchberger.POrder]
ltP_divP_pX [lemma, in Buchberger.Pspminus]
ltP1 [abbreviation, in Buchberger.Preduce]
ltP1 [abbreviation, in Buchberger.Peq]
ltP1 [abbreviation, in Buchberger.WfR0]
ltP1 [abbreviation, in Buchberger.Buch]
ltP1 [abbreviation, in Buchberger.BuchAux]
ltP1 [abbreviation, in Buchberger.Preduceplus]
ltP1 [abbreviation, in Buchberger.Pmults]
ltP1 [abbreviation, in Buchberger.Preducestar]
ltP1 [abbreviation, in Buchberger.Preducestar]
ltP1 [abbreviation, in Buchberger.BuchRed]
ltP1 [abbreviation, in Buchberger.Pminus]
ltP1 [abbreviation, in Buchberger.Pspoly]
ltP1 [abbreviation, in Buchberger.Pcrit]
ltP1 [abbreviation, in Buchberger.Pcomb]
ltP1 [abbreviation, in Buchberger.Pspminus]
ltP1 [abbreviation, in Buchberger.Pplus]
ltP1 [abbreviation, in Buchberger.Pmult]
ltT [definition, in Buchberger.POrder]
ltT_dec1 [abbreviation, in Buchberger.Preduce]
ltT_eqTl [lemma, in Buchberger.POrder]
ltT_eqTr [lemma, in Buchberger.POrder]
ltT_eqT [lemma, in Buchberger.POrder]
ltT_not_ltT [lemma, in Buchberger.POrder]
ltT_not_refl [lemma, in Buchberger.POrder]
ltT_not_eqT [lemma, in Buchberger.POrder]
ltT_dec [lemma, in Buchberger.POrder]
ltT_trans [lemma, in Buchberger.POrder]
ltT_dec1 [abbreviation, in Buchberger.WfR0]
ltT_dec1 [abbreviation, in Buchberger.Buch]
ltT_dec1 [abbreviation, in Buchberger.BuchAux]
ltT_dec1 [abbreviation, in Buchberger.Preduceplus]
ltT_dec1 [abbreviation, in Buchberger.Pmults]
ltT_dec1 [abbreviation, in Buchberger.Preducestar]
ltT_dec1 [abbreviation, in Buchberger.Preducestar]
ltT_dec1 [abbreviation, in Buchberger.BuchRed]
ltT_dec1 [abbreviation, in Buchberger.Pminus]
ltT_dec1 [abbreviation, in Buchberger.Pspoly]
ltT_dec1 [abbreviation, in Buchberger.Pcrit]
ltT_dec1 [abbreviation, in Buchberger.Pcomb]
ltT_dec1 [abbreviation, in Buchberger.Pspminus]
ltT_dec1 [abbreviation, in Buchberger.Pplus]
ltT_dec1 [abbreviation, in Buchberger.Pmult]
ltT1 [abbreviation, in Buchberger.Preduce]
ltT1 [abbreviation, in Buchberger.WfR0]
ltT1 [abbreviation, in Buchberger.Buch]
ltT1 [abbreviation, in Buchberger.BuchAux]
ltT1 [abbreviation, in Buchberger.Preduceplus]
ltT1 [abbreviation, in Buchberger.Pmults]
ltT1 [abbreviation, in Buchberger.Preducestar]
ltT1 [abbreviation, in Buchberger.Preducestar]
ltT1 [abbreviation, in Buchberger.BuchRed]
ltT1 [abbreviation, in Buchberger.Pminus]
ltT1 [abbreviation, in Buchberger.Pspoly]
ltT1 [abbreviation, in Buchberger.Pcrit]
ltT1 [abbreviation, in Buchberger.Pcomb]
ltT1 [abbreviation, in Buchberger.Pspminus]
ltT1 [abbreviation, in Buchberger.Pplus]
ltT1 [abbreviation, in Buchberger.Pmult]
l1 [lemma, in Buchberger.WfR0]
M
mainu1 [constructor, in Buchberger.Pplus]mainu2a [constructor, in Buchberger.Pplus]
mainu2b [constructor, in Buchberger.Pplus]
mainu3 [constructor, in Buchberger.Pplus]
map_rev [lemma, in Buchberger.ListProps]
map_app [lemma, in Buchberger.ListProps]
map_in [lemma, in Buchberger.ListProps]
mCoef [section, in Buchberger.moreCoefStructure]
mCoef.A [variable, in Buchberger.moreCoefStructure]
mCoef.A0 [variable, in Buchberger.moreCoefStructure]
mCoef.A1 [variable, in Buchberger.moreCoefStructure]
mCoef.cs [variable, in Buchberger.moreCoefStructure]
mCoef.divA [variable, in Buchberger.moreCoefStructure]
mCoef.eqA [variable, in Buchberger.moreCoefStructure]
mCoef.eqA_sym [variable, in Buchberger.moreCoefStructure]
mCoef.eqA_trans [variable, in Buchberger.moreCoefStructure]
mCoef.eqA_dec [variable, in Buchberger.moreCoefStructure]
mCoef.invA [variable, in Buchberger.moreCoefStructure]
mCoef.minusA [variable, in Buchberger.moreCoefStructure]
mCoef.multA [variable, in Buchberger.moreCoefStructure]
mCoef.plusA [variable, in Buchberger.moreCoefStructure]
mdiv [inductive, in Buchberger.Monomials]
mdiv_div [lemma, in Buchberger.Monomials]
mdiv_trans [lemma, in Buchberger.Monomials]
mdiv_proj [lemma, in Buchberger.Monomials]
mdiv_cons [constructor, in Buchberger.Monomials]
mdiv_nil [constructor, in Buchberger.Monomials]
Min [inductive, in Buchberger.OpenIndGoodRel]
MinD [definition, in Buchberger.Dickson]
minusA_def [projection, in Buchberger.CoefStructure]
minusP [inductive, in Buchberger.Pminus]
minuspf [definition, in Buchberger.Pminus]
minuspf_eq_inv2 [lemma, in Buchberger.Pminus]
minuspf_pOmults_eq [lemma, in Buchberger.Pminus]
minuspf_eq_inv1 [lemma, in Buchberger.Pminus]
minuspf_pO_refl_eq [lemma, in Buchberger.Pminus]
minuspf_zero [lemma, in Buchberger.Pminus]
minuspf_refl [lemma, in Buchberger.Pminus]
minuspf_refl_eq [lemma, in Buchberger.Pminus]
minuspf_pOmults [lemma, in Buchberger.Pminus]
minuspf_pO_refl [lemma, in Buchberger.Pminus]
minuspf_comp [lemma, in Buchberger.Pminus]
minuspf_inv3b [lemma, in Buchberger.Pminus]
minuspf_inv3a [lemma, in Buchberger.Pminus]
minuspf_inv2 [lemma, in Buchberger.Pminus]
minuspf_inv1 [lemma, in Buchberger.Pminus]
minuspf_inv3b_eq [lemma, in Buchberger.Pminus]
minuspf_inv3a_eq [lemma, in Buchberger.Pminus]
minuspf_inv2_eq [lemma, in Buchberger.Pminus]
minuspf_inv1_eq [lemma, in Buchberger.Pminus]
minuspf_is_pluspf_mults [lemma, in Buchberger.Pminus]
minuspf_pO_is_eqP [lemma, in Buchberger.Pminus]
minuspf_is_minusP [lemma, in Buchberger.Pminus]
minuspf_spoly_in [lemma, in Buchberger.Pcrit]
minuspf_in [lemma, in Buchberger.Pcrit]
minuspf1 [abbreviation, in Buchberger.Preduce]
minuspf1 [abbreviation, in Buchberger.WfR0]
minuspf1 [abbreviation, in Buchberger.Buch]
minuspf1 [abbreviation, in Buchberger.BuchAux]
minuspf1 [abbreviation, in Buchberger.Preduceplus]
minuspf1 [abbreviation, in Buchberger.Preducestar]
minuspf1 [abbreviation, in Buchberger.Preducestar]
minuspf1 [abbreviation, in Buchberger.BuchRed]
minuspf1 [abbreviation, in Buchberger.Pspoly]
minuspf1 [abbreviation, in Buchberger.Pcrit]
minuspf1 [abbreviation, in Buchberger.Pcomb]
minuspf1 [abbreviation, in Buchberger.Pspminus]
minuspp [definition, in Buchberger.Pminus]
minusP_pO_refl_eq [lemma, in Buchberger.Pminus]
minusP_refl [lemma, in Buchberger.Pminus]
minusP_inv3b [lemma, in Buchberger.Pminus]
minusP_inv3a [lemma, in Buchberger.Pminus]
minusP_inv2 [lemma, in Buchberger.Pminus]
minusP_inv1 [lemma, in Buchberger.Pminus]
minusP_is_plusP_mults [lemma, in Buchberger.Pminus]
minusP_inv [lemma, in Buchberger.Pminus]
minusP_pO_is_eqP [lemma, in Buchberger.Pminus]
minusTerm [definition, in Buchberger.Term]
minusTerm_ltT_l [lemma, in Buchberger.POrder]
minusTerm_zeroP [lemma, in Buchberger.Pminus]
minusTerm_zeroP_r [lemma, in Buchberger.Pminus]
minusTerm_eqT [lemma, in Buchberger.Term]
minusTerm1 [abbreviation, in Buchberger.Preduce]
minusTerm1 [abbreviation, in Buchberger.Peq]
minusTerm1 [abbreviation, in Buchberger.POrder]
minusTerm1 [abbreviation, in Buchberger.WfR0]
minusTerm1 [abbreviation, in Buchberger.Buch]
minusTerm1 [abbreviation, in Buchberger.BuchAux]
minusTerm1 [abbreviation, in Buchberger.Preduceplus]
minusTerm1 [abbreviation, in Buchberger.Pmults]
minusTerm1 [abbreviation, in Buchberger.Preducestar]
minusTerm1 [abbreviation, in Buchberger.Preducestar]
minusTerm1 [abbreviation, in Buchberger.BuchRed]
minusTerm1 [abbreviation, in Buchberger.Pminus]
minusTerm1 [abbreviation, in Buchberger.Pspoly]
minusTerm1 [abbreviation, in Buchberger.Pcrit]
minusTerm1 [abbreviation, in Buchberger.Pcomb]
minusTerm1 [abbreviation, in Buchberger.Pspminus]
minusTerm1 [abbreviation, in Buchberger.DivTerm]
minusTerm1 [abbreviation, in Buchberger.Pplus]
minusTerm1 [abbreviation, in Buchberger.Pmult]
minus_lt_0 [lemma, in Buchberger.Monomials]
minus_is_reduce [lemma, in Buchberger.Pcrit]
mkCoefStructure [constructor, in Buchberger.CoefStructure]
mkOrderStructure [constructor, in Buchberger.OrderStructure]
mks [definition, in Buchberger.Preducestar]
mks [definition, in Buchberger.Preducestar]
mks1 [abbreviation, in Buchberger.WfR0]
mks1 [abbreviation, in Buchberger.Buch]
mks1 [abbreviation, in Buchberger.BuchAux]
mks1 [abbreviation, in Buchberger.BuchRed]
mks1 [abbreviation, in Buchberger.Pspoly]
mks1 [abbreviation, in Buchberger.Pcrit]
mks1 [abbreviation, in Buchberger.Pcomb]
mk_clean [definition, in Buchberger.DivTerm]
mmainu1 [constructor, in Buchberger.Pminus]
mmainu2a [constructor, in Buchberger.Pminus]
mmainu2b [constructor, in Buchberger.Pminus]
mmainu3 [constructor, in Buchberger.Pminus]
mnillu1 [constructor, in Buchberger.Pminus]
mnillu2 [constructor, in Buchberger.Pminus]
mon [inductive, in Buchberger.Monomials]
monExistsL [lemma, in Buchberger.Bar]
monExistsL1 [lemma, in Buchberger.Bar]
monGoodR [lemma, in Buchberger.Bar]
monGoodR1 [lemma, in Buchberger.Bar]
monGRBar [lemma, in Buchberger.Bar]
monGRBarAux [lemma, in Buchberger.Bar]
monLift [definition, in Buchberger.Dickson]
monLift_lem [lemma, in Buchberger.Dickson]
Monomials [section, in Buchberger.Monomials]
Monomials [library]
Monomials.gb [variable, in Buchberger.Monomials]
Monomials.gm [variable, in Buchberger.Monomials]
monO_n0 [lemma, in Buchberger.Dickson]
mon_0 [lemma, in Buchberger.Monomials]
moreCoefStructure [library]
multA_A1_l [projection, in Buchberger.CoefStructure]
multA_A0_l [projection, in Buchberger.CoefStructure]
multA_dist_l [projection, in Buchberger.CoefStructure]
multA_com [projection, in Buchberger.CoefStructure]
multA_assoc [projection, in Buchberger.CoefStructure]
multA_eqA_comp [projection, in Buchberger.CoefStructure]
multA_invA_com_r [lemma, in Buchberger.moreCoefStructure]
multA_invA_com_l [lemma, in Buchberger.moreCoefStructure]
multA_A1_r [lemma, in Buchberger.moreCoefStructure]
multA_A0_r [lemma, in Buchberger.moreCoefStructure]
multA_dist_r [lemma, in Buchberger.moreCoefStructure]
multA_eqA_comp_r [lemma, in Buchberger.moreCoefStructure]
multA_eqA_comp_l [lemma, in Buchberger.moreCoefStructure]
multlm_comp_canonical [lemma, in Buchberger.Pmults]
multpf [definition, in Buchberger.Pmult]
multpf_assoc [lemma, in Buchberger.Pmult]
multpf_smultm_assoc [lemma, in Buchberger.Pmult]
multpf_dist_plusl [lemma, in Buchberger.Pmult]
multpf_dist_plusr [lemma, in Buchberger.Pmult]
multpf_com [lemma, in Buchberger.Pmult]
multpf_comp [lemma, in Buchberger.Pmult]
multpf_head [lemma, in Buchberger.Pmult]
multpf_disr_pX [lemma, in Buchberger.Pmult]
multpf1 [abbreviation, in Buchberger.Pcrit]
mults [definition, in Buchberger.Pmults]
mults_eqp_inv [lemma, in Buchberger.Preduce]
mults_dist_pluspf [lemma, in Buchberger.Pmults]
mults_ltP_comp [lemma, in Buchberger.Pmults]
mults_comp [lemma, in Buchberger.Pmults]
mults_com [lemma, in Buchberger.Pmults]
mults_multTerm [lemma, in Buchberger.Pmults]
mults_invTerm [lemma, in Buchberger.Pmults]
mults_T1 [lemma, in Buchberger.Pmults]
mults_dist2 [lemma, in Buchberger.Pmults]
mults_dist1 [lemma, in Buchberger.Pmults]
mults_eqp_zpO [lemma, in Buchberger.Pmults]
mults_eqp_pO_pO [lemma, in Buchberger.Pmults]
mults_order_l [lemma, in Buchberger.Pmults]
mults_comp_minuspf [lemma, in Buchberger.Pminus]
mults_minusTerm [lemma, in Buchberger.Pminus]
mults_pO [lemma, in Buchberger.Pminus]
mults_dist_minuspf [lemma, in Buchberger.Pminus]
mults1 [abbreviation, in Buchberger.Preduce]
mults1 [abbreviation, in Buchberger.WfR0]
mults1 [abbreviation, in Buchberger.Buch]
mults1 [abbreviation, in Buchberger.BuchAux]
mults1 [abbreviation, in Buchberger.Preduceplus]
mults1 [abbreviation, in Buchberger.Preducestar]
mults1 [abbreviation, in Buchberger.Preducestar]
mults1 [abbreviation, in Buchberger.BuchRed]
mults1 [abbreviation, in Buchberger.Pminus]
mults1 [abbreviation, in Buchberger.Pspoly]
mults1 [abbreviation, in Buchberger.Pcrit]
mults1 [abbreviation, in Buchberger.Pcomb]
mults1 [abbreviation, in Buchberger.Pspminus]
mults1 [abbreviation, in Buchberger.Pmult]
multTerm [definition, in Buchberger.Term]
multTerm_ltT_r [lemma, in Buchberger.POrder]
multTerm_ltT_l [lemma, in Buchberger.POrder]
multTerm_invTerm_T1_eqT_comp [lemma, in Buchberger.Pminus]
multTerm_minusTerm_dist_l [lemma, in Buchberger.Term]
multTerm_zeroP_div [lemma, in Buchberger.Term]
multTerm_com [lemma, in Buchberger.Term]
multTerm_assoc [lemma, in Buchberger.Term]
multTerm_eqT [lemma, in Buchberger.Term]
multTerm_plusTerm_dist_r [lemma, in Buchberger.Term]
multTerm_plusTerm_dist_l [lemma, in Buchberger.Term]
multTerm_or_z_d2 [lemma, in Buchberger.Pcrit]
multTerm_or_z_d1 [lemma, in Buchberger.Pcrit]
multTerm_eqTerm_inv [lemma, in Buchberger.DivTerm]
multTerm1 [abbreviation, in Buchberger.Preduce]
multTerm1 [abbreviation, in Buchberger.Peq]
multTerm1 [abbreviation, in Buchberger.POrder]
multTerm1 [abbreviation, in Buchberger.WfR0]
multTerm1 [abbreviation, in Buchberger.Buch]
multTerm1 [abbreviation, in Buchberger.BuchAux]
multTerm1 [abbreviation, in Buchberger.Preduceplus]
multTerm1 [abbreviation, in Buchberger.Pmults]
multTerm1 [abbreviation, in Buchberger.Preducestar]
multTerm1 [abbreviation, in Buchberger.Preducestar]
multTerm1 [abbreviation, in Buchberger.BuchRed]
multTerm1 [abbreviation, in Buchberger.Pminus]
multTerm1 [abbreviation, in Buchberger.Pspoly]
multTerm1 [abbreviation, in Buchberger.Pcrit]
multTerm1 [abbreviation, in Buchberger.Pcomb]
multTerm1 [abbreviation, in Buchberger.Pspminus]
multTerm1 [abbreviation, in Buchberger.DivTerm]
multTerm1 [abbreviation, in Buchberger.Pplus]
multTerm1 [abbreviation, in Buchberger.Pmult]
mult_div_id [lemma, in Buchberger.Monomials]
mult_div_com [lemma, in Buchberger.Monomials]
mult_mon_zero_l [lemma, in Buchberger.Monomials]
mult_mon_zero_r [lemma, in Buchberger.Monomials]
mult_mon_assoc [lemma, in Buchberger.Monomials]
mult_mon_com [lemma, in Buchberger.Monomials]
mult_mon [definition, in Buchberger.Monomials]
mult_invTerm_com_r [lemma, in Buchberger.Term]
mult_invTerm_com [lemma, in Buchberger.Term]
M1 [definition, in Buchberger.Term]
M1_min [projection, in Buchberger.OrderStructure]
N
nat_double_ind_set [lemma, in Buchberger.Dickson]NegRel [definition, in Buchberger.Dickson]
nf [definition, in Buchberger.BuchAux]
nf_Cb [lemma, in Buchberger.BuchAux]
nf_red [lemma, in Buchberger.BuchAux]
nf_irreducible [lemma, in Buchberger.BuchAux]
nf_divp_zero [lemma, in Buchberger.BuchRed]
nf_divp [lemma, in Buchberger.BuchRed]
nf1 [abbreviation, in Buchberger.WfR0]
nf1 [abbreviation, in Buchberger.Buch]
nf1 [abbreviation, in Buchberger.BuchRed]
nilGRBar [lemma, in Buchberger.Bar]
nillu1 [constructor, in Buchberger.Pplus]
nillu2 [constructor, in Buchberger.Pplus]
nmin [constructor, in Buchberger.OpenIndGoodRel]
not_nil_in_polySet [lemma, in Buchberger.Preduce]
not_nil_in_polySet_elm [lemma, in Buchberger.Preduce]
not_double_canonical [lemma, in Buchberger.POrder]
nzeroP_multTerm [lemma, in Buchberger.Term]
nzeroP_comp_eqTerm [lemma, in Buchberger.Term]
nZero_invTerm_T1 [lemma, in Buchberger.Term]
nZero_invTerm_nZero [lemma, in Buchberger.Term]
nZterm [definition, in Buchberger.POrder]
n_0 [constructor, in Buchberger.Monomials]
O
OBuch [inductive, in Buchberger.Buch]ObuchPincl [lemma, in Buchberger.Buch]
ObuchPred [lemma, in Buchberger.Buch]
ObuchQred [lemma, in Buchberger.Buch]
OBuch_Inv_f [lemma, in Buchberger.Buch]
OBuch_Stable_f [lemma, in Buchberger.Buch]
OBuch_Inv [lemma, in Buchberger.Buch]
OBuch_Stable [lemma, in Buchberger.Buch]
OBuch0 [constructor, in Buchberger.Buch]
OBuch1 [constructor, in Buchberger.Buch]
OBuch2 [constructor, in Buchberger.Buch]
olist [definition, in Buchberger.POrder]
olistO [lemma, in Buchberger.POrder]
olistOne [lemma, in Buchberger.POrder]
olist_pX_ltP [lemma, in Buchberger.POrder]
olist_imp_olist [lemma, in Buchberger.POrder]
olist_X [lemma, in Buchberger.POrder]
olist_pX_order [lemma, in Buchberger.POrder]
olist_pX_eqT [lemma, in Buchberger.POrder]
olist_cons [lemma, in Buchberger.POrder]
olist_ltT [lemma, in Buchberger.POrder]
one_minus_reduceplus [lemma, in Buchberger.Preduceplus]
one_plus_reduceplus [lemma, in Buchberger.Preduceplus]
OpenInd [lemma, in Buchberger.OpenIndGoodRel]
OpenIndGoodRel [section, in Buchberger.OpenIndGoodRel]
OpenIndGoodRel [library]
OpenIndGoodRel.A [variable, in Buchberger.OpenIndGoodRel]
OpenIndGoodRel.lt [variable, in Buchberger.OpenIndGoodRel]
OpenIndGoodRel.R [variable, in Buchberger.OpenIndGoodRel]
OpenIndGoodRel.wflt [variable, in Buchberger.OpenIndGoodRel]
Opm_ind [lemma, in Buchberger.Pminus]
orderc [inductive, in Buchberger.LexiOrder]
orderc_dec [lemma, in Buchberger.LexiOrder]
OrderStructure [record, in Buchberger.OrderStructure]
OrderStructure [library]
order_reduceplus [lemma, in Buchberger.Preduceplus]
order_minuspf [lemma, in Buchberger.Pminus]
order_pluspf [lemma, in Buchberger.Pminus]
order_minusP [lemma, in Buchberger.Pminus]
order_pluspf [lemma, in Buchberger.Pplus]
order_plusP [lemma, in Buchberger.Pplus]
P
pbuchf [definition, in Buchberger.Buch]pbuchf_Inv [lemma, in Buchberger.Buch]
pbuchf_Stable [lemma, in Buchberger.Buch]
Pcomb [section, in Buchberger.Pcomb]
Pcomb [library]
Pcomb.A [variable, in Buchberger.Pcomb]
Pcomb.A0 [variable, in Buchberger.Pcomb]
Pcomb.A1 [variable, in Buchberger.Pcomb]
Pcomb.cs [variable, in Buchberger.Pcomb]
Pcomb.divA [variable, in Buchberger.Pcomb]
Pcomb.eqA [variable, in Buchberger.Pcomb]
Pcomb.eqA_dec [variable, in Buchberger.Pcomb]
Pcomb.invA [variable, in Buchberger.Pcomb]
Pcomb.ltM [variable, in Buchberger.Pcomb]
Pcomb.ltM_dec [variable, in Buchberger.Pcomb]
Pcomb.minusA [variable, in Buchberger.Pcomb]
Pcomb.multA [variable, in Buchberger.Pcomb]
Pcomb.n [variable, in Buchberger.Pcomb]
Pcomb.os [variable, in Buchberger.Pcomb]
Pcomb.plusA [variable, in Buchberger.Pcomb]
Pcrit [library]
Peq [section, in Buchberger.Peq]
Peq [library]
Peq.A [variable, in Buchberger.Peq]
Peq.A0 [variable, in Buchberger.Peq]
Peq.A1 [variable, in Buchberger.Peq]
Peq.cs [variable, in Buchberger.Peq]
Peq.divA [variable, in Buchberger.Peq]
Peq.eqA [variable, in Buchberger.Peq]
Peq.eqA_dec [variable, in Buchberger.Peq]
Peq.eqTerm_imp_eqT [variable, in Buchberger.Peq]
Peq.invA [variable, in Buchberger.Peq]
Peq.ltM [variable, in Buchberger.Peq]
Peq.ltM_dec [variable, in Buchberger.Peq]
Peq.minusA [variable, in Buchberger.Peq]
Peq.multA [variable, in Buchberger.Peq]
Peq.n [variable, in Buchberger.Peq]
Peq.os [variable, in Buchberger.Peq]
Peq.plusA [variable, in Buchberger.Peq]
pickinSet [definition, in Buchberger.Preducestar]
pickinSet [definition, in Buchberger.Preducestar]
pickinSeteqp [constructor, in Buchberger.Preduce]
pickinSetp [inductive, in Buchberger.Preduce]
pickinSetp1 [abbreviation, in Buchberger.WfR0]
pickinSetp1 [abbreviation, in Buchberger.Buch]
pickinSetp1 [abbreviation, in Buchberger.BuchAux]
pickinSetp1 [abbreviation, in Buchberger.Preduceplus]
pickinSetp1 [abbreviation, in Buchberger.Preducestar]
pickinSetp1 [abbreviation, in Buchberger.Preducestar]
pickinSetp1 [abbreviation, in Buchberger.BuchRed]
pickinSetp1 [abbreviation, in Buchberger.Pspoly]
pickinSetp1 [abbreviation, in Buchberger.Pcrit]
pickinSetp1 [abbreviation, in Buchberger.Pcomb]
pickinSetskip [constructor, in Buchberger.Preduce]
pickin_is_pX [lemma, in Buchberger.Preduce]
pick_inv_eqT [lemma, in Buchberger.Preduce]
pick_inv_eqT_lem [lemma, in Buchberger.Preduce]
pick_inv_in [lemma, in Buchberger.Preduce]
plusA_A0 [projection, in Buchberger.CoefStructure]
plusA_eqA_comp [projection, in Buchberger.CoefStructure]
plusA_com [projection, in Buchberger.CoefStructure]
plusA_assoc [projection, in Buchberger.CoefStructure]
plusA_eqA_comp_r [lemma, in Buchberger.moreCoefStructure]
plusA_eqA_comp_l [lemma, in Buchberger.moreCoefStructure]
plusp [definition, in Buchberger.Pplus]
plusP [inductive, in Buchberger.Pplus]
pluspf [definition, in Buchberger.Pplus]
pluspf_is_minuspf [lemma, in Buchberger.Pminus]
pluspf_minuspf_id [lemma, in Buchberger.Pminus]
pluspf_assoc [lemma, in Buchberger.Pplus]
pluspf_inv2_eqa [lemma, in Buchberger.Pplus]
pluspf_inv1_eqa [lemma, in Buchberger.Pplus]
pluspf_inv3b_eq [lemma, in Buchberger.Pplus]
pluspf_inv3a_eq [lemma, in Buchberger.Pplus]
pluspf_inv2_eq [lemma, in Buchberger.Pplus]
pluspf_inv1_eq [lemma, in Buchberger.Pplus]
pluspf_com [lemma, in Buchberger.Pplus]
pluspf_inv3b [lemma, in Buchberger.Pplus]
pluspf_inv3a [lemma, in Buchberger.Pplus]
pluspf_inv2 [lemma, in Buchberger.Pplus]
pluspf_inv1 [lemma, in Buchberger.Pplus]
pluspf_is_plusP [lemma, in Buchberger.Pplus]
pluspf_pX [lemma, in Buchberger.Pmult]
pluspf1 [abbreviation, in Buchberger.Preduce]
pluspf1 [abbreviation, in Buchberger.WfR0]
pluspf1 [abbreviation, in Buchberger.Buch]
pluspf1 [abbreviation, in Buchberger.BuchAux]
pluspf1 [abbreviation, in Buchberger.Preduceplus]
pluspf1 [abbreviation, in Buchberger.Pmults]
pluspf1 [abbreviation, in Buchberger.Preducestar]
pluspf1 [abbreviation, in Buchberger.Preducestar]
pluspf1 [abbreviation, in Buchberger.BuchRed]
pluspf1 [abbreviation, in Buchberger.Pminus]
pluspf1 [abbreviation, in Buchberger.Pspoly]
pluspf1 [abbreviation, in Buchberger.Pcrit]
pluspf1 [abbreviation, in Buchberger.Pcomb]
pluspf1 [abbreviation, in Buchberger.Pspminus]
pluspf1 [abbreviation, in Buchberger.Pmult]
pluspf3_assoc [lemma, in Buchberger.Pplus]
plusP_uniq_eqP [lemma, in Buchberger.Pplus]
plusP_zero_pOr [lemma, in Buchberger.Pplus]
plusP_zero_pOl [lemma, in Buchberger.Pplus]
plusP_com [lemma, in Buchberger.Pplus]
plusP_inv3b [lemma, in Buchberger.Pplus]
plusP_inv3a [lemma, in Buchberger.Pplus]
plusP_inv2 [lemma, in Buchberger.Pplus]
plusP_inv1 [lemma, in Buchberger.Pplus]
plusP_decomp [lemma, in Buchberger.Pplus]
plusP_inv [lemma, in Buchberger.Pplus]
plusTerm [definition, in Buchberger.Term]
plusTerm_invTerm_zeroP [lemma, in Buchberger.Term]
plusTerm_assoc [lemma, in Buchberger.Term]
plusTerm_eqT2 [lemma, in Buchberger.Term]
plusTerm_eqT1 [lemma, in Buchberger.Term]
plusTerm_com [lemma, in Buchberger.Term]
plusTerm_comp_r [lemma, in Buchberger.Term]
plusTerm_comp_l [lemma, in Buchberger.Term]
plusTerm_is_pX [lemma, in Buchberger.Pplus]
plusTerm1 [abbreviation, in Buchberger.Preduce]
plusTerm1 [abbreviation, in Buchberger.Peq]
plusTerm1 [abbreviation, in Buchberger.POrder]
plusTerm1 [abbreviation, in Buchberger.WfR0]
plusTerm1 [abbreviation, in Buchberger.Buch]
plusTerm1 [abbreviation, in Buchberger.BuchAux]
plusTerm1 [abbreviation, in Buchberger.Preduceplus]
plusTerm1 [abbreviation, in Buchberger.Pmults]
plusTerm1 [abbreviation, in Buchberger.Preducestar]
plusTerm1 [abbreviation, in Buchberger.Preducestar]
plusTerm1 [abbreviation, in Buchberger.BuchRed]
plusTerm1 [abbreviation, in Buchberger.Pminus]
plusTerm1 [abbreviation, in Buchberger.Pspoly]
plusTerm1 [abbreviation, in Buchberger.Pcrit]
plusTerm1 [abbreviation, in Buchberger.Pcomb]
plusTerm1 [abbreviation, in Buchberger.Pspminus]
plusTerm1 [abbreviation, in Buchberger.DivTerm]
plusTerm1 [abbreviation, in Buchberger.Pplus]
plusTerm1 [abbreviation, in Buchberger.Pmult]
plus_minus_le [lemma, in Buchberger.Monomials]
Pminus [section, in Buchberger.Pminus]
Pminus [library]
Pminus.A [variable, in Buchberger.Pminus]
Pminus.A0 [variable, in Buchberger.Pminus]
Pminus.A1 [variable, in Buchberger.Pminus]
Pminus.cs [variable, in Buchberger.Pminus]
Pminus.divA [variable, in Buchberger.Pminus]
Pminus.eqA [variable, in Buchberger.Pminus]
Pminus.eqA_dec [variable, in Buchberger.Pminus]
Pminus.invA [variable, in Buchberger.Pminus]
Pminus.ltM [variable, in Buchberger.Pminus]
Pminus.ltM_dec [variable, in Buchberger.Pminus]
Pminus.minusA [variable, in Buchberger.Pminus]
Pminus.multA [variable, in Buchberger.Pminus]
Pminus.n [variable, in Buchberger.Pminus]
Pminus.os [variable, in Buchberger.Pminus]
Pminus.plusA [variable, in Buchberger.Pminus]
pmon1 [definition, in Buchberger.Monomials]
pmon2 [definition, in Buchberger.Monomials]
Pmult [section, in Buchberger.Pmult]
Pmult [library]
Pmults [section, in Buchberger.Pmults]
Pmults [library]
Pmults.A [variable, in Buchberger.Pmults]
Pmults.A0 [variable, in Buchberger.Pmults]
Pmults.A1 [variable, in Buchberger.Pmults]
Pmults.cs [variable, in Buchberger.Pmults]
Pmults.divA [variable, in Buchberger.Pmults]
Pmults.eqA [variable, in Buchberger.Pmults]
Pmults.eqA_dec [variable, in Buchberger.Pmults]
Pmults.ffst [variable, in Buchberger.Pmults]
Pmults.invA [variable, in Buchberger.Pmults]
Pmults.ltM [variable, in Buchberger.Pmults]
Pmults.ltM_dec [variable, in Buchberger.Pmults]
Pmults.minusA [variable, in Buchberger.Pmults]
Pmults.multA [variable, in Buchberger.Pmults]
Pmults.n [variable, in Buchberger.Pmults]
Pmults.os [variable, in Buchberger.Pmults]
Pmults.plusA [variable, in Buchberger.Pmults]
Pmults.ppair [variable, in Buchberger.Pmults]
Pmults.ssnd [variable, in Buchberger.Pmults]
Pmult.A [variable, in Buchberger.Pmult]
Pmult.A0 [variable, in Buchberger.Pmult]
Pmult.A1 [variable, in Buchberger.Pmult]
Pmult.cs [variable, in Buchberger.Pmult]
Pmult.divA [variable, in Buchberger.Pmult]
Pmult.eqA [variable, in Buchberger.Pmult]
Pmult.eqA_dec [variable, in Buchberger.Pmult]
Pmult.invA [variable, in Buchberger.Pmult]
Pmult.ltM [variable, in Buchberger.Pmult]
Pmult.ltM_dec [variable, in Buchberger.Pmult]
Pmult.minusA [variable, in Buchberger.Pmult]
Pmult.multA [variable, in Buchberger.Pmult]
Pmult.n [variable, in Buchberger.Pmult]
Pmult.os [variable, in Buchberger.Pmult]
Pmult.plusA [variable, in Buchberger.Pmult]
pO [definition, in Buchberger.POrder]
poly [definition, in Buchberger.POrder]
poly1 [abbreviation, in Buchberger.Preduce]
poly1 [abbreviation, in Buchberger.Peq]
poly1 [abbreviation, in Buchberger.WfR0]
poly1 [abbreviation, in Buchberger.Buch]
poly1 [abbreviation, in Buchberger.BuchAux]
poly1 [abbreviation, in Buchberger.Preduceplus]
poly1 [abbreviation, in Buchberger.Pmults]
poly1 [abbreviation, in Buchberger.Preducestar]
poly1 [abbreviation, in Buchberger.Preducestar]
poly1 [abbreviation, in Buchberger.BuchRed]
poly1 [abbreviation, in Buchberger.Pminus]
poly1 [abbreviation, in Buchberger.Pspoly]
poly1 [abbreviation, in Buchberger.Pcrit]
poly1 [abbreviation, in Buchberger.Pcomb]
poly1 [abbreviation, in Buchberger.Pspminus]
poly1 [abbreviation, in Buchberger.Pplus]
poly1 [abbreviation, in Buchberger.Pmult]
pOO [abbreviation, in Buchberger.Preduce]
pOO [abbreviation, in Buchberger.Peq]
pOO [abbreviation, in Buchberger.WfR0]
pOO [abbreviation, in Buchberger.Buch]
pOO [abbreviation, in Buchberger.BuchAux]
pOO [abbreviation, in Buchberger.Preduceplus]
pOO [abbreviation, in Buchberger.Pmults]
pOO [abbreviation, in Buchberger.Preducestar]
pOO [abbreviation, in Buchberger.Preducestar]
pOO [abbreviation, in Buchberger.BuchRed]
pOO [abbreviation, in Buchberger.Pminus]
pOO [abbreviation, in Buchberger.Pspoly]
pOO [abbreviation, in Buchberger.Pcrit]
pOO [abbreviation, in Buchberger.Pcomb]
pOO [abbreviation, in Buchberger.Pspminus]
pOO [abbreviation, in Buchberger.Pplus]
pOO [abbreviation, in Buchberger.Pmult]
Porder [section, in Buchberger.POrder]
POrder [library]
Porder.A [variable, in Buchberger.POrder]
Porder.A0 [variable, in Buchberger.POrder]
Porder.A1 [variable, in Buchberger.POrder]
Porder.consA [variable, in Buchberger.POrder]
Porder.cs [variable, in Buchberger.POrder]
Porder.DescA [variable, in Buchberger.POrder]
Porder.divA [variable, in Buchberger.POrder]
Porder.eqA [variable, in Buchberger.POrder]
Porder.eqA_dec [variable, in Buchberger.POrder]
Porder.eqT_refl [variable, in Buchberger.POrder]
Porder.invA [variable, in Buchberger.POrder]
Porder.listA [variable, in Buchberger.POrder]
Porder.ltM [variable, in Buchberger.POrder]
Porder.ltM_dec [variable, in Buchberger.POrder]
Porder.minusA [variable, in Buchberger.POrder]
Porder.multA [variable, in Buchberger.POrder]
Porder.n [variable, in Buchberger.POrder]
Porder.nilA [variable, in Buchberger.POrder]
Porder.os [variable, in Buchberger.POrder]
Porder.plusA [variable, in Buchberger.POrder]
pO_irreducible [lemma, in Buchberger.Preduce]
pO_reduce [lemma, in Buchberger.Preduce]
pO_reduceplus [lemma, in Buchberger.Preduceplus]
pO_reducestar [lemma, in Buchberger.Preducestar]
pO_reducestar [lemma, in Buchberger.Preducestar]
pO_minusP_inv2 [lemma, in Buchberger.Pminus]
pO_minusP_inv1 [lemma, in Buchberger.Pminus]
pO_pluspf_inv2 [lemma, in Buchberger.Pplus]
pO_pluspf_inv1 [lemma, in Buchberger.Pplus]
pO_plusP_inv2 [lemma, in Buchberger.Pplus]
pO_plusP_inv1 [lemma, in Buchberger.Pplus]
ppc [definition, in Buchberger.DivTerm]
ppcm [inductive, in Buchberger.DivTerm]
ppcm_mom_is_ppcm [lemma, in Buchberger.Monomials]
ppcm_prop_r [lemma, in Buchberger.Monomials]
ppcm_prop_l [lemma, in Buchberger.Monomials]
ppcm_com [lemma, in Buchberger.Monomials]
ppcm_mon [definition, in Buchberger.Monomials]
ppcm0 [constructor, in Buchberger.DivTerm]
ppcp [definition, in Buchberger.BuchAux]
ppcp1 [abbreviation, in Buchberger.WfR0]
ppcp1 [abbreviation, in Buchberger.Buch]
ppcp1 [abbreviation, in Buchberger.BuchRed]
ppc_multTerm_divP [lemma, in Buchberger.DivTerm]
ppc_is_ppcm [lemma, in Buchberger.DivTerm]
ppc_nZ [lemma, in Buchberger.DivTerm]
ppc_com [lemma, in Buchberger.DivTerm]
ppc1 [abbreviation, in Buchberger.Preduce]
ppc1 [abbreviation, in Buchberger.WfR0]
ppc1 [abbreviation, in Buchberger.Buch]
ppc1 [abbreviation, in Buchberger.BuchAux]
ppc1 [abbreviation, in Buchberger.Preduceplus]
ppc1 [abbreviation, in Buchberger.Preducestar]
ppc1 [abbreviation, in Buchberger.Preducestar]
ppc1 [abbreviation, in Buchberger.BuchRed]
ppc1 [abbreviation, in Buchberger.Pspoly]
ppc1 [abbreviation, in Buchberger.Pcrit]
ppc1 [abbreviation, in Buchberger.Pcomb]
ppc1 [abbreviation, in Buchberger.Pspminus]
Pplus [section, in Buchberger.Pplus]
Pplus [library]
Pplus.A [variable, in Buchberger.Pplus]
Pplus.A0 [variable, in Buchberger.Pplus]
Pplus.A1 [variable, in Buchberger.Pplus]
Pplus.cs [variable, in Buchberger.Pplus]
Pplus.divA [variable, in Buchberger.Pplus]
Pplus.eqA [variable, in Buchberger.Pplus]
Pplus.eqA_dec [variable, in Buchberger.Pplus]
Pplus.invA [variable, in Buchberger.Pplus]
Pplus.ltM [variable, in Buchberger.Pplus]
Pplus.ltM_dec [variable, in Buchberger.Pplus]
Pplus.minusA [variable, in Buchberger.Pplus]
Pplus.multA [variable, in Buchberger.Pplus]
Pplus.n [variable, in Buchberger.Pplus]
Pplus.os [variable, in Buchberger.Pplus]
Pplus.plusA [variable, in Buchberger.Pplus]
Pred [definition, in Buchberger.Bar]
Preduce [section, in Buchberger.Preduce]
Preduce [library]
Preduceplus [section, in Buchberger.Preduceplus]
Preduceplus [library]
Preduceplus.A [variable, in Buchberger.Preduceplus]
Preduceplus.A0 [variable, in Buchberger.Preduceplus]
Preduceplus.A1 [variable, in Buchberger.Preduceplus]
Preduceplus.cs [variable, in Buchberger.Preduceplus]
Preduceplus.divA [variable, in Buchberger.Preduceplus]
Preduceplus.eqA [variable, in Buchberger.Preduceplus]
Preduceplus.eqA_dec [variable, in Buchberger.Preduceplus]
Preduceplus.invA [variable, in Buchberger.Preduceplus]
Preduceplus.ltM [variable, in Buchberger.Preduceplus]
Preduceplus.ltM_dec [variable, in Buchberger.Preduceplus]
Preduceplus.minusA [variable, in Buchberger.Preduceplus]
Preduceplus.multA [variable, in Buchberger.Preduceplus]
Preduceplus.n [variable, in Buchberger.Preduceplus]
Preduceplus.os [variable, in Buchberger.Preduceplus]
Preduceplus.plusA [variable, in Buchberger.Preduceplus]
Preducestar [section, in Buchberger.Preducestar]
Preducestar [section, in Buchberger.Preducestar]
Preducestar [library]
Preducestar [library]
Preducestar.A [variable, in Buchberger.Preducestar]
Preducestar.A [variable, in Buchberger.Preducestar]
Preducestar.A0 [variable, in Buchberger.Preducestar]
Preducestar.A0 [variable, in Buchberger.Preducestar]
Preducestar.A1 [variable, in Buchberger.Preducestar]
Preducestar.A1 [variable, in Buchberger.Preducestar]
Preducestar.cs [variable, in Buchberger.Preducestar]
Preducestar.cs [variable, in Buchberger.Preducestar]
Preducestar.divA [variable, in Buchberger.Preducestar]
Preducestar.divA [variable, in Buchberger.Preducestar]
Preducestar.eqA [variable, in Buchberger.Preducestar]
Preducestar.eqA [variable, in Buchberger.Preducestar]
Preducestar.eqA_dec [variable, in Buchberger.Preducestar]
Preducestar.eqA_dec [variable, in Buchberger.Preducestar]
Preducestar.invA [variable, in Buchberger.Preducestar]
Preducestar.invA [variable, in Buchberger.Preducestar]
Preducestar.ltM [variable, in Buchberger.Preducestar]
Preducestar.ltM [variable, in Buchberger.Preducestar]
Preducestar.ltM_dec [variable, in Buchberger.Preducestar]
Preducestar.ltM_dec [variable, in Buchberger.Preducestar]
Preducestar.minusA [variable, in Buchberger.Preducestar]
Preducestar.minusA [variable, in Buchberger.Preducestar]
Preducestar.multA [variable, in Buchberger.Preducestar]
Preducestar.multA [variable, in Buchberger.Preducestar]
Preducestar.n [variable, in Buchberger.Preducestar]
Preducestar.n [variable, in Buchberger.Preducestar]
Preducestar.os [variable, in Buchberger.Preducestar]
Preducestar.os [variable, in Buchberger.Preducestar]
Preducestar.plusA [variable, in Buchberger.Preducestar]
Preducestar.plusA [variable, in Buchberger.Preducestar]
Preduce.A [variable, in Buchberger.Preduce]
Preduce.A0 [variable, in Buchberger.Preduce]
Preduce.A1 [variable, in Buchberger.Preduce]
Preduce.cs [variable, in Buchberger.Preduce]
Preduce.divA [variable, in Buchberger.Preduce]
Preduce.eqA [variable, in Buchberger.Preduce]
Preduce.eqA_dec [variable, in Buchberger.Preduce]
Preduce.invA [variable, in Buchberger.Preduce]
Preduce.ltM [variable, in Buchberger.Preduce]
Preduce.ltM_dec [variable, in Buchberger.Preduce]
Preduce.minusA [variable, in Buchberger.Preduce]
Preduce.multA [variable, in Buchberger.Preduce]
Preduce.n [variable, in Buchberger.Preduce]
Preduce.os [variable, in Buchberger.Preduce]
Preduce.plusA [variable, in Buchberger.Preduce]
ProdRel [definition, in Buchberger.Dickson]
prod_lt [definition, in Buchberger.Dickson]
projsig1 [definition, in Buchberger.Pplus]
proj_ok [lemma, in Buchberger.Monomials]
Pspminus [section, in Buchberger.Pspminus]
Pspminus [library]
Pspminus.A [variable, in Buchberger.Pspminus]
Pspminus.A0 [variable, in Buchberger.Pspminus]
Pspminus.A1 [variable, in Buchberger.Pspminus]
Pspminus.cs [variable, in Buchberger.Pspminus]
Pspminus.divA [variable, in Buchberger.Pspminus]
Pspminus.eqA [variable, in Buchberger.Pspminus]
Pspminus.eqA_dec [variable, in Buchberger.Pspminus]
Pspminus.invA [variable, in Buchberger.Pspminus]
Pspminus.ltM [variable, in Buchberger.Pspminus]
Pspminus.ltM_dec [variable, in Buchberger.Pspminus]
Pspminus.minusA [variable, in Buchberger.Pspminus]
Pspminus.multA [variable, in Buchberger.Pspminus]
Pspminus.n [variable, in Buchberger.Pspminus]
Pspminus.os [variable, in Buchberger.Pspminus]
Pspminus.plusA [variable, in Buchberger.Pspminus]
Pspoly [section, in Buchberger.Pspoly]
Pspoly [library]
Pspoly.A [variable, in Buchberger.Pspoly]
Pspoly.A0 [variable, in Buchberger.Pspoly]
Pspoly.A1 [variable, in Buchberger.Pspoly]
Pspoly.cs [variable, in Buchberger.Pspoly]
Pspoly.divA [variable, in Buchberger.Pspoly]
Pspoly.eqA [variable, in Buchberger.Pspoly]
Pspoly.eqA_dec [variable, in Buchberger.Pspoly]
Pspoly.invA [variable, in Buchberger.Pspoly]
Pspoly.ltM [variable, in Buchberger.Pspoly]
Pspoly.ltM_dec [variable, in Buchberger.Pspoly]
Pspoly.minusA [variable, in Buchberger.Pspoly]
Pspoly.multA [variable, in Buchberger.Pspoly]
Pspoly.n [variable, in Buchberger.Pspoly]
Pspoly.os [variable, in Buchberger.Pspoly]
Pspoly.plusA [variable, in Buchberger.Pspoly]
PtoS [definition, in Buchberger.Buch]
pX [definition, in Buchberger.POrder]
pX_invr [lemma, in Buchberger.Peq]
pX_invl [lemma, in Buchberger.Peq]
pX_inj [lemma, in Buchberger.Peq]
p0_pluspf_r [lemma, in Buchberger.Pplus]
p0_pluspf_l [lemma, in Buchberger.Pplus]
R
recomp [definition, in Buchberger.Monomials]recomp_ok [lemma, in Buchberger.Monomials]
red [definition, in Buchberger.BuchAux]
Red [definition, in Buchberger.BuchRed]
red [definition, in Buchberger.Fred]
redacc [definition, in Buchberger.BuchRed]
redacc [definition, in Buchberger.Fred]
redacc_divp [lemma, in Buchberger.BuchRed]
redacc_cb [lemma, in Buchberger.BuchRed]
redacc_divp [lemma, in Buchberger.Fred]
redacc_cb [lemma, in Buchberger.Fred]
redbuch [definition, in Buchberger.BuchRed]
redbuch_Grobner [lemma, in Buchberger.BuchRed]
redbuch_stable [lemma, in Buchberger.BuchRed]
redIn [inductive, in Buchberger.Buch]
redInclP [lemma, in Buchberger.Buch]
redInclR [lemma, in Buchberger.Buch]
redInInclQ [lemma, in Buchberger.Buch]
redIn_nil [lemma, in Buchberger.Buch]
redIn0 [constructor, in Buchberger.Buch]
redIn0b [constructor, in Buchberger.Buch]
redIn1 [constructor, in Buchberger.Buch]
redIn2 [constructor, in Buchberger.Buch]
redln_cons_gen [lemma, in Buchberger.Buch]
redln_cons [lemma, in Buchberger.Buch]
reds [inductive, in Buchberger.Buch]
reds_SpolyQ1 [lemma, in Buchberger.Buch]
reds_SpolyQ [lemma, in Buchberger.Buch]
reds_com [lemma, in Buchberger.Buch]
reds0 [constructor, in Buchberger.Buch]
reds1 [constructor, in Buchberger.Buch]
reduce [inductive, in Buchberger.Preduce]
Reduce [section, in Buchberger.Fred]
Reducef [definition, in Buchberger.Preducestar]
Reducef [definition, in Buchberger.Preducestar]
Reducef1 [abbreviation, in Buchberger.WfR0]
Reducef1 [abbreviation, in Buchberger.Buch]
Reducef1 [abbreviation, in Buchberger.BuchAux]
Reducef1 [abbreviation, in Buchberger.BuchRed]
Reducef1 [abbreviation, in Buchberger.Pspoly]
Reducef1 [abbreviation, in Buchberger.Pcrit]
Reducef1 [abbreviation, in Buchberger.Pcomb]
reducehead [inductive, in Buchberger.Preduce]
reduceheadO [constructor, in Buchberger.Preduce]
reducehead_imp_reduce [lemma, in Buchberger.Preduce]
reducep [definition, in Buchberger.BuchRed]
Reducep [inductive, in Buchberger.Pspoly]
reduceplus [inductive, in Buchberger.Preduceplus]
reduceplus_mults_inv [lemma, in Buchberger.Preduceplus]
reduceplus_mults_invf0 [lemma, in Buchberger.Preduceplus]
reduceplus_mults_invr [lemma, in Buchberger.Preduceplus]
reduceplus_mults_invr_lem [lemma, in Buchberger.Preduceplus]
reduceplus_mults [lemma, in Buchberger.Preduceplus]
reduceplus_skip [lemma, in Buchberger.Preduceplus]
reduceplus_trans [lemma, in Buchberger.Preduceplus]
reduceplus_eqp_com [lemma, in Buchberger.Preduceplus]
reduceplus_divp [lemma, in Buchberger.BuchRed]
reduceplus_divp_lem [lemma, in Buchberger.BuchRed]
reduceplus_cb2 [lemma, in Buchberger.Pcomb]
reduceplus_cb2_lem [lemma, in Buchberger.Pcomb]
reduceplus_cb1 [lemma, in Buchberger.Pcomb]
reduceplus_cb1_lem [lemma, in Buchberger.Pcomb]
reduceplus_cb [lemma, in Buchberger.Pcomb]
reduceplus1 [abbreviation, in Buchberger.WfR0]
reduceplus1 [abbreviation, in Buchberger.Buch]
reduceplus1 [abbreviation, in Buchberger.BuchAux]
reduceplus1 [abbreviation, in Buchberger.Preducestar]
reduceplus1 [abbreviation, in Buchberger.Preducestar]
reduceplus1 [abbreviation, in Buchberger.BuchRed]
reduceplus1 [abbreviation, in Buchberger.Pspoly]
reduceplus1 [abbreviation, in Buchberger.Pcrit]
reduceplus1 [abbreviation, in Buchberger.Pcomb]
Reducep0 [constructor, in Buchberger.Pspoly]
reduceskip [constructor, in Buchberger.Preduce]
reducestar [inductive, in Buchberger.Preducestar]
reducestar [inductive, in Buchberger.Preducestar]
reducestar_trans1 [abbreviation, in Buchberger.WfR0]
reducestar_trans1 [abbreviation, in Buchberger.Buch]
reducestar_trans1 [abbreviation, in Buchberger.BuchAux]
reducestar_in_pO [lemma, in Buchberger.Preducestar]
reducestar_pO_is_pO [lemma, in Buchberger.Preducestar]
reducestar_inv [lemma, in Buchberger.Preducestar]
reducestar_irreducible [lemma, in Buchberger.Preducestar]
reducestar_reduceplus [lemma, in Buchberger.Preducestar]
reducestar_trans [lemma, in Buchberger.Preducestar]
reducestar_eqp_com [lemma, in Buchberger.Preducestar]
reducestar_in_pO [lemma, in Buchberger.Preducestar]
reducestar_pO_is_pO [lemma, in Buchberger.Preducestar]
reducestar_inv [lemma, in Buchberger.Preducestar]
reducestar_irreducible [lemma, in Buchberger.Preducestar]
reducestar_reduceplus [lemma, in Buchberger.Preducestar]
reducestar_trans [lemma, in Buchberger.Preducestar]
reducestar_eqp_com [lemma, in Buchberger.Preducestar]
reducestar_divp [lemma, in Buchberger.BuchRed]
reducestar_trans1 [abbreviation, in Buchberger.BuchRed]
reducestar_trans1 [abbreviation, in Buchberger.Pspoly]
reducestar_trans1 [abbreviation, in Buchberger.Pcrit]
reducestar_cb2 [lemma, in Buchberger.Pcomb]
reducestar_cb1 [lemma, in Buchberger.Pcomb]
reducestar_cb [lemma, in Buchberger.Pcomb]
Reducestar_pO_imp_CombLinear [lemma, in Buchberger.Pcomb]
reducestar_trans1 [abbreviation, in Buchberger.Pcomb]
reducestar0 [constructor, in Buchberger.Preducestar]
reducestar0 [constructor, in Buchberger.Preducestar]
reducestar1 [abbreviation, in Buchberger.WfR0]
reducestar1 [abbreviation, in Buchberger.Buch]
reducestar1 [abbreviation, in Buchberger.BuchAux]
reducestar1 [abbreviation, in Buchberger.BuchRed]
reducestar1 [abbreviation, in Buchberger.Pspoly]
reducestar1 [abbreviation, in Buchberger.Pcrit]
reducestar1 [abbreviation, in Buchberger.Pcomb]
reducetop [constructor, in Buchberger.Preduce]
reducetopO_pO [lemma, in Buchberger.BuchAux]
reducetop_sp [lemma, in Buchberger.Preduce]
reduce_mults_invr [lemma, in Buchberger.Preduce]
reduce_mults_inv_lem [lemma, in Buchberger.Preduce]
reduce_mults [lemma, in Buchberger.Preduce]
reduce_mults_invf [lemma, in Buchberger.Preduce]
reduce_inv2 [lemma, in Buchberger.Preduce]
reduce_inv [lemma, in Buchberger.Preduce]
reduce_eqp_com [lemma, in Buchberger.Preduce]
reduce_in_pO [lemma, in Buchberger.Preduce]
reduce_plus_top [lemma, in Buchberger.Preduceplus]
reduce_imp_reduceplus [lemma, in Buchberger.Preduceplus]
reduce_divp [lemma, in Buchberger.BuchRed]
reduce_cb2 [lemma, in Buchberger.Pcomb]
reduce_cb1 [lemma, in Buchberger.Pcomb]
reduce_cb [lemma, in Buchberger.Pcomb]
Reduce.cb [variable, in Buchberger.Fred]
Reduce.cb_compo [variable, in Buchberger.Fred]
Reduce.cb_nf [variable, in Buchberger.Fred]
Reduce.cb_comp [variable, in Buchberger.Fred]
Reduce.cb_trans [variable, in Buchberger.Fred]
Reduce.cb_incl [variable, in Buchberger.Fred]
Reduce.cb_zerop [variable, in Buchberger.Fred]
Reduce.cb_id [variable, in Buchberger.Fred]
Reduce.def_grobner [variable, in Buchberger.Fred]
Reduce.divp [variable, in Buchberger.Fred]
Reduce.divp_trans [variable, in Buchberger.Fred]
Reduce.divp_id [variable, in Buchberger.Fred]
Reduce.div_reduce [variable, in Buchberger.Fred]
Reduce.grobner [variable, in Buchberger.Fred]
Reduce.grobner_def [variable, in Buchberger.Fred]
Reduce.nf [variable, in Buchberger.Fred]
Reduce.nf_div_zero1 [variable, in Buchberger.Fred]
Reduce.nf_div_zero [variable, in Buchberger.Fred]
Reduce.nf_div [variable, in Buchberger.Fred]
Reduce.nf_cb [variable, in Buchberger.Fred]
Reduce.poly [variable, in Buchberger.Fred]
Reduce.reduce [variable, in Buchberger.Fred]
Reduce.stable [variable, in Buchberger.Fred]
Reduce.zero [variable, in Buchberger.Fred]
Reduce.zerop [variable, in Buchberger.Fred]
Reduce.zerop_elim_cb [variable, in Buchberger.Fred]
Reduce.zerop_dec [variable, in Buchberger.Fred]
reduce0_reducestar [lemma, in Buchberger.Preducestar]
reduce0_reducestar [lemma, in Buchberger.Preducestar]
reduce1 [abbreviation, in Buchberger.WfR0]
reduce1 [abbreviation, in Buchberger.Buch]
reduce1 [abbreviation, in Buchberger.BuchAux]
reduce1 [abbreviation, in Buchberger.Preduceplus]
reduce1 [abbreviation, in Buchberger.Preducestar]
reduce1 [abbreviation, in Buchberger.Preducestar]
reduce1 [abbreviation, in Buchberger.BuchRed]
reduce1 [abbreviation, in Buchberger.Pspoly]
reduce1 [abbreviation, in Buchberger.Pcrit]
reduce1 [abbreviation, in Buchberger.Pcomb]
ReduStarConfluent [inductive, in Buchberger.Pspoly]
ReduStarConfluent0 [constructor, in Buchberger.Pspoly]
ReduStarConfluent1 [abbreviation, in Buchberger.WfR0]
ReduStarConfluent1 [abbreviation, in Buchberger.Buch]
ReduStarConfluent1 [abbreviation, in Buchberger.BuchAux]
ReduStarConfluent1 [abbreviation, in Buchberger.BuchRed]
ReduStarConfluent1 [abbreviation, in Buchberger.Pcrit]
ReduStarConfluent1 [abbreviation, in Buchberger.Pcomb]
red_gen_in [lemma, in Buchberger.Buch]
red_zerop [lemma, in Buchberger.BuchAux]
red_incl [lemma, in Buchberger.BuchAux]
red_id [lemma, in Buchberger.BuchAux]
red_cons [lemma, in Buchberger.BuchAux]
red_com [lemma, in Buchberger.BuchAux]
red_minus_zero_reduce [lemma, in Buchberger.Preduceplus]
red_plus_zero_reduce [lemma, in Buchberger.Preduceplus]
Red_grobner [lemma, in Buchberger.BuchRed]
Red_divp [lemma, in Buchberger.BuchRed]
Red_cb [lemma, in Buchberger.BuchRed]
red_grobner [lemma, in Buchberger.Fred]
red_divp [lemma, in Buchberger.Fred]
red_cb [lemma, in Buchberger.Fred]
red1 [abbreviation, in Buchberger.WfR0]
red1 [abbreviation, in Buchberger.Buch]
red1 [abbreviation, in Buchberger.BuchRed]
Rel [definition, in Buchberger.Bar]
rep_plus_zero_reduce [lemma, in Buchberger.Preduceplus]
rep_minus_reduce [lemma, in Buchberger.Preduceplus]
rep_plus_reduce [lemma, in Buchberger.Preduceplus]
rev_in [lemma, in Buchberger.ListProps]
rew_spminusf [lemma, in Buchberger.Pspminus]
RL [definition, in Buchberger.Buch]
Rminus [definition, in Buchberger.Pcrit]
Rminus_is_mult [lemma, in Buchberger.Pcrit]
Rminus_is_reduceplus [lemma, in Buchberger.Pcrit]
Rminus_in [lemma, in Buchberger.Pcrit]
RO [inductive, in Buchberger.WfR0]
RO_lem [lemma, in Buchberger.WfR0]
RO0 [constructor, in Buchberger.WfR0]
RO1 [abbreviation, in Buchberger.Buch]
rstar_rtopO [lemma, in Buchberger.BuchAux]
Rstar_n [constructor, in Buchberger.Preduceplus]
Rstar_0 [constructor, in Buchberger.Preduceplus]
S
Sdep [definition, in Buchberger.Buch]SearchE [constructor, in Buchberger.Bar]
SearchG [constructor, in Buchberger.Bar]
selectdivf [definition, in Buchberger.Preducestar]
selectdivf [definition, in Buchberger.Preducestar]
selectpolyf [definition, in Buchberger.Preducestar]
selectpolyf [definition, in Buchberger.Preducestar]
seqP [definition, in Buchberger.Peq]
seqp_dec1 [abbreviation, in Buchberger.Preduce]
seqp_trans [lemma, in Buchberger.Peq]
seqp_sym [lemma, in Buchberger.Peq]
seqp_refl [lemma, in Buchberger.Peq]
seqp_dec [lemma, in Buchberger.Peq]
seqp_dec1 [abbreviation, in Buchberger.WfR0]
seqp_dec1 [abbreviation, in Buchberger.Buch]
seqp_dec1 [abbreviation, in Buchberger.BuchAux]
seqp_dec1 [abbreviation, in Buchberger.Preduceplus]
seqp_dec1 [abbreviation, in Buchberger.Pmults]
seqp_dec1 [abbreviation, in Buchberger.Preducestar]
seqp_dec1 [abbreviation, in Buchberger.Preducestar]
seqp_dec1 [abbreviation, in Buchberger.BuchRed]
seqp_dec1 [abbreviation, in Buchberger.Pminus]
seqp_dec1 [abbreviation, in Buchberger.Pspoly]
seqp_dec1 [abbreviation, in Buchberger.Pcrit]
seqp_dec1 [abbreviation, in Buchberger.Pcomb]
seqp_dec1 [abbreviation, in Buchberger.Pspminus]
seqp_dec1 [abbreviation, in Buchberger.Pplus]
seqp_dec1 [abbreviation, in Buchberger.Pmult]
sgen [definition, in Buchberger.BuchAux]
size [definition, in Buchberger.Peq]
sizel [definition, in Buchberger.Peq]
sizel3 [definition, in Buchberger.Peq]
slice [definition, in Buchberger.Buch]
slicef [definition, in Buchberger.Buch]
slicef_incl [lemma, in Buchberger.Buch]
slice_Tl [lemma, in Buchberger.Buch]
slice_cons [lemma, in Buchberger.Buch]
slice_inv [lemma, in Buchberger.Buch]
sltP [definition, in Buchberger.POrder]
sltp_wf [lemma, in Buchberger.POrder]
sminus [definition, in Buchberger.Pminus]
smult [definition, in Buchberger.Pmult]
smults [definition, in Buchberger.Pmults]
sndL [definition, in Buchberger.Dickson]
splus [definition, in Buchberger.Pplus]
spminusf [definition, in Buchberger.Pspminus]
spminusf_plusTerm_z [lemma, in Buchberger.Pspminus]
spminusf_minusTerm_z [lemma, in Buchberger.Pspminus]
spminusf_minusTerm [lemma, in Buchberger.Pspminus]
spminusf_plusTerm_r [lemma, in Buchberger.Pspminus]
spminusf_minusTerm_r [lemma, in Buchberger.Pspminus]
spminusf_plusTerm_l [lemma, in Buchberger.Pspminus]
spminusf_minusTerm_l [lemma, in Buchberger.Pspminus]
spminusf_multTerm [lemma, in Buchberger.Pspminus]
spminusf_plusTerm [lemma, in Buchberger.Pspminus]
spminusf_minuspf [lemma, in Buchberger.Pspminus]
spminusf_pluspf [lemma, in Buchberger.Pspminus]
spminusf_extend [lemma, in Buchberger.Pspminus]
spminusf1 [abbreviation, in Buchberger.Preduce]
spminusf1 [abbreviation, in Buchberger.WfR0]
spminusf1 [abbreviation, in Buchberger.Buch]
spminusf1 [abbreviation, in Buchberger.BuchAux]
spminusf1 [abbreviation, in Buchberger.Preduceplus]
spminusf1 [abbreviation, in Buchberger.Preducestar]
spminusf1 [abbreviation, in Buchberger.Preducestar]
spminusf1 [abbreviation, in Buchberger.BuchRed]
spminusf1 [abbreviation, in Buchberger.Pspoly]
spminusf1 [abbreviation, in Buchberger.Pcrit]
spminusf1 [abbreviation, in Buchberger.Pcomb]
spO [definition, in Buchberger.BuchAux]
spolyf [definition, in Buchberger.Pspoly]
spolyf_def [lemma, in Buchberger.Pspoly]
spolyf_com [lemma, in Buchberger.Pspoly]
spolyf_pO [lemma, in Buchberger.Pspoly]
spolyf_canonical [lemma, in Buchberger.Pspoly]
spolyf1 [abbreviation, in Buchberger.WfR0]
spolyf1 [abbreviation, in Buchberger.Buch]
spolyf1 [abbreviation, in Buchberger.BuchAux]
spolyf1 [abbreviation, in Buchberger.BuchRed]
spolyf1 [abbreviation, in Buchberger.Pcrit]
spolyf1 [abbreviation, in Buchberger.Pcomb]
spolyp [definition, in Buchberger.BuchAux]
spolyp_addEnd_genPcPf [lemma, in Buchberger.Buch]
spolyp_cons_genPcP [lemma, in Buchberger.Buch]
spolyp_cons_genPcP0 [lemma, in Buchberger.Buch]
spolyp1 [abbreviation, in Buchberger.WfR0]
spolyp1 [abbreviation, in Buchberger.Buch]
spolyp1 [abbreviation, in Buchberger.BuchRed]
SpolyQ [inductive, in Buchberger.Pspoly]
SpolyQ_imp_ConfluentReduce [lemma, in Buchberger.Pcomb]
SpolyQ0 [constructor, in Buchberger.Pspoly]
SpolyQ1 [abbreviation, in Buchberger.WfR0]
SpolyQ1 [abbreviation, in Buchberger.Buch]
SpolyQ1 [abbreviation, in Buchberger.BuchAux]
SpolyQ1 [abbreviation, in Buchberger.BuchRed]
SpolyQ1 [abbreviation, in Buchberger.Pcrit]
SpolyQ1 [abbreviation, in Buchberger.Pcomb]
Spoly_11 [constructor, in Buchberger.Pspoly]
Spoly_10 [constructor, in Buchberger.Pspoly]
Spoly_1 [inductive, in Buchberger.Pspoly]
spoly_div_is_minus [lemma, in Buchberger.Pspoly]
spoly_is_minus [lemma, in Buchberger.Pspoly]
spoly_Reducestar_ppc [lemma, in Buchberger.Pcrit]
spoly_Reducestar_pO [lemma, in Buchberger.Pcrit]
spoly_reduceplus_pO [lemma, in Buchberger.Pcrit]
spoly_Reduce [lemma, in Buchberger.Pcrit]
Spoly1 [abbreviation, in Buchberger.WfR0]
Spoly1 [abbreviation, in Buchberger.Buch]
Spoly1 [abbreviation, in Buchberger.BuchAux]
Spoly1 [abbreviation, in Buchberger.BuchRed]
sp_Rminus [lemma, in Buchberger.Pcrit]
sp_rew [lemma, in Buchberger.Pspminus]
sp1 [definition, in Buchberger.BuchAux]
sscal [definition, in Buchberger.BuchAux]
stable [inductive, in Buchberger.Buch]
stable_sym [lemma, in Buchberger.Buch]
stable_trans [lemma, in Buchberger.Buch]
stable_refl [lemma, in Buchberger.Buch]
stable0 [constructor, in Buchberger.Buch]
stable1 [abbreviation, in Buchberger.BuchRed]
strip [definition, in Buchberger.Buch]
subPredExistsL [lemma, in Buchberger.Bar]
subRelGoodR [lemma, in Buchberger.Bar]
subRelGRBar [lemma, in Buchberger.Bar]
s2p [definition, in Buchberger.Preduce]
s2p1 [abbreviation, in Buchberger.WfR0]
s2p1 [abbreviation, in Buchberger.Buch]
s2p1 [abbreviation, in Buchberger.BuchAux]
s2p1 [abbreviation, in Buchberger.Preduceplus]
s2p1 [abbreviation, in Buchberger.Preducestar]
s2p1 [abbreviation, in Buchberger.Preducestar]
s2p1 [abbreviation, in Buchberger.BuchRed]
s2p1 [abbreviation, in Buchberger.Pspoly]
s2p1 [abbreviation, in Buchberger.Pcrit]
s2p1 [abbreviation, in Buchberger.Pcomb]
T
tdivExists_trmHd_lem [lemma, in Buchberger.Bar]tdivGoodP [lemma, in Buchberger.Bar]
Term [definition, in Buchberger.Term]
Term [section, in Buchberger.Term]
Term [library]
Term.A [variable, in Buchberger.Term]
Term.A0 [variable, in Buchberger.Term]
Term.A1 [variable, in Buchberger.Term]
Term.cs [variable, in Buchberger.Term]
Term.divA [variable, in Buchberger.Term]
Term.eqA [variable, in Buchberger.Term]
Term.eqA_dec [variable, in Buchberger.Term]
Term.invA [variable, in Buchberger.Term]
Term.ltM [variable, in Buchberger.Term]
Term.ltM_dec [variable, in Buchberger.Term]
Term.minusA [variable, in Buchberger.Term]
Term.multA [variable, in Buchberger.Term]
Term.n [variable, in Buchberger.Term]
Term.os [variable, in Buchberger.Term]
Term.plusA [variable, in Buchberger.Term]
Term1 [abbreviation, in Buchberger.Preduce]
Term1 [abbreviation, in Buchberger.Peq]
Term1 [abbreviation, in Buchberger.POrder]
Term1 [abbreviation, in Buchberger.WfR0]
Term1 [abbreviation, in Buchberger.Buch]
Term1 [abbreviation, in Buchberger.BuchAux]
Term1 [abbreviation, in Buchberger.Preduceplus]
Term1 [abbreviation, in Buchberger.Pmults]
Term1 [abbreviation, in Buchberger.Preducestar]
Term1 [abbreviation, in Buchberger.Preducestar]
Term1 [abbreviation, in Buchberger.BuchRed]
Term1 [abbreviation, in Buchberger.Pminus]
Term1 [abbreviation, in Buchberger.Pspoly]
Term1 [abbreviation, in Buchberger.Pcrit]
Term1 [abbreviation, in Buchberger.Pcomb]
Term1 [abbreviation, in Buchberger.Pspminus]
Term1 [abbreviation, in Buchberger.DivTerm]
Term1 [abbreviation, in Buchberger.Pplus]
Term1 [abbreviation, in Buchberger.Pmult]
thRO [section, in Buchberger.WfR0]
thRO.A [variable, in Buchberger.WfR0]
thRO.A0 [variable, in Buchberger.WfR0]
thRO.A1 [variable, in Buchberger.WfR0]
thRO.cs [variable, in Buchberger.WfR0]
thRO.divA [variable, in Buchberger.WfR0]
thRO.eqA [variable, in Buchberger.WfR0]
thRO.eqA_dec [variable, in Buchberger.WfR0]
thRO.invA [variable, in Buchberger.WfR0]
thRO.ltM [variable, in Buchberger.WfR0]
thRO.ltM_dec [variable, in Buchberger.WfR0]
thRO.minusA [variable, in Buchberger.WfR0]
thRO.multA [variable, in Buchberger.WfR0]
thRO.n [variable, in Buchberger.WfR0]
thRO.os [variable, in Buchberger.WfR0]
thRO.plusA [variable, in Buchberger.WfR0]
Tl [definition, in Buchberger.Buch]
tmults [definition, in Buchberger.Pmults]
tmults_zerop_eqp_pO [lemma, in Buchberger.Pmults]
total_orderc_dec [lemma, in Buchberger.LexiOrder]
total_orderc1 [constructor, in Buchberger.LexiOrder]
total_orderc0 [constructor, in Buchberger.LexiOrder]
total_orderc [inductive, in Buchberger.LexiOrder]
twoP_ind [definition, in Buchberger.Pmults]
T1 [definition, in Buchberger.Term]
T1_is_min_ltT [lemma, in Buchberger.POrder]
T1_eqT [lemma, in Buchberger.Term]
T1_multTerm_r [lemma, in Buchberger.Term]
T1_multTerm_l [lemma, in Buchberger.Term]
T1_nz [lemma, in Buchberger.Term]
T2M [definition, in Buchberger.Term]
U
uniq_minusp [lemma, in Buchberger.Pminus]uniq_plusp [lemma, in Buchberger.Pplus]
unit [definition, in Buchberger.BuchAux]
unit_nZ [lemma, in Buchberger.BuchAux]
unit_T1 [lemma, in Buchberger.BuchAux]
unit1 [abbreviation, in Buchberger.BuchRed]
W
WFlem1 [lemma, in Buchberger.Dickson]WfR0 [library]
wf_lessP3 [lemma, in Buchberger.Peq]
wf_lessP [lemma, in Buchberger.Peq]
wf_incl [lemma, in Buchberger.WfR0]
wf_RL [lemma, in Buchberger.Buch]
wf_Co [lemma, in Buchberger.Buch]
wf_Fl [lemma, in Buchberger.Buch]
wf_Tl [lemma, in Buchberger.Buch]
WR [definition, in Buchberger.Bar]
Z
zerop [definition, in Buchberger.BuchAux]zeroP [definition, in Buchberger.Term]
zeroP_dec1 [abbreviation, in Buchberger.Preduce]
zeroP_dec1 [abbreviation, in Buchberger.Peq]
zeroP_dec1 [abbreviation, in Buchberger.POrder]
zerop_dec1 [abbreviation, in Buchberger.WfR0]
zeroP_dec1 [abbreviation, in Buchberger.WfR0]
zerop_dec1 [abbreviation, in Buchberger.Buch]
zeroP_dec1 [abbreviation, in Buchberger.Buch]
zerop_red [lemma, in Buchberger.BuchAux]
zerop_red_spoly_r [lemma, in Buchberger.BuchAux]
zerop_red_spoly_l [lemma, in Buchberger.BuchAux]
zerop_ddivp_ppc [lemma, in Buchberger.BuchAux]
zerop_dec [lemma, in Buchberger.BuchAux]
zeroP_dec1 [abbreviation, in Buchberger.BuchAux]
zeroP_dec1 [abbreviation, in Buchberger.Preduceplus]
zeroP_dec1 [abbreviation, in Buchberger.Pmults]
zeroP_dec1 [abbreviation, in Buchberger.Preducestar]
zeroP_dec1 [abbreviation, in Buchberger.Preducestar]
zerop_nf_cb [lemma, in Buchberger.BuchRed]
zerop_elim_cb [lemma, in Buchberger.BuchRed]
zerop_elim_Cb [lemma, in Buchberger.BuchRed]
zerop_dec1 [abbreviation, in Buchberger.BuchRed]
zeroP_dec1 [abbreviation, in Buchberger.BuchRed]
zerop_is_eqTerm [lemma, in Buchberger.Pminus]
zeroP_dec1 [abbreviation, in Buchberger.Pminus]
zeroP_minusTerm [lemma, in Buchberger.Term]
zeroP_invTerm_zeroP [lemma, in Buchberger.Term]
zeroP_multTerm_r [lemma, in Buchberger.Term]
zeroP_multTerm_l [lemma, in Buchberger.Term]
zeroP_plusTerml [lemma, in Buchberger.Term]
zeroP_plusTermr [lemma, in Buchberger.Term]
zeroP_comp_eqTerm [lemma, in Buchberger.Term]
zeroP_dec [lemma, in Buchberger.Term]
zeroP_dec1 [abbreviation, in Buchberger.Pspoly]
zeroP_dec1 [abbreviation, in Buchberger.Pcrit]
zeroP_dec1 [abbreviation, in Buchberger.Pcomb]
zerop_nf_cb [lemma, in Buchberger.Fred]
zeroP_dec1 [abbreviation, in Buchberger.Pspminus]
zeroP_divTerm [lemma, in Buchberger.DivTerm]
zeroP_dec1 [abbreviation, in Buchberger.DivTerm]
zeroP_dec1 [abbreviation, in Buchberger.Pplus]
zeroP_dec1 [abbreviation, in Buchberger.Pmult]
zeroP1 [abbreviation, in Buchberger.Preduce]
zeroP1 [abbreviation, in Buchberger.Peq]
zeroP1 [abbreviation, in Buchberger.POrder]
zerop1 [abbreviation, in Buchberger.WfR0]
zeroP1 [abbreviation, in Buchberger.WfR0]
zerop1 [abbreviation, in Buchberger.Buch]
zeroP1 [abbreviation, in Buchberger.Buch]
zeroP1 [abbreviation, in Buchberger.BuchAux]
zeroP1 [abbreviation, in Buchberger.Preduceplus]
zeroP1 [abbreviation, in Buchberger.Pmults]
zeroP1 [abbreviation, in Buchberger.Preducestar]
zeroP1 [abbreviation, in Buchberger.Preducestar]
zerop1 [abbreviation, in Buchberger.BuchRed]
zeroP1 [abbreviation, in Buchberger.BuchRed]
zeroP1 [abbreviation, in Buchberger.Pminus]
zeroP1 [abbreviation, in Buchberger.Pspoly]
zeroP1 [abbreviation, in Buchberger.Pcrit]
zeroP1 [abbreviation, in Buchberger.Pcomb]
zeroP1 [abbreviation, in Buchberger.Pspminus]
zeroP1 [abbreviation, in Buchberger.DivTerm]
zeroP1 [abbreviation, in Buchberger.Pplus]
zeroP1 [abbreviation, in Buchberger.Pmult]
zero_mon [definition, in Buchberger.Monomials]
zRV_WR [lemma, in Buchberger.Dickson]
Variable Index
B
BuchAux.A [in Buchberger.BuchAux]BuchAux.A0 [in Buchberger.BuchAux]
BuchAux.A1 [in Buchberger.BuchAux]
BuchAux.cs [in Buchberger.BuchAux]
BuchAux.divA [in Buchberger.BuchAux]
BuchAux.eqA [in Buchberger.BuchAux]
BuchAux.eqA_dec [in Buchberger.BuchAux]
BuchAux.invA [in Buchberger.BuchAux]
BuchAux.ltM [in Buchberger.BuchAux]
BuchAux.ltM_dec [in Buchberger.BuchAux]
BuchAux.minusA [in Buchberger.BuchAux]
BuchAux.multA [in Buchberger.BuchAux]
BuchAux.n [in Buchberger.BuchAux]
BuchAux.os [in Buchberger.BuchAux]
BuchAux.plusA [in Buchberger.BuchAux]
BuchRed.A [in Buchberger.BuchRed]
BuchRed.A0 [in Buchberger.BuchRed]
BuchRed.A1 [in Buchberger.BuchRed]
BuchRed.cs [in Buchberger.BuchRed]
BuchRed.divA [in Buchberger.BuchRed]
BuchRed.eqA [in Buchberger.BuchRed]
BuchRed.eqA_dec [in Buchberger.BuchRed]
BuchRed.invA [in Buchberger.BuchRed]
BuchRed.ltM [in Buchberger.BuchRed]
BuchRed.ltM_dec [in Buchberger.BuchRed]
BuchRed.minusA [in Buchberger.BuchRed]
BuchRed.multA [in Buchberger.BuchRed]
BuchRed.n [in Buchberger.BuchRed]
BuchRed.os [in Buchberger.BuchRed]
BuchRed.plusA [in Buchberger.BuchRed]
Buch.A [in Buchberger.Buch]
Buch.A0 [in Buchberger.Buch]
Buch.A1 [in Buchberger.Buch]
Buch.Co [in Buchberger.Buch]
Buch.cs [in Buchberger.Buch]
Buch.divA [in Buchberger.Buch]
Buch.eqA [in Buchberger.Buch]
Buch.eqA_dec [in Buchberger.Buch]
Buch.FPset [in Buchberger.Buch]
Buch.invA [in Buchberger.Buch]
Buch.ltM [in Buchberger.Buch]
Buch.ltM_dec [in Buchberger.Buch]
Buch.minusA [in Buchberger.Buch]
Buch.multA [in Buchberger.Buch]
Buch.n [in Buchberger.Buch]
Buch.os [in Buchberger.Buch]
Buch.plusA [in Buchberger.Buch]
C
crit.A [in Buchberger.Pcrit]crit.A0 [in Buchberger.Pcrit]
crit.A1 [in Buchberger.Pcrit]
crit.cs [in Buchberger.Pcrit]
crit.divA [in Buchberger.Pcrit]
crit.eqA [in Buchberger.Pcrit]
crit.eqA_dec [in Buchberger.Pcrit]
crit.invA [in Buchberger.Pcrit]
crit.ltM [in Buchberger.Pcrit]
crit.ltM_dec [in Buchberger.Pcrit]
crit.minusA [in Buchberger.Pcrit]
crit.multA [in Buchberger.Pcrit]
crit.n [in Buchberger.Pcrit]
crit.os [in Buchberger.Pcrit]
crit.plusA [in Buchberger.Pcrit]
D
Dickson.A [in Buchberger.Dickson]Dickson.B [in Buchberger.Dickson]
Dickson.declt [in Buchberger.Dickson]
Dickson.lt [in Buchberger.Dickson]
Dickson.R [in Buchberger.Dickson]
Dickson.wfgt [in Buchberger.Dickson]
Dickson.wR [in Buchberger.Dickson]
DivTerm.A [in Buchberger.DivTerm]
DivTerm.A0 [in Buchberger.DivTerm]
DivTerm.A1 [in Buchberger.DivTerm]
DivTerm.cs [in Buchberger.DivTerm]
DivTerm.divA [in Buchberger.DivTerm]
DivTerm.eqA [in Buchberger.DivTerm]
DivTerm.eqA_dec [in Buchberger.DivTerm]
DivTerm.gb [in Buchberger.DivTerm]
DivTerm.gm [in Buchberger.DivTerm]
DivTerm.invA [in Buchberger.DivTerm]
DivTerm.ltM [in Buchberger.DivTerm]
DivTerm.ltM_dec [in Buchberger.DivTerm]
DivTerm.minusA [in Buchberger.DivTerm]
DivTerm.multA [in Buchberger.DivTerm]
DivTerm.n [in Buchberger.DivTerm]
DivTerm.os [in Buchberger.DivTerm]
DivTerm.plusA [in Buchberger.DivTerm]
L
lems.tdiv [in Buchberger.Bar]lems.trm [in Buchberger.Bar]
M
mCoef.A [in Buchberger.moreCoefStructure]mCoef.A0 [in Buchberger.moreCoefStructure]
mCoef.A1 [in Buchberger.moreCoefStructure]
mCoef.cs [in Buchberger.moreCoefStructure]
mCoef.divA [in Buchberger.moreCoefStructure]
mCoef.eqA [in Buchberger.moreCoefStructure]
mCoef.eqA_sym [in Buchberger.moreCoefStructure]
mCoef.eqA_trans [in Buchberger.moreCoefStructure]
mCoef.eqA_dec [in Buchberger.moreCoefStructure]
mCoef.invA [in Buchberger.moreCoefStructure]
mCoef.minusA [in Buchberger.moreCoefStructure]
mCoef.multA [in Buchberger.moreCoefStructure]
mCoef.plusA [in Buchberger.moreCoefStructure]
Monomials.gb [in Buchberger.Monomials]
Monomials.gm [in Buchberger.Monomials]
O
OpenIndGoodRel.A [in Buchberger.OpenIndGoodRel]OpenIndGoodRel.lt [in Buchberger.OpenIndGoodRel]
OpenIndGoodRel.R [in Buchberger.OpenIndGoodRel]
OpenIndGoodRel.wflt [in Buchberger.OpenIndGoodRel]
P
Pcomb.A [in Buchberger.Pcomb]Pcomb.A0 [in Buchberger.Pcomb]
Pcomb.A1 [in Buchberger.Pcomb]
Pcomb.cs [in Buchberger.Pcomb]
Pcomb.divA [in Buchberger.Pcomb]
Pcomb.eqA [in Buchberger.Pcomb]
Pcomb.eqA_dec [in Buchberger.Pcomb]
Pcomb.invA [in Buchberger.Pcomb]
Pcomb.ltM [in Buchberger.Pcomb]
Pcomb.ltM_dec [in Buchberger.Pcomb]
Pcomb.minusA [in Buchberger.Pcomb]
Pcomb.multA [in Buchberger.Pcomb]
Pcomb.n [in Buchberger.Pcomb]
Pcomb.os [in Buchberger.Pcomb]
Pcomb.plusA [in Buchberger.Pcomb]
Peq.A [in Buchberger.Peq]
Peq.A0 [in Buchberger.Peq]
Peq.A1 [in Buchberger.Peq]
Peq.cs [in Buchberger.Peq]
Peq.divA [in Buchberger.Peq]
Peq.eqA [in Buchberger.Peq]
Peq.eqA_dec [in Buchberger.Peq]
Peq.eqTerm_imp_eqT [in Buchberger.Peq]
Peq.invA [in Buchberger.Peq]
Peq.ltM [in Buchberger.Peq]
Peq.ltM_dec [in Buchberger.Peq]
Peq.minusA [in Buchberger.Peq]
Peq.multA [in Buchberger.Peq]
Peq.n [in Buchberger.Peq]
Peq.os [in Buchberger.Peq]
Peq.plusA [in Buchberger.Peq]
Pminus.A [in Buchberger.Pminus]
Pminus.A0 [in Buchberger.Pminus]
Pminus.A1 [in Buchberger.Pminus]
Pminus.cs [in Buchberger.Pminus]
Pminus.divA [in Buchberger.Pminus]
Pminus.eqA [in Buchberger.Pminus]
Pminus.eqA_dec [in Buchberger.Pminus]
Pminus.invA [in Buchberger.Pminus]
Pminus.ltM [in Buchberger.Pminus]
Pminus.ltM_dec [in Buchberger.Pminus]
Pminus.minusA [in Buchberger.Pminus]
Pminus.multA [in Buchberger.Pminus]
Pminus.n [in Buchberger.Pminus]
Pminus.os [in Buchberger.Pminus]
Pminus.plusA [in Buchberger.Pminus]
Pmults.A [in Buchberger.Pmults]
Pmults.A0 [in Buchberger.Pmults]
Pmults.A1 [in Buchberger.Pmults]
Pmults.cs [in Buchberger.Pmults]
Pmults.divA [in Buchberger.Pmults]
Pmults.eqA [in Buchberger.Pmults]
Pmults.eqA_dec [in Buchberger.Pmults]
Pmults.ffst [in Buchberger.Pmults]
Pmults.invA [in Buchberger.Pmults]
Pmults.ltM [in Buchberger.Pmults]
Pmults.ltM_dec [in Buchberger.Pmults]
Pmults.minusA [in Buchberger.Pmults]
Pmults.multA [in Buchberger.Pmults]
Pmults.n [in Buchberger.Pmults]
Pmults.os [in Buchberger.Pmults]
Pmults.plusA [in Buchberger.Pmults]
Pmults.ppair [in Buchberger.Pmults]
Pmults.ssnd [in Buchberger.Pmults]
Pmult.A [in Buchberger.Pmult]
Pmult.A0 [in Buchberger.Pmult]
Pmult.A1 [in Buchberger.Pmult]
Pmult.cs [in Buchberger.Pmult]
Pmult.divA [in Buchberger.Pmult]
Pmult.eqA [in Buchberger.Pmult]
Pmult.eqA_dec [in Buchberger.Pmult]
Pmult.invA [in Buchberger.Pmult]
Pmult.ltM [in Buchberger.Pmult]
Pmult.ltM_dec [in Buchberger.Pmult]
Pmult.minusA [in Buchberger.Pmult]
Pmult.multA [in Buchberger.Pmult]
Pmult.n [in Buchberger.Pmult]
Pmult.os [in Buchberger.Pmult]
Pmult.plusA [in Buchberger.Pmult]
Porder.A [in Buchberger.POrder]
Porder.A0 [in Buchberger.POrder]
Porder.A1 [in Buchberger.POrder]
Porder.consA [in Buchberger.POrder]
Porder.cs [in Buchberger.POrder]
Porder.DescA [in Buchberger.POrder]
Porder.divA [in Buchberger.POrder]
Porder.eqA [in Buchberger.POrder]
Porder.eqA_dec [in Buchberger.POrder]
Porder.eqT_refl [in Buchberger.POrder]
Porder.invA [in Buchberger.POrder]
Porder.listA [in Buchberger.POrder]
Porder.ltM [in Buchberger.POrder]
Porder.ltM_dec [in Buchberger.POrder]
Porder.minusA [in Buchberger.POrder]
Porder.multA [in Buchberger.POrder]
Porder.n [in Buchberger.POrder]
Porder.nilA [in Buchberger.POrder]
Porder.os [in Buchberger.POrder]
Porder.plusA [in Buchberger.POrder]
Pplus.A [in Buchberger.Pplus]
Pplus.A0 [in Buchberger.Pplus]
Pplus.A1 [in Buchberger.Pplus]
Pplus.cs [in Buchberger.Pplus]
Pplus.divA [in Buchberger.Pplus]
Pplus.eqA [in Buchberger.Pplus]
Pplus.eqA_dec [in Buchberger.Pplus]
Pplus.invA [in Buchberger.Pplus]
Pplus.ltM [in Buchberger.Pplus]
Pplus.ltM_dec [in Buchberger.Pplus]
Pplus.minusA [in Buchberger.Pplus]
Pplus.multA [in Buchberger.Pplus]
Pplus.n [in Buchberger.Pplus]
Pplus.os [in Buchberger.Pplus]
Pplus.plusA [in Buchberger.Pplus]
Preduceplus.A [in Buchberger.Preduceplus]
Preduceplus.A0 [in Buchberger.Preduceplus]
Preduceplus.A1 [in Buchberger.Preduceplus]
Preduceplus.cs [in Buchberger.Preduceplus]
Preduceplus.divA [in Buchberger.Preduceplus]
Preduceplus.eqA [in Buchberger.Preduceplus]
Preduceplus.eqA_dec [in Buchberger.Preduceplus]
Preduceplus.invA [in Buchberger.Preduceplus]
Preduceplus.ltM [in Buchberger.Preduceplus]
Preduceplus.ltM_dec [in Buchberger.Preduceplus]
Preduceplus.minusA [in Buchberger.Preduceplus]
Preduceplus.multA [in Buchberger.Preduceplus]
Preduceplus.n [in Buchberger.Preduceplus]
Preduceplus.os [in Buchberger.Preduceplus]
Preduceplus.plusA [in Buchberger.Preduceplus]
Preducestar.A [in Buchberger.Preducestar]
Preducestar.A [in Buchberger.Preducestar]
Preducestar.A0 [in Buchberger.Preducestar]
Preducestar.A0 [in Buchberger.Preducestar]
Preducestar.A1 [in Buchberger.Preducestar]
Preducestar.A1 [in Buchberger.Preducestar]
Preducestar.cs [in Buchberger.Preducestar]
Preducestar.cs [in Buchberger.Preducestar]
Preducestar.divA [in Buchberger.Preducestar]
Preducestar.divA [in Buchberger.Preducestar]
Preducestar.eqA [in Buchberger.Preducestar]
Preducestar.eqA [in Buchberger.Preducestar]
Preducestar.eqA_dec [in Buchberger.Preducestar]
Preducestar.eqA_dec [in Buchberger.Preducestar]
Preducestar.invA [in Buchberger.Preducestar]
Preducestar.invA [in Buchberger.Preducestar]
Preducestar.ltM [in Buchberger.Preducestar]
Preducestar.ltM [in Buchberger.Preducestar]
Preducestar.ltM_dec [in Buchberger.Preducestar]
Preducestar.ltM_dec [in Buchberger.Preducestar]
Preducestar.minusA [in Buchberger.Preducestar]
Preducestar.minusA [in Buchberger.Preducestar]
Preducestar.multA [in Buchberger.Preducestar]
Preducestar.multA [in Buchberger.Preducestar]
Preducestar.n [in Buchberger.Preducestar]
Preducestar.n [in Buchberger.Preducestar]
Preducestar.os [in Buchberger.Preducestar]
Preducestar.os [in Buchberger.Preducestar]
Preducestar.plusA [in Buchberger.Preducestar]
Preducestar.plusA [in Buchberger.Preducestar]
Preduce.A [in Buchberger.Preduce]
Preduce.A0 [in Buchberger.Preduce]
Preduce.A1 [in Buchberger.Preduce]
Preduce.cs [in Buchberger.Preduce]
Preduce.divA [in Buchberger.Preduce]
Preduce.eqA [in Buchberger.Preduce]
Preduce.eqA_dec [in Buchberger.Preduce]
Preduce.invA [in Buchberger.Preduce]
Preduce.ltM [in Buchberger.Preduce]
Preduce.ltM_dec [in Buchberger.Preduce]
Preduce.minusA [in Buchberger.Preduce]
Preduce.multA [in Buchberger.Preduce]
Preduce.n [in Buchberger.Preduce]
Preduce.os [in Buchberger.Preduce]
Preduce.plusA [in Buchberger.Preduce]
Pspminus.A [in Buchberger.Pspminus]
Pspminus.A0 [in Buchberger.Pspminus]
Pspminus.A1 [in Buchberger.Pspminus]
Pspminus.cs [in Buchberger.Pspminus]
Pspminus.divA [in Buchberger.Pspminus]
Pspminus.eqA [in Buchberger.Pspminus]
Pspminus.eqA_dec [in Buchberger.Pspminus]
Pspminus.invA [in Buchberger.Pspminus]
Pspminus.ltM [in Buchberger.Pspminus]
Pspminus.ltM_dec [in Buchberger.Pspminus]
Pspminus.minusA [in Buchberger.Pspminus]
Pspminus.multA [in Buchberger.Pspminus]
Pspminus.n [in Buchberger.Pspminus]
Pspminus.os [in Buchberger.Pspminus]
Pspminus.plusA [in Buchberger.Pspminus]
Pspoly.A [in Buchberger.Pspoly]
Pspoly.A0 [in Buchberger.Pspoly]
Pspoly.A1 [in Buchberger.Pspoly]
Pspoly.cs [in Buchberger.Pspoly]
Pspoly.divA [in Buchberger.Pspoly]
Pspoly.eqA [in Buchberger.Pspoly]
Pspoly.eqA_dec [in Buchberger.Pspoly]
Pspoly.invA [in Buchberger.Pspoly]
Pspoly.ltM [in Buchberger.Pspoly]
Pspoly.ltM_dec [in Buchberger.Pspoly]
Pspoly.minusA [in Buchberger.Pspoly]
Pspoly.multA [in Buchberger.Pspoly]
Pspoly.n [in Buchberger.Pspoly]
Pspoly.os [in Buchberger.Pspoly]
Pspoly.plusA [in Buchberger.Pspoly]
R
Reduce.cb [in Buchberger.Fred]Reduce.cb_compo [in Buchberger.Fred]
Reduce.cb_nf [in Buchberger.Fred]
Reduce.cb_comp [in Buchberger.Fred]
Reduce.cb_trans [in Buchberger.Fred]
Reduce.cb_incl [in Buchberger.Fred]
Reduce.cb_zerop [in Buchberger.Fred]
Reduce.cb_id [in Buchberger.Fred]
Reduce.def_grobner [in Buchberger.Fred]
Reduce.divp [in Buchberger.Fred]
Reduce.divp_trans [in Buchberger.Fred]
Reduce.divp_id [in Buchberger.Fred]
Reduce.div_reduce [in Buchberger.Fred]
Reduce.grobner [in Buchberger.Fred]
Reduce.grobner_def [in Buchberger.Fred]
Reduce.nf [in Buchberger.Fred]
Reduce.nf_div_zero1 [in Buchberger.Fred]
Reduce.nf_div_zero [in Buchberger.Fred]
Reduce.nf_div [in Buchberger.Fred]
Reduce.nf_cb [in Buchberger.Fred]
Reduce.poly [in Buchberger.Fred]
Reduce.reduce [in Buchberger.Fred]
Reduce.stable [in Buchberger.Fred]
Reduce.zero [in Buchberger.Fred]
Reduce.zerop [in Buchberger.Fred]
Reduce.zerop_elim_cb [in Buchberger.Fred]
Reduce.zerop_dec [in Buchberger.Fred]
T
Term.A [in Buchberger.Term]Term.A0 [in Buchberger.Term]
Term.A1 [in Buchberger.Term]
Term.cs [in Buchberger.Term]
Term.divA [in Buchberger.Term]
Term.eqA [in Buchberger.Term]
Term.eqA_dec [in Buchberger.Term]
Term.invA [in Buchberger.Term]
Term.ltM [in Buchberger.Term]
Term.ltM_dec [in Buchberger.Term]
Term.minusA [in Buchberger.Term]
Term.multA [in Buchberger.Term]
Term.n [in Buchberger.Term]
Term.os [in Buchberger.Term]
Term.plusA [in Buchberger.Term]
thRO.A [in Buchberger.WfR0]
thRO.A0 [in Buchberger.WfR0]
thRO.A1 [in Buchberger.WfR0]
thRO.cs [in Buchberger.WfR0]
thRO.divA [in Buchberger.WfR0]
thRO.eqA [in Buchberger.WfR0]
thRO.eqA_dec [in Buchberger.WfR0]
thRO.invA [in Buchberger.WfR0]
thRO.ltM [in Buchberger.WfR0]
thRO.ltM_dec [in Buchberger.WfR0]
thRO.minusA [in Buchberger.WfR0]
thRO.multA [in Buchberger.WfR0]
thRO.n [in Buchberger.WfR0]
thRO.os [in Buchberger.WfR0]
thRO.plusA [in Buchberger.WfR0]
Library Index
B
BarBuch
BuchAux
BuchRed
C
CoefStructureD
DicksonDivTerm
E
ExtractF
FredL
LetPLexiOrder
ListProps
M
MonomialsmoreCoefStructure
O
OpenIndGoodRelOrderStructure
P
PcombPcrit
Peq
Pminus
Pmult
Pmults
POrder
Pplus
Preduce
Preduceplus
Preducestar
Preducestar
Pspminus
Pspoly
T
TermW
WfR0Lemma Index
A
addEnd_incl [in Buchberger.Buch]addEnd_app [in Buchberger.BuchAux]
addEnd_id2 [in Buchberger.BuchAux]
addEnd_id1 [in Buchberger.BuchAux]
addEnd_cons [in Buchberger.BuchAux]
app2_inv [in Buchberger.POrder]
A_sep [in Buchberger.moreCoefStructure]
B
buch_Grobner [in Buchberger.Buch]buch_spolyQ [in Buchberger.Buch]
buch_reds [in Buchberger.Buch]
buch_Stable [in Buchberger.Buch]
C
canonicalpO [in Buchberger.Peq]canonicalp1 [in Buchberger.Peq]
canonical_reduce [in Buchberger.Preduce]
canonical_imp_in_nzero [in Buchberger.POrder]
canonical_pX_ltP [in Buchberger.POrder]
canonical_skip_fst [in Buchberger.POrder]
canonical_imp_canonical [in Buchberger.POrder]
canonical_pX_order [in Buchberger.POrder]
canonical_pX_eqT [in Buchberger.POrder]
canonical_cons [in Buchberger.POrder]
canonical_nzeroP [in Buchberger.POrder]
canonical_ltT [in Buchberger.POrder]
canonical_imp_olist [in Buchberger.POrder]
canonical_s2p [in Buchberger.BuchAux]
canonical_reduceplus [in Buchberger.Preduceplus]
canonical_mults_inv [in Buchberger.Pmults]
canonical_mults [in Buchberger.Pmults]
canonical_minuspf [in Buchberger.Pminus]
canonical_minusP [in Buchberger.Pminus]
canonical_Dmult [in Buchberger.Pcrit]
canonical_Rminus [in Buchberger.Pcrit]
canonical_spminusf_full_t [in Buchberger.Pspminus]
canonical_spminusf_full [in Buchberger.Pspminus]
canonical_spminusf [in Buchberger.Pspminus]
canonical_pluspf [in Buchberger.Pplus]
canonical_plusP [in Buchberger.Pplus]
canonical_multpf [in Buchberger.Pmult]
canonical0 [in Buchberger.POrder]
Cb_genPcPf [in Buchberger.Buch]
Cb_genPcP [in Buchberger.Buch]
Cb_stable [in Buchberger.Buch]
Cb_sp [in Buchberger.BuchAux]
Cb_in [in Buchberger.BuchAux]
Cb_in1 [in Buchberger.BuchAux]
Cb_incl [in Buchberger.BuchAux]
Cb_trans [in Buchberger.BuchAux]
Cb_id [in Buchberger.BuchAux]
cb_Red_cb2 [in Buchberger.BuchRed]
cb_Red_cb1 [in Buchberger.BuchRed]
Cb_Red [in Buchberger.BuchRed]
cb_redacc [in Buchberger.BuchRed]
Cb_compo [in Buchberger.BuchRed]
Cb_nf [in Buchberger.BuchRed]
Cb_comp [in Buchberger.BuchRed]
Cb_cons [in Buchberger.BuchRed]
Cb_trans_cons [in Buchberger.BuchRed]
Cb_cons_addEnd [in Buchberger.BuchRed]
Cb_addEnd_cons [in Buchberger.BuchRed]
cb_red_cb2 [in Buchberger.Fred]
cb_red_cb1 [in Buchberger.Fred]
cb_red [in Buchberger.Fred]
cb_redacc [in Buchberger.Fred]
CombLinear_trans1 [in Buchberger.BuchAux]
CombLinear_compo [in Buchberger.Pcomb]
CombLinear_trans_cons_lem [in Buchberger.Pcomb]
CombLinear_incl [in Buchberger.Pcomb]
CombLinear_reducestar [in Buchberger.Pcomb]
CombLinear_reduceplus [in Buchberger.Pcomb]
CombLinear_reduce [in Buchberger.Pcomb]
CombLinear_spoly [in Buchberger.Pcomb]
CombLinear_id [in Buchberger.Pcomb]
CombLinear_minuspf [in Buchberger.Pcomb]
CombLinear_mults1 [in Buchberger.Pcomb]
CombLinear_pluspf [in Buchberger.Pcomb]
CombLinear_comp [in Buchberger.Pcomb]
CombLinear_canonical [in Buchberger.Pcomb]
ConfluentReduce_imp_Grobner [in Buchberger.Pcomb]
confl_reducestar [in Buchberger.Pspoly]
confl_restar [in Buchberger.Pspoly]
confl_mix [in Buchberger.Pspoly]
confl_top [in Buchberger.Pspoly]
confl_top_simpl [in Buchberger.Pspoly]
confl_under [in Buchberger.Pspoly]
Conf_trans [in Buchberger.Pspoly]
Conf_inv1 [in Buchberger.Pspoly]
consGRBar [in Buchberger.Bar]
D
dec_lt [in Buchberger.Dickson]def_grobner [in Buchberger.BuchRed]
descA_subst [in Buchberger.POrder]
dicksonL [in Buchberger.Dickson]
divA_nZ [in Buchberger.BuchAux]
divA_nZ [in Buchberger.moreCoefStructure]
divA_A1 [in Buchberger.moreCoefStructure]
divA_A0_l [in Buchberger.moreCoefStructure]
divA_multA_comp_l [in Buchberger.moreCoefStructure]
divpf_comp [in Buchberger.Pcrit]
divpf_canonical [in Buchberger.Pcrit]
divPp_mults1 [in Buchberger.Pcrit]
divPp_divpf [in Buchberger.Pcrit]
divP_ppc [in Buchberger.BuchAux]
divp_nzeropr [in Buchberger.BuchAux]
divp_nzeropl [in Buchberger.BuchAux]
divp_ppc [in Buchberger.BuchAux]
divp_dec [in Buchberger.BuchAux]
divp_trans [in Buchberger.BuchAux]
divp_id [in Buchberger.BuchRed]
divp_reduce1 [in Buchberger.BuchRed]
divp_is_multTerm [in Buchberger.Pcrit]
divP_minusTerm_comp [in Buchberger.Pspminus]
divP_ltT_comp [in Buchberger.Pspminus]
divP_is_not_order [in Buchberger.Pspminus]
divP_eqT [in Buchberger.DivTerm]
divP_dec [in Buchberger.DivTerm]
divP_comp_ppc1 [in Buchberger.DivTerm]
divP_comp_ppc0 [in Buchberger.DivTerm]
divP_ppcr [in Buchberger.DivTerm]
divP_ppcl [in Buchberger.DivTerm]
divP_multTerm_r [in Buchberger.DivTerm]
divP_multTerm_l [in Buchberger.DivTerm]
divP_comp [in Buchberger.DivTerm]
divP_on_eqT_eqT [in Buchberger.DivTerm]
divP_on_eqT [in Buchberger.DivTerm]
divP_eqTerm_comp [in Buchberger.DivTerm]
divP_nZero [in Buchberger.DivTerm]
divP_trans [in Buchberger.DivTerm]
divP_invTerm_r [in Buchberger.DivTerm]
divP_invTerm_l [in Buchberger.DivTerm]
divP_plusTerm [in Buchberger.DivTerm]
divP_inv3 [in Buchberger.DivTerm]
divP_inv2 [in Buchberger.DivTerm]
divP_inv1 [in Buchberger.DivTerm]
divTerm_compo [in Buchberger.DivTerm]
divTerm_multTermr [in Buchberger.DivTerm]
divTerm_multTerml [in Buchberger.DivTerm]
divTerm_rew [in Buchberger.DivTerm]
divTerm_ppcr [in Buchberger.DivTerm]
divTerm_ppcl [in Buchberger.DivTerm]
divTerm_ppc [in Buchberger.DivTerm]
divTerm_on_plusM_minusM [in Buchberger.DivTerm]
divTerm_on_eqT_eqT [in Buchberger.DivTerm]
divTerm_on_eqT [in Buchberger.DivTerm]
divTerm_dec [in Buchberger.DivTerm]
divTerm_eqT [in Buchberger.DivTerm]
divTerm_nZ [in Buchberger.DivTerm]
divTerm_multTerm_r [in Buchberger.DivTerm]
divTerm_multTerm_l [in Buchberger.DivTerm]
divTerm_invTerm_r [in Buchberger.DivTerm]
divTerm_invTerm_l [in Buchberger.DivTerm]
div_clean_dec1 [in Buchberger.Monomials]
div_clean_dec2 [in Buchberger.Monomials]
div_is_T1 [in Buchberger.DivTerm]
Dmult_is_mulpf [in Buchberger.Pcrit]
E
eqA_A0 [in Buchberger.moreCoefStructure]eqA0_right [in Buchberger.moreCoefStructure]
eqA0_left [in Buchberger.moreCoefStructure]
eqmon_dec [in Buchberger.Monomials]
eqptail_spminusf_com [in Buchberger.Pspminus]
eqp_imp_canonical [in Buchberger.Peq]
eqp_eqTerm [in Buchberger.Peq]
eqp_trans [in Buchberger.Peq]
eqp_inv3r [in Buchberger.Peq]
eqp_inv3l [in Buchberger.Peq]
eqp_inv2 [in Buchberger.Peq]
eqp_inv1 [in Buchberger.Peq]
eqp_sym [in Buchberger.Peq]
eqp_refl [in Buchberger.Peq]
eqp_invT1_pO_is_pO [in Buchberger.Pmults]
eqp_spminusf_com [in Buchberger.Pspminus]
eqp_pluspf_com [in Buchberger.Pplus]
eqp_pluspf_com_r [in Buchberger.Pplus]
eqp_pluspf_com_l [in Buchberger.Pplus]
eqTerm_minusTerm_plusTerm_invTerm [in Buchberger.Term]
eqTerm_T1_eqT [in Buchberger.Term]
eqTerm_invTerm_comp [in Buchberger.Term]
eqTerm_multTerm_comp [in Buchberger.Term]
eqTerm_plusTerm_comp [in Buchberger.Term]
eqTerm_dec [in Buchberger.Term]
eqTerm_imp_eqT [in Buchberger.Term]
eqTerm_trans [in Buchberger.Term]
eqTerm_sym [in Buchberger.Term]
eqTerm_refl [in Buchberger.Term]
eqTerm_spolyf_red3 [in Buchberger.Pspoly]
eqTerm_spolyf_red2 [in Buchberger.Pspoly]
eqTerm_spminusf_com [in Buchberger.Pspminus]
eqTerm_multTerm_imp_eqTerm [in Buchberger.DivTerm]
eqTerm_divTerm_comp [in Buchberger.DivTerm]
eqT_not_ltT [in Buchberger.POrder]
eqT_dec [in Buchberger.POrder]
eqT_compat_ltTl [in Buchberger.POrder]
eqT_compat_ltTr [in Buchberger.POrder]
eqT_zerop_is_eqTerm [in Buchberger.Term]
eqT_trans [in Buchberger.Term]
eqT_sym [in Buchberger.Term]
eqT_refl [in Buchberger.Term]
eqT_nzero_eqT_divP [in Buchberger.DivTerm]
eqT_nzero_divP [in Buchberger.DivTerm]
eqT_divTerm [in Buchberger.DivTerm]
eqT_divTerm_plusTerm [in Buchberger.DivTerm]
F
fconfl_top [in Buchberger.Pspoly]fltP [in Buchberger.POrder]
foreigner_red [in Buchberger.BuchAux]
fp_tail [in Buchberger.POrder]
fP_app [in Buchberger.POrder]
fsltP [in Buchberger.POrder]
fspoly_Reduceplus_pO [in Buchberger.Pcrit]
G
genOCPf_stable [in Buchberger.Buch]genOCp_redln [in Buchberger.Buch]
genPcPf_incl [in Buchberger.Buch]
genPcP_incl [in Buchberger.Buch]
genPcP_spolyp1 [in Buchberger.Buch]
get_is_correct [in Buchberger.WfR0]
grobner_def [in Buchberger.BuchRed]
Grobner_imp_SpolyQ [in Buchberger.Pcomb]
I
imp_in [in Buchberger.Buch]Incl_inp_inPolySet [in Buchberger.Preduce]
incl_addEnd1 [in Buchberger.Buch]
inPolySet_inv1 [in Buchberger.Preduce]
inPolySet_inv0 [in Buchberger.Preduce]
inPolySet_is_pX [in Buchberger.Preduce]
inPolySet_imp_canonical [in Buchberger.Preduce]
inPolySet_addEnd [in Buchberger.BuchAux]
inP_reducestar [in Buchberger.BuchAux]
inP_reduceplus [in Buchberger.BuchAux]
inP_reduce [in Buchberger.BuchAux]
invA_is_invA1 [in Buchberger.moreCoefStructure]
invA0 [in Buchberger.moreCoefStructure]
invA0_inv [in Buchberger.moreCoefStructure]
invA0_comp [in Buchberger.moreCoefStructure]
invTerm_ltT_l [in Buchberger.POrder]
invTerm_T1_multTerm_T1 [in Buchberger.Pminus]
invTerm_T1_eqT_comp [in Buchberger.Pminus]
invTerm_eqT_comp [in Buchberger.Pminus]
invTerm_eqT [in Buchberger.Term]
invTerm_invol [in Buchberger.Term]
inv_prop [in Buchberger.Pminus]
in_inPolySet [in Buchberger.Preduce]
In_inp_inPolySet [in Buchberger.Preduce]
in_incl [in Buchberger.Buch]
in_minuspf_spoly_in [in Buchberger.Pcrit]
in_rev [in Buchberger.ListProps]
in_multpf_head [in Buchberger.Pmult]
irreducible_eqp_com [in Buchberger.Preduce]
irreducible_inv_px_l [in Buchberger.Preduce]
is_nil_id [in Buchberger.Monomials]
J
jjProp1 [in Buchberger.Dickson]jjProp2 [in Buchberger.Dickson]
K
keylem [in Buchberger.Dickson]keylem_cor [in Buchberger.Dickson]
L
lem_redln_cons_gen [in Buchberger.Buch]lem_redln_cons [in Buchberger.Buch]
lem_redIn_nil [in Buchberger.Buch]
lem0 [in Buchberger.Dickson]
lem1 [in Buchberger.Dickson]
lem1aux [in Buchberger.Dickson]
leq2le [in Buchberger.Dickson]
ltP_reduce [in Buchberger.Preduce]
ltp_eqp_comp [in Buchberger.Peq]
ltP_refl_pX [in Buchberger.Peq]
ltP_pX_canonical [in Buchberger.POrder]
ltP_order_comp [in Buchberger.POrder]
ltP_pX_olist [in Buchberger.POrder]
ltP_trans [in Buchberger.POrder]
ltp_not_refl [in Buchberger.POrder]
ltP_divP_pX [in Buchberger.Pspminus]
ltT_eqTl [in Buchberger.POrder]
ltT_eqTr [in Buchberger.POrder]
ltT_eqT [in Buchberger.POrder]
ltT_not_ltT [in Buchberger.POrder]
ltT_not_refl [in Buchberger.POrder]
ltT_not_eqT [in Buchberger.POrder]
ltT_dec [in Buchberger.POrder]
ltT_trans [in Buchberger.POrder]
l1 [in Buchberger.WfR0]
M
map_rev [in Buchberger.ListProps]map_app [in Buchberger.ListProps]
map_in [in Buchberger.ListProps]
mdiv_div [in Buchberger.Monomials]
mdiv_trans [in Buchberger.Monomials]
mdiv_proj [in Buchberger.Monomials]
minuspf_eq_inv2 [in Buchberger.Pminus]
minuspf_pOmults_eq [in Buchberger.Pminus]
minuspf_eq_inv1 [in Buchberger.Pminus]
minuspf_pO_refl_eq [in Buchberger.Pminus]
minuspf_zero [in Buchberger.Pminus]
minuspf_refl [in Buchberger.Pminus]
minuspf_refl_eq [in Buchberger.Pminus]
minuspf_pOmults [in Buchberger.Pminus]
minuspf_pO_refl [in Buchberger.Pminus]
minuspf_comp [in Buchberger.Pminus]
minuspf_inv3b [in Buchberger.Pminus]
minuspf_inv3a [in Buchberger.Pminus]
minuspf_inv2 [in Buchberger.Pminus]
minuspf_inv1 [in Buchberger.Pminus]
minuspf_inv3b_eq [in Buchberger.Pminus]
minuspf_inv3a_eq [in Buchberger.Pminus]
minuspf_inv2_eq [in Buchberger.Pminus]
minuspf_inv1_eq [in Buchberger.Pminus]
minuspf_is_pluspf_mults [in Buchberger.Pminus]
minuspf_pO_is_eqP [in Buchberger.Pminus]
minuspf_is_minusP [in Buchberger.Pminus]
minuspf_spoly_in [in Buchberger.Pcrit]
minuspf_in [in Buchberger.Pcrit]
minusP_pO_refl_eq [in Buchberger.Pminus]
minusP_refl [in Buchberger.Pminus]
minusP_inv3b [in Buchberger.Pminus]
minusP_inv3a [in Buchberger.Pminus]
minusP_inv2 [in Buchberger.Pminus]
minusP_inv1 [in Buchberger.Pminus]
minusP_is_plusP_mults [in Buchberger.Pminus]
minusP_inv [in Buchberger.Pminus]
minusP_pO_is_eqP [in Buchberger.Pminus]
minusTerm_ltT_l [in Buchberger.POrder]
minusTerm_zeroP [in Buchberger.Pminus]
minusTerm_zeroP_r [in Buchberger.Pminus]
minusTerm_eqT [in Buchberger.Term]
minus_lt_0 [in Buchberger.Monomials]
minus_is_reduce [in Buchberger.Pcrit]
monExistsL [in Buchberger.Bar]
monExistsL1 [in Buchberger.Bar]
monGoodR [in Buchberger.Bar]
monGoodR1 [in Buchberger.Bar]
monGRBar [in Buchberger.Bar]
monGRBarAux [in Buchberger.Bar]
monLift_lem [in Buchberger.Dickson]
monO_n0 [in Buchberger.Dickson]
mon_0 [in Buchberger.Monomials]
multA_invA_com_r [in Buchberger.moreCoefStructure]
multA_invA_com_l [in Buchberger.moreCoefStructure]
multA_A1_r [in Buchberger.moreCoefStructure]
multA_A0_r [in Buchberger.moreCoefStructure]
multA_dist_r [in Buchberger.moreCoefStructure]
multA_eqA_comp_r [in Buchberger.moreCoefStructure]
multA_eqA_comp_l [in Buchberger.moreCoefStructure]
multlm_comp_canonical [in Buchberger.Pmults]
multpf_assoc [in Buchberger.Pmult]
multpf_smultm_assoc [in Buchberger.Pmult]
multpf_dist_plusl [in Buchberger.Pmult]
multpf_dist_plusr [in Buchberger.Pmult]
multpf_com [in Buchberger.Pmult]
multpf_comp [in Buchberger.Pmult]
multpf_head [in Buchberger.Pmult]
multpf_disr_pX [in Buchberger.Pmult]
mults_eqp_inv [in Buchberger.Preduce]
mults_dist_pluspf [in Buchberger.Pmults]
mults_ltP_comp [in Buchberger.Pmults]
mults_comp [in Buchberger.Pmults]
mults_com [in Buchberger.Pmults]
mults_multTerm [in Buchberger.Pmults]
mults_invTerm [in Buchberger.Pmults]
mults_T1 [in Buchberger.Pmults]
mults_dist2 [in Buchberger.Pmults]
mults_dist1 [in Buchberger.Pmults]
mults_eqp_zpO [in Buchberger.Pmults]
mults_eqp_pO_pO [in Buchberger.Pmults]
mults_order_l [in Buchberger.Pmults]
mults_comp_minuspf [in Buchberger.Pminus]
mults_minusTerm [in Buchberger.Pminus]
mults_pO [in Buchberger.Pminus]
mults_dist_minuspf [in Buchberger.Pminus]
multTerm_ltT_r [in Buchberger.POrder]
multTerm_ltT_l [in Buchberger.POrder]
multTerm_invTerm_T1_eqT_comp [in Buchberger.Pminus]
multTerm_minusTerm_dist_l [in Buchberger.Term]
multTerm_zeroP_div [in Buchberger.Term]
multTerm_com [in Buchberger.Term]
multTerm_assoc [in Buchberger.Term]
multTerm_eqT [in Buchberger.Term]
multTerm_plusTerm_dist_r [in Buchberger.Term]
multTerm_plusTerm_dist_l [in Buchberger.Term]
multTerm_or_z_d2 [in Buchberger.Pcrit]
multTerm_or_z_d1 [in Buchberger.Pcrit]
multTerm_eqTerm_inv [in Buchberger.DivTerm]
mult_div_id [in Buchberger.Monomials]
mult_div_com [in Buchberger.Monomials]
mult_mon_zero_l [in Buchberger.Monomials]
mult_mon_zero_r [in Buchberger.Monomials]
mult_mon_assoc [in Buchberger.Monomials]
mult_mon_com [in Buchberger.Monomials]
mult_invTerm_com_r [in Buchberger.Term]
mult_invTerm_com [in Buchberger.Term]
N
nat_double_ind_set [in Buchberger.Dickson]nf_Cb [in Buchberger.BuchAux]
nf_red [in Buchberger.BuchAux]
nf_irreducible [in Buchberger.BuchAux]
nf_divp_zero [in Buchberger.BuchRed]
nf_divp [in Buchberger.BuchRed]
nilGRBar [in Buchberger.Bar]
not_nil_in_polySet [in Buchberger.Preduce]
not_nil_in_polySet_elm [in Buchberger.Preduce]
not_double_canonical [in Buchberger.POrder]
nzeroP_multTerm [in Buchberger.Term]
nzeroP_comp_eqTerm [in Buchberger.Term]
nZero_invTerm_T1 [in Buchberger.Term]
nZero_invTerm_nZero [in Buchberger.Term]
O
ObuchPincl [in Buchberger.Buch]ObuchPred [in Buchberger.Buch]
ObuchQred [in Buchberger.Buch]
OBuch_Inv_f [in Buchberger.Buch]
OBuch_Stable_f [in Buchberger.Buch]
OBuch_Inv [in Buchberger.Buch]
OBuch_Stable [in Buchberger.Buch]
olistO [in Buchberger.POrder]
olistOne [in Buchberger.POrder]
olist_pX_ltP [in Buchberger.POrder]
olist_imp_olist [in Buchberger.POrder]
olist_X [in Buchberger.POrder]
olist_pX_order [in Buchberger.POrder]
olist_pX_eqT [in Buchberger.POrder]
olist_cons [in Buchberger.POrder]
olist_ltT [in Buchberger.POrder]
one_minus_reduceplus [in Buchberger.Preduceplus]
one_plus_reduceplus [in Buchberger.Preduceplus]
OpenInd [in Buchberger.OpenIndGoodRel]
Opm_ind [in Buchberger.Pminus]
orderc_dec [in Buchberger.LexiOrder]
order_reduceplus [in Buchberger.Preduceplus]
order_minuspf [in Buchberger.Pminus]
order_pluspf [in Buchberger.Pminus]
order_minusP [in Buchberger.Pminus]
order_pluspf [in Buchberger.Pplus]
order_plusP [in Buchberger.Pplus]
P
pbuchf_Inv [in Buchberger.Buch]pbuchf_Stable [in Buchberger.Buch]
pickin_is_pX [in Buchberger.Preduce]
pick_inv_eqT [in Buchberger.Preduce]
pick_inv_eqT_lem [in Buchberger.Preduce]
pick_inv_in [in Buchberger.Preduce]
plusA_eqA_comp_r [in Buchberger.moreCoefStructure]
plusA_eqA_comp_l [in Buchberger.moreCoefStructure]
pluspf_is_minuspf [in Buchberger.Pminus]
pluspf_minuspf_id [in Buchberger.Pminus]
pluspf_assoc [in Buchberger.Pplus]
pluspf_inv2_eqa [in Buchberger.Pplus]
pluspf_inv1_eqa [in Buchberger.Pplus]
pluspf_inv3b_eq [in Buchberger.Pplus]
pluspf_inv3a_eq [in Buchberger.Pplus]
pluspf_inv2_eq [in Buchberger.Pplus]
pluspf_inv1_eq [in Buchberger.Pplus]
pluspf_com [in Buchberger.Pplus]
pluspf_inv3b [in Buchberger.Pplus]
pluspf_inv3a [in Buchberger.Pplus]
pluspf_inv2 [in Buchberger.Pplus]
pluspf_inv1 [in Buchberger.Pplus]
pluspf_is_plusP [in Buchberger.Pplus]
pluspf_pX [in Buchberger.Pmult]
pluspf3_assoc [in Buchberger.Pplus]
plusP_uniq_eqP [in Buchberger.Pplus]
plusP_zero_pOr [in Buchberger.Pplus]
plusP_zero_pOl [in Buchberger.Pplus]
plusP_com [in Buchberger.Pplus]
plusP_inv3b [in Buchberger.Pplus]
plusP_inv3a [in Buchberger.Pplus]
plusP_inv2 [in Buchberger.Pplus]
plusP_inv1 [in Buchberger.Pplus]
plusP_decomp [in Buchberger.Pplus]
plusP_inv [in Buchberger.Pplus]
plusTerm_invTerm_zeroP [in Buchberger.Term]
plusTerm_assoc [in Buchberger.Term]
plusTerm_eqT2 [in Buchberger.Term]
plusTerm_eqT1 [in Buchberger.Term]
plusTerm_com [in Buchberger.Term]
plusTerm_comp_r [in Buchberger.Term]
plusTerm_comp_l [in Buchberger.Term]
plusTerm_is_pX [in Buchberger.Pplus]
plus_minus_le [in Buchberger.Monomials]
pO_irreducible [in Buchberger.Preduce]
pO_reduce [in Buchberger.Preduce]
pO_reduceplus [in Buchberger.Preduceplus]
pO_reducestar [in Buchberger.Preducestar]
pO_reducestar [in Buchberger.Preducestar]
pO_minusP_inv2 [in Buchberger.Pminus]
pO_minusP_inv1 [in Buchberger.Pminus]
pO_pluspf_inv2 [in Buchberger.Pplus]
pO_pluspf_inv1 [in Buchberger.Pplus]
pO_plusP_inv2 [in Buchberger.Pplus]
pO_plusP_inv1 [in Buchberger.Pplus]
ppcm_mom_is_ppcm [in Buchberger.Monomials]
ppcm_prop_r [in Buchberger.Monomials]
ppcm_prop_l [in Buchberger.Monomials]
ppcm_com [in Buchberger.Monomials]
ppc_multTerm_divP [in Buchberger.DivTerm]
ppc_is_ppcm [in Buchberger.DivTerm]
ppc_nZ [in Buchberger.DivTerm]
ppc_com [in Buchberger.DivTerm]
proj_ok [in Buchberger.Monomials]
pX_invr [in Buchberger.Peq]
pX_invl [in Buchberger.Peq]
pX_inj [in Buchberger.Peq]
p0_pluspf_r [in Buchberger.Pplus]
p0_pluspf_l [in Buchberger.Pplus]
R
recomp_ok [in Buchberger.Monomials]redacc_divp [in Buchberger.BuchRed]
redacc_cb [in Buchberger.BuchRed]
redacc_divp [in Buchberger.Fred]
redacc_cb [in Buchberger.Fred]
redbuch_Grobner [in Buchberger.BuchRed]
redbuch_stable [in Buchberger.BuchRed]
redInclP [in Buchberger.Buch]
redInclR [in Buchberger.Buch]
redInInclQ [in Buchberger.Buch]
redIn_nil [in Buchberger.Buch]
redln_cons_gen [in Buchberger.Buch]
redln_cons [in Buchberger.Buch]
reds_SpolyQ1 [in Buchberger.Buch]
reds_SpolyQ [in Buchberger.Buch]
reds_com [in Buchberger.Buch]
reducehead_imp_reduce [in Buchberger.Preduce]
reduceplus_mults_inv [in Buchberger.Preduceplus]
reduceplus_mults_invf0 [in Buchberger.Preduceplus]
reduceplus_mults_invr [in Buchberger.Preduceplus]
reduceplus_mults_invr_lem [in Buchberger.Preduceplus]
reduceplus_mults [in Buchberger.Preduceplus]
reduceplus_skip [in Buchberger.Preduceplus]
reduceplus_trans [in Buchberger.Preduceplus]
reduceplus_eqp_com [in Buchberger.Preduceplus]
reduceplus_divp [in Buchberger.BuchRed]
reduceplus_divp_lem [in Buchberger.BuchRed]
reduceplus_cb2 [in Buchberger.Pcomb]
reduceplus_cb2_lem [in Buchberger.Pcomb]
reduceplus_cb1 [in Buchberger.Pcomb]
reduceplus_cb1_lem [in Buchberger.Pcomb]
reduceplus_cb [in Buchberger.Pcomb]
reducestar_in_pO [in Buchberger.Preducestar]
reducestar_pO_is_pO [in Buchberger.Preducestar]
reducestar_inv [in Buchberger.Preducestar]
reducestar_irreducible [in Buchberger.Preducestar]
reducestar_reduceplus [in Buchberger.Preducestar]
reducestar_trans [in Buchberger.Preducestar]
reducestar_eqp_com [in Buchberger.Preducestar]
reducestar_in_pO [in Buchberger.Preducestar]
reducestar_pO_is_pO [in Buchberger.Preducestar]
reducestar_inv [in Buchberger.Preducestar]
reducestar_irreducible [in Buchberger.Preducestar]
reducestar_reduceplus [in Buchberger.Preducestar]
reducestar_trans [in Buchberger.Preducestar]
reducestar_eqp_com [in Buchberger.Preducestar]
reducestar_divp [in Buchberger.BuchRed]
reducestar_cb2 [in Buchberger.Pcomb]
reducestar_cb1 [in Buchberger.Pcomb]
reducestar_cb [in Buchberger.Pcomb]
Reducestar_pO_imp_CombLinear [in Buchberger.Pcomb]
reducetopO_pO [in Buchberger.BuchAux]
reducetop_sp [in Buchberger.Preduce]
reduce_mults_invr [in Buchberger.Preduce]
reduce_mults_inv_lem [in Buchberger.Preduce]
reduce_mults [in Buchberger.Preduce]
reduce_mults_invf [in Buchberger.Preduce]
reduce_inv2 [in Buchberger.Preduce]
reduce_inv [in Buchberger.Preduce]
reduce_eqp_com [in Buchberger.Preduce]
reduce_in_pO [in Buchberger.Preduce]
reduce_plus_top [in Buchberger.Preduceplus]
reduce_imp_reduceplus [in Buchberger.Preduceplus]
reduce_divp [in Buchberger.BuchRed]
reduce_cb2 [in Buchberger.Pcomb]
reduce_cb1 [in Buchberger.Pcomb]
reduce_cb [in Buchberger.Pcomb]
reduce0_reducestar [in Buchberger.Preducestar]
reduce0_reducestar [in Buchberger.Preducestar]
red_gen_in [in Buchberger.Buch]
red_zerop [in Buchberger.BuchAux]
red_incl [in Buchberger.BuchAux]
red_id [in Buchberger.BuchAux]
red_cons [in Buchberger.BuchAux]
red_com [in Buchberger.BuchAux]
red_minus_zero_reduce [in Buchberger.Preduceplus]
red_plus_zero_reduce [in Buchberger.Preduceplus]
Red_grobner [in Buchberger.BuchRed]
Red_divp [in Buchberger.BuchRed]
Red_cb [in Buchberger.BuchRed]
red_grobner [in Buchberger.Fred]
red_divp [in Buchberger.Fred]
red_cb [in Buchberger.Fred]
rep_plus_zero_reduce [in Buchberger.Preduceplus]
rep_minus_reduce [in Buchberger.Preduceplus]
rep_plus_reduce [in Buchberger.Preduceplus]
rev_in [in Buchberger.ListProps]
rew_spminusf [in Buchberger.Pspminus]
Rminus_is_mult [in Buchberger.Pcrit]
Rminus_is_reduceplus [in Buchberger.Pcrit]
Rminus_in [in Buchberger.Pcrit]
RO_lem [in Buchberger.WfR0]
rstar_rtopO [in Buchberger.BuchAux]
S
seqp_trans [in Buchberger.Peq]seqp_sym [in Buchberger.Peq]
seqp_refl [in Buchberger.Peq]
seqp_dec [in Buchberger.Peq]
slicef_incl [in Buchberger.Buch]
slice_Tl [in Buchberger.Buch]
slice_cons [in Buchberger.Buch]
slice_inv [in Buchberger.Buch]
sltp_wf [in Buchberger.POrder]
spminusf_plusTerm_z [in Buchberger.Pspminus]
spminusf_minusTerm_z [in Buchberger.Pspminus]
spminusf_minusTerm [in Buchberger.Pspminus]
spminusf_plusTerm_r [in Buchberger.Pspminus]
spminusf_minusTerm_r [in Buchberger.Pspminus]
spminusf_plusTerm_l [in Buchberger.Pspminus]
spminusf_minusTerm_l [in Buchberger.Pspminus]
spminusf_multTerm [in Buchberger.Pspminus]
spminusf_plusTerm [in Buchberger.Pspminus]
spminusf_minuspf [in Buchberger.Pspminus]
spminusf_pluspf [in Buchberger.Pspminus]
spminusf_extend [in Buchberger.Pspminus]
spolyf_def [in Buchberger.Pspoly]
spolyf_com [in Buchberger.Pspoly]
spolyf_pO [in Buchberger.Pspoly]
spolyf_canonical [in Buchberger.Pspoly]
spolyp_addEnd_genPcPf [in Buchberger.Buch]
spolyp_cons_genPcP [in Buchberger.Buch]
spolyp_cons_genPcP0 [in Buchberger.Buch]
SpolyQ_imp_ConfluentReduce [in Buchberger.Pcomb]
spoly_div_is_minus [in Buchberger.Pspoly]
spoly_is_minus [in Buchberger.Pspoly]
spoly_Reducestar_ppc [in Buchberger.Pcrit]
spoly_Reducestar_pO [in Buchberger.Pcrit]
spoly_reduceplus_pO [in Buchberger.Pcrit]
spoly_Reduce [in Buchberger.Pcrit]
sp_Rminus [in Buchberger.Pcrit]
sp_rew [in Buchberger.Pspminus]
stable_sym [in Buchberger.Buch]
stable_trans [in Buchberger.Buch]
stable_refl [in Buchberger.Buch]
subPredExistsL [in Buchberger.Bar]
subRelGoodR [in Buchberger.Bar]
subRelGRBar [in Buchberger.Bar]
T
tdivExists_trmHd_lem [in Buchberger.Bar]tdivGoodP [in Buchberger.Bar]
tmults_zerop_eqp_pO [in Buchberger.Pmults]
total_orderc_dec [in Buchberger.LexiOrder]
T1_is_min_ltT [in Buchberger.POrder]
T1_eqT [in Buchberger.Term]
T1_multTerm_r [in Buchberger.Term]
T1_multTerm_l [in Buchberger.Term]
T1_nz [in Buchberger.Term]
U
uniq_minusp [in Buchberger.Pminus]uniq_plusp [in Buchberger.Pplus]
unit_nZ [in Buchberger.BuchAux]
unit_T1 [in Buchberger.BuchAux]
W
WFlem1 [in Buchberger.Dickson]wf_lessP3 [in Buchberger.Peq]
wf_lessP [in Buchberger.Peq]
wf_incl [in Buchberger.WfR0]
wf_RL [in Buchberger.Buch]
wf_Co [in Buchberger.Buch]
wf_Fl [in Buchberger.Buch]
wf_Tl [in Buchberger.Buch]
Z
zerop_red [in Buchberger.BuchAux]zerop_red_spoly_r [in Buchberger.BuchAux]
zerop_red_spoly_l [in Buchberger.BuchAux]
zerop_ddivp_ppc [in Buchberger.BuchAux]
zerop_dec [in Buchberger.BuchAux]
zerop_nf_cb [in Buchberger.BuchRed]
zerop_elim_cb [in Buchberger.BuchRed]
zerop_elim_Cb [in Buchberger.BuchRed]
zerop_is_eqTerm [in Buchberger.Pminus]
zeroP_minusTerm [in Buchberger.Term]
zeroP_invTerm_zeroP [in Buchberger.Term]
zeroP_multTerm_r [in Buchberger.Term]
zeroP_multTerm_l [in Buchberger.Term]
zeroP_plusTerml [in Buchberger.Term]
zeroP_plusTermr [in Buchberger.Term]
zeroP_comp_eqTerm [in Buchberger.Term]
zeroP_dec [in Buchberger.Term]
zerop_nf_cb [in Buchberger.Fred]
zeroP_divTerm [in Buchberger.DivTerm]
zRV_WR [in Buchberger.Dickson]
Constructor Index
B
Base [in Buchberger.Bar]C
cmin [in Buchberger.OpenIndGoodRel]CombLinear_1 [in Buchberger.Pcomb]
CombLinear_0 [in Buchberger.Pcomb]
ConfluentReduce0 [in Buchberger.Pcomb]
Confluent0 [in Buchberger.Pspoly]
c_n [in Buchberger.Monomials]
D
divTerm_def [in Buchberger.DivTerm]DontKeep [in Buchberger.Buch]
E
eqpP1 [in Buchberger.Peq]eqP0 [in Buchberger.Peq]
F
FoundE [in Buchberger.Bar]FoundG [in Buchberger.Bar]
G
genPcP0 [in Buchberger.Buch]genPcP1 [in Buchberger.Buch]
genPcP2 [in Buchberger.Buch]
Grobner0 [in Buchberger.Pcomb]
I
incons [in Buchberger.Preduce]Ind [in Buchberger.Bar]
inskip [in Buchberger.Preduce]
K
Keep [in Buchberger.Buch]L
lo1 [in Buchberger.LexiOrder]lo2 [in Buchberger.LexiOrder]
ltPO [in Buchberger.POrder]
ltP_tl [in Buchberger.POrder]
ltP_hd [in Buchberger.POrder]
M
mainu1 [in Buchberger.Pplus]mainu2a [in Buchberger.Pplus]
mainu2b [in Buchberger.Pplus]
mainu3 [in Buchberger.Pplus]
mdiv_cons [in Buchberger.Monomials]
mdiv_nil [in Buchberger.Monomials]
mkCoefStructure [in Buchberger.CoefStructure]
mkOrderStructure [in Buchberger.OrderStructure]
mmainu1 [in Buchberger.Pminus]
mmainu2a [in Buchberger.Pminus]
mmainu2b [in Buchberger.Pminus]
mmainu3 [in Buchberger.Pminus]
mnillu1 [in Buchberger.Pminus]
mnillu2 [in Buchberger.Pminus]
N
nillu1 [in Buchberger.Pplus]nillu2 [in Buchberger.Pplus]
nmin [in Buchberger.OpenIndGoodRel]
n_0 [in Buchberger.Monomials]
O
OBuch0 [in Buchberger.Buch]OBuch1 [in Buchberger.Buch]
OBuch2 [in Buchberger.Buch]
P
pickinSeteqp [in Buchberger.Preduce]pickinSetskip [in Buchberger.Preduce]
ppcm0 [in Buchberger.DivTerm]
R
redIn0 [in Buchberger.Buch]redIn0b [in Buchberger.Buch]
redIn1 [in Buchberger.Buch]
redIn2 [in Buchberger.Buch]
reds0 [in Buchberger.Buch]
reds1 [in Buchberger.Buch]
reduceheadO [in Buchberger.Preduce]
Reducep0 [in Buchberger.Pspoly]
reduceskip [in Buchberger.Preduce]
reducestar0 [in Buchberger.Preducestar]
reducestar0 [in Buchberger.Preducestar]
reducetop [in Buchberger.Preduce]
ReduStarConfluent0 [in Buchberger.Pspoly]
RO0 [in Buchberger.WfR0]
Rstar_n [in Buchberger.Preduceplus]
Rstar_0 [in Buchberger.Preduceplus]
S
SearchE [in Buchberger.Bar]SearchG [in Buchberger.Bar]
SpolyQ0 [in Buchberger.Pspoly]
Spoly_11 [in Buchberger.Pspoly]
Spoly_10 [in Buchberger.Pspoly]
stable0 [in Buchberger.Buch]
T
total_orderc1 [in Buchberger.LexiOrder]total_orderc0 [in Buchberger.LexiOrder]
Inductive Index
B
Bar [in Buchberger.Bar]C
CombLinear [in Buchberger.Pcomb]Confluent [in Buchberger.Pspoly]
ConfluentReduce [in Buchberger.Pcomb]
cpRes [in Buchberger.Buch]
D
divP [in Buchberger.DivTerm]E
eqP [in Buchberger.Peq]ExistsL [in Buchberger.Bar]
G
genPcP [in Buchberger.Buch]GoodR [in Buchberger.Bar]
Grobner [in Buchberger.Pcomb]
I
inPolySet [in Buchberger.Preduce]L
ltP [in Buchberger.POrder]M
mdiv [in Buchberger.Monomials]Min [in Buchberger.OpenIndGoodRel]
minusP [in Buchberger.Pminus]
mon [in Buchberger.Monomials]
O
OBuch [in Buchberger.Buch]orderc [in Buchberger.LexiOrder]
P
pickinSetp [in Buchberger.Preduce]plusP [in Buchberger.Pplus]
ppcm [in Buchberger.DivTerm]
R
redIn [in Buchberger.Buch]reds [in Buchberger.Buch]
reduce [in Buchberger.Preduce]
reducehead [in Buchberger.Preduce]
Reducep [in Buchberger.Pspoly]
reduceplus [in Buchberger.Preduceplus]
reducestar [in Buchberger.Preducestar]
reducestar [in Buchberger.Preducestar]
ReduStarConfluent [in Buchberger.Pspoly]
RO [in Buchberger.WfR0]
S
SpolyQ [in Buchberger.Pspoly]Spoly_1 [in Buchberger.Pspoly]
stable [in Buchberger.Buch]
T
total_orderc [in Buchberger.LexiOrder]Projection Index
A
A1_diff_A0 [in Buchberger.CoefStructure]D
divA_invA_r [in Buchberger.CoefStructure]divA_multA_comp_r [in Buchberger.CoefStructure]
divA_eqA_comp [in Buchberger.CoefStructure]
divA_is_multA [in Buchberger.CoefStructure]
divA_rew [in Buchberger.CoefStructure]
E
eqA_trans [in Buchberger.CoefStructure]eqA_sym [in Buchberger.CoefStructure]
eqA_ref [in Buchberger.CoefStructure]
I
invA_eqA_comp [in Buchberger.CoefStructure]invA_plusA [in Buchberger.CoefStructure]
L
ltM_plusl [in Buchberger.OrderStructure]ltM_plusr [in Buchberger.OrderStructure]
ltM_wf [in Buchberger.OrderStructure]
ltM_trans [in Buchberger.OrderStructure]
ltM_nonrefl [in Buchberger.OrderStructure]
M
minusA_def [in Buchberger.CoefStructure]multA_A1_l [in Buchberger.CoefStructure]
multA_A0_l [in Buchberger.CoefStructure]
multA_dist_l [in Buchberger.CoefStructure]
multA_com [in Buchberger.CoefStructure]
multA_assoc [in Buchberger.CoefStructure]
multA_eqA_comp [in Buchberger.CoefStructure]
M1_min [in Buchberger.OrderStructure]
P
plusA_A0 [in Buchberger.CoefStructure]plusA_eqA_comp [in Buchberger.CoefStructure]
plusA_com [in Buchberger.CoefStructure]
plusA_assoc [in Buchberger.CoefStructure]
Section Index
B
Buch [in Buchberger.Buch]BuchAux [in Buchberger.BuchAux]
BuchRed [in Buchberger.BuchRed]
C
crit [in Buchberger.Pcrit]D
Dickson [in Buchberger.Dickson]DivTerm [in Buchberger.DivTerm]
L
lems [in Buchberger.Bar]lexi_order [in Buchberger.LexiOrder]
M
mCoef [in Buchberger.moreCoefStructure]Monomials [in Buchberger.Monomials]
O
OpenIndGoodRel [in Buchberger.OpenIndGoodRel]P
Pcomb [in Buchberger.Pcomb]Peq [in Buchberger.Peq]
Pminus [in Buchberger.Pminus]
Pmult [in Buchberger.Pmult]
Pmults [in Buchberger.Pmults]
Porder [in Buchberger.POrder]
Pplus [in Buchberger.Pplus]
Preduce [in Buchberger.Preduce]
Preduceplus [in Buchberger.Preduceplus]
Preducestar [in Buchberger.Preducestar]
Preducestar [in Buchberger.Preducestar]
Pspminus [in Buchberger.Pspminus]
Pspoly [in Buchberger.Pspoly]
R
Reduce [in Buchberger.Fred]T
Term [in Buchberger.Term]thRO [in Buchberger.WfR0]
Abbreviation Index
A
addEnd1 [in Buchberger.WfR0]addEnd1 [in Buchberger.Buch]
addEnd1 [in Buchberger.BuchRed]
B
buch1 [in Buchberger.BuchRed]C
canonical1 [in Buchberger.Preduce]canonical1 [in Buchberger.Peq]
canonical1 [in Buchberger.WfR0]
canonical1 [in Buchberger.Buch]
canonical1 [in Buchberger.BuchAux]
canonical1 [in Buchberger.Preduceplus]
canonical1 [in Buchberger.Pmults]
canonical1 [in Buchberger.Preducestar]
canonical1 [in Buchberger.Preducestar]
canonical1 [in Buchberger.BuchRed]
canonical1 [in Buchberger.Pminus]
canonical1 [in Buchberger.Pspoly]
canonical1 [in Buchberger.Pcrit]
canonical1 [in Buchberger.Pcomb]
canonical1 [in Buchberger.Pspminus]
canonical1 [in Buchberger.Pplus]
canonical1 [in Buchberger.Pmult]
Cb1 [in Buchberger.WfR0]
Cb1 [in Buchberger.Buch]
Cb1 [in Buchberger.BuchRed]
CombLinear1 [in Buchberger.WfR0]
CombLinear1 [in Buchberger.Buch]
CombLinear1 [in Buchberger.BuchAux]
CombLinear1 [in Buchberger.BuchRed]
D
divp_trans1 [in Buchberger.WfR0]divp_dec1 [in Buchberger.WfR0]
divp_trans1 [in Buchberger.Buch]
divp_dec1 [in Buchberger.Buch]
divp_trans1 [in Buchberger.BuchRed]
divp_dec1 [in Buchberger.BuchRed]
divP1 [in Buchberger.Preduce]
divp1 [in Buchberger.WfR0]
divP1 [in Buchberger.WfR0]
divp1 [in Buchberger.Buch]
divP1 [in Buchberger.Buch]
divP1 [in Buchberger.BuchAux]
divP1 [in Buchberger.Preduceplus]
divP1 [in Buchberger.Preducestar]
divP1 [in Buchberger.Preducestar]
divp1 [in Buchberger.BuchRed]
divP1 [in Buchberger.BuchRed]
divP1 [in Buchberger.Pspoly]
divP1 [in Buchberger.Pcrit]
divP1 [in Buchberger.Pcomb]
divP1 [in Buchberger.Pspminus]
divTerm1 [in Buchberger.Preduce]
divTerm1 [in Buchberger.WfR0]
divTerm1 [in Buchberger.Buch]
divTerm1 [in Buchberger.BuchAux]
divTerm1 [in Buchberger.Preduceplus]
divTerm1 [in Buchberger.Preducestar]
divTerm1 [in Buchberger.Preducestar]
divTerm1 [in Buchberger.BuchRed]
divTerm1 [in Buchberger.Pspoly]
divTerm1 [in Buchberger.Pcrit]
divTerm1 [in Buchberger.Pcomb]
divTerm1 [in Buchberger.Pspminus]
E
eqp_sym1 [in Buchberger.Preduce]eqp_trans1 [in Buchberger.Preduce]
eqp_sym1 [in Buchberger.WfR0]
eqp_trans1 [in Buchberger.WfR0]
eqp_sym1 [in Buchberger.Buch]
eqp_trans1 [in Buchberger.Buch]
eqp_sym1 [in Buchberger.BuchAux]
eqp_trans1 [in Buchberger.BuchAux]
eqp_sym1 [in Buchberger.Preduceplus]
eqp_trans1 [in Buchberger.Preduceplus]
eqp_sym1 [in Buchberger.Pmults]
eqp_trans1 [in Buchberger.Pmults]
eqp_sym1 [in Buchberger.Preducestar]
eqp_trans1 [in Buchberger.Preducestar]
eqp_sym1 [in Buchberger.Preducestar]
eqp_trans1 [in Buchberger.Preducestar]
eqp_sym1 [in Buchberger.BuchRed]
eqp_trans1 [in Buchberger.BuchRed]
eqp_sym1 [in Buchberger.Pminus]
eqp_trans1 [in Buchberger.Pminus]
eqp_sym1 [in Buchberger.Pspoly]
eqp_trans1 [in Buchberger.Pspoly]
eqp_sym1 [in Buchberger.Pcrit]
eqp_trans1 [in Buchberger.Pcrit]
eqp_sym1 [in Buchberger.Pcomb]
eqp_trans1 [in Buchberger.Pcomb]
eqp_sym1 [in Buchberger.Pspminus]
eqp_trans1 [in Buchberger.Pspminus]
eqp_sym1 [in Buchberger.Pplus]
eqp_trans1 [in Buchberger.Pplus]
eqp_sym1 [in Buchberger.Pmult]
eqp_trans1 [in Buchberger.Pmult]
eqP1 [in Buchberger.Preduce]
eqP1 [in Buchberger.WfR0]
eqP1 [in Buchberger.Buch]
eqP1 [in Buchberger.BuchAux]
eqP1 [in Buchberger.Preduceplus]
eqP1 [in Buchberger.Pmults]
eqP1 [in Buchberger.Preducestar]
eqP1 [in Buchberger.Preducestar]
eqP1 [in Buchberger.BuchRed]
eqP1 [in Buchberger.Pminus]
eqP1 [in Buchberger.Pspoly]
eqP1 [in Buchberger.Pcrit]
eqP1 [in Buchberger.Pcomb]
eqP1 [in Buchberger.Pspminus]
eqP1 [in Buchberger.Pplus]
eqP1 [in Buchberger.Pmult]
eqTerm_dec1 [in Buchberger.Preduce]
eqTerm_trans1 [in Buchberger.Preduce]
eqTerm_sym1 [in Buchberger.Preduce]
eqTerm_dec1 [in Buchberger.Peq]
eqTerm_trans1 [in Buchberger.Peq]
eqTerm_sym1 [in Buchberger.Peq]
eqTerm_dec1 [in Buchberger.POrder]
eqTerm_trans1 [in Buchberger.POrder]
eqTerm_sym1 [in Buchberger.POrder]
eqTerm_dec1 [in Buchberger.WfR0]
eqTerm_trans1 [in Buchberger.WfR0]
eqTerm_sym1 [in Buchberger.WfR0]
eqTerm_dec1 [in Buchberger.Buch]
eqTerm_trans1 [in Buchberger.Buch]
eqTerm_sym1 [in Buchberger.Buch]
eqTerm_dec1 [in Buchberger.BuchAux]
eqTerm_trans1 [in Buchberger.BuchAux]
eqTerm_sym1 [in Buchberger.BuchAux]
eqTerm_dec1 [in Buchberger.Preduceplus]
eqTerm_trans1 [in Buchberger.Preduceplus]
eqTerm_sym1 [in Buchberger.Preduceplus]
eqTerm_dec1 [in Buchberger.Pmults]
eqTerm_trans1 [in Buchberger.Pmults]
eqTerm_sym1 [in Buchberger.Pmults]
eqTerm_dec1 [in Buchberger.Preducestar]
eqTerm_trans1 [in Buchberger.Preducestar]
eqTerm_sym1 [in Buchberger.Preducestar]
eqTerm_dec1 [in Buchberger.Preducestar]
eqTerm_trans1 [in Buchberger.Preducestar]
eqTerm_sym1 [in Buchberger.Preducestar]
eqTerm_dec1 [in Buchberger.BuchRed]
eqTerm_trans1 [in Buchberger.BuchRed]
eqTerm_sym1 [in Buchberger.BuchRed]
eqTerm_dec1 [in Buchberger.Pminus]
eqTerm_trans1 [in Buchberger.Pminus]
eqTerm_sym1 [in Buchberger.Pminus]
eqTerm_dec1 [in Buchberger.Pspoly]
eqTerm_trans1 [in Buchberger.Pspoly]
eqTerm_sym1 [in Buchberger.Pspoly]
eqTerm_dec1 [in Buchberger.Pcrit]
eqTerm_trans1 [in Buchberger.Pcrit]
eqTerm_sym1 [in Buchberger.Pcrit]
eqTerm_dec1 [in Buchberger.Pcomb]
eqTerm_trans1 [in Buchberger.Pcomb]
eqTerm_sym1 [in Buchberger.Pcomb]
eqTerm_dec1 [in Buchberger.Pspminus]
eqTerm_trans1 [in Buchberger.Pspminus]
eqTerm_sym1 [in Buchberger.Pspminus]
eqTerm_dec1 [in Buchberger.DivTerm]
eqTerm_trans1 [in Buchberger.DivTerm]
eqTerm_sym1 [in Buchberger.DivTerm]
eqTerm_dec1 [in Buchberger.Pplus]
eqTerm_trans1 [in Buchberger.Pplus]
eqTerm_sym1 [in Buchberger.Pplus]
eqTerm_dec1 [in Buchberger.Pmult]
eqTerm_trans1 [in Buchberger.Pmult]
eqTerm_sym1 [in Buchberger.Pmult]
eqTerm1 [in Buchberger.Preduce]
eqTerm1 [in Buchberger.Peq]
eqTerm1 [in Buchberger.POrder]
eqTerm1 [in Buchberger.WfR0]
eqTerm1 [in Buchberger.Buch]
eqTerm1 [in Buchberger.BuchAux]
eqTerm1 [in Buchberger.Preduceplus]
eqTerm1 [in Buchberger.Pmults]
eqTerm1 [in Buchberger.Preducestar]
eqTerm1 [in Buchberger.Preducestar]
eqTerm1 [in Buchberger.BuchRed]
eqTerm1 [in Buchberger.Pminus]
eqTerm1 [in Buchberger.Pspoly]
eqTerm1 [in Buchberger.Pcrit]
eqTerm1 [in Buchberger.Pcomb]
eqTerm1 [in Buchberger.Pspminus]
eqTerm1 [in Buchberger.DivTerm]
eqTerm1 [in Buchberger.Pplus]
eqTerm1 [in Buchberger.Pmult]
F
foreigner_dec1 [in Buchberger.WfR0]foreigner_dec1 [in Buchberger.Buch]
foreigner_dec1 [in Buchberger.BuchRed]
foreigner1 [in Buchberger.WfR0]
foreigner1 [in Buchberger.Buch]
foreigner1 [in Buchberger.BuchRed]
G
Grobner1 [in Buchberger.WfR0]Grobner1 [in Buchberger.Buch]
Grobner1 [in Buchberger.BuchAux]
Grobner1 [in Buchberger.BuchRed]
I
inPolySet1 [in Buchberger.WfR0]inPolySet1 [in Buchberger.Buch]
inPolySet1 [in Buchberger.BuchAux]
inPolySet1 [in Buchberger.Preduceplus]
inPolySet1 [in Buchberger.Preducestar]
inPolySet1 [in Buchberger.Preducestar]
inPolySet1 [in Buchberger.BuchRed]
inPolySet1 [in Buchberger.Pspoly]
inPolySet1 [in Buchberger.Pcrit]
inPolySet1 [in Buchberger.Pcomb]
invTerm1 [in Buchberger.Preduce]
invTerm1 [in Buchberger.Peq]
invTerm1 [in Buchberger.POrder]
invTerm1 [in Buchberger.WfR0]
invTerm1 [in Buchberger.Buch]
invTerm1 [in Buchberger.BuchAux]
invTerm1 [in Buchberger.Preduceplus]
invTerm1 [in Buchberger.Pmults]
invTerm1 [in Buchberger.Preducestar]
invTerm1 [in Buchberger.Preducestar]
invTerm1 [in Buchberger.BuchRed]
invTerm1 [in Buchberger.Pminus]
invTerm1 [in Buchberger.Pspoly]
invTerm1 [in Buchberger.Pcrit]
invTerm1 [in Buchberger.Pcomb]
invTerm1 [in Buchberger.Pspminus]
invTerm1 [in Buchberger.DivTerm]
invTerm1 [in Buchberger.Pplus]
invTerm1 [in Buchberger.Pmult]
irreducible1 [in Buchberger.WfR0]
irreducible1 [in Buchberger.Buch]
irreducible1 [in Buchberger.BuchAux]
irreducible1 [in Buchberger.Preduceplus]
irreducible1 [in Buchberger.Preducestar]
irreducible1 [in Buchberger.Preducestar]
irreducible1 [in Buchberger.BuchRed]
irreducible1 [in Buchberger.Pspoly]
irreducible1 [in Buchberger.Pcrit]
irreducible1 [in Buchberger.Pcomb]
L
ltP1 [in Buchberger.Preduce]ltP1 [in Buchberger.Peq]
ltP1 [in Buchberger.WfR0]
ltP1 [in Buchberger.Buch]
ltP1 [in Buchberger.BuchAux]
ltP1 [in Buchberger.Preduceplus]
ltP1 [in Buchberger.Pmults]
ltP1 [in Buchberger.Preducestar]
ltP1 [in Buchberger.Preducestar]
ltP1 [in Buchberger.BuchRed]
ltP1 [in Buchberger.Pminus]
ltP1 [in Buchberger.Pspoly]
ltP1 [in Buchberger.Pcrit]
ltP1 [in Buchberger.Pcomb]
ltP1 [in Buchberger.Pspminus]
ltP1 [in Buchberger.Pplus]
ltP1 [in Buchberger.Pmult]
ltT_dec1 [in Buchberger.Preduce]
ltT_dec1 [in Buchberger.WfR0]
ltT_dec1 [in Buchberger.Buch]
ltT_dec1 [in Buchberger.BuchAux]
ltT_dec1 [in Buchberger.Preduceplus]
ltT_dec1 [in Buchberger.Pmults]
ltT_dec1 [in Buchberger.Preducestar]
ltT_dec1 [in Buchberger.Preducestar]
ltT_dec1 [in Buchberger.BuchRed]
ltT_dec1 [in Buchberger.Pminus]
ltT_dec1 [in Buchberger.Pspoly]
ltT_dec1 [in Buchberger.Pcrit]
ltT_dec1 [in Buchberger.Pcomb]
ltT_dec1 [in Buchberger.Pspminus]
ltT_dec1 [in Buchberger.Pplus]
ltT_dec1 [in Buchberger.Pmult]
ltT1 [in Buchberger.Preduce]
ltT1 [in Buchberger.WfR0]
ltT1 [in Buchberger.Buch]
ltT1 [in Buchberger.BuchAux]
ltT1 [in Buchberger.Preduceplus]
ltT1 [in Buchberger.Pmults]
ltT1 [in Buchberger.Preducestar]
ltT1 [in Buchberger.Preducestar]
ltT1 [in Buchberger.BuchRed]
ltT1 [in Buchberger.Pminus]
ltT1 [in Buchberger.Pspoly]
ltT1 [in Buchberger.Pcrit]
ltT1 [in Buchberger.Pcomb]
ltT1 [in Buchberger.Pspminus]
ltT1 [in Buchberger.Pplus]
ltT1 [in Buchberger.Pmult]
M
minuspf1 [in Buchberger.Preduce]minuspf1 [in Buchberger.WfR0]
minuspf1 [in Buchberger.Buch]
minuspf1 [in Buchberger.BuchAux]
minuspf1 [in Buchberger.Preduceplus]
minuspf1 [in Buchberger.Preducestar]
minuspf1 [in Buchberger.Preducestar]
minuspf1 [in Buchberger.BuchRed]
minuspf1 [in Buchberger.Pspoly]
minuspf1 [in Buchberger.Pcrit]
minuspf1 [in Buchberger.Pcomb]
minuspf1 [in Buchberger.Pspminus]
minusTerm1 [in Buchberger.Preduce]
minusTerm1 [in Buchberger.Peq]
minusTerm1 [in Buchberger.POrder]
minusTerm1 [in Buchberger.WfR0]
minusTerm1 [in Buchberger.Buch]
minusTerm1 [in Buchberger.BuchAux]
minusTerm1 [in Buchberger.Preduceplus]
minusTerm1 [in Buchberger.Pmults]
minusTerm1 [in Buchberger.Preducestar]
minusTerm1 [in Buchberger.Preducestar]
minusTerm1 [in Buchberger.BuchRed]
minusTerm1 [in Buchberger.Pminus]
minusTerm1 [in Buchberger.Pspoly]
minusTerm1 [in Buchberger.Pcrit]
minusTerm1 [in Buchberger.Pcomb]
minusTerm1 [in Buchberger.Pspminus]
minusTerm1 [in Buchberger.DivTerm]
minusTerm1 [in Buchberger.Pplus]
minusTerm1 [in Buchberger.Pmult]
mks1 [in Buchberger.WfR0]
mks1 [in Buchberger.Buch]
mks1 [in Buchberger.BuchAux]
mks1 [in Buchberger.BuchRed]
mks1 [in Buchberger.Pspoly]
mks1 [in Buchberger.Pcrit]
mks1 [in Buchberger.Pcomb]
multpf1 [in Buchberger.Pcrit]
mults1 [in Buchberger.Preduce]
mults1 [in Buchberger.WfR0]
mults1 [in Buchberger.Buch]
mults1 [in Buchberger.BuchAux]
mults1 [in Buchberger.Preduceplus]
mults1 [in Buchberger.Preducestar]
mults1 [in Buchberger.Preducestar]
mults1 [in Buchberger.BuchRed]
mults1 [in Buchberger.Pminus]
mults1 [in Buchberger.Pspoly]
mults1 [in Buchberger.Pcrit]
mults1 [in Buchberger.Pcomb]
mults1 [in Buchberger.Pspminus]
mults1 [in Buchberger.Pmult]
multTerm1 [in Buchberger.Preduce]
multTerm1 [in Buchberger.Peq]
multTerm1 [in Buchberger.POrder]
multTerm1 [in Buchberger.WfR0]
multTerm1 [in Buchberger.Buch]
multTerm1 [in Buchberger.BuchAux]
multTerm1 [in Buchberger.Preduceplus]
multTerm1 [in Buchberger.Pmults]
multTerm1 [in Buchberger.Preducestar]
multTerm1 [in Buchberger.Preducestar]
multTerm1 [in Buchberger.BuchRed]
multTerm1 [in Buchberger.Pminus]
multTerm1 [in Buchberger.Pspoly]
multTerm1 [in Buchberger.Pcrit]
multTerm1 [in Buchberger.Pcomb]
multTerm1 [in Buchberger.Pspminus]
multTerm1 [in Buchberger.DivTerm]
multTerm1 [in Buchberger.Pplus]
multTerm1 [in Buchberger.Pmult]
N
nf1 [in Buchberger.WfR0]nf1 [in Buchberger.Buch]
nf1 [in Buchberger.BuchRed]
P
pickinSetp1 [in Buchberger.WfR0]pickinSetp1 [in Buchberger.Buch]
pickinSetp1 [in Buchberger.BuchAux]
pickinSetp1 [in Buchberger.Preduceplus]
pickinSetp1 [in Buchberger.Preducestar]
pickinSetp1 [in Buchberger.Preducestar]
pickinSetp1 [in Buchberger.BuchRed]
pickinSetp1 [in Buchberger.Pspoly]
pickinSetp1 [in Buchberger.Pcrit]
pickinSetp1 [in Buchberger.Pcomb]
pluspf1 [in Buchberger.Preduce]
pluspf1 [in Buchberger.WfR0]
pluspf1 [in Buchberger.Buch]
pluspf1 [in Buchberger.BuchAux]
pluspf1 [in Buchberger.Preduceplus]
pluspf1 [in Buchberger.Pmults]
pluspf1 [in Buchberger.Preducestar]
pluspf1 [in Buchberger.Preducestar]
pluspf1 [in Buchberger.BuchRed]
pluspf1 [in Buchberger.Pminus]
pluspf1 [in Buchberger.Pspoly]
pluspf1 [in Buchberger.Pcrit]
pluspf1 [in Buchberger.Pcomb]
pluspf1 [in Buchberger.Pspminus]
pluspf1 [in Buchberger.Pmult]
plusTerm1 [in Buchberger.Preduce]
plusTerm1 [in Buchberger.Peq]
plusTerm1 [in Buchberger.POrder]
plusTerm1 [in Buchberger.WfR0]
plusTerm1 [in Buchberger.Buch]
plusTerm1 [in Buchberger.BuchAux]
plusTerm1 [in Buchberger.Preduceplus]
plusTerm1 [in Buchberger.Pmults]
plusTerm1 [in Buchberger.Preducestar]
plusTerm1 [in Buchberger.Preducestar]
plusTerm1 [in Buchberger.BuchRed]
plusTerm1 [in Buchberger.Pminus]
plusTerm1 [in Buchberger.Pspoly]
plusTerm1 [in Buchberger.Pcrit]
plusTerm1 [in Buchberger.Pcomb]
plusTerm1 [in Buchberger.Pspminus]
plusTerm1 [in Buchberger.DivTerm]
plusTerm1 [in Buchberger.Pplus]
plusTerm1 [in Buchberger.Pmult]
poly1 [in Buchberger.Preduce]
poly1 [in Buchberger.Peq]
poly1 [in Buchberger.WfR0]
poly1 [in Buchberger.Buch]
poly1 [in Buchberger.BuchAux]
poly1 [in Buchberger.Preduceplus]
poly1 [in Buchberger.Pmults]
poly1 [in Buchberger.Preducestar]
poly1 [in Buchberger.Preducestar]
poly1 [in Buchberger.BuchRed]
poly1 [in Buchberger.Pminus]
poly1 [in Buchberger.Pspoly]
poly1 [in Buchberger.Pcrit]
poly1 [in Buchberger.Pcomb]
poly1 [in Buchberger.Pspminus]
poly1 [in Buchberger.Pplus]
poly1 [in Buchberger.Pmult]
pOO [in Buchberger.Preduce]
pOO [in Buchberger.Peq]
pOO [in Buchberger.WfR0]
pOO [in Buchberger.Buch]
pOO [in Buchberger.BuchAux]
pOO [in Buchberger.Preduceplus]
pOO [in Buchberger.Pmults]
pOO [in Buchberger.Preducestar]
pOO [in Buchberger.Preducestar]
pOO [in Buchberger.BuchRed]
pOO [in Buchberger.Pminus]
pOO [in Buchberger.Pspoly]
pOO [in Buchberger.Pcrit]
pOO [in Buchberger.Pcomb]
pOO [in Buchberger.Pspminus]
pOO [in Buchberger.Pplus]
pOO [in Buchberger.Pmult]
ppcp1 [in Buchberger.WfR0]
ppcp1 [in Buchberger.Buch]
ppcp1 [in Buchberger.BuchRed]
ppc1 [in Buchberger.Preduce]
ppc1 [in Buchberger.WfR0]
ppc1 [in Buchberger.Buch]
ppc1 [in Buchberger.BuchAux]
ppc1 [in Buchberger.Preduceplus]
ppc1 [in Buchberger.Preducestar]
ppc1 [in Buchberger.Preducestar]
ppc1 [in Buchberger.BuchRed]
ppc1 [in Buchberger.Pspoly]
ppc1 [in Buchberger.Pcrit]
ppc1 [in Buchberger.Pcomb]
ppc1 [in Buchberger.Pspminus]
R
Reducef1 [in Buchberger.WfR0]Reducef1 [in Buchberger.Buch]
Reducef1 [in Buchberger.BuchAux]
Reducef1 [in Buchberger.BuchRed]
Reducef1 [in Buchberger.Pspoly]
Reducef1 [in Buchberger.Pcrit]
Reducef1 [in Buchberger.Pcomb]
reduceplus1 [in Buchberger.WfR0]
reduceplus1 [in Buchberger.Buch]
reduceplus1 [in Buchberger.BuchAux]
reduceplus1 [in Buchberger.Preducestar]
reduceplus1 [in Buchberger.Preducestar]
reduceplus1 [in Buchberger.BuchRed]
reduceplus1 [in Buchberger.Pspoly]
reduceplus1 [in Buchberger.Pcrit]
reduceplus1 [in Buchberger.Pcomb]
reducestar_trans1 [in Buchberger.WfR0]
reducestar_trans1 [in Buchberger.Buch]
reducestar_trans1 [in Buchberger.BuchAux]
reducestar_trans1 [in Buchberger.BuchRed]
reducestar_trans1 [in Buchberger.Pspoly]
reducestar_trans1 [in Buchberger.Pcrit]
reducestar_trans1 [in Buchberger.Pcomb]
reducestar1 [in Buchberger.WfR0]
reducestar1 [in Buchberger.Buch]
reducestar1 [in Buchberger.BuchAux]
reducestar1 [in Buchberger.BuchRed]
reducestar1 [in Buchberger.Pspoly]
reducestar1 [in Buchberger.Pcrit]
reducestar1 [in Buchberger.Pcomb]
reduce1 [in Buchberger.WfR0]
reduce1 [in Buchberger.Buch]
reduce1 [in Buchberger.BuchAux]
reduce1 [in Buchberger.Preduceplus]
reduce1 [in Buchberger.Preducestar]
reduce1 [in Buchberger.Preducestar]
reduce1 [in Buchberger.BuchRed]
reduce1 [in Buchberger.Pspoly]
reduce1 [in Buchberger.Pcrit]
reduce1 [in Buchberger.Pcomb]
ReduStarConfluent1 [in Buchberger.WfR0]
ReduStarConfluent1 [in Buchberger.Buch]
ReduStarConfluent1 [in Buchberger.BuchAux]
ReduStarConfluent1 [in Buchberger.BuchRed]
ReduStarConfluent1 [in Buchberger.Pcrit]
ReduStarConfluent1 [in Buchberger.Pcomb]
red1 [in Buchberger.WfR0]
red1 [in Buchberger.Buch]
red1 [in Buchberger.BuchRed]
RO1 [in Buchberger.Buch]
S
seqp_dec1 [in Buchberger.Preduce]seqp_dec1 [in Buchberger.WfR0]
seqp_dec1 [in Buchberger.Buch]
seqp_dec1 [in Buchberger.BuchAux]
seqp_dec1 [in Buchberger.Preduceplus]
seqp_dec1 [in Buchberger.Pmults]
seqp_dec1 [in Buchberger.Preducestar]
seqp_dec1 [in Buchberger.Preducestar]
seqp_dec1 [in Buchberger.BuchRed]
seqp_dec1 [in Buchberger.Pminus]
seqp_dec1 [in Buchberger.Pspoly]
seqp_dec1 [in Buchberger.Pcrit]
seqp_dec1 [in Buchberger.Pcomb]
seqp_dec1 [in Buchberger.Pspminus]
seqp_dec1 [in Buchberger.Pplus]
seqp_dec1 [in Buchberger.Pmult]
spminusf1 [in Buchberger.Preduce]
spminusf1 [in Buchberger.WfR0]
spminusf1 [in Buchberger.Buch]
spminusf1 [in Buchberger.BuchAux]
spminusf1 [in Buchberger.Preduceplus]
spminusf1 [in Buchberger.Preducestar]
spminusf1 [in Buchberger.Preducestar]
spminusf1 [in Buchberger.BuchRed]
spminusf1 [in Buchberger.Pspoly]
spminusf1 [in Buchberger.Pcrit]
spminusf1 [in Buchberger.Pcomb]
spolyf1 [in Buchberger.WfR0]
spolyf1 [in Buchberger.Buch]
spolyf1 [in Buchberger.BuchAux]
spolyf1 [in Buchberger.BuchRed]
spolyf1 [in Buchberger.Pcrit]
spolyf1 [in Buchberger.Pcomb]
spolyp1 [in Buchberger.WfR0]
spolyp1 [in Buchberger.Buch]
spolyp1 [in Buchberger.BuchRed]
SpolyQ1 [in Buchberger.WfR0]
SpolyQ1 [in Buchberger.Buch]
SpolyQ1 [in Buchberger.BuchAux]
SpolyQ1 [in Buchberger.BuchRed]
SpolyQ1 [in Buchberger.Pcrit]
SpolyQ1 [in Buchberger.Pcomb]
Spoly1 [in Buchberger.WfR0]
Spoly1 [in Buchberger.Buch]
Spoly1 [in Buchberger.BuchAux]
Spoly1 [in Buchberger.BuchRed]
stable1 [in Buchberger.BuchRed]
s2p1 [in Buchberger.WfR0]
s2p1 [in Buchberger.Buch]
s2p1 [in Buchberger.BuchAux]
s2p1 [in Buchberger.Preduceplus]
s2p1 [in Buchberger.Preducestar]
s2p1 [in Buchberger.Preducestar]
s2p1 [in Buchberger.BuchRed]
s2p1 [in Buchberger.Pspoly]
s2p1 [in Buchberger.Pcrit]
s2p1 [in Buchberger.Pcomb]
T
Term1 [in Buchberger.Preduce]Term1 [in Buchberger.Peq]
Term1 [in Buchberger.POrder]
Term1 [in Buchberger.WfR0]
Term1 [in Buchberger.Buch]
Term1 [in Buchberger.BuchAux]
Term1 [in Buchberger.Preduceplus]
Term1 [in Buchberger.Pmults]
Term1 [in Buchberger.Preducestar]
Term1 [in Buchberger.Preducestar]
Term1 [in Buchberger.BuchRed]
Term1 [in Buchberger.Pminus]
Term1 [in Buchberger.Pspoly]
Term1 [in Buchberger.Pcrit]
Term1 [in Buchberger.Pcomb]
Term1 [in Buchberger.Pspminus]
Term1 [in Buchberger.DivTerm]
Term1 [in Buchberger.Pplus]
Term1 [in Buchberger.Pmult]
U
unit1 [in Buchberger.BuchRed]Z
zeroP_dec1 [in Buchberger.Preduce]zeroP_dec1 [in Buchberger.Peq]
zeroP_dec1 [in Buchberger.POrder]
zerop_dec1 [in Buchberger.WfR0]
zeroP_dec1 [in Buchberger.WfR0]
zerop_dec1 [in Buchberger.Buch]
zeroP_dec1 [in Buchberger.Buch]
zeroP_dec1 [in Buchberger.BuchAux]
zeroP_dec1 [in Buchberger.Preduceplus]
zeroP_dec1 [in Buchberger.Pmults]
zeroP_dec1 [in Buchberger.Preducestar]
zeroP_dec1 [in Buchberger.Preducestar]
zerop_dec1 [in Buchberger.BuchRed]
zeroP_dec1 [in Buchberger.BuchRed]
zeroP_dec1 [in Buchberger.Pminus]
zeroP_dec1 [in Buchberger.Pspoly]
zeroP_dec1 [in Buchberger.Pcrit]
zeroP_dec1 [in Buchberger.Pcomb]
zeroP_dec1 [in Buchberger.Pspminus]
zeroP_dec1 [in Buchberger.DivTerm]
zeroP_dec1 [in Buchberger.Pplus]
zeroP_dec1 [in Buchberger.Pmult]
zeroP1 [in Buchberger.Preduce]
zeroP1 [in Buchberger.Peq]
zeroP1 [in Buchberger.POrder]
zerop1 [in Buchberger.WfR0]
zeroP1 [in Buchberger.WfR0]
zerop1 [in Buchberger.Buch]
zeroP1 [in Buchberger.Buch]
zeroP1 [in Buchberger.BuchAux]
zeroP1 [in Buchberger.Preduceplus]
zeroP1 [in Buchberger.Pmults]
zeroP1 [in Buchberger.Preducestar]
zeroP1 [in Buchberger.Preducestar]
zerop1 [in Buchberger.BuchRed]
zeroP1 [in Buchberger.BuchRed]
zeroP1 [in Buchberger.Pminus]
zeroP1 [in Buchberger.Pspoly]
zeroP1 [in Buchberger.Pcrit]
zeroP1 [in Buchberger.Pcomb]
zeroP1 [in Buchberger.Pspminus]
zeroP1 [in Buchberger.DivTerm]
zeroP1 [in Buchberger.Pplus]
zeroP1 [in Buchberger.Pmult]
Definition Index
A
addEnd [in Buchberger.BuchAux]addRes [in Buchberger.Buch]
B
Bad [in Buchberger.Bar]BadM [in Buchberger.WfR0]
buch [in Buchberger.Buch]
C
canonical [in Buchberger.POrder]Cb [in Buchberger.BuchAux]
D
DecRel [in Buchberger.Dickson]degc [in Buchberger.LexiOrder]
divp [in Buchberger.BuchAux]
divpf [in Buchberger.Pcrit]
divPp [in Buchberger.Pcrit]
divTerm [in Buchberger.DivTerm]
div_mon_clean [in Buchberger.Monomials]
div_mon [in Buchberger.Monomials]
Dmult [in Buchberger.Pcrit]
E
eqPf [in Buchberger.Peq]eqT [in Buchberger.Term]
eqTerm [in Buchberger.Term]
F
Fl [in Buchberger.Buch]foreigner [in Buchberger.BuchAux]
foreigner_dec [in Buchberger.BuchAux]
fP [in Buchberger.POrder]
fspoly [in Buchberger.POrder]
G
GBarlR [in Buchberger.Dickson]genOCPf [in Buchberger.Buch]
genPcPf [in Buchberger.Buch]
genPcPf0 [in Buchberger.Buch]
gen_mon [in Buchberger.Monomials]
getRes [in Buchberger.Buch]
get_monL [in Buchberger.WfR0]
get_mon [in Buchberger.WfR0]
GRBar [in Buchberger.Bar]
I
inv [in Buchberger.Pminus]invTerm [in Buchberger.Term]
irreducible [in Buchberger.Preduce]
is_nil [in Buchberger.Monomials]
J
jj [in Buchberger.Dickson]L
leq [in Buchberger.Dickson]lessP [in Buchberger.Peq]
lessP3 [in Buchberger.Peq]
LetP [in Buchberger.LetP]
ltT [in Buchberger.POrder]
M
MinD [in Buchberger.Dickson]minuspf [in Buchberger.Pminus]
minuspp [in Buchberger.Pminus]
minusTerm [in Buchberger.Term]
mks [in Buchberger.Preducestar]
mks [in Buchberger.Preducestar]
mk_clean [in Buchberger.DivTerm]
monLift [in Buchberger.Dickson]
multpf [in Buchberger.Pmult]
mults [in Buchberger.Pmults]
multTerm [in Buchberger.Term]
mult_mon [in Buchberger.Monomials]
M1 [in Buchberger.Term]
N
NegRel [in Buchberger.Dickson]nf [in Buchberger.BuchAux]
nZterm [in Buchberger.POrder]
O
olist [in Buchberger.POrder]P
pbuchf [in Buchberger.Buch]pickinSet [in Buchberger.Preducestar]
pickinSet [in Buchberger.Preducestar]
plusp [in Buchberger.Pplus]
pluspf [in Buchberger.Pplus]
plusTerm [in Buchberger.Term]
pmon1 [in Buchberger.Monomials]
pmon2 [in Buchberger.Monomials]
pO [in Buchberger.POrder]
poly [in Buchberger.POrder]
ppc [in Buchberger.DivTerm]
ppcm_mon [in Buchberger.Monomials]
ppcp [in Buchberger.BuchAux]
Pred [in Buchberger.Bar]
ProdRel [in Buchberger.Dickson]
prod_lt [in Buchberger.Dickson]
projsig1 [in Buchberger.Pplus]
PtoS [in Buchberger.Buch]
pX [in Buchberger.POrder]
R
recomp [in Buchberger.Monomials]red [in Buchberger.BuchAux]
Red [in Buchberger.BuchRed]
red [in Buchberger.Fred]
redacc [in Buchberger.BuchRed]
redacc [in Buchberger.Fred]
redbuch [in Buchberger.BuchRed]
Reducef [in Buchberger.Preducestar]
Reducef [in Buchberger.Preducestar]
reducep [in Buchberger.BuchRed]
Rel [in Buchberger.Bar]
RL [in Buchberger.Buch]
Rminus [in Buchberger.Pcrit]
S
Sdep [in Buchberger.Buch]selectdivf [in Buchberger.Preducestar]
selectdivf [in Buchberger.Preducestar]
selectpolyf [in Buchberger.Preducestar]
selectpolyf [in Buchberger.Preducestar]
seqP [in Buchberger.Peq]
sgen [in Buchberger.BuchAux]
size [in Buchberger.Peq]
sizel [in Buchberger.Peq]
sizel3 [in Buchberger.Peq]
slice [in Buchberger.Buch]
slicef [in Buchberger.Buch]
sltP [in Buchberger.POrder]
sminus [in Buchberger.Pminus]
smult [in Buchberger.Pmult]
smults [in Buchberger.Pmults]
sndL [in Buchberger.Dickson]
splus [in Buchberger.Pplus]
spminusf [in Buchberger.Pspminus]
spO [in Buchberger.BuchAux]
spolyf [in Buchberger.Pspoly]
spolyp [in Buchberger.BuchAux]
sp1 [in Buchberger.BuchAux]
sscal [in Buchberger.BuchAux]
strip [in Buchberger.Buch]
s2p [in Buchberger.Preduce]
T
Term [in Buchberger.Term]Tl [in Buchberger.Buch]
tmults [in Buchberger.Pmults]
twoP_ind [in Buchberger.Pmults]
T1 [in Buchberger.Term]
T2M [in Buchberger.Term]
U
unit [in Buchberger.BuchAux]W
WR [in Buchberger.Bar]Z
zerop [in Buchberger.BuchAux]zeroP [in Buchberger.Term]
zero_mon [in Buchberger.Monomials]
Record Index
C
CoefStructure [in Buchberger.CoefStructure]O
OrderStructure [in Buchberger.OrderStructure]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1986 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (368 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (668 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (622 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (129 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |