Proof step 1 from proof insert-inset-after-retinsert-ind (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), ¬ 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)

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 3:

  SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ 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)

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # al

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  al = [], SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ sl.last.pcf(tid) = retInsert ∧ (sl.last.lsf(tid).lb → e ∈ sl.last.gstate.set), sl.last.pcf(tid) = invInsert ∧ sl.last.lsf(tid).le = e

• Proof step 26:

  al ≠ [], SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ sl.last.pcf(tid) = retInsert ∧ (sl.last.lsf(tid).lb → e ∈ sl.last.gstate.set), sl.last.pcf(tid) = invInsert ∧ sl.last.lsf(tid).le = e

Rule argument

Additional information

Used formulas: al = []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) '), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ 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)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ [].map(f) = []; (s) ⊦ ext !([]) = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ a + x = a ' + x; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  sl.last = mkstate(gstate, lsf, pcf), SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) '), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  sl.last = mkstate(gstate, lsf, pcf), sl = s + sl0, SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) '), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  sl0.head = mkstate(gstate, lsf, pcf), sl0.tail = [], sl0 ≠ [], SetInv(s.gstate, s.lsf, s.pcf), setStep(s, AInvInsert(tid, e), mkstate(gstate, lsf, pcf)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).head = a; (s) ⊦ a + x = a ' + x; (s) ⊦ x ≠ [] ∧ x.tail = [] → x.last = x.head; (s) ⊦ x ≠ [] → (a ' + x).last = x.last; (s) ⊦ frag*(IOAut(start, step, ext))(s ' + sl, a ') ↔ step(s, a, sl.head) ∧ sl ≠ [] ∧ sl.tail = []; (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  sl0.head = mkstate(gstate, lsf, pcf), sl0.tail = [], s = mkstate(gstate0, lsf0, pcf0), sl0 ≠ [], SetInv(s.gstate, s.lsf, s.pcf), setStep(s, AInvInsert(tid, e), mkstate(gstate, lsf, pcf)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used simplifier rules: SetState freely generated by mkstate;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  sl0.head = mkstate(gstate, lsf, pcf), sl0.tail = [], sl0 ≠ [], SetInv(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), setStep(mkstate(gstate0, lsf0, pcf0), AInvInsert(tid, e), mkstate(gstate, lsf, pcf)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: SetInv-thm: ⊦ SetInv(gs, lsf, pcf) ∧ setStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → SetInv(gs0, lsf0, pcf0); (forward) from specification Set-proofs ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  s = mkstate(gstate, lsf, pcf), sl0 = s + sl1, sl1 = [], sl0 ≠ [], SetInv(gstate, lsf, pcf), SetInv(gstate0, lsf0, pcf0), setStep(mkstate(gstate0, lsf0, pcf0), AInvInsert(tid, e), mkstate(gstate, lsf, pcf)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: sl0, s, sl1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  SetInv(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), setStep(mkstate(gstate0, lsf0, pcf0), AInvInsert(tid, e), mkstate(gstate, lsf, pcf)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ 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 14:

  SetInv(gstate, lsf, pcf), SetInv(gstate0, lsf0, pcf0), ∃ tid0, ls, pc. lstep(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e), gstate, ls, pc) ∧ lsf = lsf0(tid0 := ls) ∧ pcf = pcf0(tid0 := pc), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used terms: lsf0, pcf0, pcf, lsf, gstate, gstate0, AInvInsert(tid, e)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  SetInv (gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), lsf0(tid0 := lstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e))), pcf0(tid0 := pcstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)))), SetInv(gstate0, lsf0, pcf0), pre(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ (tid0 = tid ⊃ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));pcf0(tid)) = invInsert ∧ (tid0 = tid ⊃ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));lsf0(tid)).le = e, (tid0 = tid ⊃ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));pcf0(tid)) = retInsert ∧ ( (tid0 = tid ⊃ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));lsf0(tid)).lb → e ∈ gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)).set)

Rule argument

Additional information

Used simplifier rules: ⊦ 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 15 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 16:

  tid0 = tid, SetInv(gstate0, lsf0, pcf0), SetInv (gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), lsf0(tid0 := lstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e))), pcf0(tid0 := pcstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)))), pre(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ (tid0 = tid ⊃ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));pcf0(tid)) = retInsert ∧ ( (tid0 = tid ⊃ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));lsf0(tid)).lb → e ∈ gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)).set), (tid0 = tid ⊃ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));pcf0(tid)) = invInsert ∧ (tid0 = tid ⊃ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));lsf0(tid)).le = e

