internlm/Lean-Github huggingface dataset:
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:
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
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:
simp [node_to_multiset]
Proof state after:
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✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
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✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
Tactic:
cases lrule
Proof state after:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Theorem: LocalRule.Decreases
Proof state before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
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
χ✝ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α✝ χ✝ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula (unload χ✝))

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 b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ (a, [], Option.map Sum.inl b) = 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 χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
case dia α χ =>
  sorry
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 b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia' α φ =>
  sorry
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 x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
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 b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ (a, [], Option.map Sum.inl b) = 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 χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
sorry
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 b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
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:
simp [node_to_multiset]
Proof state after:
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✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
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✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
Tactic:
cases lrule
Proof state after:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Theorem: LocalRule.Decreases
Proof state before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
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
χ✝ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α✝ χ✝ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula (unload χ✝))

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 b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ ([], a, Option.map Sum.inr b) = 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 χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
case dia α χ =>
  sorry
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 b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia' α φ =>
  sorry
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 x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
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 b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ ([], a, Option.map Sum.inr b) = 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 χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
sorry
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 b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
sorry
Proof state after:
no goals
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N ↔ MultisetLT' M N
Tactic:
unfold MultisetLT'
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N ↔ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N ↔ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N → ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ (∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y) → MultisetLT M N
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N → ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
intro M_LT_N
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT_N : MultisetLT M N
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT_N : MultisetLT M N
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
cases M_LT_N
Proof state after:
case mp.MLT
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X✝ Y✝ Z✝ : Multiset α
a✝³ : Y✝ ≠ ∅
a✝² : M = Z✝ + X✝
a✝¹ : N = Z✝ + Y✝
a✝ : ∀ x ∈ X✝, ∃ y ∈ Y✝, x < y
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mp.MLT
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X✝ Y✝ Z✝ : Multiset α
a✝³ : Y✝ ≠ ∅
a✝² : M = Z✝ + X✝
a✝¹ : N = Z✝ + Y✝
a✝ : ∀ x ∈ X✝, ∃ y ∈ Y✝, x < y
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
aesop
Proof state after:
no goals
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ (∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y) → MultisetLT M N
Tactic:
intro M_LT'_N
Proof state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT'_N : ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT'_N : ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
Tactic:
rcases M_LT'_N with ⟨X,Y,Z,claim⟩
Proof state after:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
Tactic:
apply MultisetLT.MLT X Y Z
Proof state after:
case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ Y ≠ ∅

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ M = Z + X

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ N = Z + Y

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ Y ≠ ∅

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ M = Z + X

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ N = Z + Y

case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
all_goals tauto
Proof state after:
no goals
Theorem: MultisetLT.iff_MultisetLT'
Proof state before:
case mpr.intro.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
tauto
Proof state after:
no goals
Theorem: localRuleApp.decreases_DM
Proof state before:
X : TNode
B : List TNode
lrA : LocalRuleApp X B
⊢ ∀ Y ∈ B, lt_TNode Y X
Tactic:
rcases lrA with ⟨Lcond,Rcond,Ocond,rule,preconP⟩
Proof state after:
case mk
B : List TNode
L✝ R✝ : List Formula
ress✝ : List TNode
O✝ : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress✝
preconP : Lcond.Sublist L✝ ∧ Rcond.Sublist R✝ ∧ Ocond ⊆ O✝
hC✝ : B = applyLocalRule rule (L✝, R✝, O✝)
⊢ ∀ Y ∈ B, lt_TNode Y (L✝, R✝, O✝)