Proof step 1 from proof insert-inset-after-retinsert (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + (al + ARetInsert(tid, true))), ¬ e ∈ sl.last.gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Proof step 2 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  sl = sl0 + s ', sl ≠ [], SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + (al + ARetInsert(tid, true))), ¬ e ∈ s.gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + a = x + a '; (s) ⊦ a + x = a ' + x; (s) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: sl, s, sl0

Proof step 3 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  SetInv((sl0 + s ').head.gstate, (sl0 + s ').head.lsf, (sl0 + s ').head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0 + s ', AInvInsert(tid, e) ' + al + ARetInsert(tid, true) '), ¬ e ∈ s.gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ x + a = x + a '; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 4 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ frag*(IOAut(start, step, ext))(sl + s ', al + a ') ↔ step(sl.last, a, s) ∧ frag*(IOAut(start, step, ext))(sl, al)

• Proof step 6:

  SetInv((sl0 + s ').head.gstate, (sl0 + s ').head.lsf, (sl0 + s ').head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), s), ¬ e ∈ s.gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: AInvInsert(tid, e) ' + al, s, setExt, sl0, ARetInsert(tid, true), setInit, setStep

Proof step 5 from proof insert-inset-after-retinsert (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  s = mkstate(gstate, lsf, pcf), SetInv((sl0 + s ').head.gstate, (sl0 + s ').head.lsf, (sl0 + s ').head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), s), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf); (elim) Used terms: s, gstate, lsf, pcf

Proof step 7 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  SetInv((sl0 + mkstate(gstate, lsf, pcf) ').head.gstate, (sl0 + mkstate(gstate, lsf, pcf) ').head.lsf, (sl0 + mkstate(gstate, lsf, pcf) ').head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Proof step 8 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  sl0 + mkstate(gstate, lsf, pcf) ' = s + sl, sl0 + mkstate(gstate, lsf, pcf) ' ≠ [], SetInv(s.gstate, s.lsf, s.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: sl0 + mkstate(gstate, lsf, pcf) ', s, sl

Proof step 9 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  sl0 + mkstate(gstate, lsf, pcf) ' = s ' + sl, SetInv(s.gstate, s.lsf, s.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ tid ∈ setExt !(al).map(.tid), ¬ e ∈ gstate.set, mkstate(gstate, lsf, pcf) = s ∨ mkstate(gstate, lsf, pcf) ∈ sl, s ∈ sl0 ∨ s = mkstate(gstate, lsf, pcf) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s)

Proof step 10 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  sl0 + mkstate(gstate, lsf, pcf) ' = s ' + sl, s = mkstate(gstate0, lsf0, pcf0), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ tid ∈ setExt !(al).map(.tid), ¬ e ∈ gstate.set, s ∈ sl0 ∨ s = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = s ∨ mkstate(gstate, lsf, pcf) ∈ sl ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf); (elim) Used terms: s, gstate0, lsf0, pcf0

Proof step 11 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list

Proof step 12 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al), SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), ¬ tid ∈ setExt !(al).map(.tid) ⊦ sl.last.pcf(tid) = invInsert ∧ sl.last.lsf(tid).le = e ∨ sl.last.pcf(tid) = retInsert ∧ (sl.last.lsf(tid).lb → e ∈ sl.last.gstate.set)

• Proof step 14:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl ⊦ frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) + al) ∧ SetInv(sl0.head.gstate, sl0.head.lsf, sl0.head.pcf)

• Proof step 16:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl, sl0.last.pcf(tid) = invInsert ∧ sl0.last.lsf(tid).le = e ∨ sl0.last.pcf(tid) = retInsert ∧ (sl0.last.lsf(tid).lb → e ∈ sl0.last.gstate.set) ⊦

Rule argument

Additional information

Used terms: sl0, tid, e, al

Proof step 13 from proof insert-inset-after-retinsert (previous step) (back to tree)

Lemma insert-inset-after-retinsert-ind

Proof step 14 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ SetInv(sl0.head.gstate, sl0.head.lsf, sl0.head.pcf), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 15 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0; (ws) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: sl0, s, sl1

Proof step 16 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(sl0.last, ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf); (elim) Used terms: sl0.last, gstate1, lsf1, pcf1

Proof step 17 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), setStep(mkstate(gstate1, lsf1, pcf1), ARetInsert(tid, true), mkstate(gstate, lsf, pcf)), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl, pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set) ⊦

Rule argument

Additional information

Proof step 18 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ setStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ tid, ls, pc. lstep(gs, lsf(tid), pcf(tid), a, gs0, ls, pc) ∧ lsf0 = lsf(tid := ls) ∧ pcf0 = pcf(tid := pc))

• Proof step 20:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), ¬ e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid), ∃ tid0, ls, pc. lstep(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true), gstate, ls, pc) ∧ lsf = lsf1(tid0 := ls) ∧ pcf = pcf1(tid0 := pc), pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf) ⊦

Rule argument

Additional information

Used terms: lsf1, pcf1, pcf, lsf, gstate, gstate1, ARetInsert(tid, true)

Proof step 19 from proof insert-inset-after-retinsert (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  sl0 + mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ∈ sl, pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ lstep(gs, ls, pc, a, gs0, ls0, pc0) ↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a); (s)

Proof step 21 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 22:

  SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, al) ⊦ sl.head.gstate.set ⊆ sl.last.gstate.set ∧ SetInv(sl.last.gstate, sl.last.lsf, sl.last.pcf)

• Proof step 23:

  sl0 + mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), ¬ SetInv(sl0.head.gstate, sl0.head.lsf, sl0.head.pcf), ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))), pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ∈ sl ⊦

