Proof step 1 from proof fliqtStep-lem (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ flitpscStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t. pre(gs, lsf(t), pcf(t), a) ∧ gs0 = gstepf(gs, lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(gs, lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(gs, lsf(t), pcf(t), a))) ∨ (∃ 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))

Rule argument

Additional information

Used simplifier rules: lstep: ⊦ 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);

Proof step 2 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers)

• Proof step 4:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers) ⊦ flitpscStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t. pre(gs, lsf(t), pcf(t), a) ∧ gs0 = gstepf(gs, lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(gs, lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(gs, lsf(t), pcf(t), a))) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = (gs.mem:= mem(l := p(l)[firstPersistW(p(l))].val)).p:= p(l := p(l) -p firstPersistW(p(l))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = gs.p:= p(l := p(l) -p n)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used terms: gs, mem, ctr, writers, readers, p

Proof step 3 from proof fliqtStep-lem (previous step) (back to tree)

Lemma elim-mkFLITPSCgs

Proof step 4 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ flitpscStep(mkstate(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a))) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotmem: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem:= mem0 = mkFLITPSCgs(mem0, p, ctr, writers, writers0); upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0);

Proof step 5 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 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))) ∧ ⟨p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ a = globalPSCCRASH ∧ ⟨p := gs.p, ctr := gs.ctr, writers := gs.writers, readers := gs.readers; PSCCRASH(; p, ctr, writers, readers, pcf); gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf)

• Proof step 7:

  a0 = a, gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), gs2 = gs0, lsf1 = lsf0, lsf2 = lsf, pcf1 = pcf0, pcf2 = pcf ⊦ (∃ t, ls, pc. lstep(gs1, lsf2(t), pcf2(t), a0, gs2, ls, pc) ∧ lsf1 = lsf2(t := ls) ∧ pcf1 = pcf2(t := pc)) ∨ (∃ l. a0 = globalPSCPERSIST_W(l) ∧ firstPersistW(gs1.p(l)) < # gs1.p(l) ∧ gs2 = (gs1.mem:= gs1.mem(l := gs1.p(l)[firstPersistW(gs1.p(l))].val)).p:= gs1.p(l := gs1.p(l) -p firstPersistW(gs1.p(l))) ∧ lsf1 = lsf2 ∧ pcf1 = pcf2) ∨ (∃ l. a0 = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, gs1.p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs2 = gs1 ∧ lsf1 = lsf2 ∧ pcf1 = pcf2)) ∨ a0 = globalPSCCRASH ∧ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs2 = gs1 ∧ lsf1 = lsf2 ∧ pcf1 = pcf2) ↔ (∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a))) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used terms: mkFLITPSCgs(mem, p, ctr, writers, readers), gs0, lsf0, a, pcf0, pcf, lsf

Proof step 6 from proof fliqtStep-lem (previous step) (back to tree)

Lemma flitpscStep

Proof step 7 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), pcf2 = pcf ⊦ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ a = globalPSCCRASH ∧ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf2) ↔ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a))

Rule argument

Additional information

Used simplifier rules: lstep: ⊦ 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); sel-mkFLITPSCgs-dotmem: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem = mem; upd-mkFLITPSCgs-dotmem: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem:= mem0 = mkFLITPSCgs(mem0, p, ctr, writers, writers0); upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); sel-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p;

Proof step 8 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 9:

  (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf)) ∨ a = globalPSCCRASH ∧ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf2), gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), pcf2 = pcf ⊦ ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

• Proof step 29:

  gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), pcf2 = pcf, (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ a = globalPSCCRASH ∧ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf2), ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf

Rule argument

Additional information

Proof step 9 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p(l)) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf2), gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), pcf2 = pcf ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 10 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 11:

  ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), a = globalPSCPERSIST_FO(l), gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), pcf2 = pcf, isPersistFO(n, p(l)) ⊦ ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

