inductive Term (T : Sort u_1) (n : ℕ) : Sort (max 1 u_1)

• const {T : Sort u_1} {n : ℕ} : T → Term T n
• index {T : Sort u_1} {n : ℕ} : Fin n → Term T n
• add {T : Sort u_1} {n : ℕ} : Term T n → Term T n → Term T n
• sub {T : Sort u_1} {n : ℕ} : Term T n → Term T n → Term T n
• mul {T : Sort u_1} {n : ℕ} : Term T n → Term T n → Term T n

def Term.repr {T : Type} {n : ℕ} [Repr T] : Term T n → ℕ → Std.Format

Equations

• (Term.const a).repr x✝ = reprArg a
• (#k).repr x✝ = Std.Format.text "#" ++ reprArg k
• (t₁.add t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "+" ++ t₂.repr x✝) x✝
• (t₁.sub t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "-" ++ t₂.repr x✝) x✝
• (t₁.mul t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "*" ++ t₂.repr x✝) x✝

instance instReprTerm {α : Type} {n : ℕ} [Repr α] : Repr (Term α n)

Equations

• instReprTerm = { reprPrec := Term.repr }

def Term.castToAnnotatedTuple {T : Type} {n : ℕ} {K : Type u_1} (t : Term T n) : Term (T ⊕ K) (n + 1)

Equations

• (Term.const c).castToAnnotatedTuple = Term.const (Sum.inl c)
• (#k).castToAnnotatedTuple = #(k.castLT ⋯)
• (t₁.add t₂).castToAnnotatedTuple = t₁.castToAnnotatedTuple.add t₂.castToAnnotatedTuple
• (t₁.sub t₂).castToAnnotatedTuple = t₁.castToAnnotatedTuple.sub t₂.castToAnnotatedTuple
• (t₁.mul t₂).castToAnnotatedTuple = t₁.castToAnnotatedTuple.mul t₂.castToAnnotatedTuple

def Term.eval {T : Type} [ValueType T] {n : ℕ} (term : Term T n) (tuple : Tuple T n) : T

Equations

• (Term.const c).eval tuple = c
• (#k).eval tuple = tuple k
• (t₁.add t₂).eval tuple = t₁.eval tuple + t₂.eval tuple
• (t₁.sub t₂).eval tuple = t₁.eval tuple - t₂.eval tuple
• (t₁.mul t₂).eval tuple = t₁.eval tuple * t₂.eval tuple

theorem Term.castToAnnotatedTuple_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} [HasAltLinearOrder K] [SemiringWithMonus K] (t : Term T n) (tuple : Tuple T n) (α : K) : t.castToAnnotatedTuple.eval (Fin.append (fun (k : Fin n) => Sum.inl (tuple k)) ![Sum.inr α]) = Sum.inl (t.eval tuple)

instance instCoeTerm {T : Type} {n : ℕ} : Coe T (Term T n)

Equations

• instCoeTerm = { coe := fun (a : T) => Term.const a }

instance instOfNatTermNat {n a : ℕ} : OfNat (Term ℕ n) a

Equations

• instOfNatTermNat = { ofNat := Term.const a }

def «term#_» : Lean.ParserDescr

Equations

• «term#_» = Lean.ParserDescr.node `«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

inductive BoolTerm (T : Sort u_1) (n : ℕ) : Sort (max 1 u_1)

• EQ {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• NE {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• LE {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• LT {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• GE {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• GT {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n

def BoolTerm.repr {T : Type} {n : ℕ} [Repr T] : BoolTerm T n → ℕ → Std.Format

Equations

• (BoolTerm.EQ t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "==" ++ t₂.repr x✝) x✝
• (BoolTerm.NE t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "!=" ++ t₂.repr x✝) x✝
• (BoolTerm.LE t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "<=" ++ t₂.repr x✝) x✝
• (BoolTerm.LT t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "<" ++ t₂.repr x✝) x✝
• (BoolTerm.GE t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text ">=" ++ t₂.repr x✝) x✝
• (BoolTerm.GT t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text ">" ++ t₂.repr x✝) x✝

instance instReprBoolTerm {α : Type} {n : ℕ} [Repr α] : Repr (BoolTerm α n)

Equations

• instReprBoolTerm = { reprPrec := BoolTerm.repr }

def BoolTerm.castToAnnotatedTuple {T : Type} {n : ℕ} {K : Type u_1} (bt : BoolTerm T n) : BoolTerm (T ⊕ K) (n + 1)

Equations

• (BoolTerm.EQ a b).castToAnnotatedTuple = BoolTerm.EQ a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.NE a b).castToAnnotatedTuple = BoolTerm.NE a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.LE a b).castToAnnotatedTuple = BoolTerm.LE a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.LT a b).castToAnnotatedTuple = BoolTerm.LT a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.GE a b).castToAnnotatedTuple = BoolTerm.GE a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.GT a b).castToAnnotatedTuple = BoolTerm.GT a.castToAnnotatedTuple b.castToAnnotatedTuple

def «term_==__1» : Lean.TrailingParserDescr

Equations

• «term_==__1» = Lean.ParserDescr.trailingNode `«term_==__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " == ") (Lean.ParserDescr.cat `term 21))

def «term_!=__1» : Lean.TrailingParserDescr

Equations

• «term_!=__1» = Lean.ParserDescr.trailingNode `«term_!=__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `term 21))

