free_group.red.step

Reduction step: w * x * x⁻¹ * v ~> w * v

free_group.red

Reflexive-transitive closure of red.step

free_group.red.step.length

Predicate asserting that word w₁ can be reduced to w₂ in one step, i.e. there are words w₃ w₄ and letter x such that w₁ = w₃xx⁻¹w₄ and w₂ = w₃w₄

free_group.red.church_rosser

Church-Rosser theorem for word reduction: If w1 w2 w3 are words such that w1 reduces to w2 and w3 respectively, then there is a word w4 such that w2 and w3 reduce to w4 respectively.

free_group.red.nil_iff

The empty word [] only reduces to itself.

free_group.red.singleton_iff

A letter only reduces to itself.

free_group.red.cons_nil_iff_singleton

If x is a letter and w is a word such that xw reduces to the empty word, then w reduces to x⁻¹

free_group.red.inv_of_red_of_ne

If x and y are distinct letters and w₁ w₂ are words such that xw₁ reduces to yw₂, then w₁ reduces to x⁻¹yw₂.

free_group.red.sublist

If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

free_group

The free group over a type, i.e. the words formed by the elements of the type and their formal inverses, quotient by one step reduction.

free_group.of

of x is the canonical injection from the type to the free group over that type by sending each element to the equivalence class of the letter that is the element.

free_group.of.inj

The canonical injection from the type to the free group is an injection.

free_group.to_group

If β is a group, then any function from α to β extends uniquely to a group homomorphism from the free group over α to β

free_group.map

Any function from α to β extends uniquely to a group homomorphism from the free group ver α to the free group over β.

free_group.free_group_congr

Equivalent types give rise to equivalent free groups.

free_group.prod

If α is a group, then any function from α to α extends uniquely to a homomorphism from the free group over α to α. This is the multiplicative version of sum.

free_group.sum

If α is a group, then any function from α to α extends uniquely to a homomorphism from the free group over α to α. This is the additive version of prod.

free_group.reduce

The maximal reduction of a word. It is computable iff α has decidable equality.

free_group.reduce.red

The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

free_group.reduce.min

The second theorem that characterises the function reduce: the maximal reduction of a word only reduces to itself.

free_group.reduce.idem

reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

free_group.reduce.eq_of_red

If a word reduces to another word, then they have a common maximal reduction.

free_group.reduce.sound

If two words correspond to the same element in the free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.

free_group.reduce.exact

If two words have a common maximal reduction, then they correspond to the same element in the free group.

free_group.reduce.self

A word and its maximal reduction correspond to the same element of the free group.

free_group.reduce.rev

If words w₁ w₂ are such that w₁ reduces to w₂, then w₂ reduces to the maximal reduction of w₁.

free_group.to_word

The function that sends an element of the free group to its maximal reduction.

free_group.reduce.church_rosser

Constructive Church-Rosser theorem (compare church_rosser).

free_group.red.enum

A list containing every word that w₁ reduces to.