• Proof step 23:

  ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf2), a = globalPSCCRASH, gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), pcf2 = pcf ⊦ ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 11 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 12:

  ⟨PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), a = globalPSCPERSIST_FO(l), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = gs1.p, pcf2 = pcf, isPersistFO(n, p0(l)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a)), a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 12 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic split applied rule split left

And obtained the following new goals

• Proof step 13:

  ⟨gs1.p := p1⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ⟨PSCPERSIST_FO(l; p)⟩ (p = p1), a = globalPSCPERSIST_FO(l), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = gs1.p, pcf2 = pcf, isPersistFO(n, p0(l)) ⊦ ∃ t. pre(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 13 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 14:

  ⟨PSCPERSIST_FO(l; p)⟩ (p = p1), a = globalPSCPERSIST_FO(l), gs0 = gs1.p:= p1, gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf0 = lsf, p = gs1.p, pcf0 = pcf, pcf2 = pcf, isPersistFO(n, p0(l)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr, writers, readers)) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr, writers, readers), lsf(t), pcf(t), a)), a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 14 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ⟨PSCPERSIST_FO(l; p0)⟩ (p0 = p1), isPersistFO(n, p0(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p1 = p0(l := p0(l) -p n0)

Rule argument

Additional information

Used simplifier rules: sel-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; disj-globalPSCCRASH-globalPSCPERSISTuscFO: ⊦ globalPSCCRASH ≠ globalPSCPERSIST_FO(l); not-pre-global-tsync: ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_FO(l)); disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW: ⊦ globalPSCPERSIST_FO(l) ≠ globalPSCPERSIST_W(l0); inj-globalPSCPERSISTuscFO: ⊦ globalPSCPERSIST_FO(l) = globalPSCPERSIST_FO(l0) ↔ l = l0; upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;

Proof step 15 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic unfold applied rule call left

And obtained the following new goals

• Proof step 16:

  ⟨choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip⟩ (p = p1), p = p0, isPersistFO(n, p0(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p1 = p0(l := p0(l) -p n0)

Rule argument

Additional information

Used simplifier rules: PSCPERSIST_FO: ⊦ ;

Proof step 16 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 17:

  ⟨p(l) := p(l) -p n⟩ (p = p1), p = p0, isPersistFO(n1, p0(l)), isPersistFO(n, p(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p1 = p0(l := p0(l) -p n0)

• Proof step 20:

  ⟨skip⟩ (p = p1), p = p0, isPersistFO(n, p0(l)), ∀ n. ¬ isPersistFO(n, p(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p1 = p0(l := p0(l) -p n0)

Rule argument

Additional information

Proof step 17 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 18:

  p(l := p(l) -p n) = p1, p = p0, isPersistFO(n, p(l)), isPersistFO(n1, p0(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p1 = p0(l := p0(l) -p n0)

Rule argument

Additional information

Proof step 18 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  isPersistFO(n1, p0(l)), isPersistFO(n, p0(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p0(l := p0(l) -p n) = p0(l := p0(l) -p n0)

Rule argument

Additional information

Proof step 19 from proof fliqtStep-lem (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 20 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule skip left

And obtained the following new goals

• Proof step 21:

  p = p0, p = p1, isPersistFO(n, p0(l)), ∀ n. ¬ isPersistFO(n, p(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p1 = p0(l := p0(l) -p n0)

Rule argument

Additional information

Proof step 21 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  isPersistFO(n, p0(l)), ∀ n. ¬ isPersistFO(n, p0(l)) ⊦ ∃ n0. isPersistFO(n0, p0(l)) ∧ p0(l) = p0(l) -p n0

Rule argument

Additional information

Proof step 22 from proof fliqtStep-lem (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 23 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 24:

  ⟨PSCCRASH(; p, ctr, writers, readers, pcf2); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf2), a = globalPSCCRASH, ctr = gs1.ctr, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), p = gs1.p, pcf2 = pcf, readers = gs1.readers, writers = gs1.writers ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0)) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 24 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic split applied rule split left

And obtained the following new goals

• Proof step 25:

  ⟨gs1 := (((gs1.p:= p1).ctr:= ctr1).writers:= writers1).readers:= readers1⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf1), ⟨PSCCRASH(; p, ctr, writers, readers, pcf2)⟩ (p = p1 ∧ ctr = ctr1 ∧ writers = writers1 ∧ readers = readers1 ∧ pcf2 = pcf1), a = globalPSCCRASH, ctr = gs1.ctr, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), p = gs1.p, pcf2 = pcf, readers = gs1.readers, writers = gs1.writers ⊦ ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0)) ∧ lsf0 = lsf ∧ pcf0 = pcf, a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 25 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 26:

  ⟨PSCCRASH(; p, ctr, writers, readers, pcf2)⟩ (p = p1 ∧ ctr = ctr1 ∧ writers = writers1 ∧ readers = readers1 ∧ pcf2 = pcf1), a = globalPSCCRASH, ctr = gs1.ctr, gs0 = (((gs1.p:= p1).ctr:= ctr1).writers:= writers1).readers:= readers1, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf0 = lsf, p = gs1.p, pcf0 = pcf1, pcf2 = pcf, readers = gs1.readers, writers = gs1.writers ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0)) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 26 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  ⟨PSCCRASH(; p, ctr, writers, readers, pcf)⟩ (p = p1 ∧ ctr = ctr1 ∧ writers = writers1 ∧ readers = readers1 ∧ pcf = pcf1) ⊦ mkFLITPSCgs(mem, p1, ctr1, writers1, readers1) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: sel-mkFLITPSCgs-dotwriters: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers; sel-mkFLITPSCgs-dotreaders: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0; sel-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; sel-mkFLITPSCgs-dotctr: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); upd-mkFLITPSCgs-dotctr: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr:= ctr0 = mkFLITPSCgs(mem, p, ctr0, writers, writers0); upd-mkFLITPSCgs-dotwriters: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers:= writers1 = mkFLITPSCgs(mem, p, ctr, writers1, writers0); upd-mkFLITPSCgs-dotreaders: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers:= writers2 = mkFLITPSCgs(mem, p, ctr, writers, writers2); not-pre-global-crash: ⊦ ¬ pre(gs, ls, pc, globalPSCCRASH); disj-globalPSCCRASH-globalPSCPERSISTuscW: ⊦ globalPSCCRASH ≠ globalPSCPERSIST_W(l); disj-globalPSCCRASH-globalPSCPERSISTuscFO: ⊦ globalPSCCRASH ≠ globalPSCPERSIST_FO(l);

Proof step 27 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic unfold applied rule call left

And obtained the following new goals

• Proof step 28:

  ⟨pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), p := λ l. [], ctr := λ l. 0, readers := λ l. ∅, writers := λ l. ∅⟩ (p = p1 ∧ ctr = ctr1 ∧ writers = writers1 ∧ readers = readers1 ∧ pcf = pcf1) ⊦ mkFLITPSCgs(mem, p1, ctr1, writers1, readers1) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: PSCCRASH: ⊦ ;

Proof step 28 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign left

And closed the goal!

Rule argument

Additional information

Proof step 29 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ a = globalPSCCRASH ∧ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a))

Rule argument

Additional information

Proof step 30 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 31:

  gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), a ≠ globalPSCCRASH, a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf

