Theorem: LO.FirstOrder.UFormula.nrel_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
let i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
⊢ Primrec fun p => nrel p.snd.1 p.snd.2

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
have : Primrec i := Primrec.pair (Primrec.const false) (sum_inl.comp Primrec.id)
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this : Primrec i
⊢ Primrec fun p => nrel p.snd.1 p.snd.2

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this : Primrec i
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
have : Primrec (fun t => WType.mk (i t) Empty.elim) :=
  w_mk₀ (β := Edge L μ) i (by intros; exact instIsEmptyEmpty) this
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this✝ : Primrec i
this : Primrec fun t => WType.mk (i t) Empty.elim
⊢ Primrec fun p => nrel p.snd.1 p.snd.2

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this✝ : Primrec i
this : Primrec fun t => WType.mk (i t) Empty.elim
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
have := (of_equiv_symm (e := equivW L μ)).comp this
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this✝¹ : Primrec i
this✝ : Primrec fun t => WType.mk (i t) Empty.elim
this : Primrec fun a => (equivW L μ).symm (WType.mk (i a) Empty.elim)
⊢ Primrec fun p => nrel p.snd.1 p.snd.2

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this✝¹ : Primrec i
this✝ : Primrec fun t => WType.mk (i t) Empty.elim
this : Primrec fun a => (equivW L μ).symm (WType.mk (i a) Empty.elim)
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
simpa using this
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this : Primrec i
⊢ ∀ (x : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)), IsEmpty (Edge L μ (i x))
Tactic:
intros
State after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this : Primrec i
x✝ : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)
⊢ IsEmpty (Edge L μ (i x✝))

State before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (false, Sum.inl t)
this : Primrec i
x✝ : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)
⊢ IsEmpty (Edge L μ (i x✝))
Tactic:
exact instIsEmptyEmpty
State after:
no goals