inductive LO.FirstOrder.UFormula (L : LO.FirstOrder.Language) (μ : Type v) : Type (max u v)

• verum: {L : LO.FirstOrder.Language} → {μ : Type v} → LO.FirstOrder.UFormula L μ
• falsum: {L : LO.FirstOrder.Language} → {μ : Type v} → LO.FirstOrder.UFormula L μ
• rel: {L : LO.FirstOrder.Language} → {μ : Type v} → {arity : ℕ} → L.Rel arity → (Fin arity → LO.FirstOrder.UTerm L μ) → LO.FirstOrder.UFormula L μ
• nrel: {L : LO.FirstOrder.Language} → {μ : Type v} → {arity : ℕ} → L.Rel arity → (Fin arity → LO.FirstOrder.UTerm L μ) → LO.FirstOrder.UFormula L μ
• and: {L : LO.FirstOrder.Language} → {μ : Type v} → LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ
• or: {L : LO.FirstOrder.Language} → {μ : Type v} → LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ
• all: {L : LO.FirstOrder.Language} → {μ : Type v} → LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ
• ex: {L : LO.FirstOrder.Language} → {μ : Type v} → LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ

instance LO.FirstOrder.UFormula.instInhabited {L : LO.FirstOrder.Language} {μ : Type v} : Inhabited (LO.FirstOrder.UFormula L μ)

Equations

• LO.FirstOrder.UFormula.instInhabited = { default := LO.FirstOrder.UFormula.verum }

def LO.FirstOrder.UFormula.elim {L : LO.FirstOrder.Language} {μ : Type v} {γ : Type u_1} (γVerum : γ) (γFalsum : γ) (γRel : {k : ℕ} → L.Rel k → (Fin k → LO.FirstOrder.UTerm L μ) → γ) (γNrel : {k : ℕ} → L.Rel k → (Fin k → LO.FirstOrder.UTerm L μ) → γ) (γAnd : γ → γ → γ) (γOr : γ → γ → γ) (γAll : γ → γ) (γEx : γ → γ) : LO.FirstOrder.UFormula L μ → γ

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.UFormula.elim γVerum γFalsum γRel γNrel γAnd γOr γAll γEx LO.FirstOrder.UFormula.verum = γVerum
• LO.FirstOrder.UFormula.elim γVerum γFalsum γRel γNrel γAnd γOr γAll γEx LO.FirstOrder.UFormula.falsum = γFalsum
• LO.FirstOrder.UFormula.elim γVerum γFalsum γRel γNrel γAnd γOr γAll γEx (LO.FirstOrder.UFormula.rel r v) = γRel r v
• LO.FirstOrder.UFormula.elim γVerum γFalsum γRel γNrel γAnd γOr γAll γEx (LO.FirstOrder.UFormula.nrel r v) = γNrel r v
• LO.FirstOrder.UFormula.elim γVerum γFalsum γRel γNrel γAnd γOr γAll γEx p.all = γAll (LO.FirstOrder.UFormula.elim γVerum γFalsum (fun {k : ℕ} => γRel) (fun {k : ℕ} => γNrel) γAnd γOr γAll γEx p)
• LO.FirstOrder.UFormula.elim γVerum γFalsum γRel γNrel γAnd γOr γAll γEx p.ex = γEx (LO.FirstOrder.UFormula.elim γVerum γFalsum (fun {k : ℕ} => γRel) (fun {k : ℕ} => γNrel) γAnd γOr γAll γEx p)

