Proof step 1 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)), flitStep(mkstate(gs, lsf, pcf), globalPERSIST_FO(loc), mkstate(gs0, lsf0, pcf0)) ⊦ ∃ ags0, alsf0, apcf0. flitpscStep(mkstate(ags, alsf, apcf), globalPSCPERSIST_FO(loc), mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0))

Rule argument

Additional information

Proof step 2 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (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, ags.writers = gs.fwriters, FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), flitStep(mkstate(gs, lsf, pcf), globalPERSIST_FO(loc), mkstate(gs0, lsf0, pcf0)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, 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.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters; ⊦ 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-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ flitStep(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)) ∨ (∃ tid. a = doWrite(tid, gs.bq(tid).head.l, gs.bq(tid).head.v) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W?) ∧ gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ tid, l. a = (oneMember(tid, l, gs.fwriters) ⊃ doWriteFO(tid, l);propFO(tid, l)) ∧ (∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid))) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ (∃ tid. a = propSF(tid) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l))) ∧ gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc. a = globalPERSIST_W(loc) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.W?) ∧ gs0 = (gs.pmem:= gs.pmem(loc := gs.pq(loc).head.val)).pq:= gs.pq(loc := gs.pq(loc).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc. a = globalPERSIST_FO(loc) ∧ (gs.pq(loc) ≠ [] ∧ gs.pq(loc).head.FO?) ∧ gs0 = gs.pq:= gs.pq(loc := gs.pq(loc).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalCRASH ∧ ⟨pq := gs.pq, fctr := gs.fctr, bq := gs.bq, fwriters := gs.fwriters, freaders := gs.freaders, rfo := gs.rfo; CRASH(; pq, fctr, bq, fwriters, freaders, rfo, pcf); gs := (((((gs.pq:= pq).fctr:= fctr).bq:= bq).fwriters:= fwriters).freaders:= freaders).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)

• Proof step 5:

  (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalPERSIST_FO(loc), gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ (∃ tid. globalPERSIST_FO(loc) = doWrite(tid, gs.bq(tid).head.l, gs.bq(tid).head.v) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head.W?) ∧ gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ tid, l. globalPERSIST_FO(loc) = (oneMember(tid, l, gs.fwriters) ⊃ doWriteFO(tid, l);propFO(tid, l)) ∧ (∃ n. n < # gs.bq(tid) ∧ isPropFO(n, l, gs.bq(tid))) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(tid, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ (∃ tid. globalPERSIST_FO(loc) = propSF(tid) ∧ (gs.bq(tid) ≠ [] ∧ gs.bq(tid).head = SF ∧ (∀ l. ¬ FO(tid) ∈ gs.pq(l))) ∧ gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc0. globalPERSIST_FO(loc) = globalPERSIST_W(loc0) ∧ (gs.pq(loc0) ≠ [] ∧ gs.pq(loc0).head.W?) ∧ gs0 = (gs.pmem:= gs.pmem(loc0 := gs.pq(loc0).head.val)).pq:= gs.pq(loc0 := gs.pq(loc0).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ loc0. globalPERSIST_FO(loc) = globalPERSIST_FO(loc0) ∧ (gs.pq(loc0) ≠ [] ∧ gs.pq(loc0).head.FO?) ∧ gs0 = gs.pq:= gs.pq(loc0 := gs.pq(loc0).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ globalPERSIST_FO(loc) = globalCRASH ∧ ⟨pq := gs.pq, fctr := gs.fctr, bq := gs.bq, fwriters := gs.fwriters, freaders := gs.freaders, rfo := gs.rfo; CRASH(; pq, fctr, bq, fwriters, freaders, rfo, pcf); gs := (((((gs.pq:= pq).fctr:= fctr).bq:= bq).fwriters:= fwriters).freaders:= freaders).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used terms: pcf0, globalPERSIST_FO(loc), lsf, gs0, pcf, lsf0, gs

Proof step 4 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)) ∧ n < # gs.bq(t) ∧ isPropFO(n, l, gs.bq(t)) ∧ ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(t, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ loc = loc0 ∧ gs.pq(loc0) ≠ [] ∧ gs.pq(loc0).head.FO? ∧ gs0 = gs.pq:= gs.pq(loc0 := gs.pq(loc0).tail) ∧ lsf0 = lsf ∧ pcf0 = pcf, ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: ⊦ globalCRASH ≠ globalPERSIST_FO(loc); (s) ⊦ globalPERSIST_FO(loc) = globalPERSIST_FO(loc0) ↔ loc = loc0; (s) ⊦ globalPERSIST_FO(loc) ≠ globalPERSIST_W(loc0); (s) ⊦ globalPERSIST_FO(loc) ≠ propSF(t); (s) ⊦ doWrite(t, loc, v) ≠ globalPERSIST_FO(loc0); (s) ⊦ ¬ pre(gs, ls, pc, globalPERSIST_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)

Proof step 6 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(t, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), n < # gs.bq(t), FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

• Proof step 22:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, gs0 = gs.pq:= gs.pq(loc0 := gs.pq(loc0).tail), loc = loc0, lsf0 = lsf, pcf0 = pcf, gs.pq(loc0) ≠ [], gs.pq(loc0).head.FO?, FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 7 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ⟨fwriters := gs.fwriters, pq := gs.pq, bq := gs.bq, rfo := gs.rfo; PROP_FO(t, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 8 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 9:

  ⟨PROP_FO(t, l, fwriters; pq, bq, rfo); gs := ((gs.pq:= pq).bq:= bq).rfo:= rfo⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 9 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic split applied rule split left

And obtained the following new goals

• Proof step 10:

  ⟨gs := ((gs.pq:= pq0).bq:= bq0).rfo:= rfo0⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ⟨PROP_FO(t, l, fwriters; pq, bq, rfo)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs0, lsf0, pcf0), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 10 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 11:

  ⟨PROP_FO(t, l, fwriters; pq, bq, rfo)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), gs0 = ((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf0 = lsf, pcf0 = pcf, pq = gs.pq, rfo = gs.rfo, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs, lsf, pcf), FLITInv(gs0, lsf0, pcf0), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters ∧ (∀ t. labs(gs0, lsf0(t), pcf0(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 11 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ⟨PROP_FO(t, l, gs.fwriters; pq, bq, rfo)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, pq0, rfo0) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.rfo:= bq0).fwriters = gs.fwriters; (s) ⊦ (gs.rfo:= bq0).rfo = bq0; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ (gs.rfo:= bq0).pq = gs.pq; (s) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ (gs.rfo:= bq0).fctr = gs.fctr; (s) ⊦ (gs.pq:= pq).pmem = gs.pmem; (s) ⊦ (gs.bq:= bq).pmem = gs.pmem; (s) ⊦ (gs.rfo:= bq0).pmem = gs.pmem; (s)

Proof step 12 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic unfold applied rule call left

And obtained the following new goals

• Proof step 13:

  ⟨choose n with n < # bq(tid) ∧ isPropFO(n, l, bq(tid)) in pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n) ifnone skip⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, tid = t, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, pq0, rfo0) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: decl: PROP_FO(tid, l, fwriters; pq, bq, rfo) {choose n with n < # bq(tid) ∧ isPropFO(n, l, bq(tid)) in pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n) ifnone skip };

Proof step 13 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 14:

  ⟨pq(l) := pq(l) + FO(tid), bq(tid) := bq(tid) -p n, rfo(tid) := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n)⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, tid = t, gs.bq(t) ≠ [], n0 < # gs.bq(t), n < # bq(tid), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n0, l, gs.bq(t)), isPropFO(n, l, bq(tid)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, pq0, rfo0) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

• Proof step 19:

  ⟨skip⟩ (pq = pq0 ∧ bq = bq0 ∧ rfo = rfo0), ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, tid = t, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)), ∀ n. ¬(n < # bq(tid) ∧ isPropFO(n, l, bq(tid))) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, pq0, rfo0) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 14 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 15:

  pq(l := pq(l) + FO(tid)) = pq0, bq(tid := bq(tid) -p n) = bq0, rfo(tid := (tid ∈ fwriters(l) ⊃ rfo(tid);rfo(tid) -p n)) = rfo0, ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, rfo = gs.rfo, tid = t, gs.bq(t) ≠ [], n < # bq(tid), n0 < # gs.bq(t), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, bq(tid)), isPropFO(n0, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, pq0, rfo0) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 15 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), gs.bq(t) ≠ [], n0 < # gs.bq(t), n < # gs.bq(t), FLITInv(gs, lsf, pcf), FLITInv (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t) ')).bq:= gs.bq(t := gs.bq(t) -p n)).rfo:= gs.rfo(t := (t ∈ gs.fwriters(l) ⊃ gs.rfo(t);gs.rfo(t) -p n)), lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n0, l, gs.bq(t)), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(l := gs.pq(l) + FO(t) '), gs.rfo(t := (t ∈ gs.fwriters(l) ⊃ gs.rfo(t);gs.rfo(t) -p n))) ∧ ags0.writers = gs.fwriters ∧ (∀ t0. labs (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t) ')).bq:= gs.bq(t := gs.bq(t) -p n)).rfo:= gs.rfo(t := (t ∈ gs.fwriters(l) ⊃ gs.rfo(t);gs.rfo(t) -p n)), lsf(t0), pcf(t0), ags0, alsf(t0), apcf(t0)))

Rule argument

Additional information

Used simplifier rules: ⊦ x + a = x + a '; (s)

Proof step 16 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), gs.bq(t) ≠ [], n < # gs.bq(t), n0 < # gs.bq(t), FLITInv (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t) ')).bq:= gs.bq(t := gs.bq(t) -p n)).rfo:= gs.rfo(t := (t ∈ gs.fwriters(l) ⊃ gs.rfo(t);gs.rfo(t) -p n)), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), isPropFO(n0, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), t ∈ gs.fwriters(l), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(l := gs.pq(l) + FO(t) '), gs.rfo(t := (t ∈ gs.fwriters(l) ⊃ gs.rfo(t);gs.rfo(t) -p n))) ∧ ags0.writers = gs.fwriters ∧ (∀ t0. labs (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t) ')).bq:= gs.bq(t := gs.bq(t) -p n)).rfo:= gs.rfo(t := (t ∈ gs.fwriters(l) ⊃ gs.rfo(t);gs.rfo(t) -p n)), lsf(t0), pcf(t0), ags0, alsf(t0), apcf(t0)))

