def rw481.rules.rule1.elim_not {α : Type} [DecidableEq α] (e✝ : FreeMagma α) : rw481.rules.rule1 e✝ = none ↔ ¬∃ (x : FreeMagma α) (y : FreeMagma α) (z : FreeMagma α), e✝ = y ⋆ (x ⋆ (y ⋆ (z ⋆ z)))

Equations

• ⋯ = ⋯

def rw481.rules.rule2 {α : Type} [DecidableEq α] : FreeMagma α → Option (FreeMagma α)

Equations

• rw481.rules.rule2 (z1 ⋆ z2 ⋆ (x_1 ⋆ (z3 ⋆ z4))) = if z1 = z2 ∧ z2 = z3 ∧ z3 = z4 then some x_1 else none
• rw481.rules.rule2 x = none

def rw481.rules.rule3.elim {α : Type} [DecidableEq α] [Inhabited α] (e✝ r✝ : FreeMagma α) : rw481.rules.rule3 e✝ = some r✝ ↔ ∃ (x : FreeMagma α), e✝ = x ⋆ x ∧ r✝ = default ⋆ default

Equations

• ⋯ = ⋯

def rw481.rules.eq1 {α : Type} [DecidableEq α] [Inhabited α] (x y z : FreeMagma α) : rw481.rules (y ⋆ (x ⋆ (y ⋆ (z ⋆ z)))) = x

Equations

• ⋯ = ⋯

def rw481.rules.eq2 {α : Type} [DecidableEq α] [Inhabited α] (x z : FreeMagma α) : rw481.rules (z ⋆ z ⋆ (x ⋆ (z ⋆ z))) = x

Equations

• ⋯ = ⋯

def rw481.rules.rule3.elim_not {α : Type} [DecidableEq α] [Inhabited α] (e✝ : FreeMagma α) : rw481.rules.rule3 e✝ = none ↔ ¬∃ (x : FreeMagma α), e✝ = x ⋆ x

Equations

• ⋯ = ⋯

def rw481.rules.elim {α : Type} [DecidableEq α] [Inhabited α] (e✝ r✝ : FreeMagma α) : rw481.rules e✝ = r✝ ↔ ((∃ (x : FreeMagma α) (y : FreeMagma α) (z : FreeMagma α), e✝ = y ⋆ (x ⋆ (y ⋆ (z ⋆ z))) ∧ r✝ = x) ∨ (∃ (x : FreeMagma α) (z : FreeMagma α), e✝ = z ⋆ z ⋆ (x ⋆ (z ⋆ z)) ∧ r✝ = x) ∨ ∃ (x : FreeMagma α), e✝ = x ⋆ x ∧ r✝ = default ⋆ default) ∨ e✝ = r✝ ∧ (¬∃ (x : FreeMagma α) (y : FreeMagma α) (z : FreeMagma α), e✝ = y ⋆ (x ⋆ (y ⋆ (z ⋆ z)))) ∧ (¬∃ (x : FreeMagma α) (z : FreeMagma α), e✝ = z ⋆ z ⋆ (x ⋆ (z ⋆ z))) ∧ ¬∃ (x : FreeMagma α), e✝ = x ⋆ x

Equations

• ⋯ = ⋯

def rw481.rules.rule2.elim {α : Type} [DecidableEq α] (e✝ r✝ : FreeMagma α) : rw481.rules.rule2 e✝ = some r✝ ↔ ∃ (x : FreeMagma α) (z : FreeMagma α), e✝ = z ⋆ z ⋆ (x ⋆ (z ⋆ z)) ∧ r✝ = x

Equations

• ⋯ = ⋯

def rw481.rules.rule1 {α : Type} [DecidableEq α] : FreeMagma α → Option (FreeMagma α)

Equations

• rw481.rules.rule1 (y1 ⋆ (x_1 ⋆ (y2 ⋆ (z1 ⋆ z2)))) = if y1 = y2 ∧ z1 = z2 then some x_1 else none
• rw481.rules.rule1 x = none

