Proof step 1 from proof step-absstep-R2-R4-tau-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ags.pm = gs.mem, ags.pm = ∅ ⊕ (ags.h | true), ls.t = als.t, lsf(t).t = t, alsf(t).t = t, ls.v = als.ov, ags.vm = gs.mem ⊕ gs.p, ags.vm = ∅ ⊕ ags.h, R4 = pcstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), alsf(t) = als, apc = resRead, apcf(t) = apc, gs0 = gstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), ls0 = lstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = R2, pcf0(t) = R4, PLIBLInv(ags, als, apc), abs(ags.h, gs.readers, gs.p), allReadsOK(ags.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, gs0.readers), notMember(t, gs.writers), oneMember(t, ls.l, gs.readers), pendingOk(gs0.p), pendingOk(gs.p), pre(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), writersOk(gs0.p, gs0.writers), writersOk(gs.p, gs.writers), gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = [], ∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | 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 ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resRead ∧ ls0.v = als.ov ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = [])

Rule argument

Additional information

Proof step 2 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.ctr(lsf(t).l) = 0, gs.mem = ∅ ⊕ (ags.h | true), ags.pm = gs.mem, lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).ov, ags.vm = gs.mem ⊕ gs.p, ags.vm = ∅ ⊕ ags.h, apcf(t) = resRead, ctr(lsf(t).l) = 0, lsf0(t) = lsf(t), pcf(t) = R2, pcf0(t) = R4, ((ags.h | lsf(t).l) | t) | false = [], PLIBLInv(ags, alsf(t), resRead), abs(ags.h, gs.readers, gs.p), allReadsOK(ags.h), allWritesOK(ags.h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers(lsf(t).l := gs.readers(lsf(t).l) -- t)), notMember(t, gs.writers), oneMember(t, lsf(t).l, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l0. ¬ FO(t) ∈ gs.p(l0) → ((ags.h | l0) | 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 ⊦ abs(ags.h, gs.readers(lsf(t).l := gs.readers(lsf(t).l) -- t), gs.p) ∧ (¬ FO(t) ∈ gs.p(l0) → ((ags.h | l0) | t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.readers:= writers0).p = gs.p; (s) ⊦ gstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ gs;gs.readers:= gs.readers(ls.l := gs.readers(ls.l) -- ls.t)); (s) ⊦ (gs.readers:= writers0).readers = writers0; (s) ⊦ (gs.readers:= writers0).mem = gs.mem; (s) ⊦ (gs.readers:= writers0).writers = gs.writers; (s) ⊦ (gs.readers:= writers0).ctr = gs.ctr; (s) ⊦ ctrReadPSC(t, l, n) = ctrReadPSC(t0, l0, n0) ↔ t = t0 ∧ l = l0 ∧ n = n0; (ws) ⊦ pre(gs, ls, R2, a) ↔ a = ctrReadPSC(ls.t, ls.l, gs.ctr(ls.l)); (s) ⊦ R3 ≠ R4; (s) ⊦ pcstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ R3;R4); (s) ⊦ lstepf(gs, ls, R2, a) = ls; (s)

Proof step 3 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs.ctr(lsf(t).l) = 0, gs.mem = ∅ ⊕ (h | true), alsf(t).t = t, lsf(t).t = t, lsf(t).v = alsf(t).ov, ags = mkPLIBgs(mem, mem0, h), apcf(t) = resRead, ctr(lsf(t).l) = 0, lsf0(t) = lsf(t), mem = ∅ ⊕ h, mem = gs.mem ⊕ gs.p, mem0 = gs.mem, pcf(t) = R2, pcf0(t) = R4, ((h | lsf(t).l) | t) | false = [], PLIBLInv(ags, alsf(t), resRead), abs(h, gs.readers, gs.p), allReadsOK(h), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.writers), notMember(t, gs.readers(lsf(t).l := gs.readers(lsf(t).l) -- t)), oneMember(t, lsf(t).l, gs.readers), 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)), ∀ l0. ¬ FO(t) ∈ gs.p(l0) → ((h | l0) | t) | false = [] ⊦ abs(h, gs.readers(lsf(t).l := gs.readers(lsf(t).l) -- t), gs.p) ∧ (¬ FO(t) ∈ gs.p(l0) → ((h | l0) | 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, mem, mem0, h

Proof step 4 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.ctr(lsf(t).l) = 0, gs.mem = ∅ ⊕ (h | true), lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).ov, apcf(t) = resRead, ctr(lsf(t).l) = 0, lsf0(t) = lsf(t), pcf(t) = R2, pcf0(t) = R4, ((h | lsf(t).l) | t) | false = [], gs.mem ⊕ gs.p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), resRead), abs(h, gs.readers, gs.p), allReadsOK(h), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers(lsf(t).l := gs.readers(lsf(t).l) -- t)), notMember(t, gs.writers), oneMember(t, lsf(t).l, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l0. ¬ FO(t) ∈ gs.p(l0) → ((h | l0) | t) | false = [], ∀ 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)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0 ⊦ abs(h, gs.readers(lsf(t).l := gs.readers(lsf(t).l) -- t), gs.p) ∧ (¬ FO(t) ∈ gs.p(l0) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 5 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  alsf(t).t = t, lsf(t).t = t, lsf(t).v = alsf(t).ov, apcf(t) = resRead, ctr(lsf(t).l) = 0, ctr0(lsf(t).l) = 0, gs = mkFLITPSCgs(mem, p, ctr0, writers, writers0), lsf0(t) = lsf(t), mem = ∅ ⊕ (h | true), pcf(t) = R2, pcf0(t) = R4, ((h | lsf(t).l) | t) | false = [], mem ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0(lsf(t).l := writers0(lsf(t).l) -- t)), oneMember(t, lsf(t).l, writers0), pendingOk(p), writersOk(p, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, mem, h), alsf(t0), apcf(t0)), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [] ⊦ abs(h, writers0(lsf(t).l := writers0(lsf(t).l) -- t), p) ∧ (¬ FO(t) ∈ p(l0) → ((h | l0) | 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, mem, ctr0, writers, writers0, p

Proof step 6 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).ov, apcf(t) = resRead, ctr(lsf(t).l) = 0, ctr0(lsf(t).l) = 0, lsf0(t) = lsf(t), pcf(t) = R2, pcf0(t) = R4, ((h | lsf(t).l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers0(lsf(t).l := writers0(lsf(t).l) -- t)), notMember(t, writers), oneMember(t, lsf(t).l, writers0), pendingOk(p), writersOk(p, writers), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, 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 ⊦ abs(h, writers0(lsf(t).l := writers0(lsf(t).l) -- t), p) ∧ (¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 7 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  lsf(t).t = t, lsf(t).v = ov, alsf(t) = mkPLIBls(t1, il, iv, ov), apcf(t) = resRead, ctr(lsf(t).l) = 0, ctr0(lsf(t).l) = 0, lsf0(t) = lsf(t), pcf(t) = R2, pcf0(t) = R4, t1 = t, ((h | lsf(t).l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0(lsf(t).l := writers0(lsf(t).l) -- t)), oneMember(t, lsf(t).l, writers0), pendingOk(p), writersOk(p, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [] ⊦ abs(h, writers0(lsf(t).l := writers0(lsf(t).l) -- t), p) ∧ (¬ FO(t) ∈ p(l0) → ((h | l0) | 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-R2-R4-tau-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, il, iv, lsf(t).v), apcf(t) = resRead, ctr(lsf(t).l) = 0, ctr0(lsf(t).l) = 0, lsf0(t) = lsf(t), pcf(t) = R2, pcf0(t) = R4, ((h | lsf(t).l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, lsf(t).v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers0(lsf(t).l := writers0(lsf(t).l) -- t)), notMember(t, writers), oneMember(t, lsf(t).l, writers0), pendingOk(p), writersOk(p, writers), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, 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 ⊦ abs(h, writers0(lsf(t).l := writers0(lsf(t).l) -- t), p) ∧ (¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 9 from proof step-absstep-R2-R4-tau-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, il, iv, v), apcf(t) = resRead, ctr(l) = 0, ctr0(l) = 0, lsf(t) = mkFLITPSCls(t1, l, v), lsf0(t) = lsf(t), pcf(t) = R2, pcf0(t) = R4, t1 = t, ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0(l := writers0(l) -- t)), oneMember(t, l, writers0), pendingOk(p), writersOk(p, writers), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [] ⊦ abs(h, writers0(l := writers0(l) -- t), p) ∧ (¬ FO(t) ∈ p(l0) → ((h | l0) | 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, l, v

Proof step 10 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  alsf(t) = mkPLIBls(t, il, iv, v), apcf(t) = resRead, ctr(l) = 0, ctr0(l) = 0, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = R2, pcf0(t) = R4, ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers0(l := writers0(l) -- t)), notMember(t, writers), oneMember(t, l, writers0), pendingOk(p), writersOk(p, writers), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, 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 ⊦ abs(h, writers0(l := writers0(l) -- t), p) ∧ (¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 11 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  alsf(t) = mkPLIBls(t, il, iv, v), apcf(t) = resRead, ctr(l) = 0, ctr0(l) = 0, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = R2, pcf0(t) = R4, ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0(l := writers0(l) -- t)), oneMember(t, l, writers0), pendingOk(p), writersOk(p, writers), ¬ abs(h, writers0(l := writers0(l) -- t), p), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [] ⊦

• Proof step 17:

  alsf(t) = mkPLIBls(t, il, iv, v), apcf(t) = resRead, ctr(l) = 0, ctr0(l) = 0, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = R2, pcf0(t) = R4, ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | l0) | t) | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0(l := writers0(l) -- t)), oneMember(t, l, writers0), pendingOk(p), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 12 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ t ∈ rs(l) ∧ (h | l) | false = [] → (abs(h, rs(l := rs(l) -- t), p) ↔ abs(h, rs, p))

• Proof step 14:

  alsf(t) = mkPLIBls(t, il, iv, v), apcf(t) = resRead, ctr(l) = 0, ctr0(l) = 0, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = R2, pcf0(t) = R4, ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers0(l := writers0(l) -- t)), notMember(t, writers), oneMember(t, l, writers0), pendingOk(p), writersOk(p, writers), ¬ abs(h, writers0(l := writers0(l) -- t), p), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, 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 ⊦ t ∈ writers0(l) ∧ (h | l) | false = []

Rule argument

Additional information

Used terms: l, t, writers0, p, h

Proof step 13 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  alsf(t) = mkPLIBls(t, il, iv, v), apcf(t) = resRead, ctr(l) = 0, ctr0(l) = 0, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = R2, pcf0(t) = R4, ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, (h | l) | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il, iv, v), resRead), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr0, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0(l := writers0(l) -- t)), oneMember(t, l, writers0), pendingOk(p), writersOk(p, writers), ¬ abs(h, writers0(l := writers0(l) -- t), p), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr0, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ l0. ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ oneMember(t, l, tsf) → (t ∈ tsf(l0) ↔ l = l0); (s)

Proof step 15 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ 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) Used terms: p, writers0, h, l

Proof step 16 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof step-absstep-R2-R4-tau-same (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0