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 := ⋯ }

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
• φ.ex.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 := ⋯ }