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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ls0.n0 = get_hash(ls0.e, ls0.sz), ls.n0 = get_hash(ls.e, ls.sz), ls0.sz = # gs0.ar, ls.sz = # gs.ar, ls.tid = als.tid, lsf(tid).tid = tid, alsf(tid).tid = tid, I13 = pcstepf(gs, ls, I12, doINSERT(ls.tid, true)), gs0.ar[ls0.n] = ls0.e0, alsf(tid) = als, apc = invInsert, apcf(tid) = apc, gs0 = gstepf(gs, ls, I12, doINSERT(ls.tid, true)), ls0 = lstepf(gs, ls, I12, doINSERT(ls.tid, true)), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = I12, pcf0(tid) = I13, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls.e ≠ ⊥, ls0.e ≠ ⊥, gs0.ar[ls0.n] ≠ ⊥, ls0.n < # gs0.ar, ls0.n0 < # gs0.ar, ls.n < # gs.ar, ls.n0 < # gs.ar, SetLInv(ags, als, apc), absset(gs.ar, ags.set), allslotsfull(gs0.ar, ls0.n0, ls0.n, ls0.e, false), allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs0.ar), htok(gs.ar), pre(gs, ls, I12, doINSERT(ls.tid, true)), ¬ ls.b, ¬ ls0.b, apc = invMember ∨ apc = invInsert → ls.e = als.le, pre(ags, als, apc, ADoInsert(ls.tid, true)) → ags0 = gstepf(ags, als, apc, ADoInsert(ls.tid, true)) ∧ als0 = lstepf(ags, als, apc, ADoInsert(ls.tid, true)) ∧ apc0 = pcstepf(ags, als, apc, ADoInsert(ls.tid, true)), ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), ∀ tid0. tid0 ≠ tid → alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0, gs.ar[ls.n] = ⊥ ∨ gs.ar[ls.n] = ls.e ⊦ pre(ags, als, apc, ADoInsert(ls.tid, true)) ∧ absset(gs0.ar, ags0.set) ∧ ls0.tid = als0.tid ∧ apc0 = (ls0.e = ls0.e0 ⊃ retInsert;invInsert) ∧ (ls0.e = ls0.e0 → als0.lb) ∧ (apc0 = invMember ∨ apc0 = invInsert → ls0.e = als0.le)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  lsf(tid).e = alsf(tid).le, lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf(tid).sz = # gs.ar, lsf0(tid).sz = # (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, alsf(tid).tid = tid, lsf(tid).tid = tid, (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf0(tid) = (gs.ar[lsf(tid).n] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[lsf(tid).n]), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < lsf0(tid).sz, lsf0(tid).n < lsf0(tid).sz, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), allslotsfull((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), htok(gs.ar), htok((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), gs.ar[lsf(tid).n] = ⊥ ∨ gs.ar[lsf(tid).n] = alsf(tid).le ⊦ absset((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, ags.set ++ alsf(tid).le) ∧ lsf0(tid).tid = tid ∧ lsf0(tid).e = lsf0(tid).e0

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.lb:= lb).lb ↔ lb; (s) ⊦ invInsert ≠ retInsert; (s) ⊦ (ls.lb:= lb).tid = ls.tid; (s) ⊦ (gs.set:= set).set = set; (s) ⊦ ADoInsert(tid, b) = ADoInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s) ⊦ ls.tid = tid → pcstepf(gs, ls, invInsert, ADoInsert(tid, b)) = retInsert; (s) ⊦ ls.tid = tid → lstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ ls.lb:= true;ls.lb:= false); (s) ⊦ ls.tid = tid → gstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ gs.set:= (gs.set ++ ls.le);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 ⊦ invInsert ≠ invMember; (s) ⊦ invMember ≠ retInsert; (s) ⊦ gstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ gs.ar:= gs.ar[ls.n := ls.e];gs); (s) ⊦ doINSERT(tid, b) = doINSERT(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ 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) ⊦ lstepf(gs, ls, I12, a) = (gs.ar[ls.n] = ⊥ ⊃ ls.e0:= ls.e;ls.e0:= gs.ar[ls.n]); (s)

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

Heuristic use patterns applied rule case distinction

And obtained the following new goals

