Proof step 1 from proof step-absstep-M13-M14-tau-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, M14 = pcstepf(gs, ls, M13, τ), alsf(tid) = als, apc = ((ls.n + 1) % # gs.ar ≠ ls.n0 ⊃ invMember;retMember), apcf(tid) = apc, gs0 = gstepf(gs, ls, M13, τ), ls0 = lstepf(gs, ls, M13, τ), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = M13, pcf0(tid) = M14, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls.e ≠ ls.e0, ls.e ≠ ⊥, ls0.e ≠ ⊥, gs.ar[ls.n] ≠ ls.e, gs.ar[ls.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, true), allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), htok(gs0.ar), htok(gs.ar), pre(gs, ls, M13, τ), ¬ ls.b, ¬ ls0.b, (ls.n + 1) % # gs.ar = ls.n0 → ¬ als.lb, apc = invMember ∨ apc = invInsert → ls.e = als.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. tid0 ≠ tid → alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0 ⊦ absset(gs0.ar, ags.set) ∧ ls0.tid = als.tid ∧ apc = (ls0.n ≠ ls0.n0 ⊃ invMember;retMember) ∧ (ls0.n = ls0.n0 → ¬ als.lb) ∧ (apc = invMember ∨ apc = invInsert → ls0.e = als.le)

Rule argument

Additional information

Proof step 2 from proof step-absstep-M13-M14-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  lsf0(tid).n0 = get_hash(lsf0(tid).e, # gs.ar), lsf(tid).n0 = get_hash(lsf(tid).e, # gs.ar), lsf0(tid).sz = # gs.ar, lsf(tid).sz = # gs.ar, lsf(tid).tid = tid, alsf(tid).tid = tid, apcf(tid) = ((lsf(tid).n + 1) % # gs.ar ≠ lsf(tid).n0 ⊃ invMember;retMember), lsf0(tid) = lsf(tid).n:= ((lsf(tid).n + 1) % # gs.ar), pcf(tid) = M13, pcf0(tid) = M14, lsf0(tid).e ≠ ⊥, lsf(tid).e ≠ ⊥, lsf(tid).e ≠ lsf(tid).e0, gs.ar[lsf(tid).n] ≠ ⊥, gs.ar[lsf(tid).n] ≠ lsf(tid).e, lsf0(tid).n < # gs.ar, lsf0(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf(tid).n0 < # gs.ar, SetLInv(ags, alsf(tid), apcf(tid)), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, true), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, lsf(tid).e, false), htok(gs.ar), ¬ lsf0(tid).b, ¬ lsf(tid).b, (lsf(tid).n + 1) % # gs.ar = lsf(tid).n0 → ¬ alsf(tid).lb, apcf(tid) = invMember ∨ apcf(tid) = invInsert → lsf(tid).e = alsf(tid).le, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. lsf(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)) ⊦ lsf0(tid).tid = tid ∧ apcf(tid) = (lsf0(tid).n ≠ lsf0(tid).n0 ⊃ invMember;retMember) ∧ (lsf0(tid).n = lsf0(tid).n0 → ¬ alsf(tid).lb) ∧ (apcf(tid) = invMember ∨ apcf(tid) = invInsert → lsf0(tid).e = alsf(tid).le)

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, M13, τ) = gs; (s) ⊦ pre(gs, ls, M13, a) ↔ a = τ; (s) ⊦ pcstepf(gs, ls, M13, a) = M14; (s) ⊦ lstepf(gs, ls, M13, τ) = ls.n:= ((ls.n + 1) % ls.sz); (s)

Proof step 3 from proof step-absstep-M13-M14-tau-same (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

  lsf(tid).n0 = get_hash(lsf(tid).e, # 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, apcf(tid) = ((lsf(tid).n + 1) % # gs.ar ≠ lsf(tid).n0 ⊃ invMember;retMember), lsf0(tid) = lsf(tid).n:= ((lsf(tid).n + 1) % # gs.ar), pcf(tid) = M13, pcf0(tid) = M14, lsf0(tid).e ≠ ⊥, lsf(tid).e ≠ ⊥, lsf(tid).e ≠ lsf(tid).e0, gs.ar[lsf(tid).n] ≠ ⊥, gs.ar[lsf(tid).n] ≠ lsf(tid).e, apcf(tid) ≠ invInsert, lsf(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf0(tid).n0 < # gs.ar, lsf0(tid).n < # gs.ar, SetLInv(ags, alsf(tid), apcf(tid)), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, lsf(tid).e, false), allslotsfull(gs.ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, true), htok(gs.ar), ¬ lsf0(tid).b, ¬ lsf(tid).b, apcf(tid) = invMember ∨ apcf(tid) = invInsert → lsf(tid).e = alsf(tid).le, (lsf(tid).n + 1) % # gs.ar = lsf(tid).n0 → ¬ alsf(tid).lb, ∀ 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. lsf(tid0).tid = tid0, ∀ tid0. alsf(tid0).tid = tid0 ⊦ lsf0(tid).tid = tid ∧ apcf(tid) = (lsf0(tid).n ≠ lsf0(tid).n0 ⊃ invMember;retMember) ∧ (lsf0(tid).n = lsf0(tid).n0 → ¬ alsf(tid).lb) ∧ (apcf(tid) = invMember ∨ apcf(tid) = invInsert → lsf0(tid).e = alsf(tid).le)

Rule argument

Additional information

Used simplifier rules: lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ invInsert ≠ invMember; (s) ⊦ invInsert ≠ retMember; (s) Used formulas: apcf(tid) = invInsert

Proof step 4 from proof step-absstep-M13-M14-tau-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  lsf0(tid).n0 = get_hash(lsf0(tid).e, # gs.ar), lsf(tid).n0 = get_hash(lsf(tid).e, # gs.ar), lsf0(tid).sz = # gs.ar, lsf(tid).sz = # gs.ar, lsf(tid).tid = tid, alsf(tid).tid = tid, apcf(tid) = ((lsf(tid).n + 1) % # gs.ar ≠ lsf(tid).n0 ⊃ invMember;retMember), lsf0(tid) = lsf(tid).n:= ((lsf(tid).n + 1) % # gs.ar), pcf(tid) = M13, pcf0(tid) = M14, lsf0(tid).e ≠ ⊥, lsf(tid).e ≠ ⊥, lsf(tid).e ≠ lsf(tid).e0, gs.ar[lsf(tid).n] ≠ ⊥, gs.ar[lsf(tid).n] ≠ lsf(tid).e, apcf(tid) ≠ invInsert, lsf0(tid).n < # gs.ar, lsf0(tid).n0 < # gs.ar, lsf(tid).n < # gs.ar, lsf(tid).n0 < # gs.ar, SetLInv(ags, alsf(tid), apcf(tid)), absset(gs.ar, ags.set), allslotsfull(gs.ar, lsf0(tid).n0, lsf0(tid).n, lsf0(tid).e, true), allslotsfull(gs.ar, lsf(tid).n0, lsf(tid).n, lsf(tid).e, false), htok(gs.ar), ¬ lsf0(tid).b, ¬ lsf(tid).b, (lsf(tid).n + 1) % # gs.ar = lsf(tid).n0 → ¬ alsf(tid).lb, apcf(tid) = invMember → lsf(tid).e = alsf(tid).le, ∀ tid0. alsf(tid0).tid = tid0, ∀ tid0. lsf(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)) ⊦ lsf0(tid).tid = tid ∧ apcf(tid) = (lsf0(tid).n ≠ lsf0(tid).n0 ⊃ invMember;retMember) ∧ (lsf0(tid).n = lsf0(tid).n0 → ¬ alsf(tid).lb) ∧ (apcf(tid) = invMember → lsf0(tid).e = alsf(tid).le)

Rule argument

Additional information

Proof step 5 from proof step-absstep-M13-M14-tau-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).n:= sz4 = mkls(tid, e, b, sz, sz0, sz4, e0); (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).sz = sz; (s) ⊦ m < n → n ≠ 0; (s) n ≠ 0 ⊦ m % n < n; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).b ↔ b; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).tid = tid; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n = sz1; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).n0 = sz0; (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).e = e; (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