Rule argument

Additional information

Used simplifier rules: ⊦ oneMember(t, l, tsf) → (t ∈ tsf(l0) ↔ l = l0); (s) ⊦ globalPERSIST_FO(loc) ≠ propFO(t, loc0); (s) Used formulas: t ∈ gs.fwriters(l)

Proof step 17 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), # gs.fwriters(l) ≠ 0, gs.bq(t) ≠ [], gs.fwriters(l) ≠ ∅, n < # gs.bq(t), n0 < # gs.bq(t), FLITInv(((gs.pq:= gs.pq(l := gs.pq(l) + FO(t) ')).bq:= gs.bq(t := gs.bq(t) -p n)).rfo:= gs.rfo(t := gs.rfo(t)), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), isPropFO(n0, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), t ∈ gs.fwriters(l), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(l := gs.pq(l) + FO(t) '), gs.rfo(t := gs.rfo(t))) ∧ ags0.writers = gs.fwriters ∧ (∀ t0. labs (((gs.pq:= gs.pq(l := gs.pq(l) + FO(t) ')).bq:= gs.bq(t := gs.bq(t) -p n)).rfo:= gs.rfo(t := gs.rfo(t)), lsf(t0), pcf(t0), ags0, alsf(t0), apcf(t0)))

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 18 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ globalPERSIST_FO(loc) ≠ propFO(t, loc0); (s) ⊦ doWriteFO(t, loc) ≠ globalPERSIST_FO(loc0); (s) Used formulas: oneMember(t, l, gs.fwriters)