def LO.FirstOrder.UFormula.neg {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula L μ

Equations

• LO.FirstOrder.UFormula.verum.neg = LO.FirstOrder.UFormula.falsum
• LO.FirstOrder.UFormula.falsum.neg = LO.FirstOrder.UFormula.verum
• (LO.FirstOrder.UFormula.rel r v).neg = LO.FirstOrder.UFormula.nrel r v
• (LO.FirstOrder.UFormula.nrel r v).neg = LO.FirstOrder.UFormula.rel r v
• (p.and q).neg = p.neg.or q.neg
• (p.or q).neg = p.neg.and q.neg
• p.all.neg = p.neg.ex
• p.ex.neg = p.neg.all

def LO.FirstOrder.UFormula.bv {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula L μ → ℕ

Equations

• LO.FirstOrder.UFormula.verum.bv = 0
• LO.FirstOrder.UFormula.falsum.bv = 0
• (LO.FirstOrder.UFormula.rel r v).bv = Finset.univ.sup fun (i : Fin arity) => (v i).bv
• (LO.FirstOrder.UFormula.nrel r v).bv = Finset.univ.sup fun (i : Fin arity) => (v i).bv
• (p.and q).bv = max p.bv q.bv
• (p.or q).bv = max p.bv q.bv
• p.all.bv = p.bv.pred
• p.ex.bv = p.bv.pred

def LO.FirstOrder.UFormula.depth {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula L μ → ℕ

Equations

• LO.FirstOrder.UFormula.verum.depth = 0
• LO.FirstOrder.UFormula.falsum.depth = 0
• (LO.FirstOrder.UFormula.rel r v).depth = 0
• (LO.FirstOrder.UFormula.nrel r v).depth = 0
• (p.and q).depth = max p.depth q.depth + 1
• (p.or q).depth = max p.depth q.depth + 1
• p.all.depth = p.depth + 1
• p.ex.depth = p.depth + 1

def LO.FirstOrder.UFormula.shiftb {L : LO.FirstOrder.Language} {μ : Type v} (b : ℕ → LO.FirstOrder.UTerm L μ) (n : ℕ) : ℕ → LO.FirstOrder.UTerm L μ

Equations

• LO.FirstOrder.UFormula.shiftb b n x = if x < n then LO.FirstOrder.UTerm.bvar x else LO.FirstOrder.UTerm.bShifts n (b (x - n))

@[simp]

theorem LO.FirstOrder.UFormula.shiftb_zero {L : LO.FirstOrder.Language} {μ : Type v} (b : ℕ → LO.FirstOrder.UTerm L μ) : LO.FirstOrder.UFormula.shiftb b 0 = b

@[simp]

theorem LO.FirstOrder.UFormula.shiftb_shiftb_zero {L : LO.FirstOrder.Language} {μ : Type v} (b : ℕ → LO.FirstOrder.UTerm L μ) (m₁ : ℕ) (m₂ : ℕ) : LO.FirstOrder.UFormula.shiftb (LO.FirstOrder.UFormula.shiftb b m₁) m₂ = LO.FirstOrder.UFormula.shiftb b (m₁ + m₂)

def LO.FirstOrder.UFormula.bindq {L : LO.FirstOrder.Language} {μ₂ : Type u_1} {μ₁ : Type u_2} (b : ℕ → LO.FirstOrder.UTerm L μ₂) (e : μ₁ → LO.FirstOrder.UTerm L μ₂) : ℕ → LO.FirstOrder.UFormula L μ₁ → LO.FirstOrder.UFormula L μ₂

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.UFormula.bindq b e x LO.FirstOrder.UFormula.verum = LO.FirstOrder.UFormula.verum
• LO.FirstOrder.UFormula.bindq b e x LO.FirstOrder.UFormula.falsum = LO.FirstOrder.UFormula.falsum
• LO.FirstOrder.UFormula.bindq b e x (p.and q) = (LO.FirstOrder.UFormula.bindq b e x p).and (LO.FirstOrder.UFormula.bindq b e x q)
• LO.FirstOrder.UFormula.bindq b e x (p.or q) = (LO.FirstOrder.UFormula.bindq b e x p).or (LO.FirstOrder.UFormula.bindq b e x q)
• LO.FirstOrder.UFormula.bindq b e x p.all = (LO.FirstOrder.UFormula.bindq b e (x + 1) p).all
• LO.FirstOrder.UFormula.bindq b e x p.ex = (LO.FirstOrder.UFormula.bindq b e (x + 1) p).ex

def LO.FirstOrder.UFormula.bind {L : LO.FirstOrder.Language} {μ₂ : Type u_1} {μ₁ : Type u_2} (b : ℕ → LO.FirstOrder.UTerm L μ₂) (e : μ₁ → LO.FirstOrder.UTerm L μ₂) : LO.FirstOrder.UFormula L μ₁ → LO.FirstOrder.UFormula L μ₂

Equations

• LO.FirstOrder.UFormula.bind b e = LO.FirstOrder.UFormula.bindq b e 0

theorem LO.FirstOrder.UFormula.bindq_eq_bind {L : LO.FirstOrder.Language} {μ₂ : Type u_1} {μ₁ : Type u_2} {m : ℕ} {p : LO.FirstOrder.UFormula L μ₁} (b : ℕ → LO.FirstOrder.UTerm L μ₂) (e : μ₁ → LO.FirstOrder.UTerm L μ₂) : LO.FirstOrder.UFormula.bindq b e m p = LO.FirstOrder.UFormula.bind (LO.FirstOrder.UFormula.shiftb b m) (fun (x : μ₁) => LO.FirstOrder.UTerm.bShifts m (e x)) p

def LO.FirstOrder.UFormula.rewrite {L : LO.FirstOrder.Language} {μ₁ : Type u_1} {μ₂ : Type u_2} (e : μ₁ → LO.FirstOrder.UTerm L μ₂) : LO.FirstOrder.UFormula L μ₁ → LO.FirstOrder.UFormula L μ₂

Equations

• LO.FirstOrder.UFormula.rewrite e LO.FirstOrder.UFormula.verum = LO.FirstOrder.UFormula.verum
• LO.FirstOrder.UFormula.rewrite e LO.FirstOrder.UFormula.falsum = LO.FirstOrder.UFormula.falsum
• LO.FirstOrder.UFormula.rewrite e (LO.FirstOrder.UFormula.rel r v) = LO.FirstOrder.UFormula.rel r fun (i : Fin arity) => LO.FirstOrder.UTerm.rewrite e (v i)
• LO.FirstOrder.UFormula.rewrite e (LO.FirstOrder.UFormula.nrel r v) = LO.FirstOrder.UFormula.nrel r fun (i : Fin arity) => LO.FirstOrder.UTerm.rewrite e (v i)
• LO.FirstOrder.UFormula.rewrite e (p.and q) = (LO.FirstOrder.UFormula.rewrite e p).and (LO.FirstOrder.UFormula.rewrite e q)
• LO.FirstOrder.UFormula.rewrite e (p.or q) = (LO.FirstOrder.UFormula.rewrite e p).or (LO.FirstOrder.UFormula.rewrite e q)
• LO.FirstOrder.UFormula.rewrite e p.all = (LO.FirstOrder.UFormula.rewrite e p).all
• LO.FirstOrder.UFormula.rewrite e p.ex = (LO.FirstOrder.UFormula.rewrite e p).ex

@[simp]

theorem LO.FirstOrder.UFormula.bv_verum {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula.verum.bv = 0

@[simp]

theorem LO.FirstOrder.UFormula.bv_falsum {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula.falsum.bv = 0

@[simp]

theorem LO.FirstOrder.UFormula.bv_rel {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) : (LO.FirstOrder.UFormula.rel r v).bv = Finset.univ.sup fun (i : Fin k) => (v i).bv

@[simp]

theorem LO.FirstOrder.UFormula.bv_nrel {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) : (LO.FirstOrder.UFormula.nrel r v).bv = Finset.univ.sup fun (i : Fin k) => (v i).bv

@[simp]

theorem LO.FirstOrder.UFormula.bv_and {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) (q : LO.FirstOrder.UFormula L μ) : (p.and q).bv = max p.bv q.bv

@[simp]

theorem LO.FirstOrder.UFormula.bv_or {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) (q : LO.FirstOrder.UFormula L μ) : (p.or q).bv = max p.bv q.bv

@[simp]

theorem LO.FirstOrder.UFormula.bv_all {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) : p.all.bv = p.bv.pred

@[simp]

theorem LO.FirstOrder.UFormula.bv_ex {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) : p.ex.bv = p.bv.pred

@[simp]

theorem LO.FirstOrder.UFormula.subtype_val_le {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : { p : LO.FirstOrder.UFormula L μ // p.bv ≤ n }) : (↑p).bv ≤ n

theorem LO.FirstOrder.UFormula.bind_eq_bind_of_eq {L : LO.FirstOrder.Language} {μ₂ : Type u_1} {μ₁ : Type u_2} (b₁ : ℕ → LO.FirstOrder.UTerm L μ₂) (b₂ : ℕ → LO.FirstOrder.UTerm L μ₂) (e₁ : μ₁ → LO.FirstOrder.UTerm L μ₂) (e₂ : μ₁ → LO.FirstOrder.UTerm L μ₂) (p : LO.FirstOrder.UFormula L μ₁) (hb : ∀ x < p.bv, b₁ x = b₂ x) (he : ∀ (x : μ₁), e₁ x = e₂ x) : LO.FirstOrder.UFormula.bind b₁ e₁ p = LO.FirstOrder.UFormula.bind b₂ e₂ p

def LO.FirstOrder.UFormula.toSubformula {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.UFormula L μ) : p.bv ≤ n → LO.FirstOrder.Semiformula L μ n

Equations

• LO.FirstOrder.UFormula.verum.toSubformula x_4 = ⊤
• LO.FirstOrder.UFormula.falsum.toSubformula x_4 = ⊥
• (LO.FirstOrder.UFormula.rel r v).toSubformula h = LO.FirstOrder.Semiformula.rel r fun (i : Fin arity) => (v i).toSubterm ⋯
• (LO.FirstOrder.UFormula.nrel r v).toSubformula h = LO.FirstOrder.Semiformula.nrel r fun (i : Fin arity) => (v i).toSubterm ⋯
• (p.and q).toSubformula h = p.toSubformula ⋯ ⋏ q.toSubformula ⋯
• (p.or q).toSubformula h = p.toSubformula ⋯ ⋎ q.toSubformula ⋯
• p.all.toSubformula h = ∀' p.toSubformula ⋯
• p.ex.toSubformula h = ∃' p.toSubformula ⋯

def LO.FirstOrder.UFormula.ofSubformula {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} : LO.FirstOrder.Semiformula L μ n → { p : LO.FirstOrder.UFormula L μ // p.bv ≤ n }

Equations

• LO.FirstOrder.UFormula.ofSubformula LO.FirstOrder.Semiformula.verum = ⟨LO.FirstOrder.UFormula.verum, ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula LO.FirstOrder.Semiformula.falsum = ⟨LO.FirstOrder.UFormula.falsum, ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula (LO.FirstOrder.Semiformula.rel r v) = ⟨LO.FirstOrder.UFormula.rel r fun (i : Fin arity) => ↑(LO.FirstOrder.UTerm.ofSubterm (v i)), ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula (LO.FirstOrder.Semiformula.nrel r v) = ⟨LO.FirstOrder.UFormula.nrel r fun (i : Fin arity) => ↑(LO.FirstOrder.UTerm.ofSubterm (v i)), ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula (p.and q) = ⟨(↑(LO.FirstOrder.UFormula.ofSubformula p)).and ↑(LO.FirstOrder.UFormula.ofSubformula q), ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula (p.or q) = ⟨(↑(LO.FirstOrder.UFormula.ofSubformula p)).or ↑(LO.FirstOrder.UFormula.ofSubformula q), ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula p.all = ⟨(↑(LO.FirstOrder.UFormula.ofSubformula p)).all, ⋯⟩
• LO.FirstOrder.UFormula.ofSubformula p.ex = ⟨(↑(LO.FirstOrder.UFormula.ofSubformula p)).ex, ⋯⟩

theorem LO.FirstOrder.UFormula.toSubformula_ofSubformula {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.Semiformula L μ n) : (↑(LO.FirstOrder.UFormula.ofSubformula p)).toSubformula ⋯ = p

theorem LO.FirstOrder.UFormula.ofSubformula_toSubformula {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.UFormula L μ) (h : p.bv ≤ n) : ↑(LO.FirstOrder.UFormula.ofSubformula (p.toSubformula h)) = p

def LO.FirstOrder.UFormula.subfEquiv {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} : LO.FirstOrder.Semiformula L μ n ≃ { p : LO.FirstOrder.UFormula L μ // p.bv ≤ n }

Equations

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

theorem LO.FirstOrder.UFormula.ofSubformula_eq_subfEquiv {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} : LO.FirstOrder.UFormula.ofSubformula = ⇑LO.FirstOrder.UFormula.subfEquiv

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_verum {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} : LO.FirstOrder.UFormula.subfEquiv ⊤ = ⟨LO.FirstOrder.UFormula.verum, ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_falsum {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} : LO.FirstOrder.UFormula.subfEquiv ⊥ = ⟨LO.FirstOrder.UFormula.falsum, ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_rel {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L μ n) : LO.FirstOrder.UFormula.subfEquiv (LO.FirstOrder.Semiformula.rel r v) = ⟨LO.FirstOrder.UFormula.rel r fun (i : Fin k) => ↑(LO.FirstOrder.UTerm.subtEquiv (v i)), ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_nrel {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L μ n) : LO.FirstOrder.UFormula.subfEquiv (LO.FirstOrder.Semiformula.nrel r v) = ⟨LO.FirstOrder.UFormula.nrel r fun (i : Fin k) => ↑(LO.FirstOrder.UTerm.subtEquiv (v i)), ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_and {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.Semiformula L μ n) (q : LO.FirstOrder.Semiformula L μ n) : LO.FirstOrder.UFormula.subfEquiv (p ⋏ q) = ⟨(↑(LO.FirstOrder.UFormula.subfEquiv p)).and ↑(LO.FirstOrder.UFormula.subfEquiv q), ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_or {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.Semiformula L μ n) (q : LO.FirstOrder.Semiformula L μ n) : LO.FirstOrder.UFormula.subfEquiv (p ⋎ q) = ⟨(↑(LO.FirstOrder.UFormula.subfEquiv p)).or ↑(LO.FirstOrder.UFormula.subfEquiv q), ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_all {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.Semiformula L μ (n + 1)) : LO.FirstOrder.UFormula.subfEquiv (∀' p) = ⟨(↑(LO.FirstOrder.UFormula.subfEquiv p)).all, ⋯⟩

@[simp]

theorem LO.FirstOrder.UFormula.subfEquiv_ex {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.Semiformula L μ (n + 1)) : LO.FirstOrder.UFormula.subfEquiv (∃' p) = ⟨(↑(LO.FirstOrder.UFormula.subfEquiv p)).ex, ⋯⟩

@[reducible, inline]

abbrev LO.FirstOrder.UFormula.Node (L : LO.FirstOrder.Language) (μ : Type v) : Type (max u v)

Equations

• LO.FirstOrder.UFormula.Node L μ = (Bool × ((k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ) ⊕ Unit ⊕ Unit ⊕ Unit))

instance LO.FirstOrder.UFormula.instPrimcodableNode {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primcodable (LO.FirstOrder.UFormula.Node L μ)

Equations

• LO.FirstOrder.UFormula.instPrimcodableNode = Primcodable.prod

@[reducible]

def LO.FirstOrder.UFormula.Edge (L : LO.FirstOrder.Language) (μ : Type v) : LO.FirstOrder.UFormula.Node L μ → Type

Equations

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

instance LO.FirstOrder.UFormula.instInhabitedWTypeNodeEdge {L : LO.FirstOrder.Language} {μ : Type v} : Inhabited (WType (LO.FirstOrder.UFormula.Edge L μ))

Equations

• LO.FirstOrder.UFormula.instInhabitedWTypeNodeEdge = { default := WType.mk (true, Sum.inr (Sum.inl ())) Empty.elim }

def LO.FirstOrder.UFormula.toW {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula L μ → WType (LO.FirstOrder.UFormula.Edge L μ)

Equations

• (LO.FirstOrder.UFormula.rel r v).toW = WType.mk (true, Sum.inl ⟨arity, (r, v)⟩) Empty.elim
• (LO.FirstOrder.UFormula.nrel r v).toW = WType.mk (false, Sum.inl ⟨arity, (r, v)⟩) Empty.elim
• LO.FirstOrder.UFormula.verum.toW = WType.mk (true, Sum.inr (Sum.inl ())) Empty.elim
• LO.FirstOrder.UFormula.falsum.toW = WType.mk (false, Sum.inr (Sum.inl ())) Empty.elim
• (p.and q).toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) fun (t : Bool) => Bool.rec p.toW q.toW t
• (p.or q).toW = WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) fun (t : Bool) => Bool.rec p.toW q.toW t
• p.all.toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) fun (x : LO.FirstOrder.UFormula.Edge L μ (true, Sum.inr (Sum.inr (Sum.inr ())))) => p.toW
• p.ex.toW = WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) fun (x : LO.FirstOrder.UFormula.Edge L μ (false, Sum.inr (Sum.inr (Sum.inr ())))) => p.toW

def LO.FirstOrder.UFormula.ofW {L : LO.FirstOrder.Language} {μ : Type v} : WType (LO.FirstOrder.UFormula.Edge L μ) → LO.FirstOrder.UFormula L μ

Equations

• LO.FirstOrder.UFormula.ofW (WType.mk (true, Sum.inl ⟨fst, (r, v)⟩) f) = LO.FirstOrder.UFormula.rel r v
• LO.FirstOrder.UFormula.ofW (WType.mk (false, Sum.inl ⟨fst, (r, v)⟩) f) = LO.FirstOrder.UFormula.nrel r v
• LO.FirstOrder.UFormula.ofW (WType.mk (true, Sum.inr (Sum.inl PUnit.unit)) f) = LO.FirstOrder.UFormula.verum
• LO.FirstOrder.UFormula.ofW (WType.mk (false, Sum.inr (Sum.inl PUnit.unit)) f) = LO.FirstOrder.UFormula.falsum
• LO.FirstOrder.UFormula.ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inl PUnit.unit))) p) = (LO.FirstOrder.UFormula.ofW (p false)).and (LO.FirstOrder.UFormula.ofW (p true))
• LO.FirstOrder.UFormula.ofW (WType.mk (false, Sum.inr (Sum.inr (Sum.inl PUnit.unit))) p) = (LO.FirstOrder.UFormula.ofW (p false)).or (LO.FirstOrder.UFormula.ofW (p true))
• LO.FirstOrder.UFormula.ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inr PUnit.unit))) p) = (LO.FirstOrder.UFormula.ofW (p ())).all
• LO.FirstOrder.UFormula.ofW (WType.mk (false, Sum.inr (Sum.inr (Sum.inr PUnit.unit))) p) = (LO.FirstOrder.UFormula.ofW (p ())).ex

theorem LO.FirstOrder.UFormula.toW_ofW {L : LO.FirstOrder.Language} {μ : Type v} (w : WType (LO.FirstOrder.UFormula.Edge L μ)) : (LO.FirstOrder.UFormula.ofW w).toW = w

def LO.FirstOrder.UFormula.equivW (L : LO.FirstOrder.Language) (μ : Type u_2) : LO.FirstOrder.UFormula L μ ≃ WType (LO.FirstOrder.UFormula.Edge L μ)

Equations

• LO.FirstOrder.UFormula.equivW L μ = { toFun := LO.FirstOrder.UFormula.toW, invFun := LO.FirstOrder.UFormula.ofW, left_inv := ⋯, right_inv := ⋯ }

theorem LO.FirstOrder.UFormula.toW_eq_equivW {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula.toW = ⇑(LO.FirstOrder.UFormula.equivW L μ)

@[simp]

theorem LO.FirstOrder.UFormula.equivW_verum {L : LO.FirstOrder.Language} {μ : Type v} : (LO.FirstOrder.UFormula.equivW L μ) LO.FirstOrder.UFormula.verum = WType.mk (true, Sum.inr (Sum.inl ())) Empty.elim

@[simp]

theorem LO.FirstOrder.UFormula.equivW_falsum {L : LO.FirstOrder.Language} {μ : Type v} : (LO.FirstOrder.UFormula.equivW L μ) LO.FirstOrder.UFormula.falsum = WType.mk (false, Sum.inr (Sum.inl ())) Empty.elim

@[simp]

theorem LO.FirstOrder.UFormula.equivW_rel {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) : (LO.FirstOrder.UFormula.equivW L μ) (LO.FirstOrder.UFormula.rel r v) = WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim

@[simp]

theorem LO.FirstOrder.UFormula.equivW_nrel {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) : (LO.FirstOrder.UFormula.equivW L μ) (LO.FirstOrder.UFormula.nrel r v) = WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim

@[simp]

theorem LO.FirstOrder.UFormula.equivW_and {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) (q : LO.FirstOrder.UFormula L μ) : (LO.FirstOrder.UFormula.equivW L μ) (p.and q) = WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) fun (t : Bool) => Bool.rec ((LO.FirstOrder.UFormula.equivW L μ) p) ((LO.FirstOrder.UFormula.equivW L μ) q) t

@[simp]

theorem LO.FirstOrder.UFormula.equivW_or {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) (q : LO.FirstOrder.UFormula L μ) : (LO.FirstOrder.UFormula.equivW L μ) (p.or q) = WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) fun (t : Bool) => Bool.rec ((LO.FirstOrder.UFormula.equivW L μ) p) ((LO.FirstOrder.UFormula.equivW L μ) q) t

