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: |
|---|---|---|
| disj-InvInsert-InvMember | ⊦ InvInsert(tid, e) ≠ InvMember(tid0, e0) | An Axiom |
| ext-DoInsert | ⊦ setExt(ADoInsert(tid, b)) = τ | An Axiom |
| insert-inset-after-retinsert | frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + (al + ARetInsert(tid, true))), SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), ¬ tid ∈ setExt !(al).map(.tid) ⊦ e ∈ sl.last.gstate.set | A User Theorem |
| frag-retMem | # sl = # al + 2, SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al + ARetMember(tid, b) ') ⊦ (∃ n. n < # al ∧ al[n] = ADoMember(tid) ∧ (b ↔ sl[n].lsf(tid).le ∈ sl[n].gstate.set) ∧ sl[n].pcf(tid) = invMember ∧ (∀ m. n < m ∧ m < # al → al[m] ≠ τ ∧ al[m].tid ≠ tid)) ∨ (b ↔ sl.head.lsf(tid).lb) ∧ sl.head.pcf(tid) = retMember ∧ (∀ m. m < # al → al[m] ≠ τ ∧ al[m].tid ≠ tid) | A User Theorem |
| gen | EAction freely generated by InvInsert, InvMember, RetInsert, RetMember; | An Axiom |
| inj-RetInsert | ⊦ RetInsert(tid, b) = RetInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| insert-inset-after-retinsert-ind | frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al), SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), ¬ tid ∈ setExt !(al).map(.tid) ⊦ sl.last.pcf(tid) = invInsert ∧ sl.last.lsf(tid).le = e ∨ sl.last.pcf(tid) = retInsert ∧ (sl.last.lsf(tid).lb → e ∈ sl.last.gstate.set) | A User Theorem |
| frag-retIns | # sl = # al + 2, SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al + ARetInsert(tid, b) ') ⊦ (∃ n. n < # al ∧ al[n] = ADoInsert(tid, b) ∧ (b ↔ sl.last.lsf(tid).lb) ∧ sl[n].pcf(tid) = invInsert ∧ (∀ m. n < m ∧ m < # al → al[m] ≠ τ ∧ al[m].tid ≠ tid)) ∨ (b ↔ sl.head.lsf(tid).lb) ∧ (b ↔ sl.last.lsf(tid).lb) ∧ sl.head.pcf(tid) = retInsert ∧ (∀ m. m < # al → al[m] ≠ τ ∧ al[m].tid ≠ tid) | A User Theorem |
| sel-InvMember-dote | ⊦ InvMember(tid, e).e = e | An Axiom |
| disj-RetInsert-RetMember | ⊦ RetInsert(tid, b) ≠ RetMember(tid0, b0) | An Axiom |
| frag-rely-inv | SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al) ⊦ sl.head.gstate.set ⊆ sl.last.gstate.set ∧ SetInv(sl.last.gstate, sl.last.lsf, sl.last.pcf) | A User Theorem |
| sel-InvMember-dottid | ⊦ InvMember(tid, e).tid = tid | An Axiom |
| sel-RetMember-dotb | ⊦ RetMember(tid, b).b ↔ b | An Axiom |
| SetIOA-def | ⊦ SetIOA = IOAut(setInit, setStep, setExt) | An Axiom |
| inj-InvMember | ⊦ InvMember(tid, e) = InvMember(tid0, e0) ↔ tid = tid0 ∧ e = e0 | An Axiom |
| frag-in | SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al) ⊦ e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al ∧ al[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert) | A User Theorem |
| sel-RetInsert-dottid | ⊦ RetInsert(tid, b).tid = tid | An Axiom |
| frag-subset | SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al) ⊦ sl.head.gstate.set ⊆ sl.last.gstate.set | A User Theorem |
| case-EAction | ⊦ ea = InvInsert(ea.tid, ea.e) ∨ ea = InvMember(ea.tid, ea.e) ∨ ea = RetInsert(ea.tid, ea.b) ∨ ea = RetMember(ea.tid, ea.b) | An Axiom |
| ext-RetMember | ⊦ setExt(ARetMember(tid, b)) = ⌜RetMember(tid, b)⌝ | An Axiom |
| inj-InvInsert | ⊦ InvInsert(tid, e) = InvInsert(tid0, e0) ↔ tid = tid0 ∧ e = e0 | An Axiom |
| ext-RetInsert | ⊦ setExt(ARetInsert(tid, b)) = ⌜RetInsert(tid, b)⌝ | An Axiom |
| theorem-allinserts-finished-false-implies-notin | exec*(IOAut(setInit, setStep, setExt))(sl, al), ∀ tid, al1, al2. al = al1 + (AInvInsert(tid, e) + al2) → (∃ al3, al4. al2 = al3 + (ARetInsert(tid, false) + al4) ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦ ¬ e ∈ sl.last.gstate.set | A User Theorem |
| disj-InvInsert-RetMember | ⊦ InvInsert(tid, e) ≠ RetMember(tid0, b) | An Axiom |
| sel-InvInsert-dote | ⊦ InvInsert(tid, e).e = e | An Axiom |
| frag-DoIns | # sl = # al + 2, SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al + ADoInsert(tid, b) ') ⊦ (∃ n. n < # al ∧ al[n] = AInvInsert(tid, sl.last.lsf(tid).le) ∧ sl[n].pcf(tid) = idle ∧ (∀ m. n < m ∧ m < # al → al[m] ≠ τ ∧ al[m].tid ≠ tid)) ∨ sl.last.lsf(tid).le = sl.head.lsf(tid).le ∧ sl.head.pcf(tid) = invInsert ∧ (∀ m. m < # al → al[m] ≠ τ ∧ al[m].tid ≠ tid) | A User Theorem |
| sel-InvInsert-dottid | ⊦ InvInsert(tid, e).tid = tid | An Axiom |
| theorem-member-returns-true-after-insert | exec*(IOAut(setInit, setStep, setExt)) (sl, al + (AInvInsert(tid, e) + (al0 + (ARetInsert(tid, true) + (al1 + (AInvMember(tid0, e) + (al2 + ARetMember(tid0, b)))))))), ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid0 ∈ setExt !(al2).map(.tid) ⊦ b | A User Theorem |
| disj-InvMember-RetMember | ⊦ InvMember(tid, e) ≠ RetMember(tid0, b) | An Axiom |
| ext-InvMember | ⊦ setExt(AInvMember(tid, e)) = ⌜InvMember(tid, e)⌝ | An Axiom |
| allinserts-finished-false-implies-notin-ind | exec*(IOAut(setInit, setStep, setExt))(sl, al), n < # sl, ∀ tid, al1, al2. al = al1 + (AInvInsert(tid, e) + al2) → (∃ al3, al4. al2 = al3 + (ARetInsert(tid, false) + al4) ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦ ¬ e ∈ sl[n].gstate.set ∧ (sl[n].pcf(tid) = retInsert ∧ sl[n].lsf(tid).le = e → ¬ sl[n].lsf(tid).lb) | A User Theorem |
| disj-InvInsert-RetInsert | ⊦ InvInsert(tid, e) ≠ RetInsert(tid0, b) | An Axiom |
| inset-member-returns-true-ind | e ∈ sl.head.gstate.set, SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvMember(tid0, e) + al0), ¬ tid0 ∈ setExt !(al0).map(.tid) ⊦ sl.last.pcf(tid0) = invMember ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retMember ∧ sl.last.lsf(tid0).lb | A User Theorem |
| ext-DoMember | ⊦ setExt(ADoMember(tid)) = τ | An Axiom |
| inset-member-returns-true | e ∈ sl.head.gstate.set, SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvMember(tid0, e) + (al0 + ARetMember(tid0, b))), ¬ tid0 ∈ setExt !(al0).map(.tid) ⊦ b | A User Theorem |
| sel-RetInsert-dotb | ⊦ RetInsert(tid, b).b ↔ b | An Axiom |
| inv-tid | ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid | A User Theorem |
| disj-InvMember-RetInsert | ⊦ InvMember(tid, e) ≠ RetInsert(tid0, b) | An Axiom |
| inj-RetMember | ⊦ RetMember(tid, b) = RetMember(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| ext-InvInsert | ⊦ setExt(AInvInsert(tid, e)) = ⌜InvInsert(tid, e)⌝ | An Axiom |
| sel-RetMember-dottid | ⊦ RetMember(tid, b).tid = tid | An Axiom |