Proof step 1 from proof step-absstep-W3-W4-doWritePSC-other (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ls.l = als.il, ags.pm = gs.mem, ags0.pm = ∅ ⊕ (ags0.h | true), ags.pm = ∅ ⊕ (ags.h | true), lsf(t0).t = alsf(t0).t, ls.t = als.t, lsf(t0).t = t0, lsf(t).t = t, alsf(t).t = t, ls.v = als.iv, ags.vm = gs.mem ⊕ gs.p, ags0.vm = ∅ ⊕ ags0.h, ags.vm = ∅ ⊕ ags.h, W4 = pcstepf(gs, ls, W3, doWritePSC(ls.t, l, v)), alsf(t) = als, apc = invWrite, apcf(t) = apc, gs0 = gstepf(gs, ls, W3, doWritePSC(ls.t, l, v)), ls0 = lstepf(gs, ls, W3, doWritePSC(ls.t, l, v)), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = W3, pcf0(t) = W4, t ≠ t0, FLITPSCLInv(gs0, lsf(t0), pcf(t0)), FLITPSCLInv(gs, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), 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), noPending(t, gs.p), 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), pendingOk(gs0.p), pendingOk(gs.p), pre(gs, ls, W3, doWritePSC(ls.t, l, v)), writersOk(gs0.p, gs0.writers), writersOk(gs.p, gs.writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs.p(l) → ((ags.h | l) | lsf(t0).t) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | lsf(t0).t) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs.p(l0) → ((ags.h | l0) | lsf(t0).t) | false = []), pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = W4 → ((ags.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | lsf(t0).t) | false = [], pre(ags, als, apc, ADoWrite(ls.t)) → ags0 = gstepf(ags, als, apc, ADoWrite(ls.t)) ∧ als0 = lstepf(ags, als, apc, ADoWrite(ls.t)) ∧ apc0 = pcstepf(ags, als, apc, ADoWrite(ls.t)), ∀ l. ((ags.h | l) | ls.t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), ∀ t0. t0 ≠ t → alsf(t0).t = t0, ∀ t0. t0 ≠ t → lsf(t0).t = t0 ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = invRead) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite) ∧ (pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite) ∧ (pcf(t0) = R1 → lsf(t0).l = alsf(t0).il) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov) ∧ ( pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv) ∧ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ gs0.p(l) → ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags0.h | l) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ gs0.p(l0) → ((ags0.h | l0) | lsf(t0).t) | false = [])) ∧ (pcf(t0) = R2 → gs0.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = []) ∧ ( pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | lsf(t0).t) | false = [])

Rule argument

Additional information

