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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  firstPersistW(p(l)) < # p(l), ¬ rely(t, p, p(l := p(l) -p firstPersistW(p(l)))) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: firstPersistW: ⊦ firstPersistW(fowl) = fowl.indexWhere(.W?); 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-W-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).indexWhere(.W?) < # p(l) ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) -p p(l0).indexWhere(.W?);p(l0)) = fowl1 + fowl2 ∧ fowl2 | t = []

• Proof step 24:

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

Rule argument

Additional information

Used formulas: l = l0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0) ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p(l0) -p p(l0).indexWhere(.W?) = 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-W-weak (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0) ⊦ (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) -p p(l0).indexWhere(.W?) = fowl5 + fowl4) ∧ p(l0) -p p(l0).indexWhere(.W?) = (p(l0) -p p(l0).indexWhere(.W?)) + [] ∧ [] | t = []

Rule argument

Additional information

Used terms: p(l0) -p p(l0).indexWhere(.W?), []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0) ⊦ ∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) -p p(l0).indexWhere(.W?) = 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-W-weak (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 8:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0) ⊦ p(l0) = [] + p(l0).take(p(l0).indexWhere(.W?) + 1) + p(l0).drop(p(l0).indexWhere(.W?) + 1) ∧ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?) + 1))|FO ∧ p(l0) -p p(l0).indexWhere(.W?) = p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 1)

Rule argument

Additional information

Used terms: [], p(l0).take(p(l0).indexWhere(.W?) + 1), p(l0).drop(p(l0).indexWhere(.W?) + 1), p(l0).take(p(l0).indexWhere(.W?))

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0) ⊦ p(l0) = p(l0).take(p(l0).indexWhere(.W?) + 1) + p(l0).drop(p(l0).indexWhere(.W?) + 1) ∧ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?) + 1))|FO ∧ p(l0) -p p(l0).indexWhere(.W?) = p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 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-W-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).indexWhere(.W?) < # p(l0), p(l0).indexWhere(.W?) + 1 ≤ # p(l0) ⊦ p(l0) = p(l0) ∧ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?) + 1))|FO ∧ p(l0) -p p(l0).indexWhere(.W?) = p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 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), p(l0).indexWhere(.W?) + 1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0) ⊦ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?) + 1))|FO ∧ p(l0) -p p(l0).indexWhere(.W?) = p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 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-W-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).indexWhere(.W?) < # p(l0) ⊦ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?) + 1))|FO ∧ p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 1) = p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 1)

Rule argument

Additional information

Used terms: p(l0), p(l0).indexWhere(.W?)

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  p(l0).indexWhere(.W?) + 1 ≠ 0, p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0), p(l0).indexWhere(.W?) + 1 ≤ # p(l0) ⊦ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take((p(l0).indexWhere(.W?) + 1)-1) + p(l0)[(p(l0).indexWhere(.W?) + 1)-1])|FO ∧ p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 1) = p(l0).take(p(l0).indexWhere(.W?)) + p(l0).drop(p(l0).indexWhere(.W?) + 1)

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), p(l0).indexWhere(.W?) + 1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0), ¬ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?)))|FO + p(l0)[p(l0).indexWhere(.W?)] ' |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 17 from proof rely-persist-W-weak (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 18:

  p(l0)[p(l0).indexWhere(.W?)] = FO(t), p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0), ¬ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?)))|FO + p(l0)[p(l0).indexWhere(.W?)] ' |FO ⊦

• Proof step 21:

  p(l0)[p(l0).indexWhere(.W?)] = W(v, t), p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0), ¬ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?)))|FO + p(l0)[p(l0).indexWhere(.W?)] ' |FO ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  p(l0)[p(l0).indexWhere(.W?)] = FO(t), p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0), ¬ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?)))|FO + FO(t) ' ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(t) ' |FO = FO(t) '; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 20:

  ⊦ firstPersistW(fowl) < # fowl → fowl[firstPersistW(fowl)].W?

Rule argument

Additional information

Used simplifier rules: firstPersistW: ⊦ firstPersistW(fowl) = fowl.indexWhere(.W?); ⊦ ¬ FO(tid).W?; (s) Used terms: p(l0)

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

Lemma at-firstPersistW-is-W

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  p(l0)[p(l0).indexWhere(.W?)] = W(v, t), p(l0) ≠ [], p(l0).indexWhere(.W?) < # p(l0), ¬ p(l0).take(p(l0).indexWhere(.W?)) ⊆ (p(l0).take(p(l0).indexWhere(.W?)))|FO ⊦

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 23:

  ⊦ firstPersistW(fowl) < # fowl → (fowl.take(firstPersistW(fowl)))|FO = fowl.take(firstPersistW(fowl))

Rule argument

Additional information

Used simplifier rules: firstPersistW: ⊦ firstPersistW(fowl) = fowl.indexWhere(.W?); ⊦ x ⊆ x; (s) Used terms: p(l0)

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

Lemma take-firstPersistW-filter-FO

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  l ≠ l0, p(l) ≠ [], p(l).indexWhere(.W?) < # p(l) ⊦ ∃ 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 25 from proof rely-persist-W-weak (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 26:

  l ≠ l0, p(l) ≠ [], p(l).indexWhere(.W?) < # p(l) ⊦ (∃ 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 26 from proof rely-persist-W-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  l ≠ l0, p(l) ≠ [], p(l).indexWhere(.W?) < # p(l) ⊦ ∃ 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 27 from proof rely-persist-W-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), []