@[reducible, inline]

abbrev Lean.Grind.AC.Var : Type

structure Lean.Grind.AC.Context (α : Sort u) : Type u

• vars : RArray (PLift α)
• op : α → α → α

inductive Lean.Grind.AC.Expr : Type

• var (x : Var) : Expr
• op (lhs rhs : Expr) : Expr

instance Lean.Grind.AC.instInhabitedExpr : Inhabited Expr

def Lean.Grind.AC.instInhabitedExpr.default : Expr

instance Lean.Grind.AC.instReprExpr : Repr Expr

def Lean.Grind.AC.instReprExpr.repr : Expr → Nat → Std.Format

instance Lean.Grind.AC.instBEqExpr : BEq Expr

def Lean.Grind.AC.instBEqExpr.beq : Expr → Expr → Bool

@[reducible, inline]

noncomputable abbrev Lean.Grind.AC.Var.denote {α : Sort u} (ctx : Context α) (x : Var) : α

@[reducible, inline]

noncomputable abbrev Lean.Grind.AC.Expr.denote {α : Sort u_1} (ctx : Context α) (e : Expr) : α

theorem Lean.Grind.AC.Expr.denote_var {α : Sort u_1} (ctx : Context α) (x : Var) : denote ctx (var x) = Var.denote ctx x

theorem Lean.Grind.AC.Expr.denote_op {α : Sort u_1} (ctx : Context α) (a b : Expr) : denote ctx (a.op b) = ctx.op (denote ctx a) (denote ctx b)

inductive Lean.Grind.AC.Seq : Type

• var (x : Var) : Seq
• cons (x : Var) (s : Seq) : Seq

def Lean.Grind.AC.instInhabitedSeq.default : Seq

instance Lean.Grind.AC.instInhabitedSeq : Inhabited Seq

def Lean.Grind.AC.instReprSeq.repr : Seq → Nat → Std.Format

instance Lean.Grind.AC.instReprSeq : Repr Seq

def Lean.Grind.AC.instBEqSeq.beq : Seq → Seq → Bool

instance Lean.Grind.AC.instBEqSeq : BEq Seq

instance Lean.Grind.AC.instReflBEqSeq : ReflBEq Seq

instance Lean.Grind.AC.instLawfulBEqSeq : LawfulBEq Seq

noncomputable def Lean.Grind.AC.Seq.beq' (s₁ : Seq) : Seq → Bool

theorem Lean.Grind.AC.Seq.beq'_eq (s₁ s₂ : Seq) : (s₁.beq' s₂ = true) = (s₁ = s₂)

@[inline]

noncomputable abbrev Lean.Grind.AC.Seq.denote {α : Sort u_1} (ctx : Context α) (s : Seq) : α

theorem Lean.Grind.AC.Seq.denote_var {α : Sort u_1} (ctx : Context α) (x : Var) : denote ctx (var x) = Var.denote ctx x

theorem Lean.Grind.AC.Seq.denote_op {α : Sort u_1} (ctx : Context α) (x : Var) (s : Seq) : denote ctx (cons x s) = ctx.op (Var.denote ctx x) (denote ctx s)

def Lean.Grind.AC.Expr.toSeq' (e : Expr) (s : Seq) : Seq

noncomputable def Lean.Grind.AC.Expr.toSeq'_k (e : Expr) : Seq → Seq

theorem Lean.Grind.AC.Expr.toSeq'_k_eq_toSeq' (e : Expr) (s : Seq) : e.toSeq'_k s = e.toSeq' s

def Lean.Grind.AC.Expr.toSeq (e : Expr) : Seq

noncomputable def Lean.Grind.AC.Expr.toSeq_k (e : Expr) : Seq

theorem Lean.Grind.AC.Expr.toSeq_k_eq_toSeq (e : Expr) : e.toSeq_k = e.toSeq

theorem Lean.Grind.AC.Expr.denote_toSeq' {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (e : Expr) (s : Seq), Seq.denote ctx (e.toSeq' s) = ctx.op (denote ctx e) (Seq.denote ctx s)

