Theorem: localRule_does_not_increase_vocab_L (Bml/Tableau.lean)

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
⊢ ∀ res ∈ ress, voc res.1 ⊆ voc Lcond
Tactic:
intro res ress_in_ress ℓ ℓ_in_res
State after:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
ress_in_ress : res ∈ ress
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
⊢ ℓ ∈ voc Lcond

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
ress_in_ress : res ∈ ress
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
⊢ ℓ ∈ voc Lcond
Tactic:
cases rule
State after:
case oneSidedL
Lcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ress✝ : List (Finset Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
ress_in_ress : res ∈ List.map (fun res => (res, ∅)) ress✝
⊢ ℓ ∈ voc Lcond

case oneSidedR
Rcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ress✝ : List (Finset Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
ress_in_ress : res ∈ List.map (fun res => (∅, res)) ress✝
⊢ ℓ ∈ voc ∅

case LRnegL
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {ϕ✝}

case LRnegR
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {~ϕ✝}

State before:
Lcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ress : List (Finset Formula)
orule : OneSidedLocalRule Lcond ress
ress_in_ress : res ∈ List.map (fun res => (res, ∅)) ress
⊢ ℓ ∈ voc Lcond
Tactic:
case oneSidedL ress orule => cases orule <;> aesop
State after:
no goals

State before:
case oneSidedR
Rcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ress✝ : List (Finset Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
ress_in_ress : res ∈ List.map (fun res => (∅, res)) ress✝
⊢ ℓ ∈ voc ∅

case LRnegL
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {ϕ✝}

case LRnegR
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {~ϕ✝}
Tactic:
all_goals aesop
State after:
no goals

State before:
Lcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ress : List (Finset Formula)
orule : OneSidedLocalRule Lcond ress
ress_in_ress : res ∈ List.map (fun res => (res, ∅)) ress
⊢ ℓ ∈ voc Lcond
Tactic:
cases orule <;> aesop
State after:
no goals

State before:
case LRnegR
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {~ϕ✝}
Tactic:
aesop
State after:
no goals