Theorem: localRuleDecreasesLengthSide (Bml/Tableau.lean)

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
⊢ ∀ res ∈ ress, lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
Tactic:
intro res in_ress
State after:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
Tactic:
cases rule <;>
( first
  | ( rename_i rule
      cases rule
      <;> (simp at *; try rw [in_ress])
      case neg φ => simp [←Nat.add_assoc]
      case con φ ψ => simp; exact conDecreasesLength
      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)))
  | all_goals aesop)
State after:
no goals

State before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
first
| ( rename_i rule
    cases rule
    <;> (simp at *; try rw [in_ress])
    case neg φ => simp [←Nat.add_assoc]
    case con φ ψ => simp; exact conDecreasesLength
    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)))
| all_goals aesop
State after:
no goals

State before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
( rename_i rule
  cases rule
  <;> (simp at *; try rw [in_ress])
  case neg φ => simp [←Nat.add_assoc]
  case con φ ψ => simp; exact conDecreasesLength
  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)))
State after:
no goals

State before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
rename_i rule
State after:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~rule} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {rule} ∧ res.1 = ∅

State before:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~rule} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {rule} ∧ res.1 = ∅
Tactic:
cases rule
<;> (simp at *; try rw [in_ress])
State after:
no goals

State before:
res : SubPair
φ : Formula
in_ress : res = (∅, {φ})
⊢ (∅, {φ}).2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ) ∧ (∅, {φ}).1 = ∅
Tactic:
case neg φ => simp [←Nat.add_assoc]
State after:
no goals

State before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ (∅, {φ, ψ}).2.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ ∧ (∅, {φ, ψ}).1 = ∅
Tactic:
case con φ ψ => simp; exact conDecreasesLength
State after:
no goals

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

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

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]
State after:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ (∅, {φ✝, ψ✝}).2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ (∅, {φ✝, ψ✝}).1 = ∅

State before:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ res.2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ res.1 = ∅
Tactic:
rw [in_ress]
State after:
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ (∅, {φ✝, ψ✝}).2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ (∅, {φ✝, ψ✝}).1 = ∅

State before:
res : SubPair
φ : Formula
in_ress : res = (∅, {φ})
⊢ (∅, {φ}).2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ) ∧ (∅, {φ}).1 = ∅
Tactic:
simp [←Nat.add_assoc]
State after:
no goals

State before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ (∅, {φ, ψ}).2.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ ∧ (∅, {φ, ψ}).1 = ∅
Tactic:
simp
State after:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ {φ, ψ}.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ

State before:
res : SubPair
φ ψ : Formula
in_ress : res = (∅, {φ, ψ})
⊢ {φ, ψ}.sum lengthOfFormula < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
exact conDecreasesLength
State after:
no goals

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

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

State before:
case inr
res : SubPair
φ ψ : Formula
case_psi : res = (∅, {~ψ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
simp [case_psi]
State after:
no goals

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

State before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
Tactic:
simp [case_phi]
State after:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < 1 + lengthOfFormula φ + lengthOfFormula ψ

State before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
State after:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < lengthOfFormula φ + (1 + lengthOfFormula ψ)

State before:
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ lengthOfFormula φ < lengthOfFormula φ + (1 + lengthOfFormula ψ)
Tactic:
aesop
State after:
no goals

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

State before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
aesop
State after:
no goals