def «term_<=__1» : Lean.TrailingParserDescr

Equations

• «term_<=__1» = Lean.ParserDescr.trailingNode `«term_<=__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <= ") (Lean.ParserDescr.cat `term 21))

def «term_<__1» : Lean.TrailingParserDescr

Equations

• «term_<__1» = Lean.ParserDescr.trailingNode `«term_<__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `term 21))

def «term_>=__1» : Lean.TrailingParserDescr

Equations

• «term_>=__1» = Lean.ParserDescr.trailingNode `«term_>=__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >= ") (Lean.ParserDescr.cat `term 21))

def «term_>__1» : Lean.TrailingParserDescr

Equations

• «term_>__1» = Lean.ParserDescr.trailingNode `«term_>__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `term 21))

def BoolTerm.eval {T : Type} [ValueType T] {n : ℕ} (φ : BoolTerm T n) (tuple : Tuple T n) : Prop

Equations

• (BoolTerm.EQ a b).eval tuple = (a.eval tuple = b.eval tuple)
• (BoolTerm.NE a b).eval tuple = (a.eval tuple ≠ b.eval tuple)
• (BoolTerm.LE a b).eval tuple = (a.eval tuple ≤ b.eval tuple)
• (BoolTerm.LT a b).eval tuple = (a.eval tuple < b.eval tuple)
• (BoolTerm.GE a b).eval tuple = (a.eval tuple ≥ b.eval tuple)
• (BoolTerm.GT a b).eval tuple = (a.eval tuple > b.eval tuple)

theorem BoolTerm.castToAnnotatedTuple_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} [HasAltLinearOrder K] [SemiringWithMonus K] (t : BoolTerm T n) (tuple : Tuple T n) (α : K) : t.castToAnnotatedTuple.eval (Fin.append (fun (k : Fin n) => Sum.inl (tuple k)) ![Sum.inr α]) = t.eval tuple

def BoolTerm.evalDecidable {T : Type} [ValueType T] {n : ℕ} (φ : BoolTerm T n) : DecidablePred φ.eval

Equations

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

inductive Filter (T : Sort u_1) (n : ℕ) : Sort (max 1 u_1)

• BT {T : Sort u_1} {n : ℕ} : BoolTerm T n → Filter T n
• Not {T : Sort u_1} {n : ℕ} : Filter T n → Filter T n
• And {T : Sort u_1} {n : ℕ} : Filter T n → Filter T n → Filter T n
• Or {T : Sort u_1} {n : ℕ} : Filter T n → Filter T n → Filter T n
• True {T : Sort u_1} {n : ℕ} : Filter T n

def Filter.repr {T : Type} {n : ℕ} [Repr T] : Filter T n → ℕ → Std.Format

Equations

• (Filter.BT t).repr x✝ = t.repr x✝
• f.Not.repr x✝ = Std.Format.text "¬" ++ Repr.addAppParen (f.repr x✝) x✝
• (t₁.And t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "∧" ++ t₂.repr x✝) x✝
• (t₁.Or t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "∨" ++ t₂.repr x✝) x✝
• Filter.True.repr x✝ = Std.Format.text "True"

instance instReprFilter {α : Type} {n : ℕ} [Repr α] : Repr (Filter α n)