• Proof step 24:

  tid0 ≠ tid, SetInv(gstate0, lsf0, pcf0), SetInv (gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), lsf0(tid0 := lstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e))), pcf0(tid0 := pcstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)))), pre(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ (tid0 = tid ⊃ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));pcf0(tid)) = retInsert ∧ ( (tid0 = tid ⊃ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));lsf0(tid)).lb → e ∈ gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)).set), (tid0 = tid ⊃ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));pcf0(tid)) = invInsert ∧ (tid0 = tid ⊃ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e));lsf0(tid)).le = e

Rule argument

Additional information

Used formulas: tid0 = tid

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  SetInv (gstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)), lsf0(tid := lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e))), pcf0(tid := pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)))), SetInv(gstate0, lsf0, pcf0), pre(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)) = invInsert ∧ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)).le = e, pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)) = retInsert ∧ (lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)).lb → e ∈ gstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)).set)

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 18:

  pcf0(tid) = idle, SetInv(gstate0, lsf0, pcf0), SetInv (gstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)), lsf0(tid := lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e))), pcf0(tid := pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)))), pre(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)) = retInsert ∧ (lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)).lb → e ∈ gstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)).set), pcstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)) = invInsert ∧ lstepf(gstate0, lsf0(tid), pcf0(tid), AInvInsert(tid, e)).le = e

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) ⊦ AInvInsert(tid, e) ≠ ARetMember(tid0, b); (s) ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ AInvInsert(tid, e) ≠ ARetInsert(tid0, b); (s) ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s) ⊦ ADoMember(tid) ≠ AInvInsert(tid0, e); (s) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s) ⊦ ADoInsert(tid, b) ≠ AInvInsert(tid0, e); (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  pcf0(tid) = idle, e0 ≠ ⊥, SetInv (gstate0, lsf0(tid := lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0))), pcf0(tid := pcstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)))), SetInv(gstate0, lsf0, pcf0), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)) = retInsert ∧ (lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)).lb → e0 ∈ gstate0.set), pcstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)) = invInsert ∧ lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)).le = e0

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ gstepf(gs, ls, idle, a) = gs; (s) ⊦ AInvInsert(tid, e) = AInvInsert(tid0, e0) ↔ tid = tid0 ∧ e = e0; (ws) ⊦ AInvInsert(tid, e) ≠ AInvMember(tid0, e0); (s) ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ls.tid = tid → pcstepf(gs, ls, idle, AInvInsert(tid, e)) = invInsert

• Proof step 21:

  lsf0(tid).tid = tid, pcf0(tid) = idle, e0 ≠ ⊥, SetInv(gstate0, lsf0, pcf0), SetInv(gstate0, lsf0(tid := lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0))), pcf0(tid := invInsert)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ invInsert = invInsert ∧ lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)).le = e0, invInsert = retInsert ∧ (lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)).lb → e0 ∈ gstate0.set)

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; Used terms: gstate0, lsf0(tid), tid, e0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  pcf0(tid) = idle, lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0)).le ≠ e0, e0 ≠ ⊥, SetInv(gstate0, lsf0(tid := lstepf(gstate0, lsf0(tid), idle, AInvInsert(tid, e0))), pcf0(tid := invInsert)), SetInv(gstate0, lsf0, pcf0), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ invInsert ≠ retInsert; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ ls.tid = tid → lstepf(gs, ls, idle, AInvInsert(tid, e)) = ls.le:= e

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; ⊦ (ls.le:= le).le = le; (s) Used terms: gstate0, lsf0(tid), tid, e0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  tid0 ≠ tid, SetInv (gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), lsf0(tid0 := lstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e))), pcf0(tid0 := pcstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)))), SetInv(gstate0, lsf0, pcf0), pre(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)), ∀ al0, sl, tid, e. # al0 < # [] → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf0(tid) = invInsert ∧ lsf0(tid).le = e, pcf0(tid) = retInsert ∧ (lsf0(tid).lb → e ∈ gstepf(gstate0, lsf0(tid0), pcf0(tid0), AInvInsert(tid, e)).set)

Rule argument

Additional information