• Proof step 51:

  gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p(l)) ∧ gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ⟨p := gs1.p, ctr := gs1.ctr, writers := gs1.writers, readers := gs1.readers; PSCCRASH(; p, ctr, writers, readers, pcf); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t. pre(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p, ctr, writers, readers), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p(l)) < # p(l) ∧ gs0 = mkFLITPSCgs(mem(l := p(l)[firstPersistW(p(l))].val), p(l := p(l) -p firstPersistW(p(l))), ctr, writers, readers) ∧ lsf0 = lsf ∧ pcf0 = pcf

Rule argument

Additional information

Proof step 31 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), isPersistFO(n, p(l)) ⊦ (∃ n. isPersistFO(n, p(l))) ∧ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Used simplifier rules: disj-globalPSCCRASH-globalPSCPERSISTuscFO: ⊦ globalPSCCRASH ≠ globalPSCPERSIST_FO(l); disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW: ⊦ globalPSCPERSIST_FO(l) ≠ globalPSCPERSIST_W(l0); not-pre-global-tsync: ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_FO(l)); inj-globalPSCPERSISTuscFO: ⊦ globalPSCPERSIST_FO(l) = globalPSCPERSIST_FO(l0) ↔ l = l0;

Proof step 32 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 33:

  gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), isPersistFO(n, p(l)) ⊦ ∃ n. isPersistFO(n, p(l))

