Proof step 1 from proof step-absstep-PSCPERSIST_FO-tau (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITPSCInv(gs0, lsf0, pcf0), FLITPSCInv(gs, lsf, pcf), PLIBInv(ags, alsf, apcf), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)), flitpscStep(mkstate(gs, lsf, pcf), globalPSCPERSIST_FO(l), mkstate(gs0, lsf0, pcf0)), ¬ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags, alsf, apcf)) ⊦

Rule argument

Additional information

Proof step 2 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ags.pm = gs.mem, ags.vm = gs.mem ⊕ gs.p, FLITPSCInv(gs.p:= gs.p(l0 := gs.p(l0) -p n), lsf, pcf), FLITPSCInv(gs, lsf, pcf), PLIBInv(ags, alsf, apcf), abs(ags.h, gs.readers, gs.p), isPersistFO(n, gs.p(l0)), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ags.vm = gs.mem ⊕ gs.p(l0 := gs.p(l0) -p n) ∧ abs(ags.h, gs.readers, gs.p(l0 := gs.p(l0) -p n)) ∧ labs(gs.p:= gs.p(l0 := gs.p(l0) -p n), lsf(t), pcf(t), ags, alsf(t), apcf(t))

Rule argument

Additional information

Used simplifier rules: abs-def: ⊦ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ↔ gabs(gs, lsf, pcf, ags, alsf, apcf) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t))); gabs-def: ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p); ⊦ (gs.p:= p).p = p; (s) ⊦ (gs.p:= p).readers = gs.readers; (s) ⊦ (gs.p:= p).mem = gs.mem; (s) ⊦ globalPSCCRASH ≠ globalPSCPERSIST_FO(l); (s) ⊦ globalPSCPERSIST_FO(l) = globalPSCPERSIST_FO(l0) ↔ l = l0; (s) ⊦ globalPSCPERSIST_FO(l) ≠ globalPSCPERSIST_W(l0); (s) ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_FO(l)); (s) ⊦ lstep(gs, ls, pc, a, gs0, ls0, pc0) ↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a); (s) ⊦ flitpscStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(gs.p(l)) < # gs.p(l) ∧ gs0 = (gs.mem:= gs.mem(l := gs.p(l)[firstPersistW(gs.p(l))].val)) .p:= gs.p(l := gs.p(l) -p firstPersistW(gs.p(l))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, gs.p(l)) ∧ gs0 = gs.p:= gs.p(l := gs.p(l) -p n)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)); (s)

Proof step 3 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  ags = mkPLIBgs(mem, mem0, h), mem = gs.mem ⊕ gs.p, mem0 = gs.mem, FLITPSCInv(gs, lsf, pcf), FLITPSCInv(gs.p:= gs.p(l0 := gs.p(l0) -p n), lsf, pcf), PLIBInv(ags, alsf, apcf), abs(h, gs.readers, gs.p), isPersistFO(n, gs.p(l0)), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ mem = gs.mem ⊕ gs.p(l0 := gs.p(l0) -p n) ∧ abs(h, gs.readers, gs.p(l0 := gs.p(l0) -p n)) ∧ labs(gs.p:= gs.p(l0 := gs.p(l0) -p n), lsf(t), pcf(t), ags, alsf(t), apcf(t))

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-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  FLITPSCInv(gs.p:= gs.p(l0 := gs.p(l0) -p n), lsf, pcf), FLITPSCInv(gs, lsf, pcf), PLIBInv(mkPLIBgs(gs.mem ⊕ gs.p, gs.mem, h), alsf, apcf), abs(h, gs.readers, gs.p), isPersistFO(n, gs.p(l0)), ∀ t. labs(gs, lsf(t), pcf(t), mkPLIBgs(gs.mem ⊕ gs.p, gs.mem, h), alsf(t), apcf(t)) ⊦ gs.mem ⊕ gs.p = gs.mem ⊕ gs.p(l0 := gs.p(l0) -p n) ∧ abs(h, gs.readers, gs.p(l0 := gs.p(l0) -p n)) ∧ labs(gs.p:= gs.p(l0 := gs.p(l0) -p n), lsf(t), pcf(t), mkPLIBgs(gs.mem ⊕ gs.p, gs.mem, h), alsf(t), apcf(t))

Rule argument

Additional information

