Proof step 1 from proof step-I12-I13 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, pcstepf(gs, ls, I12, a) = I13, # gs.ar ≠ 0, ls.e ≠ ⊥, ls.n < # gs.ar, ls.n0 < # gs.ar, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), pre(gs, ls, I12, a), ¬ ls.b ⊦ (# gstepf(gs, ls, I12, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I12, a).ar)) ∧ (gstepf(gs, ls, I12, a).ar[lstepf(gs, ls, I12, a).n] ≠ ⊥ ∧ gstepf(gs, ls, I12, a).ar[lstepf(gs, ls, I12, a).n] = lstepf(gs, ls, I12, a).e0) ∧ allslotsfull(gstepf(gs, ls, I12, a).ar, lstepf(gs, ls, I12, a).n0, lstepf(gs, ls, I12, a).n, lstepf(gs, ls, I12, a).e, false) ∧ lstepf(gs, ls, I12, a).n < # gstepf(gs, ls, I12, a).ar ∧ lstepf(gs, ls, I12, a).e ≠ ⊥ ∧ lstepf(gs, ls, I12, a).sz = # gstepf(gs, ls, I12, a).ar ∧ ( lstepf(gs, ls, I12, a).n0 < # gstepf(gs, ls, I12, a).ar ∧ lstepf(gs, ls, I12, a).n0 = get_hash(lstepf(gs, ls, I12, a).e, lstepf(gs, ls, I12, a).sz)) ∧ ¬ lstepf(gs, ls, I12, a).b

Rule argument

Additional information

