internlm/Lean-Github huggingface dataset:
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ : Formula
in_ress : res = (∅, {φ})
⊢ (∅, {φ}).2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ) ∧ (∅, {φ}).1 = ∅
Tactic:
case neg φ => simp [←Nat.add_assoc]
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ (∅, {φ, ψ}).2.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ ∧ (∅, {φ, ψ}).1 = ∅
Tactic:
case con φ ψ => simp; exact conDecreasesLength
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {~φ}) ∨ res = (∅, {~ψ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
case ncon φ ψ =>
  cases' in_ress with case_phi case_psi
  <;> ( first
      | simp [case_psi]
      | ( simp [case_phi]
          rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
          aesop))
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ lengthOf res.1 < lengthOf {~(□a✝)} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {□a✝} ∧ res.1 = ∅
Tactic:
simp at *
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ res.2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ res.1 = ∅
Tactic:
try rw [in_ress]
Proof state after:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ (∅, {φ✝, ψ✝}).2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ (∅, {φ✝, ψ✝}).1 = ∅
Theorem: localRuleDecreasesLengthSide
Proof state before:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ res.2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ res.1 = ∅
Tactic:
rw [in_ress]
Proof state after:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ (∅, {φ✝, ψ✝}).2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ (∅, {φ✝, ψ✝}).1 = ∅
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ : Formula
in_ress : res = (∅, {φ})
⊢ (∅, {φ}).2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ) ∧ (∅, {φ}).1 = ∅
Tactic:
simp [←Nat.add_assoc]
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ (∅, {φ, ψ}).2.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ ∧ (∅, {φ, ψ}).1 = ∅
Tactic:
simp
Proof state after:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ {φ, ψ}.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ {φ, ψ}.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
exact conDecreasesLength
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {~φ}) ∨ res = (∅, {~ψ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
cases' in_ress with case_phi case_psi
<;> ( first
    | simp [case_psi]
    | ( simp [case_phi]
        rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
        aesop))
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case inr
res : SubPair
φ ψ : Formula
case_psi : res = (∅, {~ψ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
first
| simp [case_psi]
| ( simp [case_phi]
  rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
  aesop)
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case inr
res : SubPair
φ ψ : Formula
case_psi : res = (∅, {~ψ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
simp [case_psi]
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
( simp [case_phi]
  rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
  aesop)
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
simp [case_phi]
Proof state after:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < 1 + lengthOfFormula φ + lengthOfFormula ψ
Theorem: localRuleDecreasesLengthSide
Proof state before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
Proof state after:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < lengthOfFormula φ + (1 + lengthOfFormula ψ)
Theorem: localRuleDecreasesLengthSide
Proof state before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < lengthOfFormula φ + (1 + lengthOfFormula ψ)
Tactic:
aesop
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
aesop
Proof state after:
no goals
Theorem: notnot_notSelfContain
Proof state before:
φ : Formula
⊢ ~~φ ≠ φ
Tactic:
intro hyp
Proof state after:
φ : Formula
hyp : ~~φ = φ
⊢ False
Theorem: notnot_notSelfContain
Proof state before:
φ : Formula
hyp : ~~φ = φ
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: conNotSelfContainL
Proof state before:
φ1 φ2 : Formula
⊢ φ1⋀φ2 ≠ φ1
Tactic:
intro hyp
Proof state after:
φ1 φ2 : Formula
hyp : φ1⋀φ2 = φ1
⊢ False
Theorem: conNotSelfContainL
Proof state before:
φ1 φ2 : Formula
hyp : φ1⋀φ2 = φ1
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: conNotSelfContainR
Proof state before:
φ1 φ2 : Formula
⊢ φ1⋀φ2 ≠ φ2
Tactic:
intro hyp
Proof state after:
φ1 φ2 : Formula
hyp : φ1⋀φ2 = φ2
⊢ False
Theorem: conNotSelfContainR
Proof state before:
φ1 φ2 : Formula
hyp : φ1⋀φ2 = φ2
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: localRuleNoOverlap
Proof state before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
⊢ ∀ res ∈ ress, Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
Tactic:
intro res in_ress
Proof state after:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
Theorem: localRuleNoOverlap
Proof state before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
Tactic:
cases rule <;>
( rename_i rule
  cases rule
  all_goals aesop)
Proof state after:
no goals
Theorem: localRuleNoOverlap
Proof state before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ {~ϕ✝} ∩ res.1 = ∅ ∧ {ϕ✝} ∩ res.2 = ∅
Tactic:
rename_i rule
Proof state after:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ {~rule} ∩ res.1 = ∅ ∧ {rule} ∩ res.2 = ∅
Theorem: localRuleNoOverlap
Proof state before:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ {~rule} ∩ res.1 = ∅ ∧ {rule} ∩ res.2 = ∅
Tactic:
cases rule
Proof state after:
case LRnegR.bottom
res : SubPair
in_ress : res ∈ ∅
⊢ {~bottom} ∩ res.1 = ∅ ∧ {bottom} ∩ res.2 = ∅

case LRnegR.atom_prop
res : SubPair
in_ress : res ∈ ∅
a✝ : Char
⊢ {~·a✝} ∩ res.1 = ∅ ∧ {·a✝} ∩ res.2 = ∅

case LRnegR.neg
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~~a✝} ∩ res.1 = ∅ ∧ {~a✝} ∩ res.2 = ∅

case LRnegR.And
res : SubPair
in_ress : res ∈ ∅
a✝¹ a✝ : Formula
⊢ {~(a✝¹⋀a✝)} ∩ res.1 = ∅ ∧ {a✝¹⋀a✝} ∩ res.2 = ∅

case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅
Theorem: localRuleNoOverlap
Proof state before:
case LRnegR.bottom
res : SubPair
in_ress : res ∈ ∅
⊢ {~bottom} ∩ res.1 = ∅ ∧ {bottom} ∩ res.2 = ∅

case LRnegR.atom_prop
res : SubPair
in_ress : res ∈ ∅
a✝ : Char
⊢ {~·a✝} ∩ res.1 = ∅ ∧ {·a✝} ∩ res.2 = ∅

case LRnegR.neg
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~~a✝} ∩ res.1 = ∅ ∧ {~a✝} ∩ res.2 = ∅

case LRnegR.And
res : SubPair
in_ress : res ∈ ∅
a✝¹ a✝ : Formula
⊢ {~(a✝¹⋀a✝)} ∩ res.1 = ∅ ∧ {a✝¹⋀a✝} ∩ res.2 = ∅

case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: localRuleNoOverlap
Proof state before:
case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅
Tactic:
aesop
Proof state after:
no goals
Theorem: zlen_iff
Proof state before:
X Y : Finset Formula
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
Tactic:
have : ∀ W, zlengthOfSet W = lengthOfSet W := by intro W; simp
Proof state after:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
Theorem: zlen_iff
Proof state before:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
Tactic:
rw [this, this]
Proof state after:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
Theorem: zlen_iff
Proof state before:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
Tactic:
zify
Proof state after:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ ↑(lengthOf X) < ↑(lengthOf Y) ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
Theorem: zlen_iff
Proof state before:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ ↑(lengthOf X) < ↑(lengthOf Y) ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
Tactic:
simp
Proof state after:
no goals
Theorem: zlen_iff
Proof state before:
X Y : Finset Formula
⊢ ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
Tactic:
intro W
Proof state after:
X Y W : Finset Formula
⊢ zlengthOfSet W = ↑(lengthOfSet W)
Theorem: zlen_iff
Proof state before:
X Y W : Finset Formula
⊢ zlengthOfSet W = ↑(lengthOfSet W)
Tactic:
simp
Proof state after:
no goals
Theorem: zlengthOfSet.pos
Proof state before:
X : Finset Formula
⊢ zlengthOfSet X ≥ 0
Tactic:
apply Finset.sum_induction zlengthOf
Proof state after:
case hom
X : Finset Formula
⊢ ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → 0 ≤ a + b

case unit
X : Finset Formula
⊢ 0 ≤ 0

case base
X : Finset Formula
⊢ ∀ x ∈ X, 0 ≤ zlengthOf x
Theorem: zlengthOfSet.pos
Proof state before:
case hom
X : Finset Formula
⊢ ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → 0 ≤ a + b
Tactic:
intro a b a_ge b_ge
Proof state after:
case hom
X : Finset Formula
a b : ℤ
a_ge : 0 ≤ a
b_ge : 0 ≤ b
⊢ 0 ≤ a + b
Theorem: zlengthOfSet.pos
Proof state before:
case hom
X : Finset Formula
a b : ℤ
a_ge : 0 ≤ a
b_ge : 0 ≤ b
⊢ 0 ≤ a + b
Tactic:
linarith
Proof state after:
no goals
Theorem: zlengthOfSet.pos
Proof state before:
case unit
X : Finset Formula
⊢ 0 ≤ 0
Tactic:
simp
Proof state after:
no goals
Theorem: zlengthOfSet.pos
Proof state before:
case base
X : Finset Formula
⊢ ∀ x ∈ X, 0 ≤ zlengthOf x
Tactic:
intro f _
Proof state after:
case base
X : Finset Formula
f : Formula
a✝ : f ∈ X
⊢ 0 ≤ zlengthOf f
Theorem: zlengthOfSet.pos
Proof state before:
case base
X : Finset Formula
f : Formula
a✝ : f ∈ X
⊢ 0 ≤ zlengthOf f
Tactic:
exact zlengthOf.pos
Proof state after:
no goals
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf (X \ Cond ∪ Res) < lengthOf X
Tactic:
rw [zlen_iff]
Proof state after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) < zlengthOfSet X
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) < zlengthOfSet X
Tactic:
calc zlengthOfSet (X \ Cond ∪ Res)
    ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res := by
        have := @Finset.sum_union_inter _ _ (X \ Cond) Res zlengthOf _ _
        have : zlengthOfSet (X \ Cond ∩ Res) ≥ 0 := zlengthOfSet.pos
        simp_all
        linarith
  _ = zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res := by
        simp only [zlengthOfSet]
        rw [Finset.sum_sdiff_eq_sub precondProof]
  _ < zlengthOfSet X := by
        have : zlengthOfSet Res < zlengthOfSet Cond := by
          rw [← zlen_iff]
          exact hyp
        linarith
Proof state after:
no goals
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Tactic:
have := @Finset.sum_union_inter _ _ (X \ Cond) Res zlengthOf _ _
Proof state after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Tactic:
have : zlengthOfSet (X \ Cond ∩ Res) ≥ 0 := zlengthOfSet.pos
Proof state after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
this : zlengthOfSet (X \ Cond ∩ Res) ≥ 0
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
this : zlengthOfSet (X \ Cond ∩ Res) ≥ 0
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Tactic:
simp_all
Proof state after:
X Cond Res : Finset Formula
hyp : Res.sum lengthOfFormula < Cond.sum lengthOfFormula
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) + ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x) =
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
this : 0 ≤ ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x)
⊢ ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) ≤
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : Res.sum lengthOfFormula < Cond.sum lengthOfFormula
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) + ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x) =
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
this : 0 ≤ ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x)
⊢ ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) ≤
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
Tactic:
linarith
Proof state after:
no goals
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond) + zlengthOfSet Res = zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res
Tactic:
simp only [zlengthOfSet]
Proof state after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ (X \ Cond).sum zlengthOf + Res.sum zlengthOf = X.sum zlengthOf - Cond.sum zlengthOf + Res.sum zlengthOf
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ (X \ Cond).sum zlengthOf + Res.sum zlengthOf = X.sum zlengthOf - Cond.sum zlengthOf + Res.sum zlengthOf
Tactic:
rw [Finset.sum_sdiff_eq_sub precondProof]
Proof state after:
no goals
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X
Tactic:
have : zlengthOfSet Res < zlengthOfSet Cond := by
  rw [← zlen_iff]
  exact hyp
