def LO.FirstOrder.Semiterm.toNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} : Semiterm L ξ n → ℕ

Equations

• (LO.FirstOrder.Semiterm.bvar z).toNat = Nat.pair 0 ↑z + 1
• (LO.FirstOrder.Semiterm.fvar x_1).toNat = Nat.pair 1 (Encodable.encode x_1) + 1
• (LO.FirstOrder.Semiterm.func f v).toNat = Nat.pair 2 (Nat.pair arity (Nat.pair (Encodable.encode f) (Matrix.vecToNat fun (i : Fin arity) => (v i).toNat))) + 1

@[irreducible]

def LO.FirstOrder.Semiterm.ofNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] (n a✝ : ℕ) : Option (Semiterm L ξ n)

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiterm.ofNat n 0 = none

theorem LO.FirstOrder.Semiterm.ofNat_toNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (t : Semiterm L ξ n) : ofNat n t.toNat = some t

instance LO.FirstOrder.Semiterm.encodable {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} : Encodable (Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.encodable = { encode := LO.FirstOrder.Semiterm.toNat, decode := LO.FirstOrder.Semiterm.ofNat n, encodek := ⋯ }

theorem LO.FirstOrder.Semiterm.encode_eq_toNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (t : Semiterm L ξ n) : Encodable.encode t = t.toNat

theorem LO.FirstOrder.Semiterm.toNat_func {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).toNat = Nat.pair 2 (Nat.pair k (Nat.pair (Encodable.encode f) (Matrix.vecToNat fun (i : Fin k) => (v i).toNat))) + 1

@[simp]

theorem LO.FirstOrder.Semiterm.encode_emb {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (t : ClosedSemiterm L n) : Encodable.encode (Rew.emb t) = Encodable.encode t

def LO.FirstOrder.Semiformula.toNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} : Semiformula L ξ n → ℕ

Equations

• (LO.FirstOrder.Semiformula.rel R v).toNat = Nat.pair 0 (Nat.pair arity (Nat.pair (Encodable.encode R) (Matrix.vecToNat fun (i : Fin arity) => Encodable.encode (v i)))) + 1
• (LO.FirstOrder.Semiformula.nrel R v).toNat = Nat.pair 1 (Nat.pair arity (Nat.pair (Encodable.encode R) (Matrix.vecToNat fun (i : Fin arity) => Encodable.encode (v i)))) + 1
• LO.FirstOrder.Semiformula.verum.toNat = Nat.pair 2 0 + 1
• LO.FirstOrder.Semiformula.falsum.toNat = Nat.pair 3 0 + 1
• (φ.and ψ).toNat = Nat.pair 4 (Nat.pair φ.toNat ψ.toNat) + 1
• (φ.or ψ).toNat = Nat.pair 5 (Nat.pair φ.toNat ψ.toNat) + 1
• φ.all.toNat = Nat.pair 6 φ.toNat + 1
• φ.exs.toNat = Nat.pair 7 φ.toNat + 1

@[irreducible]

def LO.FirstOrder.Semiformula.ofNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] (n a✝ : ℕ) : Option (Semiformula L ξ n)

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiformula.ofNat x✝ 0 = none

theorem LO.FirstOrder.Semiformula.ofNat_toNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semiformula L ξ n) : ofNat n φ.toNat = some φ

instance LO.FirstOrder.Semiformula.encodable {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} : Encodable (Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.encodable = { encode := LO.FirstOrder.Semiformula.toNat, decode := LO.FirstOrder.Semiformula.ofNat n, encodek := ⋯ }

theorem LO.FirstOrder.Semiformula.encode_eq_toNat {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semiformula L ξ n) : Encodable.encode φ = φ.toNat

theorem LO.FirstOrder.Semiformula.encode_rel {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n arity : ℕ} (R : L.Rel arity) (v : Fin arity → Semiterm L ξ n) : Encodable.encode (rel R v) = Nat.pair 0 (Nat.pair arity (Nat.pair (Encodable.encode R) (Matrix.vecToNat fun (i : Fin arity) => Encodable.encode (v i)))) + 1

theorem LO.FirstOrder.Semiformula.encode_nrel {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n arity : ℕ} (R : L.Rel arity) (v : Fin arity → Semiterm L ξ n) : Encodable.encode (nrel R v) = Nat.pair 1 (Nat.pair arity (Nat.pair (Encodable.encode R) (Matrix.vecToNat fun (i : Fin arity) => Encodable.encode (v i)))) + 1

theorem LO.FirstOrder.Semiformula.encode_verum {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} : Encodable.encode ⊤ = Nat.pair 2 0 + 1

theorem LO.FirstOrder.Semiformula.encode_falsum {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} : Encodable.encode ⊥ = Nat.pair 3 0 + 1

theorem LO.FirstOrder.Semiformula.encode_and {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ ψ : Semiformula L ξ n) : Encodable.encode (φ ⋏ ψ) = Nat.pair 4 (Nat.pair φ.toNat ψ.toNat) + 1

theorem LO.FirstOrder.Semiformula.encode_or {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ ψ : Semiformula L ξ n) : Encodable.encode (φ ⋎ ψ) = Nat.pair 5 (Nat.pair φ.toNat ψ.toNat) + 1

theorem LO.FirstOrder.Semiformula.encode_all {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semiformula L ξ (n + 1)) : Encodable.encode (∀⁰ φ) = Nat.pair 6 φ.toNat + 1

theorem LO.FirstOrder.Semiformula.encode_ex {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semiformula L ξ (n + 1)) : Encodable.encode (∃⁰ φ) = Nat.pair 7 φ.toNat + 1

@[simp]

theorem LO.FirstOrder.Semiformula.encode_emb {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (σ : Semisentence L n) : Encodable.encode ↑σ = Encodable.encode σ

@[simp]

theorem LO.FirstOrder.Semiformula.encode_inj_sentence {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} {σ : Semisentence L n} {φ : Semiformula L ξ n} : Encodable.encode φ = Encodable.encode σ ↔ φ = ↑σ

@[simp]

theorem LO.FirstOrder.Semiformula.encode_inj_sentence' {L : Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} {σ : Semisentence L n} {φ : Semiformula L ξ n} : Encodable.encode σ = Encodable.encode φ ↔ φ = ↑σ

instance LO.FirstOrder.Semiterm.countable {ξ : Type u_1} {L : Language} [L.Encodable] {n : ℕ} [Countable ξ] : Countable (Semiterm L ξ n)

instance LO.FirstOrder.Semiformula.countable {ξ : Type u_1} {L : Language} [L.Encodable] {n : ℕ} [Countable ξ] : Countable (Semiformula L ξ n)