equational_theories.Confluence1

source

def rw477.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw477.rule (y₁ ⋆ (x_1 ⋆ (y₂ ⋆ (y₃ ⋆ y₄)))) = if y₁ = y₂ ∧ y₁ = y₃ ∧ y₁ = y₄ then x_1 else y₁ ⋆ (x_1 ⋆ (y₂ ⋆ (y₃ ⋆ y₄)))
rw477.rule x✝ = x✝

Instances For

source

instance rw477.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw477.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw477.rule_yyy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ (y ⋆ y)) = y ⋆ (y ⋆ y)

source

@[simp]

theorem rw477.rule_xyyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (y ⋆ (y ⋆ y))) = x ⋆ (y ⋆ (y ⋆ y))

source

@[simp]

theorem rw477.rule_yxyyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ (y ⋆ (y ⋆ y)))) = x

source

theorem rw477.Facts :

∃ (G : Type) (x : Magma G), Equation477 G ∧ ¬Equation1426 G ∧ ¬Equation1519 G ∧ ¬Equation2035 G ∧ ¬Equation2128 G ∧ ¬Equation3050 G ∧ ¬Equation3150 G

source

def rw467.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw467.rule (y₁ ⋆ (x_1 ⋆ (y₂ ⋆ (y₃ ⋆ y₄)))) = if y₁ = y₃ ∧ y₁ = y₄ ∧ x_1 = y₂ then x_1 else y₁ ⋆ (x_1 ⋆ (y₂ ⋆ (y₃ ⋆ y₄)))
rw467.rule x✝ = x✝

Instances For

source

instance rw467.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw467.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw467.rule_xyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (y ⋆ y)) = x ⋆ (y ⋆ y)

source

@[simp]

theorem rw467.rule_xxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (x ⋆ (y ⋆ y))) = x ⋆ (x ⋆ (y ⋆ y))

source

@[simp]

theorem rw467.rule_yxxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ (x ⋆ (y ⋆ y)))) = x

source

theorem rw467.Facts :

∃ (G : Type) (x : Magma G), Equation467 G ∧ ¬Equation2847 G

source

def rw504.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw504.rule (y₁ ⋆ (x_1 ⋆ (y₂ ⋆ (y₃ ⋆ y₄)))) = if y₁ = x_1 ∧ y₁ = y₃ ∧ y₁ = y₄ then y₂ else y₁ ⋆ (x_1 ⋆ (y₂ ⋆ (y₃ ⋆ y₄)))
rw504.rule x✝ = x✝

Instances For

source

instance rw504.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw504.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw504.rule_xyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (y ⋆ y)) = x ⋆ (y ⋆ y)

source

@[simp]

theorem rw504.rule_yxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ (y ⋆ y))) = y ⋆ (x ⋆ (y ⋆ y))

source

@[simp]

theorem rw504.rule_yyxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (y ⋆ (x ⋆ (y ⋆ y)))) = x

source

theorem rw504.Facts :

∃ (G : Type) (x : Magma G), Equation504 G ∧ ¬Equation817 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation1925 G

source

def rw1515.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw1515.rule (y₁ ⋆ y₂ ⋆ (x_1 ⋆ (x₁ ⋆ x₂))) = if y₁ = y₂ ∧ x_1 = x₁ ∧ x_1 = x₂ then x_1 else y₁ ⋆ y₂ ⋆ (x_1 ⋆ (x₁ ⋆ x₂))
rw1515.rule x✝ = x✝

Instances For

source

instance rw1515.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw1515.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw1515.rule_xyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (y ⋆ y)) = x ⋆ (y ⋆ y)

source

@[simp]

theorem rw1515.rule_yyxxx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ (x ⋆ (x ⋆ x))) = x

source

theorem rw1515.Facts :

∃ (G : Type) (x : Magma G), Equation1515 G ∧ ¬Equation4590 G

source

def rw2038.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw2038.rule (x_1 ⋆ x₁ ⋆ x₂ ⋆ (y₁ ⋆ y₂)) = if y₁ = y₂ ∧ x_1 = x₁ ∧ x_1 = x₂ then x_1 else x_1 ⋆ x₁ ⋆ x₂ ⋆ (y₁ ⋆ y₂)
rw2038.rule x✝ = x✝

