def LO.FirstOrder.Semiterm.toNat {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} : LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] (n : ℕ) : ℕ → Option (LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.ofNat n t.toNat = some t

instance LO.FirstOrder.Semiterm.encodable {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} : Encodable (LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} : LO.FirstOrder.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
• (p.and q).toNat = Nat.pair 4 (Nat.pair p.toNat q.toNat) + 1
• (p.or q).toNat = Nat.pair 5 (Nat.pair p.toNat q.toNat) + 1
• p.all.toNat = Nat.pair 6 p.toNat + 1
• p.ex.toNat = Nat.pair 7 p.toNat + 1

@[irreducible]

def LO.FirstOrder.Semiformula.ofNat {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] (n : ℕ) : ℕ → Option (LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : LO.FirstOrder.Semiformula.ofNat n p.toNat = some p

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

Equations

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