Proof state after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this : zlengthOfSet Res < zlengthOfSet Cond
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this : zlengthOfSet Res < zlengthOfSet Cond
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X
Tactic:
linarith
Proof state after:
no goals
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet Res < zlengthOfSet Cond
Tactic:
rw [← zlen_iff]
Proof state after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf Res < lengthOf Cond
Theorem: localRuleAppDecreasesLengthSide
Proof state before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf Res < lengthOf Cond
Tactic:
exact hyp
Proof state after:
no goals
Theorem: localRuleAppDecreasesLength
Proof state before:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
⊢ ∀ c ∈ C, lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
intro c c_child
Proof state after:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Theorem: localRuleAppDecreasesLength
Proof state before:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
let ⟨ress, Lcond, Rcond, rule, precondProofL, precondProofR⟩ := lrApp
Proof state after:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC✝ : C = applyLocalRule rule (L, R)
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Theorem: localRuleAppDecreasesLength
Proof state before:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC✝ : C = applyLocalRule rule (L, R)
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
rename_i C_def
Proof state after:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
C_def : C = applyLocalRule rule (L, R)
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Theorem: localRuleAppDecreasesLength
Proof state before:
C : List TNode
L R : Finset Formula
lrApp : LocalRuleApp (L, R) C
c : TNode
c_child : c ∈ C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
C_def : C = applyLocalRule rule (L, R)
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
subst C_def
Proof state after:
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
c_child : c ∈ applyLocalRule rule (L, R)
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Theorem: localRuleAppDecreasesLength
Proof state before:
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
c_child : c ∈ applyLocalRule rule (L, R)
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
simp only [applyLocalRule, List.mem_map] at c_child
Proof state after:
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
c_child : ∃ a ∈ ress, (L \ Lcond ∪ a.1, R \ Rcond ∪ a.2) = c
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Theorem: localRuleAppDecreasesLength
Proof state before:
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
c_child : ∃ a ∈ ress, (L \ Lcond ∪ a.1, R \ Rcond ∪ a.2) = c
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
rcases c_child with ⟨res, res_in_ress, def_c⟩
Proof state after:
case intro.intro
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Theorem: localRuleAppDecreasesLength
Proof state before:
case intro.intro
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
have lS := localRuleDecreasesLengthSide rule res res_in_ress
Proof state after:
case intro.intro
L R : Finset Formula
c : TNode
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
precondProofL : Lcond ⊆ L
precondProofR : Rcond ⊆ R
lrApp : LocalRuleApp (L, R) (applyLocalRule rule (L, R))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
lS : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)