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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pcstepf(gs, ls, W6, a) = W7, ctrok(gs.ctr, gs.writers), noPending(ls.t, gs.p), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), pre(gs, ls, W6, a), writersOk(gs.p, gs.writers) ⊦ ( ctrok(gstepf(gs, ls, W6, a).ctr, gstepf(gs, ls, W6, a).writers) ∧ writersOk(gstepf(gs, ls, W6, a).p, gstepf(gs, ls, W6, a).writers) ∧ pendingOk(gstepf(gs, ls, W6, a).p)) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).readers) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).writers) ∧ noPending(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).p)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ctrok(gs.ctr, gs.writers), noPending(ls.t, gs.p), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ ctrok(gs.ctr(ls.l := gs.ctr(ls.l) - 1), gs.writers(ls.l := gs.writers(ls.l) -- ls.t)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.ctr:= ctr).p = gs.p; (s) ⊦ (gs.writers:= writers).p = gs.p; (s) ⊦ gstepf(gs, ls, W6, a) = (gs.ctr:= gs.ctr(ls.l := gs.ctr(ls.l) - 1)) .writers:= gs.writers(ls.l := gs.writers(ls.l) -- ls.t); (s) ⊦ lstepf(gs, ls, W6, a) = ls; (s) ⊦ oneMember(t, l, tsf) → notMember(t, tsf(l := tsf(l) -- t)); (ss) ⊦ (gs.writers:= writers).writers = writers; (s) ⊦ (gs.ctr:= ctr).readers = gs.readers; (s) ⊦ (gs.writers:= writers).readers = gs.readers; (s) ⊦ writersOk(p, writers) ∧ oneMember(t, l, writers) ∧ noPending(t, p) → writersOk(p, writers(l := writers(l) -- t)); (ss) ⊦ (gs.ctr:= ctr).ctr = ctr; (s) ⊦ (gs.writers:= writers).ctr = gs.ctr; (s) ⊦ pre(gs, ls, W6, a) ↔ a = ctrDecPSC(ls.t, ls.l); (s) ⊦ pcstepf(gs, ls, W6, a) = W7; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers), ctrok(ctr, writers), noPending(ls.t, p), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), pendingOk(p), writersOk(p, writers), ¬ ctrok(ctr(ls.l := ctr(ls.l) - 1), writers(ls.l := writers(ls.l) -- ls.t)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ctrok(ctr, writers), noPending(ls.t, p), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), pendingOk(p), writersOk(p, writers), ¬ ctrok(ctr(ls.l := ctr(ls.l) - 1), writers(ls.l := writers(ls.l) -- ls.t)) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  ls = mkFLITPSCls(t, l, v), ctrok(ctr, writers), noPending(t, p), notMember(t, readers), oneMember(t, l, writers), pendingOk(p), writersOk(p, writers), ¬ ctrok(ctr(l := ctr(l) - 1), writers(l := writers(l) -- t)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ctrok(ctr, writers), noPending(t, p), notMember(t, readers), oneMember(t, l, writers), pendingOk(p), writersOk(p, writers), ¬ ctrok(ctr(l := ctr(l) - 1), writers(l := writers(l) -- t)) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ctrok(ctr, writers) ∧ oneMember(t, l, writers) ∧ ctr(l) = n + 1 → ctrok(ctr(l := n), writers(l := writers(l) -- t)); (ss) ⊦ oneMember(t, l, writers) ∧ ctrok(ctr, writers) → ctr(l) ≠ 0; (as) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: ctr(l), n0