internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! q
Tactic:
exact imp_trans! hC efq! ⨀ (by
  apply iff_provable_list_conj.mpr;
  exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩;
)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! Γ.conj'
Tactic:
apply iff_provable_list_conj.mpr
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, 𝓓 ⊢! p
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, 𝓓 ⊢! p
Tactic:
exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p t)
Tactic:
simp [lindenbaum_next]
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (if (𝓓)-Consistent (insert p t.1, t.2) then (insert p t.1, t.2) else (t.1, insert p t.2))
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (if (𝓓)-Consistent (insert p t.1, t.2) then (insert p t.1, t.2) else (t.1, insert p t.2))
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : (𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (insert p t.1, t.2)

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : (𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (insert p t.1, t.2)

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
. simpa;
Proof state after:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
. have := consistent_either consistent p;
  simp_all only [false_or];
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : (𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (insert p t.1, t.2)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
have := consistent_either consistent p
Proof state after:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
this : (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Theorem: LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent
Proof state before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
this : (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
simp_all only [false_or]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_zero
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
⊢ t[0] = t
Tactic:
simp [lindenbaum_next_indexed]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i + 1]
Tactic:
simp [lindenbaum_next_indexed]
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] →
    (𝓓)-Consistent
      (match decode i with
      | some p => lindenbaum_next 𝓓 p t[i]
      | none => t[i])
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] →
    (𝓓)-Consistent
      (match decode i with
      | some p => lindenbaum_next 𝓓 p t[i]
      | none => t[i])
Tactic:
split
Proof state after:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])

case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])

case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Tactic:
. intro h; apply next_parametericConsistent; assumption;
Proof state after:
case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Tactic:
. tauto;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])
Tactic:
intro h
Proof state after:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])
Tactic:
apply next_parametericConsistent
Proof state after:
case h_1.consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
case h_1.consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ
Proof state before:
case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
⊢ p ∈ t[encode p + 1].1 ∨ p ∈ t[encode p + 1].2
Tactic:
simp [lindenbaum_next_indexed, lindenbaum_next]
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
⊢ p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).1 ∨
    p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).2
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
⊢ p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).1 ∨
    p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).2
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1 ∨ p ∈ (insert p t[encode p].1, t[encode p].2).2

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1 ∨ p ∈ (insert p t[encode p].1, t[encode p].2).2

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
. left; tauto;
Proof state after:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
. right; tauto;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1 ∨ p ∈ (insert p t[encode p].1, t[encode p].2).2
Tactic:
left
Proof state after:
case isTrue.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
case isTrue.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
right
Proof state after:
case isFalse.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).2
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed
Proof state before:
case isFalse.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
⊢ (𝓓)-Consistent t[i]
Tactic:
induction i with
| zero => simpa;
| succ i ih => apply lindenbaum_next_indexed_parametricConsistent_succ; assumption;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent
Proof state before:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t[0]
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent
Proof state before:
case succ
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i + 1]
Tactic:
apply lindenbaum_next_indexed_parametricConsistent_succ
Proof state after:
case succ.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent
Proof state before:
case succ.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n : ℕ
h : m ≤ n
⊢ t[m].1 ⊆ t[n].1
Tactic:
induction h with
| refl => simp;
| step h ih =>
  simp [lindenbaum_next_indexed, lindenbaum_next];
  split;
  . split <;> tauto;
  . tauto;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof state before:
case refl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n : ℕ
⊢ t[m].1 ⊆ t[m].1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof state before:
case step
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
⊢ t[m].1 ⊆ t[m✝.succ].1
Tactic:
simp [lindenbaum_next_indexed, lindenbaum_next]
Proof state after:
case step
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
⊢ t[m].1 ⊆
    (match decode m✝ with
      | some p =>
        if (𝓓)-Consistent (insert p t[m✝].1, t[m✝].2) then (insert p t[m✝].1, t[m✝].2) else (t[m✝].1, insert p t[m✝].2)
      | none => t[m✝]).1
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof state before:
case step
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
⊢ t[m].1 ⊆
    (match decode m✝ with
      | some p =>
        if (𝓓)-Consistent (insert p t[m✝].1, t[m✝].2) then (insert p t[m✝].1, t[m✝].2) else (t[m✝].1, insert p t[m✝].2)
      | none => t[m✝]).1
Tactic:
split
Proof state after:
case step.h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].1 ⊆
    (if (𝓓)-Consistent (insert p✝ t[m✝].1, t[m✝].2) then (insert p✝ t[m✝].1, t[m✝].2)
      else (t[m✝].1, insert p✝ t[m✝].2)).1

case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1