Equations

• instReprFilter = { reprPrec := Filter.repr }

def Filter.castToAnnotatedTuple {T : Type} {n : ℕ} {K : Type u_1} (f : Filter T n) : Filter (T ⊕ K) (n + 1)

Equations

• (Filter.BT t).castToAnnotatedTuple = Filter.BT t.castToAnnotatedTuple
• φ.Not.castToAnnotatedTuple = φ.castToAnnotatedTuple.Not
• (φ₁.And φ₂).castToAnnotatedTuple = φ₁.castToAnnotatedTuple.And φ₂.castToAnnotatedTuple
• (φ₁.Or φ₂).castToAnnotatedTuple = φ₁.castToAnnotatedTuple.Or φ₂.castToAnnotatedTuple
• Filter.True.castToAnnotatedTuple = Filter.True

def Filter.eval {T : Type} [ValueType T] {n : ℕ} (φ : Filter T n) (tuple : Tuple T n) : Prop

Equations

• (Filter.BT t).eval tuple = t.eval tuple
• φ_1.Not.eval tuple = ¬φ_1.eval tuple
• (φ₁.And φ₂).eval tuple = (φ₁.eval tuple ∧ φ₂.eval tuple)
• (φ₁.Or φ₂).eval tuple = (φ₁.eval tuple ∨ φ₂.eval tuple)
• Filter.True.eval tuple = (true = true)

theorem Filter.castToAnnotatedTuple_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} [HasAltLinearOrder K] [SemiringWithMonus K] (φ : Filter T n) (tuple : Tuple T n) (α : K) : φ.castToAnnotatedTuple.eval (Fin.append (fun (k : Fin n) => Sum.inl (tuple k)) ![Sum.inr α]) = φ.eval tuple

def Filter.evalDecidable {T : Type} [ValueType T] {n : ℕ} (φ : Filter T n) : DecidablePred φ.eval

Equations

• (Filter.BT t_1).evalDecidable t = t_1.evalDecidable t
• φ_1.Not.evalDecidable t = match φ_1.evalDecidable t with | isTrue h => isFalse ⋯ | isFalse h => isTrue ⋯
• (φ₁.And φ₂).evalDecidable t = match φ₁.evalDecidable t, φ₂.evalDecidable t with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h, x => isFalse ⋯ | x, isFalse h => isFalse ⋯
• (φ₁.Or φ₂).evalDecidable t = match φ₁.evalDecidable t, φ₂.evalDecidable t with | isTrue h, x => isTrue ⋯ | x, isTrue h => isTrue ⋯ | isFalse h₁, isFalse h₂ => isFalse ⋯
• Filter.True.evalDecidable t = isTrue ⋯

instance instCoeBoolTermFilter {T : Type} {n : ℕ} : Coe (BoolTerm T n) (Filter T n)

Equations

• instCoeBoolTermFilter = { coe := fun (bt : BoolTerm T n) => Filter.BT bt }

inductive AggFunc : Type

• sum : AggFunc

def instReprAggFunc.repr : AggFunc → ℕ → Std.Format

Equations

• instReprAggFunc.repr AggFunc.sum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AggFunc.sum")).group prec✝

instance instReprAggFunc : Repr AggFunc

Equations

• instReprAggFunc = { reprPrec := instReprAggFunc.repr }

def addFn {T : Type} [ValueType T] (a b : T) : T

Equations

• addFn a b = a + b

instance instCommutativeAddFn {T : Type} [ValueType T] : Std.Commutative addFn

instance instAssociativeAddFn {T : Type} [ValueType T] : Std.Associative addFn

def AggFunc.eval {T : Type} [ValueType T] (a : AggFunc) (m : Multiset T) : T

Equations

• AggFunc.sum.eval m = Multiset.fold addFn 0 m

inductive Query (T : Type) : ℕ → Type