• Proof step 35:

  gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p, ctr, writers, readers), isPersistFO(n, p(l)) ⊦ ⟨p := gs1.p; PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 33 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  isPersistFO(n, p(l)) ⊦ ∃ n. isPersistFO(n, p(l))

Rule argument

Additional information

Proof step 34 from proof fliqtStep-lem (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 fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 36:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = gs1.p, isPersistFO(n, p0(l)) ⊦ ⟨PSCPERSIST_FO(l; p); gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 36 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 37:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = gs1.p, isPersistFO(n, p0(l)) ⊦ ⟨choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Used simplifier rules: PSCPERSIST_FO: ⊦ ;

Proof step 37 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 38:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = gs1.p, isPersistFO(n0, p0(l)) ⊦ (∀ n. ¬ isPersistFO(n, p(l))) ∧ ⟨skip; gs1.p := p⟩ (gs0 = gs1), ∃ n. isPersistFO(n, p(l)) ∧ ⟨p(l) := p(l) -p n; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 38 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n0, p0(l)) ⊦ ¬ isPersistFO(n, p0(l)) ∧ ⟨skip; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Used simplifier rules: sel-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p;

Proof step 39 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 40:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n, p0(l)), isPersistFO(n0, p0(l)) ⊦ ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

• Proof step 44:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n0, p0(l)) ⊦ ⟨skip; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 40 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 41:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n0, p0(l)), isPersistFO(n, p0(l)) ⊦ isPersistFO(n0, p0(l)) ∧ ⟨p(l) := p(l) -p n0; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Used terms: n0

Proof step 41 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n0, p0(l)), isPersistFO(n, p0(l)) ⊦ ⟨p0(l) := p0(l) -p n0; gs1.p := p0⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 42 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 43:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n, p0(l)), isPersistFO(n0, p0(l)) ⊦ ⟨gs1.p := p0(l := p0(l) -p n0)⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 43 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;

Proof step 44 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 45:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, isPersistFO(n0, p0(l)) ⊦ ⟨gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 45 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 46:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, gs0 ≠ gs1.p:= p, isPersistFO(n0, p0(l)) ⊦ ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 46 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, p0(l) ≠ p0(l) -p n0, isPersistFO(n0, p0(l)) ⊦ ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;

Proof step 47 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 48:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, p0(l) ≠ p0(l) -p n0, isPersistFO(n0, p0(l)) ⊦ isPersistFO(n0, p0(l)) ∧ ⟨p(l) := p(l) -p n0; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Used terms: n0

Proof step 48 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, p0(l) ≠ p0(l) -p n0, isPersistFO(n0, p0(l)) ⊦ ⟨p0(l) := p0(l) -p n0; gs1.p := p0⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 49 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 50:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n0), ctr, writers, readers), gs1 = mkFLITPSCgs(mem, p0, ctr, writers, readers), p = p0, p0(l) ≠ p0(l) -p n0, isPersistFO(n0, p0(l)) ⊦ ⟨gs1.p := p0(l := p0(l) -p n0)⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p0(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1)

