Proof step 1 from proof step-absstep-M16-idle-retMEMBER-same (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, ls.tid = als.tid, lsf(tid).tid = tid, alsf(tid).tid = tid, als.lb ↔ ls.b, alsf(tid) = als, apc = retMember, apcf(tid) = apc, gs0 = gstepf(gs, ls, M16, retMEMBER(ls.tid, b)), idle = pcstepf(gs, ls, M16, retMEMBER(ls.tid, b)), ls0 = lstepf(gs, ls, M16, retMEMBER(ls.tid, b)), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = M16, pcf0(tid) = idle, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls.e ≠ ⊥, ls.n < # gs.ar, ls.n0 < # gs.ar, SetLInv(ags, als, apc), absset(gs.ar, ags.set), allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true), htok(gs0.ar), htok(gs.ar), pre(gs, ls, M16, retMEMBER(ls.tid, b)), ¬ ls.b, apc = invMember ∨ apc = invInsert → ls.e = als.le, pre(ags, als, apc, ARetMember(ls.tid, b)) → ags0 = gstepf(ags, als, apc, ARetMember(ls.tid, b)) ∧ als0 = lstepf(ags, als, apc, ARetMember(ls.tid, b)) ∧ apc0 = pcstepf(ags, als, apc, ARetMember(ls.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. tid0 ≠ tid → alsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0 ⊦ pre(ags, als, apc, ARetMember(ls.tid, b)) ∧ absset(gs0.ar, ags0.set) ∧ ls0.tid = als0.tid ∧ apc0 = idle ∧ (apc0 = invMember ∨ apc0 = invInsert → ls0.e = als0.le)

Rule argument

Additional information

Proof step 2 from proof step-absstep-M16-idle-retMEMBER-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ARetMember(tid, b) = ARetMember(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ ls.tid = tid → pcstepf(gs, ls, retMember, ARetMember(tid, b0)) = idle; (s) ⊦ ls.tid = tid → lstepf(gs, ls, retMember, ARetMember(tid, b0)) = ls; (s) ⊦ ls.tid = tid → gstepf(gs, ls, retMember, ARetMember(tid, b0)) = gs; (s) ⊦ invInsert ≠ retMember; (s) ⊦ invMember ≠ retMember; (s) ⊦ m < n → n ≠ 0; (s) ⊦ ls.tid = tid ∧ ¬ ls.b → lstepf(gs, ls, M16, retMEMBER(tid, false)) = ls; (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 ⊦ idle ≠ invInsert; (s) ⊦ idle ≠ invMember; (s) ⊦ ls.tid = tid → gstepf(gs, ls, M16, retMEMBER(tid, b)) = gs; (s) ⊦ retMEMBER(tid, b) = retMEMBER(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ pre(gs, ls, M16, a) ↔ a = retMEMBER(ls.tid, ls.b); (s) ⊦ pcstepf(gs, ls, M16, a) = idle; (s)