@[simp]

theorem LO.FirstOrder.UFormula.equivW_all {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) : (LO.FirstOrder.UFormula.equivW L μ) p.all = WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) fun (x : LO.FirstOrder.UFormula.Edge L μ (true, Sum.inr (Sum.inr (Sum.inr ())))) => (LO.FirstOrder.UFormula.equivW L μ) p

@[simp]

theorem LO.FirstOrder.UFormula.equivW_ex {L : LO.FirstOrder.Language} {μ : Type v} (p : LO.FirstOrder.UFormula L μ) : (LO.FirstOrder.UFormula.equivW L μ) p.ex = WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) fun (x : LO.FirstOrder.UFormula.Edge L μ (false, Sum.inr (Sum.inr (Sum.inr ())))) => (LO.FirstOrder.UFormula.equivW L μ) p

@[simp]

theorem LO.FirstOrder.UFormula.equivW_symm_true_inl {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.UTerm L μ} : (LO.FirstOrder.UFormula.equivW L μ).symm (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) = LO.FirstOrder.UFormula.rel r v

@[simp]

theorem LO.FirstOrder.UFormula.equivW_symm_false_inl {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.UTerm L μ} : (LO.FirstOrder.UFormula.equivW L μ).symm (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) = LO.FirstOrder.UFormula.nrel r v

