internlm/Lean-Github huggingface dataset:
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
lS : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
have := localRuleNoOverlap 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 = ∅
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
⊢ 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
lS : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
cases lS
Proof state after:
case intro.intro.inl
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
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
h✝ : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)

case intro.intro.inr
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
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
h✝ : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ 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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
case inl hyp =>
  calc lengthOfTNode c
  = lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2) :=
      by subst def_c; simp
  _ ≤ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R :=
      by rw [hyp.2]; simp [Finset.sum_le_sum_of_subset]
  _ < lengthOfSet L + lengthOfSet R :=
      by have := localRuleAppDecreasesLengthSide L Lcond res.1 hyp.1 precondProofL; aesop
  _ = lengthOfTNode (L, R) := by simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
case inr hyp =>
  calc lengthOfTNode c
  = lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2) :=
      by subst def_c; simp
  _ ≤ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2) :=
      by rw [hyp.2]; simp [Finset.sum_le_sum_of_subset]
  _ < lengthOfSet L + lengthOfSet R :=
      by have := localRuleAppDecreasesLengthSide R Rcond res.2 hyp.1 precondProofR; aesop
  _ = lengthOfTNode (L, R) := by simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
calc lengthOfTNode c
= lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2) :=
    by subst def_c; simp
_ ≤ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R :=
    by rw [hyp.2]; simp [Finset.sum_le_sum_of_subset]
_ < lengthOfSet L + lengthOfSet R :=
    by have := localRuleAppDecreasesLengthSide L Lcond res.1 hyp.1 precondProofL; aesop
_ = lengthOfTNode (L, R) := by simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode c = lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2)
Tactic:
subst def_c
Proof state after:
L R : Finset Formula
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
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) =
    lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2)
Theorem: localRuleAppDecreasesLength
Proof state before:
L R : Finset Formula
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
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfTNode (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) =
    lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2)
Tactic:
simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2) ≤ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R
Tactic:
rw [hyp.2]
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ ∅) ≤ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet 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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ ∅) ≤ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R
Tactic:
simp [Finset.sum_le_sum_of_subset]
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R < lengthOfSet L + lengthOfSet R
Tactic:
have := localRuleAppDecreasesLengthSide L Lcond res.1 hyp.1 precondProofL
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this✝ : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
this : lengthOf (L \ Lcond ∪ res.1) < lengthOf L
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R < lengthOfSet L + lengthOfSet 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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this✝ : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
this : lengthOf (L \ Lcond ∪ res.1) < lengthOf L
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet R < lengthOfSet L + lengthOfSet R
Tactic:
aesop
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅
⊢ lengthOfSet L + lengthOfSet R = lengthOfTNode (L, R)
Tactic:
simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode c < lengthOfTNode (L, R)
Tactic:
calc lengthOfTNode c
= lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2) :=
    by subst def_c; simp
_ ≤ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2) :=
    by rw [hyp.2]; simp [Finset.sum_le_sum_of_subset]
_ < lengthOfSet L + lengthOfSet R :=
    by have := localRuleAppDecreasesLengthSide R Rcond res.2 hyp.1 precondProofR; aesop
_ = lengthOfTNode (L, R) := by simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode c = lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2)
Tactic:
subst def_c
Proof state after:
L R : Finset Formula
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
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) =
    lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2)
Theorem: localRuleAppDecreasesLength
Proof state before:
L R : Finset Formula
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
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfTNode (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) =
    lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2)
Tactic:
simp
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfSet (L \ Lcond ∪ res.1) + lengthOfSet (R \ Rcond ∪ res.2) ≤ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2)
Tactic:
rw [hyp.2]
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfSet (L \ Lcond ∪ ∅) + lengthOfSet (R \ Rcond ∪ res.2) ≤ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2)
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfSet (L \ Lcond ∪ ∅) + lengthOfSet (R \ Rcond ∪ res.2) ≤ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2)
Tactic:
simp [Finset.sum_le_sum_of_subset]
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2) < lengthOfSet L + lengthOfSet R
Tactic:
have := localRuleAppDecreasesLengthSide R Rcond res.2 hyp.1 precondProofR
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this✝ : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
this : lengthOf (R \ Rcond ∪ res.2) < lengthOf R
⊢ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2) < lengthOfSet L + lengthOfSet 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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this✝ : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
this : lengthOf (R \ Rcond ∪ res.2) < lengthOf R
⊢ lengthOfSet L + lengthOfSet (R \ Rcond ∪ res.2) < lengthOfSet L + lengthOfSet R
Tactic:
aesop
Proof state after:
no goals
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))
res : SubPair
res_in_ress : res ∈ ress
def_c : (L \ Lcond ∪ res.1, R \ Rcond ∪ res.2) = c
this : Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
hyp : lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
⊢ lengthOfSet L + lengthOfSet R = lengthOfTNode (L, R)
Tactic:
simp
Proof state after:
no goals
Theorem: proj_does_not_increase_vocab
Proof state before:
X : Finset Formula
⊢ voc (projection X) ⊆ voc X
Tactic:
simp
Proof state after:
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula
Theorem: proj_does_not_increase_vocab
Proof state before:
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula
Tactic:
intro φ φ_in_proj ℓ ℓ_in_φ
Proof state after:
X : Finset Formula
φ : Formula
φ_in_proj : φ ∈ projection X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
Theorem: proj_does_not_increase_vocab
Proof state before:
X : Finset Formula
φ : Formula
φ_in_proj : φ ∈ projection X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
Tactic:
rw [proj] at φ_in_proj
Proof state after:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
Theorem: proj_does_not_increase_vocab
Proof state before:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
Tactic:
simp
Proof state after:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ X, ℓ ∈ vocabOfFormula a
Theorem: proj_does_not_increase_vocab
Proof state before:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ X, ℓ ∈ vocabOfFormula a
Tactic:
tauto
Proof state after:
no goals
Theorem: vocProj
Proof state before:
X : Finset Formula
⊢ voc (projection X) ⊆ voc X
Tactic:
simp
Proof state after:
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula
Theorem: vocProj
Proof state before:
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula
Tactic:
intro ϕ phi_in_proj
Proof state after:
X : Finset Formula
ϕ : Formula
phi_in_proj : ϕ ∈ projection X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
Theorem: vocProj
Proof state before:
X : Finset Formula
ϕ : Formula
phi_in_proj : ϕ ∈ projection X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
Tactic:
rw [proj] at phi_in_proj
Proof state after:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
Theorem: vocProj
Proof state before:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
Tactic:
intro a aInVocPhi
Proof state after:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ a ∈ X.biUnion vocabOfFormula
Theorem: vocProj
Proof state before:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ a ∈ X.biUnion vocabOfFormula
Tactic:
simp
Proof state after:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Theorem: vocProj
Proof state before:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
tauto
Proof state after:
no goals
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
⊢ jvoc (diamondProjectTNode (Sum.inl φ) (L, R)) ⊆ jvoc (L, R)
Tactic:
intro ℓ ℓ_in_proj
Proof state after:
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inl φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inl φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)
Tactic:
unfold jvoc at *
Proof state after:
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2
Tactic:
apply Finset.mem_inter_of_mem
Proof state after:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1

case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1
Tactic:
have ℓ_left := (Finset.mem_inter.mp ℓ_in_proj).left
Proof state after:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1
Tactic:
simp [diamondProjectTNode ] at ℓ_left
Proof state after:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).1