Proof step 2 from proof step-absstep-W3-W4-doWritePSC-other (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, ags0.pm = ∅ ⊕ (ags0.h | true), lsf(t0).t = t0, lsf(t).t = t, alsf(t0).t = t0, alsf(t).t = t, lsf(t).v = alsf(t).iv, ags.vm = gs.mem ⊕ gs.p, ags0.vm = ∅ ⊕ ags0.h, ags.vm = ∅ ⊕ ags.h, apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, t ≠ t0, FLITPSCLInv(gs.p:= gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), lsf(t0), pcf(t0)), FLITPSCLInv(gs, lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t0), apcf(t0)), PLIBLInv(ags, alsf(t), invWrite), abs(ags.h, gs.readers, gs.p), allReadsOK(ags0.h), allReadsOK(ags.h), allWritesOK(ags0.h), allWritesOK(ags.h), ctrok(gs.ctr, gs.writers), noPending(t, gs.p), 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) + W(alsf(t).iv, t) ')), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(gs.p), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), gs.writers), writersOk(gs.p, gs.writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ gs.p(l) → ((ags.h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((ags.h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ gs.p(l0) → ((ags.h | l0) | t0) | false = []), pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags.h | lsf(t0).l) | t0) | false = [], pcf(t0) = W4 → ((ags.h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags.h | lsf(t0).l) | t0) | false = [], (ags.h | t) | false = [] → ags0 = (ags.vm:= ags.vm(alsf(t).il := alsf(t).iv)).h:= (ags.h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((ags.h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l0)) → ((ags0.h | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((ags0.h | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l2)) → ((ags0.h | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | t0) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ ls.t = t → pcstepf(gs, ls, invWrite, ADoWrite(t)) = resWrite; (s) ⊦ ls.t = t → lstepf(gs, ls, invWrite, ADoWrite(t)) = ls; (s) ⊦ x + a = x + a '; (s) ⊦ ls.t = t → gstepf(gs, ls, invWrite, ADoWrite(t)) = (gs.vm:= gs.vm(ls.il := ls.iv)).h:= (gs.h + (W(ls.t, ls.il, ls.iv), false)); (s) ⊦ ADoWrite(t) = ADoWrite(t0) ↔ t = t0; (s) ⊦ pre(gs, ls, invWrite, a) ↔ a = ADoWrite(ls.t) ∧ (gs.h | ls.t) | false = []; (s) ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ gstepf(gs, ls, W3, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + W(ls.v, ls.t)); (s) ⊦ (gs.p:= p).p = p; (s) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ (gs.p:= p).readers = gs.readers; (s) ⊦ doWritePSC(t, l, v) = doWritePSC(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0; (ws) ⊦ pre(gs, ls, W3, a) ↔ a = doWritePSC(ls.t, ls.l, ls.v); (s) ⊦ pcstepf(gs, ls, W3, a) = W4; (s) ⊦ lstepf(gs, ls, W3, a) = ls; (s)

Proof step 3 from proof step-absstep-W3-W4-doWritePSC-other (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), ags0.pm = ∅ ⊕ (ags0.h | true), alsf(t).t = t, alsf(t0).t = t0, lsf(t).t = t, lsf(t0).t = t0, lsf(t).v = alsf(t).iv, ags0.vm = ∅ ⊕ ags0.h, ags = mkPLIBgs(mem, mem0, h), apcf(t) = invWrite, lsf0(t) = lsf(t), mem = ∅ ⊕ h, mem = gs.mem ⊕ gs.p, mem0 = gs.mem, pcf(t) = W3, pcf0(t) = W4, t ≠ t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs.p:= gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), lsf(t0), pcf(t0)), PLIBLInv(ags, alsf(t), invWrite), PLIBLInv(ags, alsf(t0), apcf(t0)), abs(h, gs.readers, gs.p), allReadsOK(h), allReadsOK(ags0.h), allWritesOK(h), allWritesOK(ags0.h), ctrok(gs.ctr, gs.writers), noPending(t, gs.p), 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) + W(alsf(t).iv, t) ')), pendingOk(gs.p), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) ')), writersOk(gs.p, gs.writers), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), gs.writers), (h | t) | false = [] → ags0 = (ags.vm:= mem(alsf(t).il := alsf(t).iv)).h:= (h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ gs.p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ gs.p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l0)) → ((ags0.h | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((ags0.h | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l2)) → ((ags0.h | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | t0) | 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-W3-W4-doWritePSC-other (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), ags0.pm = ∅ ⊕ (ags0.h | true), lsf(t0).t = t0, lsf(t).t = t, alsf(t0).t = t0, alsf(t).t = t, lsf(t).v = alsf(t).iv, ags0.vm = ∅ ⊕ ags0.h, apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, gs.mem ⊕ gs.p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(gs.p:= gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), lsf(t0), pcf(t0)), FLITPSCLInv(gs, lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t0), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), invWrite), abs(h, gs.readers, gs.p), allReadsOK(ags0.h), allReadsOK(h), allWritesOK(ags0.h), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPending(t, gs.p), 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) + W(alsf(t).iv, t) ')), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(gs.p), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), gs.writers), writersOk(gs.p, gs.writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ gs.p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ gs.p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], (h | t) | false = [] → ags0 = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), gs.mem, h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l0)) → ((ags0.h | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((ags0.h | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l2)) → ((ags0.h | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((ags0.h | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((ags0.h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((ags0.h | lsf(t0).l) | t0) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBgs(vm, vm0, h).h:= h0 = mkPLIBgs(vm, vm0, h0); (s) ⊦ mkPLIBgs(vm, vm0, h).vm:= vm1 = mkPLIBgs(vm1, vm0, h); (s)