theorem Lean.Grind.AC.Expr.denote_toSeq {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (e : Expr), Seq.denote ctx e.toSeq = denote ctx e

def Lean.Grind.AC.Seq.erase0 (s : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.erase0_k (s : Seq) : Seq

theorem Lean.Grind.AC.Seq.erase0_k_var (x : Var) : (var x).erase0_k = var x

theorem Lean.Grind.AC.Seq.erase0_k_cons (x : Var) (s : Seq) : (cons x s).erase0_k = Bool.rec (Bool.rec (cons x s.erase0_k) (var x) (s.erase0_k.beq' (var 0))) s.erase0_k (Nat.beq x 0)

theorem Lean.Grind.AC.Seq.erase0_k_eq_erase0 (s : Seq) : s.erase0_k = s.erase0

theorem Lean.Grind.AC.Seq.denote_erase0 {α : Sort u_1} (ctx : Context α) {inst : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (s : Seq) : denote ctx s.erase0 = denote ctx s

def Lean.Grind.AC.Seq.insert (x : Var) (s : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.insert_k (x : Var) (s : Seq) : Seq

theorem Lean.Grind.AC.Seq.insert_k_eq_insert (x : Var) (s : Seq) : insert_k x s = insert x s

theorem Lean.Grind.AC.Seq.denote_insert {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (x : Var) (s : Seq) : denote ctx (insert x s) = ctx.op (Var.denote ctx x) (denote ctx s)

def Lean.Grind.AC.Seq.sort' (s acc : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.sort'_k (s : Seq) : Seq → Seq

theorem Lean.Grind.AC.Seq.sort'_k_eq_sort' (s acc : Seq) : s.sort'_k acc = s.sort' acc

theorem Lean.Grind.AC.Seq.denote_sort' {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (s acc : Seq) : denote ctx (s.sort' acc) = ctx.op (denote ctx s) (denote ctx acc)

def Lean.Grind.AC.Seq.sort (s : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.sort_k (s : Seq) : Seq

theorem Lean.Grind.AC.Seq.sort_k_eq_sort (s : Seq) : s.sort_k = s.sort

theorem Lean.Grind.AC.Seq.denote_sort {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (s : Seq) : denote ctx s.sort = denote ctx s

def Lean.Grind.AC.Seq.eraseDup (s : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.eraseDup_k (s : Seq) : Seq

theorem Lean.Grind.AC.Seq.eraseDup_k_cons (x : Var) (s : Seq) : (cons x s).eraseDup_k = rec (fun (y : Var) => Bool.rec (cons x (var y)) (var x) (Nat.beq x y)) (fun (y : Var) (s' x_1 : Seq) => Bool.rec (cons x (cons y s')) (cons y s') (Nat.beq x y)) s.eraseDup_k

theorem Lean.Grind.AC.Seq.eraseDup_k_eq_eraseDup (s : Seq) : s.eraseDup_k = s.eraseDup

theorem Lean.Grind.AC.Seq.denote_eraseDup {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (s : Seq) : denote ctx s.eraseDup = denote ctx s

def Lean.Grind.AC.Seq.concat (s₁ s₂ : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.concat_k (s₁ : Seq) : Seq → Seq

theorem Lean.Grind.AC.Seq.concat_k_eq_concat (s₁ s₂ : Seq) : s₁.concat_k s₂ = s₁.concat s₂

theorem Lean.Grind.AC.Seq.denote_concat {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} (s₁ s₂ : Seq) : denote ctx (s₁.concat s₂) = ctx.op (denote ctx s₁) (denote ctx s₂)

theorem Lean.Grind.AC.eq_orient {α : Sort u_1} (ctx : Context α) (lhs rhs : Seq) : Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx rhs = Seq.denote ctx lhs

theorem Lean.Grind.AC.eq_simp_lhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₂ → Seq.denote ctx rhs₁ = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx lhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₁

theorem Lean.Grind.AC.diseq_simp_lhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx rhs₁ ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx lhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₁

noncomputable def Lean.Grind.AC.simp_prefix_cert (lhs rhs tail s s' : Seq) : Bool

theorem Lean.Grind.AC.eq_simp_lhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.simp_suffix_cert (lhs rhs head s s' : Seq) : Bool

theorem Lean.Grind.AC.eq_simp_lhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.simp_middle_cert (lhs rhs head tail s s' : Seq) : Bool

theorem Lean.Grind.AC.eq_simp_lhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.superpose_cert (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool

theorem Lean.Grind.AC.superpose {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : superpose_cert p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs = Seq.denote ctx rhs

Given lhs₁ = rhs₁ and lhs₂ = rhs₂ where lhs₁ := p * c and lhs₂ := c * s, lhs = rhs where lhs := rhs₁ * s and rhs := p * rhs₂

def Lean.Grind.AC.Seq.unionFuel (fuel : Nat) (s₁ s₂ : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.unionFuel_k (fuel : Nat) : Seq → Seq → Seq

theorem Lean.Grind.AC.Seq.unionFuel_k_eq_unionFuel (fuel : Nat) (s₁ s₂ : Seq) : unionFuel_k fuel s₁ s₂ = unionFuel fuel s₁ s₂

theorem Lean.Grind.AC.Seq.denote_unionFuel {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (fuel : Nat) (s₁ s₂ : Seq) : denote ctx (unionFuel fuel s₁ s₂) = ctx.op (denote ctx s₁) (denote ctx s₂)

def Lean.Grind.AC.hugeFuel : Nat

def Lean.Grind.AC.Seq.union (s₁ s₂ : Seq) : Seq

noncomputable def Lean.Grind.AC.Seq.union_k (s₁ s₂ : Seq) : Seq

theorem Lean.Grind.AC.Seq.union_k_eq_union (s₁ s₂ : Seq) : s₁.union_k s₂ = s₁.union s₂

theorem Lean.Grind.AC.Seq.denote_union {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (s₁ s₂ : Seq) : denote ctx (s₁.union s₂) = ctx.op (denote ctx s₁) (denote ctx s₂)

noncomputable def Lean.Grind.AC.simp_ac_cert (c lhs rhs s s' : Seq) : Bool

theorem Lean.Grind.AC.simp_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs rhs s s' : Seq) : simp_ac_cert c lhs rhs s s' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx s = Seq.denote ctx s'

Given lhs = rhs, and a term s := union a lhs, rewrite it to s' := union a rhs

theorem Lean.Grind.AC.eq_simp_lhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.superpose_ac_cert (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool

theorem Lean.Grind.AC.superpose_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : superpose_ac_cert r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs = Seq.denote ctx rhs

Given lhs₁ = rhs₁ and lhs₂ = rhs₂ where lhs₁ := union c r₁ and lhs₂ := union c r₂, lhs = rhs where lhs := union r₂ rhs₁ and rhs := union r₁ rhs₂

noncomputable def Lean.Grind.AC.Seq.contains_k (s : Seq) (x : Var) : Bool

theorem Lean.Grind.AC.Seq.contains_k_var (y x : Var) : (var y).contains_k x = (x == y)

theorem Lean.Grind.AC.Seq.contains_k_cons (y x : Var) (s : Seq) : (cons y s).contains_k x = (x == y || s.contains_k x)

theorem Lean.Grind.AC.Seq.denote_insert_of_contains {α : Sort u_1} (ctx : Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.Commutative ctx.op] [inst₃ : Std.IdempotentOp ctx.op] (s : Seq) (x : Var) : s.contains_k x = true → denote ctx (insert x s) = denote ctx s

noncomputable def Lean.Grind.AC.superpose_ac_idempotent_cert (x : Var) (lhs₁ rhs₁ rhs : Seq) : Bool

Remark: see Section 4.1 of the paper "MODULARITY, COMBINATION, AC CONGRUENCE CLOSURE" to understand why superpose_ac_idempotent is needed.

theorem Lean.Grind.AC.superpose_ac_idempotent {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} {inst₃ : Std.IdempotentOp ctx.op} (x : Var) (lhs₁ rhs₁ rhs : Seq) : superpose_ac_idempotent_cert x lhs₁ rhs₁ rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs

noncomputable def Lean.Grind.AC.Seq.startsWithVar_k (s : Seq) (x : Var) : Bool

theorem Lean.Grind.AC.Seq.startsWithVar_k_var (y x : Var) : (var y).startsWithVar_k x = (x == y)

theorem Lean.Grind.AC.Seq.startsWithVar_k_cons (y x : Var) (s : Seq) : (cons y s).startsWithVar_k x = (x == y)

theorem Lean.Grind.AC.Seq.denote_concat_of_startsWithVar {α : Sort u_1} (ctx : Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.IdempotentOp ctx.op] (s : Seq) (x : Var) : s.startsWithVar_k x = true → denote ctx ((var x).concat_k s) = denote ctx s

noncomputable def Lean.Grind.AC.superpose_head_idempotent_cert (x : Var) (lhs₁ rhs₁ rhs : Seq) : Bool

theorem Lean.Grind.AC.superpose_head_idempotent {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (x : Var) (lhs₁ rhs₁ rhs : Seq) : superpose_head_idempotent_cert x lhs₁ rhs₁ rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs

superpose_ac_idempotent for the non-commutative case. This is the "head"-case

noncomputable def Lean.Grind.AC.Seq.endsWithVar_k (s : Seq) (x : Var) : Bool

theorem Lean.Grind.AC.Seq.endsWithVar_k_var (y x : Var) : (var y).endsWithVar_k x = (x == y)

theorem Lean.Grind.AC.Seq.endsWithVar_k_cons (y x : Var) (s : Seq) : (cons y s).endsWithVar_k x = s.endsWithVar_k x

theorem Lean.Grind.AC.Seq.denote_concat_of_endsWithVar {α : Sort u_1} (ctx : Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.IdempotentOp ctx.op] (s : Seq) (x : Var) : s.endsWithVar_k x = true → denote ctx (s.concat_k (var x)) = denote ctx s

noncomputable def Lean.Grind.AC.superpose_tail_idempotent_cert (x : Var) (lhs₁ rhs₁ rhs : Seq) : Bool

theorem Lean.Grind.AC.superpose_tail_idempotent {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (x : Var) (lhs₁ rhs₁ rhs : Seq) : superpose_tail_idempotent_cert x lhs₁ rhs₁ rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs

superpose_ac_idempotent for the non-commutative case. It is similar to superpose_head_idempotent but for the "tail"-case

noncomputable def Lean.Grind.AC.eq_norm_a_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

theorem Lean.Grind.AC.eq_norm_a {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_a_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_norm_ac_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

theorem Lean.Grind.AC.eq_norm_ac {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ac_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_norm_ai_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

theorem Lean.Grind.AC.eq_norm_ai {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ai_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_norm_aci_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

theorem Lean.Grind.AC.eq_norm_aci {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} {x✝¹ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_aci_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_erase_dup_cert (lhs rhs lhs' rhs' : Seq) : Bool

theorem Lean.Grind.AC.eq_erase_dup {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.IdempotentOp ctx.op} (lhs rhs lhs' rhs' : Seq), eq_erase_dup_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_erase0_cert (lhs rhs lhs' rhs' : Seq) : Bool

theorem Lean.Grind.AC.eq_erase0 {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs lhs' rhs' : Seq), eq_erase0_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_a {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_a_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_ac {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ac_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_ai {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ai_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_aci {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} {x✝¹ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_aci_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_erase_dup {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.IdempotentOp ctx.op} (lhs rhs lhs' rhs' : Seq), eq_erase_dup_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs ≠ Seq.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_erase0 {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs lhs' rhs' : Seq), eq_erase0_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs ≠ Seq.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.diseq_unsat_cert (lhs rhs : Seq) : Bool

theorem Lean.Grind.AC.diseq_unsat {α : Sort u_1} (ctx : Context α) (lhs rhs : Seq) : diseq_unsat_cert lhs rhs = true → Seq.denote ctx lhs ≠ Seq.denote ctx rhs → False

theorem Lean.Grind.AC.norm_a {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (e : Expr) (s : Seq), e.toSeq.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.norm_ac {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} (e : Expr) (s : Seq), e.toSeq.sort.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.norm_ai {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (e : Expr) (s : Seq), e.toSeq.erase0.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.norm_aci {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} {x✝¹ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (e : Expr) (s : Seq), e.toSeq.erase0.sort.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.eq_erase0_rhs {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs rhs' : Seq), rhs.erase0.beq' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs = Seq.denote ctx rhs'

theorem Lean.Grind.AC.eq_erase_dup_rhs {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.IdempotentOp ctx.op} (lhs rhs rhs' : Seq), rhs.eraseDup.beq' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs = Seq.denote ctx rhs'

theorem Lean.Grind.AC.eq_expr_seq_seq {α : Sort u_1} (ctx : Context α) (e : Expr) (s₁ s₂ : Seq) : Expr.denote ctx e = Seq.denote ctx s₁ → Seq.denote ctx s₁ = Seq.denote ctx s₂ → Expr.denote ctx e = Seq.denote ctx s₂

theorem Lean.Grind.AC.imp_eq {α : Sort u_1} (ctx : Context α) (lhs rhs : Expr) (s : Seq) : Expr.denote ctx lhs = Seq.denote ctx s → Expr.denote ctx rhs = Seq.denote ctx s → Expr.denote ctx lhs = Expr.denote ctx rhs

theorem Lean.Grind.AC.refl {α : Sort u_1} (ctx : Context α) (s : Seq) : Seq.denote ctx s = Seq.denote ctx s