def rw481.rules {α : Type} [DecidableEq α] [Inhabited α] : FreeMagma α → FreeMagma α

Equations

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

def rw481.rules.rule1.elim {α : Type} [DecidableEq α] (e✝ r✝ : FreeMagma α) : rw481.rules.rule1 e✝ = some r✝ ↔ ∃ (x : FreeMagma α) (y : FreeMagma α) (z : FreeMagma α), e✝ = y ⋆ (x ⋆ (y ⋆ (z ⋆ z))) ∧ r✝ = x

Equations

• ⋯ = ⋯

def rw481.rules.rule2.elim_not {α : Type} [DecidableEq α] (e✝ : FreeMagma α) : rw481.rules.rule2 e✝ = none ↔ ¬∃ (x : FreeMagma α) (z : FreeMagma α), e✝ = z ⋆ z ⋆ (x ⋆ (z ⋆ z))

Equations

• ⋯ = ⋯

def rw481.rules.elim' {α : Type} [DecidableEq α] [Inhabited α] (e✝ r✝ : FreeMagma α) : rw481.rules e✝ = r✝ ↔ (rw481.rules.rule1 e✝ = some r✝ ∨ rw481.rules.rule2 e✝ = some r✝ ∨ rw481.rules.rule3 e✝ = some r✝) ∨ e✝ = r✝ ∧ rw481.rules.rule1 e✝ = none ∧ rw481.rules.rule2 e✝ = none ∧ rw481.rules.rule3 e✝ = none

Equations

• ⋯ = ⋯

def rw481.rules.eq3 {α : Type} [DecidableEq α] [Inhabited α] (x : FreeMagma α) : rw481.rules (x ⋆ x) = default ⋆ default

Equations

• ⋯ = ⋯

def rw481.rules.rule3 {α : Type} [DecidableEq α] [Inhabited α] : FreeMagma α → Option (FreeMagma α)

Equations

• rw481.rules.rule3 (x1 ⋆ x2) = if x1 = x2 then some (default ⋆ default) else none
• rw481.rules.rule3 x = none

instance rw481.instIsProjOrNFRules {α : Type} [DecidableEq α] [Inhabited α] : Confluence.IsProjOrNF rw481.rules

Equations

• ⋯ = ⋯

theorem rw481.comp1_2 {α : Type} [DecidableEq α] [Inhabited α] {x y : FreeMagma α} (hx : Confluence.NF rw481.rules x) : rw481.rules (y ⋆ rw481.rules (x ⋆ (y ⋆ (default ⋆ default)))) = x

theorem rw481.comp2_2 {α : Type} [DecidableEq α] [Inhabited α] {x : FreeMagma α} (hx : Confluence.NF rw481.rules x) : rw481.rules (default ⋆ default ⋆ rw481.rules (x ⋆ (default ⋆ default))) = x

theorem rw481.comp1_3 {α : Type} [DecidableEq α] [Inhabited α] {x y : FreeMagma α} (hx : Confluence.NF rw481.rules x) : rw481.rules (y ⋆ rw481.rules (x ⋆ rw481.rules (y ⋆ (default ⋆ default)))) = x

theorem rw481.comp1_4 {α : Type} [DecidableEq α] [Inhabited α] {x y z : FreeMagma α} (hx : Confluence.NF rw481.rules x) : rw481.rules (y ⋆ rw481.rules (x ⋆ rw481.rules (y ⋆ rw481.rules (z ⋆ z)))) = x

theorem rw481.Facts : ∃ (G : Type) (x : Magma G), Equation481 G ∧ ¬Equation1488 G ∧ ¬Equation1492 G ∧ ¬Equation1496 G ∧ ¬Equation2035 G ∧ ¬Equation2038 G ∧ ¬Equation2041 G ∧ ¬Equation2124 G ∧ ¬Equation2128 G ∧ ¬Equation2132 G ∧ ¬Equation2135 G ∧ ¬Equation3050 G ∧ ¬Equation3056 G ∧ ¬Equation3139 G ∧ ¬Equation3150 G ∧ ¬Equation3161 G