Logic.FirstOrder.Computability.Term

source

inductive LO.FirstOrder.UTerm (L : LO.FirstOrder.Language) (μ : Type v) :

Type (max u v)

bvar: {L : LO.FirstOrder.Language} → {μ : Type v} → ℕ → LO.FirstOrder.UTerm L μ
fvar: {L : LO.FirstOrder.Language} → {μ : Type v} → μ → LO.FirstOrder.UTerm L μ
func: {L : LO.FirstOrder.Language} → {μ : Type v} → {arity : ℕ} → L.Func arity → (Fin arity → LO.FirstOrder.UTerm L μ) → LO.FirstOrder.UTerm L μ

Instances For

source

instance LO.FirstOrder.UTerm.instInhabited {L : LO.FirstOrder.Language} {μ : Type v} :

Inhabited (LO.FirstOrder.UTerm L μ)

Equations

LO.FirstOrder.UTerm.instInhabited = { default := LO.FirstOrder.UTerm.bvar 0 }

source

def LO.FirstOrder.UTerm.elim {L : LO.FirstOrder.Language} {μ : Type v} {γ : Type u_1} (b : ℕ → γ) (e : μ → γ) (u : {k : ℕ} → L.Func k → (Fin k → γ) → γ) :

LO.FirstOrder.UTerm L μ → γ

Equations

LO.FirstOrder.UTerm.elim b e u (LO.FirstOrder.UTerm.bvar x_1) = b x_1
LO.FirstOrder.UTerm.elim b e u (LO.FirstOrder.UTerm.fvar x_1) = e x_1
LO.FirstOrder.UTerm.elim b e u (LO.FirstOrder.UTerm.func f v) = u f fun (i : Fin arity) => LO.FirstOrder.UTerm.elim b e (fun {k : ℕ} => u) (v i)

Instances For

source

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

LO.FirstOrder.UTerm L μ₁ → LO.FirstOrder.UTerm L μ₂

Equations

LO.FirstOrder.UTerm.bind b e (LO.FirstOrder.UTerm.bvar x_1) = b x_1
LO.FirstOrder.UTerm.bind b e (LO.FirstOrder.UTerm.fvar x_1) = e x_1
LO.FirstOrder.UTerm.bind b e (LO.FirstOrder.UTerm.func f v) = LO.FirstOrder.UTerm.func f fun (i : Fin arity) => LO.FirstOrder.UTerm.bind b e (v i)

Instances For

source

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

LO.FirstOrder.UTerm L μ₁ → LO.FirstOrder.UTerm L μ₂

Equations

LO.FirstOrder.UTerm.rewrite e = LO.FirstOrder.UTerm.bind LO.FirstOrder.UTerm.bvar e

Instances For

source

def LO.FirstOrder.UTerm.bShifts {L : LO.FirstOrder.Language} {μ : Type v} (k : ℕ) :

LO.FirstOrder.UTerm L μ → LO.FirstOrder.UTerm L μ

Equations

LO.FirstOrder.UTerm.bShifts k = LO.FirstOrder.UTerm.bind (fun (x : ℕ) => LO.FirstOrder.UTerm.bvar (x + k)) LO.FirstOrder.UTerm.fvar

Instances For

source

@[simp]

theorem LO.FirstOrder.UTerm.bShifts_zero {L : LO.FirstOrder.Language} {μ : Type v} (t : LO.FirstOrder.UTerm L μ) :

LO.FirstOrder.UTerm.bShifts 0 t = t

source

theorem LO.FirstOrder.UTerm.bind_bind {L : LO.FirstOrder.Language} {μ₂ : Type u_1} {μ₁ : Type u_2} {μ₃ : Type u_3} {t : LO.FirstOrder.UTerm L μ₁} (b₁ : ℕ → LO.FirstOrder.UTerm L μ₂) (e₁ : μ₁ → LO.FirstOrder.UTerm L μ₂) (b₂ : ℕ → LO.FirstOrder.UTerm L μ₃) (e₂ : μ₂ → LO.FirstOrder.UTerm L μ₃) :