Proof step 25 from proof insert-inset-after-retinsert-ind (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) ⊦ AInvInsert(tid, e) ≠ ARetMember(tid0, b); (s) ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ AInvInsert(tid, e) ≠ ARetInsert(tid0, b); (s) ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s) ⊦ ADoMember(tid) ≠ AInvInsert(tid0, e); (s) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s) ⊦ ADoInsert(tid, b) ≠ AInvInsert(tid0, e); (s) ⊦ gstepf(gs, ls, idle, a) = gs; (s) ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥); (s) ⊦ AInvInsert(tid, e) ≠ AInvMember(tid0, e0); (s) ⊦ AInvInsert(tid, e) = AInvInsert(tid0, e0) ↔ tid = tid0 ∧ e = e0; (ws)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  al ≠ [], SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ 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)

Rule argument

Additional information

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

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

  sl = sl0 + s ', al ≠ [], sl ≠ [], SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ s.pcf(tid) = retInsert ∧ (s.lsf(tid).lb → e ∈ s.gstate.set), s.pcf(tid) = invInsert ∧ s.lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ 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 28 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  al ≠ [], SetInv((sl0 + s ').head.gstate, (sl0 + s ').head.lsf, (sl0 + s ').head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0 + s ', AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ s.pcf(tid) = invInsert ∧ s.lsf(tid).le = e, s.pcf(tid) = retInsert ∧ (s.lsf(tid).lb → e ∈ s.gstate.set)

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 30:

  s = mkstate(gstate, lsf, pcf), al ≠ [], SetInv((sl0 + s ').head.gstate, (sl0 + s ').head.lsf, (sl0 + s ').head.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0 + s ', AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

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 30 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  al ≠ [], 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 + mkstate(gstate, lsf, pcf) ', AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 32:

  sl0 + mkstate(gstate, lsf, pcf) ' = s + sl1, sl0 + mkstate(gstate, lsf, pcf) ' ≠ [], al ≠ [], SetInv(s.gstate, s.lsf, s.pcf), frag*(IOAut(setInit, setStep, setExt))(sl0 + mkstate(gstate, lsf, pcf) ', AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

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, sl1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  sl0 + mkstate(gstate, lsf, pcf) ' = s ' + sl1, al ≠ [], SetInv(s.gstate, s.lsf, s.pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate, lsf, pcf) = s ∨ mkstate(gstate, lsf, pcf) ∈ sl1, s ∈ sl0 ∨ s = mkstate(gstate, lsf, pcf), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

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 33 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 34:

  sl0 + mkstate(gstate, lsf, pcf) ' = s ' + sl1, s = mkstate(gstate0, lsf0, pcf0), al ≠ [], SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), s ∈ sl0 ∨ s = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = s ∨ mkstate(gstate, lsf, pcf) ∈ sl1, ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

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 34 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, al ≠ [], SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.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) ⊦ 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 35 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ x = [] ↔ ¬(∃ y, a. x = y + a ')

• Proof step 37:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al), ¬ tid ∈ setExt !(al).map(.tid), ∃ y, a. al = y + a ', 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) ∈ sl1, ∀ al0, sl, tid, e. # al0 < # al → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al0) ∧ ¬ tid ∈ setExt !(al0).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used terms: al

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al0 + a '), ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ (x + y).map(f) = x.map(f) + y.map(f); (s) ⊦ ext !(a ') = (ext(a) = τ ⊃ [];ext(a).e '); (s) ⊦ ext !(al + al0) = ext !(al) + ext !(al0); (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, frag*(IOAut(setInit, setStep, setExt))(sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a ') ↔ setStep(sl0.last, a, mkstate(gstate, lsf, pcf)) ∧ frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al0), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, AInvInsert(tid, e) ' + al0 + a '), ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').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) ∈ sl1, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used terms: AInvInsert(tid, e) ' + al0, mkstate(gstate, lsf, pcf), setExt, sl0, a, setInit, setStep

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), setStep(sl0.last, a, mkstate(gstate, lsf, pcf)) ∧ frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al0), 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) ∈ sl1, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 42:

  sl0 + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, sl0 = sl2 + s ', sl0 ≠ [], SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), setStep(s, a, mkstate(gstate, lsf, pcf)), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl0 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

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.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: sl0, s, sl2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  (sl2 + s ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl2 + s ', AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), setStep(s, a, mkstate(gstate, lsf, pcf)), ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = s ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 44:

  (sl2 + s ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, s = mkstate(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(sl2 + s ', AInvInsert(tid, e) ' + al0), setStep(s, a, mkstate(gstate, lsf, pcf)), ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = s ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: SetState freely generated by mkstate;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  (sl2 + mkstate(gstate1, lsf1, pcf1) ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 46:

  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 47:

  (sl2 + mkstate(gstate1, lsf1, pcf1) ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), ¬ SetInv ((sl2 + mkstate(gstate1, lsf1, pcf1) ').head.gstate, (sl2 + mkstate(gstate1, lsf1, pcf1) ').head.lsf, (sl2 + mkstate(gstate1, lsf1, pcf1) ').head.pcf), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

• Proof step 49:

  (sl2 + mkstate(gstate1, lsf1, pcf1) ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), SetInv ((sl2 + mkstate(gstate1, lsf1, pcf1) ').last.gstate, (sl2 + mkstate(gstate1, lsf1, pcf1) ').last.lsf, (sl2 + mkstate(gstate1, lsf1, pcf1) ').last.pcf), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), (sl2 + mkstate(gstate1, lsf1, pcf1) ').head.gstate.set ⊆ (sl2 + mkstate(gstate1, lsf1, pcf1) ').last.gstate.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used terms: sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0

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

Lemma frag-rely-inv

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  (sl2 + mkstate(gstate1, lsf1, pcf1) ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), ¬ SetInv ((sl2 + mkstate(gstate1, lsf1, pcf1) ').head.gstate, (sl2 + mkstate(gstate1, lsf1, pcf1) ').head.lsf, (sl2 + mkstate(gstate1, lsf1, pcf1) ').head.pcf), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Proof step 48 from proof insert-inset-after-retinsert-ind (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 = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ 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 ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: sl2 + mkstate(gstate1, lsf1, pcf1) ', s, sl0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  (sl2 + mkstate(gstate1, lsf1, pcf1) ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, SetInv(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), (sl2 + mkstate(gstate1, lsf1, pcf1) ').head.gstate.set ⊆ gstate1.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: SetInv-thm: ⊦ SetInv(gs, lsf, pcf) ∧ setStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → SetInv(gs0, lsf0, pcf0); (forward) from specification Set-proofs ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (x + a ').last = a; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 51:

  (sl2 + mkstate(gstate1, lsf1, pcf1) ') + mkstate(gstate, lsf, pcf) ' = mkstate(gstate0, lsf0, pcf0) ' + sl1, sl2 + mkstate(gstate1, lsf1, pcf1) ' = s + sl0, sl2 + mkstate(gstate1, lsf1, pcf1) ' ≠ [], SetInv(gstate, lsf, pcf), SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl1, (AInvInsert(tid, e) ' + al0) + a '), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), s.gstate.set ⊆ gstate1.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate, lsf, pcf) ∈ sl1, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

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: sl2 + mkstate(gstate1, lsf1, pcf1) ', s, sl0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  sl2 + mkstate(gstate1, lsf1, pcf1) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, SetInv(gstate, lsf, pcf), SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a '), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), gstate0.set ⊆ gstate1.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), mkstate(gstate1, lsf1, pcf1) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate1, lsf1, pcf1) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.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) ⊦ 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 ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s)

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

User applied rule apply induction

And obtained the following new goals

• Proof step 53:

  sl2 + mkstate(gstate1, lsf1, pcf1) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, SetInv(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), gstate0.set ⊆ gstate1.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate1, lsf1, pcf1) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate1, lsf1, pcf1) ∈ sl0, (mkstate(gstate0, lsf0, pcf0) ' + sl0).last.pcf(tid) = invInsert ∧ (mkstate(gstate0, lsf0, pcf0) ' + sl0).last.lsf(tid).le = e ∨ (mkstate(gstate0, lsf0, pcf0) ' + sl0).last.pcf(tid) = retInsert ∧ ((mkstate(gstate0, lsf0, pcf0) ' + sl0).last.lsf(tid).lb → e ∈ (mkstate(gstate0, lsf0, pcf0) ' + sl0).last.gstate.set), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ (a ' + x).head = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: al0, mkstate(gstate0, lsf0, pcf0) ' + sl0, tid, e

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 54:

  sl2 + mkstate(gstate1, lsf1, pcf1) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, (mkstate(gstate0, lsf0, pcf0) ' + sl0).last = mkstate(gstate2, lsf2, pcf2), SetInv(gstate, lsf, pcf), SetInv(gstate1, lsf1, pcf1), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a '), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), gstate0.set ⊆ gstate1.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), mkstate(gstate1, lsf1, pcf1) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate1, lsf1, pcf1) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set)

