Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k : ℕ
c : Code k
v : Fin k → M
z z' : M
⊢ (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
Tactic:
induction c generalizing z z' <;> simp[code, codeAux]
Proof state after:
case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 0 → z' = 0 → z = z'

case one
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 1 → z' = 1 → z = z'

case add
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ + v j✝ → z' = v i✝ + v j✝ → z = z'

case mul
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ * v j✝ → z' = v i✝ * v j✝ → z = z'

case proj
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ → z' = v i✝ → z = z'

case equal
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i✝ = v j✝ ∧ z = 1 ∨ ¬v i✝ = v j✝ ∧ z = 0 → v i✝ = v j✝ ∧ z' = 1 ∨ ¬v i✝ = v j✝ ∧ z' = 0 → z = z'

case lt
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i✝ < v j✝ ∧ z = 1 ∨ v j✝ ≤ v i✝ ∧ z = 0 → v i✝ < v j✝ ∧ z' = 1 ∨ v j✝ ≤ v i✝ ∧ z' = 0 → z = z'

case comp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m✝ n✝ : ℕ
a✝¹ : Code n✝
a✝ : Fin n✝ → Code m✝
a_ih✝¹ :
  ∀ {v : Fin n✝ → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux a✝¹) → (Semiformula.Evalfm M (z' :> v)) (codeAux a✝¹) → z = z'
a_ih✝ :
  ∀ (a : Fin n✝) {v : Fin m✝ → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (a✝ a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (a✝ a)) → z = z'
v : Fin m✝ → M
z z' : M
⊢ ∀ (x : Fin n✝ → M),
    (Semiformula.Eval (standardModel M) x (z :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹)) →
      (∀ (i : Fin n✝),
          (Semiformula.Eval (standardModel M) x (z :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))) →
        ∀ (x : Fin n✝ → M),
          (Semiformula.Eval (standardModel M) x (z' :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹)) →
            (∀ (i : Fin n✝),
                (Semiformula.Eval (standardModel M) x (z' :> v))
                  ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))) →
              z = z'

case rfind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
a✝ : Code (n✝ + 1)
a_ih✝ :
  ∀ {v : Fin (n✝ + 1) → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux a✝) → (Semiformula.Evalfm M (z' :> v)) (codeAux a✝) → z = z'
v : Fin n✝ → M
z z' : M
⊢ (Semiformula.Evalfm M (z :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux a✝)) →
    (∀ x < z,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel M) ![x_1, x] (z :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))) →
      (Semiformula.Evalfm M (z' :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux a✝)) →
        (∀ x < z',
            ∃ x_1,
              ¬x_1 = 0 ∧
                (Semiformula.Eval (standardModel M) ![x_1, x] (z' :> v))
                  ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))) →
          z = z'