Proof step 1 from proof init-state-inv (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ HashsetInv(gs, lsf, pcf), ∀ tid. tid = lsf(tid).tid, ∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle) ⊦

Rule argument

Additional information

Proof step 2 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ HashsetInv(gs, lsf, pcf) ↔ HashsetGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), pcf(tid)))

• Proof step 4:

  ∀ tid. tid = lsf(tid).tid, ∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle), ¬ HashsetGInv(gs) ∨ (∃ tid. ¬(lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), pcf(tid)))) ⊦

Rule argument

Additional information

Used terms: gs, lsf, pcf

Proof step 3 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof init-state-inv (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  ¬ HashsetGInv(gs), ∀ tid. tid = lsf(tid).tid, ∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle) ⊦

• Proof step 10:

  ∀ tid. tid = lsf(tid).tid, ∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle), ∃ tid. ¬(lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), pcf(tid))) ⊦

Rule argument

Additional information

Proof step 5 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ HashsetGInv(gs) ↔ # gs.ar ≠ 0 ∧ htok(gs.ar)

• Proof step 7:

  ∀ tid. tid = lsf(tid).tid, ∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle), # gs.ar = 0 ∨ ¬ htok(gs.ar) ⊦

Rule argument

Additional information

Used terms: gs

Proof step 6 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gs.ar = mkar(n, ⊥), n ≠ 0, ¬ htok(mkar(n, ⊥)), ∀ tid. tid = lsf(tid).tid ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # mkar(n, e) = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m > n ↔ n < m; (s)

Proof step 8 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ htok(ar) ↔ (∀ n. n < # ar ∧ ar[n] ≠ ⊥ → allslotsfull(ar, get_hash(ar[n], # ar), n, ar[n], false))

Rule argument

Additional information

Used simplifier rules: ⊦ # mkar(n, e) = n; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m < n → mkar(n, e)[m] = e; (s) Used terms: mkar(n, ⊥)

Proof step 9 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gs.ar = mkar(n, ⊥), n ≠ 0, ∀ tid. tid = lsf(tid).tid ⊦ lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m > n ↔ n < m; (s)

Proof step 11 from proof init-state-inv (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  gs.ar = mkar(n, ⊥), tid = lsf(tid).tid, n ≠ 0 ⊦ lsf(tid).tid = tid ∧ HashsetLInv(gs, lsf(tid), idle)

Rule argument

Additional information

Used terms: tid

Proof step 12 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  gs.ar = mkar(n, ⊥), tid = lsf(tid).tid, n ≠ 0, ¬ HashsetLInv(gs, lsf(tid), idle) ⊦

Rule argument

Additional information

Proof step 13 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: ⊦ I1 ≠ idle; (s) ⊦ M1 ≠ idle; (s) ⊦ I2 ≠ idle; (s) ⊦ M2 ≠ idle; (s) ⊦ I3 ≠ idle; (s) ⊦ M3 ≠ idle; (s) ⊦ I4 ≠ idle; (s) ⊦ I5 ≠ idle; (s) ⊦ I6 ≠ idle; (s) ⊦ I7 ≠ idle; (s) ⊦ I8 ≠ idle; (s) ⊦ I10 ≠ idle; (s) ⊦ I11 ≠ idle; (s) ⊦ I12 ≠ idle; (s) ⊦ I13 ≠ idle; (s) ⊦ I14 ≠ idle; (s) ⊦ I16 ≠ idle; (s) ⊦ I17 ≠ idle; (s) ⊦ I18 ≠ idle; (s) ⊦ I19 ≠ idle; (s) ⊦ I20 ≠ idle; (s) ⊦ I9 ≠ idle; (s) ⊦ I15 ≠ idle; (s) ⊦ I21 ≠ idle; (s) ⊦ M18 ≠ idle; (s) ⊦ M11 ≠ idle; (s) ⊦ M12 ≠ idle; (s) ⊦ M4 ≠ idle; (s) ⊦ M5 ≠ idle; (s) ⊦ M6 ≠ idle; (s) ⊦ M7 ≠ idle; (s) ⊦ M8 ≠ idle; (s) ⊦ M9 ≠ idle; (s) ⊦ M10 ≠ idle; (s) ⊦ M13 ≠ idle; (s) ⊦ M14 ≠ idle; (s) ⊦ M15 ≠ idle; (s) ⊦ M16 ≠ idle; (s) ⊦ M17 ≠ idle; (s) Used terms: gs, lsf(tid), idle

Proof step 14 from proof init-state-inv (previous step) (back to tree)

A spec-lemma