Rule argument

Additional information

Proof step 50 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;

Proof step 51 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 52:

  ctr = gs1.ctr, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), p = gs1.p, readers = gs1.readers, writers = gs1.writers, a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ⟨PSCCRASH(; p, ctr, writers, readers, pcf); gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a))

Rule argument

Additional information

Proof step 52 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ⟨PSCCRASH(; p0, ctr0, writers0, readers0, pcf); gs1 := (((gs1.p:= p0).ctr:= ctr0).writers:= writers0).readers:= readers0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a))

Rule argument

Additional information

Used simplifier rules: sel-mkFLITPSCgs-dotwriters: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers = writers; sel-mkFLITPSCgs-dotreaders: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0; sel-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; sel-mkFLITPSCgs-dotctr: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr;

Proof step 53 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 54:

  ctr = ctr0, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), p = p0, readers = readers0, writers = writers0, a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ⟨pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), p := λ l. [], ctr := λ l. 0, readers := λ l. ∅, writers := λ l. ∅; gs1 := (((gs1.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf

Rule argument

Additional information

Used simplifier rules: PSCCRASH: ⊦ ;

Proof step 54 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 55:

  ctr = ctr0, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), p = p0, readers = readers0, writers = writers0, a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ⟨gs1 := (((gs1.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))), ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a))

Rule argument

Additional information

Proof step 55 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 56:

  ctr = ctr0, gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), p = p0, readers = readers0, writers = writers0, a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, gs0 = (((gs1.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 56 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), a = globalPSCPERSIST_FO(l) ∧ isPersistFO(n, p0(l)) ∧ gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); upd-mkFLITPSCgs-dotctr: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr:= ctr0 = mkFLITPSCgs(mem, p, ctr0, writers, writers0); upd-mkFLITPSCgs-dotwriters: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).writers:= writers1 = mkFLITPSCgs(mem, p, ctr, writers1, writers0); upd-mkFLITPSCgs-dotreaders: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers:= writers2 = mkFLITPSCgs(mem, p, ctr, writers, writers2);

Proof step 57 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 58:

  a = globalPSCPERSIST_FO(l), gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf0 = lsf, pcf0 = pcf, isPersistFO(n, p0(l)) ⊦ ∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1 ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t. pre(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ gs0 = gstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a) ∧ lsf0 = lsf(t := lstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)) ∧ pcf0 = pcf(t := pcstepf(mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), lsf(t), pcf(t), a)), ∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(p0(l)) < # p0(l) ∧ gs0 = mkFLITPSCgs(mem(l := p0(l)[firstPersistW(p0(l))].val), p0(l := p0(l) -p firstPersistW(p0(l))), ctr0, writers0, readers0) ∧ lsf0 = lsf ∧ pcf0 = pcf, gs0 = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 58 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), isPersistFO(n, p0(l)) ⊦ (∃ n. isPersistFO(n, p0(l))) ∧ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1), mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW: ⊦ globalPSCPERSIST_FO(l) ≠ globalPSCPERSIST_W(l0); not-pre-global-tsync: ⊦ ¬ pre(gs, ls, pc, globalPSCPERSIST_FO(l)); inj-globalPSCPERSISTuscFO: ⊦ globalPSCPERSIST_FO(l) = globalPSCPERSIST_FO(l0) ↔ l = l0;

Proof step 59 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 60:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), isPersistFO(n, p0(l)) ⊦ ∃ n. isPersistFO(n, p0(l)), mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

