Proof step 1 from proof step-M7-M8 (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, M7, a) = M8, # 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, M7, a), ¬ ls.b, ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n] ⊦ (# gstepf(gs, ls, M7, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M7, a).ar)) ∧ lstepf(gs, ls, M7, a).n < # gstepf(gs, ls, M7, a).ar ∧ lstepf(gs, ls, M7, a).e ≠ ⊥ ∧ lstepf(gs, ls, M7, a).sz = # gstepf(gs, ls, M7, a).ar ∧ ( lstepf(gs, ls, M7, a).n0 < # gstepf(gs, ls, M7, a).ar ∧ lstepf(gs, ls, M7, a).n0 = get_hash(lstepf(gs, ls, M7, a).e, lstepf(gs, ls, M7, a).sz)) ∧ (∃ n. n < # gstepf(gs, ls, M7, a).ar ∧ gstepf(gs, ls, M7, a).ar[n] = lstepf(gs, ls, M7, a).e) ∧ allslotsfull(gstepf(gs, ls, M7, a).ar, lstepf(gs, ls, M7, a).n0, lstepf(gs, ls, M7, a).n, lstepf(gs, ls, M7, a).e, false)

Rule argument

Additional information

Proof step 2 from proof step-M7-M8 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: ⊦ lstepf(gs, ls, M7, τ) = ls; (s) ⊦ gstepf(gs, ls, M7, τ) = gs; (s) ⊦ 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 ⊦ pre(gs, ls, M7, a) ↔ a = τ; (s) ⊦ M8 ≠ M10; (s) ⊦ pcstepf(gs, ls, M7, a) = (ls.e = ls.e0 ⊃ M8;M10); (s)

Proof step 3 from proof step-M7-M8 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: ls.n