Proof step 1 from proof frag-in (conclusion) (back to tree)

User applied rule structural induction

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, a + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < #(a + al0) ∧ (a + al0)[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ frag*(IOAut(start, step, ext))(sl, []) ↔ sl = sl.head '; (s) ⊦ # [] = 0; (s) ⊦ ¬ n < 0; (s) ⊦ x = x.head ' → x.last = x.head; (s)

Proof step 2 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

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, a ' + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 3 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  sl = s + sl0, sl ≠ [], SetInv(s.gstate, s.lsf, s.pcf), frag*(IOAut(setInit, setStep, setExt))(sl, a ' + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ sl.last.gstate.set ↔ e ∈ s.gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)

Rule argument

Additional information

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

Proof step 4 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  SetInv(s.gstate, s.lsf, s.pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl0, a ' + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ (s ' + sl0).last.gstate.set ↔ e ∈ s.gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (s ' + sl0)[n].lsf(tid).le = e ∧ (s ' + sl0)[n].pcf(tid) = invInsert)

Rule argument

Additional information

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

Proof step 5 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  s = mkstate(gstate, lsf, pcf), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl0, a ' + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ (s ' + sl0).last.gstate.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (s ' + sl0)[n].lsf(tid).le = e ∧ (s ' + sl0)[n].pcf(tid) = invInsert)

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 6 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate, lsf, pcf) ' + sl0, a ' + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ (mkstate(gstate, lsf, pcf) ' + sl0).last.gstate.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Proof step 7 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  (mkstate(gstate, lsf, pcf) ' + sl0).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate, lsf, pcf) ' + sl0, a ' + al0), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].pcf(tid) = invInsert)

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(gstate, lsf, pcf) ' + sl0).last, gstate0, lsf0, pcf0

