Proof step 1 from proof restrict-t-b-empty-expand-loc (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [] ↔ (∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [])

Rule argument

Additional information

Used simplifier rules: restrict-loc: ⊦ h | l = h.filter(λ vpe. vpe._1.l = l); restrict-thread: ⊦ h | t = h.filter(λ vpe. vpe._1.t = t); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b);

Proof step 2 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 4:

  ⊦ ¬(∃ a. a ∈ h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2)) ↔ (∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [])

Rule argument

Additional information

Used terms: h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2)

Proof step 3 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ ¬(∃ vpe. vpe ∈ h ∧ vpe._1.t = t ∧ ¬ vpe._2) ↔ (∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [])

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 5 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  ⊦ ∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], ∃ vpe. vpe ∈ h ∧ vpe._1.t = t ∧ ¬ vpe._2

• Proof step 13:

  ∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], ∃ vpe. vpe ∈ h ∧ vpe._1.t = t ∧ ¬ vpe._2 ⊦

Rule argument

Additional information

Proof step 6 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [] ⊦ ∃ vpe. vpe ∈ h ∧ vpe._1.t = t ∧ ¬ vpe._2

Rule argument

Additional information

Proof step 7 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 9:

  ∃ a. a ∈ h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊦ ∃ vpe. vpe ∈ h ∧ vpe._1.t = t ∧ ¬ vpe._2

Rule argument

Additional information

Used terms: h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2)

Proof step 8 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  vpe ∈ h ⊦ vpe._2, ∃ vpe0. vpe0 ∈ h ∧ vpe0._1.t = vpe._1.t ∧ ¬ vpe0._2

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 10 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  ¬ boolvar, vpe = (e, boolvar), vpe ∈ h ⊦ ∃ vpe0. vpe0 ∈ h ∧ vpe0._1.t = e.t ∧ ¬ vpe0._2

Rule argument

Additional information

Used terms: e, boolvar

Proof step 11 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (e, false) ∈ h ⊦ ∃ vpe0. vpe0 ∈ h ∧ vpe0._1.t = e.t ∧ ¬ vpe0._2

Rule argument

Additional information

Proof step 12 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: (e, false)

Proof step 13 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  vpe ∈ h, ∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe0. vpe0._1.t = vpe._1.t).filter(λ vpe. ¬ vpe._2) = [] ⊦ vpe._2

Rule argument

Additional information

Proof step 14 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  ¬ boolvar, vpe = (e, boolvar), vpe ∈ h, ∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe0. vpe0._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 15 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (e, false) ∈ h, ∀ l. h.filter(λ vpe. vpe._1.l = l).filter(λ vpe0. vpe0._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [] ⊦

Rule argument

Additional information

Proof step 16 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  h.filter(λ vpe. vpe._1.l = e.l).filter(λ vpe0. vpe0._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], (e, false) ∈ h ⊦

Rule argument

Additional information

Used terms: e.l

Proof step 17 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 19:

  (e, false) ∈ h, ∀ a. ¬ a ∈ h.filter(λ vpe. vpe._1.l = e.l).filter(λ vpe0. vpe0._1.t = e.t).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Used terms: h.filter(λ vpe. vpe._1.l = e.l).filter(λ vpe0. vpe0._1.t = e.t).filter(λ vpe. ¬ vpe._2)

Proof step 18 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (e, false) ∈ h, ∀ a. ¬ a ∈ h ∨ a._1.l ≠ e.l ∨ a._1.t ≠ e.t ∨ a._2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 20 from proof restrict-t-b-empty-expand-loc (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: (e, false)