Proof step 2 from proof step-I12-I13 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, ls.e ≠ ⊥, ls.n < ls.sz, ls.n0 < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), ¬ ls.b ⊦ htok((gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar) ∧ (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar[(gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n] ≠ ⊥ ∧ (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar[(gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n] = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e0 ∧ allslotsfull ((gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n0, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e, false) ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n < # (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e ≠ ⊥ ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).sz = # (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n0 < # (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n0 = get_hash((gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).sz) ∧ ¬ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).b

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ lstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]); (s) ⊦ gstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs); (s) ⊦ pre(gs, ls, I12, a) ↔ a = (gs.ar[ls.n] = ⊥ ∨ gs.ar[ls.n] = ls.e ⊃ doINSERT(ls.tid, true);τ); (s) ⊦ pcstepf(gs, ls, I12, a) = I13; (s)

Proof step 3 from proof step-I12-I13 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n0 < ls.sz, ls.n < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), ¬ ls.b ⊦ htok((gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar) ∧ (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar[(gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n] ≠ ⊥ ∧ (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar[(gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n] = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e0 ∧ allslotsfull ((gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n0, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e, false) ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n < # (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e ≠ ⊥ ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).sz = # (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n0 < # (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).n0 = get_hash((gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).e, (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).sz) ∧ ¬ (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]).b

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.e0:= e0).e0 = e0; (s) ⊦ (ls.e0:= e0).n = ls.n; (s) ⊦ (ls.e0:= e0).n0 = ls.n0; (s) ⊦ (ls.e0:= e0).e = ls.e; (s) ⊦ (ls.e0:= e0).sz = ls.sz; (s) ⊦ (ls.e0:= e0).b ↔ ls.b; (s) Used formulas: gs.ar[ls.n] = ⊥

Proof step 4 from proof step-I12-I13 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n0 < ls.sz, ls.n < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), ¬ ls.b ⊦ htok(gs.ar[ls.n := ls.e]) ∧ allslotsfull(gs.ar[ls.n := ls.e], ls.n0, ls.n, ls.e, false)

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.e0:= e0).b ↔ ls.b; (s) ⊦ (ls.e0:= e0).sz = ls.sz; (s) ⊦ (ls.e0:= e0).e = ls.e; (s) ⊦ (ls.e0:= e0).n0 = ls.n0; (s) ⊦ # ar[n := a] = # ar; (s) ⊦ (gs.ar:= ar).ar = ar; (s) ⊦ (ls.e0:= e0).n = ls.n; (s) ⊦ (ls.e0:= e0).e0 = e0; (s) m < # ar ⊦ (ar[m := a])[m] = a; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 5 from proof step-I12-I13 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ allslotsfull(ar, get_hash(e, # ar), n, e, false) ∧ htok(ar) ∧ e ≠ ⊥ ∧ ar[n] = ⊥ → htok(ar[n := e])

• Proof step 7:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n < ls.sz, ls.n0 < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), allslotsfull(gs.ar, get_hash(ls.e, # gs.ar), ls.n, ls.e, false), htok(gs.ar), ¬ ls.b ⊦ true ∧ allslotsfull(gs.ar[ls.n := ls.e], ls.n0, ls.n, ls.e, false)

Rule argument

Additional information

Used terms: gs.ar, ls.e, ls.n

Proof step 6 from proof step-I12-I13 (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof step-I12-I13 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n < ls.sz, ls.n0 < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), ¬ ls.b, ¬ allslotsfull(gs.ar[ls.n := ls.e], ls.n0, ls.n, ls.e, false) ⊦

Rule argument

Additional information

Proof step 8 from proof step-I12-I13 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ allslotsfull(ar, n0, n, e, b) ↔ (∀ m. between(n0, m, n, b) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥)

• Proof step 10:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n0 < ls.sz, ls.n < ls.sz, htok(gs.ar), ¬ ls.b, ¬ allslotsfull(gs.ar[ls.n := ls.e], ls.n0, ls.n, ls.e, false), ∀ m. between(ls.n0, m, ls.n, false) ∧ m < # gs.ar → gs.ar[m] ≠ ls.e ∧ gs.ar[m] ≠ ⊥ ⊦

Rule argument

Additional information

Used terms: ls.n0, false, gs.ar, ls.e, ls.n

Proof step 9 from proof step-I12-I13 (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof step-I12-I13 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ allslotsfull(ar, n0, n, e, b) ↔ (∀ m. between(n0, m, n, b) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥)

• Proof step 12:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n < ls.sz, ls.n0 < ls.sz, htok(gs.ar), ¬ ls.b, ∀ m. between(ls.n0, m, ls.n, false) ∧ m < # gs.ar → gs.ar[m] ≠ ls.e ∧ gs.ar[m] ≠ ⊥, ∃ m. ¬(between(ls.n0, m, ls.n, false) ∧ m < # gs.ar[ls.n := ls.e] → (gs.ar[ls.n := ls.e])[m] ≠ ls.e ∧ (gs.ar[ls.n := ls.e])[m] ≠ ⊥) ⊦

Rule argument

Additional information

Used terms: ls.n0, false, gs.ar[ls.n := ls.e], ls.e, ls.n

Proof step 11 from proof step-I12-I13 (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof step-I12-I13 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, m < ls.sz, ls.n < ls.sz, ls.n0 < ls.sz, between(ls.n0, m, ls.n, false), htok(gs.ar), ¬ ls.b, ∀ m. between(ls.n0, m, ls.n, false) ∧ m < ls.sz → gs.ar[m] ≠ ls.e ∧ gs.ar[m] ≠ ⊥ ⊦ (gs.ar[ls.n := ls.e])[m] ≠ ls.e ∧ (gs.ar[ls.n := ls.e])[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ # ar[n := a] = # ar; (s)

Proof step 13 from proof step-I12-I13 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, ls.n0 < ls.sz, ls.n < ls.sz, m < ls.sz, between(ls.n0, m, ls.n, false), htok(gs.ar), ¬ ls.b, between(ls.n0, m, ls.n, false) ∧ m < ls.sz → gs.ar[m] ≠ ls.e ∧ gs.ar[m] ≠ ⊥ ⊦ (gs.ar[ls.n := ls.e])[m] ≠ ls.e ∧ (gs.ar[ls.n := ls.e])[m] ≠ ⊥

Rule argument

Additional information

Used terms: m

Proof step 14 from proof step-I12-I13 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ls.n0 = get_hash(ls.e, ls.sz), ls.sz = # gs.ar, gs.ar[ls.n] = ⊥, ls.e ≠ ⊥, gs.ar[m] ≠ ⊥, gs.ar[m] ≠ ls.e, m < ls.sz, ls.n < ls.sz, ls.n0 < ls.sz, between(ls.n0, m, ls.n, false), htok(gs.ar), ¬ ls.b ⊦ (gs.ar[ls.n := ls.e])[m] ≠ ls.e ∧ (gs.ar[ls.n := ls.e])[m] ≠ ⊥

Rule argument

Additional information

Proof step 15 from proof step-I12-I13 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ m ≠ n → (ar[n := a])[m] = ar[m]

Rule argument

Additional information

Used terms: gs.ar, ls.n, ls.e, m

Proof step 16 from proof step-I12-I13 (previous step) (back to tree)

A spec-lemma