Proof step 5 from proof step-absstep-W3-W4-doWritePSC-other (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, gs.mem = ∅ ⊕ (h | true), alsf(t).t = t, alsf(t0).t = t0, lsf(t).t = t, lsf(t0).t = t0, lsf(t).v = alsf(t).iv, ags0 = mkPLIBgs(mem, mem0, h0), apcf(t) = invWrite, lsf0(t) = lsf(t), mem = ∅ ⊕ h0, mem0 = ∅ ⊕ (h0 | true), pcf(t) = W3, pcf0(t) = W4, gs.mem ⊕ gs.p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs.p:= gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t0), apcf(t0)), abs(h, gs.readers, gs.p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(gs.ctr, gs.writers), noPending(t, gs.p), 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) + W(alsf(t).iv, t) ')), pendingOk(gs.p), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) ')), writersOk(gs.p, gs.writers), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), gs.writers), (h | t) | false = [] → ags0 = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), gs.mem, h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ gs.p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ gs.p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | 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-W3-W4-doWritePSC-other (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, gs.mem = ∅ ⊕ (h | true), lsf(t0).t = t0, lsf(t).t = t, alsf(t0).t = t0, alsf(t).t = t, lsf(t).v = alsf(t).iv, apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, gs.mem ⊕ gs.p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(gs.p:= gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), lsf(t0), pcf(t0)), FLITPSCLInv(gs, lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t0), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t), invWrite), abs(h, gs.readers, gs.p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(gs.ctr, gs.writers), noPending(t, gs.p), 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) + W(alsf(t).iv, t) ')), pendingOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(gs.p), writersOk(gs.p(alsf(t).il := gs.p(alsf(t).il) + W(alsf(t).iv, t) '), gs.writers), writersOk(gs.p, gs.writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ gs.p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ gs.p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), gs.mem, h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, gs.mem, h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ gs.p(alsf(t).il) + W(alsf(t).iv, t) ';gs.p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → gs.ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | false = [])

Rule argument

Additional information

Proof step 7 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  lsf(t).l = alsf(t).il, alsf(t).t = t, alsf(t0).t = t0, lsf(t).t = t, lsf(t0).t = t0, lsf(t).v = alsf(t).iv, apcf(t) = invWrite, gs = mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf0(t) = lsf(t), mem = ∅ ⊕ (h | true), pcf(t) = W3, pcf0(t) = W4, mem ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(gs.p:= p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t0), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, alsf(t).il, writers), onePendingW(t, alsf(t).il, p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(p), pendingOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), writersOk(p, writers), writersOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), writers), (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), mem, h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(gs, lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, mem, h), alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, mem, h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | 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 8 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  lsf(t).l = alsf(t).il, lsf(t0).t = t0, lsf(t).t = t, alsf(t0).t = t0, alsf(t).t = t, lsf(t).v = alsf(t).iv, apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), invWrite), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, alsf(t).il, writers), onePendingW(t, alsf(t).il, p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(p), writersOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = alsf(t0).il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = alsf(t0).ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = alsf(t0).il ∧ lsf(t0).v = alsf(t0).iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), ∅ ⊕ (h | true), h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); (s)

Proof step 9 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  lsf(t).l = alsf(t).il, alsf(t).t = t, lsf(t).t = t, lsf(t0).t = t0, lsf(t).v = alsf(t).iv, alsf(t0) = mkPLIBls(t2, il, iv, ov), apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, t2 = t0, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), ctr, writers, writers0), lsf(t0), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t0), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, alsf(t).il, writers), onePendingW(t, alsf(t).il, p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(p), pendingOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), writersOk(p, writers), writersOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), writers), (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), ∅ ⊕ (h | true), h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = il ∧ lsf(t0).v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov, pcf(t0) = R1 → lsf(t0).l = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | 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(t0), iv, t2, il, ov

Proof step 10 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  lsf(t).l = alsf(t).il, lsf(t0).t = t0, lsf(t).t = t, alsf(t).t = t, lsf(t).v = alsf(t).iv, alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), invWrite), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, alsf(t).il, writers), onePendingW(t, alsf(t).il, p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) ')), pendingOk(p), writersOk(p(alsf(t).il := p(alsf(t).il) + W(alsf(t).iv, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = il ∧ lsf(t0).v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(alsf(t).il := alsf(t).iv), ∅ ⊕ (h | true), h + (W(t, alsf(t).il, alsf(t).iv), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (alsf(t).il = l0 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (alsf(t).il = l2 ⊃ p(alsf(t).il) + W(alsf(t).iv, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | false = [])

Rule argument

Additional information