Proof step 19 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule skip left

And obtained the following new goals

• Proof step 20:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, bq = gs.bq, bq = bq0, fwriters = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), pq = gs.pq, pq = pq0, rfo = gs.rfo, rfo = rfo0, tid = t, gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ n. ¬(n < # bq(tid) ∧ isPropFO(n, l, bq(tid))), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, pq0, rfo0) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= pq0).bq:= bq0).rfo:= rfo0, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 20 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, ags.writers = gs.fwriters, globalPERSIST_FO(loc) = (oneMember(t, l, gs.fwriters) ⊃ doWriteFO(t, l);propFO(t, l)), gs.bq(t) ≠ [], n < # gs.bq(t), FLITInv(gs, lsf, pcf), FLITInv(((gs.pq:= gs.pq).bq:= gs.bq).rfo:= gs.rfo, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPropFO(n, l, gs.bq(t)), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)), ∀ n0. ¬ n0 < # gs.bq(t) ∨ ¬ isPropFO(n0, l, gs.bq(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc)) ∧ ags0 = ags.p:= ags.p(loc := ags.p(loc) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq, gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(((gs.pq:= gs.pq).bq:= gs.bq).rfo:= gs.rfo, lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 21 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 22 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (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, ags.writers = gs.fwriters, gs.pq(loc0) ≠ [], gs.pq(loc0).head.FO?, FLITInv(gs, lsf, pcf), FLITInv(gs.pq:= gs.pq(loc0 := gs.pq(loc0).tail), lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := gs.pq(loc0).tail), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := gs.pq(loc0).tail), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.pq:= pq).rfo = gs.rfo; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.pq:= pq).pmem = gs.pmem; (s)

Proof step 23 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = fow + fowl, ags.writers = gs.fwriters, gs.pq(loc0) ≠ [], fow.FO?, FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := fowl), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.pq(loc0), fow, fowl