Proof step 8 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  (mkstate(gstate, lsf, pcf) ' + sl0).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, al0), setStep(mkstate(gstate, lsf, pcf), a, sl0.head), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used terms: al0, mkstate(gstate, lsf, pcf), setExt, sl0, a, setInit, setStep

Proof step 9 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  (mkstate(gstate, lsf, pcf) ' + sl0).last = mkstate(gstate0, lsf0, pcf0), sl0 = s + sl1, sl0 ≠ [], SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(sl0, al0), setStep(mkstate(gstate, lsf, pcf), a, s), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + sl0)[n].pcf(tid) = invInsert)

Rule argument

Additional information

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

Proof step 11 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (s ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, s), ∀ sl, e. SetInv(sl.head.gstate, sl.head.lsf, sl.head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(sl, al0) → ( e ∈ sl.last.gstate.set ↔ e ∈ sl.head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ sl[n].lsf(tid).le = e ∧ sl[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].pcf(tid) = invInsert)

Rule argument

Additional information

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

Proof step 12 from proof frag-in (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  (s ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, s), SetInv((s ' + sl1).head.gstate, (s ' + sl1).head.lsf, (s ' + sl1).head.pcf) ∧ frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, al0) → ( e ∈ (s ' + sl1).last.gstate.set ↔ e ∈ (s ' + sl1).head.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (s ' + sl1)[n].lsf(tid).le = e ∧ (s ' + sl1)[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used terms: s ' + sl1, e

Proof step 13 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (s ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, s), SetInv(s.gstate, s.lsf, s.pcf) → ( e ∈ gstate0.set ↔ e ∈ s.gstate.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (s ' + sl1)[n].lsf(tid).le = e ∧ (s ' + sl1)[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used simplifier rules: ⊦ mkstate(gstate, lsf, pcf).gstate = gstate; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).head = a; (s)

Proof step 14 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  (s ' + sl1).last = mkstate(gstate0, lsf0, pcf0), s = mkstate(gstate1, lsf1, pcf1), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(s ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, s), SetInv(gstate1, lsf1, pcf1) → ( e ∈ gstate0.set ↔ e ∈ gstate1.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (s ' + sl1)[n].lsf(tid).le = e ∧ (s ' + sl1)[n].pcf(tid) = invInsert)) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + s ' + sl1)[n].pcf(tid) = invInsert)

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, gstate1, lsf1, pcf1

Proof step 15 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (mkstate(gstate1, lsf1, pcf1) ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate1, lsf1, pcf1) ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, mkstate(gstate1, lsf1, pcf1)), e ∈ gstate0.set ↔ e ∈ gstate1.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert)

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

Proof step 16 from proof frag-in (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 17:

  ⊦ SetInv(gs, lsf, pcf) ∧ setStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → SetInv(gs0, lsf0, pcf0)

• Proof step 18:

  (mkstate(gstate1, lsf1, pcf1) ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), SetInv(gstate1, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate1, lsf1, pcf1) ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, mkstate(gstate1, lsf1, pcf1)), SetInv(gstate, lsf, pcf) ∧ setStep(mkstate(gstate, lsf, pcf), a, mkstate(gstate1, lsf1, pcf1)) → SetInv(gstate1, lsf1, pcf1), e ∈ gstate0.set ↔ e ∈ gstate1.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used terms: lsf, pcf, pcf1, lsf1, gstate1, gstate, a

Proof step 17 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  (mkstate(gstate1, lsf1, pcf1) ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate1, lsf1, pcf1), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate1, lsf1, pcf1) ' + sl1, al0), setStep(mkstate(gstate, lsf, pcf), a, mkstate(gstate1, lsf1, pcf1)), e ∈ gstate0.set ↔ e ∈ gstate1.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Proof step 19 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

  (mkstate(gstate1, lsf1, pcf1) ' + sl1).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), SetInv(gstate1, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt))(mkstate(gstate1, lsf1, pcf1) ' + sl1, al0), e ∈ gstate0.set ↔ e ∈ gstate1.set ∨ (∃ n, tid. n < # al0 ∧ al0[n] = ADoInsert(tid, true) ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert), ∃ tid, ls, pc. lstep(gstate, lsf(tid), pcf(tid), a, gstate1, ls, pc) ∧ lsf1 = lsf(tid := ls) ∧ pcf1 = pcf(tid := pc) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid, true) ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].lsf(tid).le = e ∧ (mkstate(gstate, lsf, pcf) ' + mkstate(gstate1, lsf1, pcf1) ' + sl1)[n].pcf(tid) = invInsert)

Rule argument

Additional information

Used terms: lsf, pcf, pcf1, lsf1, gstate1, gstate, a

Proof step 20 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set ↔ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ (∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert)

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 22 from proof frag-in (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 23:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate.set, e ∈ gstate0.set ↔ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ (∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert)

• Proof step 39:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), ¬ e ∈ gstate.set, e ∈ gstate0.set ↔ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ (∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert) ⊦ e ∈ gstate0.set ↔ e ∈ gstate.set ∨ (∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert)

Rule argument

Additional information

Used formulas: e ∈ gstate.set

Proof step 23 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

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

Proof step 24 from proof frag-in (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 25:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = invInsert, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

• Proof step 30:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = invMember, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

• Proof step 33:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = retInsert, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

• Proof step 36:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = retMember, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

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;; ⊦ 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 25 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = invInsert, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1, al0), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s)

Proof step 26 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), lsf(tid).tid = tid, pcf(tid) = invInsert, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1, al0), e ∈ gstate.set, ¬ e ∈ (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

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

Proof step 27 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = invInsert, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1, al0), e ∈ gstate.set, ¬ e ∈ (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

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

Proof step 29 from proof frag-in (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.set:= set).set = set; (s) ⊦ a ∈ s → a ∈ s ++ b; (s)

Proof step 30 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = invMember, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1, al0), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), invMember, ADoMember(tid)).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s)

Proof step 31 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ 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: gstate, lsf(tid), tid

Proof step 32 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = retInsert, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1, al0), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ pre(gs, ls, retInsert, a) ↔ (∃ b0. a = ARetInsert(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s)

Proof step 34 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ 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: gstate, lsf(tid), tid, lsf(tid).lb

Proof step 35 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf(tid) = retMember, # gstate.set ≠ 0, gstate.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1, al0), e ∈ gstate.set, ¬ e ∈ gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)).set, ¬ e ∈ gstate0.set ⊦ ∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ pre(gs, ls, retMember, a) ↔ (∃ b0. a = ARetMember(ls.tid, b0) ∧ (b0 ↔ ls.lb)); (s)

Proof step 37 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ 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: gstate, lsf(tid), tid, lsf(tid).lb

Proof step 38 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), ¬ e ∈ gstate.set, e ∈ gstate0.set ↔ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ (∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert) ⊦ e ∈ gstate0.set ↔ (∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert)