LO.FirstOrder.UTerm.bind b₂ e₂ (LO.FirstOrder.UTerm.bind b₁ e₁ t) = LO.FirstOrder.UTerm.bind (fun (x : ℕ) => LO.FirstOrder.UTerm.bind b₂ e₂ (b₁ x)) (fun (x : μ₁) => LO.FirstOrder.UTerm.bind b₂ e₂ (e₁ x)) t

source

@[simp]

theorem LO.FirstOrder.UTerm.bShifts_bShifts {L : LO.FirstOrder.Language} {μ : Type v} (t : LO.FirstOrder.UTerm L μ) (m₁ : ℕ) (m₂ : ℕ) :

LO.FirstOrder.UTerm.bShifts m₂ (LO.FirstOrder.UTerm.bShifts m₁ t) = LO.FirstOrder.UTerm.bShifts (m₁ + m₂) t

source

def LO.FirstOrder.UTerm.substAt {L : LO.FirstOrder.Language} {μ : Type v} (z : ℕ) (t : LO.FirstOrder.UTerm L μ) :

LO.FirstOrder.UTerm L μ → LO.FirstOrder.UTerm L μ

Equations

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

Instances For

source

def LO.FirstOrder.UTerm.bv {L : LO.FirstOrder.Language} {μ : Type v} :

LO.FirstOrder.UTerm L μ → ℕ

Equations

(LO.FirstOrder.UTerm.bvar x_1).bv = x_1 + 1
(LO.FirstOrder.UTerm.fvar x_1).bv = 0
(LO.FirstOrder.UTerm.func f v).bv = Finset.univ.sup fun (i : Fin arity) => (v i).bv

Instances For

source

def LO.FirstOrder.UTerm.substLast {L : LO.FirstOrder.Language} {μ : Type v} (u : LO.FirstOrder.UTerm L μ) :

LO.FirstOrder.UTerm L μ → LO.FirstOrder.UTerm L μ

Equations

u.substLast t = LO.FirstOrder.UTerm.substAt t.bv.pred u t

Instances For

source

@[simp]

theorem LO.FirstOrder.UTerm.bv_bvar {L : LO.FirstOrder.Language} {μ : Type v} {x : ℕ} :

(LO.FirstOrder.UTerm.bvar x).bv = x + 1

source

@[simp]

theorem LO.FirstOrder.UTerm.bv_fvar {L : LO.FirstOrder.Language} {μ : Type v} {x : μ} :

(LO.FirstOrder.UTerm.fvar x).bv = 0

source

@[simp]

theorem LO.FirstOrder.UTerm.substAt_bvar {L : LO.FirstOrder.Language} {μ : Type v} (z : ℕ) (u : LO.FirstOrder.UTerm L μ) :

LO.FirstOrder.UTerm.substAt z u (LO.FirstOrder.UTerm.bvar z) = u

source

@[simp]

theorem LO.FirstOrder.UTerm.substAt_bvar_fin {L : LO.FirstOrder.Language} {μ : Type v} (z : ℕ) (u : LO.FirstOrder.UTerm L μ) (x : Fin z) :

LO.FirstOrder.UTerm.substAt z u (LO.FirstOrder.UTerm.bvar ↑x) = LO.FirstOrder.UTerm.bvar ↑x

source

@[simp]

theorem LO.FirstOrder.UTerm.substAt_fvar {L : LO.FirstOrder.Language} {μ : Type v} {x : μ} (z : ℕ) (u : LO.FirstOrder.UTerm L μ) :

LO.FirstOrder.UTerm.substAt z u (LO.FirstOrder.UTerm.fvar x) = LO.FirstOrder.UTerm.fvar x

source

@[simp]

theorem LO.FirstOrder.UTerm.substAt_func {L : LO.FirstOrder.Language} {μ : Type v} {z : ℕ} {u : LO.FirstOrder.UTerm L μ} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.UTerm L μ) :

LO.FirstOrder.UTerm.substAt z u (LO.FirstOrder.UTerm.func f v) = LO.FirstOrder.UTerm.func f fun (i : Fin k) => LO.FirstOrder.UTerm.substAt z u (v i)

source

@[simp]