Proof step 11 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  lsf(t).l = il0, lsf(t).t = t, lsf(t0).t = t0, lsf(t).v = iv0, alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t2, il0, iv0, ov0), apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, t2 = t, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(il0 := p(il0) + W(iv0, t) '), ctr, writers, writers0), lsf(t0), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, il0, writers), onePendingW(t, il0, p(il0 := p(il0) + W(iv0, t) ')), pendingOk(p), pendingOk(p(il0 := p(il0) + W(iv0, t) ')), writersOk(p, writers), writersOk(p(il0 := p(il0) + W(iv0, t) '), writers), (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(il0 := iv0), ∅ ⊕ (h | true), h + (W(t, il0, iv0), false) ') ∧ als0 = alsf(t) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = il ∧ lsf(t0).v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov, pcf(t0) = R1 → lsf(t0).l = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (il0 = l0 ⊃ p(il0) + W(iv0, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (il0 = l2 ⊃ p(il0) + W(iv0, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | 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-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  lsf(t0).t = t0, lsf(t).t = t, alsf(t) = mkPLIBls(t, lsf(t).l, lsf(t).v, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) '), ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, lsf(t).l, lsf(t).v, ov0), invWrite), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, lsf(t).l, writers), onePendingW(t, lsf(t).l, p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) ')), pendingOk(p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) ')), pendingOk(p), writersOk(p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → lsf(t0).l = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = il ∧ lsf(t0).v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t0) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t0) | false = [], (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(lsf(t).l := lsf(t).v), ∅ ⊕ (h | true), h + (W(t, lsf(t).l, lsf(t).v), false) ') ∧ als0 = mkPLIBls(t, lsf(t).l, lsf(t).v, ov0) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (lsf(t).l = l0 ⊃ p(lsf(t).l) + W(lsf(t).v, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ lsf(t0).l ∧ ¬ FO(t0) ∈ (lsf(t).l = l2 ⊃ p(lsf(t).l) + W(lsf(t).v, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h0 | lsf(t0).l) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | lsf(t0).l) | t0) | false = (W(t0, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h0 | lsf(t0).l) | t0) | false = [])

Rule argument

Additional information

Proof step 13 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  lsf(t).t = t, alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, lsf(t).l, lsf(t).v, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t2, l3, v), lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, t2 = t0, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) '), ctr, writers, writers0), lsf(t0), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, lsf(t).l, lsf(t).v, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, lsf(t).l, writers), onePendingW(t, lsf(t).l, p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) ')), pendingOk(p), pendingOk(p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) ')), writersOk(p, writers), writersOk(p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) '), writers), (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(lsf(t).l := lsf(t).v), ∅ ⊕ (h | true), h + (W(t, lsf(t).l, lsf(t).v), false) ') ∧ als0 = mkPLIBls(t, lsf(t).l, lsf(t).v, ov0) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (lsf(t).l = l0 ⊃ p(lsf(t).l) + W(lsf(t).v, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (lsf(t).l = l2 ⊃ p(lsf(t).l) + W(lsf(t).v, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(l3) = 0 → ((h0 | l3) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h0 | l3) | t0) | 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(t0), t2, l3, v

Proof step 14 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  lsf(t).t = t, alsf(t) = mkPLIBls(t, lsf(t).l, lsf(t).v, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, lsf(t).l, lsf(t).v, ov0), invWrite), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, lsf(t).l, writers), onePendingW(t, lsf(t).l, p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) ')), pendingOk(p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) ')), pendingOk(p), writersOk(p(lsf(t).l := p(lsf(t).l) + W(lsf(t).v, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(lsf(t).l := lsf(t).v), ∅ ⊕ (h | true), h + (W(t, lsf(t).l, lsf(t).v), false) ') ∧ als0 = mkPLIBls(t, lsf(t).l, lsf(t).v, ov0) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (lsf(t).l = l0 ⊃ p(lsf(t).l) + W(lsf(t).v, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (lsf(t).l = l2 ⊃ p(lsf(t).l) + W(lsf(t).v, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(l3) = 0 → ((h0 | l3) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h0 | l3) | t0) | false = [])

Rule argument

Additional information

Proof step 15 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t2, l4, v0), lsf0(t) = lsf(t), pcf(t) = W3, pcf0(t) = W4, t2 = t, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(l4 := v0), ∅ ⊕ (h | true), h + (W(t, l4, v0), false) ') ∧ als0 = mkPLIBls(t, l4, v0, ov0) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l4) + W(v0, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l4) + W(v0, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(l3) = 0 → ((h0 | l3) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h0 | l3) | t0) | 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, l4, v0

Proof step 16 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h0), allReadsOK(h), allWritesOK(h0), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], (h | t) | false = [] → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(l4 := v0), ∅ ⊕ (h | true), h + (W(t, l4, v0), false) ') ∧ als0 = mkPLIBls(t, l4, v0, ov0) ∧ apc0 = resWrite, ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(l3) = 0 → ((h0 | l3) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h0 | l3) | t0) | false = [])

