@[reducible, inline]

noncomputable abbrev TBBMinus {α : Type u_1} [DecidableEq α] (X : Set ℕ) (X_finite : X.Finite := by grind) : Formula α

Equations

• TBBMinus X X_finite = ∼⋀Finset.image TBB X_finite.toFinset

@[reducible, inline]

abbrev LogicGLBetaMinus {α : Type u_1} [DecidableEq α] (X : Set ℕ) (X_cofinite : Xᶜ.Finite := by grind) : Logic α

Equations

• LogicGLBetaMinus X X_cofinite = (LogicGL +ᴸ {TBBMinus Xᶜ X_cofinite}.lift)