Proof step 1 from proof rely-persist-FO-weak (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  isPersistFO(n, p(l)), ¬ rely(t, p, p(l := p(l) -p n)) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  p(l) ≠ [], p(l)[n].FO?, n < # p(l), ∀ m. m < n → p(l)[m].tid ≠ p(l)[n].tid ∧ p(l)[m].FO? ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) -p n;p(l0)) = fowl1 + fowl2 ∧ fowl2 | t = []

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?); allrely-def: ⊦ rely(t, p, p0) ↔ (∀ l. rely(t, p(l), p0(l))); rely-def: ⊦ rely(t, fowl, fowl0) ↔ (∃ fowl1, fowl2. fowl ⊒W fowl1 ∧ fowl0 = fowl1 + fowl2 ∧ fowl2 | t = []); weak-write-postfix: ⊦ fowl0 ⊒W fowl1 ↔ (∃ fowl2, fowl3, fowl4, fowl5. fowl0 = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4); ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  l = l0, p(l) ≠ [], p(l)[n].FO?, n < # p(l), ∀ m. m < n → p(l)[m].tid ≠ p(l)[n].tid ∧ p(l)[m].FO? ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) -p n;p(l0)) = fowl1 + fowl2 ∧ fowl2 | t = []

• Proof step 33:

  l ≠ l0, p(l) ≠ [], p(l)[n].FO?, n < # p(l), ∀ m. m < n → p(l)[m].tid ≠ p(l)[n].tid ∧ p(l)[m].FO? ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) -p n;p(l0)) = fowl1 + fowl2 ∧ fowl2 | t = []

Rule argument

Additional information

Used formulas: l = l0

Proof step 4 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p(l0) -p n = fowl1 + fowl2 ∧ fowl2 | t = []

Rule argument

Additional information

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

Proof step 5 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) -p n = fowl5 + fowl4) ∧ p(l0) -p n = (p(l0) -p n) + [] ∧ [] | t = []

Rule argument

Additional information

Used terms: p(l0) -p n, []

Proof step 6 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ ∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) -p n = fowl5 + fowl4

Rule argument

Additional information

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

Proof step 7 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 8:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ p(l0) = [] + p(l0).take(n + 1) + p(l0).drop(n + 1) ∧ p(l0).take(n) ⊆ (p(l0).take(n + 1))|FO ∧ p(l0) -p n = p(l0).take(n) + p(l0).drop(n + 1)

Rule argument

Additional information

Used terms: [], p(l0).take(n + 1), p(l0).drop(n + 1), p(l0).take(n)

Proof step 8 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ p(l0) = p(l0).take(n + 1) + p(l0).drop(n + 1) ∧ p(l0).take(n) ⊆ (p(l0).take(n + 1))|FO ∧ p(l0) -p n = p(l0).take(n) + p(l0).drop(n + 1)

Rule argument

Additional information

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

Proof step 9 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ n ≤ # x → x.take(n) + x.drop(n) = x

• Proof step 11:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), n + 1 ≤ # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ p(l0) = p(l0) ∧ p(l0).take(n) ⊆ (p(l0).take(n + 1))|FO ∧ p(l0) -p n = p(l0).take(n) + p(l0).drop(n + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: p(l0), n + 1

Proof step 10 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ p(l0).take(n) ⊆ (p(l0).take(n + 1))|FO ∧ p(l0) -p n = p(l0).take(n) + p(l0).drop(n + 1)

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 ≤ n ↔ m < n; (s)

Proof step 12 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ n < # x → x -p n = x.take(n) + x.drop(n + 1)

• Proof step 14:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦ p(l0).take(n) ⊆ (p(l0).take(n + 1))|FO ∧ p(l0).take(n) + p(l0).drop(n + 1) = p(l0).take(n) + p(l0).drop(n + 1)

Rule argument

Additional information

Used terms: p(l0), n

Proof step 13 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ (p(l0).take(n + 1))|FO, ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Proof step 15 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ n ≠ 0 ∧ n ≤ # x → x.take(n) = x.take(n -1) + x[n -1]

