Proof step 1 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  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, W1 = pcstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)), alsf(t) = als, apc = ready, apcf(t) = apc, gs0 = gstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)), ls0 = lstepf(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = ready, pcf0(t) = W1, 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.readers), notMember(t, gs0.writers), notMember(t, gs.writers), notMember(t, gs.readers), pendingOk(gs0.p), pendingOk(gs.p), pre(gs, ls, ready, invFLITPSCWRITE(ls.t, l0, v0)), writersOk(gs0.p, gs0.writers), writersOk(gs.p, gs.writers), pre(ags, als, apc, AInvWrite(ls.t, l0, v0)) → ags0 = gstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ als0 = lstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)) ∧ apc0 = pcstepf(ags, als, apc, AInvWrite(ls.t, l0, v0)), ∀ 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, AInvWrite(ls.t, l0, v0)) ∧ (ags0.pm = gs0.mem ∧ ags0.vm = gs0.mem ⊕ gs0.p ∧ abs(ags0.h, gs0.readers, gs0.p)) ∧ ls0.t = als0.t ∧ apc0 = invWrite ∧ (ls0.l = als0.il ∧ ls0.v = als0.iv) ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags0.h | l) | ls0.t) | false = [])

Rule argument

Additional information

Proof step 2 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.mem = ∅ ⊕ (ags.h | true), ags.pm = gs.mem, ags0.pm = ∅ ⊕ (ags0.h | true), lsf(t).t = t, alsf(t).t = t, ags.vm = gs.mem ⊕ gs.p, ags0.vm = ∅ ⊕ ags0.h, ags.vm = ∅ ⊕ ags.h, apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, PLIBLInv(ags, alsf(t), ready), abs(ags.h, gs.readers, gs.p), allReadsOK(ags0.h), allReadsOK(ags.h), allWritesOK(ags0.h), allWritesOK(ags.h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.writers), notMember(t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → ags0 = ags ∧ als0 = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ gs.p(l) → ((ags.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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ags0.pm = gs.mem ∧ ags0.vm = ags.vm ∧ abs(ags0.h, gs.readers, gs.p) ∧ lsf0(t).t = als0.t ∧ apc0 = invWrite ∧ lsf0(t).l = als0.il ∧ lsf0(t).v = als0.iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((ags0.h | l1) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ AInvRead(t, l) ≠ AInvWrite(t0, l0, val); (s) ⊦ AInvWrite(t, l, val) ≠ callTSync(t0); (s) ⊦ pre(gs, ls, ready, a) ↔ a = callTSync(ls.t) ∧ (gs.h | ls.t) | false = [] ∨ (∃ l, v. a = AInvWrite(ls.t, l, v)) ∨ (∃ l. a = AInvRead(ls.t, l)); (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, AInvWrite(t, l, v)) = invWrite; (s) ⊦ ls.t = t → lstepf(gs, ls, ready, AInvWrite(t, l, v)) = (ls.il:= l).iv:= v; (s) ⊦ gstepf(gs, ls, ready, a) = gs; (s) ⊦ gstepf(gs, ls, ready, a) = gs; (s) ⊦ invFLITPSCWRITE(t, l, v) = invFLITPSCWRITE(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0; (ws) ⊦ callPSCCOMPLETE(t) ≠ invFLITPSCWRITE(t0, l, v); (s) ⊦ invFLITPSCREAD(t, l) ≠ invFLITPSCWRITE(t0, l0, v); (s) ⊦ pre(gs, ls, ready, a) ↔ (∃ l0, v0. a = invFLITPSCWRITE(ls.t, l0, v0)) ∨ (∃ l0. a = invFLITPSCREAD(ls.t, l0)) ∨ a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)); (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = W1; (s) ⊦ ls.t = t → lstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = (ls.l:= l0).v:= v0; (s)

Proof step 3 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs.mem = ∅ ⊕ (h | true), ags0.pm = ∅ ⊕ (ags0.h | true), alsf(t).t = t, lsf(t).t = t, ags0.vm = ∅ ⊕ ags0.h, ags = mkPLIBgs(mem, mem0, h), apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, mem = ∅ ⊕ h, mem = gs.mem ⊕ gs.p, mem0 = gs.mem, pcf(t) = ready, pcf0(t) = W1, PLIBLInv(ags, alsf(t), ready), abs(h, gs.readers, gs.p), allReadsOK(h), allReadsOK(ags0.h), allWritesOK(h), allWritesOK(ags0.h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers), notMember(t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → ags0 = ags ∧ als0 = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ 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) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ags0.pm = gs.mem ∧ ags0.vm = mem ∧ abs(ags0.h, gs.readers, gs.p) ∧ lsf0(t).t = als0.t ∧ apc0 = invWrite ∧ lsf0(t).l = als0.il ∧ lsf0(t).v = als0.iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((ags0.h | l1) | 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, mem, mem0, h

Proof step 4 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.mem = ∅ ⊕ (h | true), ags0.pm = ∅ ⊕ (ags0.h | true), lsf(t).t = t, alsf(t).t = t, ags0.vm = ∅ ⊕ ags0.h, apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, gs.mem ⊕ gs.p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), ready), abs(h, gs.readers, gs.p), allReadsOK(ags0.h), allReadsOK(h), allWritesOK(ags0.h), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.writers), notMember(t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → ags0 = mkPLIBgs(∅ ⊕ h, gs.mem, h) ∧ als0 = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ gs.p(l) → ((h | l) | 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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ags0.pm = gs.mem ∧ ags0.vm = ∅ ⊕ h ∧ abs(ags0.h, gs.readers, gs.p) ∧ lsf0(t).t = als0.t ∧ apc0 = invWrite ∧ lsf0(t).l = als0.il ∧ lsf0(t).v = als0.iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((ags0.h | l1) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 5 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  gs.mem = ∅ ⊕ (h | true), alsf(t).t = t, lsf(t).t = t, ags0 = mkPLIBgs(mem, mem0, h0), apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, mem = ∅ ⊕ h0, mem0 = ∅ ⊕ (h0 | true), pcf(t) = ready, pcf0(t) = W1, gs.mem ⊕ gs.p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), ready), abs(h, gs.readers, gs.p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers), notMember(t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → ags0 = mkPLIBgs(∅ ⊕ h, gs.mem, h) ∧ als0 = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ 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 = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ mem0 = gs.mem ∧ mem = ∅ ⊕ h ∧ abs(h0, gs.readers, gs.p) ∧ lsf0(t).t = als0.t ∧ apc0 = invWrite ∧ lsf0(t).l = als0.il ∧ lsf0(t).v = als0.iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((h0 | l1) | 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: ags0, mem, mem0, h0

Proof step 6 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gs.mem = ∅ ⊕ (h | true), lsf(t).t = t, alsf(t).t = t, apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, gs.mem ⊕ gs.p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), ready), abs(h, gs.readers, gs.p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.writers), notMember(t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, gs.mem, h) ∧ als0 = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ gs.p(l) → ((h | l) | 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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = gs.mem ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, gs.readers, gs.p) ∧ lsf0(t).t = als0.t ∧ apc0 = invWrite ∧ lsf0(t).l = als0.il ∧ lsf0(t).v = als0.iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((h0 | l1) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 7 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  gs.mem = ∅ ⊕ (h | true), alsf(t).t = t, lsf(t).t = t, als0 = mkPLIBls(t1, il, iv, ov), apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, gs.mem ⊕ gs.p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), ready), abs(h, gs.readers, gs.p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.readers), notMember(t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, gs.mem, h) ∧ als0 = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ 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 = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = gs.mem ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, gs.readers, gs.p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((h0 | l1) | 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: als0, iv, t1, il, ov

Proof step 8 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.mem = ∅ ⊕ (h | true), lsf(t).t = t, alsf(t).t = t, apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, gs.mem ⊕ gs.p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), ready), abs(h, gs.readers, gs.p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPendingW(t, gs.p), notMember(t, gs.writers), notMember(t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, gs.mem, h) ∧ mkPLIBls(t1, il, iv, ov) = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ gs.p(l) → ((h | l) | 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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = gs.mem ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, gs.readers, gs.p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ gs.p(l1) → ((h0 | l1) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 9 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  alsf(t).t = t, lsf(t).t = t, apcf(t) = ready, gs = mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf0(t) = (lsf(t).l:= l0).v:= v0, mem = ∅ ⊕ (h | true), pcf(t) = ready, pcf0(t) = W1, mem ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t), ready), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, mem, h) ∧ mkPLIBls(t1, il, iv, ov) = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = mem ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ p(l1) → ((h0 | l1) | 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, mem, ctr, writers, writers0, p

Proof step 10 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  lsf(t).t = t, alsf(t).t = t, apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), ready), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0), pendingOk(p), writersOk(p, writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h) ∧ mkPLIBls(t1, il, iv, ov) = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | 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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ p(l1) → ((h0 | l1) | lsf0(t).t) | false = [])

