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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∃ n. isPersistFO(n, gs.p(l)) ⊦ ⟪p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 4:

  p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪PSCPERSIST_FO(l; p); gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

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

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 5:

  p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip; gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

Used simplifier rules: decl: PSCPERSIST_FO(l; p){choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip};

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

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 6:

  p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, p(l)), isPersistFO(n0, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪p(l) := p(l) -p n; gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

• Proof step 8:

  p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ n. ¬ isPersistFO(n, p(l)) ⊦ ⟪skip; gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 7:

  p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n0, gs.p(l)), isPersistFO(n, p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪gs.p := p(l := p(l) -p n)⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ writersOk(p, writers) → writersOk(p(l := p(l) -p n), writers); (ss) ⊦ (gs.p:= p).p = p; (s) ⊦ pendingOk(p) → pendingOk(p(l := p(l) -p n)); (ss)

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

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 9:

  p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ n. ¬ isPersistFO(n, p(l)) ⊦ ⟪gs.p := p⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ (gs.p:= p).p = p; (s)