@[simp]

theorem LO.FirstOrder.UFormula.equivW_symm_true_inr_inr_inl {L : LO.FirstOrder.Language} {μ : Type v} (v : Bool → WType (LO.FirstOrder.UFormula.Edge L μ)) : (LO.FirstOrder.UFormula.equivW L μ).symm (WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) v) = ((LO.FirstOrder.UFormula.equivW L μ).symm (v false)).and ((LO.FirstOrder.UFormula.equivW L μ).symm (v true))

@[simp]

theorem LO.FirstOrder.UFormula.equivW_symm_false_inr_inr_inl {L : LO.FirstOrder.Language} {μ : Type v} (v : Bool → WType (LO.FirstOrder.UFormula.Edge L μ)) : (LO.FirstOrder.UFormula.equivW L μ).symm (WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) v) = ((LO.FirstOrder.UFormula.equivW L μ).symm (v false)).or ((LO.FirstOrder.UFormula.equivW L μ).symm (v true))

@[simp]

theorem LO.FirstOrder.UFormula.equivW_symm_true_inr_inr_inr {L : LO.FirstOrder.Language} {μ : Type v} (v : Unit → WType (LO.FirstOrder.UFormula.Edge L μ)) : (LO.FirstOrder.UFormula.equivW L μ).symm (WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) v) = ((LO.FirstOrder.UFormula.equivW L μ).symm (v ())).all

