Proof step 1 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h2 |W | l) | true ≠ [], allWritesOKInd(pending, persisted, h1 + (W(t, l, v), false) ' + h2) ⊦

Rule argument

Additional information

Proof step 2 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, h1 + (W(t, l, v), false) ' + h2) ⊦

Rule argument

Additional information

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

Proof step 3 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, [] + (W(t, l, v), false) ' + h2) ⊦

• Proof step 27:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, (vpe + h) + (W(t, l, v), false) ' + h2), ∀ h2, l, pending, persisted, t, v. ¬(h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [] ∧ allWritesOKInd(pending, persisted, h + (W(t, l, v), false) ' + h2)) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 4 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), h2), ¬ pending(t) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recW: ⊦ allWritesOKInd(pending, persisted, (W(t, l, v), b) ' + h) ↔ ¬ pending(t) ∧ (b → persisted(l)) ∧ allWritesOKInd(pending(t := ¬ b), persisted(l := b), h); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 5 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  (vpe + h).filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), vpe + h), ¬ pending(t), ∀ l, pending, t, persisted. ¬ ( h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [] ∧ allWritesOKInd(pending(t := true), persisted(l := false), h) ∧ ¬ pending(t)) ⊦

Rule argument

Additional information

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

Proof step 6 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  allWritesOKInd(pending(t := true), persisted(l := false), vpe ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦ (vpe._1.W? ⊃ vpe ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) = [] ∧ h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = []

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 7 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  vpe = (e, boolvar), allWritesOKInd(pending(t := true), persisted(l := false), vpe ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦ (e.W? ⊃ vpe ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) = [] ∧ h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = []

Rule argument

Additional information

Used terms: e, boolvar

Proof step 8 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦ (e.W? ⊃ (e, boolvar) ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) = [] ∧ h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) = []

Rule argument

Additional information

Proof step 9 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  (e.W? ⊃ (e, boolvar) ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

• Proof step 15:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Proof step 10 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  (e.W? ⊃ (e, boolvar) ';[]).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], e.W?, allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s) Used formulas: e.W?

Proof step 11 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (e.l = l ⊃ (e, boolvar) ';[]).filter(._2) ≠ [], e.W?, allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

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

Proof step 12 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  e = W(t1, l1, v), (l1 = l ⊃ (e, boolvar) ';[]).filter(._2) ≠ [], e.W?, allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ e.W? → ((t = e.t ∧ l = e.l) ∧ v = e.v ↔ e = W(t, l, v)); (elim) Used terms: e, t1, l1, v

Proof step 13 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (l1 = l ⊃ (W(t1, l, v), boolvar) ';[]).filter(._2) ≠ [], t ≠ t1, allWritesOKInd(pending(t := true)(t1 := ¬ boolvar), persisted(l := false)(l1 := boolvar), h), ¬ pending(t), ¬ pending(t1), boolvar → l ≠ l1 ∧ persisted(l1), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recW: ⊦ allWritesOKInd(pending, persisted, (W(t, l, v), b) ' + h) ↔ ¬ pending(t) ∧ (b → persisted(l)) ∧ allWritesOKInd(pending(t := ¬ b), persisted(l := b), h); ⊦ W(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 14 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: persisted-update-same: ⊦ persisted(l := b0)(l := b) = persisted(l := b); ⊦ [].filter(p) = []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ a ' ≠ []; (s) Used formulas: l1 = l

Proof step 15 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 16:

  e = R(t1, l1, v), h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

• Proof step 18:

  e = W(t1, l1, v), h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), (e, boolvar) ' + h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;;

Proof step 16 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t := true), persisted(l := false), h), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recR: ⊦ allWritesOKInd(pending, persisted, (R(t, l, v), b) ' + h) ↔ allWritesOKInd(pending, persisted, h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 17 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, pending, t, persisted

Proof step 18 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], t ≠ t1, allWritesOKInd(pending(t := true)(t1 := ¬ boolvar), persisted(l := false)(l1 := boolvar), h), ¬ pending(t), ¬ pending(t1), boolvar → l ≠ l1 ∧ persisted(l1), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recW: ⊦ allWritesOKInd(pending, persisted, (W(t, l, v), b) ' + h) ↔ ¬ pending(t) ∧ (b → persisted(l)) ∧ allWritesOKInd(pending(t := ¬ b), persisted(l := b), h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 19 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ l0 ≠ l1 → persisted(l0 := b0)(l1 := b1) = persisted(l1 := b1)(l0 := b0)

• Proof step 21:

  l = l1, h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], t ≠ t1, allWritesOKInd(pending(t := true)(t1 := ¬ boolvar), persisted(l := false)(l1 := boolvar), h), ¬ pending(t), ¬ pending(t1), boolvar → l ≠ l1 ∧ persisted(l1), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

• Proof step 23:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], l ≠ l1, t ≠ t1, allWritesOKInd(pending(t := true)(t1 := ¬ boolvar), persisted(l1 := boolvar)(l := false), h), ¬ pending(t), ¬ pending(t1), boolvar → l ≠ l1 ∧ persisted(l1), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used terms: persisted, boolvar, l1, false, l

Proof step 20 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Lemma persisted-update-swap

Proof step 21 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l1).filter(._2) ≠ [], t ≠ t1, allWritesOKInd(pending(t := true)(t1 := true), persisted(l1 := false), h), ¬ pending(t1), ¬ pending(t), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used simplifier rules: persisted-update-same: ⊦ persisted(l := b0)(l := b) = persisted(l := b);

Proof step 22 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l1, pending(t := true), t1, persisted

Proof step 23 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], l ≠ l1, t ≠ t1, allWritesOKInd(pending(t := true)(t1 := ¬ boolvar), persisted(l1 := boolvar)(l := false), h), ¬ pending(t), ¬ pending(t1), boolvar → persisted(l1), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Proof step 24 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ t0 ≠ t1 → pending(t0 := b0)(t1 := b1) = pending(t1 := b1)(t0 := b0)

• Proof step 26:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], l ≠ l1, t ≠ t1, allWritesOKInd(pending(t1 := ¬ boolvar)(t := true), persisted(l1 := boolvar)(l := false), h), ¬ pending(t), ¬ pending(t1), boolvar → persisted(l1), ∀ l0, pending0, t0, persisted0. h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0(t0 := true), persisted0(l0 := false), h) ∨ pending0(t0) ⊦

