Theorem: LO.FirstOrder.UFormula.encode_rel (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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode (rel r v) = Nat.pair 1 ((Nat.pair 1 ((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]
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 (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0

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 (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
have : (WType.depth (β := Edge L μ) (WType.mk (true, Sum.inl ⟨k, r, v⟩) Empty.elim)) = 1 := rfl
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 (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0

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
⊢ 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) ⋯)) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
suffices encode (WType.SubWType.ofWType (β := Edge L μ) ⟨(true, Sum.inl ⟨k, r, v⟩), Empty.elim⟩ 1 (by rw[this])) =
  ((Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0) by
{ rw[←this]; apply congr_arg; simp }
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 (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ 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

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
⊢ 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
Tactic:
simp[WType.SubWType.encode_mk, Encodable.encode_fintypeArrow_isEmpty, Edge]
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 μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth ≤ 1
Tactic:
rw[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 μ
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) ⋯)) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
rw[←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 μ
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 ⋯)

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
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 ⋯

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
State after:
no goals