Proof step 1 from proof step-absstep-R1-R2-doReadPSC-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ls.l = als.il, ags.pm = gs.mem, ags0.pm = ∅ ⊕ (ags0.h | true), ags.pm = ∅ ⊕ (ags.h | true), ls.t = als.t, lsf(t).t = t, alsf(t).t = t, ags.vm = gs.mem ⊕ gs.p, ags0.vm = ∅ ⊕ ags0.h, ags.vm = ∅ ⊕ ags.h, R2 = pcstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))), alsf(t) = als, apc = invRead, apcf(t) = apc, gs0 = gstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))), ls0 = lstepf(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = R1, pcf0(t) = R2, PLIBLInv(ags, als, apc), abs(ags.h, gs.readers, gs.p), allReadsOK(ags0.h), allReadsOK(ags.h), allWritesOK(ags0.h), allWritesOK(ags.h), ctrok(gs0.ctr, gs0.writers), ctrok(gs.ctr, gs.writers), noPendingW(t, gs0.p), noPendingW(t, gs.p), notMember(t, gs0.writers), notMember(t, gs.writers), notMember(t, gs.readers), oneMember(t, ls0.l, gs0.readers), pendingOk(gs0.p), pendingOk(gs.p), pre(gs, ls, R1, doReadPSC(ls.t, l, ((mem ⊕ p))(l))), writersOk(gs0.p, gs0.writers), writersOk(gs.p, gs.writers), pre(ags, als, apc, ADoRead(ls.t)) → ags0 = gstepf(ags, als, apc, ADoRead(ls.t)) ∧ als0 = lstepf(ags, als, apc, ADoRead(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ADoRead(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. t0 ≠ t → alsf(t0).t = t0, ∀ t0. t0 ≠ t → lsf(t0).t = t0 ⊦ pre(ags, als, apc, ADoRead(ls.t)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = resRead ∧ ls0.v = als0.ov ∧ (∀ l0. l0 ≠ ls0.l ∧ ¬ FO(ls0.t) ∈ gs0.p(l0) → ((ags0.h | l0) | ls0.t) | false = []) ∧ (gs0.ctr(ls0.l) = 0 → ((ags0.h | ls0.l) | ls0.t) | false = [])

Rule argument

Additional information

Proof step 2 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  lsf(t).l = alsf(t).il, gs.mem = ∅ ⊕ (ags.h | true), gs.mem = ∅ ⊕ ((ags.h | true) + (ags.h.lastPersistedOrElse(alsf(t).il, true) ⊃ (R(t, alsf(t).il, ags.vm(alsf(t).il)), true) ';[])), ags.pm = gs.mem, alsf(t).t = t, lsf(t).t = t, ags.vm = ∅ ⊕ ags.h, ags.vm = gs.mem ⊕ gs.p, apcf(t) = invRead, lsf0(t) = lsf(t).v:= (gs.mem(alsf(t).il) ⊕ gs.p(alsf(t).il)), pcf(t) = R1, pcf0(t) = R2, mem(alsf(t).il) ⊕ p(alsf(t).il) = gs.mem(alsf(t).il) ⊕ gs.p(alsf(t).il), PLIBLInv(ags, alsf(t), invRead), abs(ags.h, gs.readers, gs.p), allReadsOK(ags.h), allReadsOK(ags.h + (R(t, alsf(t).il, ags.vm(alsf(t).il)), ags.h.lastPersistedOrElse(alsf(t).il, true)) '), allWritesOK(ags.h), allWritesOK(ags.h + (R(t, alsf(t).il, ags.vm(alsf(t).il)), ags.h.lastPersistedOrElse(alsf(t).il, true)) '), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers), notMember(t, gs.writers), oneMember(t, lsf0(t).l, gs.readers(alsf(t).il := gs.readers(alsf(t).il) ++ t)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ gs.p(l) → ((ags.h | l) | t) | false = [] ⊦ lsf0(t).t = t ∧ lsf0(t).v = ags.vm(alsf(t).il) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = l0 ⊃ (R(t, alsf(t).il, ags.vm(alsf(t).il)), ags.h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( gs.ctr(lsf0(t).l) = 0 → ((ags.h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = lsf0(t).l ⊃ (R(t, alsf(t).il, ags.vm(alsf(t).il)), ags.h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ h + h0 | t = (h | t) + (h0 | t); (s) ⊦ R(t, l, v).l = l; (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ (gs.h:= h).h = h; (s) ⊦ (ls.ov:= iv0).ov = iv0; (s) ⊦ (ls.ov:= iv0).t = ls.t; (s) ⊦ abs(h, rs, p) → abs(h + (R(t, l, v), b) ', rs(l := rs(l) ++ t), p); (ss) ⊦ (gs.h:= h).vm = gs.vm; (s) ⊦ (gs.h:= h).pm = gs.pm; (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ mem ⊕ (h + (R(t, l, v), b) ') = mem ⊕ h; (s) ⊦ ADoRead(t) = ADoRead(t0) ↔ t = t0; (s) ⊦ pre(gs, ls, invRead, a) ↔ a = ADoRead(ls.t); (s) ⊦ ls.t = t → pcstepf(gs, ls, invRead, ADoRead(t)) = resRead; (s) ⊦ ls.t = t → lstepf(gs, ls, invRead, ADoRead(t)) = ls.ov:= gs.vm(ls.il); (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.readers:= writers0).ctr = gs.ctr; (s) ⊦ gstepf(gs, ls, R1, a) = gs.readers:= gs.readers(ls.l := gs.readers(ls.l) ++ ls.t); (s) ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s) ⊦ (gs.readers:= writers0).p = gs.p; (s) ⊦ (gs.readers:= writers0).readers = writers0; (s) ⊦ (gs.readers:= writers0).mem = gs.mem; (s) ⊦ (gs.readers:= writers0).writers = gs.writers; (s) ⊦ doReadPSC(t, l, v) = doReadPSC(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0; (ws) ⊦ pre(gs, ls, R1, a) ↔ a = doReadPSC(ls.t, ls.l, ((gs.mem ⊕ gs.p))(ls.l)); (s) ⊦ pcstepf(gs, ls, R1, a) = R2; (s) ⊦ lstepf(gs, ls, R1, a) = ls.v:= ((gs.mem ⊕ gs.p))(ls.l); (s)

Proof step 3 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  lsf(t).l = alsf(t).il, gs.mem = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(alsf(t).il, true) ⊃ (R(t, alsf(t).il, mem0(alsf(t).il)), true) ';[])), gs.mem = ∅ ⊕ (h | true), lsf(t).t = t, alsf(t).t = t, ags = mkPLIBgs(mem0, mem1, h), apcf(t) = invRead, lsf0(t) = lsf(t).v:= (gs.mem(alsf(t).il) ⊕ gs.p(alsf(t).il)), mem0 = gs.mem ⊕ gs.p, mem0 = ∅ ⊕ h, mem1 = gs.mem, pcf(t) = R1, pcf0(t) = R2, mem(alsf(t).il) ⊕ p(alsf(t).il) = gs.mem(alsf(t).il) ⊕ gs.p(alsf(t).il), PLIBLInv(ags, alsf(t), invRead), abs(h, gs.readers, gs.p), allReadsOK(h + (R(t, alsf(t).il, mem0(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), allReadsOK(h), allWritesOK(h + (R(t, alsf(t).il, mem0(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.writers), notMember(t, gs.readers), oneMember(t, lsf0(t).l, gs.readers(alsf(t).il := gs.readers(alsf(t).il) ++ t)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l. ¬ FO(t) ∈ gs.p(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ lsf0(t).t = t ∧ lsf0(t).v = mem0(alsf(t).il) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ gs.p(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = l0 ⊃ (R(t, alsf(t).il, mem0(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( gs.ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = lsf0(t).l ⊃ (R(t, alsf(t).il, mem0(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ (vm = gs.vm ∧ pm = gs.pm) ∧ h = gs.h ↔ gs = mkPLIBgs(vm, pm, h); (elim) Used terms: ags, mem0, mem1, h

Proof step 4 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  lsf(t).l = alsf(t).il, gs.mem = ∅ ⊕ (h | true), gs.mem = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(alsf(t).il, true) ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), true) ';[])), alsf(t).t = t, lsf(t).t = t, apcf(t) = invRead, lsf0(t) = lsf(t).v:= (gs.mem(alsf(t).il) ⊕ gs.p(alsf(t).il)), pcf(t) = R1, pcf0(t) = R2, mem(alsf(t).il) ⊕ p(alsf(t).il) = gs.mem(alsf(t).il) ⊕ gs.p(alsf(t).il), ∅ ⊕ h = gs.mem ⊕ gs.p, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), invRead), abs(h, gs.readers, gs.p), allReadsOK(h), allReadsOK(h + (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), allWritesOK(h), allWritesOK(h + (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers), notMember(t, gs.writers), oneMember(t, lsf0(t).l, gs.readers(alsf(t).il := gs.readers(alsf(t).il) ++ t)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ gs.p(l) → ((h | l) | t) | false = [] ⊦ lsf0(t).t = t ∧ lsf0(t).v = ((∅ ⊕ h))(alsf(t).il) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ gs.p(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = l0 ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( gs.ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = lsf0(t).l ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 5 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  lsf(t).l = alsf(t).il, lsf(t).t = t, alsf(t).t = t, apcf(t) = invRead, gs = mkFLITPSCgs(mem0, p0, ctr, writers, writers0), lsf0(t) = lsf(t).v:= (mem0(alsf(t).il) ⊕ p0(alsf(t).il)), mem0 = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(alsf(t).il, true) ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), true) ';[])), mem0 = ∅ ⊕ (h | true), pcf(t) = R1, pcf0(t) = R2, ∅ ⊕ h = mem0 ⊕ p0, mem(alsf(t).il) ⊕ p(alsf(t).il) = mem0(alsf(t).il) ⊕ p0(alsf(t).il), PLIBLInv(mkPLIBgs(∅ ⊕ h, mem0, h), alsf(t), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), allReadsOK(h), allWritesOK(h + (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, lsf0(t).l, writers0(alsf(t).il := writers0(alsf(t).il) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, mem0, h), alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, mem0, h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ lsf0(t).t = t ∧ lsf0(t).v = ((∅ ⊕ h))(alsf(t).il) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ p0(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = l0 ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = lsf0(t).l ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers); (elim) Used terms: gs, mem0, ctr, writers, writers0, p0

Proof step 6 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  lsf(t).l = alsf(t).il, alsf(t).t = t, lsf(t).t = t, apcf(t) = invRead, lsf0(t) = lsf(t).v:= (((∅ ⊕ (h | true)))(alsf(t).il) ⊕ p0(alsf(t).il)), pcf(t) = R1, pcf0(t) = R2, mem(alsf(t).il) ⊕ p(alsf(t).il) = ((∅ ⊕ (h | true)))(alsf(t).il) ⊕ p0(alsf(t).il), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(alsf(t).il, true) ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), true) ';[])), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), allWritesOK(h), allWritesOK(h + (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, lsf0(t).l, writers0(alsf(t).il := writers0(alsf(t).il) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦ lsf0(t).t = t ∧ lsf0(t).v = ((∅ ⊕ h))(alsf(t).il) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ p0(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = l0 ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((alsf(t).il = lsf0(t).l ⊃ (R(t, alsf(t).il, ((∅ ⊕ h))(alsf(t).il)), h.lastPersistedOrElse(alsf(t).il, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 7 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  lsf(t).l = il, lsf(t).t = t, alsf(t) = mkPLIBls(t1, il, iv, ov), apcf(t) = invRead, lsf0(t) = lsf(t).v:= (((∅ ⊕ (h | true)))(il) ⊕ p0(il)), pcf(t) = R1, pcf0(t) = R2, t1 = t, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(il, true) ⊃ (R(t, il, ((∅ ⊕ h))(il)), true) ';[])), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(il) ⊕ p(il) = ((∅ ⊕ (h | true)))(il) ⊕ p0(il), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, il, ((∅ ⊕ h))(il)), h.lastPersistedOrElse(il, true)) '), allReadsOK(h), allWritesOK(h + (R(t, il, ((∅ ⊕ h))(il)), h.lastPersistedOrElse(il, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, lsf0(t).l, writers0(il := writers0(il) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ lsf0(t).t = t ∧ lsf0(t).v = ((∅ ⊕ h))(il) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ p0(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((il = l0 ⊃ (R(t, il, ((∅ ⊕ h))(il)), h.lastPersistedOrElse(il, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((il = lsf0(t).l ⊃ (R(t, il, ((∅ ⊕ h))(il)), h.lastPersistedOrElse(il, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ ((t = ls.t ∧ il = ls.il) ∧ iv = ls.iv) ∧ ov = ls.ov ↔ ls = mkPLIBls(t, il, iv, ov); (elim) Used terms: alsf(t), iv, t1, il, ov