Proof step 24 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = fow ' + fowl, ags.writers = gs.fwriters, fow.FO?, FLITInv(gs, lsf, pcf), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := fowl), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 25 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ fow.FO? ↔ (∃ tid. fow = FO(tid))

• Proof step 27:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = fow ' + fowl, ags.writers = gs.fwriters, FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)), ∃ tid. fow = FO(tid) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := fowl), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used terms: fow

Proof step 26 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, FLITInv(gs, lsf, pcf), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := fowl), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 28 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 29:

  ⊦ reorder(p, pq, rfo) ∧ pq(l) = FO(t) ' + fowl1 → (∃ n. isPersistFO(n, p(l)) ∧ p(l)[n] = FO(t))

• Proof step 30:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), reorder(ags.p, gs.pq, gs.rfo) ∧ gs.pq(loc0) = FO(t) ' + fowl → (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags.p(loc0)[n] = FO(t)), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := fowl), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Used terms: loc0, gs.rfo, t, gs.pq, fowl, ags.p

Proof step 29 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, ags.p(loc0)[n] = FO(t), FLITInv(gs, lsf, pcf), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPersistFO(n, ags.p(loc0)), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ ags0. (∃ n. isPersistFO(n, ags.p(loc0)) ∧ ags0 = ags.p:= ags.p(loc0 := ags.p(loc0) -p n)) ∧ ags0.mem = gs.pmem ∧ ags0.ctr = gs.fctr ∧ reorder(ags0.p, gs.pq(loc0 := fowl), gs.rfo) ∧ ags0.writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags0, alsf(t), apcf(t)))

Rule argument

Additional information

Proof step 31 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 32:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, ags.p(loc0)[n] = FO(t), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPersistFO(n, ags.p(loc0)), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ (∃ n0. isPersistFO(n0, ags.p(loc0)) ∧ ags.p:= ags.p(loc0 := ags.p(loc0) -p n) = ags.p:= ags.p(loc0 := ags.p(loc0) -p n0)) ∧ (ags.p:= ags.p(loc0 := ags.p(loc0) -p n)).mem = gs.pmem ∧ (ags.p:= ags.p(loc0 := ags.p(loc0) -p n)).ctr = gs.fctr ∧ reorder((ags.p:= ags.p(loc0 := ags.p(loc0) -p n)).p, gs.pq(loc0 := fowl), gs.rfo) ∧ (ags.p:= ags.p(loc0 := ags.p(loc0) -p n)).writers = gs.fwriters ∧ (∀ t. labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t), pcf(t), ags.p:= ags.p(loc0 := ags.p(loc0) -p n), alsf(t), apcf(t)))

