Theorem: unfoldBox.decreases_lmOf (Pdl/LocalTableau.lean)

State before:
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_E : y ∈ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
cases y
State after:
case bottom
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_E : Formula.bottom ∈ E
⊢ lmOfFormula Formula.bottom < lmOfProgram α + lmOfFormula φ

case atom_prop
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝ : ℕ
y_in_E : (·a✝) ∈ E
⊢ lmOfFormula (·a✝) < lmOfProgram α + lmOfFormula φ

case neg
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝ : Formula
y_in_E : (~a✝) ∈ E
⊢ lmOfFormula (~a✝) < lmOfProgram α + lmOfFormula φ

case and
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝¹ a✝ : Formula
y_in_E : a✝¹⋀a✝ ∈ E
⊢ lmOfFormula (a✝¹⋀a✝) < lmOfProgram α + lmOfFormula φ

case box
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝¹ : Program
a✝ : Formula
y_in_E : (⌈a✝¹⌉a✝) ∈ E
⊢ lmOfFormula (⌈a✝¹⌉a✝) < lmOfProgram α + lmOfFormula φ

State before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
β : Program
φ : Formula
y_in_E : (⌈β⌉φ) ∈ E
⊢ lmOfFormula (⌈β⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
case box β φ =>
  cases β
  case star β =>
    simp
    sorry
  all_goals sorry
State after:
no goals

State before:
case bottom
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_E : Formula.bottom ∈ E
⊢ lmOfFormula Formula.bottom < lmOfProgram α + lmOfFormula φ

case atom_prop
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝ : ℕ
y_in_E : (·a✝) ∈ E
⊢ lmOfFormula (·a✝) < lmOfProgram α + lmOfFormula φ

case neg
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝ : Formula
y_in_E : (~a✝) ∈ E
⊢ lmOfFormula (~a✝) < lmOfProgram α + lmOfFormula φ

case and
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝¹ a✝ : Formula
y_in_E : a✝¹⋀a✝ ∈ E
⊢ lmOfFormula (a✝¹⋀a✝) < lmOfProgram α + lmOfFormula φ
Tactic:
all_goals sorry
State after:
no goals

State before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
β : Program
φ : Formula
y_in_E : (⌈β⌉φ) ∈ E
⊢ lmOfFormula (⌈β⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
cases β
State after:
case atom_prog
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝ : ℕ
y_in_E : (⌈·a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈·a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case sequence
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝¹ a✝ : Program
y_in_E : (⌈a✝¹;'a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈a✝¹;'a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case union
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝¹ a✝ : Program
y_in_E : (⌈a✝¹⋓a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈a✝¹⋓a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case star
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝ : Program
y_in_E : (⌈∗a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈∗a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case test
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ a✝ : Formula
y_in_E : (⌈?'a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈?'a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

State before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ lmOfFormula (⌈∗β⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
case star β =>
  simp
  sorry
State after:
no goals

State before:
case atom_prog
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝ : ℕ
y_in_E : (⌈·a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈·a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case sequence
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝¹ a✝ : Program
y_in_E : (⌈a✝¹;'a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈a✝¹;'a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case union
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
a✝¹ a✝ : Program
y_in_E : (⌈a✝¹⋓a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈a✝¹⋓a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝

case test
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ a✝ : Formula
y_in_E : (⌈?'a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈?'a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
all_goals sorry
State after:
no goals

State before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ lmOfFormula (⌈∗β⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
simp
State after:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ 1 + lmOfProgram β + lmOfFormula φ < lmOfProgram α + lmOfFormula φ✝

State before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ 1 + lmOfProgram β + lmOfFormula φ < lmOfProgram α + lmOfFormula φ✝
Tactic:
sorry
State after:
no goals

State before:
case test
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ a✝ : Formula
y_in_E : (⌈?'a✝⌉φ) ∈ E
⊢ lmOfFormula (⌈?'a✝⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
sorry
State after:
no goals

State before:
case and
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
a✝¹ a✝ : Formula
y_in_E : a✝¹⋀a✝ ∈ E
⊢ lmOfFormula (a✝¹⋀a✝) < lmOfProgram α + lmOfFormula φ
Tactic:
sorry
State after:
no goals