Ascending sets and basic sets

This file defines the abstract theory of ascending sets and basic sets. An ascending set is a triangular set with additional reduction properties. A basic set is the "smallest" ascending set contained in a given set of polynomials.

Main declarations

• AscendingSetTheory: A typeclass abstracting the ascending-set predicate (e.g., strong vs. weak reduction) and the algorithm to compute a basic set from a list of polynomials.

References

• [Wen-Tsun Wu, Basic principles of mechanical theorem proving in elementary geometries] [WT86]
• Wen-Tsun Wu, Mathematics Mechanization

class AscendingSetTheory (σ : Type u_1) (R : Type u_2) [CommSemiring R] [DecidableEq R] [LinearOrder σ] (isAscendingSet : TriangularSet σ R → Prop) : Type (max u_1 u_2)

The abstract theory of Ascending Sets. This class allows us to define what it means for a TriangularSet to be an "Ascending Set". Different instances can implement Ritt's strong ascending sets or Wu's weak ascending sets.

• decidableReducedTo : DecidablePred isAscendingSet
• initial_reducedToSet_of_max_vars_ne_bot ⦃S : TriangularSet σ R⦄ ⦃i : ℕ⦄ : isAscendingSet S → (S i).vars.max ≠ ⊥ → (S i).initial.reducedToSet S

  A key property linking the ascending set structure to the initial. If S is an ascending set, the initial of any non-constant element in S must be reduced with respect to S.

• basicSet : List (MvPolynomial σ R) → TriangularSet σ R

  Computes a Basic Set from a list of polynomials.

• basicSet_isAscendingSet (l : List (MvPolynomial σ R)) : isAscendingSet (basicSet isAscendingSet l)

  The output is always an Ascending Set.

• basicSet_subset (l : List (MvPolynomial σ R)) ⦃c : MvPolynomial σ R⦄ : c ∈ basicSet isAscendingSet l → c ∈ l

  The output is a subset of the input.

• basicSet_minimal (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : isAscendingSet S → (∀ ⦃p : MvPolynomial σ R⦄, p ∈ S → p ∈ l) → basicSet isAscendingSet l ≤ S

  Minimality condition: the output is ≤ any other ascending set contained in the input.

• basicSet_append_lt_of_exists_reducedToSet ⦃l1 l2 : List (MvPolynomial σ R)⦄ : (∃ p ∈ l2, p ≠ 0 ∧ p.reducedToSet (basicSet isAscendingSet l1)) → basicSet isAscendingSet (l2 ++ l1) < basicSet isAscendingSet l1

  Order reduction property: appending a reduced element strictly decreases the basic set order. Crucial for proving termination of zero decomposition.

def TriangularSet.IsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangularSet σ R) : Prop

Definition of Standard (Ritt) Ascending Set: A Triangular Set is an Ascending Set if every element is reduced with respect to its predecessors.

Equations

• S.IsAscendingSet = ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).reducedTo (S i)

def TriangularSet.IsWeakAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (S : TriangularSet σ R) : Prop

Definition of Weak (Wu) Ascending Set: A Triangular Set is an Ascending Set if every element's initial is reduced with respect to its predecessors.

Equations

• S.IsWeakAscendingSet = ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).initial.reducedTo (S i)

theorem TriangularSet.isAscendingSet_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} : S.IsAscendingSet ↔ ∀ ⦃i j : ℕ⦄, i < j → i < S.length → (S j).reducedTo (S i)

theorem TriangularSet.isWeakAscendingSet_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} : S.IsWeakAscendingSet ↔ ∀ ⦃i j : ℕ⦄, i < j → i < S.length → (S j).initial.reducedTo (S i)

@[instance_reducible]

noncomputable instance TriangularSet.instDecidablePredIsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : DecidablePred IsAscendingSet

Equations

• x✝.instDecidablePredIsAscendingSet = decidable_of_iff (∀ j < x✝.length, ∀ i < j, (x✝ j).reducedTo (x✝ i)) ⋯

@[instance_reducible]

noncomputable instance TriangularSet.instDecidablePredIsWeakAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : DecidablePred IsWeakAscendingSet

Equations

• x✝.instDecidablePredIsWeakAscendingSet = decidable_of_iff (∀ j < x✝.length, ∀ i < j, (x✝ j).initial.reducedTo (x✝ i)) ⋯

theorem TriangularSet.isWeakAscendingSet_of_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} : S.IsAscendingSet → S.IsWeakAscendingSet

theorem TriangularSet.initial_reducedToSet_of_max_vars_ne_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] {S : TriangularSet σ R} {i : ℕ} : isAscendingSet S → (S i).vars.max ≠ ⊥ → (S i).initial.reducedToSet S

theorem TriangularSet.initial_reducedToSet_of_max_vars_ne_bot' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : isAscendingSet S) : p ∈ S → p.vars.max ≠ ⊥ → p.initial.reducedToSet S

theorem TriangularSet.isAscendingSet_single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (p : MvPolynomial σ R) : (single p).IsAscendingSet

theorem TriangularSet.isAscendingSet_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : ∅.IsAscendingSet

