Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation (Logic/FirstOrder/Computability/Calculus.lean)

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
property✝ : CutFree (axL Γ r v)
⊢ (ofDerivation ⟨axL Γ r v, property✝⟩).isProper = true
Tactic:
simp[ofDerivation, isProper]
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
property✝ : CutFree (verum Γ)
⊢ (ofDerivation ⟨verum Γ, property✝⟩).isProper = true
Tactic:
simp[ofDerivation, isProper]
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H : CutFree (bp.and bq)
⊢ (ofDerivation ⟨bp.and bq, H⟩).isProper = true
Tactic:
have H : CutFree bp ∧ CutFree bq := by simpa [CutFree] using H
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp.and bq, H✝⟩).isProper = true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp.and bq, H✝⟩).isProper = true
Tactic:
simp[ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ isProper
      ((Code.and p q, p ⋏ q :: Γ) ::
        (Code.wk (p :: Γ), p :: p ⋏ q :: Γ) ::
          (Code.wk (q :: Γ), q :: p ⋏ q :: Γ) :: (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩)) =
    true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ isProper
      ((Code.and p q, p ⋏ q :: Γ) ::
        (Code.wk (p :: Γ), p :: p ⋏ q :: Γ) ::
          (Code.wk (q :: Γ), q :: p ⋏ q :: Γ) :: (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩)) =
    true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩).isProper = true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩).isProper = true
Tactic:
exact isProper_append (isProper_ofDerivation ⟨bp, H.1⟩) (isProper_ofDerivation ⟨bq, H.2⟩)
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H : CutFree (bp.and bq)
⊢ CutFree bp ∧ CutFree bq
Tactic:
simpa [CutFree] using H
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ (ofDerivation ⟨b.or, H⟩).isProper = true
Tactic:
simp[ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ isProper ((Code.or p q, p ⋎ q :: Γ) :: (Code.wk (p :: q :: Γ), p :: q :: p ⋎ q :: Γ) :: ofDerivation ⟨b, ⋯⟩) = true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ isProper ((Code.or p q, p ⋎ q :: Γ) :: (Code.wk (p :: q :: Γ), p :: q :: p ⋎ q :: Γ) :: ofDerivation ⟨b, ⋯⟩) = true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧ Γ ⊆ p :: q :: p ⋎ q :: Γ

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧ Γ ⊆ p :: q :: p ⋎ q :: Γ
Tactic:
exact ⟨isProper_ofDerivation ⟨b, by simpa[CutFree] using H⟩, by simp[List.subset_def]; intro x hx; simp[hx]⟩
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ CutFree b
Tactic:
simpa[CutFree] using H
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ Γ ⊆ p :: q :: p ⋎ q :: Γ
Tactic:
simp[List.subset_def]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ ∀ {a : SyntacticFormula L}, a ∈ Γ → a = p ∨ a = q ∨ a = p ⋎ q ∨ a ∈ Γ

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ ∀ {a : SyntacticFormula L}, a ∈ Γ → a = p ∨ a = q ∨ a = p ⋎ q ∨ a ∈ Γ
Tactic:
intro x hx
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
x : SyntacticFormula L
hx : x ∈ Γ
⊢ x = p ∨ x = q ∨ x = p ⋎ q ∨ x ∈ Γ

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
x : SyntacticFormula L
hx : x ∈ Γ
⊢ x = p ∨ x = q ∨ x = p ⋎ q ∨ x ∈ Γ
Tactic:
simp[hx]
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ (ofDerivation ⟨b.all, H⟩).isProper = true
Tactic:
simp[ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ isProper
      ((Code.all p, (∀' p) :: Γ) ::
        (Code.wk ((Rew.hom Rew.free) p :: shifts Γ),
            (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ) ::
          ofDerivation ⟨b, ⋯⟩) =
    true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ isProper
      ((Code.all p, (∀' p) :: Γ) ::
        (Code.wk ((Rew.hom Rew.free) p :: shifts Γ),
            (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ) ::
          ofDerivation ⟨b, ⋯⟩) =
    true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧
    shifts Γ ⊆ (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧
    shifts Γ ⊆ (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ
Tactic:
exact ⟨isProper_ofDerivation ⟨b, by simpa[CutFree] using H⟩, List.subset_cons_of_subset _ $ List.subset_cons_of_subset _ $ by simp[shifts]⟩
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ CutFree b
Tactic:
simpa[CutFree] using H
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ shifts Γ ⊆ List.map (⇑(Rew.hom ⇑)) Γ
Tactic:
simp[shifts]
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ (ofDerivation ⟨ex t b, H⟩).isProper = true
Tactic:
simp[ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ isProper
      ((Code.ex p t, (∃' p) :: Γ) :: (Code.wk ([→ t].hom p :: Γ), [→ t].hom p :: (∃' p) :: Γ) :: ofDerivation ⟨b, ⋯⟩) =
    true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ isProper
      ((Code.ex p t, (∃' p) :: Γ) :: (Code.wk ([→ t].hom p :: Γ), [→ t].hom p :: (∃' p) :: Γ) :: ofDerivation ⟨b, ⋯⟩) =
    true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true
Tactic:
exact isProper_ofDerivation ⟨b, by simpa[CutFree] using H⟩
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ CutFree b
Tactic:
simpa[CutFree] using H
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ (ofDerivation ⟨b.wk ss, H⟩).isProper = true
Tactic:
simp[ofDerivation]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ isProper ((Code.wk Γ, Γ') :: ofDerivation ⟨b, ⋯⟩) = true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ isProper ((Code.wk Γ, Γ') :: ofDerivation ⟨b, ⋯⟩) = true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation, ss]
State after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true
Tactic:
exact isProper_ofDerivation ⟨b, by simpa[CutFree] using H⟩
State after:
no goals

State before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ CutFree b
Tactic:
simpa[CutFree] using H
State after:
no goals