Proof step 1 from proof rely-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.tid ≠ tid0, 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, ¬ rely(gs.ar, gstepf(gs, ls, I12, a).ar) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-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.tid ≠ tid0, ls.n < ls.sz, ls.n0 < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), ¬ ls.b, ¬ rely(gs.ar, (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar) ⊦

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 ⊦ 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 rely-I12-I13 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ rely(ar, ar0) ↔ # ar = # ar0 ∧ (∀ n. n < # ar → ar[n] ≠ ⊥ → ar0[n] = ar[n])

• Proof step 5:

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

Rule argument

Additional information

Used terms: gs.ar, (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs).ar

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Used formulas: gs.ar[ls.n] = ⊥

Proof step 7 from proof rely-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.tid ≠ tid0, gs.ar[n] ≠ ⊥, (gs.ar[ls.n := ls.e])[n] ≠ gs.ar[n], n < ls.sz, ls.n0 < ls.sz, ls.n < ls.sz, allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs.ar), ¬ ls.b ⊦

Rule argument

Additional information

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

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (ar[n := a])[m] = ar[m]; (s) Used formulas: n = ls.n