Proof step 1 from proof step-absstep-W4-W5-tau-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, ags.pm = ∅ ⊕ (ags.h | true), ls.t = als.t, lsf(t).t = t, alsf(t).t = t, ls.v = als.iv, ags.vm = gs.mem ⊕ gs.p, ags.vm = ∅ ⊕ ags.h, W5 = pcstepf(gs, ls, W4, pwbPSC(t, l)), alsf(t) = als, apc = resWrite, apcf(t) = apc, gs0 = gstepf(gs, ls, W4, pwbPSC(t, l)), ls0 = lstepf(gs, ls, W4, pwbPSC(t, l)), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = W4, pcf0(t) = W5, FOFollowsW(t, gs0.p(ls0.l)), 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), notMember(t, gs0.readers), notMember(t, gs.readers), oneMember(t, ls0.l, gs0.writers), oneMember(t, ls.l, gs.writers), onePendingW(t, ls0.l, gs0.p), onePendingW(t, ls.l, gs.p), pendingOk(gs0.p), pendingOk(gs.p), pre(gs, ls, W4, pwbPSC(t, l)), writersOk(gs0.p, gs0.writers), writersOk(gs.p, gs.writers), ∀ 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.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = [] ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = resWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = [])

Rule argument

Additional information

Proof step 2 from proof step-absstep-W4-W5-tau-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), ags.pm = gs.mem, lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).iv, ags.vm = gs.mem ⊕ gs.p, ags.vm = ∅ ⊕ ags.h, apcf(t) = resWrite, lsf0(t) = lsf(t), pcf(t) = W4, pcf0(t) = W5, FOFollowsW(t, gs.p(alsf(t).il) + FO(t) '), PLIBLInv(ags, alsf(t), resWrite), abs(ags.h, gs.readers, gs.p), allReadsOK(ags.h), allWritesOK(ags.h), ctrok(gs.ctr, gs.writers), notMember(t, gs.readers), oneMember(t, alsf(t).il, gs.writers), onePendingW(t, alsf(t).il, gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')), onePendingW(t, alsf(t).il, gs.p), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')), pendingOk(gs.p), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) '), gs.writers), writersOk(gs.p, gs.writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(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)), ((ags.h | alsf(t).il) | t) | false = (W(t, alsf(t).il, alsf(t).iv), false) ' ∨ ((ags.h | alsf(t).il) | t) | false = [] ⊦ abs(ags.h, gs.readers, gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')) ∧ (¬ FO(t) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + FO(t) ';gs.p(l0)) → ((ags.h | l0) | t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.p:= p).p = p; (s) ⊦ x + a = x + a '; (s) ⊦ gstepf(gs, ls, W4, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + FO(ls.t)); (s) ⊦ (gs.p:= p).readers = gs.readers; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mem ⊕ p(l := p(l) + FO(t) ') = mem ⊕ p; (s) ⊦ (gs.p:= p).mem = gs.mem; (s) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ pwbPSC(t, l) = pwbPSC(t0, l0) ↔ t = t0 ∧ l = l0; (ws) ⊦ pre(gs, ls, W4, a) ↔ a = pwbPSC(ls.t, ls.l); (s) ⊦ pcstepf(gs, ls, W4, a) = W5; (s) ⊦ lstepf(gs, ls, W4, a) = ls; (s)

Proof step 3 from proof step-absstep-W4-W5-tau-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), alsf(t).t = t, lsf(t).t = t, lsf(t).v = alsf(t).iv, ags = mkPLIBgs(mem, mem0, h), apcf(t) = resWrite, lsf0(t) = lsf(t), mem = ∅ ⊕ h, mem = gs.mem ⊕ gs.p, mem0 = gs.mem, pcf(t) = W4, pcf0(t) = W5, FOFollowsW(t, gs.p(alsf(t).il) + FO(t) '), PLIBLInv(ags, alsf(t), resWrite), abs(h, gs.readers, gs.p), allReadsOK(h), allWritesOK(h), ctrok(gs.ctr, gs.writers), notMember(t, gs.readers), oneMember(t, alsf(t).il, gs.writers), onePendingW(t, alsf(t).il, gs.p), onePendingW(t, alsf(t).il, gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')), pendingOk(gs.p), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')), writersOk(gs.p, gs.writers), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) '), gs.writers), ∀ 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. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | alsf(t).il) | t) | false = (W(t, alsf(t).il, alsf(t).iv), false) ' ∨ ((h | alsf(t).il) | t) | false = [] ⊦ abs(h, gs.readers, gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')) ∧ (¬ FO(t) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + 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-W4-W5-tau-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), lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).iv, apcf(t) = resWrite, lsf0(t) = lsf(t), pcf(t) = W4, pcf0(t) = W5, gs.mem ⊕ gs.p = ∅ ⊕ h, FOFollowsW(t, gs.p(alsf(t).il) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), resWrite), abs(h, gs.readers, gs.p), allReadsOK(h), allWritesOK(h), ctrok(gs.ctr, gs.writers), notMember(t, gs.readers), oneMember(t, alsf(t).il, gs.writers), onePendingW(t, alsf(t).il, gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')), onePendingW(t, alsf(t).il, gs.p), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')), pendingOk(gs.p), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) '), gs.writers), writersOk(gs.p, gs.writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(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)), ((h | alsf(t).il) | t) | false = (W(t, alsf(t).il, alsf(t).iv), false) ' ∨ ((h | alsf(t).il) | t) | false = [] ⊦ abs(h, gs.readers, gs.p(alsf(t).il := gs.p(alsf(t).il) + FO(t) ')) ∧ (¬ FO(t) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + FO(t) ';gs.p(l0)) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 5 from proof step-absstep-W4-W5-tau-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, alsf(t).t = t, lsf(t).t = t, lsf(t).v = alsf(t).iv, apcf(t) = resWrite, gs = mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf0(t) = lsf(t), mem = ∅ ⊕ (h | true), pcf(t) = W4, pcf0(t) = W5, mem ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(alsf(t).il) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, alsf(t).il, writers), onePendingW(t, alsf(t).il, p), onePendingW(t, alsf(t).il, p(alsf(t).il := p(alsf(t).il) + FO(t) ')), pendingOk(p), pendingOk(p(alsf(t).il := p(alsf(t).il) + FO(t) ')), writersOk(p, writers), writersOk(p(alsf(t).il := p(alsf(t).il) + FO(t) '), writers), ∀ 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)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | alsf(t).il) | t) | false = (W(t, alsf(t).il, alsf(t).iv), false) ' ∨ ((h | alsf(t).il) | t) | false = [] ⊦ abs(h, writers0, p(alsf(t).il := p(alsf(t).il) + FO(t) ')) ∧ (¬ FO(t) ∈ (alsf(t).il = l0 ⊃ p(alsf(t).il) + 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, ctr, writers, writers0, p

Proof step 6 from proof step-absstep-W4-W5-tau-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, lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).iv, apcf(t) = resWrite, lsf0(t) = lsf(t), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(alsf(t).il) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, alsf(t).il, writers), onePendingW(t, alsf(t).il, p(alsf(t).il := p(alsf(t).il) + FO(t) ')), onePendingW(t, alsf(t).il, p), pendingOk(p(alsf(t).il := p(alsf(t).il) + FO(t) ')), pendingOk(p), writersOk(p(alsf(t).il := p(alsf(t).il) + FO(t) '), writers), writersOk(p, writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | alsf(t).il) | t) | false = (W(t, alsf(t).il, alsf(t).iv), false) ' ∨ ((h | alsf(t).il) | t) | false = [] ⊦ abs(h, writers0, p(alsf(t).il := p(alsf(t).il) + FO(t) ')) ∧ (¬ FO(t) ∈ (alsf(t).il = l0 ⊃ p(alsf(t).il) + FO(t) ';p(l0)) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 7 from proof step-absstep-W4-W5-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).l = il, lsf(t).t = t, lsf(t).v = iv, alsf(t) = mkPLIBls(t1, il, iv, ov), apcf(t) = resWrite, lsf0(t) = lsf(t), pcf(t) = W4, pcf0(t) = W5, t1 = t, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(il) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, il, writers), onePendingW(t, il, p), onePendingW(t, il, p(il := p(il) + FO(t) ')), pendingOk(p), pendingOk(p(il := p(il) + FO(t) ')), writersOk(p, writers), writersOk(p(il := p(il) + FO(t) '), writers), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | il) | t) | false = (W(t, il, iv), false) ' ∨ ((h | il) | t) | false = [] ⊦ abs(h, writers0, p(il := p(il) + FO(t) ')) ∧ (¬ FO(t) ∈ (il = l0 ⊃ p(il) + 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-W4-W5-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, lsf(t).l, lsf(t).v, ov), apcf(t) = resWrite, lsf0(t) = lsf(t), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(lsf(t).l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, lsf(t).l, lsf(t).v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, lsf(t).l, writers), onePendingW(t, lsf(t).l, p(lsf(t).l := p(lsf(t).l) + FO(t) ')), onePendingW(t, lsf(t).l, p), pendingOk(p(lsf(t).l := p(lsf(t).l) + FO(t) ')), pendingOk(p), writersOk(p(lsf(t).l := p(lsf(t).l) + FO(t) '), writers), writersOk(p, writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | lsf(t).l) | t) | false = (W(t, lsf(t).l, lsf(t).v), false) ' ∨ ((h | lsf(t).l) | t) | false = [] ⊦ abs(h, writers0, p(lsf(t).l := p(lsf(t).l) + FO(t) ')) ∧ (¬ FO(t) ∈ (lsf(t).l = l0 ⊃ p(lsf(t).l) + FO(t) ';p(l0)) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 9 from proof step-absstep-W4-W5-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, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t1, l, v), lsf0(t) = lsf(t), pcf(t) = W4, pcf0(t) = W5, t1 = t, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦ abs(h, writers0, p(l := p(l) + FO(t) ')) ∧ (¬ FO(t) ∈ (l = l0 ⊃ p(l) + 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-W4-W5-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, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦ abs(h, writers0, p(l := p(l) + FO(t) ')) ∧ (¬ FO(t) ∈ (l = l0 ⊃ p(l0) + FO(t) ';p(l0)) → ((h | l0) | t) | false = [])

Rule argument

Additional information

Proof step 11 from proof step-absstep-W4-W5-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, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ abs(h, writers0, p(l := p(l) + FO(t) ')), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

• Proof step 20:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ (l = l0 ⊃ p(l0) + FO(t) ';p(l0)), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 12 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ((h | t) | false)|R = [] → (abs(h, rs, p(l := p(l) + FO(t) ')) ↔ abs(h, rs, p))

• Proof step 14:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | t) | false)|R ≠ [], FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ abs(h, writers0, p(l := p(l) + FO(t) ')), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

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

Proof step 13 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ PLIBLInv(gs, ls, pc) ↔ pc = resWrite → (gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) '

• Proof step 16:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | t) | false)|R ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ abs(h, writers0, p(l := p(l) + FO(t) ')), resWrite = resWrite → (mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h).h | mkPLIBls(t, l, v, ov).t) | false = [] ∨ (mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h).h | mkPLIBls(t, l, v, ov).t) | false = (W(mkPLIBls(t, l, v, ov).t, mkPLIBls(t, l, v, ov).il, mkPLIBls(t, l, v, ov).iv), false) ', ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Used terms: mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite

Proof step 15 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | t) | false)|R ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ abs(h, writers0, p(l := p(l) + FO(t) ')), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [], (h | t) | false = [] ∨ (h | t) | false = (W(t, l, v), false) ' ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBls(t, il, iv, iv0).iv = iv; (s) ⊦ mkPLIBls(t, il, iv, iv0).il = il; (s) ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s)

Proof step 17 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | t) | false)|R ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ abs(h, writers0, p(l := p(l) + FO(t) ')), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] |R = []; (s)

Proof step 18 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | t) | false)|R ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ abs(h, writers0, p(l := p(l) + FO(t) ')), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (h | t) | false ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 19 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ vpe ' |R = (vpe._1.W? ⊃ [];vpe '); (s) ⊦ W(t, l, v).W?; (s)

Proof step 20 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 21:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ (l = l0 ⊃ p(l0) + FO(t) ';p(l0)), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: l = l0

Proof step 21 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ p(l0), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 22 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ PLIBLInv(gs, ls, pc) ↔ pc = resWrite → (gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) '

• Proof step 24:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ p(l0), resWrite = resWrite → (mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h).h | mkPLIBls(t, l, v, ov).t) | false = [] ∨ (mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h).h | mkPLIBls(t, l, v, ov).t) | false = (W(mkPLIBls(t, l, v, ov).t, mkPLIBls(t, l, v, ov).il, mkPLIBls(t, l, v, ov).iv), false) ', ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Used terms: mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l, v, ov), resWrite

Proof step 23 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ p(l0), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [], (h | t) | false = [] ∨ (h | t) | false = (W(t, l, v), false) ' ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBls(t, il, iv, iv0).iv = iv; (s) ⊦ mkPLIBls(t, il, iv, iv0).il = il; (s) ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s)

Proof step 25 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

• Proof step 35:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (W(t, l, v), false) ' ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 26 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 27:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = [], ((h | l) | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ p(l0), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 31:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = [], ((h | l) | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ p(l0), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

Rule argument

Additional information

Proof step 27 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ (h | l) | t = (h | t) | l

• Proof step 29:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, ((h | t) | l) | false = (W(t, l, v), false) ', (h | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ⊦

Rule argument

Additional information

Used terms: h, l, t

Proof step 28 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ (h | l) | b = (h | b) | l

Rule argument

Additional information

Used simplifier rules: ⊦ [] | l = []; (s) ⊦ a ' ≠ []; (s) Used terms: h | t, l, false

Proof step 30 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ (h | l) | t = (h | t) | l

• Proof step 33:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, ((h | l) | t) | false = [], (h | t) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | t) | l0) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ⊦

Rule argument

Additional information

Used terms: h, l0, t

Proof step 32 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ (h | l) | b = (h | b) | l

Rule argument

Additional information

Used simplifier rules: ⊦ [] | l = []; (s) Used terms: h | t, l0, false

Proof step 34 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | l0) | t) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ p(l0), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (h | t) | false ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Proof step 36 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ (h | l) | t = (h | t) | l