Proof step 8 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  lsf(t).t = t, alsf(t) = mkPLIBls(t, lsf(t).l, iv, ov), apcf(t) = invRead, lsf0(t) = lsf(t).v:= (((∅ ⊕ (h | true)))(lsf(t).l) ⊕ p0(lsf(t).l)), pcf(t) = R1, pcf0(t) = R2, mem(lsf(t).l) ⊕ p(lsf(t).l) = ((∅ ⊕ (h | true)))(lsf(t).l) ⊕ p0(lsf(t).l), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(lsf(t).l, true) ⊃ (R(t, lsf(t).l, ((∅ ⊕ h))(lsf(t).l)), true) ';[])), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, lsf(t).l, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, lsf(t).l, ((∅ ⊕ h))(lsf(t).l)), h.lastPersistedOrElse(lsf(t).l, true)) '), allWritesOK(h), allWritesOK(h + (R(t, lsf(t).l, ((∅ ⊕ h))(lsf(t).l)), h.lastPersistedOrElse(lsf(t).l, true)) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, lsf0(t).l, writers0(lsf(t).l := writers0(lsf(t).l) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦ lsf0(t).t = t ∧ lsf0(t).v = ((∅ ⊕ h))(lsf(t).l) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ p0(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((lsf(t).l = l0 ⊃ (R(t, lsf(t).l, ((∅ ⊕ h))(lsf(t).l)), h.lastPersistedOrElse(lsf(t).l, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((lsf(t).l = lsf0(t).l ⊃ (R(t, lsf(t).l, ((∅ ⊕ h))(lsf(t).l)), h.lastPersistedOrElse(lsf(t).l, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 9 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, lsf(t) = mkFLITPSCls(t1, l1, v), lsf0(t) = lsf(t).v:= (((∅ ⊕ (h | true)))(l1) ⊕ p0(l1)), pcf(t) = R1, pcf0(t) = R2, t1 = t, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allReadsOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, lsf0(t).l, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ lsf0(t).t = t ∧ lsf0(t).v = ((∅ ⊕ h))(l1) ∧ ( l0 ≠ lsf0(t).l ∧ ¬ FO(lsf0(t).t) ∈ p0(l0) → ((h | l0) | lsf0(t).t) | false = [] ∧ ((l1 = l0 ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) ';[]) | lsf0(t).t) | false = []) ∧ ( ctr(lsf0(t).l) = 0 → ((h | lsf0(t).l) | lsf0(t).t) | false = [] ∧ ((l1 = lsf0(t).l ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) ';[]) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ (t = ls.t ∧ l = ls.l) ∧ v = ls.v ↔ ls = mkFLITPSCls(t, l, v); (elim) Used terms: lsf(t), t1, l1, v

Proof step 10 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦ mem(l1) ⊕ p(l1) = ((∅ ⊕ h))(l1) ∧ (l0 ≠ l1 ∧ ¬ FO(t) ∈ p0(l0) → ((h | l0) | t) | false = []) ∧ (ctr(l1) = 0 → ((h | l1) | t) | false = [] ∧ h.lastPersistedOrElse(l1, true))

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s) ⊦ R(t, l, v).t = t; (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ [] | b = []; (s) ⊦ [] | t = []; (s) ⊦ mkFLITPSCls(t, l, v).v = v; (s) ⊦ mkFLITPSCls(t, l, v).v:= v0 = mkFLITPSCls(t, l, v0); (s)

Proof step 11 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), mem(l1) ⊕ p(l1) ≠ ((∅ ⊕ h))(l1), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allReadsOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦

• Proof step 14:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), l0 ≠ l1, ((h | l0) | t) | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allReadsOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ¬ FO(t) ∈ p0(l0), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦

• Proof step 15:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, ctr(l1) = 0, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allReadsOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ ((h | l1) | t) | false = [] ∧ h.lastPersistedOrElse(l1, true)

Rule argument

Additional information

Proof step 12 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 13:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, (((∅ ⊕ (h | true)) ⊕ p0))(l1)), true) ';[])), mem(l1) ⊕ p(l1) ≠ (((∅ ⊕ (h | true)) ⊕ p0))(l1), PLIBLInv(mkPLIBgs((∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, l1, (((∅ ⊕ (h | true)) ⊕ p0))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), allWritesOK(h + (R(t, l1, (((∅ ⊕ (h | true)) ⊕ p0))(l1)), h.lastPersistedOrElse(l1, true)) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs((∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs (mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs((∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 13 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s)

Proof step 14 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 15 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ (h |W | l) | false = [] → (h.lastPersistedOrElse(l, true) ↔ true)

• Proof step 17:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, ctr(l1) = 0, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), (h |W | l1) | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦ ((h | l1) | t) | false = [] ∧ h.lastPersistedOrElse(l1, true)

• Proof step 23:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, ctr(l1) = 0, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, (h |W | l1) | false = [], mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (true ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), true) '), allWritesOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), true) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦ ((h | l1) | t) | false = [] ∧ true

Rule argument

Additional information

Used terms: h, l1

Proof step 16 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ h |W | l = (h | l)|W

• Proof step 19:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, ctr(l1) = 0, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), (h | l1)|W | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allReadsOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ ((h | l1) | t) | false = [] ∧ h.lastPersistedOrElse(l1, true)

Rule argument

Additional information

Used terms: h, l1

Proof step 18 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ h |W | b = (h | b)|W

• Proof step 21:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, ctr(l1) = 0, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, ∅ ⊕ (h | true) = ∅ ⊕ ((h | true) + (h.lastPersistedOrElse(l1, true) ⊃ (R(t, l1, ((∅ ⊕ h))(l1)), true) ';[])), ((h | l1) | false)|W ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), allWritesOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), h.lastPersistedOrElse(l1, true)) '), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers0), notMember(t, writers), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [] ⊦ ((h | l1) | t) | false = [] ∧ h.lastPersistedOrElse(l1, true)

Rule argument

Additional information

Used terms: h | l1, false

Proof step 20 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ p(l) |W = [] ∧ allReadsOK(h) ∧ abs(h, rs, p) → (h | l) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ ctr(l) = 0 ∧ ctrok(ctr, ws) ∧ writersOk(p, ws) → p(l) |W = []; (s) ⊦ [] |W = []; (s) Used terms: p0, writers0, h, l1

Proof step 22 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  alsf(t) = mkPLIBls(t, l1, iv, ov), apcf(t) = invRead, ctr(l1) = 0, lsf(t) = mkFLITPSCls(t, l1, v), lsf0(t) = mkFLITPSCls(t, l1, mem(l1) ⊕ p(l1)), pcf(t) = R1, pcf0(t) = R2, (h |W | l1) | false = [], ∅ ⊕ h = (∅ ⊕ (h | true)) ⊕ p0, mem(l1) ⊕ p(l1) = ((∅ ⊕ (h | true)))(l1) ⊕ p0(l1), ((h | l1) | t) | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l1, iv, ov), invRead), abs(h, writers0, p0), allReadsOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), true) '), allReadsOK(h), allWritesOK(h + (R(t, l1, ((∅ ⊕ h))(l1)), true) '), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p0), notMember(t, writers), notMember(t, writers0), oneMember(t, l1, writers0(l1 := writers0(l1) ++ t)), pendingOk(p0), writersOk(p0, writers), ∀ l. ¬ FO(t) ∈ p0(l) → ((h | l) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p0, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mem ⊕ (h + (R(t, l, v), b) ') = mem ⊕ h; (s)

Proof step 24 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ p(l) |W = [] ∧ allReadsOK(h) ∧ abs(h, rs, p) → ((h | l) | t) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ ctr(l) = 0 ∧ ctrok(ctr, ws) ∧ writersOk(p, ws) → p(l) |W = []; (s) Used terms: l1, t, writers0, p0, h

Proof step 25 from proof step-absstep-R1-R2-doReadPSC-same (previous step) (back to tree)

A spec-lemma