Theorem: localRuleAppDecreasesLength (Bml/Tableau.lean)

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
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)

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
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)

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
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)

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
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)

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
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)

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⟩
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)

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
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)

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)

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
State after:
no goals

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]
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

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]
State after:
no goals

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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)

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
State after:
no goals

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]
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)

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]
State after:
no goals

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

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
State after:
no goals

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
State after:
no goals