Rule argument

Additional information

Used simplifier rules: ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf); (elim) Used terms: (mkstate(gstate0, lsf0, pcf0) ' + sl0).last, gstate2, lsf2, pcf2

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

User applied rule subst equation

And obtained the following new goals

• Proof step 55:

  sl2 + mkstate(gstate1, lsf1, pcf1) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, (sl2 + mkstate(gstate1, lsf1, pcf1) ').last = mkstate(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(sl2 + mkstate(gstate1, lsf1, pcf1) ', AInvInsert(tid, e) ' + al0), setStep(mkstate(gstate1, lsf1, pcf1), a, mkstate(gstate, lsf, pcf)), gstate0.set ⊆ gstate1.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate1, lsf1, pcf1) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate1, lsf1, pcf1) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate1, lsf1, pcf1) ∈ sl0, pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, SetInv(gstate, lsf, pcf), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a '), setStep(mkstate(gstate2, lsf2, pcf2), a, mkstate(gstate, lsf, pcf)), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = invInsert ∧ lsf(tid).le = e, pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.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) ⊦ 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 ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0; (ws) ⊦ (x + a ').last = a; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ 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 58:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate, lsf, pcf) ', (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ∃ tid, ls, pc. lstep(gstate2, lsf2(tid), pcf2(tid), a, gstate, ls, pc) ∧ lsf = lsf2(tid := ls) ∧ pcf = pcf2(tid := pc), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate, lsf, pcf), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcf(tid) = retInsert ∧ (lsf(tid).lb → e ∈ gstate.set), pcf(tid) = invInsert ∧ lsf(tid).le = e

Rule argument

Additional information

Used terms: lsf2, pcf2, pcf, lsf, gstate, gstate2, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), pre(gstate2, lsf2(tid0), pcf2(tid0), a), gstate0.set ⊆ gstate2.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ (tid0 = tid ⊃ pcstepf(gstate2, lsf2(tid), pcf2(tid), a);pcf2(tid)) = retInsert ∧ ((tid0 = tid ⊃ lstepf(gstate2, lsf2(tid), pcf2(tid), a);lsf2(tid)).lb → e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set), (tid0 = tid ⊃ pcstepf(gstate2, lsf2(tid), pcf2(tid), a);pcf2(tid)) = invInsert ∧ (tid0 = tid ⊃ lstepf(gstate2, lsf2(tid), pcf2(tid), a);lsf2(tid)).le = e

