internlm/Lean-Github huggingface dataset:
Theorem: localRuleTruth
Proof state before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
g : Formula
g_def : g = (~unload val.1)
⊢ evaluate M w g
Tactic:
subst g_def
Proof state after:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (~unload val.1)
Theorem: localRuleTruth
Proof state before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ evaluate M w (~unload val.1)
Tactic:
apply w_Ci
Proof state after:
case h.right.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ (~unload val.1) ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList
Theorem: localRuleTruth
Proof state before:
case h.right.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L, R ++ X, some (Sum.inr (~'val.1)))
⊢ (~unload val.1) ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'val.1)))).toList
Tactic:
simp_all
Proof state after:
no goals
Theorem: LocalRule.cond_non_empty
Proof state before:
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
X : List TNode
rule : LocalRule (Lcond, Rcond, Ocond) X
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅
Tactic:
cases rule
Proof state after:
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ node_to_multiset (Lcond, ∅, none) ≠ ∅

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ node_to_multiset (∅, Rcond, none) ≠ ∅

case LRnegL
ϕ✝ : Formula
⊢ node_to_multiset ([ϕ✝], [~ϕ✝], none) ≠ ∅

case LRnegR
ϕ✝ : Formula
⊢ node_to_multiset ([~ϕ✝], [ϕ✝], none) ≠ ∅

case loadedL
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))) ≠ ∅

case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅
Theorem: LocalRule.cond_non_empty
Proof state before:
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ node_to_multiset (Lcond, ∅, none) ≠ ∅

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ node_to_multiset (∅, Rcond, none) ≠ ∅

case LRnegL
ϕ✝ : Formula
⊢ node_to_multiset ([ϕ✝], [~ϕ✝], none) ≠ ∅

case LRnegR
ϕ✝ : Formula
⊢ node_to_multiset ([~ϕ✝], [ϕ✝], none) ≠ ∅

case loadedL
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))) ≠ ∅

case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅
Tactic:
all_goals simp [node_to_multiset]
Proof state after:
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ ¬Lcond = []

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ ¬Rcond = []
Theorem: LocalRule.cond_non_empty
Proof state before:
Lcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Lcond ress✝
⊢ ¬Lcond = []
Tactic:
case oneSidedL _ orule => cases orule <;> simp
Proof state after:
no goals
Theorem: LocalRule.cond_non_empty
Proof state before:
Rcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Rcond ress✝
⊢ ¬Rcond = []
Tactic:
case oneSidedR _ orule => cases orule <;> simp
Proof state after:
no goals
Theorem: LocalRule.cond_non_empty
Proof state before:
case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅
Tactic:
simp [node_to_multiset]
Proof state after:
no goals
Theorem: LocalRule.cond_non_empty
Proof state before:
Lcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Lcond ress✝
⊢ ¬Lcond = []
Tactic:
cases orule <;> simp
Proof state after:
no goals
Theorem: LocalRule.cond_non_empty
Proof state before:
Rcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Rcond ress✝
⊢ ¬Rcond = []
Tactic:
cases orule <;> simp
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof 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 φ
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof state before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
β : Program
φ : Formula
y_in_E : (⌈β⌉φ) ∈ E
⊢ lmOfFormula (⌈β⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
cases β
Proof 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 φ✝
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof state before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ lmOfFormula (⌈∗β⌉φ) < lmOfProgram α + lmOfFormula φ✝
Tactic:
simp
Proof state after:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ 1 + lmOfProgram β + lmOfFormula φ < lmOfProgram α + lmOfFormula φ✝
Theorem: unfoldBox.decreases_lmOf
Proof state before:
α : Program
φ✝ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ✝
φ : Formula
β : Program
y_in_E : (⌈∗β⌉φ) ∈ E
⊢ 1 + lmOfProgram β + lmOfFormula φ < lmOfProgram α + lmOfFormula φ✝
Tactic:
sorry
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof state after:
no goals
Theorem: unfoldBox.decreases_lmOf
Proof 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
Proof state after:
no goals
Theorem: unfoldDiamond.decreases_lmOf
Proof state before:
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_E : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
Tactic:
sorry
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
X : TNode
ress : List TNode
rule : LocalRule X ress
⊢ ∀ Y ∈ ress, ∀ y ∈ node_to_multiset Y, ∃ x ∈ node_to_multiset X, y < x
Tactic:
intro Y Y_in_ress y y_in_Y
Proof state after:
X : TNode
ress : List TNode
rule : LocalRule X ress
Y : TNode
Y_in_ress : Y ∈ ress
y : Formula
y_in_Y : y ∈ node_to_multiset Y
⊢ ∃ x ∈ node_to_multiset X, y < x
Theorem: LocalRule.Decreases
Proof state before:
X : TNode
ress : List TNode
rule : LocalRule X ress
Y : TNode
Y_in_ress : Y ∈ ress
y : Formula
y_in_Y : y ∈ node_to_multiset Y
⊢ ∃ x ∈ node_to_multiset X, y < x
Tactic:
cases rule
Proof state after:
case oneSidedL
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

case oneSidedR
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

case LRnegL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x

case LRnegR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x

case loadedL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x

case loadedR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))), y < x
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x
Tactic:
case LRnegL => simp at *
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x
Tactic:
case LRnegR => simp at *
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:
case oneSidedL orule =>
  cases orule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case neg.refl => linarith
  case con.refl => cases y_in_Y <;> (subst_eqs; linarith)
  case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
  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
  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:
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:
case oneSidedR orule =>
  cases orule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case neg.refl => linarith
  case con.refl => cases y_in_Y <;> (subst_eqs; linarith)
  case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
  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
  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:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x
Tactic:
case loadedL lrule =>
  simp [node_to_multiset]
  cases lrule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case dia α χ =>
    sorry
  case dia' α φ =>
    sorry
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))), y < x
Tactic:
case loadedR lrule =>
  simp [node_to_multiset]
  cases lrule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case dia α χ =>
    sorry
  case dia' α φ =>
    sorry
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x
Tactic:
simp at *
Proof state after:
no goals
Theorem: LocalRule.Decreases
Proof state before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x
Tactic:
simp at *
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 : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)
Tactic:
case neg.refl => 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:
case con.refl => cases y_in_Y <;> (subst_eqs; 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:
case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
Proof state after:
no goals