• Proof step 4:

  lsf(tid).e = alsf(tid).le, lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).sz = # (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf(tid).sz = # gs.ar, lsf(tid).tid = tid, alsf(tid).tid = tid, (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf0(tid) = (gs.ar[lsf(tid).n] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[lsf(tid).n]), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf0(tid).n < lsf0(tid).sz, lsf0(tid).n0 < lsf0(tid).sz, lsf(tid).n < # gs.ar, lsf(tid).n0 < # gs.ar, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), htok((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar), htok(gs.ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ¬ absset((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, ags.set ++ alsf(tid).le), ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. lsf(tid0).tid = tid0, gs.ar[lsf(tid).n] = ⊥ ∨ gs.ar[lsf(tid).n] = alsf(tid).le ⊦

• Proof step 6:

  lsf(tid).e = alsf(tid).le, lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).sz = # (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf(tid).sz = # gs.ar, lsf(tid).tid = tid, alsf(tid).tid = tid, (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf0(tid) = (gs.ar[lsf(tid).n] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[lsf(tid).n]), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf0(tid).tid ≠ tid, lsf0(tid).n < lsf0(tid).sz, lsf0(tid).n0 < lsf0(tid).sz, lsf(tid).n < # gs.ar, lsf(tid).n0 < # gs.ar, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), htok((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar), htok(gs.ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. lsf(tid0).tid = tid0, gs.ar[lsf(tid).n] = ⊥ ∨ gs.ar[lsf(tid).n] = alsf(tid).le ⊦

• Proof step 9:

  lsf(tid).e = alsf(tid).le, lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).sz = # (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf(tid).sz = # gs.ar, lsf(tid).tid = tid, alsf(tid).tid = tid, (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf0(tid) = (gs.ar[lsf(tid).n] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[lsf(tid).n]), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ lsf0(tid).e0, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf0(tid).n < lsf0(tid).sz, lsf0(tid).n0 < lsf0(tid).sz, lsf(tid).n < # gs.ar, lsf(tid).n0 < # gs.ar, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), htok((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar), htok(gs.ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. lsf(tid0).tid = tid0, gs.ar[lsf(tid).n] = ⊥ ∨ gs.ar[lsf(tid).n] = alsf(tid).le ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  lsf(tid).e = alsf(tid).le, lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).n0 = get_hash(lsf0(tid).e, # gs.ar), lsf(tid).sz = # gs.ar, lsf0(tid).sz = # gs.ar, alsf(tid).tid = tid, lsf(tid).tid = tid, gs.ar[lsf0(tid).n] = lsf0(tid).e0, gs.ar[lsf(tid).n] = alsf(tid).le, apcf(tid) = invInsert, lsf0(tid) = lsf(tid).e0:= alsf(tid).le, pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < # gs.ar, lsf0(tid).n < # gs.ar, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), allslotsfull(gs.ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), htok(gs.ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ¬ absset(gs.ar, ags.set ++ alsf(tid).le), ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)) ⊦

Rule argument

Additional information

Used simplifier rules: 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 n < # ar, ar[n] = ⊥ ⊦ absset(ar, set) → (absset(ar[n := e], set ++ e) ↔ e ≠ ⊥); (s) ⊦ (gs.ar:= ar).ar = ar; (s) ⊦ # ar[n := a] = # ar; (s)

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

Heuristic use patterns applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0:= e2 = mkls(tid, e, b, sz, sz0, sz1, e2); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) n < # ar ⊦ absset(ar, set) → (absset(ar, set ++ ar[n]) ↔ ar[n] ≠ ⊥); (s) ⊦ (((((tid = ls.tid ∧ e = ls.e) ∧ (b ↔ ls.b)) ∧ sz = ls.sz) ∧ sz0 = ls.n0) ∧ n = ls.n) ∧ e0 = ls.e0 ↔ ls = mkls(tid, e, b, sz, sz0, n, e0); (elim) Used terms: lsf(tid), b, tid1, n0, e0, e, n, n1

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