Rule argument

Additional information

Proof step 11 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  lsf(t).t = t, alsf(t) = mkPLIBls(t2, il0, iv0, ov0), apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, t2 = t, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), ready), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h) ∧ mkPLIBls(t1, il, iv, ov) = (alsf(t).il:= l0).iv:= v0 ∧ apc0 = invWrite, ∀ 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ p(l1) → ((h0 | l1) | 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), iv0, t2, il0, ov0

Proof step 12 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  lsf(t).t = t, alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h) ∧ mkPLIBls(t1, il, iv, ov) = mkPLIBls(t, l0, v0, ov0) ∧ apc0 = invWrite, ∀ 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ p(l1) → ((h0 | l1) | lsf0(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBls(t, il, iv, iv0).iv:= iv1 = mkPLIBls(t, il, iv1, iv0); (s) ⊦ mkPLIBls(t, il, iv, iv0).il:= il0 = mkPLIBls(t, il0, iv, iv0); (s)

Proof step 13 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t2, l2, v1), lsf0(t) = (lsf(t).l:= l0).v:= v0, pcf(t) = ready, pcf0(t) = W1, t2 = t, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0), pendingOk(p), writersOk(p, writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h) ∧ mkPLIBls(t1, il, iv, ov) = mkPLIBls(t, l0, v0, ov0) ∧ apc0 = invWrite, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | 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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ lsf0(t).t = t1 ∧ apc0 = invWrite ∧ lsf0(t).l = il ∧ lsf0(t).v = iv ∧ (¬ FO(lsf0(t).t) ∈ p(l1) → ((h0 | l1) | 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), t2, l2, v1

Proof step 14 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, writers), (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h) ∧ mkPLIBls(t1, il, iv, ov) = mkPLIBls(t, l0, v0, ov0) ∧ apc0 = invWrite, ∀ 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ (∃ l, v. AInvWrite(t1, il, iv) = AInvWrite(t1, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ t = t1 ∧ apc0 = invWrite ∧ l0 = il ∧ v0 = iv ∧ (¬ FO(t1) ∈ p(l1) → ((h0 | l1) | t1) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkFLITPSCls(t, l, v).v = v; (s) ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ mkFLITPSCls(t, l, v).v:= v0 = mkFLITPSCls(t, l, v0); (s) ⊦ mkFLITPSCls(t, l, v).l:= l0 = mkFLITPSCls(t, l0, v); (s)

Proof step 15 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0), pendingOk(p), writersOk(p, writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | 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)) ⊦ ∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v), (∃ l, v. AInvWrite(t1, il, iv) = AInvWrite(t1, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ t = t1 ∧ apc0 = invWrite ∧ l0 = il ∧ v0 = iv ∧ (¬ FO(t1) ∈ p(l1) → ((h0 | l1) | t1) | false = [])

• Proof step 18:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apc0 = invWrite, apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t1, il, iv, ov) = mkPLIBls(t, l0, v0, ov0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0), pendingOk(p), writersOk(p, writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | 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)) ⊦ (∃ l, v. AInvWrite(t1, il, iv) = AInvWrite(t1, l, v)) ∧ ∅ ⊕ (h0 | true) = ∅ ⊕ (h | true) ∧ ∅ ⊕ h0 = ∅ ⊕ h ∧ abs(h0, writers0, p) ∧ t = t1 ∧ apc0 = invWrite ∧ l0 = il ∧ v0 = iv ∧ (¬ FO(t1) ∈ p(l1) → ((h0 | l1) | t1) | false = [])