• Proof step 17:

  n + 1 ≠ 0, p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), n + 1 ≤ # p(l0), ¬ p(l0).take(n) ⊆ (p(l0).take((n + 1)-1) + p(l0)[(n + 1)-1])|FO, ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: p(l0), n + 1

Proof step 16 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ (p(l0).take(n))|FO + p(l0)[n] ' |FO, ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (fowl + fowl0)|FO = fowl |FO + fowl0 |FO; (s) ⊦ x + a = x + a '; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (m + 1)-1 = m; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 18 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ fowl |FO = fowl.filter(λ fow. fow.FO?)

• Proof step 20:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(λ fow. fow.FO?) + p(l0)[n] ' |FO, ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used terms: p(l0).take(n)

Proof step 19 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ' |FO, ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Proof step 21 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ fowl |FO = fowl.filter(λ fow. fow.FO?)

• Proof step 23:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] '.filter(λ fow. fow.FO?), ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used terms: p(l0)[n] '

Proof step 22 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ', ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s)

Proof step 24 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ x.forall(p) → x.filter(p) = x

• Proof step 26:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n).forall(.FO?), ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ', ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ⊆ x + y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: p(l0).take(n), .FO?

Proof step 25 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ x.forall(p) ↔ (∀ n. n < # x → p(x[n]))

• Proof step 28:

  p(l0) ≠ [], p(l0)[n].FO?, n < # p(l0), ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ', ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO?, ∃ n0. ¬(n0 < # p(l0).take(n) → p(l0).take(n)[n0].FO?) ⊦

Rule argument

Additional information

Used terms: p(l0).take(n), .FO?

Proof step 27 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  p(l0) ≠ [], p(l0)[n].FO?, n0 < # p(l0), n0 < n, n < # p(l0), n0 + 1 < # p(l0), ¬ p(l0).take(n)[n0].FO?, ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ', ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[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 ⊦ n < # x → # x.take(n) = n; (s)

Proof step 29 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ n < m ∧ m ≤ # x → x.take(m)[n] = x[n]

• Proof step 31:

  p(l0) ≠ [], p(l0)[n].FO?, n0 + 1 < # p(l0), n < # p(l0), n0 < # p(l0), n0 < n, n ≤ # p(l0), ¬ p(l0)[n0].FO?, ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ', ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) Used terms: p(l0), n, n0

Proof step 30 from proof rely-persist-FO-weak (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  p(l0) ≠ [], p(l0)[n].FO?, n0 < n, n0 < # p(l0), n < # p(l0), n0 + 1 < # p(l0), ¬ p(l0)[n0].FO?, ¬ p(l0).take(n) ⊆ p(l0).take(n).filter(.FO?) + p(l0)[n] ', ∀ m. m < n → p(l0)[m].tid ≠ p(l0)[n].tid ∧ p(l0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 32 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 33 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  l ≠ l0, p(l) ≠ [], p(l)[n].FO?, n < # p(l), ∀ m. m < n → p(l)[m].tid ≠ p(l)[n].tid ∧ p(l)[m].FO? ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p(l0) = fowl1 + fowl2 ∧ fowl2 | t = []

Rule argument

Additional information

Proof step 34 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 35:

  l ≠ l0, p(l) ≠ [], p(l)[n].FO?, n < # p(l), ∀ m. m < n → p(l)[m].tid ≠ p(l)[n].tid ∧ p(l)[m].FO? ⊦ (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) = fowl5 + fowl4) ∧ p(l0) = p(l0) + [] ∧ [] | t = []

Rule argument

Additional information

Used terms: p(l0), []

Proof step 35 from proof rely-persist-FO-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  l ≠ l0, p(l) ≠ [], p(l)[n].FO?, n < # p(l), ∀ m. m < n → p(l)[m].tid ≠ p(l)[n].tid ∧ p(l)[m].FO? ⊦ ∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) = fowl5 + fowl4

Rule argument

Additional information

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

Proof step 36 from proof rely-persist-FO-weak (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] |FO = []; (s) ⊦ [] ⊆ x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: [], [], p(l0), []