Proof step 5 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  gs = mkFLITPSCgs(mem, p, ctr, writers, writers0), FLITPSCInv(gs, lsf, pcf), FLITPSCInv(gs.p:= p(l0 := p(l0) -p n), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(gs, lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ mem ⊕ p = mem ⊕ p(l0 := p(l0) -p n) ∧ abs(h, writers0, p(l0 := p(l0) -p n)) ∧ labs(gs.p:= p(l0 := p(l0) -p n), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t))

Rule argument

Additional information

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

Proof step 6 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ mem ⊕ p = mem ⊕ p(l0 := p(l0) -p n) ∧ abs(h, writers0, p(l0 := p(l0) -p n)) ∧ labs(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t))

Rule argument

Additional information

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

Proof step 7 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  mem ⊕ p ≠ mem ⊕ p(l0 := p(l0) -p n), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

• Proof step 14:

  FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ abs(h, writers0, p(l0 := p(l0) -p n)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

• Proof step 16:

  FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ labs(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 8 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 9:

  ((mem ⊕ p))(l) ≠ ((mem ⊕ p(l0 := p(l0) -p n)))(l), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 9 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  mem(l) ⊕ p(l) ≠ mem(l) ⊕ (l0 = l ⊃ p(l) -p n;p(l)), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

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

Proof step 10 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  l0 = l, mem(l) ⊕ p(l) ≠ mem(l) ⊕ (p(l) -p n), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 11 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  mem(l) ⊕ p(l) ≠ mem(l) ⊕ (p(l) -p n), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 12 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ isPersistFO(n, fowl) ↔ n < # fowl ∧ fowl[n].FO? ∧ (∀ m. m < n → fowl[m].tid ≠ fowl[n].tid ∧ fowl[m].FO?)

Rule argument

Additional information

Used simplifier rules: ⊦ fowl[n].FO? ∧ n < # fowl → v ⊕ (fowl -p n) = v ⊕ fowl; (s) ⊦ fowl0 |W = fowl1 |W → (v ⊕ fowl0 = v ⊕ fowl1 ↔ true); (s) Used terms: n, p(l)

Proof step 13 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ allReadsOK(h) ∧ isPersistFO(n, p(l)) ∧ abs(h, rs, p) → abs(h, rs, p(l := p(l) -p n))

Rule argument

Additional information

Used simplifier rules: ⊦ PLIBInv(mkPLIBgs(vm, pm, h), lsf, pcf) → allReadsOK(h); (ss) Used terms: l0, writers0, n, p, h

Proof step 15 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ lsf(t).t = alsf(t).t ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) = ready → apcf(t) = ready) ∧ (pcf(t) = crashed → apcf(t) = crashed) ∧ (pcf(t) = R1 → apcf(t) = invRead) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite) ∧ (pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite) ∧ (pcf(t) = R1 → lsf(t).l = alsf(t).il) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → lsf(t).v = alsf(t).ov) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → lsf(t).l = alsf(t).il ∧ lsf(t).v = alsf(t).iv) ∧ ( pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → ¬ FO(lsf(t).t) ∈ (l0 = l ⊃ p(l) -p n;p(l)) → ((h | l) | lsf(t).t) | false = []) ∧ (pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → ((h | l1) | lsf(t).t) | false = []) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 → l2 ≠ lsf(t).l ∧ ¬ FO(lsf(t).t) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)) → ((h | l2) | lsf(t).t) | false = []) ∧ (pcf(t) = R2 → ctr(lsf(t).l) = 0 → ((h | lsf(t).l) | lsf(t).t) | false = []) ∧ (pcf(t) = W4 → ((h | lsf(t).l) | lsf(t).t) | false = (W(lsf(t).t, lsf(t).l, lsf(t).v), false) ' ∨ ((h | lsf(t).l) | lsf(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ ( pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ ( pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ ( pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []); ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s)

Proof step 17 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 18:

  alsf(t) = mkPLIBls(t0, il, iv, ov), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ lsf(t).t = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) = ready → apcf(t) = ready) ∧ (pcf(t) = crashed → apcf(t) = crashed) ∧ (pcf(t) = R1 → apcf(t) = invRead) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite) ∧ (pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite) ∧ (pcf(t) = R1 → lsf(t).l = il) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → lsf(t).v = ov) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → lsf(t).l = il ∧ lsf(t).v = iv) ∧ ( pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → ¬ FO(lsf(t).t) ∈ (l0 = l ⊃ p(l) -p n;p(l)) → ((h | l) | lsf(t).t) | false = []) ∧ (pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → ((h | l1) | lsf(t).t) | false = []) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 → l2 ≠ lsf(t).l ∧ ¬ FO(lsf(t).t) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)) → ((h | l2) | lsf(t).t) | false = []) ∧ (pcf(t) = R2 → ctr(lsf(t).l) = 0 → ((h | lsf(t).l) | lsf(t).t) | false = []) ∧ (pcf(t) = W4 → ((h | lsf(t).l) | lsf(t).t) | false = (W(lsf(t).t, lsf(t).l, lsf(t).v), false) ' ∨ ((h | lsf(t).l) | lsf(t).t) | false = [])

Rule argument

Additional information

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

Proof step 18 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 19:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l3, v), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) = ready → apcf(t) = ready) ∧ (pcf(t) = crashed → apcf(t) = crashed) ∧ (pcf(t) = R1 → apcf(t) = invRead) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite) ∧ (pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite) ∧ (pcf(t) = R1 → l3 = il) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv) ∧ ( pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → ¬ FO(t1) ∈ (l0 = l ⊃ p(l) -p n;p(l)) → ((h | l) | t1) | false = []) ∧ (pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → ((h | l1) | t1) | false = []) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 → l2 ≠ l3 ∧ ¬ FO(t1) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)) → ((h | l2) | t1) | false = []) ∧ (pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t1) | false = []) ∧ (pcf(t) = W4 → ((h | l3) | t1) | false = (W(t1, l3, v), false) ' ∨ ((h | l3) | t1) | false = [])

Rule argument

Additional information

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

Proof step 19 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l3, v), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) = ready → apcf(t) = ready) ∧ (pcf(t) = crashed → apcf(t) = crashed) ∧ (pcf(t) = R1 → apcf(t) = invRead) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite) ∧ (pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite) ∧ (pcf(t) = R1 → l3 = il) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv) ∧ ( pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → ¬ FO(t0) ∈ (l0 = l ⊃ p(l) -p n;p(l)) → ((h | l) | t0) | false = []) ∧ (pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → ((h | l1) | t0) | false = []) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)) → ((h | l2) | t0) | false = []) ∧ (pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = []) ∧ (pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [])