@[simp]

theorem LO.FirstOrder.UFormula.equivW_symm_false_inr_inr_inr {L : LO.FirstOrder.Language} {μ : Type v} (v : Unit → WType (LO.FirstOrder.UFormula.Edge L μ)) : (LO.FirstOrder.UFormula.equivW L μ).symm (WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) v) = ((LO.FirstOrder.UFormula.equivW L μ).symm (v ())).ex

instance LO.FirstOrder.UFormula.instFintypeEdge {L : LO.FirstOrder.Language} {μ : Type v} (a : LO.FirstOrder.UFormula.Node L μ) : Fintype (LO.FirstOrder.UFormula.Edge L μ a)

Equations

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

instance LO.FirstOrder.UFormula.instPrimcodableEdge {L : LO.FirstOrder.Language} {μ : Type v} (a : LO.FirstOrder.UFormula.Node L μ) : Primcodable (LO.FirstOrder.UFormula.Edge L μ a)

Equations

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

instance LO.FirstOrder.UFormula.instDecidableEqEdge {L : LO.FirstOrder.Language} {μ : Type v} (a : LO.FirstOrder.UFormula.Node L μ) : DecidableEq (LO.FirstOrder.UFormula.Edge L μ a)

Equations

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

instance LO.FirstOrder.UFormula.instPrimrecCardNodeEdge {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : PrimrecCard (LO.FirstOrder.UFormula.Edge L μ)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.UFormula.primcodable {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primcodable (LO.FirstOrder.UFormula L μ)

Equations

• LO.FirstOrder.UFormula.primcodable = Primcodable.ofEquiv (WType (LO.FirstOrder.UFormula.Edge L μ)) (LO.FirstOrder.UFormula.equivW L μ)

theorem LO.FirstOrder.UFormula.qeq {α : Sort u_1} {a : α} {b : α} {c : α} {d : α} (h₁ : a = b) (h₂ : b = c) (h₃ : c = d) : a = d

theorem LO.FirstOrder.UFormula.encode_rel {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) : Encodable.encode (LO.FirstOrder.UFormula.rel r v) = Nat.pair 1 (Nat.pair (Nat.pair 1 ((2 * Nat.pair k) (Nat.pair (Encodable.encode r) (Encodable.encode v)))) 0)

theorem LO.FirstOrder.UFormula.encode_nrel {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) : Encodable.encode (LO.FirstOrder.UFormula.nrel r v) = Nat.pair 1 (Nat.pair (Nat.pair 0 ((2 * Nat.pair k) (Nat.pair (Encodable.encode r) (Encodable.encode v)))) 0)

theorem LO.FirstOrder.UFormula.rel_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec fun (p : (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ)) => LO.FirstOrder.UFormula.rel p.snd.1 p.snd.2

theorem LO.FirstOrder.UFormula.nrel_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec fun (p : (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ)) => LO.FirstOrder.UFormula.nrel p.snd.1 p.snd.2

def LO.FirstOrder.UFormula.relL {L : LO.FirstOrder.Language} {μ : Type v} (r : (k : ℕ) × L.Rel k) (l : List (LO.FirstOrder.UTerm L μ)) : Option (LO.FirstOrder.UFormula L μ)

Equations

• LO.FirstOrder.UFormula.relL r l = if h : l.length = r.fst then some (LO.FirstOrder.UFormula.rel r.snd fun (i : Fin r.fst) => l.get (Fin.cast ⋯ i)) else none

def LO.FirstOrder.UFormula.nrelL {L : LO.FirstOrder.Language} {μ : Type v} (r : (k : ℕ) × L.Rel k) (l : List (LO.FirstOrder.UTerm L μ)) : Option (LO.FirstOrder.UFormula L μ)

Equations

• LO.FirstOrder.UFormula.nrelL r l = if h : l.length = r.fst then some (LO.FirstOrder.UFormula.nrel r.snd fun (i : Fin r.fst) => l.get (Fin.cast ⋯ i)) else none

theorem LO.FirstOrder.UFormula.relL_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec₂ LO.FirstOrder.UFormula.relL

theorem LO.FirstOrder.UFormula.nrelL_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec₂ LO.FirstOrder.UFormula.nrelL

theorem LO.FirstOrder.UFormula.and_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec₂ LO.FirstOrder.UFormula.and

theorem LO.FirstOrder.UFormula.or_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec₂ LO.FirstOrder.UFormula.or

theorem LO.FirstOrder.UFormula.all_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec LO.FirstOrder.UFormula.all

theorem LO.FirstOrder.UFormula.ex_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec LO.FirstOrder.UFormula.ex

theorem LO.FirstOrder.UFormula.elim_primrec_param {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] {σ : Type u_1} {γ : Type u_2} [Primcodable σ] [Primcodable γ] [Inhabited γ] {γVerum : σ → γ} {γFalsum : σ → γ} {γRel : σ → (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ) → γ} {γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ) → γ} {γAnd : σ → γ × γ → γ} {γOr : σ → γ × γ → γ} {γAll : σ → γ → γ} {γEx : σ → γ → γ} {f : σ → LO.FirstOrder.UFormula L μ} (hVerum : Primrec γVerum) (hFalsum : Primrec γFalsum) (hRel : Primrec₂ γRel) (hNrel : Primrec₂ γNrel) (hAnd : Primrec₂ γAnd) (hOr : Primrec₂ γOr) (hAll : Primrec₂ γAll) (hEx : Primrec₂ γEx) (hf : Primrec f) : Primrec fun (x : σ) => LO.FirstOrder.UFormula.elim (γVerum x) (γFalsum x) (fun {k : ℕ} (f : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) => γRel x ⟨k, (f, v)⟩) (fun {k : ℕ} (f : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) => γNrel x ⟨k, (f, v)⟩) (fun (y₁ y₂ : γ) => γAnd x (y₁, y₂)) (fun (y₁ y₂ : γ) => γOr x (y₁, y₂)) (γAll x) (γEx x) (f x)

theorem LO.FirstOrder.UFormula.elim_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] {γ : Type u_1} [Primcodable γ] [Inhabited γ] (γVerum : γ) (γFalsum : γ) {γRel : (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ) → γ} {γNrel : (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.UTerm L μ) → γ} {γAnd : γ → γ → γ} {γOr : γ → γ → γ} {γAll : γ → γ} {γEx : γ → γ} (hRel : Primrec γRel) (hNrel : Primrec γNrel) (hAnd : Primrec₂ γAnd) (hOr : Primrec₂ γOr) (hAll : Primrec γAll) (hEx : Primrec γEx) : Primrec (LO.FirstOrder.UFormula.elim γVerum γFalsum (fun {k : ℕ} (f : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) => γRel ⟨k, (f, v)⟩) (fun {k : ℕ} (f : L.Rel k) (v : Fin k → LO.FirstOrder.UTerm L μ) => γNrel ⟨k, (f, v)⟩) γAnd γOr γAll γEx)

