Proof step 1 from proof allreadsok-ind-add-write (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  allReadsOKInd(mem, persisted, h), ¬ allReadsOKInd(mem, persisted, h + (W(t, l, v), b) ') ⊦

Rule argument

Additional information

Proof step 2 from proof allreadsok-ind-add-write (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  hPred([]), ∀ t, l, v, h. hPred(h) → hPred((W(t, l, v), true) ' + h), ∀ t, l, v, h. hPred(h) → hPred((W(t, l, v), false) ' + h), ∀ t, l, v, h. hPred(h) → hPred((R(t, l, v), true) ' + h), ∀ t, l, v, h. hPred(h) → hPred((R(t, l, v), false) ' + h) ⊦ hPred(h)

• Proof step 4:

  [] = h, allReadsOKInd(mem, persisted, h), ¬ allReadsOKInd(mem, persisted, h + (W(t, l, v), b) ') ⊦

• Proof step 5:

  ∀ mem, persisted, h1, t, l, v, b. ¬(h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t, l, v), b) ')) ⊦ ∀ mem, persisted, h1, t0, l0, v0, b. ¬((W(t, l, v), true) ' + h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t0, l0, v0), b) '))

• Proof step 7:

  ∀ mem, persisted, h1, t, l, v, b. ¬(h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t, l, v), b) ')) ⊦ ∀ mem, persisted, h1, t0, l0, v0, b. ¬((W(t, l, v), false) ' + h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t0, l0, v0), b) '))

• Proof step 9:

  ∀ mem, persisted, h1, t, l, v, b. ¬(h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t, l, v), b) ')) ⊦ ∀ mem, persisted, h1, t0, l0, v0, b. ¬((R(t, l, v), true) ' + h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t0, l0, v0), b) '))

• Proof step 11:

  ∀ mem, persisted, h1, t, l, v, b. ¬(h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t, l, v), b) ')) ⊦ ∀ mem, persisted, h1, t0, l0, v0, b. ¬((R(t, l, v), false) ' + h = h1 ∧ allReadsOKInd(mem, persisted, h1) ∧ ¬ allReadsOKInd(mem, persisted, h1 + (W(t0, l0, v0), b) '))

Rule argument

Additional information

Used terms: h, λ h0. ∀ mem, persisted, h, t, l, v, b. ¬ ( h0 = h ∧ allReadsOKInd(mem, persisted, h) ∧ ¬ allReadsOKInd(mem, persisted, h + (W(t, l, v), b) '))

Proof step 3 from proof allreadsok-ind-add-write (previous step) (back to tree)

Lemma hist-ind

Proof step 4 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: allReadsOKInd-base: ⊦ allReadsOKInd(mem, persisted, []); allreadsok-ind-one: ⊦ allReadsOKInd(mem, persisted, (e, b) ') ↔ e.W? ∨ e.R? ∧ e.v = mem(e.l) ∧ (b ↔ persisted(e.l)); ⊦ W(t, l, v).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 5 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  allReadsOKInd(mem(l := v), persisted(l := true), h), ¬ allReadsOKInd(mem(l := v), persisted(l := true), h + (W(t0, l0, v0), b) '), ∀ mem0, persisted0, t, l1, v1, b0. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (W(t, l1, v1), b0) ') ⊦

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); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 6 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem(l := v), persisted(l := true), t0, l0, v0, b

Proof step 7 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  allReadsOKInd(mem(l := v), persisted(l := false), h), ¬ allReadsOKInd(mem(l := v), persisted(l := false), h + (W(t0, l0, v0), b) '), ∀ mem0, persisted0, t, l1, v1, b0. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (W(t, l1, v1), b0) ') ⊦

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); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 8 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem(l := v), persisted(l := false), t0, l0, v0, b

Proof step 9 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  allReadsOKInd(mem, persisted, h), persisted(l), ¬ allReadsOKInd(mem, persisted, h + (W(t0, l0, v0), b) '), ∀ mem0, persisted0, t, l1, v1, b0. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (W(t, l1, v1), b0) ') ⊦

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); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 10 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, persisted, t0, l0, v0, b

Proof step 11 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  allReadsOKInd(mem, persisted, h), ¬ allReadsOKInd(mem, persisted, h + (W(t0, l0, v0), b) '), ¬ persisted(l), ∀ mem0, persisted0, t, l1, v1, b0. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (W(t, l1, v1), b0) ') ⊦

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); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 12 from proof allreadsok-ind-add-write (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mem, persisted, t0, l0, v0, b