Rule argument

Additional information

Proof step 20 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 21:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l3, v), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) = ready → apcf(t) = ready) ∧ (pcf(t) = crashed → apcf(t) = crashed) ∧ (pcf(t) = R1 → apcf(t) = invRead) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite) ∧ (pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite) ∧ (pcf(t) = R1 → l3 = il) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov) ∧ (pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv) ∧ ( pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → ¬ FO(t0) ∈ (l0 = l ⊃ p(l) -p n;p(l)) → ((h | l) | t0) | false = []) ∧ (pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → ((h | l1) | t0) | false = []) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)) → ((h | l2) | t0) | false = []) ∧ (pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = []) ∧ (pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [])

Rule argument

Additional information

Used terms: t

Proof step 21 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), pcf(t) = R1 → l3 = il, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ ( pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → ¬ FO(t0) ∈ (l0 = l ⊃ p(l) -p n;p(l)) → ((h | l) | t0) | false = []) ∧ (pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → ((h | l1) | t0) | false = []) ∧ (pcf(t) = R2 ∨ pcf(t) = R3 → l2 ≠ l3 ∧ ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)) → ((h | l2) | t0) | false = [])

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ ( pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ ( pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ ( pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []); ⊦ mkPLIBls(t, il, iv, iv0).il = il; (s) ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ mkPLIBls(t, il, iv, iv0).ov = iv0; (s) ⊦ mkFLITPSCls(t, l, v).v = v; (s) ⊦ mkPLIBls(t, il, iv, iv0).iv = iv; (s) ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s)

Proof step 22 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 23:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l ⊃ p(l) -p n;p(l)), pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

• Proof step 52:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), ((h | l1) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 ⊦

• Proof step 54:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)), pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 23 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l ⊃ p(l) -p n;p(l)), pcf(t) = R1 → l3 = il, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

Rule argument

Additional information

Proof step 24 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 25:

  alsf(t) = mkPLIBls(t0, il, iv, ov), l0 = l, lsf(t) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ p(l) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

• Proof step 51:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), l0 ≠ l, ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ p(l), pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

Rule argument

Additional information

Proof step 25 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), ¬ FO(t0) ∈ p(l) -p n, pcf(t) = R1 → l3 = il, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

Rule argument

Additional information

Proof step 26 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 27:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), t = t0, ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), ¬ FO(t0) ∈ p(l) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

• Proof step 48:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), t ≠ t0, ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), ¬ FO(t0) ∈ p(l) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = R1 → l3 = il, ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

Rule argument

Additional information

Used formulas: t = t0