theorem LO.FirstOrder.UFormula.bv_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec LO.FirstOrder.UFormula.bv

theorem LO.FirstOrder.UFormula.depth_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec LO.FirstOrder.UFormula.depth

theorem LO.FirstOrder.UFormula.neg_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec LO.FirstOrder.UFormula.neg

def LO.FirstOrder.UFormula.inversion {L : LO.FirstOrder.Language} {μ : Type v} : LO.FirstOrder.UFormula L μ → LO.FirstOrder.UFormula.Node L μ × List (LO.FirstOrder.UFormula L μ)

Equations

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

theorem LO.FirstOrder.UFormula.inversion_primrec {L : LO.FirstOrder.Language} {μ : Type v} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] [Primcodable μ] : Primrec LO.FirstOrder.UFormula.inversion

theorem LO.FirstOrder.UFormula.bindq_param_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] {σ : Type u_1} {μ₁ : Type u_2} {μ₂ : Type u_3} [Primcodable μ₁] [Primcodable μ₂] [Primcodable σ] {b : σ → ℕ → LO.FirstOrder.UTerm L μ₂} {e : σ → μ₁ → LO.FirstOrder.UTerm L μ₂} {k : σ → ℕ} {p : σ → LO.FirstOrder.UFormula L μ₁} (hb : Primrec₂ b) (he : Primrec₂ e) (hk : Primrec k) (hp : Primrec p) : Primrec fun (x : σ) => LO.FirstOrder.UFormula.bindq (b x) (e x) (k x) (p x)