• Proof step 38:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | t) | l0) | false ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p(l := p(l) + FO(t) ')), onePendingW(t, l, p), pendingOk(p(l := p(l) + FO(t) ')), pendingOk(p), writersOk(p(l := p(l) + FO(t) '), writers), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ((h | l) | t) | false = (h | t) | false ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Used terms: h, l0, t

Proof step 37 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ (h | l) | b = (h | b) | l

• Proof step 40:

  alsf(t) = mkPLIBls(t, l, v, ov), apcf(t) = resWrite, lsf(t) = mkFLITPSCls(t, l, v), lsf0(t) = mkFLITPSCls(t, l, v), pcf(t) = W4, pcf0(t) = W5, (h | t) | false = (W(t, l, v), false) ', (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l ≠ l0, ((h | t) | false) | l0 ≠ [], FOFollowsW(t, p(l) + FO(t) '), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), notMember(t, writers0), oneMember(t, l, writers), onePendingW(t, l, p), onePendingW(t, l, p(l := p(l) + FO(t) ')), pendingOk(p), pendingOk(p(l := p(l) + FO(t) ')), writersOk(p, writers), writersOk(p(l := p(l) + FO(t) '), writers), ¬ FO(t) ∈ p(l0), ∀ t0. t0 ≠ t → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0, ((h | l) | t) | false = (h | t) | false ∨ ((h | l) | t) | false = [] ⊦

Rule argument

Additional information

Used terms: h | t, l0, false

Proof step 39 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof step-absstep-W4-W5-tau-same (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ W(t, l, v).l = l; (s)