This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| sel-ARetMember-dottid | ⊦ ARetMember(tid, b).tid = tid | An Axiom |
| updsel--dotpcf-dotpcf | ⊦ (s.pcf:= pcf).pcf = pcf | An Axiom |
| gen-SetAction | SetAction freely generated by τ, ADoInsert, ADoMember, AInvInsert, AInvMember, ARetInsert, ARetMember; | An Axiom |
| pcstepf-idle-INVINSERT | ⊦ ls.tid = tid → pcstepf(gs, ls, idle, AInvInsert(tid, e)) = invInsert | An Axiom |
| updsel--dotlsf-dotpcf | ⊦ (s.lsf:= lsf).pcf = s.pcf | An Axiom |
| gen-SetState | SetState freely generated by mkstate; | An Axiom |
| case-SetPC | ⊦ pc = idle ∨ pc = invInsert ∨ pc = invMember ∨ pc = retInsert ∨ pc = retMember | An Axiom |
| disj-idle-retInsert | ⊦ idle ≠ retInsert | An Axiom |
| disj-ADoMember-ARetInsert | ⊦ ADoMember(tid) ≠ ARetInsert(tid0, b) | An Axiom |
| updsel--dotlb-dotle | ⊦ (ls.lb:= lb).le = ls.le | An Axiom |
| upd-mkstate-dotlsf | ⊦ (mkstate(gstate, lsf, pcf).lsf:= lsf0) = mkstate(gstate, lsf0, pcf) | An Axiom |
| disj-AInvInsert-AInvMember | ⊦ AInvInsert(tid, e) ≠ AInvMember(tid0, e0) | An Axiom |
| pre-retInsert | ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)) | An Axiom |
| disj-invInsert-invMember | ⊦ invInsert ≠ invMember | An Axiom |
| disj-ADoInsert-ARetMember | ⊦ ADoInsert(tid, b) ≠ ARetMember(tid0, b0) | An Axiom |
| disj-ADoInsert-ADoMember | ⊦ ADoInsert(tid, b) ≠ ADoMember(tid0) | An Axiom |
| disj-ADoInsert-ARetInsert | ⊦ ADoInsert(tid, b) ≠ ARetInsert(tid0, b0) | An Axiom |
| updsel--dotle-dotle | ⊦ (ls.le:= le).le = le | An Axiom |
| upd-mkls-dotlb | ⊦ mkls(tid, le, lb).lb:= lb0 = mkls(tid, le, lb0) | An Axiom |
| updsel--dotlb-dotlb | ⊦ (ls.lb:= lb).lb ↔ lb | An Axiom |
| sel-mkstate-dotgstate | ⊦ mkstate(gstate, lsf, pcf).gstate = gstate | An Axiom |
| upd-mkls-dottid | ⊦ mkls(tid, le, lb).tid:= tid0 = mkls(tid0, le, lb) | An Axiom |
| sel-AInvMember-dote | ⊦ AInvMember(tid, e).e = e | An Axiom |
| updsel--dotle-dotlb | ⊦ (ls.le:= le).lb ↔ ls.lb | An Axiom |
| gstepf-invMember-DOMEMBER | ⊦ ls.tid = tid → gstepf(gs, ls, invMember, ADoMember(tid)) = gs | An Axiom |
| pcstepf-invMember-DOMEMBER | ⊦ ls.tid = tid → pcstepf(gs, ls, invMember, ADoMember(tid)) = retMember | An Axiom |
| upd-mkls-dotle | ⊦ mkls(tid, le, lb).le:= le0 = mkls(tid, le0, lb) | An Axiom |
| disj-ARetInsert-ARetMember | ⊦ ARetInsert(tid, b) ≠ ARetMember(tid0, b0) | An Axiom |
| updsel--dotset-dotset | ⊦ (gs.set:= set).set = set | An Axiom |
| setInit | ⊦ setInit(mkstate(gs, lsf, pcf)) ↔ (gs.set = ∅ ∧ pcf = (λ tid. idle)) ∧ (∀ tid. lsf(tid).tid = tid) | An Axiom |
| inj-ARetInsert | ⊦ ARetInsert(tid, b) = ARetInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| sel-mkgs-dotset | ⊦ mkgs(set).set = set | An Axiom |
| disj-AInvMember-ARetMember | ⊦ AInvMember(tid, e) ≠ ARetMember(tid0, b) | An Axiom |
| sel-AInvMember-dottid | ⊦ AInvMember(tid, e).tid = tid | An Axiom |
| disj-retInsert-retMember | ⊦ retInsert ≠ retMember | An Axiom |
| elim-mkstate | ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf) | An Axiom |
| pre-idle | ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥) | An Axiom |
| sel-ARetMember-dotb | ⊦ ARetMember(tid, b).b ↔ b | An Axiom |
| inj-ARetMember | ⊦ ARetMember(tid, b) = ARetMember(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| upd-mkgs-dotset | ⊦ mkgs(set).set:= set0 = mkgs(set0) | An Axiom |
| case-SetLState | ⊦ mkls(ls.tid, ls.le, ls.lb) = ls | An Axiom |
| sel-mkstate-dotlsf | ⊦ mkstate(gstate, lsf, pcf).lsf = lsf | An Axiom |
| 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) | An Axiom |
| updsel--dotgstate-dotlsf | ⊦ (s.gstate:= gstate).lsf = s.lsf | An Axiom |
| sel-ADoInsert-dottid | ⊦ ADoInsert(tid, b).tid = tid | An Axiom |
| SetLInv | ⊦ SetLInv(gs, ls, pc) ↔ (pc = invInsert ∨ pc = retInsert ∨ pc = invMember ∨ pc = retMember → ls.le ≠ ⊥) ∧ (pc = retMember ∨ pc = retInsert → ls.lb → ls.le ∈ gs.set) | An Axiom |
| inj-ADoMember | ⊦ ADoMember(tid) = ADoMember(tid0) ↔ tid = tid0 | An Axiom |
| case-SetGState | ⊦ mkgs(gs.set) = gs | An Axiom |
| updsel--dotlb-dottid | ⊦ (ls.lb:= lb).tid = ls.tid | An Axiom |
| SetInv | ⊦ SetInv(gs, lsf, pcf) ↔ SetGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ SetLInv(gs, lsf(tid), pcf(tid))) | An Axiom |
| updsel--dotlsf-dotlsf | ⊦ (s.lsf:= lsf).lsf = lsf | An Axiom |
| disj-ADoMember-AInvMember | ⊦ ADoMember(tid) ≠ AInvMember(tid0, e) | An Axiom |
| disj-ADoMember-AInvInsert | ⊦ ADoMember(tid) ≠ AInvInsert(tid0, e) | An Axiom |
| disj-idle-invInsert | ⊦ idle ≠ invInsert | An Axiom |
| disj-idle-invMember | ⊦ idle ≠ invMember | An Axiom |
| sel-ARetInsert-dottid | ⊦ ARetInsert(tid, b).tid = tid | An Axiom |
| disj-AInvMember-ARetInsert | ⊦ AInvMember(tid, e) ≠ ARetInsert(tid0, b) | An Axiom |
| updsel--dotgstate-dotgstate | ⊦ (s.gstate:= gstate).gstate = gstate | An Axiom |
| disj-ADoInsert-AInvMember | ⊦ ADoInsert(tid, b) ≠ AInvMember(tid0, e) | An Axiom |
| gstepf-retInsert-RETINSERT | ⊦ ls.tid = tid → gstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = gs | An Axiom |
| pre-invMember | ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid) | An Axiom |
| SetRely | ⊦ SetRely(gs, tid, gs0) ↔ gs.set ⊆ gs0.set | An Axiom |
| lstepf-retMember-RETMEMBER | ⊦ ls.tid = tid → lstepf(gs, ls, retMember, ARetMember(tid, b0)) = ls | An Axiom |
| disj-invInsert-retMember | ⊦ invInsert ≠ retMember | An Axiom |
| disj-AInvInsert-ARetMember | ⊦ AInvInsert(tid, e) ≠ ARetMember(tid0, b) | An Axiom |
| lstepf-invInsert-DOINSERT | ⊦ ls.tid = tid → lstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ ls.lb:= true;ls.lb:= false) | An Axiom |
| lstepf-retInsert-RETINSERT | ⊦ ls.tid = tid → lstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = ls | An Axiom |
| pcstepf-retMember-RETMEMBER | ⊦ ls.tid = tid → pcstepf(gs, ls, retMember, ARetMember(tid, b0)) = idle | An Axiom |
| inj-mkstate | ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0 | An Axiom |
| gstepf-retMember-RETMEMBER | ⊦ ls.tid = tid → gstepf(gs, ls, retMember, ARetMember(tid, b0)) = gs | An Axiom |
| updsel--dotpcf-dotgstate | ⊦ (s.pcf:= pcf).gstate = s.gstate | An Axiom |
| inj-ADoInsert | ⊦ ADoInsert(tid, b) = ADoInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| updsel--dotpcf-dotlsf | ⊦ (s.pcf:= pcf).lsf = s.lsf | An Axiom |
| pcstepf-retInsert-RETINSERT | ⊦ ls.tid = tid → pcstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = idle | An Axiom |
| pre-invInsert | ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)) | An Axiom |
| sel-AInvInsert-dote | ⊦ AInvInsert(tid, e).e = e | An Axiom |
| case-SetAction | ⊦ a = ADoInsert(a.tid, a.b) ∨ a = ADoMember(a.tid) ∨ a = AInvInsert(a.tid, a.e) ∨ a = AInvMember(a.tid, a.e) ∨ a = ARetInsert(a.tid, a.b) ∨ a = ARetMember(a.tid, a.b) ∨ a = τ | An Axiom |
| gstepf-idle | ⊦ gstepf(gs, ls, idle, a) = gs | An Axiom |
| disj-ADoInsert-AInvInsert | ⊦ ADoInsert(tid, b) ≠ AInvInsert(tid0, e) | An Axiom |
| disj-ARetInsert-tau | ⊦ ARetInsert(tid, b) ≠ τ | An Axiom |
| inj-AInvMember | ⊦ AInvMember(tid, e) = AInvMember(tid0, e0) ↔ tid = tid0 ∧ e = e0 | An Axiom |
| disj-ARetMember-tau | ⊦ ARetMember(tid, b) ≠ τ | An Axiom |
| updsel--dottid-dotlb | ⊦ (ls.tid:= tid).lb ↔ ls.lb | An Axiom |
| sel-AInvInsert-dottid | ⊦ AInvInsert(tid, e).tid = tid | An Axiom |
| disj-invInsert-retInsert | ⊦ invInsert ≠ retInsert | An Axiom |
| updsel--dottid-dotle | ⊦ (ls.tid:= tid).le = ls.le | An Axiom |
| upd-mkstate-dotpcf | ⊦ (mkstate(gstate, lsf, pcf).pcf:= pcf0) = mkstate(gstate, lsf, pcf0) | An Axiom |
| disj-ADoMember-tau | ⊦ ADoMember(tid) ≠ τ | An Axiom |
| disj-ADoInsert-tau | ⊦ ADoInsert(tid, b) ≠ τ | An Axiom |
| elim-mkgs | ⊦ set = gs.set ↔ gs = mkgs(set) | An Axiom |
| disj-AInvInsert-ARetInsert | ⊦ AInvInsert(tid, e) ≠ ARetInsert(tid0, b) | An Axiom |
| gen-SetLState | SetLState freely generated by mkls; | An Axiom |
| lstepf-idle-INVMEMBER | ⊦ ls.tid = tid → lstepf(gs, ls, idle, AInvMember(tid, e)) = ls.le:= e | An Axiom |
| sel-ADoInsert-dotb | ⊦ ADoInsert(tid, b).b ↔ b | An Axiom |
| gen-SetGState | SetGState freely generated by mkgs; | An Axiom |
| case-SetState | ⊦ mkstate(s.gstate, s.lsf, s.pcf) = s | An Axiom |
| lstepf-invMember-DOMEMBER | ⊦ ls.tid = tid → lstepf(gs, ls, invMember, ADoMember(tid)) = ls.lb:= (ls.le ∈ gs.set) | An Axiom |
| pcstepf-invInsert-DOINSERT | ⊦ ls.tid = tid → pcstepf(gs, ls, invInsert, ADoInsert(tid, b)) = retInsert | An Axiom |
| sel-mkstate-dotpcf | ⊦ mkstate(gstate, lsf, pcf).pcf = pcf | An Axiom |
| updsel--dotlsf-dotgstate | ⊦ (s.lsf:= lsf).gstate = s.gstate | An Axiom |
| upd-mkstate-dotgstate | ⊦ (mkstate(gstate, lsf, pcf).gstate:= gstate0) = mkstate(gstate0, lsf, pcf) | An Axiom |
| disj-AInvInsert-tau | ⊦ AInvInsert(tid, e) ≠ τ | An Axiom |
| sel-mkls-dotlb | ⊦ mkls(tid, le, lb).lb ↔ lb | An Axiom |
| disj-AInvMember-tau | ⊦ AInvMember(tid, e) ≠ τ | An Axiom |
| SetGInv | ⊦ SetGInv(gs) ↔ true | An Axiom |
| inj-mkgs | ⊦ mkgs(set) = mkgs(set0) ↔ set = set0 | An Axiom |
| inj-AInvInsert | ⊦ AInvInsert(tid, e) = AInvInsert(tid0, e0) ↔ tid = tid0 ∧ e = e0 | An Axiom |
| disj-idle-retMember | ⊦ idle ≠ retMember | An Axiom |
| disj-ADoMember-ARetMember | ⊦ ADoMember(tid) ≠ ARetMember(tid0, b) | An Axiom |
| updsel--dotle-dottid | ⊦ (ls.le:= le).tid = ls.tid | An Axiom |
| pcstepf-idle-INVMEMBER | ⊦ ls.tid = tid → pcstepf(gs, ls, idle, AInvMember(tid, e)) = invMember | An Axiom |
| disj-invMember-retInsert | ⊦ invMember ≠ retInsert | An Axiom |
| disj-invMember-retMember | ⊦ invMember ≠ retMember | An Axiom |
| lstepf-idle-INVINSERT | ⊦ ls.tid = tid → lstepf(gs, ls, idle, AInvInsert(tid, e)) = ls.le:= e | An Axiom |
| gen-SetPC | SetPC freely generated by idle, invInsert, invMember, retInsert, retMember; | An Axiom |
| pre-retMember | ⊦ pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb)) | An Axiom |
| setStep | ⊦ setStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ tid, ls, pc. lstep(gs, lsf(tid), pcf(tid), a, gs0, ls, pc) ∧ lsf0 = lsf(tid := ls) ∧ pcf0 = pcf(tid := pc)) | An Axiom |
| sel-ADoMember-dottid | ⊦ ADoMember(tid).tid = tid | An Axiom |
| sel-ARetInsert-dotb | ⊦ ARetInsert(tid, b).b ↔ b | An Axiom |
| sel-mkls-dotle | ⊦ mkls(tid, le, lb).le = le | An Axiom |
| inj-mkls | ⊦ mkls(tid, le, lb) = mkls(tid0, le0, lb0) ↔ tid = tid0 ∧ le = le0 ∧ (lb ↔ lb0) | An Axiom |
| sel-mkls-dottid | ⊦ mkls(tid, le, lb).tid = tid | An Axiom |
| gstepf-invInsert-DOINSERT | ⊦ ls.tid = tid → gstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ gs.set:= (gs.set ++ ls.le);gs) | An Axiom |
| elim-mkls | ⊦ (tid = ls.tid ∧ le = ls.le) ∧ (lb ↔ ls.lb) ↔ ls = mkls(tid, le, lb) | An Axiom |
| updsel--dottid-dottid | ⊦ (ls.tid:= tid).tid = tid | An Axiom |
| updsel--dotgstate-dotpcf | ⊦ (s.gstate:= gstate).pcf = s.pcf | An Axiom |