Rule argument

Additional information

Used simplifier rules: ⊦ 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 59 from proof insert-inset-after-retinsert-ind (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 60:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, tid0 = tid, SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid0), pcf2(tid0), a), gstate0.set ⊆ gstate2.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ (tid0 = tid ⊃ pcstepf(gstate2, lsf2(tid), pcf2(tid), a);pcf2(tid)) = invInsert ∧ (tid0 = tid ⊃ lstepf(gstate2, lsf2(tid), pcf2(tid), a);lsf2(tid)).le = e, (tid0 = tid ⊃ pcstepf(gstate2, lsf2(tid), pcf2(tid), a);pcf2(tid)) = retInsert ∧ ((tid0 = tid ⊃ lstepf(gstate2, lsf2(tid), pcf2(tid), a);lsf2(tid)).lb → e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set)

• Proof step 73:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, tid0 ≠ tid, SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid0), pcf2(tid0), a), gstate0.set ⊆ gstate2.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ (tid0 = tid ⊃ pcstepf(gstate2, lsf2(tid), pcf2(tid), a);pcf2(tid)) = invInsert ∧ (tid0 = tid ⊃ lstepf(gstate2, lsf2(tid), pcf2(tid), a);lsf2(tid)).le = e, (tid0 = tid ⊃ pcstepf(gstate2, lsf2(tid), pcf2(tid), a);pcf2(tid)) = retInsert ∧ ((tid0 = tid ⊃ lstepf(gstate2, lsf2(tid), pcf2(tid), a);lsf2(tid)).lb → e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set)

Rule argument

Additional information

