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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h | t) | false = (W(t, l, v), b) ', (h0 | t) | false ≠ (W(t, l, v), b) ', (h0 | t) | false ≠ [], rely(t, h, h0) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-stable-write-one (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) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', 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 + [] = x; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 3 from proof rely-stable-write-one (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) = (W(t, l, v), b) ', h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe + h0 ⊑p h2, ∀ t, l, v, b, h3, h2. ¬ ( h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ' ∧ h3.filter(λ vpe. vpe._1.t = t) = [] ∧ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ' ∧ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [] ∧ h0 ⊑p h2) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (vpe._1.t = t ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe ' + h0 ⊑p h2, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ 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).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-one (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  (e.t = t ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], vpe = (e, b0), h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], vpe ' + h0 ⊑p h2, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦

Rule argument

Additional information

Used terms: e, b0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], (e, b0) ' + h0 ⊑p h2, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ 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-one (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], h2 = vpe0 + h4, h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], (e, b0) ' + h0 ⊑p h2, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ 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 [], +;; ⊦ a ' ≠ []; (s) ⊦ [].filter(p) = []; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (vpe0._1.t = t ⊃ (vpe0._1, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], (vpe0._1.t = t ⊃ vpe0 ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h0 ⊑p h4, b0 → vpe0._2, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ (vpe0._1.t = t ⊃ vpe0 ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = []

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: ⊦ (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 9 from proof rely-stable-write-one (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], vpe0 = (e, b1), (e.t = t ⊃ vpe0 ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ (e.t = t ⊃ vpe0 ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used terms: e, b1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 12:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1, h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ' ∨ h3.filter(λ vpe. vpe._1.t = t) ≠ [] ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h4 ⊦ (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used terms: t, l, v, b, h3, h4

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1, h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [] ⊦ (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 14:

  (e.t = t ⊃ (e, b0) ';[]).filter(λ vpe. ¬ vpe._2) + h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = t) = [], e.t = t, (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1, h0.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ (W(t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = (W(t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [] ⊦ (e.t = t ⊃ (e, b1) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [].filter(p) = []; (s) Used formulas: e.t = t

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (¬ b0 ⊃ (e, false) ';[]) + h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = (W(e.t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = e.t) = [], (¬ b1 ⊃ (e, false) ';[]) + h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ (W(e.t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1, h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ (W(e.t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = (W(e.t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [] ⊦ b1 ∧ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  (¬ b0 ⊃ (e, false) ';[]) + h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = (W(e.t, l, v), b) ', h3.filter(λ vpe. vpe._1.t = e.t) = [], ¬ b0, (¬ b1 ⊃ (e, false) ';[]) + h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ (W(e.t, l, v), b) ', h0 ⊑p h4, b0 → b1, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1, h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ (W(e.t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = (W(e.t, l, v), b) ' ∨ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [] ⊦ b1 ∧ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ y ≠ [] → (a ' = x + y ↔ x = [] ∧ a ' = y); (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: ¬ b0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h3.filter(λ vpe. vpe._1.t = e.t) = [], h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], W(e.t, l, v) = e, (¬ b1 ⊃ (e, false) ';[]) + h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ (e, false) ', h0 ⊑p h4, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ b1 ∧ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

  h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = e.t) = [], W(e.t, l, v) = e, (¬ b1 ⊃ (e, false) ';[]) + h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ (e, false) ', h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ b1 ∧ h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used simplifier rules: ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h3.filter(λ vpe. vpe._1.t = e.t) = [], h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], W(e.t, l, v) = e, h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ b1 ∧ (e, false) ' = h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2)

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], h3.filter(λ vpe. vpe._1.t = e.t) = [], W(e.t, l, v) = e, h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, rely(e.t, h0, h4) ∧ (h0 | e.t) | false = [] → (h4 | e.t) | false = [], ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ b1 ∧ (e, false) ' = h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2)

Rule argument

Additional information

Used terms: e.t, h0, h4

Proof step 20 from proof rely-stable-write-one (previous step) (back to tree)

Lemma rely-stable-write-empty

Proof step 21 from proof rely-stable-write-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  h3.filter(λ vpe. vpe._1.t = e.t) = [], h0.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) = [], W(e.t, l, v) = e, h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2) ≠ [], h0 ⊑p h4, ∀ t0, l0, v0, b0, h, h1. h0.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ≠ (W(t0, l0, v0), b0) ' ∨ h.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = (W(t0, l0, v0), b0) ' ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ h0 ⊑p h1 ⊦ ∃ h2, h. h4 = h2 + h ∧ h0 ⊑p h2 ∧ h.filter(λ vpe. vpe._1.t = e.t) = [], b1 ∧ (e, false) ' = h4.filter(λ vpe. vpe._1.t = e.t).filter(λ vpe. ¬ vpe._2)

Rule argument

Additional information

Used simplifier rules: 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); restrict-vp: ⊦ h | b = h.filter(λ vpe. vpe._2 ↔ b);

Proof step 22 from proof rely-stable-write-one (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [].filter(p) = []; (s) Used terms: h4, []