Proof step 1 from proof step-invRead-resRead (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, pcstepf(gs, ls, invRead, a) = resRead, allReadsOK(gs.h), allWritesOK(gs.h), pre(gs, ls, invRead, a) ⊦ allReadsOK(gstepf(gs, ls, invRead, a).h) ∧ allWritesOK(gstepf(gs, ls, invRead, a).h) ∧ gstepf(gs, ls, invRead, a).vm = ∅ ⊕ gstepf(gs, ls, invRead, a).h ∧ gstepf(gs, ls, invRead, a).pm = ∅ ⊕ (gstepf(gs, ls, invRead, a).h | true)

Rule argument

Additional information

Proof step 2 from proof step-invRead-resRead (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, allReadsOK(gs.h), allWritesOK(gs.h) ⊦ allReadsOK(gs.h + (R(ls.t, ls.il, gs.vm(ls.il)), gs.h.lastPersistedOrElse(ls.il, true)) ') ∧ gs.pm = ∅ ⊕ ((gs.h | true) + (gs.h.lastPersistedOrElse(ls.il, true) ⊃ (R(ls.t, ls.il, gs.vm(ls.il)), true) ';[]))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ (gs.h:= h).h = h; (s) ⊦ x + a = x + a '; (s) ⊦ ls.t = t → gstepf(gs, ls, invRead, ADoRead(t)) = gs .h:= (gs.h + (R(ls.t, ls.il, gs.vm(ls.il)), gs.h.lastPersistedOrElse(ls.il, true))); (s) ⊦ (gs.h:= h).pm = gs.pm; (s) ⊦ mem ⊕ (h + (R(t, l, v), b) ') = mem ⊕ h; (s) ⊦ (gs.h:= h).vm = gs.vm; (s) ⊦ allWritesOK(h) → allWritesOK(h + (R(t, l, v), b) '); (ss) ⊦ ls.t = t → pcstepf(gs, ls, invRead, ADoRead(t)) = resRead; (s) ⊦ pre(gs, ls, invRead, a) ↔ a = ADoRead(ls.t); (s)

Proof step 3 from proof step-invRead-resRead (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 4:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, allReadsOK(gs.h), allWritesOK(gs.h) ⊦ allReadsOK(gs.h + (R(ls.t, ls.il, ((∅ ⊕ gs.h))(ls.il)), gs.h.lastPersistedOrElse(ls.il, true)) ') ∧ gs.pm = ∅ ⊕ ((gs.h | true) + (gs.h.lastPersistedOrElse(ls.il, true) ⊃ (R(ls.t, ls.il, ((∅ ⊕ gs.h))(ls.il)), true) ';[]))

Rule argument

Additional information

Proof step 4 from proof step-invRead-resRead (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ⊦ allReadsOK(h) → allReadsOK(h + (R(t, l, ((∅ ⊕ h))(l)), h.lastPersistedOrElse(l, true)) ')

• Proof step 6:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, allReadsOK(gs.h), allWritesOK(gs.h), allReadsOK(gs.h) → allReadsOK(gs.h + (R(ls.t, ls.il, ((∅ ⊕ gs.h))(ls.il)), gs.h.lastPersistedOrElse(ls.il, true)) ') ⊦ allReadsOK(gs.h + (R(ls.t, ls.il, ((∅ ⊕ gs.h))(ls.il)), gs.h.lastPersistedOrElse(ls.il, true)) ') ∧ gs.pm = ∅ ⊕ ((gs.h | true) + (gs.h.lastPersistedOrElse(ls.il, true) ⊃ (R(ls.t, ls.il, ((∅ ⊕ gs.h))(ls.il)), true) ';[]))

Rule argument

Additional information

Used terms: gs.h, ls.t, ls.il

Proof step 5 from proof step-invRead-resRead (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof step-invRead-resRead (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, gs.pm ≠ ∅ ⊕ ((gs.h | true) + (gs.h.lastPersistedOrElse(ls.il, true) ⊃ (R(ls.t, ls.il, gs.vm(ls.il)), true) ';[])), allReadsOK(gs.h), allReadsOK(gs.h + (R(ls.t, ls.il, gs.vm(ls.il)), gs.h.lastPersistedOrElse(ls.il, true)) '), allWritesOK(gs.h) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ allReadsOK(h) → allReadsOK(h + (R(t, l, ((∅ ⊕ h))(l)), h.lastPersistedOrElse(l, true)) '); (ss)

Proof step 7 from proof step-invRead-resRead (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mem ⊕ (h + (R(t, l, v), b) ') = mem ⊕ h; (s) Used formulas: gs.h.lastPersistedOrElse(ls.il, true)