theorem LO.FirstOrder.UTerm.subtype_val_bv_le {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (t : { t : LO.FirstOrder.UTerm L μ // t.bv ≤ n }) :

(↑t).bv ≤ n

source

theorem LO.FirstOrder.UTerm.bv_bind {L : LO.FirstOrder.Language} {μ₂ : Type u_1} {μ₁ : Type u_2} {m : ℕ} {b : ℕ → LO.FirstOrder.UTerm L μ₂} {e : μ₁ → LO.FirstOrder.UTerm L μ₂} (t : LO.FirstOrder.UTerm L μ₁) (hb : ∀ x < t.bv, (b x).bv ≤ m) (he : ∀ (x : μ₁), (e x).bv ≤ m) :

(LO.FirstOrder.UTerm.bind b e t).bv ≤ m

source

theorem LO.FirstOrder.UTerm.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 μ₂) (t : LO.FirstOrder.UTerm L μ₁) (hb : ∀ x < t.bv, b₁ x = b₂ x) (he : ∀ (x : μ₁), e₁ x = e₂ x) :

LO.FirstOrder.UTerm.bind b₁ e₁ t = LO.FirstOrder.UTerm.bind b₂ e₂ t

source

theorem LO.FirstOrder.UTerm.bv_rewrite {L : LO.FirstOrder.Language} {μ₁ : Type u_1} {μ₂ : Type u_2} {m : ℕ} {e : μ₁ → LO.FirstOrder.UTerm L μ₂} {t : LO.FirstOrder.UTerm L μ₁} (ht : t.bv ≤ m) (he : ∀ (x : μ₁), (e x).bv ≤ m) :

(LO.FirstOrder.UTerm.rewrite e t).bv ≤ m

source

theorem LO.FirstOrder.UTerm.bv_substLast {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} {t : LO.FirstOrder.UTerm L μ} {u : LO.FirstOrder.UTerm L μ} (ht : t.bv ≤ n + 1) (hu : u.bv ≤ n) :

(u.substLast t).bv ≤ n

source

def LO.FirstOrder.UTerm.toSubterm {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (t : LO.FirstOrder.UTerm L μ) :

t.bv ≤ n → LO.FirstOrder.Semiterm L μ n

Equations

(LO.FirstOrder.UTerm.bvar x_2).toSubterm h = LO.FirstOrder.Semiterm.bvar ⟨x_2, ⋯⟩
(LO.FirstOrder.UTerm.fvar x_2).toSubterm x_3 = LO.FirstOrder.Semiterm.fvar x_2
(LO.FirstOrder.UTerm.func f v).toSubterm h = LO.FirstOrder.Semiterm.func f fun (i : Fin arity) => (v i).toSubterm ⋯

Instances For

source

def LO.FirstOrder.UTerm.ofSubterm {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} :

LO.FirstOrder.Semiterm L μ n → { t : LO.FirstOrder.UTerm L μ // t.bv ≤ n }

Equations

LO.FirstOrder.UTerm.ofSubterm (LO.FirstOrder.Semiterm.bvar x_1) = ⟨LO.FirstOrder.UTerm.bvar ↑x_1, ⋯⟩
LO.FirstOrder.UTerm.ofSubterm (LO.FirstOrder.Semiterm.fvar x_1) = ⟨LO.FirstOrder.UTerm.fvar x_1, ⋯⟩
LO.FirstOrder.UTerm.ofSubterm (LO.FirstOrder.Semiterm.func f v) = ⟨LO.FirstOrder.UTerm.func f fun (i : Fin arity) => ↑(LO.FirstOrder.UTerm.ofSubterm (v i)), ⋯⟩

Instances For

source

theorem LO.FirstOrder.UTerm.toSubterm_ofSubterm {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (t : LO.FirstOrder.Semiterm L μ n) :

(↑(LO.FirstOrder.UTerm.ofSubterm t)).toSubterm ⋯ = t

source

theorem LO.FirstOrder.UTerm.ofSubterm_toSubterm {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (t : LO.FirstOrder.UTerm L μ) (h : t.bv ≤ n) :

↑(LO.FirstOrder.UTerm.ofSubterm (t.toSubterm h)) = t

source

def LO.FirstOrder.UTerm.subtEquiv {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} :

LO.FirstOrder.Semiterm L μ n ≃ { t : LO.FirstOrder.UTerm L μ // t.bv ≤ n }

Equations

LO.FirstOrder.UTerm.subtEquiv = { toFun := LO.FirstOrder.UTerm.ofSubterm, invFun := fun (t : { t : LO.FirstOrder.UTerm L μ // t.bv ≤ n }) => (↑t).toSubterm ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LO.FirstOrder.UTerm.subtEquiv_bvar {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (x : Fin n) :

LO.FirstOrder.UTerm.subtEquiv (LO.FirstOrder.Semiterm.bvar x) = ⟨LO.FirstOrder.UTerm.bvar ↑x, ⋯⟩

source

@[simp]

theorem LO.FirstOrder.UTerm.subtEquiv_fvar {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (x : μ) :

LO.FirstOrder.UTerm.subtEquiv (LO.FirstOrder.Semiterm.fvar x) = ⟨LO.FirstOrder.UTerm.fvar x, ⋯⟩

source

@[simp]

theorem LO.FirstOrder.UTerm.subtEquiv_func {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L μ n) :

LO.FirstOrder.UTerm.subtEquiv (LO.FirstOrder.Semiterm.func f v) = ⟨LO.FirstOrder.UTerm.func f fun (i : Fin k) => ↑(LO.FirstOrder.UTerm.subtEquiv (v i)), ⋯⟩

source

theorem LO.FirstOrder.UTerm.ofSubterm_eq_subtEquiv {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} :

LO.FirstOrder.UTerm.ofSubterm = ⇑LO.FirstOrder.UTerm.subtEquiv

source

@[reducible, inline]

abbrev LO.FirstOrder.UTerm.Node (L : LO.FirstOrder.Language) (μ : Type v) :

Type (max u v)

Equations

LO.FirstOrder.UTerm.Node L μ = (ℕ ⊕ μ ⊕ (k : ℕ) × L.Func k)

Instances For

source

@[reducible]

def LO.FirstOrder.UTerm.Edge (L : LO.FirstOrder.Language) (μ : Type v) :

LO.FirstOrder.UTerm.Node L μ → Type

Equations

LO.FirstOrder.UTerm.Edge L μ x = match x with | Sum.inl val => Empty | Sum.inr (Sum.inl val) => Empty | Sum.inr (Sum.inr ⟨k, snd⟩) => Fin k

Instances For

source

def LO.FirstOrder.UTerm.toW {L : LO.FirstOrder.Language} {μ : Type v} :

LO.FirstOrder.UTerm L μ → WType (LO.FirstOrder.UTerm.Edge L μ)

Equations

(LO.FirstOrder.UTerm.bvar x_1).toW = WType.mk (Sum.inl x_1) Empty.elim
(LO.FirstOrder.UTerm.fvar x_1).toW = WType.mk (Sum.inr (Sum.inl x_1)) Empty.elim
(LO.FirstOrder.UTerm.func f v).toW = WType.mk (Sum.inr (Sum.inr ⟨arity, f⟩)) fun (i : LO.FirstOrder.UTerm.Edge L μ (Sum.inr (Sum.inr ⟨arity, f⟩))) => (v i).toW

Instances For

source

def LO.FirstOrder.UTerm.ofW {L : LO.FirstOrder.Language} {μ : Type v} :

WType (LO.FirstOrder.UTerm.Edge L μ) → LO.FirstOrder.UTerm L μ

Equations

LO.FirstOrder.UTerm.ofW (WType.mk (Sum.inl x_1) f) = LO.FirstOrder.UTerm.bvar x_1
LO.FirstOrder.UTerm.ofW (WType.mk (Sum.inr (Sum.inl x_1)) f) = LO.FirstOrder.UTerm.fvar x_1
LO.FirstOrder.UTerm.ofW (WType.mk (Sum.inr (Sum.inr ⟨fst, f⟩)) v) = LO.FirstOrder.UTerm.func f fun (i : Fin fst) => LO.FirstOrder.UTerm.ofW (v i)

Instances For

source

def LO.FirstOrder.UTerm.equivW (L : LO.FirstOrder.Language) (μ : Type u_2) :

LO.FirstOrder.UTerm L μ ≃ WType (LO.FirstOrder.UTerm.Edge L μ)

Equations

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

Instances For

source

instance LO.FirstOrder.UTerm.instInhabitedWTypeNodeEdge {L : LO.FirstOrder.Language} {μ : Type v} :

Inhabited (WType (LO.FirstOrder.UTerm.Edge L μ))

Equations

LO.FirstOrder.UTerm.instInhabitedWTypeNodeEdge = { default := WType.mk (Sum.inl 0) Empty.elim }

source

@[simp]

theorem LO.FirstOrder.UTerm.equivW_bvar {L : LO.FirstOrder.Language} {μ : Type v} (x : ℕ) :

(LO.FirstOrder.UTerm.equivW L μ) (LO.FirstOrder.UTerm.bvar x) = WType.mk (Sum.inl x) Empty.elim

source

@[simp]

theorem LO.FirstOrder.UTerm.equivW_fvar {L : LO.FirstOrder.Language} {μ : Type v} (x : μ) :

(LO.FirstOrder.UTerm.equivW L μ) (LO.FirstOrder.UTerm.fvar x) = WType.mk (Sum.inr (Sum.inl x)) Empty.elim

source

@[simp]

theorem LO.FirstOrder.UTerm.equivW_func {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.UTerm L μ) :

(LO.FirstOrder.UTerm.equivW L μ) (LO.FirstOrder.UTerm.func f v) = WType.mk (Sum.inr (Sum.inr ⟨k, f⟩)) fun (i : LO.FirstOrder.UTerm.Edge L μ (Sum.inr (Sum.inr ⟨k, f⟩))) => (LO.FirstOrder.UTerm.equivW L μ) (v i)

source

@[simp]

theorem LO.FirstOrder.UTerm.equivW_symm_inr_inr {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (f : L.Func k) (v : Fin k → WType (LO.FirstOrder.UTerm.Edge L μ)) :

(LO.FirstOrder.UTerm.equivW L μ).symm (WType.mk (Sum.inr (Sum.inr ⟨k, f⟩)) v) = LO.FirstOrder.UTerm.func f fun (i : Fin k) => (LO.FirstOrder.UTerm.equivW L μ).symm (v i)

source

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

Fintype (LO.FirstOrder.UTerm.Edge L μ a)

Equations

LO.FirstOrder.UTerm.instFintypeEdge x = match x with | Sum.inl val => Fintype.ofIsEmpty | Sum.inr (Sum.inl val) => Fintype.ofIsEmpty | Sum.inr (Sum.inr ⟨k, snd⟩) => Fin.fintype k

source

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

Primcodable (LO.FirstOrder.UTerm.Edge L μ a)

Equations

LO.FirstOrder.UTerm.instPrimcodableEdge x = match x with | Sum.inl val => Primcodable.empty | Sum.inr (Sum.inl val) => Primcodable.empty | Sum.inr (Sum.inr ⟨fst, snd⟩) => Primcodable.fin

source

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

DecidableEq (LO.FirstOrder.UTerm.Edge L μ a)

Equations

LO.FirstOrder.UTerm.instDecidableEqEdge x = match x with | Sum.inl val => instDecidableEqEmpty | Sum.inr (Sum.inl val) => instDecidableEqEmpty | Sum.inr (Sum.inr ⟨fst, snd⟩) => inferInstance

source

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

PrimrecCard (LO.FirstOrder.UTerm.Edge L μ)

Equations

⋯ = ⋯

source

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

Primcodable (LO.FirstOrder.UTerm L μ)

Equations

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

source

theorem LO.FirstOrder.UTerm.bvar_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] :

Primrec LO.FirstOrder.UTerm.bvar

source

theorem LO.FirstOrder.UTerm.fvar_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] :

Primrec LO.FirstOrder.UTerm.fvar

source

def LO.FirstOrder.UTerm.funcL {L : LO.FirstOrder.Language} {μ : Type v} (f : (k : ℕ) × L.Func k) (l : List (LO.FirstOrder.UTerm L μ)) :

Option (LO.FirstOrder.UTerm L μ)

Equations

LO.FirstOrder.UTerm.funcL f l = if h : l.length = f.fst then some (LO.FirstOrder.UTerm.func f.snd fun (i : Fin f.fst) => l.get (Fin.cast ⋯ i)) else none

Instances For

source

theorem LO.FirstOrder.UTerm.funcL_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] :

Primrec₂ LO.FirstOrder.UTerm.funcL

source

theorem LO.FirstOrder.UTerm.funcL_primrec' {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] (k : ℕ) :

Primrec₂ fun (x : L.Func k) => LO.FirstOrder.UTerm.funcL ⟨k, x⟩

source

theorem LO.FirstOrder.UTerm.func_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] (k : ℕ) :

Primrec₂ LO.FirstOrder.UTerm.func

source

theorem LO.FirstOrder.UTerm.elim_primrec_param {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {σ : Type u_1} {γ : Type u_2} [Primcodable σ] [Primcodable γ] {b : σ → ℕ → γ} {e : σ → μ → γ} {u : σ → ((k : ℕ) × L.Func k) × List γ → γ} {t : σ → LO.FirstOrder.UTerm L μ} (hb : Primrec₂ b) (he : Primrec₂ e) (hu : Primrec₂ u) (ht : Primrec t) :

Primrec fun (x : σ) => LO.FirstOrder.UTerm.elim (b x) (e x) (fun {k : ℕ} (f : L.Func k) (v : Fin k → γ) => u x (⟨k, f⟩, List.ofFn v)) (t x)

source

theorem LO.FirstOrder.UTerm.elim_primrec_param_opt {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {σ : Type u_1} {γ : Type u_2} [Primcodable σ] [Inhabited γ] [Primcodable γ] {b : σ → ℕ → γ} {e : σ → μ → γ} {t : σ → LO.FirstOrder.UTerm L μ} (hb : Primrec₂ b) (he : Primrec₂ e) (u : σ → {k : ℕ} → L.Func k → (Fin k → γ) → γ) {uOpt : σ → ((k : ℕ) × L.Func k) × List γ → Option γ} (hu : Primrec₂ uOpt) (ht : Primrec t) (H : ∀ (x : σ) {k : ℕ} (f : L.Func k) (v : Fin k → γ), uOpt x (⟨k, f⟩, List.ofFn v) = some (u x f v)) :

Primrec fun (x : σ) => LO.FirstOrder.UTerm.elim (b x) (e x) (fun {k : ℕ} => u x) (t x)

source

theorem LO.FirstOrder.UTerm.elim_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {γ : Type u_1} [Primcodable γ] {b : ℕ → γ} {e : μ → γ} {u : (k : ℕ) × L.Func k → List γ → γ} (hb : Primrec b) (he : Primrec e) (hu : Primrec₂ u) :

Primrec (LO.FirstOrder.UTerm.elim b e fun {k : ℕ} (f : L.Func k) (v : Fin k → γ) => u ⟨k, f⟩ (List.ofFn v))

source

theorem LO.FirstOrder.UTerm.elim_primrec_opt {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {γ : Type u_1} [Inhabited γ] [Primcodable γ] {b : ℕ → γ} {e : μ → γ} (hb : Primrec b) (he : Primrec e) (u : {k : ℕ} → L.Func k → (Fin k → γ) → γ) {uOpt : (k : ℕ) × L.Func k → List γ → Option γ} (hu : Primrec₂ uOpt) (H : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → γ), uOpt ⟨k, f⟩ (List.ofFn v) = some (u f v)) :

Primrec (LO.FirstOrder.UTerm.elim b e fun {k : ℕ} => u)

source

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

Primrec LO.FirstOrder.UTerm.bv

source

theorem LO.FirstOrder.UTerm.bind_primrec_param {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {μ₁ : Type u_1} {μ₂ : Type u_2} [Primcodable μ₁] [Primcodable μ₂] {σ : Type u_3} [Primcodable σ] {b : σ → ℕ → LO.FirstOrder.UTerm L μ₂} {e : σ → μ₁ → LO.FirstOrder.UTerm L μ₂} {g : σ → LO.FirstOrder.UTerm L μ₁} (hb : Primrec₂ b) (he : Primrec₂ e) (hg : Primrec g) :

Primrec fun (x : σ) => LO.FirstOrder.UTerm.bind (b x) (e x) (g x)

source

theorem LO.FirstOrder.UTerm.bind_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {μ₁ : Type u_1} {μ₂ : Type u_2} [Primcodable μ₁] [Primcodable μ₂] {b : ℕ → LO.FirstOrder.UTerm L μ₂} {e : μ₁ → LO.FirstOrder.UTerm L μ₂} (hb : Primrec b) (he : Primrec e) :

Primrec (LO.FirstOrder.UTerm.bind b e)

source

theorem LO.FirstOrder.UTerm.bShifts_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] :

Primrec₂ LO.FirstOrder.UTerm.bShifts

source

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

Primcodable (LO.FirstOrder.Semiterm L μ n)

Equations

LO.FirstOrder.Semiterm.instPrimcodable = Primcodable.ofEquiv { t : LO.FirstOrder.UTerm L μ // t.bv ≤ n } LO.FirstOrder.UTerm.subtEquiv

source

theorem LO.FirstOrder.Semiterm.bvar_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec LO.FirstOrder.Semiterm.bvar

source

theorem LO.FirstOrder.Semiterm.fvar_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec LO.FirstOrder.Semiterm.fvar

source

def LO.FirstOrder.Semiterm.funcL {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (f : (k : ℕ) × L.Func k) (l : List (LO.FirstOrder.Semiterm L μ n)) :

Option (LO.FirstOrder.Semiterm L μ n)

Equations

LO.FirstOrder.Semiterm.funcL f l = if h : l.length = f.fst then some (LO.FirstOrder.Semiterm.func f.snd fun (i : Fin f.fst) => l.get (Fin.cast ⋯ i)) else none

Instances For

source

theorem LO.FirstOrder.Semiterm.funcL_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec₂ LO.FirstOrder.Semiterm.funcL

source

theorem LO.FirstOrder.Semiterm.funcL_primrec' {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} (k : ℕ) :

Primrec₂ fun (x : L.Func k) => LO.FirstOrder.Semiterm.funcL ⟨k, x⟩

source

theorem LO.FirstOrder.Semiterm.func₁_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec₂ fun (x : L.Func 1) (x_1 : LO.FirstOrder.Semiterm L μ n) => LO.FirstOrder.Semiterm.func x ![x_1]

source

theorem LO.FirstOrder.Semiterm.func₂_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec₂ fun (f : L.Func 2) (t : LO.FirstOrder.Semiterm L μ n × LO.FirstOrder.Semiterm L μ n) => LO.FirstOrder.Semiterm.func f ![t.1, t.2]

source

theorem LO.FirstOrder.Semiterm.subtEquiv_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₂) (t : LO.FirstOrder.Semiterm L μ₁ n₁) :

↑(LO.FirstOrder.UTerm.subtEquiv ((LO.FirstOrder.Rew.bind b e) t)) = LO.FirstOrder.UTerm.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.UTerm.subtEquiv t)

source

theorem LO.FirstOrder.Semiterm.bv_subtEquiv {L : LO.FirstOrder.Language} {μ : Type v} {n : ℕ} (t : LO.FirstOrder.Semiterm L μ n) :

(↑(LO.FirstOrder.UTerm.subtEquiv t)).bv ≤ n

source

theorem LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift {L : LO.FirstOrder.Language} {μ : Type v} {k : ℕ} (t : LO.FirstOrder.Semiterm L μ k) :

↑(LO.FirstOrder.UTerm.subtEquiv (LO.FirstOrder.Rew.bShift t)) = LO.FirstOrder.UTerm.bShifts 1 ↑(LO.FirstOrder.UTerm.subtEquiv t)

source

theorem LO.FirstOrder.Semiterm.brew_primrec {L : LO.FirstOrder.Language} {α : Type u_1} [Primcodable α] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {μ₂ : Type u_4} [Primcodable μ₂] {n₁ : ℕ} {n₂ : ℕ} {b : α → Fin n₁ → LO.FirstOrder.Semiterm L μ₂ n₂} (hb : Primrec b) :

Primrec₂ fun (z : α) (x : ℕ) => if hx : x < n₁ then ↑(LO.FirstOrder.UTerm.subtEquiv (b z ⟨x, hx⟩)) else default

source

theorem LO.FirstOrder.Semiterm.bind_primrec {L : LO.FirstOrder.Language} {α : Type u_1} [Primcodable α] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {μ₁ : Type u_3} {μ₂ : Type u_4} [Primcodable μ₁] [Primcodable μ₂] {n₁ : ℕ} {n₂ : ℕ} {b : α → Fin n₁ → LO.FirstOrder.Semiterm L μ₂ n₂} {e : α → μ₁ → LO.FirstOrder.Semiterm L μ₂ n₂} {t : α → LO.FirstOrder.Semiterm L μ₁ n₁} (hb : Primrec b) (he : Primrec₂ e) (ht : Primrec t) :

Primrec fun (x : α) => (LO.FirstOrder.Rew.bind (b x) (e x)) (t x)

source

theorem LO.FirstOrder.Semiterm.rewrite_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {k : ℕ} {n : ℕ} :

Primrec₂ fun (v : Fin k → LO.FirstOrder.Semiterm L μ n) (p : LO.FirstOrder.Semiterm L (Fin k) n) => (LO.FirstOrder.Rew.rewrite v) p

source

theorem LO.FirstOrder.Semiterm.castLE_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n₁ : ℕ} {n₂ : ℕ} (h : n₁ ≤ n₂) :

Primrec ⇑(LO.FirstOrder.Rew.castLE h)

source

theorem LO.FirstOrder.Semiterm.substs_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} {n' : ℕ} :

Primrec₂ fun (v : Fin n → LO.FirstOrder.Semiterm L μ n') (p : LO.FirstOrder.Semiterm L μ n) => (LO.FirstOrder.Rew.substs v) p

source

theorem LO.FirstOrder.Semiterm.substs₀_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n' : ℕ} :

Primrec fun (u : LO.FirstOrder.Semiterm L μ 0) => (LO.FirstOrder.Rew.substs ![]) u

source

theorem LO.FirstOrder.Semiterm.substs₁_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n' : ℕ} :

Primrec₂ fun (t : LO.FirstOrder.Semiterm L μ n') (u : LO.FirstOrder.Semiterm L μ 1) => (LO.FirstOrder.Rew.substs ![t]) u

source

theorem LO.FirstOrder.Semiterm.substs₂_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n' : ℕ} :

Primrec₂ fun (v : LO.FirstOrder.Semiterm L μ n' × LO.FirstOrder.Semiterm L μ n') (u : LO.FirstOrder.Semiterm L μ 2) => (LO.FirstOrder.Rew.substs ![v.1, v.2]) u

source

theorem LO.FirstOrder.Semiterm.emb_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec ⇑LO.FirstOrder.Rew.emb

source

instance LO.FirstOrder.Semiterm.Operator.instPrimcodable {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] (k : ℕ) :

Primcodable (LO.FirstOrder.Semiterm.Operator L k)

Equations

LO.FirstOrder.Semiterm.Operator.instPrimcodable k = Primcodable.ofEquiv (LO.FirstOrder.Semiterm L Empty k) LO.FirstOrder.Semiterm.Operator.equiv

source

theorem LO.FirstOrder.Semiterm.Operator.term_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {k : ℕ} :

Primrec LO.FirstOrder.Semiterm.Operator.term

source

theorem LO.FirstOrder.Semiterm.Operator.mk_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {k : ℕ} :

Primrec LO.FirstOrder.Semiterm.Operator.mk

source

theorem LO.FirstOrder.Semiterm.Operator.operator_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {k : ℕ} {n : ℕ} :

Primrec₂ LO.FirstOrder.Semiterm.Operator.operator

source

theorem LO.FirstOrder.Semiterm.Operator.comp_primrec₂ {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {l : ℕ} (o : LO.FirstOrder.Semiterm.Operator L 2) :

Primrec₂ fun (o₁ o₂ : LO.FirstOrder.Semiterm.Operator L l) => o.comp ![o₁, o₂]

source

theorem LO.FirstOrder.Semiterm.Operator.foldr_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {k : ℕ} (f : LO.FirstOrder.Semiterm.Operator L 2) (z : LO.FirstOrder.Semiterm.Operator L k) :

Primrec (f.foldr z)

source

theorem LO.FirstOrder.Semiterm.Operator.numeral_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] [LO.FirstOrder.Semiterm.Operator.Zero L] [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Add L] :

Primrec (LO.FirstOrder.Semiterm.Operator.numeral L)

source

theorem LO.FirstOrder.Semiterm.Operator.const_primrec {L : LO.FirstOrder.Language} {μ : Type v} [Primcodable μ] [(k : ℕ) → Primcodable (L.Func k)] [UniformlyPrimcodable L.Func] {n : ℕ} :

Primrec LO.FirstOrder.Semiterm.Operator.const