Proof step 1 from proof B-postfix-weak-same-loc (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  bel.forall(λ be. be = SF ∨ be.l = l), bel ⊒w bel0, ¬ bel0.forall(λ be. be = SF ∨ be.l = l) ⊦

Rule argument

Additional information

Proof step 2 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  bel.forall(λ be. be = SF ∨ be.l = l), ¬ bel0.forall(λ be. be = SF ∨ be.l = l), ∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel0.filter(λ be. be = SF ∨ be.l = l0) ⊦

Rule argument

Additional information

Used simplifier rules: B-postfix-weak: ⊦ bel0 ⊒w bel1 ↔ (∀ l. bel0 |SF l ⊒ bel1 |SF l); B-restrict-SF-l: ⊦ bel |SF l = bel.filter(λ be. be = SF ∨ be.l = l);

Proof step 3 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  bel.forall(λ be. be = SF ∨ be.l = l), ¬ (be + bel1).forall(λ be. be = SF ∨ be.l = l), ∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be + bel1).filter(λ be. be = SF ∨ be.l = l0), ∀ bel, l. ¬ ( bel.forall(λ be. be = SF ∨ be.l = l) ∧ ¬ bel1.forall(λ be. be = SF ∨ be.l = l) ∧ (∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0))) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ [].forall(p); (s)

Proof step 4 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  bel.forall(λ be. be = SF ∨ be.l = l), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be = SF ∨ be.l = l0 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l0) ⊦ (be = SF ∨ be.l = l) ∧ bel1.forall(λ be. be = SF ∨ be.l = l)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).forall(p) ↔ p(a) ∧ x.forall(p); (s)

Proof step 5 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  bel.forall(λ be. be = SF ∨ be.l = l), ∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be = SF ∨ be.l = l0 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ¬ bel.forall(λ be. be = SF ∨ be.l = l) ∨ bel1.forall(λ be. be = SF ∨ be.l = l) ∨ ¬(∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)) ⊦ (be = SF ∨ be.l = l) ∧ bel1.forall(λ be. be = SF ∨ be.l = l)

Rule argument

Additional information

Used terms: bel, l

Proof step 6 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  bel.forall(λ be. be = SF ∨ be.l = l), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be = SF ∨ be.l = l0 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l0), bel1.forall(λ be. be = SF ∨ be.l = l) ∨ ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0) ⊦ (be = SF ∨ be.l = l) ∧ bel1.forall(λ be. be = SF ∨ be.l = l)

Rule argument

Additional information

Proof step 7 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  bel.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be = SF ∨ be.l = l0 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ l0. bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be = SF ∨ be.l = l0 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), bel1.forall(λ be. be = SF ∨ be.l = l) ∨ ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0) ⊦ (be = SF ∨ be.l = l) ∧ bel1.forall(λ be. be = SF ∨ be.l = l)

Rule argument

Additional information

Used terms: l0

Proof step 8 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  be.l ≠ l, be ≠ SF, bel.forall(λ be. be = SF ∨ be.l = l), bel1.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (be.l = l0 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ z ⊒ x + y → z ⊒ y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 9 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  be.l = l0, be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), bel.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ be ' + bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)) ⊦

• Proof step 17:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), bel.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ [] + bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)) ⊦

Rule argument

Additional information

Proof step 10 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  be.l ≠ l, be ≠ SF, bel.forall(λ be. be = SF ∨ be.l = l), bel1.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1) ⊦

Rule argument

Additional information

Proof step 11 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ a ∈ x ∧ ¬ a ∈ y → ¬ y ⊒ x

• Proof step 13:

  be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), bel.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)) ⊦ be ∈ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l) ∧ ¬ be ∈ bel.filter(λ be0. be0 = SF ∨ be0.l = be.l)

Rule argument

Additional information

Used terms: bel.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), be

Proof step 12 from proof B-postfix-weak-same-loc (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  be.l ≠ l, be ≠ SF, bel.forall(λ be. be = SF ∨ be.l = l), bel1.forall(λ be. be = SF ∨ be.l = l), be ∈ bel, bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s)

Proof step 14 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ x.forall(p) ↔ (∀ a. a ∈ x → p(a))

• Proof step 16:

  be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), be ∈ bel, bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ a. a ∈ bel → a = SF ∨ a.l = l ⊦

Rule argument

Additional information

Used terms: bel, λ be. be = SF ∨ be.l = l

Proof step 15 from proof B-postfix-weak-same-loc (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: be

Proof step 17 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel.forall(λ be. be = SF ∨ be.l = l), bel1.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 18 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), bel.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0), bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ (be.l = be.l ⊃ be ';[]) + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)) ⊦

Rule argument

Additional information

Used terms: be.l

Proof step 19 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel.forall(λ be. be = SF ∨ be.l = l), bel1.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0), bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1) ⊦

Rule argument

Additional information

Proof step 20 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ a ∈ x ∧ ¬ a ∈ y → ¬ y ⊒ x

• Proof step 22:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), bel.forall(λ be. be = SF ∨ be.l = l), bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)) ⊦ be ∈ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l) ∧ ¬ be ∈ bel.filter(λ be0. be0 = SF ∨ be0.l = be.l)

Rule argument

Additional information

Used terms: bel.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), be

Proof step 21 from proof B-postfix-weak-same-loc (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel.forall(λ be. be = SF ∨ be.l = l), bel1.forall(λ be. be = SF ∨ be.l = l), be ∈ bel, bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0), bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s)

Proof step 23 from proof B-postfix-weak-same-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ x.forall(p) ↔ (∀ a. a ∈ x → p(a))

• Proof step 25:

  be.l ≠ l0, be.l ≠ l, be ≠ SF, bel1.forall(λ be. be = SF ∨ be.l = l), be ∈ bel, bel.filter(λ be0. be0 = SF ∨ be0.l = be.l) ⊒ be ' + bel1.filter(λ be0. be0 = SF ∨ be0.l = be.l), bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0), ∀ l1. bel.filter(λ be. be = SF ∨ be.l = l1) ⊒ (be.l = l1 ⊃ be ';[]) + bel1.filter(λ be. be = SF ∨ be.l = l1), ∀ bel0, l0. ¬ bel0.forall(λ be. be = SF ∨ be.l = l0) ∨ bel1.forall(λ be. be = SF ∨ be.l = l0) ∨ ¬(∀ l0. bel0.filter(λ be. be = SF ∨ be.l = l0) ⊒ bel1.filter(λ be. be = SF ∨ be.l = l0)), ∀ a. a ∈ bel → a = SF ∨ a.l = l ⊦

Rule argument

Additional information

Used terms: bel, λ be. be = SF ∨ be.l = l

Proof step 24 from proof B-postfix-weak-same-loc (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof B-postfix-weak-same-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: be