theorem TriangularSet.isAscendingSet_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} (n : ℕ) : S.IsAscendingSet → (S.take n).IsAscendingSet

theorem TriangularSet.isAscendingSet_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} (n : ℕ) : S.IsAscendingSet → (S.drop n).IsAscendingSet

theorem TriangularSet.isAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) (hp : p.reducedToSet S) : S.IsAscendingSet → (S.concat p h).IsAscendingSet

theorem TriangularSet.isAscendingSet_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (hp : p.reducedToSet S) : S.IsAscendingSet → (S.takeConcat p).IsAscendingSet

theorem TriangularSet.isWeakAscendingSet_single {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (p : MvPolynomial σ R) : (single p).IsWeakAscendingSet

theorem TriangularSet.isWeakAscendingSet_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : ∅.IsWeakAscendingSet

theorem TriangularSet.isWeakAscendingSet_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} (n : ℕ) : S.IsWeakAscendingSet → (S.take n).IsWeakAscendingSet

theorem TriangularSet.isWeakAscendingSet_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} (n : ℕ) : S.IsWeakAscendingSet → (S.drop n).IsWeakAscendingSet

theorem TriangularSet.isWeakAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) (hp : p.initial.reducedToSet S) : S.IsWeakAscendingSet → (S.concat p h).IsWeakAscendingSet

theorem TriangularSet.isWeakAscendingSet_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {S : TriangularSet σ R} {p : MvPolynomial σ R} (hp : p.initial.reducedToSet S) : S.IsWeakAscendingSet → (S.takeConcat p).IsWeakAscendingSet

def MvPolynomial.List.basicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (isAscendingSet : TriangularSet σ R → Prop) [AscendingSetTheory σ R isAscendingSet] (l : List (MvPolynomial σ R)) : TriangularSet σ R

The Basic Set of a list l, as computed by the AscendingSetTheory instance.

Equations

• MvPolynomial.List.basicSet isAscendingSet l = AscendingSetTheory.basicSet isAscendingSet l

theorem MvPolynomial.List.basicSet_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] (l : List (MvPolynomial σ R)) : ↑(basicSet isAscendingSet l) ⊆ {p : MvPolynomial σ R | p ∈ l}

theorem MvPolynomial.List.basicSet_minimal {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : isAscendingSet S → ↑S ⊆ {p : MvPolynomial σ R | p ∈ l} → basicSet isAscendingSet l ≤ S

theorem MvPolynomial.List.basicSet_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] (l : List (MvPolynomial σ R)) : isAscendingSet (basicSet isAscendingSet l)

theorem MvPolynomial.List.basicSet_toList_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] (l : List (MvPolynomial σ R)) : basicSet isAscendingSet (basicSet isAscendingSet l).toList ≈ basicSet isAscendingSet l

theorem MvPolynomial.List.basicSet_ge_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] {l1 l2 : List (MvPolynomial σ R)} : l1 ⊆ l2 → basicSet isAscendingSet l2 ≤ basicSet isAscendingSet l1

theorem MvPolynomial.List.basicSet_append_comm {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] {l1 l2 : List (MvPolynomial σ R)} : basicSet isAscendingSet (l1 ++ l2) ≈ basicSet isAscendingSet (l2 ++ l1)

theorem MvPolynomial.List.basicSet_append_lt_of_exists_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] {l1 l2 : List (MvPolynomial σ R)} (h : ∃ p ∈ l2, p ≠ 0 ∧ p.reducedToSet (basicSet isAscendingSet l1)) : basicSet isAscendingSet (l2 ++ l1) < basicSet isAscendingSet l1

theorem TriangularSet.basicSet_toList_le_of_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {isAscendingSet : TriangularSet σ R → Prop} [AscendingSetTheory σ R isAscendingSet] {S : TriangularSet σ R} (hS : isAscendingSet S) : MvPolynomial.List.basicSet isAscendingSet S.toList ≤ S

@[irreducible]

noncomputable def IsAscendingSet.basicSet.go {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : TriangularSet σ R

The recursive algorithm for computing the Standard Basic Set.

Equations

• One or more equations did not get rendered due to their size.
• IsAscendingSet.basicSet.go [] BS hl1_2 = BS

noncomputable def IsAscendingSet.basicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) : TriangularSet σ R

Computes the Standard Basic Set of a list of polynomials. The algorithm works by:

1. Sort the list and let BS = ∅.
2. Pick the first (minimal) element B in the list.
3. Update the current basic set BS with B using takeConcat (which handles replacements).
4. Filter the remaining list to keep only elements reduced w.r.t. the new BS and go to step 2.

Equations

• IsAscendingSet.basicSet l = IsAscendingSet.basicSet.go (List.filter (fun (x : MvPolynomial σ R) => decide (x ≠ 0)) (l.mergeSort fun (a b : MvPolynomial σ R) => decide (a ≤ b))) ∅ ⋯

theorem IsAscendingSet.basicSetGo_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (h : l ≠ []) (hl2 : (l.head h).reducedToSet BS) : basicSet.go l BS hl1 < BS