Instances For

source

instance rw2038.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw2038.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw2038.rule_xyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x) = y ⋆ y ⋆ x

source

@[simp]

theorem rw2038.rule_xxxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ x ⋆ x ⋆ (y ⋆ y)) = x

source

theorem rw2038.Facts :

∃ (G : Type) (x : Magma G), Equation2038 G ∧ ¬Equation4270 G

source

def rw3140.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw3140.rule (y₁ ⋆ y₂ ⋆ x_1 ⋆ x₁ ⋆ y₃) = if y₁ = y₂ ∧ y₁ = y₃ ∧ x_1 = x₁ then x_1 else y₁ ⋆ y₂ ⋆ x_1 ⋆ x₁ ⋆ y₃
rw3140.rule x✝ = x✝

Instances For

source

instance rw3140.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw3140.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw3140.rule_yyx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x) = y ⋆ y ⋆ x

source

@[simp]

theorem rw3140.rule_yyxx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x ⋆ x) = y ⋆ y ⋆ x ⋆ x

source

@[simp]

theorem rw3140.rule_yyxxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x ⋆ x ⋆ y) = x

source

theorem rw3140.Facts :

∃ (G : Type) (x : Magma G), Equation3140 G ∧ ¬Equation614 G

source

def rw3143.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw3143.rule (y₁ ⋆ y₂ ⋆ x_1 ⋆ x₁ ⋆ y₃) = if y₁ = y₂ ∧ y₁ = x₁ ∧ y₁ = y₃ then x_1 else y₁ ⋆ y₂ ⋆ x_1 ⋆ x₁ ⋆ y₃
rw3143.rule x✝ = x✝

Instances For

source

instance rw3143.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw3143.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw3143.rule_yyx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x) = y ⋆ y ⋆ x

source

@[simp]

theorem rw3143.rule_yyxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x ⋆ y) = y ⋆ y ⋆ x ⋆ y

source

@[simp]

theorem rw3143.rule_yyxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x ⋆ y ⋆ y) = x

source

theorem rw3143.Facts :

∃ (G : Type) (x : Magma G), Equation3143 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2644 G

source

def rw3150.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw3150.rule (y₁ ⋆ y₂ ⋆ x_1 ⋆ x₁ ⋆ y₃) = if y₁ = y₂ ∧ y₁ = x_1 ∧ y₁ = y₃ then x₁ else y₁ ⋆ y₂ ⋆ x_1 ⋆ x₁ ⋆ y₃
rw3150.rule x✝ = x✝

Instances For

source

instance rw3150.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw3150.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw3150.rule_yyx {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y ⋆ y) = y ⋆ y ⋆ y

source

@[simp]

theorem rw3150.rule_yyyx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ y ⋆ x) = y ⋆ y ⋆ y ⋆ x

source

@[simp]

theorem rw3150.rule_yyyxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ y ⋆ x ⋆ y) = x

source

theorem rw3150.Facts :

∃ (G : Type) (x : Magma G), Equation3150 G ∧ ¬Equation411 G ∧ ¬Equation1426 G ∧ ¬Equation2035 G

source

def rw1110.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw1110.rule (y₁ ⋆ (y₂ ⋆ (x_1 ⋆ x₁) ⋆ y₃)) = if y₁ = y₂ ∧ y₁ = y₃ ∧ x_1 = x₁ then x_1 else y₁ ⋆ (y₂ ⋆ (x_1 ⋆ x₁) ⋆ y₃)
rw1110.rule x✝ = x✝

Instances For

source

instance rw1110.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw1110.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw1110.rule_yxx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ x)) = y ⋆ (x ⋆ x)

source

@[simp]

theorem rw1110.rule_yxxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ x) ⋆ y) = y ⋆ (x ⋆ x) ⋆ y

source

@[simp]

theorem rw1110.rule_yyxxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (y ⋆ (x ⋆ x) ⋆ y)) = x

source

theorem rw1110.Facts :