Proof step 27 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), ¬ FO(t0) ∈ p(l) -p n, 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 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 28 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), ¬ FO(t0) ∈ p(l) -p n, 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | 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, ¬ FO(t0) ∈ p(l) → ((h | l) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Used terms: l

Proof step 29 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, 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 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), 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: delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del

Proof step 30 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

• Proof step 32:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. lsf(t).t = t ∧ FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Used terms: mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf

Proof step 31 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 33:

  lsf(t0).t = t0, FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t0), pcf(t0)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, 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 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Used terms: t0

Proof step 33 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, 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 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), 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: ⊦ mkFLITPSCls(t, l, v).t = t; (s)

Proof step 34 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p))

• Proof step 36:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | 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) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).readers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).writers), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 → oneMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCls(t0, l3, v).l, mkFLITPSCgs(mem, p, ctr, writers, writers0).writers), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).p), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).p), pcf(t0) = W4 ∨ pcf(t0) = W5 → onePendingW(mkFLITPSCls(t0, l3, v).t, mkFLITPSCls(t0, l3, v).l, mkFLITPSCgs(mem, p, ctr, writers, writers0).p), pcf(t0) = W5 → FOFollowsW(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).p(mkFLITPSCls(t0, l3, v).l)), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).writers), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).readers), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCls(t0, l3, v).l, mkFLITPSCgs(mem, p, ctr, writers, writers0).readers), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).writers), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).readers), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).p), pcf(t0) = idle → noPending(mkFLITPSCls(t0, l3, v).t, mkFLITPSCgs(mem, p, ctr, writers, writers0).p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Used terms: mkFLITPSCgs(mem, p, ctr, writers, writers0), mkFLITPSCls(t0, l3, v), pcf(t0)

Proof step 35 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, 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 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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) = idle → noPending(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = W5 → FOFollowsW(t0, p(l3)), pcf(t0) = W4 ∨ pcf(t0) = W5 → onePendingW(t0, l3, p), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(t0, writers0), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), 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: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0; (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers; (s) ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s)

Proof step 37 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 38:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) = W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(t0, writers0), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = W4 ∨ pcf(t0) = W5 → onePendingW(t0, l3, p), pcf(t0) = W5 → FOFollowsW(t0, p(l3)), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle → noPending(t0, p), 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

• Proof step 41:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) ≠ W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(t0, writers0), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = W4 ∨ pcf(t0) = W5 → onePendingW(t0, l3, p), pcf(t0) = W5 → FOFollowsW(t0, p(l3)), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle → noPending(t0, p), 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | 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, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 ⊦

Rule argument

Additional information

Used formulas: pcf(t0) = W5

Proof step 38 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t0) = resWrite, lsf(t0) = mkFLITPSCls(t0, il, iv), pcf(t0) = W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FOFollowsW(t0, p(il)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), notMember(t0, writers0), oneMember(t0, il, writers), onePendingW(t0, il, p), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W5 ≠ W6; (s) ⊦ W3 ≠ W5; (s) ⊦ W4 ≠ W5; (s) ⊦ W5 ≠ crashed; (s) ⊦ W1 ≠ W5; (s) ⊦ W2 ≠ W5; (s) ⊦ W5 ≠ W7; (s) ⊦ W5 ≠ idle; (s) ⊦ W5 ≠ ready; (s) ⊦ R2 ≠ W5; (s) ⊦ R3 ≠ W5; (s) ⊦ R1 ≠ W5; (s) ⊦ R4 ≠ W5; (s) ⊦ oneMember(t, l, tsf) → ¬ notMember(t, tsf); (as) ⊦ notMember(t, tsf) → ¬ oneMember(t, l, tsf); (as)

Proof step 39 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ onePendingW(t, l0, p) ∧ FOFollowsW(t, p(l0)) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ p(l) ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = []

Rule argument

Additional information

Used simplifier rules: ⊦ PLIBInv(mkPLIBgs(vm, pm, h), lsf, pcf) → allReadsOK(h); (ss) ⊦ notMember(t, tsf) → ¬ t ∈ tsf(l); (as) Used terms: l, il, t0, writers0, n, p, h

Proof step 40 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) ≠ W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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) = idle → noPending(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W4 → onePendingW(t0, l3, p), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(t0, writers0), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ⊦

Rule argument

Additional information

Proof step 42 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ noPendingW(t, p) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ fowl ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = []

• Proof step 44:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) ≠ W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(t0, writers0), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W4 → onePendingW(t0, l3, p), pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle → noPending(t0, p), 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ⊦ abs(h, writers0, p) ∧ allReadsOK(h) ∧ noPendingW(t0, p) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t0) ∈ p(l) -p n ∧ FO(t0) ∈ p(l) ∧ ¬ t0 ∈ writers0(l)

