def FirstOrder.Language.Term.encode {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} : L.Term n → ℕ

Equations

• (#x_1).encode = 2 * ↑x_1
• (f ⬝ᶠ v).encode = 2 * Nat.pair m (Nat.pair (Encodable.encode f) (Vec.paired fun (i : Fin m) => (v i).encode)) + 1

@[irreducible]

def FirstOrder.Language.Term.decode {L : Language} [(n : ℕ) → Encodable (L.Func n)] (n k : ℕ) : Option (L.Term n)

Equations

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

@[irreducible]

def FirstOrder.Language.Term.decodeVec {L : Language} [(n : ℕ) → Encodable (L.Func n)] (n k m : ℕ) : Option (Vec (L.Term n) m)

Equations

• FirstOrder.Language.Term.decodeVec n k 0 = if k = 0 then some []ᵥ else none
• FirstOrder.Language.Term.decodeVec n k m.succ = do let t ← FirstOrder.Language.Term.decode n (Nat.unpair k).1 let v ← FirstOrder.Language.Term.decodeVec n (Nat.unpair k).2 m some (t ∷ᵥ v)

theorem FirstOrder.Language.Term.encode_decode {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {t : L.Term n} : decode n t.encode = some t

instance FirstOrder.Language.instEncodableTerm {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} : Encodable (L.Term n)

Equations

• FirstOrder.Language.instEncodableTerm = { encode := FirstOrder.Language.Term.encode, decode := FirstOrder.Language.Term.decode n, encodek := ⋯ }

instance FirstOrder.Language.instEncodableSubst {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} : Encodable (L.Subst n m)

Equations

• FirstOrder.Language.instEncodableSubst = Vec.encodable

theorem FirstOrder.Language.Term.encode_var {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {x : Fin n} : Encodable.encode #x = 2 * ↑x

theorem FirstOrder.Language.Term.encode_func {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {f : L.Func m} {v : Vec (L.Term n) m} : Encodable.encode (f ⬝ᶠ v) = 2 * Nat.pair m (Nat.pair (Encodable.encode f) (Encodable.encode v)) + 1

theorem FirstOrder.Language.Subst.encode_eq {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {σ : L.Subst n m} : Encodable.encode σ = Vec.paired fun (i : Fin n) => Encodable.encode (σ i)

theorem FirstOrder.Language.Term.encode_lt_func_m {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {f : L.Func m} {v : Vec (L.Term n) m} : m < Encodable.encode (f ⬝ᶠ v)

theorem FirstOrder.Language.Term.encode_lt_func_f {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {f : L.Func m} {v : Vec (L.Term n) m} : Encodable.encode f < Encodable.encode (f ⬝ᶠ v)

theorem FirstOrder.Language.Term.encode_lt_func_v {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {f : L.Func m} {v : Vec (L.Term n) m} : Encodable.encode v < Encodable.encode (f ⬝ᶠ v)

theorem FirstOrder.Language.Term.encode_le_subst {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {x : Fin n} {m✝ : ℕ} {σ : L.Subst n m✝} {t : L.Term n} : x ∈ t.vars → Encodable.encode (σ x) ≤ Encodable.encode t[σ]ₜ

theorem FirstOrder.Language.Term.encode_subst_le_subst {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m✝ : ℕ} {σ₁ : L.Subst n m✝} {m✝¹ : ℕ} {σ₂ : L.Subst n m✝¹} {t : L.Term n} : (∀ (x : Fin n), Encodable.encode (σ₁ x) ≤ Encodable.encode (σ₂ x)) → Encodable.encode t[σ₁]ₜ ≤ Encodable.encode t[σ₂]ₜ

theorem FirstOrder.Language.Term.encode_le_shift {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {t : L.Term n} : Encodable.encode t ≤ Encodable.encode ↑ₜt

def FirstOrder.Language.Formula.encode {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} : L.Formula n → ℕ

Equations

• (r ⬝ʳ v).encode = 4 * Nat.pair m (Nat.pair (Encodable.encode r) (Vec.paired fun (i : Fin m) => (v i).encode)) + 1
• (t₁ ≐ t₂).encode = 4 * Nat.pair t₁.encode t₂.encode + 2
• FirstOrder.Language.Formula.false.encode = 0
• (p.imp q).encode = 4 * Nat.pair p.encode q.encode + 3
• (∀' p).encode = 4 * p.encode + 4

@[irreducible]

def FirstOrder.Language.Formula.decode {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] (n k : ℕ) : Option (L.Formula n)

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.Formula.decode n 0 = some ⊥

theorem FirstOrder.Language.Formula.encode_decode {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : decode n p.encode = some p

instance FirstOrder.Language.instEncodableFormula {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} : Encodable (L.Formula n)

Equations

• FirstOrder.Language.instEncodableFormula = { encode := FirstOrder.Language.Formula.encode, decode := FirstOrder.Language.Formula.decode n, encodek := ⋯ }

theorem FirstOrder.Language.Formula.encode_rel {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {r : L.Rel m} {v : Vec (L.Term n) m} : Encodable.encode (r ⬝ʳ v) = 4 * Nat.pair m (Nat.pair (Encodable.encode r) (Encodable.encode v)) + 1

theorem FirstOrder.Language.Formula.encode_eq {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {t₁ t₂ : L.Term n} : Encodable.encode (t₁ ≐ t₂) = 4 * Nat.pair (Encodable.encode t₁) (Encodable.encode t₂) + 2

theorem FirstOrder.Language.Formula.encode_false {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} : Encodable.encode ⊥ = 0

theorem FirstOrder.Language.Formula.encode_imp {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : Encodable.encode (p ⇒ q) = 4 * Nat.pair (Encodable.encode p) (Encodable.encode q) + 3

theorem FirstOrder.Language.Formula.encode_all {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula (n + 1)} : Encodable.encode (∀' p) = 4 * Encodable.encode p + 4

theorem FirstOrder.Language.Formula.encode_lt_rel_m {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {r : L.Rel m} {v : Vec (L.Term n) m} : m < Encodable.encode (r ⬝ʳ v)

theorem FirstOrder.Language.Formula.encode_lt_rel_r {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {r : L.Rel m} {v : Vec (L.Term n) m} : Encodable.encode r < Encodable.encode (r ⬝ʳ v)

theorem FirstOrder.Language.Formula.encode_lt_rel_v {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {r : L.Rel m} {v : Vec (L.Term n) m} : Encodable.encode v < Encodable.encode (r ⬝ʳ v)

theorem FirstOrder.Language.Formula.encode_lt_eq_left {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {t₁ t₂ : L.Term n} : Encodable.encode t₁ < Encodable.encode (t₁ ≐ t₂)

theorem FirstOrder.Language.Formula.encode_lt_eq_right {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {t₁ t₂ : L.Term n} : Encodable.encode t₂ < Encodable.encode (t₁ ≐ t₂)

theorem FirstOrder.Language.Formula.encode_lt_imp_left {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : Encodable.encode p < Encodable.encode (p ⇒ q)

theorem FirstOrder.Language.Formula.encode_lt_imp_right {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : Encodable.encode q < Encodable.encode (p ⇒ q)

theorem FirstOrder.Language.Formula.encode_lt_all {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula (n + 1)} : Encodable.encode p < Encodable.encode (∀' p)

theorem FirstOrder.Language.Formula.encode_le_alls {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : Encodable.encode p + n ≤ Encodable.encode (∀* p)

theorem FirstOrder.Language.Formula.encode_le_alls_n {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : n ≤ Encodable.encode (∀* p)

theorem FirstOrder.Language.Formula.encode_le_alls_p {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : Encodable.encode p ≤ Encodable.encode (∀* p)

theorem FirstOrder.Language.Formula.encode_le_subst {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {x : Fin n} {p : L.Formula n} {σ : L.Subst n m} : x ∈ p.free → Encodable.encode (σ x) ≤ Encodable.encode p[σ]ₚ

theorem FirstOrder.Language.Formula.encode_le_subst_single {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {t : L.Term n} {p : L.Formula (n + 1)} : 0 ∈ p.free → Encodable.encode t ≤ Encodable.encode p[↦ₛ t]ₚ

class FirstOrder.Language.HasConstEncodeZero (L : Language) [Encodable L.Const] : Prop

• hasConstEncodeZero : ∃ (r : L.Const), Encodable.encode r = 0

theorem FirstOrder.Language.Formula.exists_encode_le_succ_subst_single {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} [L.HasConstEncodeZero] {p : L.Formula (n + 1)} {t : L.Term n} : ∃ (t' : L.Term n), p[↦ₛ t]ₚ = p[↦ₛ t']ₚ ∧ Encodable.encode t' ≤ Encodable.encode p[↦ₛ t]ₚ + 1

noncomputable def FirstOrder.Language.instEncodableFunc {L : Language} [∀ (n : ℕ), Countable (L.Func n)] {n : ℕ} : Encodable (L.Func n)

Equations

• FirstOrder.Language.instEncodableFunc = Encodable.ofCountable (L.Func n)

noncomputable def FirstOrder.Language.instEncodableRel {L : Language} [∀ (n : ℕ), Countable (L.Rel n)] {n : ℕ} : Encodable (L.Rel n)

Equations

• FirstOrder.Language.instEncodableRel = Encodable.ofCountable (L.Rel n)

instance FirstOrder.Language.instCountableTerm {L : Language} [∀ (n : ℕ), Countable (L.Func n)] {n : ℕ} : Countable (L.Term n)

instance FirstOrder.Language.instCountableFormula {L : Language} [∀ (n : ℕ), Countable (L.Func n)] [∀ (n : ℕ), Countable (L.Rel n)] {n : ℕ} : Countable (L.Formula n)