Proof step 1 from proof allReadsOK-nowrites-allpersisted-ind (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ((h | l) | false)|W = [], (h | l) | false ≠ [], allReadsOKInd(mem, persisted, h), persisted(l) ⊦

Rule argument

Additional information

Proof step 2 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], h.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], allReadsOKInd(mem, persisted, h), persisted(l) ⊦

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 allReadsOK-nowrites-allpersisted-ind (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.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (vpe + h0).filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], allReadsOKInd(mem, persisted, vpe + h0), persisted(l), ∀ l, mem, persisted. ¬ ( h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [] ∧ allReadsOKInd(mem, persisted, h0) ∧ persisted(l)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (vpe._1.l = l ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem, persisted, vpe ' + h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (vpe._1.l = l ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).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 allReadsOK-nowrites-allpersisted-ind (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.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (e.l = l ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], vpe = (e, boolvar), allReadsOKInd(mem, persisted, vpe ' + h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (e.l = l ⊃ vpe ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used terms: e, boolvar

Proof step 6 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (e.l = l ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (e.l = l ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Proof step 7 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (e.l = l ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], e = R(t, l1, v), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (e.l = l ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

• Proof step 14:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (e.l = l ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], e = W(t, l1, v), allReadsOKInd(mem, persisted, (e, boolvar) ' + h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (e.l = l ⊃ (e, boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

Proof step 8 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (l1 = l ⊃ (R(t, l, mem(l)), true) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem, persisted, h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (l1 = l ⊃ (R(t, l, mem(l)), true) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

Proof step 9 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (R(t, l, mem(l)), true) '.filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], l1 = l, allReadsOKInd(mem, persisted, h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (l1 = l ⊃ (R(t, l, mem(l)), true) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

• Proof step 12:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], [].filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], l1 ≠ l, allReadsOKInd(mem, persisted, h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (l1 = l ⊃ (R(t, l, mem(l)), true) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Proof step 10 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], allReadsOKInd(mem, persisted, h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦

Rule argument

Additional information

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

Proof step 11 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem, persisted

Proof step 12 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) ≠ [], l1 ≠ l, allReadsOKInd(mem, persisted, h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦

Rule argument

Additional information

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

Proof step 13 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, mem, persisted

Proof step 14 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem(l1 := v), persisted(l1 := boolvar), h0), persisted(l), ∀ l0, mem0, persisted0. h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l0).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem0, persisted0, h0) ∨ ¬ persisted0(l0) ⊦ (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used simplifier rules: allReadsOKInd-recW: ⊦ allReadsOKInd(mem, persisted, (W(t, l, v), b) ' + h) ↔ allReadsOKInd(mem(l := v), persisted(l := b), h); ⊦ W(t, l, v).l = l; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 15 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem(l1 := v), persisted(l1 := boolvar), h0), persisted(l), h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) ≠ [] ∨ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ allReadsOKInd(mem(l1 := v), persisted(l1 := boolvar), h0) ∨ ¬ persisted(l1 := boolvar)(l) ⊦ (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Used terms: l, mem(l1 := v), persisted(l1 := boolvar)

Proof step 16 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem(l1 := v), persisted(l1 := boolvar), h0), persisted(l), h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬(l1 = l → boolvar) ⊦ (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

Proof step 17 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (W(t, l, v), boolvar) '.filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], l1 = l, allReadsOKInd(mem(l1 := v), persisted(l1 := boolvar), h0), persisted(l), h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬(l1 = l → boolvar) ⊦ (l1 = l ⊃ (W(t, l, v), boolvar) ';[]).filter(λ vpe. ¬ vpe._2) = [] ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

Proof step 18 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2).filter(λ vpe. vpe._1.W?) = [], (¬ boolvar ⊃ (W(t, l, v), false) ';[]).filter(λ vpe. vpe._1.W?) = [], allReadsOKInd(mem(l := v), persisted(l := boolvar), h0), persisted(l), h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = [] ∨ ¬ boolvar ⊦ boolvar ∧ h0.filter(λ vpe. vpe._1.l = l).filter(λ vpe. ¬ vpe._2) = []

Rule argument

Additional information

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

Proof step 19 from proof allReadsOK-nowrites-allpersisted-ind (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [].filter(p) = []; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ W(t, l, v).W?; (s) ⊦ a ' ≠ []; (s)