Rule argument

Additional information

Used terms: p(l), l, t0, writers0, n, p, h

Proof step 43 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) ≠ W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | 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 = [], 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) = idle → noPending(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W4 → onePendingW(t0, l3, p), pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → notMember(t0, writers0), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ⊦ noPendingW(t0, p) ∧ ¬ t0 ∈ writers0(l)

Rule argument

Additional information

Used simplifier rules: ⊦ PLIBInv(mkPLIBgs(vm, pm, h), lsf, pcf) → allReadsOK(h); (ss)

Proof step 45 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 46:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) ≠ W1, pcf(t0) ≠ W2, pcf(t0) ≠ W3, pcf(t0) ≠ W4, pcf(t0) ≠ W6, pcf(t0) ≠ W7, pcf(t0) ≠ W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 → oneMember(t0, l3, writers), pcf(t0) = W4 → onePendingW(t0, l3, p), pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → apcf(t0) = resWrite, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → l3 = il ∧ v = iv, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W7 → notMember(t0, writers), pcf(t0) = W1 ∨ pcf(t0) = W2 → noPendingW(t0, p), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → noPending(t0, p), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle → noPending(t0, p), 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, 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 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R1 → l3 = il, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ⊦ noPendingW(t0, p) ∧ ¬ t0 ∈ writers0(l)

Rule argument

Additional information

Used simplifier rules: ⊦ notMember(t, tsf) → ¬ oneMember(t, l, tsf); (as) ⊦ notMember(t, tsf) → ¬ t ∈ tsf(l); (as)

Proof step 46 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  FO(t0) = p(l)[n], alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l3, v), pcf(t0) ≠ W1, pcf(t0) ≠ W2, pcf(t0) ≠ W3, pcf(t0) ≠ W4, pcf(t0) ≠ W6, pcf(t0) ≠ W7, pcf(t0) ≠ W5, ((h | l) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l)), FO(t0) ∈ p(l), ¬ FO(t0) ∈ p(l) -p n, pcf(t0) = R1 → l3 = il, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → v = ov, pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t0) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], 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) = idle → noPending(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → noPendingW(t0, p), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers0), pcf(t0) = idle ∨ pcf(t0) = ready → notMember(t0, writers), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → noPendingW(t0, p), pcf(t0) = R2 ∨ pcf(t0) = R3 → oneMember(t0, l3, writers0), pcf(t0) = R1 ∨ pcf(t0) = R4 → notMember(t0, writers0), pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → notMember(t0, writers), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ⊦ noPendingW(t0, p) ∧ ¬ t0 ∈ writers0(l)

Rule argument

Additional information

Proof step 47 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ notMember(t, tsf) → ¬ oneMember(t, l, tsf); (as) ⊦ notMember(t, tsf) → ¬ t ∈ tsf(l); (as) ⊦ noPending(t, p) → noPendingW(t, p); (ss)

Proof step 48 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ PLIBInv(gs, lsf, pcf) ↔ PLIBGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ PLIBLInv(gs, lsf(t), pcf(t)))

• Proof step 50:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), t ≠ t0, ((h | l) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBGInv(mkPLIBgs(mem ⊕ p, mem, h)), abs(h, writers0, p), isPersistFO(n, p(l)), ¬ FO(t0) ∈ p(l) -p n, pcf(t) = R1 → l3 = il, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. alsf(t).t = t ∧ PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 ⊦

Rule argument

Additional information

Used terms: mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf

Proof step 49 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 51 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l

Proof step 52 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), ((h | l1) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), pcf(t) = R1 → l3 = il, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = R2 ∨ pcf(t) = R3 → (∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. ((h | l4) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 ⊦

Rule argument

Additional information

Proof step 53 from proof step-absstep-PSCPERSIST_FO-tau (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 54 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)), pcf(t) = R1 → l3 = il, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → v = ov, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 55 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 56:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, v), v = ov, l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)), pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, v), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ v = iv, pcf(t) = R1 → l3 = il, ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 56 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)), pcf(t) = R1 → l3 = il, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 57 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 58:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)), pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = R1 → l3 = il, l2 ≠ l3 ∧ ¬ FO(t0) ∈ p(l2) → ((h | l2) | t0) | false = [], ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used terms: l2

