def Lean.Grind.AC.Seq.length : Seq → Nat

Equations

• (Lean.Grind.AC.Seq.var x_1).length = 1
• (Lean.Grind.AC.Seq.cons x_1 s).length = s.length + 1

def Lean.Grind.AC.Seq.isVar (s : Seq) : Bool

Returns true if s is a variable.

Equations

• (Lean.Grind.AC.Seq.var x_1).isVar = true
• x✝.isVar = false

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

Reverses the sequence

Equations

• (Lean.Grind.AC.Seq.var x_1).reverse = Lean.Grind.AC.Seq.var x_1
• (Lean.Grind.AC.Seq.cons x_1 s_1).reverse = Lean.Grind.AC.Seq.reverse.go✝ s_1 (Lean.Grind.AC.Seq.var x_1)

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

Equations

• s₁.compare s₂ = if s₁.length < s₂.length then Ordering.lt else if s₁.length > s₂.length then Ordering.gt else Lean.Grind.AC.Seq.compare.lex✝ s₁ s₂

instance Lean.Grind.AC.instOrdSeq_lean : Ord Seq

Equations

• Lean.Grind.AC.instOrdSeq_lean = { compare := Lean.Grind.AC.Seq.compare }

instance Lean.Grind.AC.instAppendSeq_lean : Append Seq

Equations

• Lean.Grind.AC.instAppendSeq_lean = { append := Lean.Grind.AC.Seq.concat }

def Lean.Grind.AC.instOfNatSeq_lean {n : Nat} : OfNat Seq n

Equations

• Lean.Grind.AC.instOfNatSeq_lean = { ofNat := Lean.Grind.AC.Seq.var n }

inductive Lean.Grind.AC.SubseqResult : Type

Result type for s₁.subseq s₂

• false : SubseqResult

  s₁ is not a subsequence of s₂

• exact : SubseqResult

  s₁ == s₂

• prefix (s : Seq) : SubseqResult

  s₁ ++ s == s₂

• suffix (s : Seq) : SubseqResult

  s ++ s₁ == s₂

• middle (p s : Seq) : SubseqResult

  p ++ s₁ ++ s == s₂

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

s₁.subseq s₂ checks whether s₁ is a subsequence of s₂

Equations

• One or more equations did not get rendered due to their size.
• s₁.subseq (Lean.Grind.AC.Seq.var x_1) = if (s₁ == Lean.Grind.AC.Seq.var x_1) = true then Lean.Grind.AC.SubseqResult.exact else Lean.Grind.AC.SubseqResult.false

inductive Lean.Grind.AC.SubsetResult : Type

Result type for s₁.subset s₂

• false : SubsetResult

  s₁ is not a subset of s₂

• exact : SubsetResult

  s₁ == s₂

• strict (s : Seq) : SubsetResult

  s₁.union s == s₂

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

s₁.subset s₂ checks whether s₁ is a subset of s₂. It assumes s₁ and s₂ are sorted.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Grind.AC.Seq.var x).subset (Lean.Grind.AC.Seq.var y) = if (x == y) = true then Lean.Grind.AC.SubsetResult.exact else Lean.Grind.AC.SubsetResult.false
• (Lean.Grind.AC.Seq.cons x s).subset (Lean.Grind.AC.Seq.var x_1) = Lean.Grind.AC.SubsetResult.false

def Lean.Grind.AC.Seq.isSorted (s : Seq) : Bool

Equations

• (Lean.Grind.AC.Seq.var x_1).isSorted = true
• (Lean.Grind.AC.Seq.cons x_1 s_1).isSorted = Lean.Grind.AC.Seq.isSorted.go✝ x_1 s_1

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

Equations

• (Lean.Grind.AC.Seq.var x_2).contains x = (x == x_2)
• (Lean.Grind.AC.Seq.cons x_2 s_1).contains x = (x == x_2 || s_1.contains x)

def Lean.Grind.AC.Seq.noAdjacentDuplicates (s : Seq) : Bool

Equations

• (Lean.Grind.AC.Seq.var x_1).noAdjacentDuplicates = true
• (Lean.Grind.AC.Seq.cons x_1 s_1).noAdjacentDuplicates = Lean.Grind.AC.Seq.noAdjacentDuplicates.go✝ x_1 s_1

@[irreducible]

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

Returns true if s₁ and s₂ have at least one variable in common. The function assumes both of them are sorted.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Grind.AC.Seq.var x).sharesVar (Lean.Grind.AC.Seq.var y) = (x == y)
• (Lean.Grind.AC.Seq.var x).sharesVar (Lean.Grind.AC.Seq.cons y s) = (x == y || (Lean.Grind.AC.Seq.var x).sharesVar s)
• (Lean.Grind.AC.Seq.cons x s).sharesVar (Lean.Grind.AC.Seq.var x_1) = (x == x_1 || s.sharesVar (Lean.Grind.AC.Seq.var x_1))

def Lean.Grind.AC.toSeq? (xs : List Var) : Option Seq

Equations

• Lean.Grind.AC.toSeq? [] = none
• Lean.Grind.AC.toSeq? (x :: xs_2) = some (Lean.Grind.AC.toSeq?.go✝ xs_2 (Lean.Grind.AC.Seq.var x))

def Lean.Grind.AC.Seq.superposeAC? (s₁ s₂ : Seq) : Option (Seq × Seq × Seq)

Returns some (r₁, c, r₂) if s₁ == r₁.union c and s₂ == r₂.union c

It assumes s₁ and s₂ are sorted

Equations

• s₁.superposeAC? s₂ = Lean.Grind.AC.Seq.superposeAC?.go✝ s₁ s₂ none none none

def Lean.Grind.AC.Seq.superpose? (s₁ s₂ : Seq) : Option (Seq × Seq × Seq)

Returns some (p, c, s) if s₁ == p ++ c and s₂ == c ++ s

Equations

• (Lean.Grind.AC.Seq.var x_1).superpose? s₂ = none
• (Lean.Grind.AC.Seq.cons x_1 s).superpose? s₂ = Lean.Grind.AC.Seq.superpose?.go✝ s s₂ (Lean.Grind.AC.Seq.var x_1)

def Lean.Grind.AC.Seq.firstVar (s : Seq) : Var

Equations

• (Lean.Grind.AC.Seq.var x_1).firstVar = x_1
• (Lean.Grind.AC.Seq.cons x_1 s_1).firstVar = x_1

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

Equations

• (Lean.Grind.AC.Seq.var x_2).startsWithVar x = (x == x_2)
• (Lean.Grind.AC.Seq.cons x_2 s_1).startsWithVar x = (x == x_2)

def Lean.Grind.AC.Seq.lastVar (s : Seq) : Var

Equations

• (Lean.Grind.AC.Seq.var x_1).lastVar = x_1
• (Lean.Grind.AC.Seq.cons x_1 s_1).lastVar = s_1.lastVar

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

Equations

• (Lean.Grind.AC.Seq.var x_2).endsWithVar x = (x == x_2)
• (Lean.Grind.AC.Seq.cons x_2 s_1).endsWithVar x = s_1.endsWithVar x