Bounded formulas with bounds supplied by an operator; this operator-parametric presentation and its rewriting lemmas are specific to this formalization.

inductive FFL.FirstOrder.Semiformula.Bounded {L : Language} {ξ : Type u_1} (R : Operator L 2) {n : ℕ} : Semiformula L ξ n → Prop

• verum {L : Language} {ξ : Type u_1} {R : Operator L 2} (n : ℕ) : Bounded R ⊤
• falsum {L : Language} {ξ : Type u_1} {R : Operator L 2} (n : ℕ) : Bounded R ⊥
• rel {L : Language} {ξ : Type u_1} {R : Operator L 2} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : Bounded R (Semiformula.rel r v)
• nrel {L : Language} {ξ : Type u_1} {R : Operator L 2} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : Bounded R (Semiformula.nrel r v)
• and {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ ψ : Semiformula L ξ n} : Bounded R φ → Bounded R ψ → Bounded R (φ ⋏ ψ)
• or {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ ψ : Semiformula L ξ n} : Bounded R φ → Bounded R ψ → Bounded R (φ ⋎ ψ)
• ball {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} : t.Positive → Bounded R φ → Bounded R (∀¹[R.operator ![Semiterm.bvar 0, t]] φ)
• bexs {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} : t.Positive → Bounded R φ → Bounded R (∃¹[R.operator ![Semiterm.bvar 0, t]] φ)

@[simp]

theorem FFL.FirstOrder.Semiformula.Bounded.and_iff {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ ψ : Semiformula L ξ n} : Bounded R (φ ⋏ ψ) ↔ Bounded R φ ∧ Bounded R ψ

@[simp]

theorem FFL.FirstOrder.Semiformula.Bounded.or_iff {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ ψ : Semiformula L ξ n} : Bounded R (φ ⋎ ψ) ↔ Bounded R φ ∧ Bounded R ψ

theorem FFL.FirstOrder.Semiformula.Bounded.neg {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ : Semiformula L ξ n} : Bounded R φ → Bounded R (∼φ)

@[simp]

theorem FFL.FirstOrder.Semiformula.Bounded.neg_iff {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ : Semiformula L ξ n} : Bounded R (∼φ) ↔ Bounded R φ

@[simp]

theorem FFL.FirstOrder.Semiformula.Bounded.ball_iff {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) : Bounded R (∀¹[R.operator ![Semiterm.bvar 0, t]] φ) ↔ Bounded R φ

@[simp]

theorem FFL.FirstOrder.Semiformula.Bounded.bexs_iff {L : Language} {ξ : Type u_1} {R : Operator L 2} {n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) : Bounded R (∃¹[R.operator ![Semiterm.bvar 0, t]] φ) ↔ Bounded R φ

theorem FFL.FirstOrder.Semiformula.Bounded.rew {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {R : Operator L 2} {n₁ n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} : Bounded R φ → Bounded R ((Rewriting.app ω) φ)

theorem FFL.FirstOrder.Semiformula.Bounded.operator_preimage {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {R : Operator L 2} {n₁ n₂ : ℕ} [R.SymbolLike ξ₁ ξ₂] {ω : Rew L ξ₁ n₁ ξ₂ n₂} {χ : Semiformula L ξ₁ (n₁ + 1)} {t : Semiterm L ξ₂ (n₂ + 1)} (hχ : (Rewriting.app ω.q) χ = R.operator ![Semiterm.bvar 0, t]) (ht : t.Positive) : ∃ (u : Semiterm L ξ₁ (n₁ + 1)), χ = R.operator ![Semiterm.bvar 0, u] ∧ u.Positive

@[simp]

theorem FFL.FirstOrder.Semiformula.Bounded.rew_iff {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {R : Operator L 2} {n₁ n₂ : ℕ} [R.SymbolLike ξ₁ ξ₂] {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} : Bounded R ((Rewriting.app ω) φ) ↔ Bounded R φ