Proof step 58 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ (l0 = l2 ⊃ p(l2) -p n;p(l2)), pcf(t) = R1 → l3 = il, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 59 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 60:

  alsf(t) = mkPLIBls(t0, il, iv, ov), l0 = l2, lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l0 := p(l0) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l0)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = R1 → l3 = il, ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 60 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  FO(t0) = p(l2)[n], alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t) = R1 → l3 = il, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used simplifier rules: delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del

Proof step 61 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 62:

  FO(t0) = p(l2)[n], alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(mem ⊕ p, mem, h), alsf(t0), apcf(t0)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = R1 → l3 = il, ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used terms: t0

Proof step 62 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  lsf(t0).t = alsf(t0).t, FO(t0) = p(l2)[n], alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t) = R1 → l3 = il, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, 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(alsf(t0).t) ∈ p(l) → ((h | l) | alsf(t0).t) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | alsf(t0).t) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(alsf(t0).t) ∈ p(l0) → ((h | l0) | alsf(t0).t) | false = []), pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | alsf(t0).t) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | alsf(t0).t) | false = (W(alsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | alsf(t0).t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ ( pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ ( pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ ( pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []); ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s)

Proof step 63 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 64:

  lsf(t0).t = t1, FO(t0) = p(l2)[n], alsf(t) = mkPLIBls(t0, il, iv, ov), alsf(t0) = mkPLIBls(t1, il0, iv0, ov0), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t0) = W4 → ((h | lsf(t0).l) | t1) | false = (W(t1, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | t1) | false = [], pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | t1) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(t1) ∈ p(l0) → ((h | l0) | t1) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | t1) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(t1) ∈ p(l) → ((h | l) | t1) | 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 = il0 ∧ lsf(t0).v = iv0, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov0, pcf(t0) = R1 → lsf(t0).l = il0, 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, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = R1 → l3 = il, ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

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), iv0, t1, il0, ov0

Proof step 64 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  FO(t0) = p(l2)[n], alsf(t0) = mkPLIBls(lsf(t0).t, il0, iv0, ov0), alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t) = R1 → l3 = il, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, 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 = il0, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov0, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = il0 ∧ lsf(t0).v = iv0, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ p(l) → ((h | l) | lsf(t0).t) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | lsf(t0).t) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ p(l0) → ((h | l0) | lsf(t0).t) | false = []), pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | lsf(t0).t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Proof step 65 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 66:

  FO(t0) = p(l2)[n], alsf(t) = mkPLIBls(t0, il, iv, ov), alsf(t0) = mkPLIBls(lsf(t0).t, il0, iv0, ov0), lsf(t) = mkFLITPSCls(t0, l3, ov), t0 = t, l2 ≠ l3, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t0) = W4 → ((h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ p(l0) → ((h | l0) | lsf(t0).t) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | lsf(t0).t) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ p(l) → ((h | l) | lsf(t0).t) | 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 = il0 ∧ lsf(t0).v = iv0, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov0, pcf(t0) = R1 → lsf(t0).l = il0, 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, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = R1 → l3 = il, ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

• Proof step 76:

  FO(t0) = p(l2)[n], alsf(t) = mkPLIBls(t0, il, iv, ov), alsf(t0) = mkPLIBls(lsf(t0).t, il0, iv0, ov0), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, t0 ≠ t, ((h | l2) | t0) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t0) = W4 → ((h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ p(l0) → ((h | l0) | lsf(t0).t) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | lsf(t0).t) | false = []), pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ p(l) → ((h | l) | lsf(t0).t) | 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 = il0 ∧ lsf(t0).v = iv0, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov0, pcf(t0) = R1 → lsf(t0).l = il0, 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, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = R1 → l3 = il, ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used formulas: t0 = t

Proof step 66 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  FO(t) = p(l2)[n], alsf(t) = mkPLIBls(t, il0, iv0, ov), lsf(t) = mkFLITPSCls(t, l3, ov), l2 ≠ l3, ((h | l2) | t) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t) ∈ p(l2), ¬ FO(t) ∈ p(l2) -p n, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l. ((h | l) | t) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t) | false = [], pcf(t) = W4 → ((h | l3) | t) | false = (W(t, l3, ov), false) ' ∨ ((h | l3) | t) | false = [], pcf(t) = R1 → l3 = il0, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il0 ∧ ov = iv0, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t) | false = []), pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ mkFLITPSCls(t, l, v).v = v; (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkPLIBls(t, il, iv, iv0) = mkPLIBls(t0, il0, iv1, iv2) ↔ t = t0 ∧ il = il0 ∧ iv = iv1 ∧ iv0 = iv2; (ws) delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del

