Proof step 1 from proof step-absstep-idle-I1-invINSERT-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ls.tid = als.tid, lsf(tid).tid = tid, alsf(tid).tid = tid, I1 = pcstepf(gs, ls, idle, invINSERT(ls.tid, e0)), alsf(tid) = als, apc = idle, apcf(tid) = apc, gs0 = gstepf(gs, ls, idle, invINSERT(ls.tid, e0)), ls0 = lstepf(gs, ls, idle, invINSERT(ls.tid, e0)), lsf(tid) = ls, lsf0(tid) = ls0, pcf(tid) = idle, pcf0(tid) = I1, # gs.ar ≠ 0, # gs0.ar ≠ 0, ls0.e ≠ ⊥, SetLInv(ags, als, apc), absset(gs.ar, ags.set), htok(gs0.ar), htok(gs.ar), pre(gs, ls, idle, invINSERT(ls.tid, e0)), apc = invMember ∨ apc = invInsert → ls.e = als.le, pre(ags, als, apc, AInvInsert(ls.tid, e0)) → ags0 = gstepf(ags, als, apc, AInvInsert(ls.tid, e0)) ∧ als0 = lstepf(ags, als, apc, AInvInsert(ls.tid, e0)) ∧ apc0 = pcstepf(ags, als, apc, AInvInsert(ls.tid, e0)), ∀ 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, AInvInsert(ls.tid, e0)) ∧ absset(gs0.ar, ags0.set) ∧ ls0.tid = als0.tid ∧ apc0 = invInsert ∧ (apc0 = invMember ∨ apc0 = invInsert → ls0.e = als0.le)

Rule argument

Additional information

Proof step 2 from proof step-absstep-idle-I1-invINSERT-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  alsf(tid).tid = tid, lsf(tid).tid = tid, apcf(tid) = idle, lsf0(tid) = lsf(tid).e:= e1, pcf(tid) = idle, pcf0(tid) = I1, # gs.ar ≠ 0, lsf0(tid).e ≠ ⊥, e1 ≠ ⊥, SetLInv(ags, alsf(tid), idle), absset(gs.ar, ags.set), htok(gs.ar), ∀ 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)) ⊦ lsf0(tid).tid = tid ∧ lsf0(tid).e = e1

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.le:= le).le = le; (s) ⊦ (ls.le:= le).tid = ls.tid; (s) ⊦ AInvInsert(tid, e) = AInvInsert(tid0, e0) ↔ tid = tid0 ∧ e = e0; (ws) ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥); (s) ⊦ ls.tid = tid → pcstepf(gs, ls, idle, AInvInsert(tid, e)) = invInsert; (s) ⊦ ls.tid = tid → lstepf(gs, ls, idle, AInvInsert(tid, e)) = ls.le:= e; (s) ⊦ gstepf(gs, ls, idle, a) = gs; (s) ⊦ idle ≠ invInsert; (s) ⊦ idle ≠ invMember; (s) ⊦ invInsert ≠ invMember; (s) ⊦ gstepf(gs, ls, idle, a) = gs; (s) ⊦ invINSERT(tid, invINSERTe) = invINSERT(tid0, invINSERTe0) ↔ tid = tid0 ∧ invINSERTe = invINSERTe0; (ws) ⊦ invINSERT(tid, invINSERTe) ≠ invMEMBER(tid0, invINSERTe0); (s) ⊦ pre(gs, ls, idle, a) ↔ (∃ e1. a = invINSERT(ls.tid, e1) ∧ e1 ≠ ⊥) ∨ (∃ e1. a = invMEMBER(ls.tid, e1) ∧ e1 ≠ ⊥); (s) ⊦ ls.tid = tid → pcstepf(gs, ls, idle, invINSERT(tid, e1)) = I1; (s) ⊦ ls.tid = tid → lstepf(gs, ls, idle, invINSERT(tid, e1)) = ls.e:= e1; (s)

Proof step 3 from proof step-absstep-idle-I1-invINSERT-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).e:= e1 = mkls(tid, e1, b, sz, sz0, sz1, e0); (s) ⊦ mkls(tid, e, b, sz, sz0, sz1, e0).tid = tid; (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