Heuristic use patterns applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf0(tid).sz = # (gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar, alsf(tid).tid = tid, (gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, ¬ b, e = alsf(tid).le, lsf(tid) = mkls(tid1, e, b, n, n0, n1, e0), lsf0(tid) = (gs.ar[n1] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[n1]), n = # gs.ar, n0 = get_hash(alsf(tid).le, # gs.ar), pcf(tid) = I12, pcf0(tid) = I13, tid1 = tid, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf0(tid).tid ≠ tid, n0 < # gs.ar, n1 < # gs.ar, lsf0(tid).n0 < lsf0(tid).sz, lsf0(tid).n < lsf0(tid).sz, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, n0, n1, alsf(tid).le, false), allslotsfull((gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), htok(gs.ar), htok((gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar), ¬ lsf0(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), gs.ar[n1] = ⊥ ∨ gs.ar[n1] = alsf(tid).le ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (((((tid = ls.tid ∧ e = ls.e) ∧ (b ↔ ls.b)) ∧ sz = ls.sz) ∧ sz0 = ls.n0) ∧ n = ls.n) ∧ e0 = ls.e0 ↔ ls = mkls(tid, e, b, sz, sz0, n, e0); (elim) Used terms: lsf(tid), b, tid1, n0, e0, e, n, n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf0(tid).sz = # (gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar, alsf(tid).tid = tid, (gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf(tid) = mkls(tid, alsf(tid).le, false, # gs.ar, get_hash(alsf(tid).le, # gs.ar), n1, e0), lsf0(tid) = (gs.ar[n1] = ⊥ ⊃ mkls(tid, alsf(tid).le, false, # gs.ar, get_hash(alsf(tid).le, # gs.ar), n1, alsf(tid).le) ;mkls(tid, alsf(tid).le, false, # gs.ar, get_hash(alsf(tid).le, # gs.ar), n1, gs.ar[n1]) ), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf0(tid).tid ≠ tid, get_hash(alsf(tid).le, # gs.ar) < # gs.ar, n1 < # gs.ar, lsf0(tid).n0 < lsf0(tid).sz, lsf0(tid).n < lsf0(tid).sz, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, get_hash(alsf(tid).le, # gs.ar), n1, alsf(tid).le, false), allslotsfull((gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), htok(gs.ar), htok((gs.ar[n1] = ⊥ ⊃ gs.ar:= gs.ar[n1 := alsf(tid).le];gs).ar), ¬ lsf0(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), gs.ar[n1] = ⊥ ∨ gs.ar[n1] = alsf(tid).le ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0:= e2 = mkls(tid, e, b, sz, sz0, sz1, e2); (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).sz = sz; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n = sz1; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0 = e0; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n0 = sz0; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e = e; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).tid = tid; (s) ⊦ # ar[n := a] = # ar; (s) ⊦ (gs.ar:= ar).ar = ar; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) htok-returnfalse-f: n < # ar ⊦ htok(ar) ∧ ar[n] = ⊥ ∧ e ≠ ⊥ ∧ allslotsfull(ar, get_hash(e, # ar), n, e, false) → (∀ m. m < # ar → ar[m] ≠ e); (forward) from specification hashset-preds ⊦ m < # ar → (ar[m := a])[m] = a; (s) Used formulas: gs.ar[n1] = ⊥

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  lsf(tid).e = alsf(tid).le, lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf(tid).sz = # gs.ar, lsf0(tid).sz = # (gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le]).ar, alsf(tid).tid = tid, lsf(tid).tid = tid, (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, gs.ar[lsf(tid).n] = ⊥, apcf(tid) = invInsert, lsf0(tid) = (gs.ar[lsf(tid).n] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[lsf(tid).n]), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ lsf0(tid).e0, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < lsf0(tid).sz, lsf0(tid).n < lsf0(tid).sz, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), allslotsfull((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), htok(gs.ar), htok((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), gs.ar[lsf(tid).n] = ⊥ ∨ gs.ar[lsf(tid).n] = alsf(tid).le ⊦

