def r : Relation String 4

Equations

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

def d : Database String

Equations

• d = [("Personnel", ⟨4, r⟩)]

def qPersonnel : Query String 4

Equations

• qPersonnel = Query.Rel 4 "Personnel"

def q₀ : Query String (Nat.succ 0)

Equations

• q₀ = ε (Π ![#3] qPersonnel)

def q₁ : Query String (Nat.succ 0)

Equations

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

def q₂ : Query String (Nat.succ 0)

Equations

• q₂ = (q₀ - q₁)

def qc : Query String (Nat.succ 0 + Nat.succ 0)

Equations

• qc = Query.Agg ![3] ![Term.const "1"] ![AggFunc.sum] qPersonnel

def r_count : AnnotatedRelation String ℕ 4

Equations

• r_count = Relation.annotate (fun (x : Tuple String 4) => 1) r

def d_count : AnnotatedDatabase String ℕ

Equations

• d_count = [("Personnel", ⟨4, r_count⟩)]

def r_tropical : AnnotatedRelation String (Tropical (WithTop ℕ)) 4

Equations

• r_tropical = Relation.annotate (fun (x : Tuple String 4) => Tropical.trop 1) r

def d_tropical : AnnotatedDatabase String (Tropical (WithTop ℕ))

Equations

• d_tropical = [("Personnel", ⟨4, r_tropical⟩)]