• Proof step 62:

  gs0 = mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p0, ctr0, writers0, readers0), isPersistFO(n, p0(l)) ⊦ ⟨p0 := gs1.p; PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1), mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 60 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  isPersistFO(n, p0(l)) ⊦ ∃ n. isPersistFO(n, p0(l)), mkFLITPSCgs(mem, p0(l := p0(l) -p n), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 61 from proof fliqtStep-lem (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 62 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 63:

  gs0 = mkFLITPSCgs(mem, p(l := p(l) -p n), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p, ctr0, writers0, readers0), p0 = gs1.p, isPersistFO(n, p(l)) ⊦ ⟨PSCPERSIST_FO(l; p0); gs1.p := p0⟩ (gs0 = gs1), mkFLITPSCgs(mem, p(l := p(l) -p n), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 63 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 64:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p0, p0 = gs1.p, isPersistFO(n, p1(l)) ⊦ ⟨choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: PSCPERSIST_FO: ⊦ ;

Proof step 64 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 65:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p0, p0 = gs1.p, isPersistFO(n0, p1(l)) ⊦ (∀ n. ¬ isPersistFO(n, p(l))) ∧ ⟨skip; gs1.p := p⟩ (gs0 = gs1), ∃ n. isPersistFO(n, p(l)) ∧ ⟨p(l) := p(l) -p n; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 65 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n0, p1(l)) ⊦ ¬ isPersistFO(n, p1(l)) ∧ ⟨skip; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: sel-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p;

Proof step 66 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 67:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n, p1(l)), isPersistFO(n0, p1(l)) ⊦ ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

• Proof step 71:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n0, p1(l)) ⊦ ⟨skip; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 67 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 68:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n0, p1(l)), isPersistFO(n, p1(l)) ⊦ isPersistFO(n0, p1(l)) ∧ ⟨p(l) := p(l) -p n0; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used terms: n0

Proof step 68 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n0, p1(l)), isPersistFO(n, p1(l)) ⊦ ⟨p1(l) := p1(l) -p n0; gs1.p := p1⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 69 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 70:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n, p1(l)), isPersistFO(n0, p1(l)) ⊦ ⟨gs1.p := p1(l := p1(l) -p n0)⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 70 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;

Proof step 71 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 72:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, isPersistFO(n0, p1(l)) ⊦ ⟨gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 72 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 73:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, gs0 ≠ gs1.p:= p, isPersistFO(n0, p1(l)) ⊦ ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 73 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, p1(l) ≠ p1(l) -p n0, isPersistFO(n0, p1(l)) ⊦ ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;

Proof step 74 from proof fliqtStep-lem (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 75:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, p1(l) ≠ p1(l) -p n0, isPersistFO(n0, p1(l)) ⊦ isPersistFO(n0, p1(l)) ∧ ⟨p(l) := p(l) -p n0; gs1.p := p⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Used terms: n0

Proof step 75 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, p1(l) ≠ p1(l) -p n0, isPersistFO(n0, p1(l)) ⊦ ⟨p1(l) := p1(l) -p n0; gs1.p := p1⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 76 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 77:

  gs0 = mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0), gs1 = mkFLITPSCgs(mem, p1, ctr0, writers0, readers0), p = p1, p1(l) ≠ p1(l) -p n0, isPersistFO(n0, p1(l)) ⊦ ⟨gs1.p := p1(l := p1(l) -p n0)⟩ (gs0 = gs1), ∃ n1. isPersistFO(n1, p1(l)) ∧ ⟨p(l) := p(l) -p n1; gs1.p := p⟩ (gs0 = gs1), mkFLITPSCgs(mem, p1(l := p1(l) -p n0), ctr0, writers0, readers0) = mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ pcf(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 77 from proof fliqtStep-lem (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: upd-mkFLITPSCgs-dotp: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p:= p0 = mkFLITPSCgs(mem, p0, ctr, writers, writers0); inj-mkFLITPSCgs: ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0) = mkFLITPSCgs(mem0, p0, ctr0, writers1, writers2) ↔ mem = mem0 ∧ p = p0 ∧ ctr = ctr0 ∧ writers = writers1 ∧ writers0 = writers2;