theorem LO.FirstOrder.UFormula.bind_primrec_param {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] {σ : Type u_1} {μ₁ : Type u_2} {μ₂ : Type u_3} [Primcodable μ₁] [Primcodable μ₂] [Primcodable σ] {b : σ → ℕ → LO.FirstOrder.UTerm L μ₂} {e : σ → μ₁ → LO.FirstOrder.UTerm L μ₂} {p : σ → LO.FirstOrder.UFormula L μ₁} (hb : Primrec₂ b) (he : Primrec₂ e) (hp : Primrec p) : Primrec fun (x : σ) => LO.FirstOrder.UFormula.bind (b x) (e x) (p x)

instance LO.FirstOrder.Semiformula.instPrimcodable {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primcodable (LO.FirstOrder.Semiformula L μ n)

Equations

• LO.FirstOrder.Semiformula.instPrimcodable = Primcodable.ofEquiv { p : LO.FirstOrder.UFormula L μ // p.bv ≤ n } LO.FirstOrder.UFormula.subfEquiv

theorem LO.FirstOrder.Semiformula.rel_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec fun (p : (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.Semiterm L μ n)) => LO.FirstOrder.Semiformula.rel p.snd.1 p.snd.2

theorem LO.FirstOrder.Semiformula.nrel_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec fun (p : (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.Semiterm L μ n)) => LO.FirstOrder.Semiformula.nrel p.snd.1 p.snd.2

def LO.FirstOrder.Semiformula.relL {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (r : (k : ℕ) × L.Rel k) (l : List (LO.FirstOrder.Semiterm L μ n)) : Option (LO.FirstOrder.Semiformula L μ n)

Equations

• LO.FirstOrder.Semiformula.relL r l = if h : l.length = r.fst then some (LO.FirstOrder.Semiformula.rel r.snd fun (i : Fin r.fst) => l.get (Fin.cast ⋯ i)) else none

def LO.FirstOrder.Semiformula.nrelL {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (r : (k : ℕ) × L.Rel k) (l : List (LO.FirstOrder.Semiterm L μ n)) : Option (LO.FirstOrder.Semiformula L μ n)

Equations

• LO.FirstOrder.Semiformula.nrelL r l = if h : l.length = r.fst then some (LO.FirstOrder.Semiformula.nrel r.snd fun (i : Fin r.fst) => l.get (Fin.cast ⋯ i)) else none

theorem LO.FirstOrder.Semiformula.relL_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec₂ LO.FirstOrder.Semiformula.relL

theorem LO.FirstOrder.Semiformula.nrelL_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec₂ LO.FirstOrder.Semiformula.nrelL

theorem LO.FirstOrder.Semiformula.and_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec₂ fun (x x_1 : LO.FirstOrder.Semiformula L μ n) => x ⋏ x_1

theorem LO.FirstOrder.Semiformula.or_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec₂ fun (x x_1 : LO.FirstOrder.Semiformula L μ n) => x ⋎ x_1

theorem LO.FirstOrder.Semiformula.all_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec fun (x : LO.FirstOrder.Semiformula L μ (n + 1)) => ∀' x

theorem LO.FirstOrder.Semiformula.ex_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec fun (x : LO.FirstOrder.Semiformula L μ (n + 1)) => ∃' x

theorem LO.FirstOrder.Semiformula.neg_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec fun (x : LO.FirstOrder.Semiformula L μ n) => ~x

theorem LO.FirstOrder.Semiformula.imply_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec₂ fun (x x_1 : LO.FirstOrder.Semiformula L μ n) => x ⟶ x_1

theorem LO.FirstOrder.Semiformula.bv_subtEquiv {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (p : LO.FirstOrder.Semiformula L μ n) : (↑(LO.FirstOrder.UFormula.subfEquiv p)).bv ≤ n

theorem LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind {L : LO.FirstOrder.Language} {n₁ : ℕ} {μ₂ : Type u_2} {n₂ : ℕ} {μ₁ : Type u_3} (b : Fin n₁ → LO.FirstOrder.Semiterm L μ₂ n₂) (e : μ₁ → LO.FirstOrder.Semiterm L μ₂ n₂) (p : LO.FirstOrder.Semiformula L μ₁ n₁) : ↑(LO.FirstOrder.UFormula.subfEquiv ((LO.FirstOrder.Rew.bind b e).hom p)) = LO.FirstOrder.UFormula.bind (fun (x : ℕ) => if hx : x < n₁ then ↑(LO.FirstOrder.UTerm.subtEquiv (b ⟨x, hx⟩)) else default) (fun (x : μ₁) => ↑(LO.FirstOrder.UTerm.subtEquiv (e x))) ↑(LO.FirstOrder.UFormula.subfEquiv p)

theorem LO.FirstOrder.Semiformula.bind_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {σ : Type u_2} {μ₁ : Type u_3} {μ₂ : Type u_4} [Primcodable μ₁] [Primcodable μ₂] [Primcodable σ] {n₁ : ℕ} {n₂ : ℕ} {b : σ → Fin n₁ → LO.FirstOrder.Semiterm L μ₂ n₂} {e : σ → μ₁ → LO.FirstOrder.Semiterm L μ₂ n₂} {p : σ → LO.FirstOrder.Semiformula L μ₁ n₁} (hb : Primrec b) (he : Primrec₂ e) (hp : Primrec p) : Primrec fun (x : σ) => (LO.FirstOrder.Rew.bind (b x) (e x)).hom (p x)

theorem LO.FirstOrder.Semiformula.rewrite_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {k : ℕ} {n : ℕ} : Primrec₂ fun (v : Fin k → LO.FirstOrder.Semiterm L μ n) (p : LO.FirstOrder.Semiformula L (Fin k) n) => (LO.FirstOrder.Rew.rewrite v).hom p

theorem LO.FirstOrder.Semiformula.substs_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} {n' : ℕ} : Primrec₂ fun (v : Fin n → LO.FirstOrder.Semiterm L μ n') (p : LO.FirstOrder.Semiformula L μ n) => (LO.FirstOrder.Rew.substs v).hom p

theorem LO.FirstOrder.Semiformula.substs₁_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n' : ℕ} : Primrec₂ fun (t : LO.FirstOrder.Semiterm L μ n') (p : LO.FirstOrder.Semiformula L μ 1) => (LO.FirstOrder.Rew.substs ![t]).hom p

theorem LO.FirstOrder.Semiformula.shift_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec ⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)

theorem LO.FirstOrder.Semiformula.free_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] {n : ℕ} : Primrec ⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free)

theorem LO.FirstOrder.Semiformula.emb_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Rel] : Primrec ⇑LO.FirstOrder.Rew.emb.hom