Proof step 1 from proof rely-stable-write-empty (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h | t) | false = [], (h0 | t) | false ≠ [], rely(t, h, h0) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], h ⊑p h2 ⊦

Rule argument

Additional information

Used simplifier rules: restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b); rely-def: ⊦ rely(t, h0, h1) ↔ (∃ h2, h3. h1 = h2 + h3 ∧ h0 ⊑p h2 ∧ h3 | t = []); restrict-thread: ⊦ h | t = h.filter(λ vpe. vpe._1.t = t); ⊦ [].filter(p) = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

Proof step 3 from proof rely-stable-write-empty (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  h3.filter(λ vpe. vpe._1.t = t) = [], (vpe + h0).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe + h0 ⊑p h2, ∀ t, h3, h2. ¬ ( h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [] ∧ h3.filter(λ vpe. vpe._1.t = t) = [] ∧ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [] ∧ h0 ⊑p h2) ⊦

Rule argument

Additional information

Used simplifier rules: hist-more-persisted-base1: ⊦ [] ⊑p h ↔ h = []; List('a) freely generated by [], +;; ⊦ [].filter(p) = []; (s)

Proof step 4 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h3.filter(λ vpe. vpe._1.t = t) = [], (vpe._1.t = t ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) = [], h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

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

Proof step 5 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], (e.t = t ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], vpe = (e, boolvar), h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 6 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  h3.filter(λ vpe. vpe._1.t = t) = [], (e.t = t ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [], h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], (e, boolvar) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Proof step 7 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], (e, boolvar) '.filter(λ vpe. ¬ vpe._2) = [], e.t = t, h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], (e, boolvar) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

• Proof step 14:

  h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], [].filter(λ vpe. ¬ vpe._2) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], e.t ≠ t, (e, boolvar) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Proof step 8 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = e.t) = [], h2.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], (e, true) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s)

Proof step 9 from proof rely-stable-write-empty (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  h3.filter(λ vpe. vpe._1.t = e.t) = [], h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], h2 = vpe0 + h4, h2.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], (e, true) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

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

Proof step 10 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h3.filter(λ vpe. vpe._1.t = vpe0._1.t) = [], h0.filter(λ vpe. vpe._1.t = vpe0._1.t).filter(λ vpe. ¬ vpe._2) = [], h4.filter(λ vpe. vpe._1.t = vpe0._1.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, vpe0._2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used simplifier rules: hist-more-persisted-rec: ⊦ vpe0 ' + h0 ⊑p vpe1 ' + h1 ↔ vpe0._1 = vpe1._1 ∧ (vpe0._2 → vpe1._2) ∧ h0 ⊑p h1; ⊦ a ' ≠ []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 11 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = e.t) = [], boolvar, vpe0 = (e, boolvar), h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 12 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h3.filter(λ vpe. vpe._1.t = e.t) = [], h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Proof step 13 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: e.t, h3, h4

Proof step 14 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h3.filter(λ vpe. vpe._1.t = t) = [], h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], e.t ≠ t, (e, boolvar) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s)

Proof step 15 from proof rely-stable-write-empty (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 16:

  h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], h2 = vpe0 + h4, h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], e.t ≠ t, (e, boolvar) ' + h0 ⊑p h2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

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

Proof step 16 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe0._1.t ≠ t, h0 ⊑p h4, boolvar → vpe0._2, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used simplifier rules: hist-more-persisted-rec: ⊦ vpe0 ' + h0 ⊑p vpe1 ' + h1 ↔ vpe0._1 = vpe1._1 ∧ (vpe0._2 → vpe1._2) ∧ h0 ⊑p h1; ⊦ [].filter(p) = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 17 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 18:

  h3.filter(λ vpe. vpe._1.t = t) = [], h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], vpe0 = (e, boolvar0), h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], e.t ≠ t, h0 ⊑p h4, boolvar → boolvar0, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used terms: e, boolvar0

Proof step 18 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = t) = [], h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], e.t ≠ t, h0 ⊑p h4, boolvar → boolvar0, ∀ t0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ [] ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Proof step 19 from proof rely-stable-write-empty (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, h3, h4