Theorem: LO.FirstOrder.UFormula.nrelL_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 μ
this :
  Primrec₂ fun r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((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 0 ((2 * a.fst.pair) ((encode a.snd).pair (encode b)))).pair 0) + 1
      else 0) =
      encode (nrelL a b)
Tactic:
rintro ⟨k, r⟩ l
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 0 ((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 0 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (nrelL ⟨k, r⟩ l)

State before:
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 0 ((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 0 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (nrelL ⟨k, r⟩ l)
Tactic:
by_cases hl : l.length = k <;> simp[hl, nrelL, primcodable, Primcodable.ofEquiv_toEncodable]
State after:
case pos
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 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))

State before:
case pos
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 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
{ rcases hl with rfl
  simp[encode_nrel, encode_finArrow, List.ofFn_get] }
State after:
no goals

State before:
case pos
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 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
rcases hl with rfl
State after:
case pos
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 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
l : List (UTerm L μ)
r : L.Rel l.length
⊢ Nat.pair 1 ((Nat.pair 0 (2 * l.length.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))

State before:
case pos
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 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
l : List (UTerm L μ)
r : L.Rel l.length
⊢ Nat.pair 1 ((Nat.pair 0 (2 * l.length.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
Tactic:
simp[encode_nrel, encode_finArrow, List.ofFn_get]
State after:
no goals