internlm/Lean-Github huggingface dataset:
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  rw [← add_assoc]
  exact unfoldDiamond.decreases_lmOf E_in y_in_Y
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, (a, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
case box α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  exact unfoldBox.decreases_lmOf E_in y_in_Y
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([~⌈α✝⌉φ✝], ∅, none), y < x
Tactic:
simp [node_to_multiset] at *
Proof state after:
case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)
Theorem: LocalRule.Decreases
Proof state before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([φ✝, ψ✝], [], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try subst_eqs
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try simp at *
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case neg.refl
y φ✝ : Formula
y_in_Y : y = φ✝
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝)
Tactic:
try subst_eqs
Proof state after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)
Theorem: LocalRule.Decreases
Proof state before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([φ✝, ψ✝], [], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
subst_eqs
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
simp at *
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case neg.refl
y φ✝ : Formula
y_in_Y : y = φ✝
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝)
Tactic:
subst_eqs
Proof state after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)
Theorem: LocalRule.Decreases
Proof state before:
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)
Tactic:
linarith
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
cases y_in_Y <;> (subst_eqs; linarith)
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
case inr
y φ✝ ψ✝ : Formula
h✝ : y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
subst_eqs
Proof state after:
case inr.refl
y φ✝ : Formula
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula y
Theorem: LocalRule.Decreases
Proof state before:
case inr.refl
y φ✝ : Formula
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula y
Tactic:
linarith
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([~φ✝], [], none) ∨ Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *)
Proof state after:
case inl.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula φ✝ < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case inl.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula φ✝ < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
linarith
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
case inr
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
h✝ : Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
subst_eqs
Proof state after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([~ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Theorem: LocalRule.Decreases
Proof state before:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([~ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
simp at *
Proof state after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = (~ψ✝)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Theorem: LocalRule.Decreases
Proof state before:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = (~ψ✝)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
subst_eqs
Proof state after:
case inr.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula (~ψ✝) < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Theorem: LocalRule.Decreases
Proof state before:
case inr.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula (~ψ✝) < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
simp at *
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
rcases Y_in_ress with ⟨E, E_in, E_def⟩
Proof state after:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
subst E_def
Proof state after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
simp_all only [List.append_nil, Multiset.mem_coe]
Proof state after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
rw [← add_assoc]
Proof state after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
Tactic:
exact unfoldDiamond.decreases_lmOf E_in y_in_Y
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, (a, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
rcases Y_in_ress with ⟨E, E_in, E_def⟩
Proof state after:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
subst E_def
Proof state after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
simp_all only [List.append_nil, Multiset.mem_coe]
Proof state after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Theorem: LocalRule.Decreases
Proof state before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
exact unfoldBox.decreases_lmOf E_in y_in_Y
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (∅, precond✝, none), y < x
Tactic:
cases orule
Proof state after:
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [⊥], none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝, ~φ✝], none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~~φ✝], none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝⋀ψ✝], none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~φ✝⋀ψ✝], none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [⌈α✝⌉φ✝], none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [~⌈α✝⌉φ✝], none), y < x
Theorem: LocalRule.Decreases
Proof state before:
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [⊥], none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝, ~φ✝], none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~~φ✝], none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝⋀ψ✝], none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~φ✝⋀ψ✝], none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [⌈α✝⌉φ✝], none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [~⌈α✝⌉φ✝], none), y < x
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
Proof state after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)

case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

case nCo
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

case box
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < lmOfProgram α✝ + lmOfFormula φ✝

case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  rw [← add_assoc]
  exact unfoldDiamond.decreases_lmOf E_in y_in_Y
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, ([], a, none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
case box α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  exact unfoldBox.decreases_lmOf E_in y_in_Y
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [~⌈α✝⌉φ✝], none), y < x
Tactic:
simp [node_to_multiset] at *
Proof state after:
case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)
Theorem: LocalRule.Decreases
Proof state before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [φ✝, ψ✝], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try subst_eqs
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try simp at *
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [φ✝, ψ✝], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
subst_eqs
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
simp at *
Proof state after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *)
Proof state after:
case inl.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula φ✝ < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Theorem: LocalRule.Decreases
Proof state before:
case inr
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
h✝ : Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
subst_eqs
Proof state after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [~ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)