• Proof step 12:

  lsf(tid).e = alsf(tid).le, lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).n0 = get_hash(lsf0(tid).e, lsf0(tid).sz), lsf(tid).sz = # gs.ar, lsf0(tid).sz = # gs.ar, alsf(tid).tid = tid, lsf(tid).tid = tid, (gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf0(tid) = (gs.ar[lsf(tid).n] = ⊥ ⊃ lsf(tid).e0:= alsf(tid).le;lsf(tid).e0:= gs.ar[lsf(tid).n]), pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ lsf0(tid).e0, lsf0(tid).e ≠ ⊥, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, gs.ar[lsf(tid).n] ≠ ⊥, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < lsf0(tid).sz, lsf0(tid).n < lsf0(tid).sz, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), allslotsfull((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), htok(gs.ar), htok((gs.ar[lsf(tid).n] = ⊥ ⊃ gs.ar:= gs.ar[lsf(tid).n := alsf(tid).le];gs).ar), ¬ lsf(tid).b, ¬ lsf0(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), gs.ar[lsf(tid).n] = ⊥ ∨ gs.ar[lsf(tid).n] = alsf(tid).le ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  lsf(tid).e = alsf(tid).le, lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).n0 = get_hash(lsf0(tid).e, # gs.ar), lsf0(tid).sz = # gs.ar, lsf(tid).sz = # gs.ar, alsf(tid).tid = tid, lsf(tid).tid = tid, (gs.ar[lsf(tid).n := alsf(tid).le])[lsf0(tid).n] = lsf0(tid).e0, gs.ar[lsf(tid).n] = ⊥, apcf(tid) = invInsert, lsf0(tid) = lsf(tid).e0:= alsf(tid).le, pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e ≠ lsf0(tid).e0, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < # gs.ar, lsf0(tid).n < # gs.ar, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar[lsf(tid).n := alsf(tid).le], lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), htok(gs.ar), htok(gs.ar[lsf(tid).n := alsf(tid).le]), ¬ lsf0(tid).b, ¬ lsf(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)) ⊦

Rule argument

Additional information

Used simplifier rules: 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 ⊦ (gs.ar:= ar).ar = ar; (s) ⊦ # ar[n := a] = # ar; (s)

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

Heuristic use patterns applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) htok-returnfalse-f: n < # ar ⊦ htok(ar) ∧ ar[n] = ⊥ ∧ e ≠ ⊥ ∧ allslotsfull(ar, get_hash(e, # ar), n, e, false) → (∀ m. m < # ar → ar[m] ≠ e); (forward) from specification hashset-preds ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0:= e2 = mkls(tid, e, b, sz, sz0, sz1, e2); (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n = sz1; (s) ⊦ m < # ar → (ar[m := a])[m] = a; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).sz = sz; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n0 = sz0; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e = e; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0 = e0; (s) ⊦ (((((tid = ls.tid ∧ e = ls.e) ∧ (b ↔ ls.b)) ∧ sz = ls.sz) ∧ sz0 = ls.n0) ∧ n = ls.n) ∧ e0 = ls.e0 ↔ ls = mkls(tid, e, b, sz, sz0, n, e0); (elim) Used terms: lsf(tid), b, tid1, n0, e0, e, n, n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  lsf(tid).e = alsf(tid).le, lsf(tid).n0 = get_hash(alsf(tid).le, # gs.ar), lsf0(tid).n0 = get_hash(lsf0(tid).e, # gs.ar), lsf(tid).sz = # gs.ar, lsf0(tid).sz = # gs.ar, alsf(tid).tid = tid, lsf(tid).tid = tid, gs.ar[lsf(tid).n] = alsf(tid).le, gs.ar[lsf0(tid).n] = lsf0(tid).e0, apcf(tid) = invInsert, lsf0(tid) = lsf(tid).e0:= alsf(tid).le, pcf(tid) = I12, pcf0(tid) = I13, lsf0(tid).e ≠ ⊥, lsf0(tid).e ≠ lsf0(tid).e0, lsf0(tid).e0 ≠ ⊥, alsf(tid).le ≠ ⊥, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < # gs.ar, lsf0(tid).n < # gs.ar, SetLInv(ags, alsf(tid), invInsert), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, false), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, alsf(tid).le, false), htok(gs.ar), ¬ lsf0(tid).b, ¬ lsf(tid).b, ∀ tid0. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)) ⊦

Rule argument

Additional information

Used simplifier rules: 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

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

Heuristic use patterns applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0:= e2 = mkls(tid, e, b, sz, sz0, sz1, e2); (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n = sz1; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).sz = sz; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n0 = sz0; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e = e; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e0 = e0; (s) ⊦ (((((tid = ls.tid ∧ e = ls.e) ∧ (b ↔ ls.b)) ∧ sz = ls.sz) ∧ sz0 = ls.n0) ∧ n = ls.n) ∧ e0 = ls.e0 ↔ ls = mkls(tid, e, b, sz, sz0, n, e0); (elim) Used terms: lsf(tid), b, tid1, n0, e0, e, n, n1