Rule argument

Additional information

Proof step 16 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ ∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)

Rule argument

Additional information

Proof step 17 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: l0, v0

Proof step 18 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, writers0), pendingOk(p), writersOk(p, writers), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | 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)) ⊦ (∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)) ∧ (¬ FO(t) ∈ p(l1) → ((h | l1) | t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBgs(vm, vm0, h) = mkPLIBgs(vm1, vm2, h0) ↔ vm = vm1 ∧ vm0 = vm2 ∧ h = h0; (ws) ⊦ mkPLIBls(t, il, iv, iv0) = mkPLIBls(t0, il0, iv1, iv2) ↔ t = t0 ∧ il = il0 ∧ iv = iv1 ∧ iv0 = iv2; (ws)

Proof step 19 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ ∃ l, v. AInvWrite(t, l0, v0) = AInvWrite(t, l, v)

• Proof step 21:

  alsf(t) = mkPLIBls(t, il0, iv0, ov0), apcf(t) = ready, lsf(t) = mkFLITPSCls(t, l2, v1), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = ready, pcf0(t) = W1, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, ((h | l1) | t) | false ≠ [], PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, il0, iv0, ov0), ready), abs(h, writers0, p), allReadsOK(h), allWritesOK(h), ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers0), notMember(t, writers), pendingOk(p), writersOk(p, writers), ¬ FO(t) ∈ p(l1), ∀ 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)), ∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = [], ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

Rule argument

Additional information

Proof step 20 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: l0, v0

Proof step 21 from proof step-absstep-ready-W1-invFLITPSCWRITE-same (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l1