Rule argument

Additional information

Used terms: ags.p:= ags.p(loc0 := ags.p(loc0) -p n)

Proof step 32 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, ags.p(loc0)[n] = FO(t), FLITInv(gs, lsf, pcf), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPersistFO(n, ags.p(loc0)), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ (∃ n0. isPersistFO(n0, ags.p(loc0)) ∧ ags.p:= ags.p(loc0 := ags.p(loc0) -p n) = ags.p:= ags.p(loc0 := ags.p(loc0) -p n0)) ∧ labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t0), pcf(t0), ags.p:= ags.p(loc0 := ags.p(loc0) -p n), alsf(t0), apcf(t0))

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ reorder(p, pq, rfo) ∧ pq(l) = FO(t) ' + fowl ∧ isPersistFO(n, p(l)) ∧ p(l)[n] = FO(t) → reorder(p(l := p(l) -p n), pq(l := fowl), rfo); (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (gs.p:= p).p = p; (s) ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ (gs.p:= p).mem = gs.mem; (s)

Proof step 33 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 34:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, ags.p(loc0)[n] = FO(t), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPersistFO(n, ags.p(loc0)), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ ∃ n0. isPersistFO(n0, ags.p(loc0)) ∧ ags.p:= ags.p(loc0 := ags.p(loc0) -p n) = ags.p:= ags.p(loc0 := ags.p(loc0) -p n0)

• Proof step 35:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, ags.p(loc0)[n] = FO(t), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITInv(gs, lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPersistFO(n, ags.p(loc0)), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ¬ labs(gs.pq:= gs.pq(loc0 := fowl), lsf(t0), pcf(t0), ags.p:= ags.p(loc0 := ags.p(loc0) -p n), alsf(t0), apcf(t0)), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 34 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 35 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  ags.ctr = gs.fctr, ags.mem = gs.pmem, gs.pq(loc0) = FO(t) ' + fowl, ags.writers = gs.fwriters, ags.p(loc0)[n] = FO(t), FLITInv(gs, lsf, pcf), FLITInv(gs.pq:= gs.pq(loc0 := fowl), lsf, pcf), FLITPSCInv(ags, alsf, apcf), isPersistFO(n, ags.p(loc0)), reorder(ags.p, gs.pq, gs.rfo), FO(t) ∈ gs.pq(loc0), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v)

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 = R1) ∧ (pc = R2 → apc = R2) ∧ (pc = R3 → apc = R3) ∧ (pc = R4 → apc = R4) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.loc = als.l) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.val = als.v) ∧ (pc = W1 → apc = W1) ∧ (pc = W2 → apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2)) ∧ (pc = W3 → apc = W3) ∧ (pc = W4 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4)) ∧ ( pc = W5 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5))) ∧ ( pc = W6 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3 ;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6)) )) ∧ (pc = W7 → apc = W7) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.loc = als.l) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.val = als.v); ⊦ (gs.pq:= pq).bq = gs.bq; (s)

Proof step 36 from proof step-absstep-PERSIST_FO-globalPERSIST_FO (previous step) (back to tree)

User applied rule all left

And closed the goal!

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 = R1) ∧ (pc = R2 → apc = R2) ∧ (pc = R3 → apc = R3) ∧ (pc = R4 → apc = R4) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.loc = als.l) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.val = als.v) ∧ (pc = W1 → apc = W1) ∧ (pc = W2 → apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2)) ∧ (pc = W3 → apc = W3) ∧ (pc = W4 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;W4)) ∧ ( pc = W5 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;W5))) ∧ ( pc = W6 → apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3 ;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6)) )) ∧ (pc = W7 → apc = W7) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.loc = als.l) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.val = als.v); Used terms: t0