∃ (G : Type) (x : Magma G), Equation1110 G ∧ ¬Equation8 G ∧ ¬Equation411 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation3253 G ∧ ¬Equation3319 G ∧ ¬Equation3862 G ∧ ¬Equation3915 G

source

def rw1086.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw1086.rule (y₁ ⋆ (y₂ ⋆ (x_1 ⋆ x₁) ⋆ y₃)) = if y₁ = x_1 ∧ y₁ = x₁ ∧ y₁ = y₃ then y₂ else y₁ ⋆ (y₂ ⋆ (x_1 ⋆ x₁) ⋆ y₃)
rw1086.rule x✝ = x✝

Instances For

source

instance rw1086.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw1086.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw1086.rule_xyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (y ⋆ y)) = x ⋆ (y ⋆ y)

source

@[simp]

theorem rw1086.rule_xyyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ (y ⋆ y) ⋆ y) = x ⋆ (y ⋆ y) ⋆ y

source

@[simp]

theorem rw1086.rule_yxyyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ (y ⋆ y) ⋆ y)) = x

source

theorem rw1086.Facts :

∃ (G : Type) (x : Magma G), Equation1086 G ∧ ¬Equation1832 G ∧ ¬Equation1898 G ∧ ¬Equation2644 G ∧ ¬Equation2710 G

source

def rw2497.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw2497.rule (y₁ ⋆ (x_1 ⋆ x₁ ⋆ y₂) ⋆ y₃) = if y₁ = y₂ ∧ y₁ = y₃ ∧ x_1 = x₁ then x_1 else y₁ ⋆ (x_1 ⋆ x₁ ⋆ y₂) ⋆ y₃
rw2497.rule x✝ = x✝

Instances For

source

instance rw2497.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw2497.rule_xx {α : Type} [DecidableEq α] (x : FreeMagma α) :

rule (x ⋆ x) = x ⋆ x

source

@[simp]

theorem rw2497.rule_xxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (x ⋆ x ⋆ y) = x ⋆ x ⋆ y

source

@[simp]

theorem rw2497.rule_yxxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ x ⋆ y)) = y ⋆ (x ⋆ x ⋆ y)

source

@[simp]

theorem rw2497.rule_yxxyy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (x ⋆ x ⋆ y) ⋆ y) = x

source

theorem rw2497.Facts :

∃ (G : Type) (x : Magma G), Equation2497 G ∧ ¬Equation23 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation3050 G ∧ ¬Equation3456 G ∧ ¬Equation3522 G ∧ ¬Equation4065 G ∧ ¬Equation4118 G

source

def rw2541.rule {α : Type} [DecidableEq α] :

FreeMagma α → FreeMagma α

Equations

rw2541.rule (y₁ ⋆ (x_1 ⋆ x₁ ⋆ y₂) ⋆ y₃) = if y₁ = x_1 ∧ y₁ = x₁ ∧ y₁ = y₃ then y₂ else y₁ ⋆ (x_1 ⋆ x₁ ⋆ y₂) ⋆ y₃
rw2541.rule x✝ = x✝

Instances For

source

instance rw2541.rule_projection {α : Type} [DecidableEq α] :

FreeMagma.IsProj rule

source

@[simp]

theorem rw2541.rule_yy {α : Type} [DecidableEq α] (y : FreeMagma α) :

rule (y ⋆ y) = y ⋆ y

source

@[simp]

theorem rw2541.rule_yyx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ y ⋆ x) = y ⋆ y ⋆ x

source

@[simp]

theorem rw2541.rule_yyyx {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (y ⋆ y ⋆ x)) = y ⋆ (y ⋆ y ⋆ x)

source

@[simp]

theorem rw2541.rule_yyyxy {α : Type} [DecidableEq α] (x y : FreeMagma α) :

rule (y ⋆ (y ⋆ y ⋆ x) ⋆ y) = x

source

theorem rw2541.Facts :

∃ (G : Type) (x : Magma G), Equation2541 G ∧ ¬Equation817 G ∧ ¬Equation917 G ∧ ¬Equation1629 G ∧ ¬Equation1729 G