Theorem: localRule_does_not_increase_vocab_R (Bml/Tableau.lean)

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
⊢ ∀ res ∈ ress, voc res.2 ⊆ voc Rcond
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.2
⊢ ℓ ∈ voc Rcond

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.2
⊢ ℓ ∈ voc Rcond
Tactic:
cases rule
State after:
case oneSidedL
Lcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.2
ress✝ : List (Finset Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
ress_in_ress : res ∈ List.map (fun res => (res, ∅)) ress✝
⊢ ℓ ∈ voc ∅

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

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

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

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

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

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

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

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

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