[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem 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)