Proof step 67 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ abs(h, rs, p) ∧ allReadsOK(h) ∧ noPendingW(t, p) ∧ isPersistFO(n, p(l)) ∧ ¬ FO(t) ∈ p(l) -p n ∧ FO(t) ∈ fowl ∧ ¬ t ∈ rs(l) → ((h | l) | t) | false = []

• Proof step 69:

  FO(t) = p(l2)[n], alsf(t) = mkPLIBls(t, il0, iv0, ov), lsf(t) = mkFLITPSCls(t, l3, ov), l2 ≠ l3, ((h | l2) | t) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t) ∈ p(l2), ¬ FO(t) ∈ p(l2) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il0 ∧ ov = iv0, pcf(t) = R1 → l3 = il0, pcf(t) = W4 → ((h | l3) | t) | false = (W(t, l3, ov), false) ' ∨ ((h | l3) | t) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l. ((h | l) | t) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = []), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l0. l0 ≠ l3 ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦ abs(h, writers0, p) ∧ allReadsOK(h) ∧ noPendingW(t, p) ∧ isPersistFO(n, p(l2)) ∧ ¬ FO(t) ∈ p(l2) -p n ∧ FO(t) ∈ p(l2) ∧ ¬ t ∈ writers0(l2)

Rule argument

Additional information

Used terms: p(l2), l2, t, writers0, n, p, h

Proof step 68 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 69 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  FO(t) = p(l2)[n], alsf(t) = mkPLIBls(t, il0, iv0, ov), lsf(t) = mkFLITPSCls(t, l3, ov), l2 ≠ l3, ((h | l2) | t) | false ≠ [], FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t) ∈ p(l2), ¬ FO(t) ∈ p(l2) -p n, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l. ((h | l) | t) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t) | false = [], pcf(t) = W4 → ((h | l3) | t) | false = (W(t, l3, ov), false) ' ∨ ((h | l3) | t) | false = [], pcf(t) = R1 → l3 = il0, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il0 ∧ ov = iv0, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t) | false = []), pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦ noPendingW(t, p) ∧ ¬ t ∈ writers0(l2)

Rule argument

Additional information

Used simplifier rules: ⊦ PLIBInv(mkPLIBgs(vm, pm, h), lsf, pcf) → allReadsOK(h); (ss)

Proof step 70 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

  ⊦ FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

• Proof step 72:

  FO(t) = p(l2)[n], alsf(t) = mkPLIBls(t, il0, iv0, ov), lsf(t) = mkFLITPSCls(t, l3, ov), l2 ≠ l3, ((h | l2) | t) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t) ∈ p(l2), ¬ FO(t) ∈ p(l2) -p n, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = ready → apcf(t) = ready, pcf(t) = idle → apcf(t) = idle, pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = []), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il0 ∧ ov = iv0, pcf(t) = R1 → l3 = il0, pcf(t) = W4 → ((h | l3) | t) | false = (W(t, l3, ov), false) ' ∨ ((h | l3) | t) | false = [], pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t) | false = [], pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l. ((h | l) | t) | false = []), pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = []), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l0. l0 ≠ l3 ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t. lsf(t).t = t ∧ FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦ noPendingW(t, p) ∧ ¬ t ∈ writers0(l2)

Rule argument

Additional information

Used terms: mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf

Proof step 71 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 72 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 73:

  lsf(t).t = t, FO(t) = p(l2)[n], alsf(t) = mkPLIBls(t, il0, iv0, ov), lsf(t) = mkFLITPSCls(t, l3, ov), l2 ≠ l3, ((h | l2) | t) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t) ∈ p(l2), ¬ FO(t) ∈ p(l2) -p n, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l. ((h | l) | t) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t) | false = [], pcf(t) = W4 → ((h | l3) | t) | false = (W(t, l3, ov), false) ' ∨ ((h | l3) | t) | false = [], pcf(t) = R1 → l3 = il0, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il0 ∧ ov = iv0, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t) | false = []), pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦ noPendingW(t, p) ∧ ¬ t ∈ writers0(l2)

Rule argument

Additional information

Used terms: t

