Theorem: diamondproj_does_not_increase_vocab_R (Bml/Tableau.lean)

State before:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
⊢ jvoc (diamondProjectTNode (Sum.inr φ) (L, R)) ⊆ jvoc (L, R)
Tactic:
intro ℓ ℓ_in_proj
State after:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inr φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)

State before:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inr φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)
Tactic:
unfold jvoc at *
State after:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2

State before:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2
Tactic:
apply Finset.mem_inter_of_mem
State after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1

case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2

State before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1
Tactic:
have ℓ_left := (Finset.mem_inter.mp ℓ_in_proj).left
State after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1

State before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1
Tactic:
simp [diamondProjectTNode ] at ℓ_left
State after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).1

State before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).1
Tactic:
apply proj_does_not_increase_vocab
State after:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (projection (L, R).1)

State before:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (projection (L, R).1)
Tactic:
simp
State after:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a

State before:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
Tactic:
exact ℓ_left
State after:
no goals

State before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Tactic:
have ℓ_right := (Finset.mem_inter.mp ℓ_in_proj).right
State after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2

State before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Tactic:
simp [diamondProjectTNode ] at ℓ_right
State after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).2

State before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).2
Tactic:
apply Or.elim ℓ_right
State after:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).2

case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ projection R, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).2

State before:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).2
Tactic:
intro ℓ_in_φ
State after:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).2

State before:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).2
Tactic:
simp
State after:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
use ~(□φ)
State after:
case h
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R ∧ ℓ ∈ vocabOfFormula (~(□φ))

State before:
case h
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R ∧ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
constructor
State after:
case h.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R

case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))

State before:
case h.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R

case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
exact valid_proj
State after:
case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))

State before:
case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
aesop
State after:
no goals

State before:
case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ projection R, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).2
Tactic:
intro ⟨ψ, ψ_in_proj, ℓ_in_ψ⟩
State after:
case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (L, R).2

State before:
case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (L, R).2
Tactic:
apply proj_does_not_increase_vocab
State after:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (projection (L, R).2)

State before:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (projection (L, R).2)
Tactic:
simp
State after:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a

State before:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
Tactic:
use ψ
State after:
no goals