Proof step 1 from proof one-pending-del-persist-FO-no-pending (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FOFollowsW(t, p(l)), isPersistFO(n, p(l)), onePendingW(t, l, p), FO(t) ∈ p(l), ¬ noPendingW(t, p), ¬ FO(t) ∈ p(l) -p n ⊦

Rule argument

Additional information

Proof step 2 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  FO(t) = p(l)[n], p(l) ≠ [], n < # p(l), FOFollowsW(t, p(l)), onePendingW(t, l, p), FO(t) ∈ p(l), ¬ noPendingW(t, p), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: isPersistFO: ⊦ isPersistFO(n, fowl) ↔ n < # fowl ∧ fowl[n].FO? ∧ (∀ m. m < n → fowl[m].tid ≠ fowl[n].tid ∧ fowl[m].FO?); ⊦ FO(tid).tid = tid; (s) ⊦ FO(tid).FO?; (s) ⊦ # x = 0 ↔ x = []; (s) delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ noPendingW(t, p) ↔ (∀ l. p(l) |W | t = [])

• Proof step 5:

  FO(t) = p(l)[n], p(l) ≠ [], n < # p(l), FOFollowsW(t, p(l)), onePendingW(t, l, p), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∃ l. p(l) |W | t ≠ [] ⊦

Rule argument

Additional information

Used terms: t, p

Proof step 4 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  FO(t) = p(l)[n], p(l) ≠ [], p(l0) |W | t ≠ [], n < # p(l), FOFollowsW(t, p(l)), onePendingW(t, l, p), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Proof step 6 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = [])

• Proof step 8:

  FO(t) = p(l)[n], p(l) ≠ [], p(l0) |W | t ≠ [], n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∀ l0. l0 ≠ l → p(l0) |W | t = [] ⊦

Rule argument

Additional information

Used terms: t, l, p

Proof step 7 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  FO(t) = p(l)[n], p(l) ≠ [], p(l0) |W | t ≠ [], n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, l0 ≠ l → p(l0) |W | t = [], ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used terms: l0

Proof step 9 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  FO(t) = p(l)[n], p(l) ≠ [], p(l) |W | t ≠ [], n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Proof step 10 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 12:

  FO(t) = p(l)[n], p(l) ≠ [], n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∃ a. a ∈ p(l) |W | t ⊦

Rule argument

Additional information

Used terms: p(l) |W | t

Proof step 11 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  FO(fow.tid) = p(l)[n], p(l) ≠ [], fow.W?, n < # p(l), FOFollowsW(fow.tid, p(l)), fow ∈ p(l), FO(fow.tid) ∈ p(l), ¬ FO(fow.tid) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ fow.tid ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del ⊦ fow ∈ fowl |W ↔ fow ∈ fowl ∧ fow.W?; (s) ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 13 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  FO(t) = p(l)[n], fow = W(v, t), p(l) ≠ [], fow.W?, n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), fow ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow.W? → (val = fow.val ∧ tid = fow.tid ↔ fow = W(val, tid)); (elim) Used terms: fow, v, t

Proof step 14 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  FO(t) = p(l)[n], p(l) ≠ [], n < # p(l), FOFollowsW(t, p(l)), W(v, t) ∈ p(l), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del ⊦ W(v, tid).W?; (s)

Proof step 15 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 17:

  FO(t) = p(l)[n], p(l) ≠ [], n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∃ n. n < # p(l) ∧ p(l)[n] = W(v, t) ⊦

Rule argument

Additional information

Used terms: W(v, t), p(l)

Proof step 16 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l) ≠ [], n0 < # p(l), n < # p(l), FOFollowsW(t, p(l)), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Proof step 18 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ FOFollowsW(t, fowl) ↔ (∀ n. n < # fowl ∧ fowl[n].W? ∧ fowl[n].tid = t → (∃ n0. n < n0 ∧ n0 < # fowl ∧ fowl[n0] = FO(t)))

• Proof step 20:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l) ≠ [], n < # p(l), n0 < # p(l), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∀ n. n < # p(l) ∧ p(l)[n].W? ∧ p(l)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l) ∧ p(l)[n0] = FO(t)) ⊦

Rule argument

Additional information

Used terms: t, p(l)

Proof step 19 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l) ≠ [], n0 < # p(l), n < # p(l), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∀ n1. n1 < # p(l) ∧ p(l)[n1].W? ∧ p(l)[n1].tid = t → (∃ n0. n1 < n0 ∧ n0 < # p(l) ∧ p(l)[n0] = FO(p(l)[n1].tid)) ⊦

Rule argument

Additional information

Proof step 21 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l) ≠ [], n < # p(l), n0 < # p(l), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, n0 < # p(l) ∧ p(l)[n0].W? ∧ p(l)[n0].tid = t → (∃ n. n0 < n ∧ n < # p(l) ∧ p(l)[n] = FO(p(l)[n0].tid)), ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used terms: n0