Rule argument

Additional information

Used terms: ¬ boolvar, pending, true, t1, t

Proof step 25 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Lemma pending-update-swap

Proof step 26 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, pending(t1 := ¬ boolvar), t, persisted(l1 := boolvar)

Proof step 27 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, (vpe ' + h) + (W(t, l, v), false) ' + h2), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

Rule argument

Additional information

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

Proof step 28 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 29:

  vpe = (e, b), h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, (vpe ' + h) + (W(t, l, v), false) ' + h2), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

Rule argument

Additional information

Proof step 29 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, ((e, b) ' + h) + (W(t, l, v), false) ' + h2), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

Rule argument

Additional information

Proof step 30 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 31:

  e = R(t1, l1, v1), h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, ((e, b) ' + h) + (W(t, l, v), false) ' + h2), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

• Proof step 33:

  e = W(t1, l1, v1), h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, ((e, b) ' + h) + (W(t, l, v), false) ' + h2), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;;

Proof step 31 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending, persisted, h + (W(t, l, v), false) ' + h2), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recR: ⊦ allWritesOKInd(pending, persisted, (R(t, l, v), b) ' + h) ↔ allWritesOKInd(pending, persisted, h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 32 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: h2, l, pending, persisted, t, v

Proof step 33 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  h2.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l).filter(._2) ≠ [], allWritesOKInd(pending(t1 := ¬ b), persisted(l1 := b), h + (W(t, l, v), false) ' + h2), ¬ pending(t1), b → persisted(l1), ∀ h0, l0, pending0, persisted0, t0, v0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.l = l0).filter(._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h + (W(t0, l0, v0), false) ' + h0) ⊦

Rule argument

Additional information

Used simplifier rules: allWritesOKInd-recW: ⊦ allWritesOKInd(pending, persisted, (W(t, l, v), b) ' + h) ↔ ¬ pending(t) ∧ (b → persisted(l)) ∧ allWritesOKInd(pending(t := ¬ b), persisted(l := b), h); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 34 from proof allwritesOK-ind-one-unpersisted-write-no-persisted-after (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: h2, l, pending(t1 := ¬ b), persisted(l1 := b), t, v