Proof step 1 from proof rely-unpersisted-subset (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  rely(t, h0, h1), ¬ (h1 | t) | false ⊆ (h0 | t) | false ⊦

Rule argument

Additional information

Proof step 2 from proof rely-unpersisted-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h3.filter(λ vpe. vpe._1.t = t) = [], h0 ⊑p h2, ¬ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ h0.filter(λ vpe. vpe._1.t = 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); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ [].filter(p) = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

Proof step 3 from proof rely-unpersisted-subset (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 + h ⊑p h2, ¬ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (vpe + h).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), ∀ h3, t, h2. ¬ ( h3.filter(λ vpe. vpe._1.t = t) = [] ∧ h ⊑p h2 ∧ ¬ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof rely-unpersisted-subset (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 ' + h ⊑p h2, ¬ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (vpe._1.t = t ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), ∀ h0, t0, h1. h0.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ ¬ h ⊑p h1 ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Used simplifier rules: 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) ⊦ a + x = a ' + x; (s)

Proof step 5 from proof rely-unpersisted-subset (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used terms: e, boolvar

Proof step 6 from proof rely-unpersisted-subset (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, boolvar) ' + h ⊑p h2, ¬ h2.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (e.t = t ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), ∀ h0, t0, h1. h0.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ ¬ h ⊑p h1 ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Proof step 7 from proof rely-unpersisted-subset (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: hist-more-persisted-base2: ⊦ ¬ vpe ' + h ⊑p []; List('a) freely generated by [], +;; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 8 from proof rely-unpersisted-subset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h3.filter(λ vpe. vpe._1.t = t) = [], h ⊑p h4, ¬ (vpe0._1.t = t ⊃ vpe0 ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (vpe0._1.t = t ⊃ (vpe0._1, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), boolvar → vpe0._2, ∀ h0, t0, h1. h0.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ ¬ h ⊑p h1 ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t0).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 ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s)

Proof step 9 from proof rely-unpersisted-subset (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used terms: e, boolvar0

Proof step 10 from proof rely-unpersisted-subset (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 = t) = [], h ⊑p h4, ¬ (e.t = t ⊃ (e, boolvar0) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (e.t = t ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), boolvar → boolvar0, ∀ h0, t0, h1. h0.filter(λ vpe. vpe._1.t = t0) ≠ [] ∨ ¬ h ⊑p h1 ∨ h1.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Proof step 11 from proof rely-unpersisted-subset (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  h3.filter(λ vpe. vpe._1.t = t) = [], h ⊑p h4, ¬ (e.t = t ⊃ (e, boolvar0) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (e.t = t ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), boolvar → boolvar0, h3.filter(λ vpe. vpe._1.t = t) ≠ [] ∨ ¬ h ⊑p h4 ∨ h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊦

Rule argument

Additional information

Used terms: h3, t, h4

Proof step 12 from proof rely-unpersisted-subset (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 = t) = [], h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), h ⊑p h4, ¬ (e.t = t ⊃ (e, boolvar0) ';[]).filter(λ vpe. ¬ vpe._2) + h4.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ⊆ (e.t = t ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) + h.filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2), boolvar → boolvar0 ⊦

Rule argument

Additional information

Proof step 13 from proof rely-unpersisted-subset (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

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