Used formulas: tid0 = tid

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid), pcf2(tid), a), lsf2(tid := lstepf(gstate2, lsf2(tid), pcf2(tid), a)), pcf2(tid := pcstepf(gstate2, lsf2(tid), pcf2(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid), pcf2(tid), a), lsf2(tid := lstepf(gstate2, lsf2(tid), pcf2(tid), a)), pcf2(tid := pcstepf(gstate2, lsf2(tid), pcf2(tid), a))) ', (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), pre(gstate2, lsf2(tid), pcf2(tid), a), gstate0.set ⊆ gstate2.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid), pcf2(tid), a), lsf2(tid := lstepf(gstate2, lsf2(tid), pcf2(tid), a)), pcf2(tid := pcstepf(gstate2, lsf2(tid), pcf2(tid), a))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, pcf2(tid) = invInsert ∧ lsf2(tid).le = e ∨ pcf2(tid) = retInsert ∧ (lsf2(tid).lb → e ∈ gstate2.set), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcstepf(gstate2, lsf2(tid), pcf2(tid), a) = retInsert ∧ (lstepf(gstate2, lsf2(tid), pcf2(tid), a).lb → e ∈ gstepf(gstate2, lsf2(tid), pcf2(tid), a).set), pcstepf(gstate2, lsf2(tid), pcf2(tid), a) = invInsert ∧ lstepf(gstate2, lsf2(tid), pcf2(tid), a).le = e

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 62:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, lsf2(tid).le = e, pcf2(tid) = invInsert, SetInv (gstepf(gstate2, lsf2(tid), pcf2(tid), a), lsf2(tid := lstepf(gstate2, lsf2(tid), pcf2(tid), a)), pcf2(tid := pcstepf(gstate2, lsf2(tid), pcf2(tid), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid), pcf2(tid), a), lsf2(tid := lstepf(gstate2, lsf2(tid), pcf2(tid), a)), pcf2(tid := pcstepf(gstate2, lsf2(tid), pcf2(tid), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid), pcf2(tid), a), gstate0.set ⊆ gstate2.set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid), pcf2(tid), a), lsf2(tid := lstepf(gstate2, lsf2(tid), pcf2(tid), a)), pcf2(tid := pcstepf(gstate2, lsf2(tid), pcf2(tid), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦ pcstepf(gstate2, lsf2(tid), pcf2(tid), a) = invInsert ∧ lstepf(gstate2, lsf2(tid), pcf2(tid), a).le = e, pcstepf(gstate2, lsf2(tid), pcf2(tid), a) = retInsert ∧ (lstepf(gstate2, lsf2(tid), pcf2(tid), a).lb → e ∈ gstepf(gstate2, lsf2(tid), pcf2(tid), a).set)

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ext-RetInsert: ⊦ setExt(ARetInsert(tid, b)) = ⌜RetInsert(tid, b)⌝ ; sel-RetInsert-dottid: ⊦ RetInsert(tid, b).tid = tid; ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s) ⊦ ⌜e⌝ ≠ τ; (s) ⊦ ⌜e⌝ .e = e; (s) ⊦ a '.map(f) = f(a) '; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = invInsert, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := pcstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := pcstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)))) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, b) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := pcstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦ pcstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)) = retInsert ∧ (lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).lb → lsf2(tid).le ∈ gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).set), pcstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)) = invInsert ∧ lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).le = lsf2(tid).le

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ext-DoInsert: ⊦ setExt(ADoInsert(tid, b)) = τ; ⊦ ¬ a ∈ []; (s) ⊦ [].map(f) = []; (s) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

  ⊦ ls.tid = tid → pcstepf(gs, ls, invInsert, ADoInsert(tid, b)) = retInsert

• Proof step 65:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, lsf2(tid).tid = tid, pcf2(tid) = invInsert, SetInv (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, b) '), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦ retInsert = invInsert ∧ lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).le = lsf2(tid).le, retInsert = retInsert ∧ (lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).lb → lsf2(tid).le ∈ gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).set)

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; Used terms: gstate2, lsf2(tid), tid, b

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = invInsert, lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, b) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ lsf2(tid).le ∈ gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).set, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ invInsert ≠ retInsert; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ ls.tid = tid → gstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ gs.set:= (gs.set ++ ls.le);gs)