Rule argument

Additional information

Proof step 17 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ (h | t) | false = [] ↔ (∀ l. ((h | l) | t) | false = [])

• Proof step 19:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h0), allWritesOK(h), allWritesOK(h0), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), (∀ l. ((h | l) | t) | false = []) → mkPLIBgs(∅ ⊕ h0, ∅ ⊕ (h0 | true), h0) = mkPLIBgs((∅ ⊕ h)(l4 := v0), ∅ ⊕ (h | true), h + (W(t, l4, v0), false) ') ∧ als0 = mkPLIBls(t, l4, v0, ov0) ∧ apc0 = resWrite, pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)) → ((h0 | l0) | t0) | false = []) ∧ (pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h0 | l1) | t0) | false = []) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)) → ((h0 | l2) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(l3) = 0 → ((h0 | l3) | t0) | false = []) ∧ (pcf(t0) = W4 → ((h0 | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h0 | l3) | t0) | false = [])

Rule argument

Additional information

Used terms: h, t

Proof step 18 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1 ⊦ ( pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)) → ((h | l0) | t0) | false = [] ∧ ((l4 = l0 ⊃ (W(t, l0, v0), false) ';[]) | t0) | false = []) ∧ ( pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → ((h | l1) | t0) | false = [] ∧ ((l4 = l1 ⊃ (W(t, l1, v0), false) ';[]) | t0) | false = []) ∧ ( pcf(t0) = R2 ∨ pcf(t0) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)) → ((h | l2) | t0) | false = [] ∧ ((l4 = l2 ⊃ (W(t, l2, v0), false) ';[]) | t0) | false = []) ∧ (pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [] ∧ ((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false = []) ∧ ( pcf(t0) = W4 → (((h | l3) | t0) | false) + (((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false) = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [] ∧ ((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false = [])

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ h + h0 | t = (h | t) + (h0 | t); (s) ⊦ W(t, l, v).l = l; (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ h + (e, false) ' | true = h | true; (s) ⊦ mem ⊕ (h + (W(t, l, v), b) ') = (mem ⊕ h)(l := v); (s) ⊦ mkPLIBgs(vm, vm0, h) = mkPLIBgs(vm1, vm2, h0) ↔ vm = vm1 ∧ vm0 = vm2 ∧ h = h0; (ws)

Proof step 20 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 21:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦ ((h | l0) | t0) | false = [] ∧ ((l4 = l0 ⊃ (W(t, l0, v0), false) ';[]) | t0) | false = []

• Proof step 28:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 ⊦ ((h | l1) | t0) | false = [] ∧ ((l4 = l1 ⊃ (W(t, l1, v0), false) ';[]) | t0) | false = []

• Proof step 32:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦ ((h | l2) | t0) | false = [] ∧ ((l4 = l2 ⊃ (W(t, l2, v0), false) ';[]) | t0) | false = []

• Proof step 39:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, ctr(l3) = 0, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t0) = R2, pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ((h | l3) | t0) | false = [] ∧ ((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false = []

• Proof step 41:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t0) = W4, pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, (((h | l3) | t0) | false) + (((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false) ≠ (W(t0, l3, v), false) ', t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦ ((h | l3) | t0) | false = [] ∧ ((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false = []

Rule argument

Additional information

Proof step 21 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)), pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦ ((h | l0) | t0) | false = [] ∧ ((l4 = l0 ⊃ (W(t, l0, v0), false) ';[]) | t0) | false = []

Rule argument

Additional information

Proof step 22 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 23:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((h | l0) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

• Proof step 27:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((l4 = l0 ⊃ (W(t, l0, v0), false) ';[]) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ (l4 = l0 ⊃ p(l0) + W(v0, t) ';p(l0)), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Proof step 23 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 24:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, l4 = l0, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((h | l0) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), ¬ FO(t0) ∈ p(l0) + W(v0, t) ', pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

• Proof step 26:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l4 ≠ l0, t ≠ t0, ((h | l0) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), ¬ FO(t0) ∈ p(l0), pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Proof step 24 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  alsf(t) = mkPLIBls(t, l0, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l0, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l0, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((h | l0) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l0 := p(l0) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l0, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l0, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l0, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l0, writers), onePendingW(t, l0, p(l0 := p(l0) + W(v0, t) ')), pendingOk(p(l0 := p(l0) + W(v0, t) ')), pendingOk(p), writersOk(p(l0 := p(l0) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ p(l0), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid) ≠ W(v, tid0); (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 25 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 26 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 27 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] | b = []; (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s) ⊦ W(t, l, v).t = t; (s) Used formulas: l4 = l0

Proof step 28 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l. ((h | l) | t0) | false = [], pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 ⊦ ((h | l1) | t0) | false = [] ∧ ((l4 = l1 ⊃ (W(t, l1, v0), false) ';[]) | t0) | false = []

Rule argument

Additional information

Proof step 29 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 30:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((h | l1) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l. ((h | l) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 ⊦

• Proof step 31:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((l4 = l1 ⊃ (W(t, l1, v0), false) ';[]) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l. ((h | l) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 ⊦

Rule argument

Additional information

Proof step 30 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l1

Proof step 31 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] | b = []; (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s) ⊦ W(t, l, v).t = t; (s) Used formulas: l4 = l1

Proof step 32 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)), pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦ ((h | l2) | t0) | false = [] ∧ ((l4 = l2 ⊃ (W(t, l2, v0), false) ';[]) | t0) | false = []

Rule argument

Additional information

Proof step 33 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 34:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, t ≠ t0, ((h | l2) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦

• Proof step 38:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, t ≠ t0, ((l4 = l2 ⊃ (W(t, l2, v0), false) ';[]) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ (l4 = l2 ⊃ p(l2) + W(v0, t) ';p(l2)), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦

Rule argument

Additional information

Proof step 34 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 35:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, l4 = l2, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, t ≠ t0, ((h | l2) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), ¬ FO(t0) ∈ p(l2) + W(v0, t) ', pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦

• Proof step 37:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), alsf(t) = mkPLIBls(t, l4, v0, ov0), apcf(t) = invWrite, lsf(t0) = mkFLITPSCls(t0, l3, v), lsf(t) = mkFLITPSCls(t, l4, v0), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, l4 ≠ l2, t ≠ t0, ((h | l2) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), allReadsOK(h), allReadsOK(h + (W(t, l4, v0), false) '), allWritesOK(h), allWritesOK(h + (W(t, l4, v0), false) '), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), pendingOk(p(l4 := p(l4) + W(v0, t) ')), writersOk(p, writers), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), ¬ FO(t0) ∈ p(l2), pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = idle → apcf(t0) = idle, ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ∀ l. ((h | l) | t) | false = [], ∀ t1. lsf(t1).t = t1, ∀ t1. alsf(t1).t = t1, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦

Rule argument

Additional information

Proof step 35 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  alsf(t) = mkPLIBls(t, l2, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l2, v0), lsf(t0) = mkFLITPSCls(t0, l3, v), lsf0(t) = mkFLITPSCls(t, l2, v0), pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, l2 ≠ l3, t ≠ t0, ((h | l2) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l2 := p(l2) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), apcf(t0)), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l2, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l2, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l2, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l2, writers), onePendingW(t, l2, p(l2 := p(l2) + W(v0, t) ')), pendingOk(p(l2 := p(l2) + W(v0, t) ')), pendingOk(p), writersOk(p(l2 := p(l2) + W(v0, t) '), writers), writersOk(p, writers), ¬ FO(t0) ∈ p(l2), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = invRead, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → apcf(t0) = resRead, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 → apcf(t0) = invWrite, pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t0) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], ∀ l0. l0 ≠ l3 ∧ ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), pcf(t0) = R2 ∨ pcf(t0) = R3 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid) ≠ W(v, tid0); (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 36 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l2

Proof step 37 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l2

Proof step 38 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] | b = []; (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s) ⊦ W(t, l, v).t = t; (s) Used formulas: l4 = l2

Proof step 39 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t0) = resRead, apcf(t) = invWrite, ctr(l3) = 0, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, l3, ov), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t0) = R2, pcf(t) = W3, pcf0(t) = W4, ((h | l3) | t0) | false = [], (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, t ≠ t0, ((l4 = l3 ⊃ (W(t, l3, v0), false) ';[]) | t0) | false ≠ [], FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, l3, ov), R2), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, l3, ov), R2), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), resRead), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ∀ l. ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], ∀ l0. ¬ FO(t0) ∈ p(l0) → ((h | l0) | t0) | false = [], ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ R1 ≠ R2; (s) ⊦ R2 ≠ crashed; (s) ⊦ R2 ≠ ready; (s) ⊦ R2 ≠ idle; (s) ⊦ R2 ≠ W7; (s) ⊦ R2 ≠ W6; (s) ⊦ R2 ≠ W3; (s) ⊦ R2 ≠ W2; (s) ⊦ R2 ≠ W5; (s) ⊦ R2 ≠ W4; (s) ⊦ R2 ≠ W1; (s)

Proof step 40 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] | b = []; (s) ⊦ oneMember(t, l, writers) ∧ ctrok(ctr, writers) → ctr(l) ≠ 0; (as) Used formulas: l4 = l3

Proof step 41 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  alsf(t) = mkPLIBls(t, l4, v0, ov0), alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t0) = resWrite, apcf(t) = invWrite, lsf(t) = mkFLITPSCls(t, l4, v0), lsf(t0) = mkFLITPSCls(t0, il, iv), lsf0(t) = mkFLITPSCls(t, l4, v0), pcf(t0) = W4, pcf(t) = W3, pcf0(t) = W4, (∅ ⊕ (h | true)) ⊕ p = ∅ ⊕ h, (((h | il) | t0) | false) + (((l4 = il ⊃ (W(t, il, v0), false) ';[]) | t0) | false) ≠ (W(t0, il, iv), false) ', t ≠ t0, FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), mkFLITPSCls(t0, il, iv), W4), FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p(l4 := p(l4) + W(v0, t) '), ctr, writers, writers0), mkFLITPSCls(t0, il, iv), W4), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t0, il, iv, ov), resWrite), PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), mkPLIBls(t, l4, v0, ov0), invWrite), abs(h, writers0, p), allReadsOK(h + (W(t, l4, v0), false) '), allReadsOK(h), allWritesOK(h + (W(t, l4, v0), false) '), allWritesOK(h), ctrok(ctr, writers), noPending(t, p), notMember(t, writers0), oneMember(t, l4, writers), onePendingW(t, l4, p(l4 := p(l4) + W(v0, t) ')), pendingOk(p(l4 := p(l4) + W(v0, t) ')), pendingOk(p), writersOk(p(l4 := p(l4) + W(v0, t) '), writers), writersOk(p, writers), ∀ t1. alsf(t1).t = t1, ∀ t1. lsf(t1).t = t1, ∀ l. ((h | l) | t) | false = [], ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITPSCLInv(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1)) ∧ PLIBLInv(mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)) ∧ labs(mkFLITPSCgs(∅ ⊕ (h | true), p, ctr, writers, writers0), lsf(t1), pcf(t1), mkPLIBgs(∅ ⊕ h, ∅ ⊕ (h | true), h), alsf(t1), apcf(t1)), ((h | il) | t0) | false = (W(t0, il, iv), false) ' ∨ ((h | il) | t0) | false = [] ⊦ ((h | il) | t0) | false = [] ∧ ((l4 = il ⊃ (W(t, il, v0), false) ';[]) | t0) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ W3 ≠ W4; (s) ⊦ W2 ≠ W4; (s) ⊦ W1 ≠ W4; (s) ⊦ R4 ≠ W4; (s) ⊦ R3 ≠ W4; (s) ⊦ R2 ≠ W4; (s) ⊦ R1 ≠ W4; (s) ⊦ W4 ≠ crashed; (s) ⊦ W4 ≠ ready; (s) ⊦ W4 ≠ idle; (s) ⊦ W4 ≠ W7; (s) ⊦ W4 ≠ W6; (s) ⊦ W4 ≠ W5; (s)

Proof step 42 from proof step-absstep-W3-W4-doWritePSC-other (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] | t = []; (s) ⊦ [] | b = []; (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s) ⊦ W(t, l, v).t = t; (s) Used formulas: l4 = il