Rule argument

Additional information

Proof step 40 from proof frag-in (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 41:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, ¬ e ∈ gstate.set, e ∈ gstate0.set ↔ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ (∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert) ⊦ ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

• Proof step 64:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), ¬ e ∈ gstate0.set, ¬ e ∈ gstate.set, e ∈ gstate0.set ↔ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ (∃ n, tid0. n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert), ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert ⊦

Rule argument

Additional information

Proof step 41 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), # gstate0.set ≠ 0, gstate0.set ≠ ∅, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, ¬ e ∈ gstate.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert ⊦ ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

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

Proof step 42 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 43:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), # gstate0.set ≠ 0, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, ¬ e ∈ gstate.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ lsf1(tid0).le = e ∧ pcf1(tid0) = invInsert ⊦ ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

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 (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ], gstate1, lsf1, pcf1

Proof step 43 from proof frag-in (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 44:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), # gstate0.set ≠ 0, gstate0.set ≠ ∅, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ lsf1(tid0).le = e ∧ pcf1(tid0) = invInsert ⊦ ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

• Proof step 62:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), # gstate0.set ≠ 0, gstate0.set ≠ ∅, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, ¬ e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ∨ n < # al0 ∧ al0[n] = ADoInsert(tid0, true) ∧ lsf1(tid0).le = e ∧ pcf1(tid0) = invInsert ⊦ ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

Used formulas: e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set

Proof step 44 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate.set ⊦ ∃ n, tid0. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid0, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert

Rule argument

Additional information

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

Proof step 45 from proof frag-in (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 46:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, e ∈ gstate0.set, ¬ e ∈ gstate.set ⊦ ¬ # al0 < 0 ∧ (a ' + al0)[0] = ADoInsert(tid, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[0 ] .lsf (tid) .le = e ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[0 ] .pcf (tid) = invInsert

Rule argument

Additional information

Used terms: 0, tid

Proof step 46 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ e ∈ gstate.set ⊦ a = ADoInsert(tid, true) ∧ lsf(tid).le = e ∧ pcf(tid) = invInsert

Rule argument

Additional information

Used simplifier rules: ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[0] = a; (s) ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ ¬ n < 0; (s)

Proof step 47 from proof frag-in (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 48:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = invInsert, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, e ∈ gstate0.set, ¬ e ∈ gstate.set ⊦ a = ADoInsert(tid, true) ∧ lsf(tid).le = e ∧ pcf(tid) = invInsert

• Proof step 53:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = invMember, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, e ∈ gstate0.set, ¬ e ∈ gstate.set ⊦ a = ADoInsert(tid, true) ∧ lsf(tid).le = e ∧ pcf(tid) = invInsert

• Proof step 56:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = retInsert, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, e ∈ gstate0.set, ¬ e ∈ gstate.set ⊦ a = ADoInsert(tid, true) ∧ lsf(tid).le = e ∧ pcf(tid) = invInsert

• Proof step 59:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = retMember, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ 0, gstepf(gstate, lsf(tid), pcf(tid), a).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), e ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, e ∈ gstate0.set, ¬ e ∈ gstate.set ⊦ a = ADoInsert(tid, true) ∧ lsf(tid).le = e ∧ pcf(tid) = invInsert

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;; ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ⊦ 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 48 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = invInsert, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)).set ≠ 0, gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)).set ≠ ∅, gstate0.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1, al0), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)).set, ¬ e ∈ gstate.set ⊦ b ∧ lsf(tid).le = e

Rule argument

Additional information

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

Proof step 49 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

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

• Proof step 51:

  ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), lsf(tid).tid = tid, ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = invInsert, # gstate0.set ≠ 0, # (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set ≠ 0, (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set ≠ ∅, gstate0.set ≠ ∅, SetInv(gstate, lsf, pcf), SetInv ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1, al0), e ∈ (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set, e ∈ gstate0.set, ¬ e ∈ gstate.set ⊦ b ∧ lsf(tid).le = e

Rule argument

Additional information

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

