def treeConcat {α : Type u_1} (t : FreeMagma α) : List α

Equations

• treeConcat (Lf a) = [a]
• treeConcat (tl ⋆ tr) = treeConcat tl ++ treeConcat tr

def rightJoinTrees {α : Type u_1} (t1 t2 : FreeMagma α) : FreeMagma α

Equations

• rightJoinTrees (Lf a) t2 = Lf a ⋆ t2
• rightJoinTrees (tl ⋆ tr) t2 = tl ⋆ rightJoinTrees tr t2

def rightAssociateTree {α : Type u_1} (t : FreeMagma α) : FreeMagma α

Equations

• rightAssociateTree (Lf a) = Lf a
• rightAssociateTree (tl ⋆ tr) = rightJoinTrees (rightAssociateTree tl) (rightAssociateTree tr)

theorem AssocImpliesForkEquivRightJoin {α : Type u_1} {G : Type u_2} [Magma G] (assoc : Equation4512 G) (f : α → G) (tl tr : FreeMagma α) : tl ⋆ tr ⬝ f = rightJoinTrees tl tr ⬝ f

theorem AssocFullyRightAssociate {α : Type u_1} {G : Type u_2} [Magma G] (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α) : t ⬝ f = rightAssociateTree t ⬝ f

theorem Assoc4 {G : Type u_1} [Magma G] (assoc : Equation4512 G) (x y z w : G) : ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w))

Example usage of AssocFullyRightAssociate

inductive FreeSemigroup (α : Type u_1) : Type u_1

• Singleton: {α : Type u_1} → α → FreeSemigroup α
• Cons: {α : Type u_1} → α → FreeSemigroup α → FreeSemigroup α

def semigroupConcat {α : Type u_1} (s1 s2 : FreeSemigroup α) : FreeSemigroup α

Equations

• semigroupConcat (FreeSemigroup.Singleton a) s2 = FreeSemigroup.Cons a s2
• semigroupConcat (FreeSemigroup.Cons a s1tail) s2 = FreeSemigroup.Cons a (semigroupConcat s1tail s2)

instance instMagmaFreeSemigroup (α : Type u_1) : Magma (FreeSemigroup α)

Equations

• instMagmaFreeSemigroup α = { op := semigroupConcat }

theorem FreeSgrAssoc {α : Type} : Equation4512 (FreeSemigroup α)

def freeMagmaToFreeSgr {α : Type u_1} : FreeMagma α →◇ FreeSemigroup α

Equations

• freeMagmaToFreeSgr = { toFun := fun (t : FreeMagma α) => t ⬝ FreeSemigroup.Singleton, map_op' := ⋯ }

def evalInSgr {α : Type u_1} {G : Type u_2} [Magma G] (f : α → G) (ls : FreeSemigroup α) : G

Equations

• evalInSgr f (FreeSemigroup.Singleton a) = f a
• evalInSgr f (FreeSemigroup.Cons a s1tail) = f a ◇ evalInSgr f s1tail

def evalInSgrHom {α : Type u_1} {G : Type u_2} [Magma G] (assoc : Equation4512 G) (f : α → G) : FreeSemigroup α →◇ G

Equations

• evalInSgrHom assoc f = { toFun := evalInSgr f, map_op' := ⋯ }

theorem evalInSgrHom.mapper {α : Type u_1} {G : Type u_2} [Magma G] (assoc : Equation4512 G) (f : α → G) (ls1 ls2 : FreeSemigroup α) : evalInSgr f (ls1 ◇ ls2) = evalInSgr f ls1 ◇ evalInSgr f ls2

def foldFreeSemigroup {G : Type u_1} [Magma G] (ls : FreeSemigroup G) : G

Equations

• foldFreeSemigroup (FreeSemigroup.Singleton a) = a
• foldFreeSemigroup (FreeSemigroup.Cons a s1tail) = a ◇ foldFreeSemigroup s1tail

theorem AssocImpliesSgrProjFaithful {α : Type u_1} {G : Type u_2} [Magma G] (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α) : t ⬝ f = evalInSgr f (freeMagmaToFreeSgr t)

def insertSgrSorted {n : ℕ} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n)

Equations

• insertSgrSorted i (FreeSemigroup.Singleton j) = if i ≤ j then FreeSemigroup.Cons i (FreeSemigroup.Singleton j) else FreeSemigroup.Cons j (FreeSemigroup.Singleton i)
• insertSgrSorted i (FreeSemigroup.Cons j lstail) = if i ≤ j then FreeSemigroup.Cons i (FreeSemigroup.Cons j lstail) else FreeSemigroup.Cons j (FreeSemigroup.Cons i lstail)

def insertionSortSgr {n : ℕ} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n)

Equations

• insertionSortSgr (FreeSemigroup.Singleton j) = FreeSemigroup.Singleton j
• insertionSortSgr (FreeSemigroup.Cons j lstail) = insertSgrSorted j (insertionSortSgr lstail)

theorem CommSgrImpliesInsertSortedFaithful {n : ℕ} {G : Type u_1} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G) (i : Fin n) (ls : FreeSemigroup (Fin n)) : evalInSgr f (insertSgrSorted i ls) = f i ◇ evalInSgr f ls

theorem CommSgrImpliesInsertionSortFaithful {n : ℕ} {G : Type u_1} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G) (ls : FreeSemigroup (Fin n)) : evalInSgr f ls = evalInSgr f (insertionSortSgr ls)

def involutionReduce {α : Type u_1} [DecidableEq α] (ls : FreeSemigroup α) : FreeSemigroup α

Equations

• involutionReduce (FreeSemigroup.Singleton a) = FreeSemigroup.Singleton a
• involutionReduce (FreeSemigroup.Cons a (FreeSemigroup.Singleton b)) = FreeSemigroup.Cons a (FreeSemigroup.Singleton b)
• involutionReduce (FreeSemigroup.Cons a (FreeSemigroup.Cons b lstail)) = if a = b then involutionReduce lstail else FreeSemigroup.Cons a (involutionReduce (FreeSemigroup.Cons b lstail))

def InvolutiveImpliesInvolutionReduceFaithful {α : Type u_1} [DecidableEq α] {G : Type u_2} [Magma G] (ls : FreeSemigroup α) (invol : Equation16 G) (f : α → G) : evalInSgr f ls = evalInSgr f (involutionReduce ls)

Equations

• ⋯ = ⋯

def equation1571Reducer {n : ℕ} (t : FreeMagma (Fin (n + 1))) : FreeSemigroup (Fin (n + 1))

Equations

• equation1571Reducer t = involutionReduce (insertionSortSgr (freeMagmaToFreeSgr (t ⋆ (Lf (Fin.last n) ⋆ Lf (Fin.last n)))))

theorem AbGrpPow2ImpliesEquation1571ReducerFaithful {n : ℕ} {G : Type u_1} [Magma G] (t : FreeMagma (Fin (n + 1))) (f : Fin (n + 1) → G) (assoc : Equation4512 G) (comm : Equation43 G) (invol : Equation16 G) : t ⬝ f = evalInSgr f (equation1571Reducer t)