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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs0.rfo(t) = gs0.bq(t), gs.rfo(t) = gs.bq(t), ls.t = als.t, lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, W1 = pcstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)), alsf(t) = als, apc = ready, apcf(t) = apc, gs0 = gstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)), ls0 = lstepf(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = ready, pcf0(t) = W1, FLITPSCLInv(ags, als, apc), SFTrailing(gs0.bq), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(ags.ctr, ags.writers), ctrok(gs0.fctr, gs0.fwriters), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs0.bq, gs0.pq), noPendingW(t, gs.bq, gs.pq), notMember(t, gs0.freaders), notMember(t, gs0.fwriters), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), pre(gs, ls, ready, invFLITWRITE(ls.t, loc0, val0)), readFOsOk(gs0.rfo, gs0.fwriters), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, ags.writers), writersOk(gs0.bq, gs0.pq, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ¬ SF ∈ gs0.bq(t), pre(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) → ags0 = gstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ als0 = lstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ apc0 = pcstepf(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. t0 ≠ t → alsf(t0).t = t0, ∀ t0. t0 ≠ t → lsf(t0).t = t0 ⊦ pre(ags, als, apc, invFLITPSCWRITE(ls.t, loc0, val0)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = W1 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq, gs.rfo) ∧ ags0.writers = gs.fwriters ∧ lsf0(t).t = als0.t ∧ apc0 = W1 ∧ lsf0(t).loc = als0.l ∧ lsf0(t).val = als0.v

Rule argument

Additional information

Used simplifier rules: ⊦ callPSCCOMPLETE(t) ≠ invFLITPSCWRITE(t0, l, v); (s) ⊦ invFLITPSCREAD(t, l) ≠ invFLITPSCWRITE(t0, l0, v); (s) ⊦ pre(gs, ls, ready, a) ↔ (∃ l0, v0. a = invFLITPSCWRITE(ls.t, l0, v0)) ∨ (∃ l0. a = invFLITPSCREAD(ls.t, l0)) ∨ a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)); (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = W1; (s) ⊦ ls.t = t → lstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = (ls.l:= l0).v:= v0; (s) ⊦ gstepf(gs, ls, ready, a) = gs; (s) ⊦ gstepf(gs, ls, ready, a) = gs; (s) ⊦ invFLITWRITE(t, loc, v) = invFLITWRITE(t0, loc0, v0) ↔ t = t0 ∧ loc = loc0 ∧ v = v0; (ws) ⊦ callFLITCOMPLETE(t) ≠ invFLITWRITE(t0, loc, v); (s) ⊦ invFLITREAD(t, loc) ≠ invFLITWRITE(t0, loc0, v); (s) ⊦ pre(gs, ls, ready, a) ↔ (∃ loc0, val0. a = invFLITWRITE(ls.t, loc0, val0)) ∨ (∃ loc0. a = invFLITREAD(ls.t, loc0)) ∨ a = callFLITCOMPLETE(ls.t) ∧ gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l)); (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITWRITE(t, loc0, val0)) = W1; (s) ⊦ ls.t = t → lstepf(gs, ls, ready, invFLITWRITE(t, loc0, val0)) = (ls.loc:= loc0).val:= val0; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

• Proof step 6:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, ags0.mem ≠ gs.pmem, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 8:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, ags0.ctr ≠ gs.fctr, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 10:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ reorder(ags0.p, gs.pq, gs.rfo), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 12:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, ags0.writers ≠ gs.fwriters, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 14:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).t ≠ als0.t, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 18:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, apc0 ≠ W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 20:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).loc ≠ als0.l, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

• Proof step 24:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).val ≠ als0.v, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), ctrok(ags0.ctr, ags0.writers), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), pendingOk(ags0.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), writersOk(ags0.p, ags0.writers), ¬ SF ∈ gs.bq(t), (∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)) → ags0 = ags ∧ als0 = (alsf(t).l:= loc0).v:= val0 ∧ apc0 = W1, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, ags0.mem ≠ gs.pmem, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, ags0.ctr ≠ gs.fctr, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ reorder(ags0.p, gs.pq, gs.rfo), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, ags0.writers ≠ gs.fwriters, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).t ≠ als0.t, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

• Proof step 16:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, ags0 = ags, als0 = (alsf(t).l:= loc0).v:= val0, apc0 = W1, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).t ≠ als0.t, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).t ≠ t, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

Rule argument

Additional information

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

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

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.val:= val).t = ls.t; (s) ⊦ (ls.loc:= loc).t = ls.t; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, apc0 ≠ W1, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

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

User applied rule case distinction

And obtained the following new goals

• Proof step 21:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).loc ≠ als0.l, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

• Proof step 22:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, ags0 = ags, als0 = (alsf(t).l:= loc0).v:= val0, apc0 = W1, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).loc ≠ als0.l, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

Proof step 22 from proof step-absstep-ready-W1-invFLITWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).loc ≠ loc0, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.l:= l).l = l; (s) ⊦ (ls.v:= v).l = ls.l; (s)

Proof step 23 from proof step-absstep-ready-W1-invFLITWRITE-same (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.val:= val).loc = ls.loc; (s) ⊦ (ls.loc:= loc).loc = loc; (s)

Proof step 24 from proof step-absstep-ready-W1-invFLITWRITE-same (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 25:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).val ≠ als0.v, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦ ∃ l0, v0. invFLITPSCWRITE(t, loc0, val0) = invFLITPSCWRITE(t, l0, v0)

• Proof step 26:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, ags0 = ags, als0 = (alsf(t).l:= loc0).v:= val0, apc0 = W1, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).val ≠ als0.v, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)) ⊦

Rule argument

Additional information

Proof step 25 from proof step-absstep-ready-W1-invFLITWRITE-same (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: loc0, val0

Proof step 26 from proof step-absstep-ready-W1-invFLITWRITE-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), alsf(t).t = t, lsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = ready, lsf0(t) = (lsf(t).loc:= loc0).val:= val0, pcf(t) = ready, pcf0(t) = W1, lsf0(t).val ≠ val0, FLITPSCLInv(ags, alsf(t), ready), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.freaders), notMember(t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(ags.p), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), ∀ t0. lsf(t0).t = t0, ∀ t0. alsf(t0).t = t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.v:= v).v = v; (s)

Proof step 27 from proof step-absstep-ready-W1-invFLITWRITE-same (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.val:= val).val = val; (s)