• Rel {T : Type} (n : ℕ) : String → Query T n
• Proj {T : Type} {n m : ℕ} : Tuple (Term T n) m → Query T n → Query T m
• Sel {T : Type} {n : ℕ} : Filter T n → Query T n → Query T n
• Prod {T : Type} {n₁ n₂ n : ℕ} {hn : n₁ + n₂ = n} : Query T n₁ → Query T n₂ → Query T n
• Sum {T : Type} {n : ℕ} : Query T n → Query T n → Query T n
• Dedup {T : Type} {n : ℕ} : Query T n → Query T n
• Diff {T : Type} {n : ℕ} : Query T n → Query T n → Query T n
• Agg {T : Type} {m n₁ n₂ : ℕ} : Tuple (Fin m) n₁ → Tuple (Term T m) n₂ → Tuple AggFunc n₂ → Query T m → Query T (n₁ + n₂)

def Query.repr {T : Type} {n : ℕ} [Repr T] : Query T n → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• (Query.Rel n s).repr x✝ = Std.Format.text s
• (Π ts q).repr x✝ = Std.Format.text "Π_" ++ Repr.addAppParen (ts.repr x✝) x✝ ++ Repr.addAppParen (q.repr x✝) x✝
• (σ φ q).repr x✝ = Std.Format.text "σ_" ++ Repr.addAppParen (φ.repr x✝) x✝ ++ Repr.addAppParen (q.repr x✝) x✝
• (q₁ × q₂).repr x✝ = Repr.addAppParen (q₁.repr x✝ ++ Std.Format.text "×" ++ q₂.repr x✝) x✝
• (q₁ ⊎ q₂).repr x✝ = Repr.addAppParen (q₁.repr x✝ ++ Std.Format.text "⊎" ++ q₂.repr x✝) x✝
• (ε q).repr x✝ = Std.Format.text "ε" ++ Repr.addAppParen (q.repr x✝) x✝
• (q₁ - q₂).repr x✝ = Repr.addAppParen (q₁.repr x✝ ++ Std.Format.text "-" ++ q₂.repr x✝) x✝

instance instReprQuery {α : Type} {n : ℕ} [Repr α] : Repr (Query α n)

Equations

• instReprQuery = { reprPrec := Query.repr }

def Query.noAgg {T : Type} {n : ℕ} (q : Query T n) : Prop

Equations

• (Query.Rel n s).noAgg = True
• (Π a q_2).noAgg = q_2.noAgg
• (σ a q_2).noAgg = q_2.noAgg
• (q₁ × q₂).noAgg = (q₁.noAgg ∧ q₂.noAgg)
• (q₁ ⊎ q₂).noAgg = (q₁.noAgg ∧ q₂.noAgg)
• (ε q_2).noAgg = q_2.noAgg
• (q₁ - q₂).noAgg = (q₁.noAgg ∧ q₂.noAgg)
• (Query.Agg a a_1 a_2 q_2).noAgg = False

def Query.noAggDecidable {T : Type} {n : ℕ} : DecidablePred noAgg

Equations

• (Query.Rel n s).noAggDecidable = isTrue True.intro
• (Π a q_2).noAggDecidable = match q_2.noAggDecidable with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (σ a q_2).noAggDecidable = match q_2.noAggDecidable with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (q₁ × q₂).noAggDecidable = match q₁.noAggDecidable, q₂.noAggDecidable with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h₁, x => isFalse ⋯ | x, isFalse h₂ => isFalse ⋯
• (q₁ ⊎ q₂).noAggDecidable = match q₁.noAggDecidable, q₂.noAggDecidable with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h₁, x => isFalse ⋯ | x, isFalse h₂ => isFalse ⋯
• (ε q_2).noAggDecidable = match q_2.noAggDecidable with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (q₁ - q₂).noAggDecidable = match q₁.noAggDecidable, q₂.noAggDecidable with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h₁, x => isFalse ⋯ | x, isFalse h₂ => isFalse ⋯
• (Query.Agg a a_1 a_2 q_2).noAggDecidable = isFalse Query.noAggDecidable._proof_16

instance instDecidablePredQueryNoAgg {T : Type} {n : ℕ} : DecidablePred Query.noAgg

Equations

• instDecidablePredQueryNoAgg = Query.noAggDecidable

@[simp]

theorem Query.noAggProd {T : Type} [ValueType T] {n n₂ : ℕ} {q : Query T n} : q.noAgg → ∀ {n₁ : ℕ} {q₁ : Query T n₁} {q₂ : Query T n₂} {hn : n₁ + n₂ = n}, q = q₁ × q₂ → q₁.noAgg ∧ q₂.noAgg

@[simp]