Proof step 50 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 51 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := (b ⊃ lsf(tid).lb:= true;lsf(tid).lb:= false)), pcf(tid := retInsert)) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = invInsert, # gstate0.set ≠ 0, # (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set ≠ 0, (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set ≠ ∅, gstate0.set ≠ ∅, SetInv ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate ((b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate), lsf(tid := lstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b))), pcf(tid := pcstepf(gstate, lsf(tid), invInsert, ADoInsert(tid, b)))) ' + sl1, al0), e ∈ gstate0.set, e ∈ (b ⊃ gstate.set:= (gstate.set ++ lsf(tid).le);gstate).set, ¬ e ∈ gstate.set ⊦ b ∧ lsf(tid).le = e

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ ls.tid = tid → pcstepf(gs, ls, invInsert, ADoInsert(tid, b)) = retInsert; (s) ⊦ ls.tid = tid → lstepf(gs, ls, invInsert, ADoInsert(tid, b)) = (b ⊃ ls.lb:= true;ls.lb:= false); (s)

Proof step 52 from proof frag-in (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ ≠ s ++ a; (s) ⊦ (gs.set:= set).set = set; (s) ⊦ ¬ a ∈ s → (a ∈ s ++ b ↔ a = b); (s)

Proof step 53 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = invMember, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), invMember, ADoMember(tid)).set ≠ 0, gstepf(gstate, lsf(tid), invMember, ADoMember(tid)).set ≠ ∅, gstate0.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), invMember, ADoMember(tid)), lsf(tid := lstepf(gstate, lsf(tid), invMember, ADoMember(tid))), pcf(tid := pcstepf(gstate, lsf(tid), invMember, ADoMember(tid)))) ' + sl1, al0), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), invMember, ADoMember(tid)).set, ¬ e ∈ gstate.set ⊦

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ invInsert ≠ invMember; (s) ⊦ pre(gs, ls, invMember, a) ↔ a = ADoMember(ls.tid); (s)

Proof step 54 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ 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: gstate, lsf(tid), tid

Proof step 55 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = retInsert, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)).set ≠ 0, gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)).set ≠ ∅, gstate0.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)))) ' + sl1, al0), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), retInsert, ARetInsert(tid, lsf(tid).lb)).set, ¬ e ∈ gstate.set ⊦

Rule argument

Additional information

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

Proof step 57 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ 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: gstate, lsf(tid), tid, lsf(tid).lb

Proof step 58 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf(tid) = retMember, # gstate0.set ≠ 0, # gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)).set ≠ 0, gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)).set ≠ ∅, gstate0.set ≠ ∅, SetInv (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)), lsf(tid := lstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb))), pcf(tid := pcstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)))) ' + sl1, al0), e ∈ gstate0.set, e ∈ gstepf(gstate, lsf(tid), retMember, ARetMember(tid, lsf(tid).lb)).set, ¬ e ∈ gstate.set ⊦

Rule argument

Additional information

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

Proof step 60 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 61:

  ⊦ 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: gstate, lsf(tid), tid, lsf(tid).lb

Proof step 61 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 62 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), al0[n] = ADoInsert(tid0, true), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf1(tid0) = invInsert, # gstate0.set ≠ 0, gstate0.set ≠ ∅, al0 ≠ [], n < # al0, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n, tid1. ¬ # al0 < n ∧ (a ' + al0)[n] = ADoInsert(tid1, true) ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 63 from proof frag-in (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ mkstate(gstate, lsf, pcf).lsf = lsf; (s) ⊦ mkstate(gstate, lsf, pcf).pcf = pcf; (s) Used terms: n + 1, tid0

Proof step 64 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .pcf (tid0) = invInsert, (a ' + al0)[n] = ADoInsert(tid0, true), SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), n ≤ # al0, ¬ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le ∈ gstate0.set, ¬ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le ∈ gstate.set, ¬ ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] .lsf (tid0) .le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 65 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 66:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), (a ' + al0)[n] = ADoInsert(tid0, true), ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), pcf1(tid0) = invInsert, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), n ≤ # al0, ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

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(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ], gstate1, lsf1, pcf1

