Proof step 1 from proof step-I18-I19 (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, I18, a) = I19, # gs.ar ≠ 0, ls.e ≠ ⊥, ls.n < # gs.ar, ls.n0 < # gs.ar, allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true), htok(gs.ar), pre(gs, ls, I18, a), ¬ ls.b ⊦ (# gstepf(gs, ls, I18, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I18, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I18, a).ar, lstepf(gs, ls, I18, a).n0, lstepf(gs, ls, I18, a).n0, lstepf(gs, ls, I18, a).e, true) ∧ lstepf(gs, ls, I18, a).n < # gstepf(gs, ls, I18, a).ar ∧ lstepf(gs, ls, I18, a).e ≠ ⊥ ∧ lstepf(gs, ls, I18, a).sz = # gstepf(gs, ls, I18, a).ar ∧ ( lstepf(gs, ls, I18, a).n0 < # gstepf(gs, ls, I18, a).ar ∧ lstepf(gs, ls, I18, a).n0 = get_hash(lstepf(gs, ls, I18, a).e, lstepf(gs, ls, I18, a).sz)) ∧ ¬ lstepf(gs, ls, I18, a).b

Rule argument

Additional information

Proof step 2 from proof step-I18-I19 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.b:= b).b ↔ b; (s) ⊦ lstepf(gs, ls, I18, a) = ls.b:= false; (s) ⊦ (ls.b:= b).sz = ls.sz; (s) ⊦ (ls.b:= b).e = ls.e; (s) ⊦ (ls.b:= b).n0 = ls.n0; (s) ⊦ gstepf(gs, ls, I18, a) = gs; (s) ⊦ (ls.b:= b).n = ls.n; (s) ⊦ m < n → n ≠ 0; (s) ⊦ pre(gs, ls, I18, a) ↔ a = doINSERT(ls.tid, false); (s) ⊦ pcstepf(gs, ls, I18, a) = I19; (s)