Proof step 1 from proof allreadsok-ind-add-read (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 + (R(t, l, ((mem ⊕ h))(l)), h.lastPersistedOrElse(l, persisted(l))) ') ⊦

Rule argument

Additional information

Proof step 2 from proof allreadsok-ind-add-read (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 + (R(t, l, ((mem ⊕ h))(l)), h.lastPersistedOrElse(l, persisted(l))) ') ⊦

• Proof step 5:

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

• Proof step 7:

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

• Proof step 9:

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

• Proof step 11:

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

Rule argument

Additional information

Used terms: h, λ h0. ∀ mem, persisted, h, t, l. ¬ ( h0 = h ∧ allReadsOKInd(mem, persisted, h) ∧ ¬ allReadsOKInd (mem, persisted, h + (R(t, l, ((mem ⊕ h))(l)), h.lastPersistedOrElse(l, persisted(l))) '))

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

Lemma hist-ind

Proof step 4 from proof allreadsok-ind-add-read (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, []); overwrite-base: ⊦ mem ⊕ [] = mem; lastPersistedOrElse-base: ⊦ [].lastPersistedOrElse(l, b) ↔ b; allreadsok-ind-one: ⊦ allReadsOKInd(mem, persisted, (e, b) ') ↔ e.W? ∨ e.R? ∧ e.v = mem(e.l) ∧ (b ↔ persisted(e.l)); ⊦ R(t, l, v).l = l; (s) ⊦ R(t, l, v).v = v; (s) ⊦ R(t, l, v).R?; (s) ⊦ ¬ R(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-read (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 + (R(t0, l0, ((mem(l := v) ⊕ h))(l0)), h.lastPersistedOrElse(l0, l0 ≠ l → persisted(l0))) '), ∀ mem0, persisted0, t, l1. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (R(t, l1, ((mem0 ⊕ h))(l1)), h.lastPersistedOrElse(l1, persisted0(l1))) ') ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; lastPersistedOrElse-recW: ⊦ ((W(t0, l0, v0), b0) ' + h).lastPersistedOrElse(l, b) ↔ h.lastPersistedOrElse(l, (l = l0 ⊃ b0;b)); 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-read (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 7 from proof allreadsok-ind-add-read (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 + (R(t0, l0, ((mem(l := v) ⊕ h))(l0)), h.lastPersistedOrElse(l0, l0 ≠ l ∧ persisted(l0))) '), ∀ mem0, persisted0, t, l1. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (R(t, l1, ((mem0 ⊕ h))(l1)), h.lastPersistedOrElse(l1, persisted0(l1))) ') ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-write: ⊦ mem ⊕ ((W(t, l, v), b) ' + h) = mem(l := v) ⊕ h; lastPersistedOrElse-recW: ⊦ ((W(t0, l0, v0), b0) ' + h).lastPersistedOrElse(l, b) ↔ h.lastPersistedOrElse(l, (l = l0 ⊃ b0;b)); 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-read (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 9 from proof allreadsok-ind-add-read (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 + (R(t0, l0, ((mem ⊕ h))(l0)), h.lastPersistedOrElse(l0, persisted(l0))) '), ∀ mem0, persisted0, t, l1. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (R(t, l1, ((mem0 ⊕ h))(l1)), h.lastPersistedOrElse(l1, persisted0(l1))) ') ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; lastPersistedOrElse-recR: ⊦ ((R(t0, l0, v0), b0) ' + h).lastPersistedOrElse(l, b) ↔ h.lastPersistedOrElse(l, b); 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-read (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

Proof step 11 from proof allreadsok-ind-add-read (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 + (R(t0, l0, ((mem ⊕ h))(l0)), h.lastPersistedOrElse(l0, persisted(l0))) '), ¬ persisted(l), ∀ mem0, persisted0, t, l1. ¬ allReadsOKInd(mem0, persisted0, h) ∨ allReadsOKInd(mem0, persisted0, h + (R(t, l1, ((mem0 ⊕ h))(l1)), h.lastPersistedOrElse(l1, persisted0(l1))) ') ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec-read: ⊦ mem ⊕ ((R(t, l, v), b) ' + h) = mem ⊕ h; lastPersistedOrElse-recR: ⊦ ((R(t0, l0, v0), b0) ' + h).lastPersistedOrElse(l, b) ↔ h.lastPersistedOrElse(l, b); 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-read (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