theorem IsAscendingSet.basicSetGo_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : Option.all (fun (p : MvPolynomial σ R) => decide (p.reducedToSet BS)) l.head? = true) : basicSet.go l BS hl1 ≤ BS

theorem IsAscendingSet.mem_of_mem_basicSetGo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (p : MvPolynomial σ R) : p ∉ BS → p ∈ basicSet.go l BS hl1 → p ∈ l

theorem IsAscendingSet.basicSetGo_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : Option.all (fun (p : MvPolynomial σ R) => decide (p.reducedToSet BS)) l.head? = true → BS.IsAscendingSet → (basicSet.go l BS hl1).IsAscendingSet

theorem IsAscendingSet.basicSetGo_le_ascendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) : List.Pairwise (fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2) l → (∀ p ∈ l, BS.CanConcat p) → Option.all (fun (x : MvPolynomial σ R) => decide (x.reducedToSet BS)) l.head? = true → ∀ (T : TriangularSet σ R), T.IsAscendingSet → (BS.length ≤ T.length ∧ ∀ i < BS.length, BS i ≈ T i) → (∀ p ∈ T, (∀ i < BS.length, ¬BS i ≈ p) → p ∈ l) → basicSet.go l BS hl1 ≤ T

The core lemma proving that the computed Basic Set is indeed minimal among all ascending sets contained in l.

theorem IsAscendingSet.basicSet_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) : (basicSet l).IsAscendingSet

theorem IsAscendingSet.basicSet_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) ⦃p : MvPolynomial σ R⦄ : p ∈ basicSet l → p ∈ l

theorem IsAscendingSet.basicSet_minimal {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : S.IsAscendingSet → (∀ ⦃p : MvPolynomial σ R⦄, p ∈ S → p ∈ l) → basicSet l ≤ S

@[instance_reducible]

noncomputable instance IsAscendingSet.instAscendingSetTheoryIsAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : AscendingSetTheory σ R TriangularSet.IsAscendingSet

The Standard Basic Set algorithm satisfies the abstract AscendingSetTheory interface.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

noncomputable def IsWeakAscendingSet.basicSet.go {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : TriangularSet σ R

The recursive algorithm for computing the Weak Basic Set.

Equations

• One or more equations did not get rendered due to their size.
• IsWeakAscendingSet.basicSet.go [] BS hl1_2 hl2_2 = BS

noncomputable def IsWeakAscendingSet.basicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) : TriangularSet σ R

Computes the Weak Basic Set of a list of polynomials. Difference from Standard: The filter condition includes B.max_vars < p.max_vars. This is because p.initial.reducedTo B does NOT imply B.max_vars < p.max_vars (unlike strong reduction). We must enforce the triangular structure explicitly.

Equations

• One or more equations did not get rendered due to their size.

theorem IsWeakAscendingSet.basicSetGo_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) (h : l ≠ []) : (l.head h).initial.reducedToSet BS → basicSet.go l BS hl1 hl2 < BS

theorem IsWeakAscendingSet.basicSetGo_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : Option.all (fun (p : MvPolynomial σ R) => decide (p.initial.reducedToSet BS)) l.head? = true → basicSet.go l BS hl1 hl2 ≤ BS

theorem IsWeakAscendingSet.mem_of_mem_basicSetGo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) (p : MvPolynomial σ R) : p ∉ BS → p ∈ basicSet.go l BS hl1 hl2 → p ∈ l

theorem IsWeakAscendingSet.basicSetGo_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : Option.all (fun (p : MvPolynomial σ R) => decide (p.initial.reducedToSet BS)) l.head? = true → BS.IsWeakAscendingSet → (basicSet.go l BS hl1 hl2).IsWeakAscendingSet

theorem IsWeakAscendingSet.basicSetGo_le_ascendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : List.Pairwise (fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2) l → Option.all (fun (p : MvPolynomial σ R) => decide (p.initial.reducedToSet BS)) l.head? = true → ∀ (T : TriangularSet σ R), T.IsWeakAscendingSet → (BS.length ≤ T.length ∧ ∀ i < BS.length, BS i ≈ T i) → (∀ p ∈ T, (∀ i < BS.length, ¬BS i ≈ p) → p ∈ l) → basicSet.go l BS hl1 hl2 ≤ T

theorem IsWeakAscendingSet.basicSet_isWeakAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) : (basicSet l).IsWeakAscendingSet

theorem IsWeakAscendingSet.basicSet_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) ⦃p : MvPolynomial σ R⦄ : p ∈ basicSet l → p ∈ l

theorem IsWeakAscendingSet.basicSet_minimal {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : S.IsWeakAscendingSet → (∀ ⦃p : MvPolynomial σ R⦄, p ∈ S → p ∈ l) → basicSet l ≤ S

@[instance_reducible]

noncomputable instance IsWeakAscendingSet.instAscendingSetTheoryIsWeakAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] : AscendingSetTheory σ R TriangularSet.IsWeakAscendingSet

The Weak Basic Set algorithm satisfies the abstract AscendingSetTheory interface.

Equations

• One or more equations did not get rendered due to their size.