internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯)
Tactic:
apply congr_arg
Proof state after:
case h
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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ WType.SubWType.cast this✝
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
case h
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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ WType.SubWType.cast this✝
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode (nrel r v) = Nat.pair 1 ((Nat.pair 0 ((2 * k.pair) ((encode r).pair (encode v)))).pair 0)
Tactic:
simp[primcodable, Primcodable.ofEquiv_toEncodable,
  Encodable.encode_ofEquiv (equivW L μ), WType.encode_eq, WType.SubWType.ofW, WType.depth]
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode
      (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode
      (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
have : (WType.depth (β := Edge L μ) (WType.mk (false, Sum.inl ⟨k, r, v⟩) Empty.elim)) = 1 := rfl
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode
      (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode
      (WType.SubWType.cast this
        (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
suffices encode (WType.SubWType.ofWType (β := Edge L μ) ⟨(false, Sum.inl ⟨k, r, v⟩), Empty.elim⟩ 1 (by rw[this])) =
  ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0) by
{ rw[←this]; apply congr_arg; simp }
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
simp[WType.SubWType.encode_mk, Encodable.encode_fintypeArrow_isEmpty, Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth ≤ 1
Tactic:
rw[this]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
rw[←this]
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯)
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof 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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯)
Tactic:
apply congr_arg
Proof state after:
case h
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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ WType.SubWType.cast this✝
      (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯
Theorem: LO.FirstOrder.UFormula.encode_nrel
Proof state before:
case h
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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ WType.SubWType.cast this✝
      (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => rel p.snd.1 p.snd.2
Tactic:
let i : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → Node L μ := fun t => (true, Sum.inl t)
Proof 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 => (true, Sum.inl t)
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => (true, Sum.inl t)
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Tactic:
have : Primrec i := Primrec.pair (Primrec.const true) (sum_inl.comp Primrec.id)
Proof 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 => (true, Sum.inl t)
this : Primrec i
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => (true, Sum.inl t)
this : Primrec i
⊢ Primrec fun p => rel 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
Proof 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 => (true, Sum.inl t)
this✝ : Primrec i
this : Primrec fun t => WType.mk (i t) Empty.elim
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => (true, Sum.inl t)
this✝ : Primrec i
this : Primrec fun t => WType.mk (i t) Empty.elim
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Tactic:
have := (of_equiv_symm (e := equivW L μ)).comp this
Proof 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 => (true, 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 => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => (true, 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 => rel p.snd.1 p.snd.2
Tactic:
simpa using this
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => (true, Sum.inl t)
this : Primrec i
⊢ ∀ (x : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)), IsEmpty (Edge L μ (i x))
Tactic:
intros
Proof 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 => (true, Sum.inl t)
this : Primrec i
x✝ : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)
⊢ IsEmpty (Edge L μ (i x✝))
Theorem: LO.FirstOrder.UFormula.rel_primrec
Proof 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 => (true, Sum.inl t)
this : Primrec i
x✝ : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)
⊢ IsEmpty (Edge L μ (i x✝))
Tactic:
exact instIsEmptyEmpty
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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)
Proof 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
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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)
Proof 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
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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
Proof 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✝))
Theorem: LO.FirstOrder.UFormula.nrel_primrec
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.relL_primrec
Proof 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 μ
this :
  Primrec₂ fun r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
⊢ ∀ (a : (k : ℕ) × L.Rel k) (b : List (UTerm L μ)),
    (if b.length = a.fst then Nat.pair 1 ((Nat.pair 1 ((2 * a.fst.pair) ((encode a.snd).pair (encode b)))).pair 0) + 1
      else 0) =
      encode (relL a b)
Tactic:
rintro ⟨k, r⟩ l
Proof state after:
case mk
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 μ
this :
  Primrec₂ fun r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
⊢ (if l.length = ⟨k, r⟩.fst then
      Nat.pair 1 ((Nat.pair 1 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (relL ⟨k, r⟩ l)