Proof step 1 from proof theorem-allinserts-finished-false-implies-notin (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  exec*(IOAut(setInit, setStep, setExt))(sl, al), e ∈ sl.last.gstate.set, ∀ tid, al1, al2. al = al1 + (AInvInsert(tid, e) + al2) → (∃ al3, al4. al2 = al3 + (ARetInsert(tid, false) + al4) ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

Rule argument

Additional information

Proof step 2 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # sl.last.gstate.set ≠ 0, sl.last.gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(sl[0]), e ∈ sl.last.gstate.set, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

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 a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

Proof step 3 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(sl[0]), e ∈ gstate.set, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  exec*(IOAut(setInit, setStep, setExt))(sl, al), n < # sl, ∀ tid, al1, al2. al = al1 + (AInvInsert(tid, e) + al2) → (∃ al3, al4. al2 = al3 + (ARetInsert(tid, false) + al4) ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦ ¬ e ∈ sl[n].gstate.set ∧ (sl[n].pcf(tid) = retInsert ∧ sl[n].lsf(tid).le = e → ¬ sl[n].lsf(tid).lb)

• Proof step 6:

  sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(sl[0]), e ∈ gstate.set, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦ exec*(IOAut(setInit, setStep, setExt))(sl, al) ∧ # sl - 1 < # sl ∧ (∀ tid, al1, al2. al = al1 + (AInvInsert(tid, e) + al2) → (∃ al3, al4. al2 = al3 + (ARetInsert(tid, false) + al4) ∧ ¬ tid ∈ setExt !(al3).map(.tid)))

• Proof step 10:

  sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(sl[0]), e ∈ gstate.set, ¬ e ∈ sl[# sl - 1].gstate.set, sl[# sl - 1].pcf(tid) = retInsert ∧ sl[# sl - 1].lsf(tid).le = e → ¬ sl[# sl - 1].lsf(tid).lb, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

Rule argument

Additional information

Used terms: sl, al, tid, e, # sl - 1

Proof step 5 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Lemma allinserts-finished-false-implies-notin-ind

Proof step 6 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al1 + AInvInsert(tid, e) ' + al2), setInit(sl[0]), e ∈ gstate.set, ∀ tid0, al0, al3. al1 + AInvInsert(tid, e) ' + al2 = al0 + AInvInsert(tid0, e) ' + al3 → (∃ al, al4. al3 = al + ARetInsert(tid0, false) ' + al4 ∧ ¬ tid0 ∈ setExt !(al).map(.tid)) ⊦ ∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)

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 a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ 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 ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

Proof step 7 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al1 + AInvInsert(tid, e) ' + al2), setInit(sl[0]), e ∈ gstate.set, al1 + AInvInsert(tid, e) ' + al2 = al1 + AInvInsert(tid, e) ' + al2 → (∃ al, al4. al2 = al + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al).map(.tid)) ⊦ ∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)

Rule argument

Additional information

Used terms: tid, al1, al2

Proof step 8 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al1 + AInvInsert(tid, e) ' + al + ARetInsert(tid, false) ' + al4), setInit(sl[0]), e ∈ gstate.set, ¬ tid ∈ setExt !(al).map(.tid) ⊦ ∃ al3, al0. al + ARetInsert(tid, false) ' + al4 = al3 + ARetInsert(tid, false) ' + al0 ∧ ¬ tid ∈ setExt !(al3).map(.tid)

Rule argument

Additional information

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

Proof step 9 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

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

Proof step 10 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  # sl = m + 1, sl.last = mkstate(gstate, lsf, pcf), # sl ≠ 0, # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(sl[0]), e ∈ gstate.set, ¬ e ∈ sl[m].gstate.set, sl[m].pcf(tid) = retInsert ∧ sl[m].lsf(tid).le = e → ¬ sl[m].lsf(tid).lb, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: # sl, m

Proof step 11 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # sl = m + 1, sl.last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, sl ≠ [], frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(sl.head), e ∈ gstate.set, ¬ e ∈ sl[m].gstate.set, sl[m].pcf(tid) = retInsert ∧ sl[m].lsf(tid).le = e → ¬ sl[m].lsf(tid).lb, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

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 ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ # x = 0 ↔ x = []; (s)

Proof step 12 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  # sl = m + 1, sl.last = mkstate(gstate, lsf, pcf), sl = s + sl0, # gstate.set ≠ 0, gstate.set ≠ ∅, sl ≠ [], frag*(IOAut(setInit, setStep, setExt))(sl, al), setInit(s), e ∈ gstate.set, ¬ e ∈ sl[m].gstate.set, sl[m].pcf(tid) = retInsert ∧ sl[m].lsf(tid).le = e → ¬ sl[m].lsf(tid).lb, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

Rule argument

Additional information

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

Proof step 13 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (s ' + sl0).last = mkstate(gstate, lsf, pcf), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(s ' + sl0, al), setInit(s), e ∈ gstate.set, ¬ e ∈ (s ' + sl0)[# sl0].gstate.set, (s ' + sl0)[# sl0].pcf(tid) = retInsert ∧ (s ' + sl0)[# sl0].lsf(tid).le = e → ¬ (s ' + sl0)[# sl0].lsf(tid).lb, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

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) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 14 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  (s ' + sl0).last = mkstate(gstate, lsf, pcf), (s ' + sl0)[# sl0] = mkstate(gstate0, lsf0, pcf0), # gstate.set ≠ 0, gstate.set ≠ ∅, frag*(IOAut(setInit, setStep, setExt))(s ' + sl0, al), setInit(s), e ∈ gstate.set, ¬ e ∈ gstate0.set, pcf0(tid) = retInsert ∧ lsf0(tid).le = e → ¬ lsf0(tid).lb, ∀ tid, al1, al2. al = al1 + AInvInsert(tid, e) ' + al2 → (∃ al3, al4. al2 = al3 + ARetInsert(tid, false) ' + al4 ∧ ¬ tid ∈ setExt !(al3).map(.tid)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gstate = s.gstate ∧ lsf = s.lsf) ∧ pcf = s.pcf ↔ s = mkstate(gstate, lsf, pcf); (elim) Used terms: (s ' + sl0)[# sl0], gstate0, lsf0, pcf0

Proof step 15 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ n = # x - 1 ∧ 0 < # x → x[n] = x.last

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ mkstate(gstate, lsf, pcf) = mkstate(gstate0, lsf0, pcf0) ↔ gstate = gstate0 ∧ lsf = lsf0 ∧ pcf = pcf0; (ws) Used terms: s ' + sl0, # sl0

Proof step 16 from proof theorem-allinserts-finished-false-implies-notin (previous step) (back to tree)

A spec-lemma