• Proof step 68:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, lsf2(tid).tid = tid, pcf2(tid) = invInsert, lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).lb, SetInv ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, b) '), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ lsf2(tid).le ∈ (b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2).set, mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; Used terms: gstate2, lsf2(tid), tid, b

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = invInsert, lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, b) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ lsf2(tid).le ∈ (b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2).set, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid;

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

User applied rule case distinction

And obtained the following new goals

• Proof step 70:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, ¬ b, pcf2(tid) = invInsert, lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b)).lb, SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, b) '), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ lsf2(tid).le ∈ (b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2).set, mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid).le);gstate2), lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, b))), pcf2(tid := retInsert)), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (gs.set:= set).set = set; (s) ⊦ a ∈ s ++ b ↔ ¬(a ≠ b ∧ ¬ a ∈ s); (ss)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = invInsert, lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, false)).lb, SetInv(gstate2, lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, false))), pcf2(tid := retInsert)), SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, lsf2(tid).le) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate(gstate2, lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, false))), pcf2(tid := retInsert)) ', (AInvInsert(tid, lsf2(tid).le) ' + al0) + ADoInsert(tid, false) '), gstate0.set ⊆ gstate2.set, ¬ tid ∈ setExt !(al0).map(.tid), ¬ lsf2(tid).le ∈ gstate2.set, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2(tid := lstepf(gstate2, lsf2(tid), invInsert, ADoInsert(tid, false))), pcf2(tid := retInsert)), ∀ al1, sl, tid0, e. # al1 < #(al0 + ADoInsert(tid, false) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid0, e) + al1) ∧ ¬ tid0 ∈ setExt !(al1).map(.tid) → sl.last.pcf(tid0) = invInsert ∧ sl.last.lsf(tid0).le = e ∨ sl.last.pcf(tid0) = retInsert ∧ (sl.last.lsf(tid0).lb → e ∈ sl.last.gstate.set) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ ls.tid = tid → lstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ ls.lb:= true;ls.lb:= false)

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; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (ls.lb:= lb).lb ↔ lb; (s) Used terms: gstate2, lsf2(tid), tid, false

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), pre(gstate2, lsf2(tid0), pcf2(tid0), a), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ⊦ invInsert ≠ retInsert; (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 75:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = retInsert, pcf2(tid0) = invInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid0), pcf2(tid0), a), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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 80:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = retInsert, pcf2(tid0) = invMember, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid0), pcf2(tid0), a), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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 83:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = retInsert, pcf2(tid0) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid0), pcf2(tid0), a), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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 86:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid) = retInsert, pcf2(tid0) = retMember, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))) ', (AInvInsert(tid, e) ' + al0) + a '), pre(gstate2, lsf2(tid0), pcf2(tid0), a), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), pcf2(tid0), a).set, ¬ tid ∈ (setExt(a) = τ ⊃ [];setExt(a).e ').map(.tid), ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), pcf2(tid0), a), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), pcf2(tid0), a)), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), pcf2(tid0), a))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + a ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; SetPC freely generated by idle, invInsert, invMember, retInsert, retMember;; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ pre(gs, ls, idle, a) ↔ (∃ e. a = AInvInsert(ls.tid, e) ∧ e ≠ ⊥) ∨ (∃ e. a = AInvMember(ls.tid, e) ∧ e ≠ ⊥); (s) ⊦ gstepf(gs, ls, idle, a) = gs; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid0) = invInsert, pcf2(tid) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))) ', (AInvInsert(tid, e) ' + al0) + ADoInsert(tid0, b) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)).set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid, e. # al1 < #(al0 + ADoInsert(tid0, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ext-DoInsert: ⊦ setExt(ADoInsert(tid, b)) = τ; ⊦ ¬ a ∈ []; (s) ⊦ [].map(f) = []; (s) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

  ⊦ ls.tid = tid → gstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ gs.set:= (gs.set ++ ls.le);gs)