Proof step 66 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 68:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), (a ' + al0)[n] = ADoInsert(tid0, true), pcf1(tid0) = invInsert, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), n ≤ # al0, ¬ n < # a ', ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

• Proof step 72:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), a '[n] = ADoInsert(tid0, true), pcf1(tid0) = invInsert, n < # a ', SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), n ≤ # al0, ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used terms: n, a ', al0

Proof step 67 from proof frag-in (previous step) (back to tree)

A spec-lemma

Proof step 68 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), al0[n - 1] = ADoInsert(tid0, true), pcf1(tid0) = invInsert, n ≠ 0, SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), SetInv(gstate, lsf, pcf), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), n ≤ # al0, ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 69 from proof frag-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 70:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), al0[m] = ADoInsert(tid0, true), ( mkstate(gstate, lsf, pcf) ' + mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n ] = mkstate(gstate1, lsf1, pcf1), n = m + 1, pcf1(tid0) = invInsert, n ≠ 0, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), n ≤ # al0, ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 70 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[m ] = mkstate(gstate1, lsf1, pcf1), al0[m] = ADoInsert(tid0, true), pcf1(tid0) = invInsert, al0 ≠ [], m < # al0, SetInv(gstate, lsf, pcf), SetInv(gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1, al0), pre(gstate, lsf(tid), pcf(tid), a), ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf(tid), pcf(tid), a).set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstate0.set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf(tid), pcf(tid), a), lsf(tid := lstepf(gstate, lsf(tid), pcf(tid), a)), pcf(tid := pcstepf(gstate, lsf(tid), pcf(tid), a))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[n + 1] = x[n]; (s)

Proof step 71 from proof frag-in (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

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

Proof step 72 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf1(tid0) = invInsert, SetInv (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))), SetInv(gstate, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1, al0), pre(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) ⊦ a '[0] = a; (s) ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[0] = a; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s)

Proof step 73 from proof frag-in (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 74:

  ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf1(tid0) = invInsert, pcf1(tid) = invInsert, SetInv(gstate, lsf1, pcf1), SetInv (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1, al0), pre(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), ¬ lsf1(tid0).le ∈ gstate0.set, ¬ lsf1(tid0).le ∈ gstate.set, ¬ lsf1(tid0).le ∈ gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid0).le ∧ ( mkstate (gstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)), lsf1(tid := lstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), pcf1(tid), ADoInsert(tid0, true)))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

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

Proof step 74 from proof frag-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  ( mkstate (gstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)), lsf1(tid := lstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)))) ' + sl1 ).last = mkstate(gstate0, lsf0, pcf0), pcf1(tid) = invInsert, SetInv (gstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)), lsf1(tid := lstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)))), SetInv(gstate, lsf1, pcf1), frag*(IOAut(setInit, setStep, setExt)) ( mkstate (gstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)), lsf1(tid := lstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)))) ' + sl1, al0), ¬ lsf1(tid).le ∈ gstate0.set, ¬ lsf1(tid).le ∈ gstate.set, ¬ lsf1(tid).le ∈ gstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)).set ⊦ ∃ n0, tid1. n0 < # al0 ∧ al0[n0] = ADoInsert(tid1, true) ∧ ( mkstate (gstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)), lsf1(tid := lstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)))) ' + sl1 )[n0 ] .lsf (tid1) .le = lsf1(tid).le ∧ ( mkstate (gstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)), lsf1(tid := lstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true))), pcf1(tid := pcstepf(gstate, lsf1(tid), invInsert, ADoInsert(tid, true)))) ' + sl1 )[n0 ] .pcf (tid1) = invInsert

Rule argument

Additional information

Used simplifier rules: inv-tid: ⊦ SetInv(gstate, lsf, pcf) → lsf(tid).tid = tid; ⊦ ADoInsert(tid, b) = ADoInsert(tid0, b0) ↔ tid = tid0 ∧ (b ↔ b0); (ws) ⊦ pre(gs, ls, invInsert, a) ↔ (∃ b. a = ADoInsert(ls.tid, b)); (s)

Proof step 75 from proof frag-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

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

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; ⊦ (gs.set:= set).set = set; (s) ⊦ ¬ a ∈ s → (a ∈ s ++ b ↔ a = b); (s) Used terms: gstate, lsf1(tid), tid, true

Proof step 76 from proof frag-in (previous step) (back to tree)

A spec-lemma