| # gs.ar ≠ 0 ∧ htok(gs.ar), # gs0.ar ≠ 0 ∧ htok(gs0.ar), lsf(tid) = ls, lsf0(tid) = ls0, alsf(tid) = als, alsf(tid).tid = tid, lsf(tid).tid = tid, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → alsf(tid0).tid = tid0, pcf(tid) = M5, pcf0(tid) = M18, apcf(tid) = apc, ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), false, SetLInv(ags, als, apc), ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), pre(gs, ls, M5, τ) ∧ gs0 = gstepf(gs, ls, M5, τ) ∧ ls0 = lstepf(gs, ls, M5, τ) ∧ M18 = pcstepf(gs, ls, M5, τ), absset(gs.ar, ags.set), ls.tid = als.tid ∧ apc = invMember ∧ (apc = invMember ∨ apc = invInsert → ls.e = als.le) ⊦ absset(gs0.ar, ags.set) ∧ ls0.tid = als.tid ∧ (apc = invMember ∨ apc = invInsert → ls0.e = als.le) |
ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, ls.tid = als.tid, lsf(tid).tid = tid, alsf(tid).tid = tid, M18 = pcstepf(gs, ls, M5, τ), alsf(tid) = als, apc = invMember, apcf(tid) = apc, gs0 = gstepf(gs, ls, M5, τ), ls0 = lstepf(gs, ls, M5, τ), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = M5, pcf0(tid) = M18, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls.e ≠ ⊥, ls.n < # gs.ar, ls.n0 < # gs.ar, SetLInv(ags, als, apc), absset(gs.ar, ags.set), allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs0.ar), htok(gs.ar), pre(gs, ls, M5, τ), ¬ ls.b, apc = invMember ∨ apc = invInsert → ls.e = als.le, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), ∀ tid0. tid0 ≠ tid → alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0, false ⊦ absset(gs0.ar, ags.set) ∧ ls0.tid = als.tid ∧ (apc = invMember ∨ apc = invInsert → ls0.e = als.le)
| ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, ls.tid = als.tid, lsf(tid).tid = tid, alsf(tid).tid = tid, M18 = pcstepf(gs, ls, M5, τ), alsf(tid) = als, apc = invMember, apcf(tid) = apc, gs0 = gstepf(gs, ls, M5, τ), ls0 = lstepf(gs, ls, M5, τ), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = M5, pcf0(tid) = M18, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls.e ≠ ⊥, ls.n < # gs.ar, ls.n0 < # gs.ar, SetLInv(ags, als, apc), absset(gs.ar, ags.set), allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs0.ar), htok(gs.ar), pre(gs, ls, M5, τ), ¬ ls.b, apc = invMember ∨ apc = invInsert → ls.e = als.le, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), ∀ tid0. tid0 ≠ tid → alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0, false ⊦ absset(gs0.ar, ags.set) ∧ ls0.tid = als.tid ∧ (apc = invMember ∨ apc = invInsert → ls0.e = als.le) |
The following image shows the proof tree of sequent calculus. The proved goal is at the bottom. You can click on the nodes to view additional rules. See here for details on colors in a proof tree.