Proof step 73 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  FO(t) = p(l2)[n], alsf(t) = mkPLIBls(t, il0, iv0, ov), lsf(t) = mkFLITPSCls(t, l3, ov), l2 ≠ l3, ((h | l2) | t) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), mkFLITPSCls(t, l3, ov), pcf(t)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t) ∈ p(l2), ¬ FO(t) ∈ p(l2) -p n, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l. ¬ FO(t) ∈ p(l) → ((h | l) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l. ((h | l) | t) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t) | false = [], pcf(t) = W4 → ((h | l3) | t) | false = (W(t, l3, ov), false) ' ∨ ((h | l3) | t) | false = [], pcf(t) = R1 → l3 = il0, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il0 ∧ ov = iv0, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t) | false = []), pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, ∀ l0. l0 ≠ l3 ∧ ¬ FO(t) ∈ p(l0) → ((h | l0) | t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t) ∈ p(l4) → ((h | l4) | t) | false = [], pcf(t) = R2 ∨ pcf(t) = R3 ⊦ noPendingW(t, p) ∧ ¬ t ∈ writers0(l2)

Rule argument

Additional information

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

Proof step 74 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p))

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s) ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ notMember(t, tsf) → ¬ oneMember(t, l, tsf); (as) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers; (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0; (s) ⊦ oneMember(t, l, tsf) → ¬ notMember(t, tsf); (as) ⊦ oneMember(t, l, tsf) → (t ∈ tsf(l0) ↔ l = l0); (s) Used terms: mkFLITPSCgs(mem, p, ctr, writers, writers0), mkFLITPSCls(t, l3, ov), pcf(t)

Proof step 75 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

  ⊦ FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

• Proof step 78:

  FO(t0) = p(l2)[n], alsf(t0) = mkPLIBls(lsf(t0).t, il0, iv0, ov0), alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t0, l3, ov), l2 ≠ l3, t0 ≠ t, ((h | l2) | t0) | false ≠ [], FLITPSCGInv(mkFLITPSCgs(mem, p, ctr, writers, writers0)), FLITPSCInv(mkFLITPSCgs(mem, p(l2 := p(l2) -p n), ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), isPersistFO(n, p(l2)), FO(t0) ∈ p(l2), ¬ FO(t0) ∈ p(l2) -p n, pcf(t) = R1 → l3 = il, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → l3 = il ∧ ov = iv, pcf(t) = idle ∨ pcf(t) = ready ∨ pcf(t) = R1 ∨ pcf(t) = R4 ∨ pcf(t) = W1 ∨ pcf(t) = W5 → (∀ l4. ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = []), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → (∀ l4. ((h | l4) | t0) | false = []), pcf(t) = R2 → ctr(l3) = 0 → ((h | l3) | t0) | false = [], pcf(t) = W4 → ((h | l3) | t0) | false = (W(t0, l3, ov), false) ' ∨ ((h | l3) | t0) | false = [], pcf(t) = idle → apcf(t) = idle, pcf(t) = ready → apcf(t) = ready, pcf(t) = crashed → apcf(t) = crashed, pcf(t) = R1 → apcf(t) = invRead, pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → apcf(t) = resRead, pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 → apcf(t) = invWrite, pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → apcf(t) = resWrite, 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 = il0, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).v = ov0, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).l = il0 ∧ lsf(t0).v = iv0, pcf(t0) = idle ∨ pcf(t0) = ready ∨ pcf(t0) = R1 ∨ pcf(t0) = R4 ∨ pcf(t0) = W1 ∨ pcf(t0) = W5 → (∀ l. ¬ FO(lsf(t0).t) ∈ p(l) → ((h | l) | lsf(t0).t) | false = []), pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → (∀ l. ((h | l) | lsf(t0).t) | false = []), pcf(t0) = R2 ∨ pcf(t0) = R3 → (∀ l0. l0 ≠ lsf(t0).l ∧ ¬ FO(lsf(t0).t) ∈ p(l0) → ((h | l0) | lsf(t0).t) | false = []), pcf(t0) = R2 → ctr(lsf(t0).l) = 0 → ((h | lsf(t0).l) | lsf(t0).t) | false = [], pcf(t0) = W4 → ((h | lsf(t0).l) | lsf(t0).t) | false = (W(lsf(t0).t, lsf(t0).l, lsf(t0).v), false) ' ∨ ((h | lsf(t0).l) | lsf(t0).t) | false = [], ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ l4. l4 ≠ l3 ∧ ¬ FO(t0) ∈ p(l4) → ((h | l4) | t0) | false = [], ∀ t. lsf(t).t = t ∧ FLITPSCLInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t)), pcf(t) = R2 ∨ pcf(t) = R3 ⊦

Rule argument

Additional information

Used terms: mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf

Proof step 77 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

A spec-lemma

Proof step 78 from proof step-absstep-PSCPERSIST_FO-tau (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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