Proof step 22 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  FO(t) = p(l)[n], p(l)[n1] = FO(t), p(l)[n0] = W(v, t), p(l) ≠ [], n1 < # p(l), n0 < n1, n0 < # p(l), n < # p(l), n0 + 1 < # p(l), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ W(v, tid).tid = tid; (s) ⊦ W(v, tid).W?; (s)

Proof step 23 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l)[n1] = FO(t), p(l) ≠ [], n0 + 1 < # p(l), n < # p(l), n0 < # p(l), n0 < n1, n1 < # p(l), n < n0, FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

• Proof step 31:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l)[n1] = FO(t), p(l) ≠ [], n0 + 1 < # p(l), n < # p(l), n0 < # p(l), n0 < n1, n1 < # p(l), FO(t) ∈ p(l), ¬ n < n0, ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used formulas: n < n0

Proof step 24 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  FO(t) = p(l)[n], p(l)[n1] = FO(t), p(l)[n0] = W(v, t), p(l) ≠ [], n + 1 < # p(l), n + 1 < n1, n < n0, n1 < # p(l), n0 < n1, n0 < # p(l), n0 + 1 < # p(l), n < n1, n < # p(l), 2 + n < # p(l), FO(t) ∈ p(l), ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 25 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 27:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l)[n1] = FO(t), p(l) ≠ [], 2 + n < # p(l), n < # p(l), n < n1, n0 + 1 < # p(l), n0 < # p(l), n0 < n1, n1 < # p(l), n < n0, n + 1 < n1, n + 1 < # p(l), FO(t) ∈ p(l), ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∀ n0. ¬(n0 < #(p(l) -p n) ∧ (p(l) -p n)[n0] = FO(t)) ⊦

Rule argument

Additional information

Used terms: FO(t), p(l) -p n

Proof step 26 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  FO(t) = p(l)[n], p(l)[n1] = FO(t), p(l)[n0] = W(v, t), p(l) ≠ [], n + 1 < # p(l), n + 1 < n1, n < n0, n1 < # p(l), n0 < n1, n0 < # p(l), n0 + 1 < # p(l), n < n1, n < # p(l), 2 + n < # p(l), FO(t) ∈ p(l), ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∀ n2. ¬ n2 + 1 < # p(l) ∨ (n2 < n ⊃ p(l)[n2];p(l)[n2 + 1]) ≠ FO(t) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n + 1 < # x ∧ m < # x → (x -p m)[n] = (n < m ⊃ x[n];x[n + 1]); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n < # x → #(x -p n) = # x - 1; (s)

Proof step 28 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

  FO(t) = p(l)[n], p(l)[n0] = W(v, t), p(l)[n1] = FO(t), p(l) ≠ [], 2 + n < # p(l), n < # p(l), n < n1, n0 + 1 < # p(l), n0 < # p(l), n0 < n1, n1 < # p(l), n < n0, n + 1 < n1, n + 1 < # p(l), FO(t) ∈ p(l), ∀ n2. ¬ n2 + 1 < # p(l) ∨ (n2 < n ⊃ p(l)[n2];p(l)[n2 + 1]) ≠ FO(t), ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ¬ (n1 - 1) + 1 < # p(l) ∨ (n1 - 1 < n ⊃ p(l)[n1 - 1];p(l)[(n1 - 1) + 1]) ≠ FO(t) ⊦

Rule argument

Additional information

Used terms: n1 - 1

Proof step 29 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  FO(t) = p(l)[n], p(l)[n1] = FO(t), p(l)[n0] = W(v, t), p(l) ≠ [], n + 1 < # p(l), n + 1 < n1, n < n0, n1 < # p(l), n0 < n1, n0 < # p(l), n0 + 1 < # p(l), n < n1, n < # p(l), 2 + n < # p(l), FO(t) ∈ p(l), ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO?, ∀ n2. ¬ n2 + 1 < # p(l) ∨ (n2 < n ⊃ p(l)[n2];p(l)[n2 + 1]) ≠ FO(t), ¬ (n1 - 1) + 1 < # p(l) ∨ p(l)[(n1 - 1) + 1] ≠ FO(t) ⊦

Rule argument

Additional information

Used simplifier rules: 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) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 30 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ x ≠ [] → x[0] = x.head; (s) n0 < n ⊦ ¬ m + (* n) < (* n0); (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n1, m0

Proof step 31 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  FO(t) = p(l)[n], p(l)[n1] = FO(t), p(l)[n0] = W(v, t), p(l) ≠ [], n1 < # p(l), n0 < n1, n0 < # p(l), n < # p(l), n0 + 1 < # p(l), FO(t) ∈ p(l), n0 ≤ n, ¬ FO(t) ∈ p(l) -p n, ∀ m. m < n → p(l)[m].tid ≠ t ∧ p(l)[m].FO? ⊦

Rule argument

Additional information

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

Proof step 32 from proof one-pending-del-persist-FO-no-pending (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).tid = tid; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m ≤ m; (s) lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic delpos-get-fw: ⊦ ¬ a ∈ x -p n ∧ a ∈ x → a = x[n]; (forward) from specification list-del ⊦ FO(tid) ≠ W(v, tid0); (s) Used terms: n0