FreeGroup.Red.trans
theorem FreeGroup.Red.trans :
∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₃ → FreeGroup.Red L₁ L₃ := by
sorry
This theorem states that for any type `α` and any three lists `L₁`, `L₂`, and `L₃` of pairs of elements from `α` and boolean values, if there is a reflexive-transitive relation (`FreeGroup.Red`) from `L₁` to `L₂`, and another reflexive-transitive relation from `L₂` to `L₃`, then there is also a reflexive-transitive relation from `L₁` to `L₃`. In other words, the reflexive-transitive relation `FreeGroup.Red` is transitive.
More concisely: If `R₁` is a reflexive-transitive relation from `α × bool` to `α × bool` between lists `L₁` and `L₂`, and `R₂` is another reflexive-transitive relation from `α × bool` to `α × bool` between lists `L₂` and `L₃`, then the composition of `R₁` and `R₂` is a reflexive-transitive relation between `L₁` and `L₃`.
|
FreeGroup.lift.of
theorem FreeGroup.lift.of :
∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β} {x : α}, (FreeGroup.lift f) (FreeGroup.of x) = f x := by
sorry
The theorem `FreeGroup.lift.of` asserts that for any types `α` and `β`, given that `β` is a group, for any function `f` from `α` to `β`, and for any element `x` of `α`, the free group lift of `f` applied to the canonical injection of `x` into the free group over `α` is equal to `f` applied to `x`. In other words, lifting a function to a free group and then applying it to an element of the group (which has been injected into the group via the canonical injection) gives the same result as simply applying the function to the element in the first place.
More concisely: For any function `f` from type `α` to group `β`, and for any element `x` in type `α`, the free group lift of `f` applied to the canonical injection of `x` equals `f` applied to `x`.
|
FreeAddGroup.reduce.rev
theorem FreeAddGroup.reduce.rev :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
This theorem states that for any type `α` with decidable equality and any pair of lists of pairs of elements of `α` and booleans, `L₁` and `L₂`, if `L₁` reduces to `L₂` under the reflexive-transitive closure of `Red.Step`, then `L₂` can be reduced to the maximal reduction of `L₁` under the same relation. In other words, if we can get from `L₁` to `L₂` by a series of reduction steps, then we can get from `L₂` to the maximal reduction of `L₁` by a similar series of reduction steps.
More concisely: If `L₁` reduces to `L₂` under the reflexive-transitive closure of reduction steps in Lean 4 for a decidably equal type `α`, then `L₂` can be reduced to the maximal reduction of `L₁`.
|
FreeAddGroup.reduce.self
theorem FreeAddGroup.reduce.self :
∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.mk (FreeAddGroup.reduce L) = FreeAddGroup.mk L
The theorem `FreeAddGroup.reduce.self` states that for any type `α` with decidable equality and any list `L` of pairs of elements from `α` and boolean values, the additive free group element corresponding to the maximal reduction of the list `L` is the same as the additive free group element corresponding to the original list `L` itself. In essence, this says that the process of maximal reduction does not change the element of the additive free group that a given list represents.
More concisely: For any type `α` with decidable equality and any list `L` of pairs from `α × bool` in the additive free group, the maximal reduction of `L` leaves the group element unchanged.
|
FreeGroup.Red.Step.cons_not
theorem FreeGroup.Red.Step.cons_not :
∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool}, FreeGroup.Red.Step ((x, b) :: (x, !b) :: L) L
This theorem states that for any type `α`, any list `L` of pairs of `α` and `Bool`, and any `α` value `x` and boolean value `b`, a `FreeGroup.Red.Step` from a list beginning with the pair `(x, b)` followed by `(x, !b)` and then `L` to the list `L` itself always exists. Essentially, it says that in the reduction process of a free group, a pair and its inverse can be removed from the list.
More concisely: For any type `α` and list `L` of pairs of `α` and booleans, there exists a `FreeGroup.Red.Step` between lists `[(x, b), (x, !b), L]` and `L`, where `x : α` and `b : Bool`.
|
FreeGroup.map.unique
theorem FreeGroup.map.unique :
∀ {α : Type u} {β : Type v} {f : α → β} (g : FreeGroup α →* FreeGroup β),
(∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)) → ∀ {x : FreeGroup α}, g x = (FreeGroup.map f) x
This theorem states that for any two types `α` and `β`, and any function `f` from `α` to `β`, if we have a group homomorphism `g` from the free group over `α` to the free group over `β` such that `g` when applied to any element `x` of `α` (considered as an element of the free group over `α` via the canonical injection `FreeGroup.of`) gives the same result as first applying the function `f` to `x` and then considering the result as an element of the free group over `β` (also via `FreeGroup.of`), then this group homomorphism `g` is equal to the unique group homomorphism from the free group over `α` to the free group over `β` that extends the function `f`, i.e., `g` equals `FreeGroup.map f` applied to any element of the free group over `α`. In short, any function from `α` to `β` extends uniquely to a group homomorphism from the free group over `α` to the free group over `β`.
More concisely: Given any function between types `α` and `β`, there exists a unique group homomorphism from the free group over `α` to the free group over `β` extending that function.
|
FreeGroup.toWord_injective
theorem FreeGroup.toWord_injective : ∀ {α : Type u} [inst : DecidableEq α], Function.Injective FreeGroup.toWord := by
sorry
This theorem states that for any type `α` with decidable equality (i.e., given any two elements of `α`, we can decide whether they are equal or not), the function `FreeGroup.toWord` is injective. In other words, if `FreeGroup.toWord` is applied to two elements from the free group over `α` and produces the same result, then those two elements were initially the same. The `FreeGroup.toWord` function converts an element of the free group into a list of pairs, where each pair consists of an element from `α` and a boolean value, and this function performs a "maximal reduction" on the free group element. The theorem is stating that this function uniquely identifies each element of the free group.
More concisely: For every type `α` with decidable equality, the injective function `FreeGroup.toWord` from the free group over `α` to the list of pairs of elements from `α` and booleans uniquely identifies each element in the free group.
|
FreeGroup.Red.cons_nil_iff_singleton
theorem FreeGroup.Red.cons_nil_iff_singleton :
∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool},
FreeGroup.Red ((x, b) :: L) [] ↔ FreeGroup.Red L [(x, !b)]
This theorem establishes a property of the reflexive-transitive closure of the `Red.Step` relation on lists of pairs of elements of an arbitrary type and booleans, referred to as the "FreeGroup.Red" relation. Specifically, for any type `α`, any list `L` of pairs of `α` and `bool`, and any `α` element `x` and `bool` element `b`, it states that a list starting with the pair `(x, b)` followed by `L` can be reduced to the empty list under the `FreeGroup.Red` relation if and only if the list `L` can be reduced to a list containing solely the pair `(x, !b)`, where `!b` is the negation of `b`. In intuitive terms, if a word `xw` can be reduced to the empty word, then `w` can be reduced to the inverse of `x`.
More concisely: For any type `α` and list `L` of pairs of `α` and booleans, if the list `[(x, b) :: L]` can be reduced to the empty list under the `FreeGroup.Red` relation, then `L` can be reduced to the list `[(x, !b)]`.
|
FreeGroup.reduce.eq_of_red
theorem FreeGroup.reduce.eq_of_red :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.Red L₁ L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
The theorem `FreeGroup.reduce.eq_of_red` asserts that for any type `α` with decidable equality and any two lists `L₁` and `L₂` of pairs of elements of `α` and Boolean values, if there exists a reflexive-transitive reduction from `L₁` to `L₂`, then these two lists have the same maximal reduction. In other words, if one word can be reduced to another, then their maximal reductions, which are computable when `α` has decidable equality, are identical.
More concisely: If `α` has decidable equality and there exists a reflexive-transitive reduction from list `L₁` to list `L₂` of pairs of elements and Boolean values from `α`, then `L₁` and `L₂` have the same maximal reduction.
|
FreeGroup.Red.church_rosser
theorem FreeGroup.Red.church_rosser :
∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ L₃ → Relation.Join FreeGroup.Red L₂ L₃
The Church-Rosser theorem for word reduction states that for any given type `α` and three lists of pairs of elements of type `α` and booleans `L₁`, `L₂`, and `L₃`, if the list `L₁` reduces to both `L₂` and `L₃` under the reflexive-transitive closure of the `Red.Step` relation (represented as `FreeGroup.Red L₁ L₂` and `FreeGroup.Red L₁ L₃`), then there exists a list `L₄` such that `L₂` and `L₃` can both reduce to `L₄` under the same relation. This condition is represented by the join of the reduction relation between `L₂` and `L₃`. This theorem is also known as Newman's diamond lemma.
More concisely: If `L₁` reduces to both `L₂` and `L₃` under the reflexive-transitive closure of `Red.Step` relation, then there exists a list `L₄` such that `L₂` and `L₃` can both reduce to `L₄` under the same relation (Church-Rosser theorem for word reduction, or Newman's diamond lemma).
|
FreeAddGroup.lift.of
theorem FreeAddGroup.lift.of :
∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β} {x : α},
(FreeAddGroup.lift f) (FreeAddGroup.of x) = f x
The theorem `FreeAddGroup.lift.of` states that for any types `α` and `β`, where `β` is an additive group, and for any function `f` from `α` to `β`, and for any element `x` of type `α`, the result of applying the group homomorphism, produced by `FreeAddGroup.lift` on the function `f`, to the `FreeAddGroup` representation of `x` (which is obtained by the function `FreeAddGroup.of`) is equal to the result of applying the function `f` to `x`. In other words, lifting the function to a homomorphism and then applying it to the free group element of `x` is equivalent to applying the function directly to `x`.
More concisely: For any function `f` from type `α` to an additive group `β`, and for any `x` in `α`, the group homomorphism obtained from `f` through `FreeAddGroup.lift` applied to `FreeAddGroup.of x` equals `f(x)`.
|
FreeGroup.reduce.red
theorem FreeGroup.reduce.red :
∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.Red L (FreeGroup.reduce L)
The theorem `FreeGroup.reduce.red` states that, for an arbitrary type `α` with decidable equality and any list `L` of pairs of elements from `α` and Boolean values, the reflexive-transitive closure of the `FreeGroup.Red.Step` relation (i.e., `FreeGroup.Red`) holds between `L` and its maximal reduction (i.e., `FreeGroup.reduce L`). Essentially, this means that any word can be reduced to its maximal reduction using the `FreeGroup.Red` relation.
More concisely: For any type `α` with decidable equality and list `L` of pairs of elements from `α` and Boolean values, the reflexive-transitive closure of the `FreeGroup.Red.Step` relation equals the reduction of `L` in the free group.
|
FreeGroup.Red.Step.length
theorem FreeGroup.Red.Step.length :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length
This theorem asserts that for any data type `α` and any two lists `L₁` and `L₂` of pairs of elements from `α` and boolean values, if list `L₁` can be reduced to list `L₂` in one step in the Free Group (i.e., there exist two intermediate words and a letter such that `L₁` is equivalent to the concatenation of the two words with the letter and its inverse, and `L₂` is equivalent to the concatenation of the two words), then the length of list `L₂` plus 2 equals the length of list `L₁`. This means that the reduction step in the Free Group removes two elements from the list.
More concisely: For any data type `α`, if two lists `L₁` and `L₂` of pairs `(α × bool)` can be connected by a single reduction step in the Free Group, then `length L₁ = length L₂ + 2`.
|
FreeAddGroup.Red.exact
theorem FreeAddGroup.Red.exact :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂
This theorem, `FreeAddGroup.Red.exact`, states that for any type `α` and any two lists `L₁` and `L₂` of pairs of elements from `α` and a Boolean, the canonical mapping of `L₁` to the free additive group on `α` is equal to the canonical mapping of `L₂` to the same free additive group if and only if `L₁` and `L₂` are related by the join of the reflexive-transitive closure of the reduction step relation in the free additive group. In other words, two lists are mapped to the same element in the free additive group if they can both be reduced to the same list through a sequence of reduction steps.
More concisely: The canonical mappings of two lists of pairs to the free additive group on a type `α` are equal if and only if the lists are related by the reduction step relation's reflexive-transitive closure.
|
FreeAddGroup.Red.Step.length
theorem FreeAddGroup.Red.Step.length :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length
The theorem `FreeAddGroup.Red.Step.length` states that for any type `α` and any two lists `L₁` and `L₂` of pairs of elements of `α` and Booleans, if `L₁` can be reduced to `L₂` in one step according to the rules of the free add group, then the length of `L₂` plus two is equal to the length of `L₁`. Here, a one-step reduction means that there exist two sublists `w₃` and `w₄` and a pair `(x, bool)` such that `L₁` is obtained by inserting `x` and its negation `-x` into `L₂` between `w₃` and `w₄`.
More concisely: For any lists `L₁` and `L₂` of pair-wise distinct elements and Booleans in a type `α`, if `L₁` can be obtained from `L₂` by inserting a pair `(x, bool)` between two sublists `w₃` and `w₄`, then the length of `L₁` equals the length of `L₂` plus two.
|
FreeGroup.reduce.min
theorem FreeGroup.reduce.min :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.Red (FreeGroup.reduce L₁) L₂ → FreeGroup.reduce L₁ = L₂
The theorem `FreeGroup.reduce.min` states that for any type `α` and for any lists `L₁` and `L₂` of pairs of elements of `α` and a boolean, if `α` has decidable equality, then if there is a reflexive-transitive closure of `Red.Step` (a reduction step) from the maximal reduction of `L₁` to `L₂`, the maximal reduction of `L₁` must be equal to `L₂`. In essence, this theorem characterizes the behavior of the `reduce` function in the `FreeGroup` context: the maximal reduction of a word can only reduce to the word itself.
More concisely: If `α` has decidable equality and there exists a reflexive-transitive closure of reduction steps from the maximal reduction of `L₁` to `L₂` in the free group on `α`, then `L₁` and `L₂` are equal.
|
FreeGroup.map.comp
theorem FreeGroup.map.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeGroup α),
(FreeGroup.map g) ((FreeGroup.map f) x) = (FreeGroup.map (g ∘ f)) x
This theorem states that for any three types `α`, `β`, and `γ` and any two functions `f : α → β` and `g : β → γ`, the composition of the group homomorphisms induced by the two functions is the same as the group homomorphism induced by the composition of the two functions, when applied to any element of the free group over `α`. In essence, this theorem ensures that the `FreeGroup.map` function respects the composition of functions, a property known in mathematics as functoriality.
More concisely: For any groups `α`, `β`, `γ`, and functions `f : α → β` and `g : β → γ`, the group homomorphism induced by their composition `g ∘ f` on the free group over `α` is equal to the composition of the homomorphisms induced by `f` and `g`.
|
FreeGroup.Red.singleton_iff
theorem FreeGroup.Red.singleton_iff :
∀ {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool}, FreeGroup.Red [x] L₁ ↔ L₁ = [x]
This theorem states that for any type `α`, any list `L₁` of pairs of `α` and `Bool`, and any pair `x` of `α` and `Bool`, the reflexive-transitive closure of `Red.Step` on `x` and `L₁` holds if and only if `L₁` is a list containing only `x`. In other words, a single element only reduces to itself in the context of the free group's reduction operation.
More concisely: For any type `α` and list `L₁` of pairs of `α` and `Bool`, the reflexive-transitive closure of `Red.Step` on the pair `(x, b)` and `L₁` holds if and only if `(x, b)` is in `L₁`.
|
FreeGroup.reduce.self
theorem FreeGroup.reduce.self :
∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.mk (FreeGroup.reduce L) = FreeGroup.mk L
This theorem states that for any type `α` and any list `L` of pairs consisting of elements from `α` and boolean values, given that `α` has decidable equality, the free group element represented by the maximal reduction of `L` is identical to the element represented by `L` itself. In other words, reducing a word to its maximal reduction in the free group (which is computable under decidable equality) does not change the free group element that the word represents.
More concisely: For any type `α` with decidable equality, the free group element represented by a list of pairs of `α` and booleans is equivalent to the element represented by the list itself.
|
FreeAddGroup.Red.cons_nil_iff_singleton
theorem FreeAddGroup.Red.cons_nil_iff_singleton :
∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool},
FreeAddGroup.Red ((x, b) :: L) [] ↔ FreeAddGroup.Red L [(x, !b)]
This theorem states that for any type `α`, any list `L` of tuples of `α` and `Bool`, any element `x` of type `α`, and any boolean `b`, if a letter `x` with a boolean `b` is prepended to the list `L` results in a list that reduces to an empty list under the Reflexive-transitive closure of `Red.Step`, then the list `L` itself reduces to a list containing a single tuple consisting of `x` and the negation of `b` under the same reduction relation. Essentially, if appending an element to a list results in an empty list after reduction, then the original list corresponds to the negation of that single element after reduction.
More concisely: If appending a tuple of `(x, b)` to a list `L` of tuples of `α` and `Bool` results in an empty list under Reflexive-transitive closure of `Red.Step`, then `L` is equal to the list containing `(x, ∨b.neg)` as an element.
|
FreeAddGroup.Red.church_rosser
theorem FreeAddGroup.Red.church_rosser :
∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ L₃ → Relation.Join FreeAddGroup.Red L₂ L₃
The **Church-Rosser theorem** for word reduction states that for any given type `α` and any three lists `L₁`, `L₂`, and `L₃` of pairs of elements from `α` and Boolean values, if `L₁` can be reduced to both `L₂` and `L₃` (in the sense of `FreeAddGroup.Red`), then there exists a list to which both `L₂` and `L₃` can be reduced to, according to the `Relation.Join` of `FreeAddGroup.Red`. This theorem is also known as Newman's diamond lemma, and it captures the notion of confluence in term rewriting systems, ensuring that different reduction paths can be reconciled.
More concisely: The Church-Rosser theorem for word reduction in Lean 4 asserts that for any type `α` and lists `L₁`, `L₂`, and `L₃` of pairs from `α` and Boolean values, if `L₁` can be reduced to both `L₂` and `L₃`, then there exists a common reduction result.
|
FreeAddGroup.reduce.idem
theorem FreeAddGroup.reduce.idem :
∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.reduce (FreeAddGroup.reduce L) = FreeAddGroup.reduce L
The theorem `FreeAddGroup.reduce.idem` asserts that the function `reduce`, from the `FreeAddGroup` structure, is idempotent for any type `α` with decidable equality and any list `L` of pairs of elements from `α` and boolean values. In other words, applying `reduce` twice on `L` yields the same result as applying `reduce` once. This is also equivalent to saying that the maximal reduction of the maximal reduction of a word is the same as the maximal reduction of the word itself.
More concisely: The idempotent function `reduce` in `FreeAddGroup` structure maintains maximal reduction of a list of pairs from a type with decidable equality.
|
FreeGroup.reduce.sound
theorem FreeGroup.reduce.sound :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.mk L₁ = FreeGroup.mk L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
The theorem `FreeGroup.reduce.sound` asserts that for any type `α` with decidable equality and any two lists of pairs of `α` and `Bool`, `L₁` and `L₂`, if these two lists correspond to the same element in the free group, then their maximal reductions are also the same. In other words, if `FreeGroup.mk L₁` is equal to `FreeGroup.mk L₂`, then `FreeGroup.reduce L₁` is equal to `FreeGroup.reduce L₂`. This theorem serves as the proof that the function `FreeGroup.reduce`, which sends an element of the free group to its maximal reduction, is well-defined.
More concisely: If two lists of pairs from a type `α` with decidable equality represent the same element in the free group, then their maximal reductions are equal.
|
FreeGroup.Red.sublist
theorem FreeGroup.Red.sublist : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → L₂.Sublist L₁ := by
sorry
The theorem `FreeGroup.Red.sublist` states that for any type `α` and for any two lists `L₁` and `L₂` of pairs of `α` and `Bool`, if the list `L₁` reduces to the list `L₂` under the reflexive-transitive closure of the `FreeGroup.Red.Step` relation (denoted as `FreeGroup.Red`), then `L₂` is a sublist of `L₁`. This means that `L₂` can be obtained from `L₁` by deleting some elements, with the remaining elements retaining their original order.
More concisely: If two lists of pairs `L₁` and `L₂` of type `α × Bool` reduce to each other under the reflexive-transitive closure of `FreeGroup.Red.Step` in the FreeGroup algebra, then `L₂` is a sublist of `L₁`.
|
FreeAddGroup.negRev_negRev
theorem FreeAddGroup.negRev_negRev :
∀ {α : Type u} {L₁ : List (α × Bool)}, FreeAddGroup.negRev (FreeAddGroup.negRev L₁) = L₁
The theorem `FreeAddGroup.negRev_negRev` states that for any list `L₁` of pairs consisting of an element from an arbitrary type `α` and a boolean, the function `FreeAddGroup.negRev` is an involution. In other words, applying the function `FreeAddGroup.negRev` twice to `L₁` yields `L₁` itself. This function `FreeAddGroup.negRev` first negates the boolean in each pair, and then reverses the entire list, which essentially represents the negative of a free group element. So, the theorem asserts that the negative of the negative of any element in the free group is the element itself.
More concisely: For any list of pairs from an arbitrary type with boolean values, the function `FreeAddGroup.negRev` applying negation and list reversal twice results in the original list.
|
FreeGroup.ext_hom
theorem FreeGroup.ext_hom :
∀ {α : Type u} {G : Type u_1} [inst : Group G] (f g : FreeGroup α →* G),
(∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)) → f = g
This theorem states that for any type `α` and any group `G`, if two homomorphisms `f` and `g` from the free group over `α` to `G` are equal when applied to the generators of the free group (that is, the elements obtained via the `FreeGroup.of` function), then these two homomorphisms are actually identical. This is a statement about the uniqueness of homomorphisms out of free groups in terms of their behavior on generators.
More concisely: If two homomorphisms from the free group over a type to a group agree on the generators, then they are equal.
|
FreeAddGroup.reduce.min
theorem FreeAddGroup.reduce.min :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.Red (FreeAddGroup.reduce L₁) L₂ → FreeAddGroup.reduce L₁ = L₂
The theorem `FreeAddGroup.reduce.min` asserts that, for any type `α` with decidable equality and any lists `L₁` and `L₂` of pairs of elements from `α` and booleans, if `L₂` is reachable from the maximal reduction of `L₁` via the reflexive-transitive closure of the `Red.Step` relation, then the maximal reduction of `L₁` is indeed `L₂`. In other words, the maximal reduction of a word only reduces to itself within the context of the `FreeAddGroup.Red` relation.
More concisely: If `L₂` is reachable from the maximal reduction of list `L₁` of pairs of elements and booleans from a type `α` with decidable equality via the reflexive-transitive closure of the reduction step relation `Red.Step` in the free additive group, then the maximal reduction of `L₁` equals `L₂`.
|
FreeGroup.Red.inv_of_red_of_ne
theorem FreeGroup.Red.inv_of_red_of_ne :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
(x1, b1) ≠ (x2, b2) →
FreeGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂) → FreeGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
This theorem states that for any type `α` and any lists `L₁` and `L₂` of pairs of elements of `α` and booleans, and for any distinct pairs `(x1, b1)` and `(x2, b2)`, if the list `L₁` appended to `(x1, b1)` can be reduced to the list `L₂` appended to `(x2, b2)` via the reflexive-transitive closure of the reduction relation `Red.Step`, then the list `L₁` can also be reduced to the list `L₂` appended to `(x2, b2)` and the inverse of `(x1, b1)`, i.e., `(x1, not b1)`, using the same reduction relation. Here, a "reduction" is a sequence of steps where each step is a valid `Red.Step` move.
More concisely: If `(x1, b1)` and `(x2, b2)` are distinct pairs, and `L₁` can be transformed into `L₂` via the reflexive-transitive closure of `Red.Step` with an additional step adding `(x2, b2)` and removing `(x1, b1)` or its inverse, then `L₁` can be transformed into `L₂` with `(x2, b2)` using `Red.Step`.
|
FreeAddGroup.reduce.exact
theorem FreeAddGroup.reduce.exact :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂ → FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂
This theorem is stating that for any type `α` with decidable equality and any two lists of pairs `L₁` and `L₂` of type `α` and `Bool`, if the maximal reduction of `L₁` and `L₂` (as defined by `FreeAddGroup.reduce`) are equal, then the elements corresponding to `L₁` and `L₂` in the free additive group on `α` (as defined by `FreeAddGroup.mk`) are also equal. In other words, common maximal reduction of two words implies that they represent the same element in the free additive group on `α`.
More concisely: If two lists of pairs over a type `α` with decidable equality have equal maximal reductions under `FreeAddGroup.reduce`, then the corresponding elements in the free additive group on `α` (as defined by `FreeAddGroup.mk`) are equal.
|
FreeAddGroup.negRev_involutive
theorem FreeAddGroup.negRev_involutive : ∀ {α : Type u}, Function.Involutive FreeAddGroup.negRev
The theorem `FreeAddGroup.negRev_involutive` asserts that for any type `α`, the function `FreeAddGroup.negRev` is involutive. In other words, applying the `FreeAddGroup.negRev` function twice to any list of pairs in `α × Bool` (representing elements of a free group) will return the original list. This means that `FreeAddGroup.negRev` is its own inverse: reversing the list and negating the booleans in the list, and then doing the same operation again, brings you back to where you started.
More concisely: The map `FreeAddGroup.negRev` on lists of pairs in `α × Bool` is an involution.
|
FreeAddGroup.Red.neg_of_red_of_ne
theorem FreeAddGroup.Red.neg_of_red_of_ne :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
(x1, b1) ≠ (x2, b2) →
FreeAddGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂) → FreeAddGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
This theorem states that for any type `α` and given two lists `L₁` and `L₂` of pairs of elements of `α` and Booleans, and two pairs `(x1, b1)` and `(x2, b2)` such that `(x1, b1)` is not equal to `(x2, b2)`, if the list that starts with `(x1, b1)` and continues with `L₁` can be reduced to the list that starts with `(x2, b2)` and continues with `L₂` (according to the reflexivity-transitivity closure of the `Red.Step` relation), then `L₁` can be reduced to the list that starts with `(x1, !b1)`, continues with `(x2, b2)`, and ends with `L₂`. In simpler terms, if a word formed by appending `x` and `w₁` can be reduced to a word formed by appending `y` and `w₂`, where `x` and `y` are distinct letters, then `w₁` can be reduced to a word formed by appending `-x`, `y`, and `w₂`.
More concisely: If `(x1, b1)` is distinct from `(x2, b2)` and `[(x1, b1)] ++ L₁` can be reduced to `[(x2, b2)] ++ L₂` in the reflexivity-transitivity closure of the `Red.Step` relation, then `L₁` can be reduced to `[(x1, !b1)] ++ [(x2, b2)] ++ L₂`.
|
FreeAddGroup.reduce.eq_of_red
theorem FreeAddGroup.reduce.eq_of_red :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
The theorem `FreeAddGroup.reduce.eq_of_red` states that for any type `α` with decidable equality and any two lists `L₁` and `L₂` consisting of pairs of elements of `α` and boolean values, if there exists a reflexive-transitive closure of the `Red.Step` relation between `L₁` and `L₂` (in other words, if `L₁` can be reduced to `L₂`), then the maximal reduction of `L₁` is equal to the maximal reduction of `L₂`. In simpler terms, this theorem indicates that if a word can be reduced to another word, then their respective maximal reductions are equivalent.
More concisely: If `L₁` can be reduced to `L₂` via a series of `Red.Step` operations, then the maximal reduction of `L₁` equals the maximal reduction of `L₂`.
|
FreeAddGroup.reduce.red
theorem FreeAddGroup.reduce.red :
∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α], FreeAddGroup.Red L (FreeAddGroup.reduce L)
This theorem characterizes the `reduce` function in the `FreeAddGroup` context. It states that for any type `α` with a decidable equality and any list `L` of pairs of elements from `α` and boolean values, there is a reflexive-transitive reduction from `L` to its maximally reduced form as computed by the `reduce` function. In other words, given a "word" (represented as a list of pairs of elements and booleans), the `reduce` function will transform this word to its maximally reduced form following the reflexive and transitive property.
More concisely: For any decidably equal type α and list L of pairs of elements from α with boolean values, the `reduce` function in the `FreeAddGroup` context produces the reflexive-transitive closure of L.
|
FreeGroup.Red.Step.to_red
theorem FreeGroup.Red.Step.to_red :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red L₁ L₂
This theorem states that for all types `α` and lists `L₁` and `L₂` of pairs of `α` and `Bool`, if there is a single step reduction (`FreeGroup.Red.Step`) from `L₁` to `L₂`, then `L₁` and `L₂` are related by the reflexive-transitive closure of the single step reduction relation (`FreeGroup.Red`). This implies that a single step reduction is considered part of the broader `FreeGroup.Red` relation, which includes both single step reductions and sequences of such reductions.
More concisely: If there exists a single step reduction from list `L₁` to list `L₂` of pairs of type `α` and `Bool` in the free group, then `L₁` and `L₂` are related in the reflexive-transitive closure of the free group reduction relation.
|
FreeGroup.reduce.rev
theorem FreeGroup.reduce.rev :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ (FreeGroup.reduce L₁)
The theorem `FreeGroup.reduce.rev` states that for any type `α` with decidable equality and any two lists of pairs of `α` and `Bool` (denoted `L₁` and `L₂`), if `L₁` reduces to `L₂` via the reflexive-transitive closure of `Red.Step` (represented here as `FreeGroup.Red`), then `L₂` can be reduced to the maximal reduction of `L₁` via the same process. In the context of free groups, these lists represent words and the reduction process represents simplification by eliminating inverse pairs.
More concisely: In the context of free groups with decidable equality, if two lists of pairs of group elements and boolean values reduce to each other via the reflexive-transitive closure of the reduction relation, then they can be reduced to the same maximal reduction.
|
FreeAddGroup.map.comp
theorem FreeAddGroup.map.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeAddGroup α),
(FreeAddGroup.map g) ((FreeAddGroup.map f) x) = (FreeAddGroup.map (g ∘ f)) x
This theorem states that for any three types `α`, `β`, and `γ`, and any two functions `f` from `α` to `β` and `g` from `β` to `γ`, the composition of the two functions `g ∘ f` (meaning first apply `f`, then apply `g` to the result) behaves the same as first mapping with `f` and then mapping the result with `g`, for any element `x` of the free additive group over `α`. In other words, the `FreeAddGroup.map` function respects function composition, making it a functor in the category theory sense.
More concisely: For any functions `f: α → β` and `g: β → γ`, the function composition `g ∘ f` equals the function `FreeAddGroup.map g ∘ FreeAddGroup.map f` when mapping elements of the free additive group over `α`.
|
FreeAddGroup.Red.nil_iff
theorem FreeAddGroup.Red.nil_iff : ∀ {α : Type u} {L : List (α × Bool)}, FreeAddGroup.Red [] L ↔ L = []
This theorem states that for any type `α` and any list `L` of pairs of elements from `α` and boolean values, the reflexive-transitive closure of the `FreeAddGroup.Red.Step` relation from the empty list to `L` holds if and only if `L` is the empty list. In other words, the empty word (or list) can only reduce to itself according to the rules of the `FreeAddGroup.Red.Step` relation in the context of free add groups.
More concisely: The empty list of pairs in a free add group is the only list that can be reflexively-transitively closed with respect to the `FreeAddGroup.Red.Step` relation.
|
FreeGroup.reduce.exact
theorem FreeGroup.reduce.exact :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.reduce L₁ = FreeGroup.reduce L₂ → FreeGroup.mk L₁ = FreeGroup.mk L₂
This theorem states that given any type `α` with a decidable equality and two lists of pairs of `α` and Boolean (`α × Bool`), `L₁` and `L₂`, if the maximal reductions of these two lists (as computed by the `FreeGroup.reduce` function) are equal, then the elements they correspond to in the free group on `α` (as computed by the `FreeGroup.mk` function) are also equal. In other words, if two words can be reduced to the same form, they represent the same element in the free group.
More concisely: If two lists of pairs from a type `α` with decidable equality to Boolean, `L₁` and `L₂`, have equal maximal reductions computed by `FreeGroup.reduce`, then the corresponding elements in the free group on `α` (as computed by `FreeGroup.mk`) are equal.
|
FreeGroup.lift.unique
theorem FreeGroup.lift.unique :
∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β} (g : FreeGroup α →* β),
(∀ (x : α), g (FreeGroup.of x) = f x) → ∀ {x : FreeGroup α}, g x = (FreeGroup.lift f) x
The theorem `FreeGroup.lift.unique` states that for all types `α` and `β`, where `β` is a group, and for all functions `f` from `α` to `β`, if we have a group homomorphism `g` from the free group over `α` to `β` such that for every element `x` of type `α`, `g` applied to the canonical injection of `x` into the free group equals `f` of `x`, then `g` applied to any element of the free group over `α` equals the unique group homomorphism from the free group over `α` to `β` that extends `f`. In other words, any group homomorphism from a free group to a group that respects the original function `f` from which the free group was created is necessarily the unique homomorphism that extends `f`.
More concisely: Given a group `β`, any group homomorphism from the free group over `α` to `β` that agrees with a given function `f : α → β` on the generators of the free group is the unique such homomorphism.
|
FreeAddGroup.Red.sublist
theorem FreeAddGroup.Red.sublist : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red L₁ L₂ → L₂.Sublist L₁
This theorem states that for any type `α` and any two lists `L₁` and `L₂` of pairs of `α` and `Bool`, if `L₁` reduces to `L₂` according to the reflexive-transitive closure of the `FreeAddGroup.Red.Step` relation (`FreeAddGroup.Red`), then `L₂` is a sublist of `L₁`. In other words, if we can get from `L₁` to `L₂` by a series of reduction steps, then all the elements of `L₂` will be found in `L₁` in the same order, but possibly with additional elements in between.
More concisely: If two lists of pairs `L₁` and `L₂` reduce to each other via the reflexive-transitive closure of the `FreeAddGroup.Red.Step` relation in Lean 4, then `L₂` is a sublist of `L₁`.
|
FreeGroup.freeAddGroup.red.reduce_eq
theorem FreeGroup.freeAddGroup.red.reduce_eq :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.Red L₁ L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
This theorem, titled as an "Alias of `FreeAddGroup.reduce.eq_of_red`", states that for a given type `α` with decidable equality and two lists `L₁` and `L₂` of pairs consisting of elements of type `α` and a boolean, if one list can be transformed into the other through the reflexive-transitive closure of the `FreeAddGroup.Red.Step` relation, then they both reduce to the same maximal reduction under the `FreeAddGroup.reduce` function. In simple terms, if one word changes into another word following certain steps, they will share a common maximal reduction.
More concisely: If two lists of pairs over a type with decidable equality can be transformed into each other through the reflexive-transitive closure of `FreeAddGroup.Red.Step`, then their maximal reductions under `FreeAddGroup.reduce` are equal.
|
FreeGroup.Red.nil_iff
theorem FreeGroup.Red.nil_iff : ∀ {α : Type u} {L : List (α × Bool)}, FreeGroup.Red [] L ↔ L = []
This theorem states that for any type `α` and any list `L` of pairs of `α` and `Bool`, `FreeGroup.Red [] L` is true if and only if `L` is an empty list. In other words, the reflexive-transitive closure of the `FreeGroup.Red.Step` relation, when applied to the empty list, only reduces to itself. This means an empty word in the context of free groups only reduces to itself.
More concisely: The empty list of pairings between a type `α` and `Bool` reduces to itself and only under the reflexive-transitive closure of the `FreeGroup.Red.Step` relation.
|
FreeAddGroup.ext_hom
theorem FreeAddGroup.ext_hom :
∀ {α : Type u} {G : Type u_1} [inst : AddGroup G] (f g : FreeAddGroup α →+ G),
(∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)) → f = g
This theorem states that for a given type `α` and an additive group `G`, two homomorphisms (`f` and `g`) from the free additive group over `α` to `G` are equal if they yield the same results when applied to the generators of the free additive group (i.e., individual elements of `α`). This is a specific case of an extensionality lemma, which are principles stating that functions with equal outputs for equal inputs are themselves equal.
More concisely: If two homomorphisms from the free additive group over a type `α` to an additive group `G` agree on all generators of the free group, then they are equal.
|
FreeGroup.invRev_invRev
theorem FreeGroup.invRev_invRev : ∀ {α : Type u} {L₁ : List (α × Bool)}, FreeGroup.invRev (FreeGroup.invRev L₁) = L₁
This theorem states that for all types `α` and all lists `L₁` of pairs of `α` and `Bool`, applying the function `FreeGroup.invRev` twice returns the original list. In other words, the function `FreeGroup.invRev` is its own inverse. This function, which transforms a word representing a free group element into a word representing its inverse, is an involution: applying it twice gives the original word back.
More concisely: For all types `α` and lists `L₁` of pairs `(α, bool)`, the function `FreeGroup.invRev` applied twice to `L₁` equals `L₁`.
|
FreeAddGroup.toWord_injective
theorem FreeAddGroup.toWord_injective : ∀ {α : Type u} [inst : DecidableEq α], Function.Injective FreeAddGroup.toWord
The theorem `FreeAddGroup.toWord_injective` states that for all types `α` with decidable equality, the function `FreeAddGroup.toWord` is injective. In other words, for any two elements of the additive free group, if their maximal reductions (computed by `FreeAddGroup.toWord`) are equal, then the two original elements themselves must be equal. This property is essential in situations where we need to ensure that different elements map to different reductions, thus preserving uniqueness.
More concisely: The function `FreeAddGroup.toWord` from the additive free group to its quotient by the equivalence relation of commutativity and associativity maps equal elements to equal words.
|
FreeGroup.reduce.idem
theorem FreeGroup.reduce.idem :
∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.reduce (FreeGroup.reduce L) = FreeGroup.reduce L
The theorem `FreeGroup.reduce.idem` states that the `reduce` function for a `FreeGroup` is idempotent. In other words, applying the `reduce` function twice on a list `L` of pairs consisting of an element of type `α` and a boolean, under the condition that `α` has decidable equality, will yield the same result as applying the `reduce` function once. This means that the maximal reduction of the maximal reduction of a word is equivalent to the maximal reduction of the word itself.
More concisely: The `reduce` function for a `FreeGroup` over a decidably equated type `α` is idempotent, i.e., applying it twice to a list of pairs `(α × bool)` yields the same result as applying it once.
|
FreeGroup.invRev_involutive
theorem FreeGroup.invRev_involutive : ∀ {α : Type u}, Function.Involutive FreeGroup.invRev
The theorem `FreeGroup.invRev_involutive` states that for all types `α`, the function `FreeGroup.invRev` is involutive. In other words, applying `FreeGroup.invRev` twice to any list of pairs of elements from type `α` and boolean values will return the original list. This means that `FreeGroup.invRev` is its own inverse function.
More concisely: The function `FreeGroup.invRev` on lists of pairs from type `α` and boolean values is self-inverse.
|
FreeAddGroup.reduce.sound
theorem FreeAddGroup.reduce.sound :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
The theorem `FreeAddGroup.reduce.sound` states that for any type `α` with decidable equality and any two lists of pairs `(α × Bool)`, `L₁` and `L₂`, if the two lists correspond to the same element in the free additive group, then they have a common maximal reduction. This theorem establishes the well-definedness of the function that maps an element of the free group to its maximal reduction. In other words, two words in the free additive group, despite potentially having different representations (`L₁` and `L₂`), will share the same simplified or 'reduced' form if they represent the same group element.
More concisely: Given two lists of pairs `(α × Bool)` representing elements in the free additive group with decidable equality, if they represent the same group element, then they have a common maximal reduction.
|
FreeAddGroup.of_injective
theorem FreeAddGroup.of_injective : ∀ {α : Type u}, Function.Injective FreeAddGroup.of
This theorem states that the canonical map from a type to the additive free group over that type is injective. In other words, if `FreeAddGroup.of x` equals `FreeAddGroup.of y` then `x` must be equal to `y`. The canonical map is defined by the function `FreeAddGroup.of` which sends each element from a type to the equivalence class of the letter that is the element in the free additive group over that type.
More concisely: The canonical map from any type to its additive free group is an injection.
|
FreeAddGroup.Red.singleton_iff
theorem FreeAddGroup.Red.singleton_iff :
∀ {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool}, FreeAddGroup.Red [x] L₁ ↔ L₁ = [x]
The theorem `FreeAddGroup.Red.singleton_iff` is stating that for any type `α`, any list `L₁` of tuples of `α` and `Bool`, and any tuple `x` of `α` and `Bool`, the reflexive-transitive closure of the `Red.Step` relation (`FreeAddGroup.Red`) applied to a list containing only `x` and `L₁` is equivalent to `L₁` being a list containing only `x`. In plain language, this means that a single "letter" (a tuple of `α` and `Bool`) can only reduce to itself in the reflexive-transitive closure of the `Red.Step` relation.
More concisely: For any type `α` and any list `L` of tuples of `α` and `Bool`, the reflexive-transitive closure of the `Red.Step` relation on the list `[x, h] :: L` equals `[x]` if and only if `[x, h]` is in `L`.
|
FreeGroup.of_injective
theorem FreeGroup.of_injective : ∀ {α : Type u}, Function.Injective FreeGroup.of
This theorem states that the canonical map from a certain type to the free group over that type is injective. In other words, the function `FreeGroup.of` has a property such that for any two elements `x` and `y` of the type `α`, if `FreeGroup.of x` equals `FreeGroup.of y`, then `x` must equal `y`. This function `FreeGroup.of` works by mapping each element of the type to an equivalence class of the letter that represents the element in the free group over the type.
More concisely: The `FreeGroup.of` function mapping each element of type `α` to its corresponding free group element is an injection.
|
FreeGroup.Red.cons_cons
theorem FreeGroup.Red.cons_cons :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool}, FreeGroup.Red L₁ L₂ → FreeGroup.Red (p :: L₁) (p :: L₂)
The theorem `FreeGroup.Red.cons_cons` states that for any type `α` and any pair `p` of type `α × Bool`, if there is a reflexive-transitive closure of the `Red.Step` relation (denoted by `FreeGroup.Red`) from list `L₁` to list `L₂`, then there is also a reflexive-transitive closure of the `Red.Step` relation from the list formed by consing `p` onto `L₁` to the list formed by consing `p` onto `L₂`. This essentially means that if `L₁` can be transformed into `L₂` by a series of steps, then the same series of steps can transform `p :: L₁` into `p :: L₂`.
More concisely: If `FreeGroup.Red` connects lists `L₁` and `L₂`, then it also connects the lists `[p] :: L₁` and `[p] :: L₂` for any pair `p` of type `α × Bool`.
|
FreeGroup.Red.exact
theorem FreeGroup.Red.exact :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.mk L₁ = FreeGroup.mk L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂
This theorem, named `FreeGroup.Red.exact`, is about free groups and certain relations between them. For every type `α` and any two lists `L₁` and `L₂` of pairs of `α` and `Bool`, it states that the canonical map to the free group on `α` (denoted by `FreeGroup.mk`) applied to `L₁` is equal to `FreeGroup.mk` applied to `L₂` if and only if `L₁` and `L₂` are related by the join of the reflexive-transitive closure of `Red.Step` (denoted by `Relation.Join FreeGroup.Red`). In other words, two lists are identified in the free group if and only if there exists a common list they can both be transformed into by series of `Red.Step` operations.
More concisely: For any type `α` and lists `L₁` and `L₂` of pairs of `α` and `Bool`, the canonical maps from `L₁` and `L₂` to the free group on `α` are equal if and only if `L₁` and `L₂` are related by the reflexive-transitive closure of `Red.Step` in the free group on `α`.
|
FreeGroup.red.reduce_eq
theorem FreeGroup.red.reduce_eq :
∀ {α : Type u} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
FreeGroup.Red L₁ L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
The theorem `FreeGroup.red.reduce_eq` states that for any type `α` with decidable equality, and for any two lists `L₁` and `L₂` consisting of pairs of elements of `α` and a Boolean, if the relation `FreeGroup.Red` holds between `L₁` and `L₂` (meaning that `L₁` can be transformed into `L₂` through a series of `Red.Step`s), then the maximal reductions of `L₁` and `L₂` (obtained through `FreeGroup.reduce`) are equal. In other words, if a word (represented as a list of pairs) can be transformed into another word through a series of single-step reductions, then the two words share a common maximally reduced word.
More concisely: If `α` has decidable equality and `L₁` and `L₂` are lists of pairs of elements from `α` and Booleans such that `FreeGroup.Red` holds between them, then the maximal reductions of `L₁` and `L₂` are equal.
|