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-M4-M18 | ⊦ M4 ≠ M18 | An Axiom |
| pcstepf-M17 | ⊦ pcstepf(gs, ls, M17, a) = M5 | An Axiom |
| disj-I2-M7 | ⊦ I2 ≠ M7 | An Axiom |
| pcstepf-I4 | ⊦ pcstepf(gs, ls, I4, a) = I5 | An Axiom |
| disj-I10-M13 | ⊦ I10 ≠ M13 | An Axiom |
| gstepf-M14 | ⊦ gstepf(gs, ls, M14, τ) = gs | An Axiom |
| disj-I7-M18 | ⊦ I7 ≠ M18 | An Axiom |
| updsel--dotpcf-dotpcf | ⊦ (s.pcf:= pcf).pcf = pcf | An Axiom |
| disj-M8-M15 | ⊦ M8 ≠ M15 | An Axiom |
| disj-I3-M12 | ⊦ I3 ≠ M12 | An Axiom |
| disj-I17-M2 | ⊦ I17 ≠ M2 | An Axiom |
| updsel--dote0-dotsz | ⊦ (ls.e0:= e0).sz = ls.sz | An Axiom |
| gstepf-I4 | ⊦ gstepf(gs, ls, I4, τ) = gs | An Axiom |
| disj-M2-M4 | ⊦ M2 ≠ M4 | An Axiom |
| updsel--dottid-dotsz | ⊦ (ls.tid:= tid).sz = ls.sz | An Axiom |
| disj-doMEMBER-tau | ⊦ doMEMBER(tid) ≠ τ | An Axiom |
| disj-I6-M7 | ⊦ I6 ≠ M7 | An Axiom |
| disj-M12-M17 | ⊦ M12 ≠ M17 | An Axiom |
| disj-I15-I18 | ⊦ I15 ≠ I18 | An Axiom |
| disj-I19-I21 | ⊦ I19 ≠ I21 | An Axiom |
| disj-I8-M13 | ⊦ I8 ≠ M13 | An Axiom |
| disj-M9-M10 | ⊦ M9 ≠ M10 | An Axiom |
| disj-I11-I12 | ⊦ I11 ≠ I12 | An Axiom |
| disj-I2-I12 | ⊦ I2 ≠ I12 | An Axiom |
| disj-I19-M11 | ⊦ I19 ≠ M11 | An Axiom |
| updsel--dotlsf-dotpcf | ⊦ (s.lsf:= lsf).pcf = s.pcf | An Axiom |
| lstepf-M12 | ⊦ ls.tid = tid → lstepf(gs, ls, M12, retMEMBER(tid, ls.b)) = ls | An Axiom |
| disj-I13-M2 | ⊦ I13 ≠ M2 | An Axiom |
| updsel--dotn-dotn0 | ⊦ (ls.n:= sz1).n0 = ls.n0 | An Axiom |
| disj-I21-M6 | ⊦ I21 ≠ M6 | An Axiom |
| updsel--dote-dote0 | ⊦ (ls.e:= e).e0 = ls.e0 | An Axiom |
| upd-mkgs-dotar | ⊦ mkgs(ar).ar:= ar0 = mkgs(ar0) | An Axiom |
| disj-I3-I16 | ⊦ I3 ≠ I16 | An Axiom |
| disj-M11-M13 | ⊦ M11 ≠ M13 | An Axiom |
| disj-I7-I13 | ⊦ I7 ≠ I13 | An Axiom |
| pcstepf-I12 | ⊦ pcstepf(gs, ls, I12, a) = I13 | An Axiom |
| disj-I16-M18 | ⊦ I16 ≠ M18 | An Axiom |
| disj-I8-M7 | ⊦ I8 ≠ M7 | An Axiom |
| disj-I18-idle | ⊦ I18 ≠ idle | An Axiom |
| lstepf-M3 | ⊦ lstepf(gs, ls, M3, τ) = ls.n:= ls.n0 | An Axiom |
| pre-I7 | ⊦ pre(gs, ls, I7, a) ↔ a = τ | An Axiom |
| sel-retINSERT-dotretINSERTb | ⊦ retINSERT(tid, b).retINSERTb ↔ b | An Axiom |
| disj-I10-I17 | ⊦ I10 ≠ I17 | An Axiom |
| disj-I4-I11 | ⊦ I4 ≠ I11 | An Axiom |
| disj-I14-M10 | ⊦ I14 ≠ M10 | An Axiom |
| disj-I11-M2 | ⊦ I11 ≠ M2 | An Axiom |
| disj-I15-M2 | ⊦ I15 ≠ M2 | An Axiom |
| lstepf-I16 | ⊦ lstepf(gs, ls, I16, τ) = ls.n:= ((ls.n + 1) % ls.sz) | An Axiom |
| disj-I4-M7 | ⊦ I4 ≠ M7 | An Axiom |
| disj-I6-M14 | ⊦ I6 ≠ M14 | An Axiom |
| disj-M7-M11 | ⊦ M7 ≠ M11 | An Axiom |
| disj-I8-I17 | ⊦ I8 ≠ I17 | An Axiom |
| disj-I11-M17 | ⊦ I11 ≠ M17 | An Axiom |
| sel-retINSERT-dottid | ⊦ retINSERT(tid, b).tid = tid | An Axiom |
| disj-I2-M17 | ⊦ I2 ≠ M17 | An Axiom |
| disj-I8-idle | ⊦ I8 ≠ idle | An Axiom |
| disj-M3-M14 | ⊦ M3 ≠ M14 | An Axiom |
| disj-I19-M2 | ⊦ I19 ≠ M2 | An Axiom |
| HashsetInv | ⊦ HashsetInv(gs, lsf, pcf) ↔ HashsetGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), pcf(tid))) | An Axiom |
| disj-M17-M18 | ⊦ M17 ≠ M18 | An Axiom |
| disj-I14-I20 | ⊦ I14 ≠ I20 | An Axiom |
| disj-I15-M14 | ⊦ I15 ≠ M14 | An Axiom |
| lstepf-M15 | ⊦ lstepf(gs, ls, M15, τ) = ls.b:= false | An Axiom |
| disj-I16-M9 | ⊦ I16 ≠ M9 | An Axiom |
| disj-I8-I11 | ⊦ I8 ≠ I11 | An Axiom |
| disj-I6-M17 | ⊦ I6 ≠ M17 | An Axiom |
| disj-I5-M13 | ⊦ I5 ≠ M13 | An Axiom |
| disj-M3-M17 | ⊦ M3 ≠ M17 | An Axiom |
| upd-mkstate-dotlsf | ⊦ (mkstate(gstate, lsf, pcf).lsf:= lsf0) = mkstate(gstate, lsf0, pcf) | An Axiom |
| disj-I9-M5 | ⊦ I9 ≠ M5 | An Axiom |
| disj-I2-M11 | ⊦ I2 ≠ M11 | An Axiom |
| lstepf-I19-b | ⊦ ls.tid = tid ∧ ¬ ls.b → lstepf(gs, ls, I19, retINSERT(tid, false)) = ls | A User Theorem |
| lstepf-I10 | ⊦ lstepf(gs, ls, I10, τ) = ls | An Axiom |
| disj-I19-M14 | ⊦ I19 ≠ M14 | An Axiom |
| disj-I13-M5 | ⊦ I13 ≠ M5 | An Axiom |
| disj-I15-M17 | ⊦ I15 ≠ M17 | An Axiom |
| disj-M6-M7 | ⊦ M6 ≠ M7 | An Axiom |
| disj-I4-I8 | ⊦ I4 ≠ I8 | An Axiom |
| pcstepf-M11 | ⊦ pcstepf(gs, ls, M11, a) = M12 | An Axiom |
| disj-I20-M4 | ⊦ I20 ≠ M4 | An Axiom |
| pre-M2 | ⊦ pre(gs, ls, M2, a) ↔ a = τ | An Axiom |
| disj-I2-M1 | ⊦ I2 ≠ M1 | An Axiom |
| disj-I14-M9 | ⊦ I14 ≠ M9 | An Axiom |
| updsel--dottid-dotb | ⊦ (ls.tid:= tid).b ↔ ls.b | An Axiom |
| disj-I18-M9 | ⊦ I18 ≠ M9 | An Axiom |
| disj-M11-M16 | ⊦ M11 ≠ M16 | An Axiom |
| disj-doINSERT-retINSERT | ⊦ doINSERT(tid, b) ≠ retINSERT(tid0, b0) | An Axiom |
| disj-I18-I20 | ⊦ I18 ≠ I20 | An Axiom |
| disj-I7-M12 | ⊦ I7 ≠ M12 | An Axiom |
| disj-I7-M5 | ⊦ I7 ≠ M5 | An Axiom |
| disj-I2-I21 | ⊦ I2 ≠ I21 | An Axiom |
| disj-M8-M18 | ⊦ M8 ≠ M18 | An Axiom |
| disj-I1-I11 | ⊦ I1 ≠ I11 | An Axiom |
| disj-I2-I8 | ⊦ I2 ≠ I8 | An Axiom |
| disj-I12-idle | ⊦ I12 ≠ idle | An Axiom |
| gstepf-I12 | ⊦ gstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs) | An Axiom |
| disj-M2-M7 | ⊦ M2 ≠ M7 | An Axiom |
| disj-M16-M17 | ⊦ M16 ≠ M17 | An Axiom |
| gstepf-M8 | ⊦ gstepf(gs, ls, M8, τ) = gs | An Axiom |
| disj-I14-M13 | ⊦ I14 ≠ M13 | An Axiom |
| lstepf-I4 | ⊦ lstepf(gs, ls, I4, τ) = ls.b:= false | An Axiom |
| disj-I11-M5 | ⊦ I11 ≠ M5 | An Axiom |
| lstepf-I19 | ⊦ ls.tid = tid → lstepf(gs, ls, I19, retINSERT(tid, ls.b)) = ls | An Axiom |
| disj-M10-M12 | ⊦ M10 ≠ M12 | An Axiom |
| disj-I6-I12 | ⊦ I6 ≠ I12 | An Axiom |
| disj-invMEMBER-retMEMBER | ⊦ invMEMBER(tid, invINSERTe) ≠ retMEMBER(tid0, b) | An Axiom |
| disj-I21-M11 | ⊦ I21 ≠ M11 | An Axiom |
| disj-I2-I15 | ⊦ I2 ≠ I15 | An Axiom |
| disj-I3-M5 | ⊦ I3 ≠ M5 | An Axiom |
| disj-M7-M14 | ⊦ M7 ≠ M14 | An Axiom |
| disj-I18-M10 | ⊦ I18 ≠ M10 | An Axiom |
| lstepf-idle-MEMBER | ⊦ ls.tid = tid → lstepf(gs, ls, idle, invMEMBER(tid, e1)) = ls.e:= e1 | An Axiom |
| disj-I5-M5 | ⊦ I5 ≠ M5 | An Axiom |
| disj-M18-idle | ⊦ M18 ≠ idle | An Axiom |
| disj-I13-M18 | ⊦ I13 ≠ M18 | An Axiom |
| disj-I3-I19 | ⊦ I3 ≠ I19 | An Axiom |
| disj-I6-I8 | ⊦ I6 ≠ I8 | An Axiom |
| pcstepf-I15 | ⊦ pcstepf(gs, ls, I15, a) = idle | An Axiom |
| updsel--dotb-dotsz | ⊦ (ls.b:= b).sz = ls.sz | An Axiom |
| disj-I3-idle | ⊦ I3 ≠ idle | An Axiom |
| sel-invINSERT-dottid | ⊦ invINSERT(tid, invINSERTe).tid = tid | An Axiom |
| disj-I10-I11 | ⊦ I10 ≠ I11 | An Axiom |
| lstepf-M6 | ⊦ lstepf(gs, ls, M6, a) = ls.e0:= gs.ar[ls.n] | An Axiom |
| disj-I7-I16 | ⊦ I7 ≠ I16 | An Axiom |
| updsel--dotb-dotb | ⊦ (ls.b:= b).b ↔ b | An Axiom |
| disj-I10-M16 | ⊦ I10 ≠ M16 | An Axiom |
| updsel--dote0-dotb | ⊦ (ls.e0:= e0).b ↔ ls.b | An Axiom |
| disj-I1-M16 | ⊦ I1 ≠ M16 | An Axiom |
| disj-I3-I10 | ⊦ I3 ≠ I10 | An Axiom |
| disj-M4-M7 | ⊦ M4 ≠ M7 | An Axiom |
| gstepf-M17 | ⊦ gstepf(gs, ls, M17, τ) = gs | An Axiom |
| disj-I15-M5 | ⊦ I15 ≠ M5 | An Axiom |
| disj-M2-M13 | ⊦ M2 ≠ M13 | An Axiom |
| disj-I4-M1 | ⊦ I4 ≠ M1 | An Axiom |
| disj-I14-I17 | ⊦ I14 ≠ I17 | An Axiom |
| disj-I12-M3 | ⊦ I12 ≠ M3 | An Axiom |
| disj-I13-I16 | ⊦ I13 ≠ I16 | An Axiom |
| disj-I20-M10 | ⊦ I20 ≠ M10 | An Axiom |
| disj-I7-I10 | ⊦ I7 ≠ I10 | An Axiom |
| disj-I5-M16 | ⊦ I5 ≠ M16 | An Axiom |
| disj-I20-M7 | ⊦ I20 ≠ M7 | An Axiom |
| pre-M5 | ⊦ pre(gs, ls, M5, a) ↔ a = τ | An Axiom |
| disj-I7-I19 | ⊦ I7 ≠ I19 | An Axiom |
| updsel--dotb-dote | ⊦ (ls.b:= b).e = ls.e | An Axiom |
| disj-I1-M10 | ⊦ I1 ≠ M10 | An Axiom |
| updsel--dote0-dote | ⊦ (ls.e0:= e0).e = ls.e | An Axiom |
| pcstepf-M2 | ⊦ pcstepf(gs, ls, M2, a) = M3 | An Axiom |
| disj-I3-M8 | ⊦ I3 ≠ M8 | An Axiom |
| disj-I7-M8 | ⊦ I7 ≠ M8 | An Axiom |
| gstepf-I15 | ⊦ ls.tid = tid → gstepf(gs, ls, I15, retINSERT(tid, b)) = gs | An Axiom |
| disj-I9-M13 | ⊦ I9 ≠ M13 | An Axiom |
| pre-I17 | ⊦ pre(gs, ls, I17, a) ↔ a = τ | An Axiom |
| disj-I14-M16 | ⊦ I14 ≠ M16 | An Axiom |
| disj-M3-M5 | ⊦ M3 ≠ M5 | An Axiom |
| lstepf-I7 | ⊦ lstepf(gs, ls, I7, τ) = ls | An Axiom |
| updsel--dote-dotsz | ⊦ (ls.e:= e).sz = ls.sz | An Axiom |
| disj-I6-M11 | ⊦ I6 ≠ M11 | An Axiom |
| disj-I21-M14 | ⊦ I21 ≠ M14 | An Axiom |
| disj-I18-M13 | ⊦ I18 ≠ M13 | An Axiom |
| disj-M7-M17 | ⊦ M7 ≠ M17 | An Axiom |
| gstepf-M2 | ⊦ gstepf(gs, ls, M2, τ) = gs | An Axiom |
| disj-M3-M11 | ⊦ M3 ≠ M11 | An Axiom |
| disj-M12-idle | ⊦ M12 ≠ idle | An Axiom |
| updsel--dotb-dotn | ⊦ (ls.b:= b).n = ls.n | An Axiom |
| disj-I18-M3 | ⊦ I18 ≠ M3 | An Axiom |
| disj-I13-M12 | ⊦ I13 ≠ M12 | An Axiom |
| disj-M1-M5 | ⊦ M1 ≠ M5 | An Axiom |
| disj-I1-I20 | ⊦ I1 ≠ I20 | An Axiom |
| disj-I1-I14 | ⊦ I1 ≠ I14 | An Axiom |
| disj-M6-M13 | ⊦ M6 ≠ M13 | An Axiom |
| sel-invINSERT-dotinvINSERTe | ⊦ invINSERT(tid, invINSERTe).invINSERTe = invINSERTe | An Axiom |
| disj-I1-M8 | ⊦ I1 ≠ M8 | An Axiom |
| disj-I9-M8 | ⊦ I9 ≠ M8 | An Axiom |
| gstepf-M11 | ⊦ gstepf(gs, ls, M11, τ) = gs | An Axiom |
| disj-M15-M16 | ⊦ M15 ≠ M16 | An Axiom |
| updsel--dote0-dotn | ⊦ (ls.e0:= e0).n = ls.n | An Axiom |
| disj-I14-M3 | ⊦ I14 ≠ M3 | An Axiom |
| disj-M2-M16 | ⊦ M2 ≠ M16 | An Axiom |
| pre-M13 | ⊦ pre(gs, ls, M13, a) ↔ a = τ | An Axiom |
| disj-I2-I18 | ⊦ I2 ≠ I18 | An Axiom |
| disj-I12-M17 | ⊦ I12 ≠ M17 | An Axiom |
| disj-I10-M3 | ⊦ I10 ≠ M3 | An Axiom |
| disj-M10-M15 | ⊦ M10 ≠ M15 | An Axiom |
| disj-I6-I21 | ⊦ I6 ≠ I21 | An Axiom |
| disj-I5-I11 | ⊦ I5 ≠ I11 | An Axiom |
| disj-M5-idle | ⊦ M5 ≠ idle | An Axiom |
| disj-I16-M3 | ⊦ I16 ≠ M3 | An Axiom |
| gstepf-I21 | ⊦ ls.tid = tid → gstepf(gs, ls, I21, retINSERT(tid, b)) = gs | An Axiom |
| disj-I17-M18 | ⊦ I17 ≠ M18 | An Axiom |
| inj-invINSERT | ⊦ invINSERT(tid, invINSERTe) = invINSERT(tid0, invINSERTe0) ↔ tid = tid0 ∧ invINSERTe = invINSERTe0 | An Axiom |
| disj-I5-M8 | ⊦ I5 ≠ M8 | An Axiom |
| disj-I6-I15 | ⊦ I6 ≠ I15 | An Axiom |
| sel-doMEMBER-dottid | ⊦ doMEMBER(tid).tid = tid | An Axiom |
| disj-I19-M17 | ⊦ I19 ≠ M17 | An Axiom |
| disj-M1-M12 | ⊦ M1 ≠ M12 | An Axiom |
| disj-I2-I5 | ⊦ I2 ≠ I5 | An Axiom |
| disj-I9-M16 | ⊦ I9 ≠ M16 | An Axiom |
| disj-I1-I17 | ⊦ I1 ≠ I17 | An Axiom |
| gstepf-M5 | ⊦ gstepf(gs, ls, M5, τ) = gs | An Axiom |
| disj-I5-M10 | ⊦ I5 ≠ M10 | An Axiom |
| disj-I16-M6 | ⊦ I16 ≠ M6 | An Axiom |
| sel-mkstate-dotgstate | ⊦ mkstate(gstate, lsf, pcf).gstate = gstate | An Axiom |
| disj-I7-I9 | ⊦ I7 ≠ I9 | An Axiom |
| disj-I9-M2 | ⊦ I9 ≠ M2 | An Axiom |
| gstepf-I3 | ⊦ gstepf(gs, ls, I3, τ) = gs | An Axiom |
| disj-I16-M17 | ⊦ I16 ≠ M17 | An Axiom |
| disj-I6-I18 | ⊦ I6 ≠ I18 | An Axiom |
| disj-M14-M15 | ⊦ M14 ≠ M15 | An Axiom |
| disj-I9-idle | ⊦ I9 ≠ idle | An Axiom |
| gstepf-I18 | ⊦ gstepf(gs, ls, I18, a) = gs | An Axiom |
| case-HashsetAction | ⊦ a = doINSERT(a.tid, a.b) ∨ a = doMEMBER(a.tid) ∨ a = invINSERT(a.tid, a.invINSERTe) ∨ a = invMEMBER(a.tid, a.invMEMBERe) ∨ a = retINSERT(a.tid, a.retINSERTb) ∨ a = retMEMBER(a.tid, a.retMEMBERb) ∨ a = τ | An Axiom |
| disj-M5-M8 | ⊦ M5 ≠ M8 | An Axiom |
| updsel--dotn-dote | ⊦ (ls.n:= sz1).e = ls.e | An Axiom |
| upd-mkls-dottid | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).tid:= tid0 = mkls(tid0, e, b, sz, sz0, sz1, e0) | An Axiom |
| disj-I20-M1 | ⊦ I20 ≠ M1 | An Axiom |
| disj-I13-M15 | ⊦ I13 ≠ M15 | An Axiom |
| disj-M9-M18 | ⊦ M9 ≠ M18 | An Axiom |
| updsel--dotn-dotn | ⊦ (ls.n:= sz1).n = sz1 | An Axiom |
| disj-I4-M15 | ⊦ I4 ≠ M15 | An Axiom |
| disj-I14-M6 | ⊦ I14 ≠ M6 | An Axiom |
| updsel--dotsz-dotn0 | ⊦ (ls.sz:= sz).n0 = ls.n0 | An Axiom |
| disj-I5-I14 | ⊦ I5 ≠ I14 | An Axiom |
| disj-M7-M8 | ⊦ M7 ≠ M8 | An Axiom |
| disj-I5-I9 | ⊦ I5 ≠ I9 | An Axiom |
| disj-M5-M12 | ⊦ M5 ≠ M12 | An Axiom |
| disj-I19-idle | ⊦ I19 ≠ idle | An Axiom |
| disj-I7-M2 | ⊦ I7 ≠ M2 | An Axiom |
| disj-I20-M13 | ⊦ I20 ≠ M13 | An Axiom |
| disj-I18-M16 | ⊦ I18 ≠ M16 | An Axiom |
| disj-I17-M12 | ⊦ I17 ≠ M12 | An Axiom |
| pre-I11 | ⊦ pre(gs, ls, I11, a) ↔ a = τ | An Axiom |
| disj-I8-M6 | ⊦ I8 ≠ M6 | An Axiom |
| disj-I12-I21 | ⊦ I12 ≠ I21 | An Axiom |
| disj-I12-I15 | ⊦ I12 ≠ I15 | An Axiom |
| disj-I1-M13 | ⊦ I1 ≠ M13 | An Axiom |
| disj-I3-I9 | ⊦ I3 ≠ I9 | An Axiom |
| disj-M2-M10 | ⊦ M2 ≠ M10 | An Axiom |
| disj-I10-M6 | ⊦ I10 ≠ M6 | An Axiom |
| disj-M3-M8 | ⊦ M3 ≠ M8 | An Axiom |
| disj-M10-M18 | ⊦ M10 ≠ M18 | An Axiom |
| disj-I3-M2 | ⊦ I3 ≠ M2 | An Axiom |
| disj-I21-M17 | ⊦ I21 ≠ M17 | An Axiom |
| disj-I4-I19 | ⊦ I4 ≠ I19 | An Axiom |
| disj-I5-M2 | ⊦ I5 ≠ M2 | An Axiom |
| disj-doMEMBER-retMEMBER | ⊦ doMEMBER(tid) ≠ retMEMBER(tid0, b) | An Axiom |
| disj-I4-I5 | ⊦ I4 ≠ I5 | An Axiom |
| lstepf-I1 | ⊦ lstepf(gs, ls, I1, τ) = ls.sz:= # gs.ar | An Axiom |
| disj-M1-M15 | ⊦ M1 ≠ M15 | An Axiom |
| disj-I18-M6 | ⊦ I18 ≠ M6 | An Axiom |
| disj-I11-M16 | ⊦ I11 ≠ M16 | An Axiom |
| disj-I5-I20 | ⊦ I5 ≠ I20 | An Axiom |
| disj-I4-I10 | ⊦ I4 ≠ I10 | An Axiom |
| disj-I13-I19 | ⊦ I13 ≠ I19 | An Axiom |
| disj-I21-M5 | ⊦ I21 ≠ M5 | An Axiom |
| disj-I12-M6 | ⊦ I12 ≠ M6 | An Axiom |
| disj-M1-M8 | ⊦ M1 ≠ M8 | An Axiom |
| updsel--dotb-dottid | ⊦ (ls.b:= b).tid = ls.tid | An Axiom |
| pre-M8 | ⊦ pre(gs, ls, M8, a) ↔ a = τ | An Axiom |
| disj-M6-M16 | ⊦ M6 ≠ M16 | An Axiom |
| upd-mkls-dotn0 | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n0:= sz3 = mkls(tid, e, b, sz, sz3, sz1, e0) | An Axiom |
| disj-I1-M2 | ⊦ I1 ≠ M2 | An Axiom |
| updsel--dotsz-dottid | ⊦ (ls.sz:= sz).tid = ls.tid | An Axiom |
| pcstepf-M5 | ⊦ pcstepf(gs, ls, M5, a) = (¬ ls.b ⊃ M6;M18) | An Axiom |
| disj-I9-I11 | ⊦ I9 ≠ I11 | An Axiom |
| updsel--dotn-dottid | ⊦ (ls.n:= sz1).tid = ls.tid | An Axiom |
| pre-I6 | ⊦ pre(gs, ls, I6, a) ↔ a = (ls.e = gs.ar[ls.n] ⊃ doINSERT(ls.tid, true);τ) | An Axiom |
| pre-M16 | ⊦ pre(gs, ls, M16, a) ↔ a = retMEMBER(ls.tid, ls.b) | An Axiom |
| disj-I12-M11 | ⊦ I12 ≠ M11 | An Axiom |
| disj-M1-M18 | ⊦ M1 ≠ M18 | An Axiom |
| disj-I8-I19 | ⊦ I8 ≠ I19 | An Axiom |
| lstepf-idle-INSERT | ⊦ ls.tid = tid → lstepf(gs, ls, idle, invINSERT(tid, e1)) = ls.e:= e1 | An Axiom |
| disj-I10-M15 | ⊦ I10 ≠ M15 | An Axiom |
| disj-M9-M12 | ⊦ M9 ≠ M12 | An Axiom |
| disj-I4-I13 | ⊦ I4 ≠ I13 | An Axiom |
| disj-I12-M9 | ⊦ I12 ≠ M9 | An Axiom |
| disj-I11-M4 | ⊦ I11 ≠ M4 | An Axiom |
| lstepf-I18 | ⊦ lstepf(gs, ls, I18, a) = ls.b:= false | An Axiom |
| pcstepf-I20 | ⊦ pcstepf(gs, ls, I20, a) = I5 | An Axiom |
| gen-HashsetPC | HashsetPC freely generated by I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15, I16, I17, I18, I19, I20, I21, M1, M2, M3, M4, M5, M6, M7, M8, M9, M10, M11, M12, M13, M14, M15, M16, M17, M18, idle ; | An Axiom |
| disj-I1-M5 | ⊦ I1 ≠ M5 | An Axiom |
| disj-I17-M4 | ⊦ I17 ≠ M4 | An Axiom |
| disj-M5-M15 | ⊦ M5 ≠ M15 | An Axiom |
| disj-I5-I17 | ⊦ I5 ≠ I17 | An Axiom |
| pcstepf-M8 | ⊦ pcstepf(gs, ls, M8, a) = M9 | An Axiom |
| disj-I15-M16 | ⊦ I15 ≠ M16 | An Axiom |
| disj-M13-M14 | ⊦ M13 ≠ M14 | An Axiom |
| disj-I9-I20 | ⊦ I9 ≠ I20 | An Axiom |
| pcstepf-M10 | ⊦ pcstepf(gs, ls, M10, a) = (ls.e0 = ⊥ ⊃ M11;M13) | An Axiom |
| disj-I13-idle | ⊦ I13 ≠ idle | An Axiom |
| disj-I21-M8 | ⊦ I21 ≠ M8 | An Axiom |
| disj-I9-M10 | ⊦ I9 ≠ M10 | An Axiom |
| disj-I7-I21 | ⊦ I7 ≠ I21 | An Axiom |
| disj-I11-M10 | ⊦ I11 ≠ M10 | An Axiom |
| disj-I6-M9 | ⊦ I6 ≠ M9 | An Axiom |
| disj-M1-M2 | ⊦ M1 ≠ M2 | An Axiom |
| pcstepf-I6 | ⊦ pcstepf(gs, ls, I6, a) = I7 | An Axiom |
| pre-I14 | ⊦ pre(gs, ls, I14, a) ↔ a = τ | An Axiom |
| disj-I8-M9 | ⊦ I8 ≠ M9 | An Axiom |
| disj-I12-M14 | ⊦ I12 ≠ M14 | An Axiom |
| disj-I16-M11 | ⊦ I16 ≠ M11 | An Axiom |
| disj-I4-idle | ⊦ I4 ≠ idle | An Axiom |
| disj-I10-M9 | ⊦ I10 ≠ M9 | An Axiom |
| disj-I3-M14 | ⊦ I3 ≠ M14 | An Axiom |
| gstepf-I6 | ⊦ gstepf(gs, ls, I6, a) = gs | An Axiom |
| disj-invMEMBER-retINSERT | ⊦ invMEMBER(tid, invINSERTe) ≠ retINSERT(tid0, b) | An Axiom |
| disj-M4-M11 | ⊦ M4 ≠ M11 | An Axiom |
| disj-I15-M4 | ⊦ I15 ≠ M4 | An Axiom |
| pre-I20 | ⊦ pre(gs, ls, I20, a) ↔ a = τ | An Axiom |
| disj-I8-M15 | ⊦ I8 ≠ M15 | An Axiom |
| elim-mkstate | ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf) | An Axiom |
| disj-I4-M9 | ⊦ I4 ≠ M9 | An Axiom |
| disj-M14-M18 | ⊦ M14 ≠ M18 | An Axiom |
| disj-I11-I20 | ⊦ I11 ≠ I20 | An Axiom |
| disj-I11-I14 | ⊦ I11 ≠ I14 | An Axiom |
| lstepf-M5 | ⊦ lstepf(gs, ls, M5, τ) = ls | An Axiom |
| pre-idle | ⊦ pre(gs, ls, idle, a) ↔ (∃ e1. a = invINSERT(ls.tid, e1) ∧ e1 ≠ ⊥) ∨ (∃ e1. a = invMEMBER(ls.tid, e1) ∧ e1 ≠ ⊥) | An Axiom |
| lstepf-M14 | ⊦ lstepf(gs, ls, M14, τ) = ls | An Axiom |
| disj-I13-M4 | ⊦ I13 ≠ M4 | An Axiom |
| disj-I19-M4 | ⊦ I19 ≠ M4 | An Axiom |
| disj-I16-I21 | ⊦ I16 ≠ I21 | An Axiom |
| disj-I20-M16 | ⊦ I20 ≠ M16 | An Axiom |
| disj-I17-M15 | ⊦ I17 ≠ M15 | An Axiom |
| lstepf-M16-b | ⊦ ls.tid = tid ∧ ¬ ls.b → lstepf(gs, ls, M16, retMEMBER(tid, false)) = ls | A User Theorem |
| pcstepf-I14 | ⊦ pcstepf(gs, ls, I14, a) = I15 | An Axiom |
| disj-I9-I14 | ⊦ I9 ≠ I14 | An Axiom |
| pre-M10 | ⊦ pre(gs, ls, M10, a) ↔ a = τ | An Axiom |
| sel-mkls-dote0 | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0 = e0 | An Axiom |
| disj-I2-M9 | ⊦ I2 ≠ M9 | An Axiom |
| pre-I9 | ⊦ pre(gs, ls, I9, a) ↔ a = retINSERT(ls.tid, ls.b) | An Axiom |
| disj-I1-I3 | ⊦ I1 ≠ I3 | An Axiom |
| disj-I12-I18 | ⊦ I12 ≠ I18 | An Axiom |
| disj-I3-I18 | ⊦ I3 ≠ I18 | An Axiom |
| disj-I4-M18 | ⊦ I4 ≠ M18 | An Axiom |
| disj-M6-M10 | ⊦ M6 ≠ M10 | An Axiom |
| HashsetGInv | ⊦ HashsetGInv(gs) ↔ # gs.ar ≠ 0 ∧ htok(gs.ar) | An Axiom |
| disj-I17-I19 | ⊦ I17 ≠ I19 | An Axiom |
| disj-I8-I10 | ⊦ I8 ≠ I10 | An Axiom |
| disj-I2-M3 | ⊦ I2 ≠ M3 | An Axiom |
| pre-I3 | ⊦ pre(gs, ls, I3, a) ↔ a = τ | An Axiom |
| disj-I6-M3 | ⊦ I6 ≠ M3 | An Axiom |
| disj-I7-I18 | ⊦ I7 ≠ I18 | An Axiom |
| disj-I10-M18 | ⊦ I10 ≠ M18 | An Axiom |
| disj-I3-I12 | ⊦ I3 ≠ I12 | An Axiom |
| disj-I3-M17 | ⊦ I3 ≠ M17 | An Axiom |
| disj-M2-M9 | ⊦ M2 ≠ M9 | An Axiom |
| disj-M4-M14 | ⊦ M4 ≠ M14 | An Axiom |
| disj-I14-M15 | ⊦ I14 ≠ M15 | An Axiom |
| disj-M12-M13 | ⊦ M12 ≠ M13 | An Axiom |
| disj-I16-I18 | ⊦ I16 ≠ I18 | An Axiom |
| disj-I11-M7 | ⊦ I11 ≠ M7 | An Axiom |
| disj-I8-M18 | ⊦ I8 ≠ M18 | An Axiom |
| disj-M9-M15 | ⊦ M9 ≠ M15 | An Axiom |
| disj-M8-M11 | ⊦ M8 ≠ M11 | An Axiom |
| lstepf-I12 | ⊦ lstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]) | An Axiom |
| disj-I3-I6 | ⊦ I3 ≠ I6 | An Axiom |
| disj-I2-I17 | ⊦ I2 ≠ I17 | An Axiom |
| disj-I17-M7 | ⊦ I17 ≠ M7 | An Axiom |
| disj-I11-M13 | ⊦ I11 ≠ M13 | An Axiom |
| disj-M6-M9 | ⊦ M6 ≠ M9 | An Axiom |
| disj-I15-M10 | ⊦ I15 ≠ M10 | An Axiom |
| disj-I4-I16 | ⊦ I4 ≠ I16 | An Axiom |
| disj-M11-M18 | ⊦ M11 ≠ M18 | An Axiom |
| pcstepf-I17 | ⊦ pcstepf(gs, ls, I17, a) = (ls.n = ls.n0 ⊃ I18;I20) | An Axiom |
| disj-I7-M14 | ⊦ I7 ≠ M14 | An Axiom |
| disj-I19-M16 | ⊦ I19 ≠ M16 | An Axiom |
| disj-M14-idle | ⊦ M14 ≠ idle | An Axiom |
| disj-M13-M17 | ⊦ M13 ≠ M17 | An Axiom |
| disj-I9-I17 | ⊦ I9 ≠ I17 | An Axiom |
| sel-mkstate-dotlsf | ⊦ mkstate(gstate, lsf, pcf).lsf = lsf | An Axiom |
| disj-M13-idle | ⊦ M13 ≠ idle | An Axiom |
| disj-I1-I6 | ⊦ I1 ≠ I6 | An Axiom |
| disj-I21-M2 | ⊦ I21 ≠ M2 | An Axiom |
| pcstepf-I9 | ⊦ pcstepf(gs, ls, I9, a) = idle | An Axiom |
| disj-I15-M7 | ⊦ I15 ≠ M7 | An Axiom |
| disj-M4-M9 | ⊦ M4 ≠ M9 | 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 |
| disj-M8-M9 | ⊦ M8 ≠ M9 | An Axiom |
| disj-I4-M3 | ⊦ I4 ≠ M3 | An Axiom |
| disj-I16-M14 | ⊦ I16 ≠ M14 | An Axiom |
| disj-I8-M3 | ⊦ I8 ≠ M3 | An Axiom |
| gstepf-I9 | ⊦ ls.tid = tid → gstepf(gs, ls, I9, retINSERT(tid, b)) = gs | An Axiom |
| disj-M5-M18 | ⊦ M5 ≠ M18 | An Axiom |
| disj-I8-I13 | ⊦ I8 ≠ I13 | An Axiom |
| disj-I10-I13 | ⊦ I10 ≠ I13 | An Axiom |
| lstepf-M8 | ⊦ lstepf(gs, ls, M8, τ) = ls.b:= true | An Axiom |
| disj-I2-M13 | ⊦ I2 ≠ M13 | An Axiom |
| disj-I5-I6 | ⊦ I5 ≠ I6 | An Axiom |
| disj-invINSERT-invMEMBER | ⊦ invINSERT(tid, invINSERTe) ≠ invMEMBER(tid0, invINSERTe0) | An Axiom |
| disj-M3-M10 | ⊦ M3 ≠ M10 | An Axiom |
| disj-I19-M7 | ⊦ I19 ≠ M7 | An Axiom |
| updsel--dotn-dotb | ⊦ (ls.n:= sz1).b ↔ ls.b | An Axiom |
| disj-I15-I20 | ⊦ I15 ≠ I20 | An Axiom |
| disj-I11-I17 | ⊦ I11 ≠ I17 | An Axiom |
| updsel--dotgstate-dotlsf | ⊦ (s.gstate:= gstate).lsf = s.lsf | An Axiom |
| disj-I4-M12 | ⊦ I4 ≠ M12 | An Axiom |
| disj-I20-idle | ⊦ I20 ≠ idle | An Axiom |
| disj-M6-idle | ⊦ M6 ≠ idle | An Axiom |
| lstepf-M17 | ⊦ lstepf(gs, ls, M17, τ) = ls | An Axiom |
| disj-I13-M7 | ⊦ I13 ≠ M7 | An Axiom |
| pcstepf-M13 | ⊦ pcstepf(gs, ls, M13, a) = M14 | An Axiom |
| disj-I16-M5 | ⊦ I16 ≠ M5 | An Axiom |
| lstepf-M2 | ⊦ lstepf(gs, ls, M2, τ) = ls.n0:= get_hash(ls.e, ls.sz) | An Axiom |
| disj-retINSERT-tau | ⊦ retINSERT(tid, b) ≠ τ | An Axiom |
| disj-I9-M1 | ⊦ I9 ≠ M1 | An Axiom |
| lstepf-I21-b | ⊦ ls.tid = tid ∧ ls.b → lstepf(gs, ls, I21, retINSERT(tid, true)) = ls | A User Theorem |
| disj-I19-I20 | ⊦ I19 ≠ I20 | An Axiom |
| disj-I8-M12 | ⊦ I8 ≠ M12 | An Axiom |
| disj-I6-I17 | ⊦ I6 ≠ I17 | An Axiom |
| disj-I3-I21 | ⊦ I3 ≠ I21 | An Axiom |
| disj-I2-I11 | ⊦ I2 ≠ I11 | An Axiom |
| disj-invMEMBER-tau | ⊦ invMEMBER(tid, invINSERTe) ≠ τ | An Axiom |
| lstepf-M11 | ⊦ lstepf(gs, ls, M11, τ) = ls.b:= false | An Axiom |
| disj-I13-M1 | ⊦ I13 ≠ M1 | An Axiom |
| disj-doMEMBER-retINSERT | ⊦ doMEMBER(tid) ≠ retINSERT(tid0, b) | An Axiom |
| disj-M3-M13 | ⊦ M3 ≠ M13 | An Axiom |
| pcstepf-M16 | ⊦ pcstepf(gs, ls, M16, a) = idle | An Axiom |
| disj-M7-M10 | ⊦ M7 ≠ M10 | An Axiom |
| disj-I18-M5 | ⊦ I18 ≠ M5 | An Axiom |
| disj-I13-M14 | ⊦ I13 ≠ M14 | An Axiom |
| lstepf-I9 | ⊦ ls.tid = tid → lstepf(gs, ls, I9, retINSERT(tid, ls.b)) = ls | An Axiom |
| disj-I6-M6 | ⊦ I6 ≠ M6 | An Axiom |
| inj-retMEMBER | ⊦ retMEMBER(tid, b) = retMEMBER(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| disj-I5-M1 | ⊦ I5 ≠ M1 | An Axiom |
| disj-I15-I17 | ⊦ I15 ≠ I17 | An Axiom |
| sel-retMEMBER-dottid | ⊦ retMEMBER(tid, b).tid = tid | An Axiom |
| disj-I19-M10 | ⊦ I19 ≠ M10 | An Axiom |
| disj-I7-M1 | ⊦ I7 ≠ M1 | An Axiom |
| disj-I7-M17 | ⊦ I7 ≠ M17 | An Axiom |
| updsel--dotn-dote0 | ⊦ (ls.n:= sz1).e0 = ls.e0 | An Axiom |
| lstepf-I21 | ⊦ ls.tid = tid → lstepf(gs, ls, I21, retINSERT(tid, ls.b)) = ls | An Axiom |
| disj-M8-M14 | ⊦ M8 ≠ M14 | An Axiom |
| disj-I3-M11 | ⊦ I3 ≠ M11 | An Axiom |
| disj-I1-I16 | ⊦ I1 ≠ I16 | An Axiom |
| disj-M2-M3 | ⊦ M2 ≠ M3 | An Axiom |
| gstepf-I17 | ⊦ gstepf(gs, ls, I17, τ) = gs | An Axiom |
| disj-M4-M17 | ⊦ M4 ≠ M17 | An Axiom |
| disj-invINSERT-tau | ⊦ invINSERT(tid, invINSERTe) ≠ τ | An Axiom |
| disj-M15-M18 | ⊦ M15 ≠ M18 | An Axiom |
| pcstepf-idle-INSERT | ⊦ ls.tid = tid → pcstepf(gs, ls, idle, invINSERT(tid, e1)) = I1 | An Axiom |
| pcstepf-idle-MEMBER | ⊦ ls.tid = tid → pcstepf(gs, ls, idle, invMEMBER(tid, e1)) = M1 | An Axiom |
| disj-I14-M18 | ⊦ I14 ≠ M18 | An Axiom |
| disj-M12-M16 | ⊦ M12 ≠ M16 | An Axiom |
| disj-M11-M12 | ⊦ M11 ≠ M12 | An Axiom |
| disj-I10-M12 | ⊦ I10 ≠ M12 | An Axiom |
| updsel--dotlsf-dotlsf | ⊦ (s.lsf:= lsf).lsf = lsf | An Axiom |
| inj-doMEMBER | ⊦ doMEMBER(tid) = doMEMBER(tid0) ↔ tid = tid0 | An Axiom |
| disj-I4-M6 | ⊦ I4 ≠ M6 | An Axiom |
| disj-I21-M16 | ⊦ I21 ≠ M16 | An Axiom |
| disj-I18-M15 | ⊦ I18 ≠ M15 | An Axiom |
| disj-I17-M1 | ⊦ I17 ≠ M1 | An Axiom |
| disj-I8-I16 | ⊦ I8 ≠ I16 | An Axiom |
| sel-mkls-dotsz | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).sz = sz | An Axiom |
| disj-I2-M16 | ⊦ I2 ≠ M16 | An Axiom |
| disj-I11-M1 | ⊦ I11 ≠ M1 | An Axiom |
| disj-I19-M1 | ⊦ I19 ≠ M1 | An Axiom |
| lstepf-I15 | ⊦ ls.tid = tid → lstepf(gs, ls, I15, retINSERT(tid, ls.b)) = ls | An Axiom |
| disj-M1-idle | ⊦ M1 ≠ idle | An Axiom |
| pcstepf-I11 | ⊦ pcstepf(gs, ls, I11, a) = I17 | An Axiom |
| disj-retMEMBER-tau | ⊦ retMEMBER(tid, b) ≠ τ | An Axiom |
| disj-I15-M13 | ⊦ I15 ≠ M13 | An Axiom |
| disj-I6-M13 | ⊦ I6 ≠ M13 | An Axiom |
| disj-I10-I16 | ⊦ I10 ≠ I16 | An Axiom |
| disj-I7-I12 | ⊦ I7 ≠ I12 | An Axiom |
| disj-I20-M9 | ⊦ I20 ≠ M9 | An Axiom |
| pre-M7 | ⊦ pre(gs, ls, M7, a) ↔ a = τ | An Axiom |
| sel-doINSERT-dotb | ⊦ doINSERT(tid, b).b ↔ b | An Axiom |
| disj-I2-M6 | ⊦ I2 ≠ M6 | An Axiom |
| disj-I1-I9 | ⊦ I1 ≠ I9 | An Axiom |
| disj-I1-M12 | ⊦ I1 ≠ M12 | An Axiom |
| pcstepf-I3 | ⊦ pcstepf(gs, ls, I3, a) = I4 | An Axiom |
| disj-I15-M1 | ⊦ I15 ≠ M1 | An Axiom |
| disj-I3-I15 | ⊦ I3 ≠ I15 | An Axiom |
| gstepf-M13 | ⊦ gstepf(gs, ls, M13, τ) = gs | An Axiom |
| disj-I18-I19 | ⊦ I18 ≠ I19 | An Axiom |
| disj-M2-M18 | ⊦ M2 ≠ M18 | An Axiom |
| upd-mkls-dote0 | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0:= e2 = mkls(tid, e, b, sz, sz0, sz1, e2) | An Axiom |
| disj-I2-I4 | ⊦ I2 ≠ I4 | An Axiom |
| disj-I20-M3 | ⊦ I20 ≠ M3 | An Axiom |
| updsel--dote-dottid | ⊦ (ls.e:= e).tid = ls.tid | An Axiom |
| disj-I5-M4 | ⊦ I5 ≠ M4 | An Axiom |
| disj-I7-I15 | ⊦ I7 ≠ I15 | An Axiom |
| disj-I1-M4 | ⊦ I1 ≠ M4 | An Axiom |
| pcstepf-M7 | ⊦ pcstepf(gs, ls, M7, a) = (ls.e = ls.e0 ⊃ M8;M10) | An Axiom |
| disj-I19-M13 | ⊦ I19 ≠ M13 | An Axiom |
| disj-I7-M4 | ⊦ I7 ≠ M4 | An Axiom |
| disj-I5-idle | ⊦ I5 ≠ idle | An Axiom |
| disj-I6-I7 | ⊦ I6 ≠ I7 | An Axiom |
| disj-I10-I19 | ⊦ I10 ≠ I19 | An Axiom |
| updsel--dotgstate-dotgstate | ⊦ (s.gstate:= gstate).gstate = gstate | An Axiom |
| disj-I1-I19 | ⊦ I1 ≠ I19 | An Axiom |
| disj-I14-M12 | ⊦ I14 ≠ M12 | An Axiom |
| disj-M2-M6 | ⊦ M2 ≠ M6 | An Axiom |
| disj-I5-M12 | ⊦ I5 ≠ M12 | An Axiom |
| pre-M1 | ⊦ pre(gs, ls, M1, a) ↔ a = τ | An Axiom |
| disj-I14-M8 | ⊦ I14 ≠ M8 | An Axiom |
| disj-I14-idle | ⊦ I14 ≠ idle | An Axiom |
| disj-I3-M4 | ⊦ I3 ≠ M4 | An Axiom |
| disj-I18-M18 | ⊦ I18 ≠ M18 | An Axiom |
| disj-I2-M10 | ⊦ I2 ≠ M10 | An Axiom |
| lstepf-M9-b | ⊦ ls.tid = tid ∧ ls.b → lstepf(gs, ls, M9, retMEMBER(tid, true)) = ls | A User Theorem |
| disj-I4-I7 | ⊦ I4 ≠ I7 | An Axiom |
| gstepf-M7 | ⊦ gstepf(gs, ls, M7, τ) = gs | An Axiom |
| disj-M3-M16 | ⊦ M3 ≠ M16 | An Axiom |
| disj-M4-M6 | ⊦ M4 ≠ M6 | An Axiom |
| lstepf-I3 | ⊦ lstepf(gs, ls, I3, τ) = ls.n:= ls.n0 | An Axiom |
| disj-I18-M8 | ⊦ I18 ≠ M8 | An Axiom |
| disj-I13-M17 | ⊦ I13 ≠ M17 | An Axiom |
| disj-M11-M15 | ⊦ M11 ≠ M15 | An Axiom |
| disj-I6-I11 | ⊦ I6 ≠ I11 | An Axiom |
| disj-I12-M8 | ⊦ I12 ≠ M8 | An Axiom |
| disj-I6-M16 | ⊦ I6 ≠ M16 | An Axiom |
| disj-I1-I10 | ⊦ I1 ≠ I10 | An Axiom |
| disj-M8-M17 | ⊦ M8 ≠ M17 | An Axiom |
| updsel--dotn0-dotn0 | ⊦ (ls.n0:= sz0).n0 = sz0 | An Axiom |
| disj-M7-M13 | ⊦ M7 ≠ M13 | An Axiom |
| disj-I20-M15 | ⊦ I20 ≠ M15 | An Axiom |
| gstepf-I11 | ⊦ gstepf(gs, ls, I11, τ) = gs | An Axiom |
| disj-I17-M14 | ⊦ I17 ≠ M14 | An Axiom |
| disj-M2-M12 | ⊦ M2 ≠ M12 | An Axiom |
| gstepf-M16 | ⊦ ls.tid = tid → gstepf(gs, ls, M16, retMEMBER(tid, b)) = gs | An Axiom |
| lstepf-I9-b | ⊦ ls.tid = tid ∧ ls.b → lstepf(gs, ls, I9, retINSERT(tid, true)) = ls | A User Theorem |
| disj-I1-M15 | ⊦ I1 ≠ M15 | An Axiom |
| pre-M18 | ⊦ pre(gs, ls, M18, a) ↔ a = retMEMBER(ls.tid, ls.b) | An Axiom |
| disj-I2-I7 | ⊦ I2 ≠ I7 | An Axiom |
| disj-I14-I16 | ⊦ I14 ≠ I16 | An Axiom |
| disj-I10-M8 | ⊦ I10 ≠ M8 | An Axiom |
| disj-I7-M11 | ⊦ I7 ≠ M11 | An Axiom |
| updsel--dotn0-dotb | ⊦ (ls.n0:= sz0).b ↔ ls.b | An Axiom |
| disj-I5-I16 | ⊦ I5 ≠ I16 | An Axiom |
| disj-I16-M8 | ⊦ I16 ≠ M8 | An Axiom |
| disj-I2-I20 | ⊦ I2 ≠ I20 | An Axiom |
| disj-I21-M10 | ⊦ I21 ≠ M10 | An Axiom |
| disj-M6-M18 | ⊦ M6 ≠ M18 | An Axiom |
| disj-I9-M4 | ⊦ I9 ≠ M4 | An Axiom |
| disj-M14-M17 | ⊦ M14 ≠ M17 | An Axiom |
| disj-I12-M13 | ⊦ I12 ≠ M13 | An Axiom |
| disj-I2-I14 | ⊦ I2 ≠ I14 | An Axiom |
| disj-M10-M11 | ⊦ M10 ≠ M11 | An Axiom |
| disj-M1-M17 | ⊦ M1 ≠ M17 | An Axiom |
| disj-doINSERT-invMEMBER | ⊦ doINSERT(tid, b) ≠ invMEMBER(tid0, invINSERTe) | An Axiom |
| gstepf-I14 | ⊦ gstepf(gs, ls, I14, τ) = gs | An Axiom |
| disj-M1-M4 | ⊦ M1 ≠ M4 | An Axiom |
| disj-retINSERT-retMEMBER | ⊦ retINSERT(tid, b) ≠ retMEMBER(tid0, b0) | An Axiom |
| pre-I16 | ⊦ pre(gs, ls, I16, a) ↔ a = τ | An Axiom |
| disj-I16-M13 | ⊦ I16 ≠ M13 | An Axiom |
| disj-I9-M7 | ⊦ I9 ≠ M7 | An Axiom |
| pcstepf-M1 | ⊦ pcstepf(gs, ls, M1, a) = M2 | An Axiom |
| disj-I5-I19 | ⊦ I5 ≠ I19 | An Axiom |
| updsel--dotn0-dotn | ⊦ (ls.n0:= sz0).n = ls.n | An Axiom |
| disj-I21-M13 | ⊦ I21 ≠ M13 | An Axiom |
| disj-I3-M7 | ⊦ I3 ≠ M7 | An Axiom |
| disj-M1-M11 | ⊦ M1 ≠ M11 | An Axiom |
| disj-I18-M12 | ⊦ I18 ≠ M12 | An Axiom |
| updsel--dotn-dotsz | ⊦ (ls.n:= sz1).sz = ls.sz | An Axiom |
| disj-I4-I21 | ⊦ I4 ≠ I21 | An Axiom |
| disj-I16-M2 | ⊦ I16 ≠ M2 | An Axiom |
| disj-I13-I21 | ⊦ I13 ≠ I21 | An Axiom |
| disj-I21-idle | ⊦ I21 ≠ idle | An Axiom |
| disj-I20-M6 | ⊦ I20 ≠ M6 | An Axiom |
| disj-I4-M11 | ⊦ I4 ≠ M11 | An Axiom |
| disj-I10-M2 | ⊦ I10 ≠ M2 | An Axiom |
| disj-I6-I14 | ⊦ I6 ≠ I14 | An Axiom |
| case-HashsetState | ⊦ mkstate(s.gstate, s.lsf, s.pcf) = s | An Axiom |
| disj-M5-M17 | ⊦ M5 ≠ M17 | An Axiom |
| disj-I7-M7 | ⊦ I7 ≠ M7 | An Axiom |
| disj-I20-M18 | ⊦ I20 ≠ M18 | An Axiom |
| disj-I17-M17 | ⊦ I17 ≠ M17 | An Axiom |
| disj-I1-M18 | ⊦ I1 ≠ M18 | An Axiom |
| gstepf-M10 | ⊦ gstepf(gs, ls, M10, τ) = gs | An Axiom |
| disj-I13-M11 | ⊦ I13 ≠ M11 | An Axiom |
| gen-HashsetLState | HashsetLState freely generated by mkls; | An Axiom |
| pre-M4 | ⊦ pre(gs, ls, M4, a) ↔ a = τ | An Axiom |
| disj-M2-M15 | ⊦ M2 ≠ M15 | An Axiom |
| disj-I14-M2 | ⊦ I14 ≠ M2 | An Axiom |
| pre-M12 | ⊦ pre(gs, ls, M12, a) ↔ a = retMEMBER(ls.tid, ls.b) | An Axiom |
| disj-I12-M16 | ⊦ I12 ≠ M16 | An Axiom |
| updsel--dotn0-dote | ⊦ (ls.n0:= sz0).e = ls.e | An Axiom |
| disj-I6-I20 | ⊦ I6 ≠ I20 | An Axiom |
| disj-I5-I10 | ⊦ I5 ≠ I10 | An Axiom |
| disj-I14-I19 | ⊦ I14 ≠ I19 | An Axiom |
| disj-I5-M15 | ⊦ I5 ≠ M15 | An Axiom |
| disj-M7-M16 | ⊦ M7 ≠ M16 | An Axiom |
| disj-I9-M12 | ⊦ I9 ≠ M12 | An Axiom |
| disj-M6-M12 | ⊦ M6 ≠ M12 | An Axiom |
| gstepf-M1 | ⊦ gstepf(gs, ls, M1, τ) = gs | An Axiom |
| disj-I5-M7 | ⊦ I5 ≠ M7 | An Axiom |
| updsel--dotsz-dotn | ⊦ (ls.sz:= sz).n = ls.n | An Axiom |
| disj-I18-M2 | ⊦ I18 ≠ M2 | An Axiom |
| disj-M3-M4 | ⊦ M3 ≠ M4 | An Axiom |
| disj-M7-idle | ⊦ M7 ≠ idle | An Axiom |
| lstepf-I6 | ⊦ lstepf(gs, ls, I6, a) = ls.e0:= gs.ar[ls.n] | An Axiom |
| disj-M10-M14 | ⊦ M10 ≠ M14 | An Axiom |
| disj-I13-I15 | ⊦ I13 ≠ I15 | An Axiom |
| disj-I12-M2 | ⊦ I12 ≠ M2 | An Axiom |
| upd-mkls-dotsz | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).sz:= sz2 = mkls(tid, e, b, sz2, sz0, sz1, e0) | An Axiom |
| disj-I6-M10 | ⊦ I6 ≠ M10 | An Axiom |
| disj-I4-I15 | ⊦ I4 ≠ I15 | An Axiom |
| gstepf-I20 | ⊦ gstepf(gs, ls, I20, τ) = gs | An Axiom |
| updsel--dotsz-dote | ⊦ (ls.sz:= sz).e = ls.e | An Axiom |
| disj-I1-M7 | ⊦ I1 ≠ M7 | An Axiom |
| disj-M15-idle | ⊦ M15 ≠ idle | An Axiom |
| disj-I9-I16 | ⊦ I9 ≠ I16 | An Axiom |
| disj-I1-I13 | ⊦ I1 ≠ I13 | An Axiom |
| pre-I5 | ⊦ pre(gs, ls, I5, a) ↔ a = τ | An Axiom |
| disj-I12-M10 | ⊦ I12 ≠ M10 | An Axiom |
| disj-I8-I15 | ⊦ I8 ≠ I15 | An Axiom |
| gstepf-M4 | ⊦ gstepf(gs, ls, M4, τ) = gs | An Axiom |
| disj-I12-M5 | ⊦ I12 ≠ M5 | An Axiom |
| disj-M2-idle | ⊦ M2 ≠ idle | An Axiom |
| pcstepf-I2 | ⊦ pcstepf(gs, ls, I2, a) = I3 | An Axiom |
| inj-doINSERT | ⊦ doINSERT(tid, b) = doINSERT(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| disj-I4-I18 | ⊦ I4 ≠ I18 | An Axiom |
| disj-M9-M17 | ⊦ M9 ≠ M17 | An Axiom |
| disj-M5-M7 | ⊦ M5 ≠ M7 | An Axiom |
| lstepf-I20 | ⊦ lstepf(gs, ls, I20, τ) = ls | An Axiom |
| disj-I3-I8 | ⊦ I3 ≠ I8 | An Axiom |
| inj-mkstate | ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0 | An Axiom |
| inj-retINSERT | ⊦ retINSERT(tid, b) = retINSERT(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0) | An Axiom |
| disj-M5-M11 | ⊦ M5 ≠ M11 | An Axiom |
| hashsetStep | ⊦ hashsetStep(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 |
| disj-I17-M9 | ⊦ I17 ≠ M9 | An Axiom |
| disj-I15-M12 | ⊦ I15 ≠ M12 | An Axiom |
| gstepf-I2 | ⊦ gstepf(gs, ls, I2, τ) = gs | An Axiom |
| disj-I13-M9 | ⊦ I13 ≠ M9 | An Axiom |
| disj-I11-M15 | ⊦ I11 ≠ M15 | An Axiom |
| pre-I10 | ⊦ pre(gs, ls, I10, a) ↔ a = τ | An Axiom |
| disj-I3-I20 | ⊦ I3 ≠ I20 | An Axiom |
| updsel--dotn0-dottid | ⊦ (ls.n0:= sz0).tid = ls.tid | An Axiom |
| pre-I19 | ⊦ pre(gs, ls, I19, a) ↔ a = retINSERT(ls.tid, ls.b) | An Axiom |
| disj-I12-I14 | ⊦ I12 ≠ I14 | An Axiom |
| disj-I7-I8 | ⊦ I7 ≠ I8 | An Axiom |
| disj-I9-I19 | ⊦ I9 ≠ I19 | An Axiom |
| disj-I3-M10 | ⊦ I3 ≠ M10 | An Axiom |
| disj-I10-M5 | ⊦ I10 ≠ M5 | An Axiom |
| disj-M3-M7 | ⊦ M3 ≠ M7 | An Axiom |
| disj-M10-M17 | ⊦ M10 ≠ M17 | An Axiom |
| disj-I5-I13 | ⊦ I5 ≠ I13 | An Axiom |
| disj-I21-M4 | ⊦ I21 ≠ M4 | An Axiom |
| disj-M4-M16 | ⊦ M4 ≠ M16 | An Axiom |
| disj-I3-M1 | ⊦ I3 ≠ M1 | An Axiom |
| pcstepf-M15 | ⊦ pcstepf(gs, ls, M15, a) = M16 | An Axiom |
| disj-I15-M9 | ⊦ I15 ≠ M9 | An Axiom |
| lstepf-I15-b | ⊦ ls.tid = tid ∧ ls.b → lstepf(gs, ls, I15, retINSERT(tid, true)) = ls | A User Theorem |
| disj-I2-M5 | ⊦ I2 ≠ M5 | An Axiom |
| disj-I4-M5 | ⊦ I4 ≠ M5 | An Axiom |
| disj-I8-M5 | ⊦ I8 ≠ M5 | An Axiom |
| HashsetLInv | ⊦ HashsetLInv(gs, ls, pc) ↔ (pc = I7 ∨ pc = I10 → ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ (pc = I8 ∨ pc = I14 → ls.e = ls.e0) ∧ (pc = I10 ∨ pc = I11 → ls.e ≠ ls.e0) ∧ (pc = I11 → ls.e0 ≠ ⊥ ∧ ls.e0 = gs.ar[ls.n]) ∧ (pc = I13 → gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] = ls.e0) ∧ (pc = I14 ∨ pc = I15 → ls.e = gs.ar[ls.n]) ∧ (pc = I16 → gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ ( pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I20 → allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ (pc = I17 → allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ (pc = I18 ∨ pc = I19 → allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true)) ∧ (pc = I20 → ls.n ≠ ls.n0) ∧ (pc = I8 ∨ pc = I9 → ls.e = gs.ar[ls.n]) ∧ ( pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17 → ls.n < # gs.ar) ∧ ( pc = I1 ∨ pc = I2 ∨ pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M1 ∨ pc = M2 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17 → ls.e ≠ ⊥) ∧ ( pc = I2 ∨ pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M2 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17 → ls.sz = # gs.ar) ∧ ( pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17 → ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ (pc = I4 ∨ pc = M4 → ls.n = ls.n0) ∧ ( pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17 → ¬ ls.b) ∧ (pc = I9 ∨ pc = I15 ∨ pc = M9 → ls.b) ∧ (pc = I21 ∨ pc = M18 → false) ∧ (pc = M7 ∨ pc = M10 → ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ (pc = M8 ∨ pc = M9 → (∃ n. n < # gs.ar ∧ gs.ar[n] = ls.e)) ∧ (pc = M13 → gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ (pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 → ls.e ≠ ls.e0) ∧ (pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M13 ∨ pc = M17 → allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ (pc = M14 → allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ (pc = M15 ∨ pc = M16 → allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true)) ∧ (pc = M17 → ls.n ≠ ls.n0) | An Axiom |
| disj-I9-I10 | ⊦ I9 ≠ I10 | An Axiom |
| disj-I11-I19 | ⊦ I11 ≠ I19 | An Axiom |
| sel-doINSERT-dottid | ⊦ doINSERT(tid, b).tid = tid | An Axiom |
| disj-I4-M14 | ⊦ I4 ≠ M14 | An Axiom |
| lstepf-M10 | ⊦ lstepf(gs, ls, M10, τ) = ls | An Axiom |
| disj-M1-M14 | ⊦ M1 ≠ M14 | An Axiom |
| updsel--dotsz-dote0 | ⊦ (ls.sz:= sz).e0 = ls.e0 | An Axiom |
| disj-I5-I8 | ⊦ I5 ≠ I8 | An Axiom |
| updsel--dotpcf-dotgstate | ⊦ (s.pcf:= pcf).gstate = s.gstate | An Axiom |
| disj-doMEMBER-invMEMBER | ⊦ doMEMBER(tid) ≠ invMEMBER(tid0, invINSERTe) | An Axiom |
| disj-I13-I18 | ⊦ I13 ≠ I18 | An Axiom |
| disj-I17-I21 | ⊦ I17 ≠ I21 | An Axiom |
| disj-I20-M12 | ⊦ I20 ≠ M12 | An Axiom |
| disj-I19-M9 | ⊦ I19 ≠ M9 | An Axiom |
| lstepf-M12-b | ⊦ ls.tid = tid ∧ ¬ ls.b → lstepf(gs, ls, M12, retMEMBER(tid, false)) = ls | A User Theorem |
| disj-I17-M11 | ⊦ I17 ≠ M11 | An Axiom |
| disj-I8-M11 | ⊦ I8 ≠ M11 | An Axiom |
| disj-I1-M1 | ⊦ I1 ≠ M1 | An Axiom |
| disj-I12-I20 | ⊦ I12 ≠ I20 | An Axiom |
| updsel--dotpcf-dotlsf | ⊦ (s.pcf:= pcf).lsf = s.lsf | An Axiom |
| pcstepf-M4 | ⊦ pcstepf(gs, ls, M4, a) = M5 | An Axiom |
| disj-I14-M5 | ⊦ I14 ≠ M5 | An Axiom |
| pre-M15 | ⊦ pre(gs, ls, M15, a) ↔ a = τ | An Axiom |
| disj-I6-M5 | ⊦ I6 ≠ M5 | An Axiom |
| updsel--dotb-dotn0 | ⊦ (ls.b:= b).n0 = ls.n0 | An Axiom |
| disj-I9-M15 | ⊦ I9 ≠ M15 | An Axiom |
| gen-HashsetGState | HashsetGState freely generated by mkgs; | An Axiom |
| disj-I1-I8 | ⊦ I1 ≠ I8 | An Axiom |
| disj-I3-I14 | ⊦ I3 ≠ I14 | An Axiom |
| disj-M1-M7 | ⊦ M1 ≠ M7 | An Axiom |
| disj-I5-M18 | ⊦ I5 ≠ M18 | An Axiom |
| disj-M6-M15 | ⊦ M6 ≠ M15 | An Axiom |
| disj-I16-M16 | ⊦ I16 ≠ M16 | An Axiom |
| disj-I8-I21 | ⊦ I8 ≠ I21 | An Axiom |
| pcstepf-M18 | ⊦ pcstepf(gs, ls, M18, a) = idle | An Axiom |
| disj-I17-I18 | ⊦ I17 ≠ I18 | An Axiom |
| pre-I8 | ⊦ pre(gs, ls, I8, a) ↔ a = τ | An Axiom |
| disj-I6-M8 | ⊦ I6 ≠ M8 | An Axiom |
| disj-doINSERT-invINSERT | ⊦ doINSERT(tid, b) ≠ invINSERT(tid0, invINSERTe) | An Axiom |
| disj-I9-M18 | ⊦ I9 ≠ M18 | An Axiom |
| disj-I8-M14 | ⊦ I8 ≠ M14 | An Axiom |
| disj-I16-I20 | ⊦ I16 ≠ I20 | An Axiom |
| disj-I12-I17 | ⊦ I12 ≠ I17 | An Axiom |
| pcstepf-I5 | ⊦ pcstepf(gs, ls, I5, a) = (¬ ls.b ⊃ I6;I21) | An Axiom |
| disj-I3-I17 | ⊦ I3 ≠ I17 | An Axiom |
| disj-I15-idle | ⊦ I15 ≠ idle | An Axiom |
| disj-I13-M3 | ⊦ I13 ≠ M3 | An Axiom |
| disj-M2-M5 | ⊦ M2 ≠ M5 | An Axiom |
| pcstepf-I13 | ⊦ pcstepf(gs, ls, I13, a) = (ls.e0 = ls.e ⊃ I14;I16) | An Axiom |
| disj-M4-M10 | ⊦ M4 ≠ M10 | An Axiom |
| sel-invMEMBER-dottid | ⊦ invMEMBER(tid, invINSERTe).tid = tid | An Axiom |
| disj-I2-M8 | ⊦ I2 ≠ M8 | An Axiom |
| disj-M12-M18 | ⊦ M12 ≠ M18 | An Axiom |
| disj-I7-I14 | ⊦ I7 ≠ I14 | An Axiom |
| disj-I10-M14 | ⊦ I10 ≠ M14 | An Axiom |
| gstepf-idle | ⊦ gstepf(gs, ls, idle, a) = gs | An Axiom |
| disj-I4-M8 | ⊦ I4 ≠ M8 | An Axiom |
| disj-M8-M16 | ⊦ M8 ≠ M16 | An Axiom |
| disj-I17-M3 | ⊦ I17 ≠ M3 | An Axiom |
| disj-I8-I18 | ⊦ I8 ≠ I18 | An Axiom |
| lstepf-M13 | ⊦ lstepf(gs, ls, M13, τ) = ls.n:= ((ls.n + 1) % ls.sz) | An Axiom |
| gstepf-I5 | ⊦ gstepf(gs, ls, I5, τ) = gs | An Axiom |
| updsel--dotar-dotar | ⊦ (gs.ar:= ar).ar = ar | An Axiom |
| disj-I2-M18 | ⊦ I2 ≠ M18 | An Axiom |
| disj-I4-I12 | ⊦ I4 ≠ I12 | An Axiom |
| updsel--dote-dotn0 | ⊦ (ls.e:= e).n0 = ls.n0 | An Axiom |
| disj-M3-M15 | ⊦ M3 ≠ M15 | An Axiom |
| disj-I7-I20 | ⊦ I7 ≠ I20 | An Axiom |
| updsel--dotsz-dotb | ⊦ (ls.sz:= sz).b ↔ ls.b | An Axiom |
| disj-I6-idle | ⊦ I6 ≠ idle | An Axiom |
| disj-I15-I19 | ⊦ I15 ≠ I19 | An Axiom |
| disj-M9-M11 | ⊦ M9 ≠ M11 | An Axiom |
| pre-I13 | ⊦ pre(gs, ls, I13, a) ↔ a = τ | An Axiom |
| disj-I19-M12 | ⊦ I19 ≠ M12 | An Axiom |
| disj-I9-I13 | ⊦ I9 ≠ I13 | An Axiom |
| disj-I11-I13 | ⊦ I11 ≠ I13 | An Axiom |
| updsel--dote-dotb | ⊦ (ls.e:= e).b ↔ ls.b | An Axiom |
| disj-I14-I21 | ⊦ I14 ≠ I21 | An Axiom |
| disj-I1-I2 | ⊦ I1 ≠ I2 | An Axiom |
| disj-I3-M13 | ⊦ I3 ≠ M13 | An Axiom |
| disj-I11-M18 | ⊦ I11 ≠ M18 | An Axiom |
| disj-I21-M7 | ⊦ I21 ≠ M7 | An Axiom |
| disj-I15-M3 | ⊦ I15 ≠ M3 | An Axiom |
| disj-I19-M3 | ⊦ I19 ≠ M3 | An Axiom |
| disj-I16-M10 | ⊦ I16 ≠ M10 | An Axiom |
| disj-I7-M10 | ⊦ I7 ≠ M10 | An Axiom |
| disj-I8-M8 | ⊦ I8 ≠ M8 | An Axiom |
| lstepf-M4 | ⊦ lstepf(gs, ls, M4, τ) = ls.b:= false | An Axiom |
| disj-I10-I18 | ⊦ I10 ≠ I18 | An Axiom |
| disj-M4-M5 | ⊦ M4 ≠ M5 | An Axiom |
| disj-I11-M3 | ⊦ I11 ≠ M3 | An Axiom |
| lstepf-I17 | ⊦ lstepf(gs, ls, I17, τ) = ls | An Axiom |
| disj-I4-M17 | ⊦ I4 ≠ M17 | An Axiom |
| disj-M5-M14 | ⊦ M5 ≠ M14 | An Axiom |
| disj-I15-M15 | ⊦ I15 ≠ M15 | An Axiom |
| disj-M2-M8 | ⊦ M2 ≠ M8 | An Axiom |
| disj-M4-M13 | ⊦ M4 ≠ M13 | An Axiom |
| pre-I2 | ⊦ pre(gs, ls, I2, a) ↔ a = τ | An Axiom |
| pcstepf-M12 | ⊦ pcstepf(gs, ls, M12, a) = idle | An Axiom |
| disj-I10-I12 | ⊦ I10 ≠ I12 | An Axiom |
| disj-I2-M2 | ⊦ I2 ≠ M2 | An Axiom |
| disj-I7-I17 | ⊦ I7 ≠ I17 | An Axiom |
| disj-I1-idle | ⊦ I1 ≠ idle | An Axiom |
| disj-M16-idle | ⊦ M16 ≠ idle | An Axiom |
| disj-M8-idle | ⊦ M8 ≠ idle | An Axiom |
| disj-I8-M17 | ⊦ I8 ≠ M17 | An Axiom |
| disj-I10-M17 | ⊦ I10 ≠ M17 | An Axiom |
| updsel--dote0-dotn0 | ⊦ (ls.e0:= e0).n0 = ls.n0 | An Axiom |
| disj-I3-I5 | ⊦ I3 ≠ I5 | An Axiom |
| updsel--dottid-dotn0 | ⊦ (ls.tid:= tid).n0 = ls.n0 | An Axiom |
| disj-I2-I16 | ⊦ I2 ≠ I16 | An Axiom |
| disj-I2-I9 | ⊦ I2 ≠ I9 | An Axiom |
| lstepf-M16 | ⊦ ls.tid = tid → lstepf(gs, ls, M16, retMEMBER(tid, ls.b)) = ls | An Axiom |
| gstepf-I8 | ⊦ gstepf(gs, ls, I8, τ) = gs | An Axiom |
| disj-I17-M6 | ⊦ I17 ≠ M6 | An Axiom |
| updsel--dote-dotn | ⊦ (ls.e:= e).n = ls.n | An Axiom |
| disj-I8-I9 | ⊦ I8 ≠ I9 | An Axiom |
| disj-M3-M18 | ⊦ M3 ≠ M18 | An Axiom |
| disj-I6-M2 | ⊦ I6 ≠ M2 | An Axiom |
| disj-I6-I13 | ⊦ I6 ≠ I13 | An Axiom |
| upd-mkstate-dotpcf | ⊦ (mkstate(gstate, lsf, pcf).pcf:= pcf0) = mkstate(gstate, lsf, pcf0) | An Axiom |
| updsel--dotsz-dotsz | ⊦ (ls.sz:= sz).sz = sz | An Axiom |
| pcstepf-I16 | ⊦ pcstepf(gs, ls, I16, a) = I17 | An Axiom |
| disj-M9-M14 | ⊦ M9 ≠ M14 | An Axiom |
| disj-I11-I16 | ⊦ I11 ≠ I16 | An Axiom |
| gstepf-I13 | ⊦ gstepf(gs, ls, I13, τ) = gs | An Axiom |
| disj-I13-M6 | ⊦ I13 ≠ M6 | An Axiom |
| updsel--dote-dote | ⊦ (ls.e:= e).e = e | An Axiom |
| disj-M6-M8 | ⊦ M6 ≠ M8 | An Axiom |
| disj-I21-M1 | ⊦ I21 ≠ M1 | An Axiom |
| sel-mkgs-dotar | ⊦ mkgs(ar).ar = ar | An Axiom |
| elim-mkgs | ⊦ ar = gs.ar ↔ gs = mkgs(ar) | An Axiom |
| disj-I16-I17 | ⊦ I16 ≠ I17 | An Axiom |
| disj-I20-M5 | ⊦ I20 ≠ M5 | An Axiom |
| disj-I10-idle | ⊦ I10 ≠ idle | An Axiom |
| disj-M11-M17 | ⊦ M11 ≠ M17 | An Axiom |
| disj-I18-I21 | ⊦ I18 ≠ I21 | An Axiom |
| disj-I7-M13 | ⊦ I7 ≠ M13 | An Axiom |
| disj-M8-M10 | ⊦ M8 ≠ M10 | An Axiom |
| lstepf-M7 | ⊦ lstepf(gs, ls, M7, τ) = ls | An Axiom |
| disj-doINSERT-doMEMBER | ⊦ doINSERT(tid, b) ≠ doMEMBER(tid0) | An Axiom |
| disj-M16-M18 | ⊦ M16 ≠ M18 | An Axiom |
| disj-I9-M6 | ⊦ I9 ≠ M6 | An Axiom |
| disj-I2-M12 | ⊦ I2 ≠ M12 | An Axiom |
| disj-I14-M14 | ⊦ I14 ≠ M14 | An Axiom |
| disj-I4-I9 | ⊦ I4 ≠ I9 | An Axiom |
| lstepf-I11 | ⊦ lstepf(gs, ls, I11, τ) = ls.n:= ((ls.n + 1) % ls.sz) | An Axiom |
| disj-I11-M6 | ⊦ I11 ≠ M6 | An Axiom |
| disj-M4-M8 | ⊦ M4 ≠ M8 | An Axiom |
| disj-I4-M2 | ⊦ I4 ≠ M2 | An Axiom |
| disj-I15-M18 | ⊦ I15 ≠ M18 | An Axiom |
| disj-M13-M16 | ⊦ M13 ≠ M16 | An Axiom |
| disj-I8-I12 | ⊦ I8 ≠ I12 | An Axiom |
| disj-I6-M18 | ⊦ I6 ≠ M18 | An Axiom |
| disj-I11-M12 | ⊦ I11 ≠ M12 | An Axiom |
| disj-M7-M15 | ⊦ M7 ≠ M15 | An Axiom |
| disj-I1-I5 | ⊦ I1 ≠ I5 | An Axiom |
| case-HashsetPC | ⊦ pc = I1 ∨ pc = I2 ∨ pc = I3 ∨ pc = I4 ∨ pc = I5 ∨ pc = I6 ∨ pc = I7 ∨ pc = I8 ∨ pc = I9 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I13 ∨ pc = I14 ∨ pc = I15 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I19 ∨ pc = I20 ∨ pc = I21 ∨ pc = M1 ∨ pc = M2 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M7 ∨ pc = M8 ∨ pc = M9 ∨ pc = M10 ∨ pc = M11 ∨ pc = M12 ∨ pc = M13 ∨ pc = M14 ∨ pc = M15 ∨ pc = M16 ∨ pc = M17 ∨ pc = M18 ∨ pc = idle | An Axiom |
| disj-I1-M17 | ⊦ I1 ≠ M17 | An Axiom |
| disj-I3-I11 | ⊦ I3 ≠ I11 | An Axiom |
| pcstepf-I8 | ⊦ pcstepf(gs, ls, I8, a) = I9 | An Axiom |
| gstepf-M18 | ⊦ ls.tid = tid → gstepf(gs, ls, M18, retMEMBER(tid, b)) = gs | An Axiom |
| disj-I15-M6 | ⊦ I15 ≠ M6 | An Axiom |
| disj-I19-M15 | ⊦ I19 ≠ M15 | An Axiom |
| disj-M2-M14 | ⊦ M2 ≠ M14 | An Axiom |
| disj-I19-M6 | ⊦ I19 ≠ M6 | An Axiom |
| disj-I6-I9 | ⊦ I6 ≠ I9 | An Axiom |
| disj-I14-I18 | ⊦ I14 ≠ I18 | An Axiom |
| disj-I8-M2 | ⊦ I8 ≠ M2 | An Axiom |
| disj-I3-M16 | ⊦ I3 ≠ M16 | An Axiom |
| disj-I16-M4 | ⊦ I16 ≠ M4 | An Axiom |
| disj-I13-I17 | ⊦ I13 ≠ I17 | An Axiom |
| disj-I12-M4 | ⊦ I12 ≠ M4 | An Axiom |
| disj-I6-M12 | ⊦ I6 ≠ M12 | An Axiom |
| disj-I10-I21 | ⊦ I10 ≠ I21 | An Axiom |
| disj-M12-M15 | ⊦ M12 ≠ M15 | An Axiom |
| disj-I20-M8 | ⊦ I20 ≠ M8 | An Axiom |
| gstepf-M12 | ⊦ ls.tid = tid → gstepf(gs, ls, M12, retMEMBER(tid, b)) = gs | An Axiom |
| disj-doMEMBER-invINSERT | ⊦ doMEMBER(tid) ≠ invINSERT(tid0, invINSERTe) | An Axiom |
| disj-I19-M18 | ⊦ I19 ≠ M18 | An Axiom |
| disj-I7-M9 | ⊦ I7 ≠ M9 | An Axiom |
| disj-M1-M13 | ⊦ M1 ≠ M13 | An Axiom |
| disj-I1-I15 | ⊦ I1 ≠ I15 | An Axiom |
| pre-M6 | ⊦ pre(gs, ls, M6, a) ↔ a = (gs.ar[ls.n] = ls.e ∨ gs.ar[ls.n] = ⊥ ∨ (ls.n + 1) % ls.sz = ls.n0 ⊃ doMEMBER(ls.tid);τ) | An Axiom |
| disj-I14-M4 | ⊦ I14 ≠ M4 | An Axiom |
| disj-M2-M17 | ⊦ M2 ≠ M17 | An Axiom |
| pcstepf-M3 | ⊦ pcstepf(gs, ls, M3, a) = M4 | An Axiom |
| disj-I7-M16 | ⊦ I7 ≠ M16 | An Axiom |
| disj-I2-I10 | ⊦ I2 ≠ I10 | An Axiom |
| disj-M8-M13 | ⊦ M8 ≠ M13 | An Axiom |
| disj-I10-I15 | ⊦ I10 ≠ I15 | An Axiom |
| disj-I2-I3 | ⊦ I2 ≠ I3 | An Axiom |
| disj-I21-M15 | ⊦ I21 ≠ M15 | An Axiom |
| disj-I2-M15 | ⊦ I2 ≠ M15 | An Axiom |
| gstepf-M3 | ⊦ gstepf(gs, ls, M3, τ) = gs | An Axiom |
| disj-M3-M12 | ⊦ M3 ≠ M12 | An Axiom |
| disj-I18-M4 | ⊦ I18 ≠ M4 | An Axiom |
| lstepf-I8 | ⊦ lstepf(gs, ls, I8, τ) = ls.b:= true | An Axiom |
| disj-I15-I16 | ⊦ I15 ≠ I16 | An Axiom |
| disj-M10-M16 | ⊦ M10 ≠ M16 | An Axiom |
| disj-I6-I16 | ⊦ I6 ≠ I16 | An Axiom |
| disj-I17-I20 | ⊦ I17 ≠ I20 | An Axiom |
| sel-mkstate-dotpcf | ⊦ mkstate(gstate, lsf, pcf).pcf = pcf | An Axiom |
| pcstepf-I19 | ⊦ pcstepf(gs, ls, I19, a) = idle | An Axiom |
| disj-I1-I21 | ⊦ I1 ≠ I21 | An Axiom |
| disj-M7-M18 | ⊦ M7 ≠ M18 | An Axiom |
| updsel--dotlsf-dotgstate | ⊦ (s.lsf:= lsf).gstate = s.gstate | An Axiom |
| disj-M3-idle | ⊦ M3 ≠ idle | An Axiom |
| gstepf-I16 | ⊦ gstepf(gs, ls, I16, τ) = gs | An Axiom |
| disj-I1-M9 | ⊦ I1 ≠ M9 | An Axiom |
| disj-I5-M9 | ⊦ I5 ≠ M9 | An Axiom |
| disj-invINSERT-retMEMBER | ⊦ invINSERT(tid, invINSERTe) ≠ retMEMBER(tid0, b) | An Axiom |
| disj-M15-M17 | ⊦ M15 ≠ M17 | An Axiom |
| disj-I13-M13 | ⊦ I13 ≠ M13 | An Axiom |
| pcstepf-I10 | ⊦ pcstepf(gs, ls, I10, a) = (ls.e0 ≠ ⊥ ⊃ I11;I12) | An Axiom |
| updsel--dote0-dottid | ⊦ (ls.e0:= e0).tid = ls.tid | An Axiom |
| disj-I14-M17 | ⊦ I14 ≠ M17 | An Axiom |
| lstepf-M1 | ⊦ lstepf(gs, ls, M1, τ) = ls.sz:= # gs.ar | An Axiom |
| disj-I18-M14 | ⊦ I18 ≠ M14 | An Axiom |
| disj-I7-I11 | ⊦ I7 ≠ I11 | An Axiom |
| disj-I5-M17 | ⊦ I5 ≠ M17 | An Axiom |
| disj-I10-M11 | ⊦ I10 ≠ M11 | An Axiom |
| disj-I9-M9 | ⊦ I9 ≠ M9 | An Axiom |
| disj-M6-M14 | ⊦ M6 ≠ M14 | An Axiom |
| disj-M10-idle | ⊦ M10 ≠ idle | An Axiom |
| disj-I1-M11 | ⊦ I1 ≠ M11 | An Axiom |
| lstepf-I14 | ⊦ lstepf(gs, ls, I14, τ) = ls.b:= true | An Axiom |
| disj-I11-M9 | ⊦ I11 ≠ M9 | An Axiom |
| disj-I2-I19 | ⊦ I2 ≠ I19 | An Axiom |
| disj-I3-M9 | ⊦ I3 ≠ M9 | An Axiom |
| disj-I5-I21 | ⊦ I5 ≠ I21 | An Axiom |
| disj-M1-M16 | ⊦ M1 ≠ M16 | An Axiom |
| gstepf-I19 | ⊦ ls.tid = tid → gstepf(gs, ls, I19, retINSERT(tid, b)) = gs | An Axiom |
| pre-I12 | ⊦ pre(gs, ls, I12, a) ↔ a = (gs.ar[ls.n] = ⊥ ∨ gs.ar[ls.n] = ls.e ⊃ doINSERT(ls.tid, true);τ) | An Axiom |
| disj-M1-M9 | ⊦ M1 ≠ M9 | An Axiom |
| disj-I5-M11 | ⊦ I5 ≠ M11 | An Axiom |
| disj-I20-M14 | ⊦ I20 ≠ M14 | An Axiom |
| disj-I7-idle | ⊦ I7 ≠ idle | An Axiom |
| disj-M11-M14 | ⊦ M11 ≠ M14 | An Axiom |
| disj-I9-M3 | ⊦ I9 ≠ M3 | An Axiom |
| pre-M9 | ⊦ pre(gs, ls, M9, a) ↔ a = retMEMBER(ls.tid, ls.b) | An Axiom |
| pcstepf-M6 | ⊦ pcstepf(gs, ls, M6, a) = M7 | An Axiom |
| upd-mkstate-dotgstate | ⊦ (mkstate(gstate, lsf, pcf).gstate:= gstate0) = mkstate(gstate0, lsf, pcf) | An Axiom |
| disj-I3-M3 | ⊦ I3 ≠ M3 | An Axiom |
| disj-I2-I6 | ⊦ I2 ≠ I6 | An Axiom |
| disj-I21-M18 | ⊦ I21 ≠ M18 | An Axiom |
| disj-I18-M17 | ⊦ I18 ≠ M17 | An Axiom |
| disj-I9-M17 | ⊦ I9 ≠ M17 | An Axiom |
| disj-I14-M11 | ⊦ I14 ≠ M11 | An Axiom |
| disj-I4-I6 | ⊦ I4 ≠ I6 | An Axiom |
| disj-I12-I16 | ⊦ I12 ≠ I16 | An Axiom |
| disj-I4-M16 | ⊦ I4 ≠ M16 | An Axiom |
| disj-I6-I10 | ⊦ I6 ≠ I10 | An Axiom |
| disj-I10-M7 | ⊦ I10 ≠ M7 | An Axiom |
| disj-I18-M7 | ⊦ I18 ≠ M7 | An Axiom |
| disj-M3-M9 | ⊦ M3 ≠ M9 | An Axiom |
| disj-I6-I19 | ⊦ I6 ≠ I19 | An Axiom |
| disj-M5-M13 | ⊦ M5 ≠ M13 | An Axiom |
| disj-I17-idle | ⊦ I17 ≠ idle | An Axiom |
| disj-I20-M2 | ⊦ I20 ≠ M2 | An Axiom |
| gstepf-M15 | ⊦ gstepf(gs, ls, M15, τ) = gs | An Axiom |
| disj-I13-M16 | ⊦ I13 ≠ M16 | An Axiom |
| disj-I14-M7 | ⊦ I14 ≠ M7 | An Axiom |
| pre-M17 | ⊦ pre(gs, ls, M17, a) ↔ a = τ | An Axiom |
| sel-invMEMBER-dotinvMEMBERe | ⊦ invMEMBER(tid, invINSERTe).invMEMBERe = invINSERTe | An Axiom |
| disj-M7-M9 | ⊦ M7 ≠ M9 | An Axiom |
| disj-I14-I15 | ⊦ I14 ≠ I15 | An Axiom |
| disj-I5-I15 | ⊦ I5 ≠ I15 | An Axiom |
| disj-I7-M3 | ⊦ I7 ≠ M3 | An Axiom |
| inj-mkgs | ⊦ mkgs(ar) = mkgs(ar0) ↔ ar = ar0 | An Axiom |
| disj-M6-M17 | ⊦ M6 ≠ M17 | An Axiom |
| disj-I1-M3 | ⊦ I1 ≠ M3 | An Axiom |
| gstepf-M6 | ⊦ gstepf(gs, ls, M6, a) = gs | An Axiom |
| disj-I1-M14 | ⊦ I1 ≠ M14 | An Axiom |
| disj-M2-M11 | ⊦ M2 ≠ M11 | An Axiom |
| disj-M14-M16 | ⊦ M14 ≠ M16 | An Axiom |
| lstepf-I2 | ⊦ lstepf(gs, ls, I2, τ) = ls.n0:= get_hash(ls.e, ls.sz) | An Axiom |
| disj-I9-I12 | ⊦ I9 ≠ I12 | An Axiom |
| sel-mkls-dotb | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).b ↔ b | An Axiom |
| disj-I12-M12 | ⊦ I12 ≠ M12 | An Axiom |
| disj-I2-I13 | ⊦ I2 ≠ I13 | An Axiom |
| gen-HashsetAction | HashsetAction freely generated by τ, doINSERT, doMEMBER, invINSERT, invMEMBER, retINSERT, retMEMBER; | An Axiom |
| disj-I12-M7 | ⊦ I12 ≠ M7 | An Axiom |
| disj-I6-M15 | ⊦ I6 ≠ M15 | An Axiom |
| disj-I16-M7 | ⊦ I16 ≠ M7 | An Axiom |
| disj-M5-M9 | ⊦ M5 ≠ M9 | An Axiom |
| disj-M7-M12 | ⊦ M7 ≠ M12 | An Axiom |
| updsel--dotn0-dote0 | ⊦ (ls.n0:= sz0).e0 = ls.e0 | An Axiom |
| disj-I17-M13 | ⊦ I17 ≠ M13 | An Axiom |
| disj-I5-M3 | ⊦ I5 ≠ M3 | An Axiom |
| disj-I16-idle | ⊦ I16 ≠ idle | An Axiom |
| disj-doINSERT-tau | ⊦ doINSERT(tid, b) ≠ τ | An Axiom |
| disj-I1-I18 | ⊦ I1 ≠ I18 | An Axiom |
| gstepf-I10 | ⊦ gstepf(gs, ls, I10, τ) = gs | An Axiom |
| disj-I12-M15 | ⊦ I12 ≠ M15 | An Axiom |
| disj-I9-M11 | ⊦ I9 ≠ M11 | An Axiom |
| sel-mkls-dotn | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n = sz1 | An Axiom |
| disj-M10-M13 | ⊦ M10 ≠ M13 | An Axiom |
| disj-I1-I4 | ⊦ I1 ≠ I4 | An Axiom |
| disj-I4-I20 | ⊦ I4 ≠ I20 | An Axiom |
| disj-I16-M1 | ⊦ I16 ≠ M1 | An Axiom |
| gstepf-M9 | ⊦ ls.tid = tid → gstepf(gs, ls, M9, retMEMBER(tid, b)) = gs | An Axiom |
| pcstepf-I7 | ⊦ pcstepf(gs, ls, I7, a) = (ls.e = ls.e0 ⊃ I8;I10) | An Axiom |
| disj-I17-M5 | ⊦ I17 ≠ M5 | An Axiom |
| disj-I5-M6 | ⊦ I5 ≠ M6 | An Axiom |
| disj-I16-M12 | ⊦ I16 ≠ M12 | An Axiom |
| gstepf-I7 | ⊦ gstepf(gs, ls, I7, τ) = gs | An Axiom |
| disj-I9-I21 | ⊦ I9 ≠ I21 | An Axiom |
| disj-I20-M17 | ⊦ I20 ≠ M17 | An Axiom |
| disj-I17-M16 | ⊦ I17 ≠ M16 | An Axiom |
| disj-I12-M1 | ⊦ I12 ≠ M1 | An Axiom |
| pre-I21 | ⊦ pre(gs, ls, I21, a) ↔ a = retINSERT(ls.tid, ls.b) | An Axiom |
| pre-I15 | ⊦ pre(gs, ls, I15, a) ↔ a = retINSERT(ls.tid, ls.b) | An Axiom |
| disj-I13-M10 | ⊦ I13 ≠ M10 | An Axiom |
| disj-I11-I15 | ⊦ I11 ≠ I15 | An Axiom |
| disj-I4-M10 | ⊦ I4 ≠ M10 | An Axiom |
| disj-I14-M1 | ⊦ I14 ≠ M1 | An Axiom |
| updsel--dottid-dote0 | ⊦ (ls.tid:= tid).e0 = ls.e0 | An Axiom |
| HashsetRely | ⊦ HashsetRely(gs, tid, gs0) ↔ rely(gs.ar, gs0.ar) | An Axiom |
| disj-I3-M15 | ⊦ I3 ≠ M15 | An Axiom |
| disj-I5-I18 | ⊦ I5 ≠ I18 | An Axiom |
| disj-I21-M9 | ⊦ I21 ≠ M9 | An Axiom |
| disj-I3-M6 | ⊦ I3 ≠ M6 | An Axiom |
| disj-I1-I12 | ⊦ I1 ≠ I12 | An Axiom |
| disj-I18-M11 | ⊦ I18 ≠ M11 | An Axiom |
| disj-doINSERT-retMEMBER | ⊦ doINSERT(tid, b) ≠ retMEMBER(tid0, b0) | An Axiom |
| disj-I6-M1 | ⊦ I6 ≠ M1 | An Axiom |
| hashsetInit | ⊦ hashsetInit(mkstate(gs, lsf, pcf)) ↔ (∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle)) ∧ (∀ tid. lsf(tid).tid = tid) | An Axiom |
| disj-I13-I20 | ⊦ I13 ≠ I20 | An Axiom |
| disj-I8-M1 | ⊦ I8 ≠ M1 | An Axiom |
| disj-I9-I15 | ⊦ I9 ≠ I15 | An Axiom |
| disj-I12-I19 | ⊦ I12 ≠ I19 | An Axiom |
| disj-I3-I4 | ⊦ I3 ≠ I4 | An Axiom |
| updsel--dote0-dote0 | ⊦ (ls.e0:= e0).e0 = e0 | An Axiom |
| disj-I10-M1 | ⊦ I10 ≠ M1 | An Axiom |
| lstepf-I5 | ⊦ lstepf(gs, ls, I5, τ) = ls | An Axiom |
| disj-M4-M12 | ⊦ M4 ≠ M12 | An Axiom |
| disj-I11-idle | ⊦ I11 ≠ idle | An Axiom |
| disj-I21-M12 | ⊦ I21 ≠ M12 | An Axiom |
| disj-I4-I14 | ⊦ I4 ≠ I14 | An Axiom |
| disj-M9-idle | ⊦ M9 ≠ idle | An Axiom |
| upd-mkls-dotb | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).b:= b0 = mkls(tid, e, b0, sz, sz0, sz1, e0) | An Axiom |
| disj-I8-M16 | ⊦ I8 ≠ M16 | An Axiom |
| disj-I1-M6 | ⊦ I1 ≠ M6 | An Axiom |
| disj-M5-M16 | ⊦ M5 ≠ M16 | An Axiom |
| disj-M9-M13 | ⊦ M9 ≠ M13 | An Axiom |
| disj-I11-I21 | ⊦ I11 ≠ I21 | An Axiom |
| gen-HashsetState | HashsetState freely generated by mkstate; | An Axiom |
| sel-mkls-dotn0 | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n0 = sz0 | An Axiom |
| disj-M1-M10 | ⊦ M1 ≠ M10 | An Axiom |
| disj-I18-M1 | ⊦ I18 ≠ M1 | An Axiom |
| disj-I11-M11 | ⊦ I11 ≠ M11 | An Axiom |
| disj-I13-I14 | ⊦ I13 ≠ I14 | An Axiom |
| disj-I19-M5 | ⊦ I19 ≠ M5 | An Axiom |
| disj-M1-M3 | ⊦ M1 ≠ M3 | An Axiom |
| disj-I2-idle | ⊦ I2 ≠ idle | An Axiom |
| disj-I5-M14 | ⊦ I5 ≠ M14 | An Axiom |
| pre-M3 | ⊦ pre(gs, ls, M3, a) ↔ a = τ | An Axiom |
| disj-M17-idle | ⊦ M17 ≠ idle | An Axiom |
| disj-M6-M11 | ⊦ M6 ≠ M11 | An Axiom |
| pcstepf-I21 | ⊦ pcstepf(gs, ls, I21, a) = idle | An Axiom |
| inj-mkls | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0) = mkls(tid0, e1, b0, sz2, sz3, sz4, e2) ↔ tid = tid0 ∧ e = e1 ∧ (b ↔ b0) ∧ sz = sz2 ∧ sz0 = sz3 ∧ sz1 = sz4 ∧ e0 = e2 | An Axiom |
| case-HashsetLState | ⊦ mkls(ls.tid, ls.e, ls.b, ls.sz, ls.n0, ls.n, ls.e0) = ls | An Axiom |
| sel-retMEMBER-dotretMEMBERb | ⊦ retMEMBER(tid, b).retMEMBERb ↔ b | An Axiom |
| pcstepf-M9 | ⊦ pcstepf(gs, ls, M9, a) = idle | An Axiom |
| pre-I1 | ⊦ pre(gs, ls, I1, a) ↔ a = τ | An Axiom |
| pre-M11 | ⊦ pre(gs, ls, M11, a) ↔ a = τ | An Axiom |
| disj-M13-M15 | ⊦ M13 ≠ M15 | An Axiom |
| disj-I7-M6 | ⊦ I7 ≠ M6 | An Axiom |
| sel-mkls-dote | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e = e | An Axiom |
| disj-I6-M4 | ⊦ I6 ≠ M4 | An Axiom |
| disj-I8-I14 | ⊦ I8 ≠ I14 | An Axiom |
| disj-I11-M14 | ⊦ I11 ≠ M14 | An Axiom |
| inj-invMEMBER | ⊦ invMEMBER(tid, invINSERTe) = invMEMBER(tid0, invINSERTe0) ↔ tid = tid0 ∧ invINSERTe = invINSERTe0 | An Axiom |
| updsel--dottid-dotn | ⊦ (ls.tid:= tid).n = ls.n | An Axiom |
| disj-M1-M6 | ⊦ M1 ≠ M6 | An Axiom |
| case-HashsetGState | ⊦ mkgs(gs.ar) = gs | An Axiom |
| disj-M9-M16 | ⊦ M9 ≠ M16 | An Axiom |
| pre-I18 | ⊦ pre(gs, ls, I18, a) ↔ a = doINSERT(ls.tid, false) | An Axiom |
| updsel--dotn0-dotsz | ⊦ (ls.n0:= sz0).sz = ls.sz | An Axiom |
| disj-I13-M8 | ⊦ I13 ≠ M8 | An Axiom |
| disj-M4-M15 | ⊦ M4 ≠ M15 | An Axiom |
| sel-mkls-dottid | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).tid = tid | An Axiom |
| disj-I15-M11 | ⊦ I15 ≠ M11 | An Axiom |
| pre-I4 | ⊦ pre(gs, ls, I4, a) ↔ a = τ | An Axiom |
| disj-M13-M18 | ⊦ M13 ≠ M18 | An Axiom |
| disj-I16-I19 | ⊦ I16 ≠ I19 | An Axiom |
| disj-I10-I20 | ⊦ I10 ≠ I20 | An Axiom |
| pcstepf-M14 | ⊦ pcstepf(gs, ls, M14, a) = (ls.n = ls.n0 ⊃ M15;M17) | An Axiom |
| updsel--dottid-dote | ⊦ (ls.tid:= tid).e = ls.e | An Axiom |
| disj-I9-M14 | ⊦ I9 ≠ M14 | An Axiom |
| disj-I10-M10 | ⊦ I10 ≠ M10 | An Axiom |
| disj-I12-I13 | ⊦ I12 ≠ I13 | An Axiom |
| pcstepf-I1 | ⊦ pcstepf(gs, ls, I1, a) = I2 | An Axiom |
| disj-I3-I13 | ⊦ I3 ≠ I13 | An Axiom |
| elim-mkls | ⊦ (((((tid = ls.tid ∧ e = ls.e) ∧ (b ↔ ls.b)) ∧ sz = ls.sz) ∧ sz0 = ls.n0) ∧ n = ls.n) ∧ e0 = ls.e0 ↔ ls = mkls(tid, e, b, sz, sz0, n, e0) | An Axiom |
| lstepf-M9 | ⊦ ls.tid = tid → lstepf(gs, ls, M9, retMEMBER(tid, ls.b)) = ls | An Axiom |
| disj-I12-M18 | ⊦ I12 ≠ M18 | An Axiom |
| disj-I10-M4 | ⊦ I10 ≠ M4 | An Axiom |
| disj-I20-I21 | ⊦ I20 ≠ I21 | An Axiom |
| gstepf-I1 | ⊦ gstepf(gs, ls, I1, τ) = gs | An Axiom |
| lstepf-M18 | ⊦ ls.tid = tid → lstepf(gs, ls, M18, retMEMBER(tid, ls.b)) = ls | An Axiom |
| disj-I4-I17 | ⊦ I4 ≠ I17 | An Axiom |
| disj-I8-I20 | ⊦ I8 ≠ I20 | An Axiom |
| disj-M12-M14 | ⊦ M12 ≠ M14 | An Axiom |
| disj-M4-idle | ⊦ M4 ≠ idle | An Axiom |
| disj-I11-M8 | ⊦ I11 ≠ M8 | An Axiom |
| updsel--dotb-dote0 | ⊦ (ls.b:= b).e0 = ls.e0 | An Axiom |
| disj-I8-M10 | ⊦ I8 ≠ M10 | An Axiom |
| disj-I4-M4 | ⊦ I4 ≠ M4 | An Axiom |
| upd-mkls-dote | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e:= e1 = mkls(tid, e1, b, sz, sz0, sz1, e0) | An Axiom |
| upd-mkls-dotn | ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n:= sz4 = mkls(tid, e, b, sz, sz0, sz4, e0) | An Axiom |
| disj-I11-I18 | ⊦ I11 ≠ I18 | An Axiom |
| pre-M14 | ⊦ pre(gs, ls, M14, a) ↔ a = τ | An Axiom |
| disj-I1-I7 | ⊦ I1 ≠ I7 | An Axiom |
| disj-I3-M18 | ⊦ I3 ≠ M18 | An Axiom |
| disj-I5-I12 | ⊦ I5 ≠ I12 | An Axiom |
| disj-I2-M14 | ⊦ I2 ≠ M14 | An Axiom |
| disj-I5-I7 | ⊦ I5 ≠ I7 | An Axiom |
| disj-I21-M3 | ⊦ I21 ≠ M3 | An Axiom |
| disj-I15-M8 | ⊦ I15 ≠ M8 | An Axiom |
| disj-I20-M11 | ⊦ I20 ≠ M11 | An Axiom |
| disj-I19-M8 | ⊦ I19 ≠ M8 | An Axiom |
| disj-I17-M10 | ⊦ I17 ≠ M10 | An Axiom |
| disj-M11-idle | ⊦ M11 ≠ idle | An Axiom |
| updsel--dottid-dottid | ⊦ (ls.tid:= tid).tid = tid | An Axiom |
| disj-I16-M15 | ⊦ I16 ≠ M15 | An Axiom |
| disj-invINSERT-retINSERT | ⊦ invINSERT(tid, invINSERTe) ≠ retINSERT(tid0, b) | An Axiom |
| disj-I8-M4 | ⊦ I8 ≠ M4 | An Axiom |
| disj-I7-M15 | ⊦ I7 ≠ M15 | An Axiom |
| pcstepf-I18 | ⊦ pcstepf(gs, ls, I18, a) = I19 | An Axiom |
| updsel--dotgstate-dotpcf | ⊦ (s.gstate:= gstate).pcf = s.pcf | An Axiom |
| disj-I9-I18 | ⊦ I9 ≠ I18 | An Axiom |
| disj-M8-M12 | ⊦ M8 ≠ M12 | An Axiom |
| disj-I10-I14 | ⊦ I10 ≠ I14 | An Axiom |
| disj-I2-M4 | ⊦ I2 ≠ M4 | An Axiom |
| disj-M3-M6 | ⊦ M3 ≠ M6 | An Axiom |
| disj-M5-M6 | ⊦ M5 ≠ M6 | An Axiom |
| disj-I15-I21 | ⊦ I15 ≠ I21 | An Axiom |
| disj-I3-I7 | ⊦ I3 ≠ I7 | An Axiom |
| lstepf-I13 | ⊦ lstepf(gs, ls, I13, τ) = ls | An Axiom |
| disj-I4-M13 | ⊦ I4 ≠ M13 | An Axiom |
| disj-M5-M10 | ⊦ M5 ≠ M10 | An Axiom |
| disj-I17-M8 | ⊦ I17 ≠ M8 | An Axiom |