Proof step 1 from proof allwritesOK-ind-pending-zero-write (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h |W | t) | false ≠ [], allWritesOKInd(pending, persisted, h), pending(t) ⊦

Rule argument

Additional information

Proof step 2 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], allWritesOKInd(pending, persisted, h), pending(t) ⊦

Rule argument

Additional information

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

Proof step 3 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

Proof step 4 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  allWritesOKInd(pending, persisted, vpe ' + h0), pending(t), ∀ t0, pending0, persisted0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h0) ∨ ¬ pending0(t0) ⊦ (vpe._1.W? ⊃ vpe ';[]).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._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 5 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used terms: e, boolvar

Proof step 6 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

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

• Proof step 11:

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

Rule argument

Additional information

Proof step 8 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

Proof step 9 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

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

Proof step 10 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

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 ⊦ [].filter(p) = []; (s) ⊦ e.W? → ((t = e.t ∧ l = e.l) ∧ v = e.v ↔ e = W(t, l, v)); (elim) Used terms: e, t1, l, v

Proof step 11 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

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

• Proof step 14:

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

Rule argument

Additional information

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

Proof step 12 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], allWritesOKInd(pending, persisted, h0), pending(t), ∀ t0, pending0, persisted0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h0) ∨ ¬ 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 13 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, pending, persisted

Proof step 14 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t).filter(λ vpe. ¬ vpe._2) ≠ [], allWritesOKInd(pending(t1 := ¬ boolvar), persisted(l := boolvar), h0), pending(t), ¬ pending(t1), boolvar → persisted(l), ∀ t0, pending0, persisted0. h0.filter(λ vpe. vpe._1.W?).filter(λ vpe. vpe._1.t = t0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allWritesOKInd(pending0, persisted0, h0) ∨ ¬ 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 15 from proof allwritesOK-ind-pending-zero-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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