• Proof step 25:

  sl0 + mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), SetInv(sl0.last.gstate, sl0.last.lsf, sl0.last.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), sl0.head.gstate.set ⊆ sl0.last.gstate.set, ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))), pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ∈ sl ⊦

Rule argument

Additional information

Used terms: sl0, AInvInsert(tid, e) ' + al

Proof step 22 from proof insert-inset-after-retinsert (previous step) (back to tree)

Lemma frag-rely-inv

Proof step 23 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  sl0 + mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), ¬ SetInv(sl0.head.gstate, sl0.head.lsf, sl0.head.pcf), ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ∈ sl, pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ⊦

Rule argument

Additional information

Proof step 24 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0; (ws) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: sl0, s, sl1

Proof step 25 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  sl0 + mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), sl0.head.gstate.set ⊆ gstate1.set, ¬ tid ∈ setExt !(al).map(.tid), ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))), pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ∈ sl ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s)

Proof step 26 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 27:

  sl0 + mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ' = mkstate(gstate0, lsf0, pcf0) ' + sl, sl0.last = mkstate(gstate1, lsf1, pcf1), sl0 = s + sl1, sl0 ≠ [], SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), s.gstate.set ⊆ gstate1.set, ¬ tid ∈ setExt !(al).map(.tid), ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ∈ sl, pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set), mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), lsf1(tid0 := lstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true))), pcf1(tid0 := pcstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0; (ws) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: sl0, s, sl1

Proof step 27 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  (mkstate(gstate0, lsf0, pcf0) ' + sl1).last = mkstate(gstate1, lsf1, pcf1), SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), gstate0.set ⊆ gstate1.set, ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), pcf1(tid) = invInsert ∧ lsf1(tid).le = e ∨ pcf1(tid) = retInsert ∧ (lsf1(tid).lb → e ∈ gstate1.set) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws)

Proof step 28 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  (mkstate(gstate0, lsf0, pcf0) ' + sl1).last = mkstate(gstate1, lsf1, pcf1), lsf1(tid).le = e, pcf1(tid) = invInsert, SetInv(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), gstate0.set ⊆ gstate1.set, ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

• Proof step 31:

  (mkstate(gstate0, lsf0, pcf0) ' + sl1).last = mkstate(gstate1, lsf1, pcf1), pcf1(tid) = retInsert, SetInv(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), gstate0.set ⊆ gstate1.set, ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), lsf1(tid).lb → e ∈ gstate1.set ⊦

Rule argument

Additional information

Proof step 29 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  (mkstate(gstate0, lsf0, pcf0) ' + sl1).last = mkstate(gstate1, lsf1, pcf1), pcf1(tid) = invInsert, SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, lsf1(tid).le) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), gstate0.set ⊆ gstate1.set, ¬ lsf1(tid).le ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid) ⊦

Rule argument

Additional information

Proof step 30 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; SetPC freely generated by idle, invInsert, invMember, retInsert, retMember;; ⊦ pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ ARetInsert(tid, b) ≠ ARetMember(tid0, b0); (s) ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ ARetInsert(tid, b) = ARetInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ invInsert ≠ retInsert; (s) ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s) ⊦ ADoMember(tid) ≠ ARetInsert(tid0, b); (s) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s) ⊦ ADoInsert(tid, b) ≠ ARetInsert(tid0, b0); (s) ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥); (s) ⊦ AInvInsert(tid, e) ≠ ARetInsert(tid0, b); (s) ⊦ AInvMember(tid, e) ≠ ARetInsert(tid0, b); (s)

Proof step 31 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 32:

  (mkstate(gstate0, lsf0, pcf0) ' + sl1).last = mkstate(gstate1, lsf1, pcf1), pcf1(tid) = retInsert, pcf1(tid0) = retInsert, SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al), pre(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)), gstate0.set ⊆ gstate1.set, ¬ e ∈ gstepf(gstate1, lsf1(tid0), pcf1(tid0), ARetInsert(tid, true)).set, ¬ tid ∈ setExt !(al).map(.tid), lsf1(tid).lb → e ∈ gstate1.set ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; SetPC freely generated by idle, invInsert, invMember, retInsert, retMember;; ⊦ pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ ARetInsert(tid, b) ≠ ARetMember(tid0, b0); (s) ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s) ⊦ ADoMember(tid) ≠ ARetInsert(tid0, b); (s) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s) ⊦ ADoInsert(tid, b) ≠ ARetInsert(tid0, b0); (s) ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥); (s) ⊦ AInvInsert(tid, e) ≠ ARetInsert(tid0, b); (s) ⊦ AInvMember(tid, e) ≠ ARetInsert(tid0, b); (s)

Proof step 32 from proof insert-inset-after-retinsert (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  (mkstate(gstate0, lsf0, pcf0) ' + sl1).last = mkstate(gstate1, lsf1, pcf1), pcf1(tid0) = retInsert, # gstate1.set ≠ 0, gstate1.set ≠ ∅, lsf1(tid0).lb, SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid0, e) ' + al), e ∈ gstate1.set, gstate0.set ⊆ gstate1.set, ¬ tid0 ∈ setExt !(al).map(.tid), ¬ e ∈ gstepf(gstate1, lsf1(tid0), retInsert, ARetInsert(tid0, true)).set ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ ARetInsert(tid, b) = ARetInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s)

Proof step 33 from proof insert-inset-after-retinsert (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ ls.tid = tid → gstepf(gs, ls, retInsert, ARetInsert(tid, b0)) = gs

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; Used terms: gstate1, lsf1(tid0), tid0, true

Proof step 34 from proof insert-inset-after-retinsert (previous step) (back to tree)

A spec-lemma