Proof step 1 from proof sublist-move (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x.sublist(n0, m0).sublist(n, m) ≠ x.sublist(n0 + n, m), n + m ≤ m0, n0 + m0 ≤ # x ⊦

Rule argument

Additional information

Proof step 2 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x.drop(n0).take(m0).drop(n).take(m) ≠ x.drop(n0 + n).take(m), n0 + m0 ≤ # x, n + m ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: sublist-def: ⊦ x.sublist(m, n) = x.drop(m).take(n);

Proof step 3 from proof sublist-move (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  (a + x0).drop(n0).take(m0).drop(n).take(m) ≠ (a + x0).drop(n0 + n).take(m), n + m ≤ m0, n0 + m0 ≤ #(a + x0), ∀ n0, m0, n, m. ¬(x0.drop(n0).take(m0).drop(n).take(m) ≠ x0.drop(n0 + n).take(m) ∧ n0 + m0 ≤ # x0 ∧ n + m ≤ m0) ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ x.drop(0) = x; firstN-zero: ⊦ x.take(0) = []; List('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 4 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (a ' + x0).drop(n0).take(m0).drop(n).take(m) ≠ (a ' + x0).drop(n0 + n).take(m), n + m ≤ m0, n0 + m0 ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a + x = a ' + x; (s)

Proof step 5 from proof sublist-move (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 0 < n → x.drop(n) = x.tail.drop(n -1)

• Proof step 7:

  (a ' + x0).drop(n0).take(m0).drop(n).take(m) ≠ (a ' + x0).drop(n0 + n).take(m), n0 + m0 ≤ # x0 + 1, n + m ≤ m0, ¬ 0 < n0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

• Proof step 25:

  (a ' + x0).tail.drop(n0 -1).take(m0).drop(n).take(m) ≠ (a ' + x0).drop(n0 + n).take(m), 0 < n0, n0 + m0 ≤ # x0 + 1, n + m ≤ m0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used terms: a ' + x0, n0

Proof step 6 from proof sublist-move (previous step) (back to tree)

Lemma rest-rec

Proof step 7 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (a ' + x0).take(m0).drop(n).take(m) ≠ (a ' + x0).drop(n).take(m), n + m ≤ m0, m0 ≤ # x0 + 1, n + m ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ x.drop(0) = x; let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 8 from proof sublist-move (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  n ≠ 0 ⊦ x.take((* n)) = x.head ' + x.tail.take(n -1)

• Proof step 10:

  ((a ' + x0).head ' + (a ' + x0).tail.take(m0 -1)).drop(n).take(m) ≠ (a ' + x0).drop(n).take(m), m0 ≠ 0, n + m ≤ # x0 + 1, m0 ≤ # x0 + 1, n + m ≤ m0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ x.drop(0) = x; firstN-zero: ⊦ x.take(0) = []; ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 ≤ m; (s) Used terms: a ' + x0, m0

Proof step 9 from proof sublist-move (previous step) (back to tree)

Lemma first-num

Proof step 10 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (a ' + x0.take(m0 - 1)).drop(n).take(m) ≠ (a ' + x0).drop(n).take(m), m0 ≠ 0, n + m ≤ m0, m0 ≤ # x0 + 1, n + m ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s) ⊦ (a ' + x).head = a; (s)

Proof step 11 from proof sublist-move (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  m0 = m3 + 1, (a ' + x0.take(m3)).drop(n).take(m) ≠ (a ' + x0).drop(n).take(m), m0 ≠ 0, n + m ≤ # x0 + 1, m0 ≤ # x0 + 1, n + m ≤ m0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

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

Proof step 12 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (a ' + x0.take(m3)).drop(n).take(m) ≠ (a ' + x0).drop(n).take(m), n + m ≤ # x0 + 1, n + m ≤ m3 + 1, m3 ≤ # x0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

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 ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 13 from proof sublist-move (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ 0 < n → x.drop(n) = x.tail.drop(n -1)

• Proof step 15:

  (a ' + x0.take(m3)).drop(n).take(m) ≠ (a ' + x0).drop(n).take(m), m3 ≤ # x0, n + m ≤ m3 + 1, n + m ≤ # x0 + 1, ¬ 0 < n, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

• Proof step 20:

  (a ' + x0.take(m3)).tail.drop(n -1).take(m) ≠ (a ' + x0).drop(n).take(m), 0 < n, m3 ≤ # x0, n + m ≤ m3 + 1, n + m ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used terms: a ' + x0.take(m3), n

Proof step 14 from proof sublist-move (previous step) (back to tree)

Lemma rest-rec

Proof step 15 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (a ' + x0.take(m3)).take(m) ≠ (a ' + x0).take(m), m3 ≤ # x0, m ≤ m3 + 1, m ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ x.drop(0) = x; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 16 from proof sublist-move (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  n ≠ 0 ⊦ x.take((* n)) = x.head ' + x.tail.take(n -1)

• Proof step 18:

  (a ' + x0.take(m3)).head ' + (a ' + x0.take(m3)).tail.take(m -1) ≠ (a ' + x0).take(m), m ≠ 0, m ≤ # x0 + 1, m ≤ m3 + 1, m3 ≤ # x0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: firstN-zero: ⊦ x.take(0) = []; Used terms: a ' + x0.take(m3), m

Proof step 17 from proof sublist-move (previous step) (back to tree)

Lemma first-num

Proof step 18 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  a ' + x0.take(m3).take(m - 1) ≠ (a ' + x0).take(m), m ≠ 0, m3 ≤ # x0, m ≤ m3 + 1, m ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s) ⊦ (a ' + x).head = a; (s)

Proof step 19 from proof sublist-move (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: firstN-rec: ⊦ x.take(n + 1) = x.head + x.tail.take(n); firstn-firstn: ⊦ m ≤ n ∧ n ≤ # x → x.take(n).take(m) = x.take(m); ⊦ (a ' + x).head = a; (s) ⊦ (a ' + x).tail = x; (s) ⊦ a + x = a ' + x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + 1 ≠ 0; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: m, m0

Proof step 20 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  x0.take(m3).drop(n - 1).take(m) ≠ (a ' + x0).drop(n).take(m), n ≠ 0, n + m ≤ # x0 + 1, n + m ≤ m3 + 1, m3 ≤ # x0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ n -1 = n - 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s)

Proof step 21 from proof sublist-move (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  n = m0 + 1, x0.take(m3).drop(m0).take(m) ≠ (a ' + x0).drop(n).take(m), n ≠ 0, m3 ≤ # x0, n + m ≤ m3 + 1, n + m ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

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

Proof step 22 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  x0.take(m3).drop(m0).take(m) ≠ x0.drop(m0).take(m), m3 ≤ # x0, m0 + m ≤ m3, m0 + m ≤ # x0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: restN-rec: ⊦ x.drop(n + 1) = x.tail.drop(n); let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat 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 ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s)

Proof step 23 from proof sublist-move (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  ⊦ n ≤ # x → (y = x.take(n) ∧ z = x.drop(n) ↔ x = y + z ∧ # y = n)

Rule argument

Additional information

Used simplifier rules: rest-append: ⊦ n + m ≤ # x → (x + y).drop(n) = x.drop(n) + y; first-append-01: ⊦ n + m ≤ # x → (x.drop(n) + y).take(m) = x.drop(n).take(m); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x0, m3, y, z

Proof step 24 from proof sublist-move (previous step) (back to tree)

Lemma elim-firstn-restn

Proof step 25 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  x0.drop(n0 - 1).take(m0).drop(n).take(m) ≠ (a ' + x0).drop(n0 + n).take(m), n0 ≠ 0, n + m ≤ m0, n0 + m0 ≤ # x0 + 1, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ n -1 = n - 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s)

Proof step 26 from proof sublist-move (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 27:

  n0 = m3 + 1, x0.drop(m3).take(m0).drop(n).take(m) ≠ (a ' + x0).drop(n0 + n).take(m), n0 ≠ 0, n0 + m0 ≤ # x0 + 1, n + m ≤ m0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

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

Proof step 27 from proof sublist-move (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  x0.drop(m3).take(m0).drop(n).take(m) ≠ x0.drop(m3 + n).take(m), n + m ≤ m0, m3 + m0 ≤ # x0, ∀ n1, m1, n2, m2. x0.drop(n1).take(m1).drop(n2).take(m2) = x0.drop(n1 + n2).take(m2) ∨ ¬ n1 + m1 ≤ # x0 ∨ ¬ n2 + m2 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: restN-rec: ⊦ x.drop(n + 1) = x.tail.drop(n); 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 ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s)

Proof step 28 from proof sublist-move (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m3, m0, n, m