theorem Query.noAggSum {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.noAgg → ∀ {q₁ q₂ : Query T n}, q = (q₁ ⊎ q₂) → q₁.noAgg ∧ q₂.noAgg

@[simp]

theorem Query.noAggDiff {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.noAgg → ∀ {q₁ q₂ : Query T n}, q = (q₁ - q₂) → q₁.noAgg ∧ q₂.noAgg

@[simp]

theorem Query.noAggProj {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.noAgg → ∀ {m : ℕ} {t : Tuple (Term T m) n} {q' : Query T m}, q = Π t q' → q'.noAgg

@[simp]

theorem Query.noAggSel {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.noAgg → ∀ {φ : Filter T n} {q' : Query T n}, q = σ φ q' → q'.noAgg

@[simp]

theorem Query.noAggDedup {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.noAgg → ∀ {q' : Query T n}, q = ε q' → q'.noAgg

def «termΠ_» : Lean.ParserDescr

Equations

• «termΠ_» = Lean.ParserDescr.node `«termΠ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Π ") (Lean.ParserDescr.cat `term 1024))

def termσ_ : Lean.ParserDescr

Equations

• termσ_ = Lean.ParserDescr.node `termσ_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "σ ") (Lean.ParserDescr.cat `term 1024))

def «term_×__2» : Lean.TrailingParserDescr

Equations

• «term_×__2» = Lean.ParserDescr.trailingNode `«term_×__2» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " × ") (Lean.ParserDescr.cat `term 81))

def «term_⊎_» : Lean.TrailingParserDescr

Equations

• «term_⊎_» = Lean.ParserDescr.trailingNode `«term_⊎_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊎ ") (Lean.ParserDescr.cat `term 51))

def termε_ : Lean.ParserDescr

Equations

• termε_ = Lean.ParserDescr.node `termε_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ε ") (Lean.ParserDescr.cat `term 1024))

def «term_-__1» : Lean.TrailingParserDescr

Equations

• «term_-__1» = Lean.ParserDescr.trailingNode `«term_-__1» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `term 51))

def «term_⋈_» : Lean.TrailingParserDescr

Equations

• «term_⋈_» = Lean.ParserDescr.trailingNode `«term_⋈_» 1020 1021 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 1021))

def «term_∪__1» : Lean.TrailingParserDescr

Equations

• «term_∪__1» = Lean.ParserDescr.trailingNode `«term_∪__1» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∪ ") (Lean.ParserDescr.cat `term 51))

def Query.arity {T : Type} {n : ℕ} : Query T n → ℕ

Equations

• x✝.arity = n

def Query.aggdepth2_plus_depth {T : Type} {n : ℕ} (q : Query T n) : ℕ

Equations

• (Query.Rel n s).aggdepth2_plus_depth = 0
• (Π a q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 1
• (σ a q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 1
• (q₁ × q₂).aggdepth2_plus_depth = max q₁.aggdepth2_plus_depth q₂.aggdepth2_plus_depth + 1
• (q₁ ⊎ q₂).aggdepth2_plus_depth = max q₁.aggdepth2_plus_depth q₂.aggdepth2_plus_depth + 1
• (ε q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 1
• (q₁ - q₂).aggdepth2_plus_depth = max q₁.aggdepth2_plus_depth q₂.aggdepth2_plus_depth + 1
• (Query.Agg a a_1 a_2 q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 3

@[irreducible]

def Query.evaluate {T : Type} [ValueType T] {n : ℕ} (q : Query T n) (d : Database T) : Relation T n

Equations

• One or more equations did not get rendered due to their size.
• (Query.Rel n s).evaluate d = match Database.find n s d with | none => ∅ | some rn => rn
• (Π a q_2).evaluate d = Multiset.map (fun (t : Tuple T n_3) (k : Fin n) => (a k).eval t) (q_2.evaluate d)
• (σ a q_2).evaluate d = Multiset.filter a.eval (q_2.evaluate d)
• (q₁ × q₂).evaluate d = Relation.cast hn (q₁.evaluate d * q₂.evaluate d)
• (q₁ ⊎ q₂).evaluate d = q₁.evaluate d + q₂.evaluate d
• (ε q_2).evaluate d = Multiset.dedup (q_2.evaluate d)
• (q₁ - q₂).evaluate d = q₁.evaluate d - q₂.evaluate d