• Proof step 78:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, lsf2(tid0).tid = tid0, pcf2(tid) = retInsert, pcf2(tid0) = invInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))), SetInv(gstate2, lsf2, pcf2), SetInv(gstate0, lsf0, pcf0), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))) ', (AInvInsert(tid, e) ' + al0) + ADoInsert(tid0, b) '), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ (b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2).set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), ∀ al1, sl, tid, e. # al1 < #(al0 + ADoInsert(tid0, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; Used terms: gstate2, lsf2(tid0), tid0, b

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid0) = invInsert, pcf2(tid) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))) ', (AInvInsert(tid, e) ' + al0) + ADoInsert(tid0, b) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ (b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2).set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate ((b ⊃ gstate2.set:= (gstate2.set ++ lsf2(tid0).le);gstate2), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invInsert, ADoInsert(tid0, b)))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid, e. # al1 < #(al0 + ADoInsert(tid0, b) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid;

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

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (gs.set:= set).set = set; (s) ⊦ a ∈ s → a ∈ s ++ b; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid0) = invMember, pcf2(tid) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)))) ', (AInvInsert(tid, e) ' + al0) + ADoMember(tid0) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)).set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), invMember, ADoMember(tid0)))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid, e. # al1 < #(al0 + ADoMember(tid0) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ext-DoMember: ⊦ setExt(ADoMember(tid)) = τ; ⊦ ¬ a ∈ []; (s) ⊦ [].map(f) = []; (s) ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

  ⊦ ls.tid = tid → gstepf(gs, ls, invMember, ADoMember(tid)) = gs

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid0) = retInsert, pcf2(tid) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)))) ', (AInvInsert(tid, e) ' + al0) + ARetInsert(tid0, lsf2(tid0).lb) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)).set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), retInsert, ARetInsert(tid0, lsf2(tid0).lb)))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid, e. # al1 < #(al0 + ARetInsert(tid0, lsf2(tid0).lb) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ext-RetInsert: ⊦ setExt(ARetInsert(tid, b)) = ⌜RetInsert(tid, b)⌝ ; sel-RetInsert-dottid: ⊦ RetInsert(tid, b).tid = tid; ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a '.map(f) = f(a) '; (s) ⊦ ⌜e⌝ .e = e; (s) ⊦ ⌜e⌝ ≠ τ; (s) ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

  ⊦ 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: gstate2, lsf2(tid0), tid0, lsf2(tid0).lb

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  sl2 + mkstate(gstate2, lsf2, pcf2) ' = mkstate(gstate0, lsf0, pcf0) ' + sl0, pcf2(tid0) = retMember, pcf2(tid) = retInsert, # gstate2.set ≠ 0, gstate2.set ≠ ∅, tid0 ≠ tid, lsf2(tid).lb, SetInv(gstate0, lsf0, pcf0), SetInv(gstate2, lsf2, pcf2), SetInv (gstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate(gstate0, lsf0, pcf0) ' + sl0 + mkstate (gstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)))) ', (AInvInsert(tid, e) ' + al0) + ARetMember(tid0, lsf2(tid0).lb) '), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate0, lsf0, pcf0) ' + sl0, AInvInsert(tid, e) ' + al0), e ∈ gstate2.set, gstate0.set ⊆ gstate2.set, ¬ e ∈ gstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)).set, ¬ tid ∈ setExt !(al0).map(.tid), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2), mkstate(gstate0, lsf0, pcf0) ∈ sl2 ∨ mkstate(gstate0, lsf0, pcf0) = mkstate(gstate2, lsf2, pcf2) ∨ mkstate(gstate0, lsf0, pcf0) = mkstate (gstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)), lsf2(tid0 := lstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb))), pcf2(tid0 := pcstepf(gstate2, lsf2(tid0), retMember, ARetMember(tid0, lsf2(tid0).lb)))), mkstate(gstate2, lsf2, pcf2) = mkstate(gstate0, lsf0, pcf0) ∨ mkstate(gstate2, lsf2, pcf2) ∈ sl0, ∀ al1, sl, tid, e. # al1 < #(al0 + ARetMember(tid0, lsf2(tid0).lb) ') → SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, AInvInsert(tid, e) + al1) ∧ ¬ tid ∈ setExt !(al1).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) ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ext-RetMember: ⊦ setExt(ARetMember(tid, b)) = ⌜RetMember(tid, b)⌝ ; sel-RetMember-dottid: ⊦ RetMember(tid, b).tid = tid; ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a '.map(f) = f(a) '; (s) ⊦ ⌜e⌝ .e = e; (s) ⊦ ⌜e⌝ ≠ τ; (s) ⊦ pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

  ⊦ ls.tid = tid → gstepf(gs, ls, retMember, ARetMember(tid, b0)) = gs

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; Used terms: gstate2, lsf2(tid0), tid0, lsf2(tid0).lb

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

A spec-lemma