Proof step 1 from proof trans-list (conclusion) (back to tree)

⊦ x < x0 ∧ x0 < x1 → x < x1

System applied rule normalize

And obtained the following new goals

Proof step 2:
x < x0, x0 < x1, ¬ x < x1 ⊦

Rule argument

Additional information

Proof step 2 from proof trans-list (previous step) (back to tree)

x < x0, x0 < x1, ¬ x < x1 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 3:
⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)
Proof step 4:
x0 < x1, x < x0, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Rule argument

spec: array-listops, name:postfix, seq:⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0), subst:[ar0, ar1] → [x, x1], <all paths>

Additional information

Used terms: x, x1

Proof step 3 from proof trans-list (previous step) (back to tree)

⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)

A spec-lemma

Proof step 4 from proof trans-list (previous step) (back to tree)

x0 < x1, x < x0, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 5:
⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)
Proof step 6:
x = subarray(x0, # x0 - # x, # x), # x < # x0, x0 < x1, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Rule argument

spec: array-listops, name:postfix, seq:⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0), subst:[ar0, ar1] → [x, x0], <all paths>

Additional information

Used terms: x, x0

Proof step 5 from proof trans-list (previous step) (back to tree)

⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)

A spec-lemma

Proof step 6 from proof trans-list (previous step) (back to tree)

x = subarray(x0, # x0 - # x, # x), # x < # x0, x0 < x1, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

Proof step 7:
# x0 = n0 + # x, x = subarray(x0, n0, # x), x0 < x1, # x < # x0, # x ≤ # x0, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[m, n, n0] → [# x0, # x, n0]

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x0, # x, n0

Proof step 7 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, x = subarray(x0, n0, # x), x0 < x1, # x < # x0, # x ≤ # x0, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 8:
# x0 = n0 + # x, x = subarray(x0, n0, # x), n0 ≠ 0, x0 < x1, # x < # x0, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

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 < m + n ↔ n ≠ 0; (s) ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s)

Proof step 8 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, x = subarray(x0, n0, # x), n0 ≠ 0, x0 < x1, # x < # x0, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 9:
⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)
Proof step 10:
# x0 = n0 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, # x1 - # x0, # x0), n0 ≠ 0, # x < # x0, # x0 < # x1, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Rule argument

spec: array-listops, name:postfix, seq:⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0), subst:[ar0, ar1] → [x0, x1], <all paths>

Additional information

Used terms: x0, x1

Proof step 9 from proof trans-list (previous step) (back to tree)

⊦ ar0 < ar1 ↔ # ar0 < # ar1 ∧ ar0 = subarray(ar1, # ar1 - # ar0, # ar0)

A spec-lemma

Proof step 10 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, # x1 - # x0, # x0), n0 ≠ 0, # x < # x0, # x0 < # x1, ¬ # x < # x1 ∨ x ≠ subarray(x1, # x1 - # x, # x) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 11:
# x0 = n0 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, # x1 - # x0, # x0), n0 ≠ 0, x ≠ subarray(x1, # x1 - # x, # x), # x < # x1, # x < # x0, # x0 < # x1, # x + 1 < # x1 ⊦

Rule argument

Additional information

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

Proof step 11 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, # x1 - # x0, # x0), n0 ≠ 0, x ≠ subarray(x1, # x1 - # x, # x), # x < # x1, # x < # x0, # x0 < # x1, # x + 1 < # x1 ⊦

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

Proof step 12:
# x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, x ≠ subarray(x1, # x1 - # x, # x), # x + 1 < # x1, # x0 < # x1, # x < # x0, # x < # x1, # x0 ≤ # x1 ⊦

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[m, n, n0] → [# x1, # x0, n1]

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x1, # x0, n

Proof step 12 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, x ≠ subarray(x1, # x1 - # x, # x), # x + 1 < # x1, # x0 < # x1, # x < # x0, # x < # x1, # x0 ≤ # x1 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 13:
# x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, x ≠ subarray(x1, # x1 - # x, # x), # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1 ⊦

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 < m + n ↔ n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s)

Proof step 13 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, x ≠ subarray(x1, # x1 - # x, # x), # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1 ⊦

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

Proof step 14:
# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, x ≠ subarray(x1, n2, # x), # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, # x ≤ # x1 ⊦

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[m, n, n0] → [# x1, # x, n2]

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x1, # x, n

Proof step 14 from proof trans-list (previous step) (back to tree)

# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, x ≠ subarray(x1, n2, # x), # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, # x ≤ # x1 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 15:
# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, n2 ≠ 1, n2 ≠ 0, x ≠ subarray(x1, n2, # x), # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1 ⊦

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 < m + n ↔ n ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s)

Proof step 15 from proof trans-list (previous step) (back to tree)

# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, n2 ≠ 1, n2 ≠ 0, x ≠ subarray(x1, n2, # x), # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 16:
⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])
Proof step 17:
# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, n2 ≠ 1, n2 ≠ 0, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, # x ≠ # subarray(x1, n2, # x) ∨ (∃ n. ¬(n < # x → x[n] = subarray(x1, n2, # x)[n])) ⊦

Rule argument

spec: array, name:Extension, seq:⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n]), subst:[ar1, ar2] → [x, subarray(x1, n2, # x)], <all paths>

Additional information

Used terms: x, subarray(x1, n2, # x)

Proof step 16 from proof trans-list (previous step) (back to tree)

⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

A spec-lemma

Proof step 17 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), n0 ≠ 0, n1 ≠ 0, n2 ≠ 1, n2 ≠ 0, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, # x ≠ # subarray(x1, n2, # x) ∨ (∃ n. ¬(n < # x → x[n] = subarray(x1, n2, # x)[n])) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 18:
# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic 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) ⊦ m + n < m0 → m + n < m0 + n0; (s) trans: ⊦ 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 ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 18 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x = subarray(x0, n0, # x), x0 = subarray(x1, n1, # x0), x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 19:
⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])
Proof step 20:
# x = # subarray(x0, n0, # x), # x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x0 = subarray(x1, n1, # x0), x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, ∀ n. n < # x → x[n] = subarray(x0, n0, # x)[n] ⊦

Rule argument

spec: array, name:Extension, seq:⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n]), subst:[ar1, ar2] → [x, subarray(x0, n0, # x)], <all paths>

Additional information

Used terms: x, subarray(x0, n0, # x)

Proof step 19 from proof trans-list (previous step) (back to tree)

⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

A spec-lemma

Proof step 20 from proof trans-list (previous step) (back to tree)

# x = # subarray(x0, n0, # x), # x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x0 = subarray(x1, n1, # x0), x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, ∀ n. n < # x → x[n] = subarray(x0, n0, # x)[n] ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 21:
# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x0 = subarray(x1, n1, # x0), x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 21 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x0 = subarray(x1, n1, # x0), x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 22:
⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])
Proof step 23:
# x0 = # subarray(x1, n1, # x0), # x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n. n < # x0 → x0[n] = subarray(x1, n1, # x0)[n] ⊦

Rule argument

spec: array, name:Extension, seq:⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n]), subst:[ar1, ar2] → [x0, subarray(x1, n1, # x0)], <all paths>

Additional information

Used terms: x0, subarray(x1, n1, # x0)

Proof step 22 from proof trans-list (previous step) (back to tree)

⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

A spec-lemma

Proof step 23 from proof trans-list (previous step) (back to tree)

# x0 = # subarray(x1, n1, # x0), # x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n. n < # x0 → x0[n] = subarray(x1, n1, # x0)[n] ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 24:
# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 24 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3] ⊦

User applied rule all left

And obtained the following new goals

Proof step 25:
# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, n < # x → x[n] = x0[n0 + n], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3], ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

Rule argument

pos: left 19 terms: n abort: F discard: F computed: T

Additional information

Used terms: n

Proof step 25 from proof trans-list (previous step) (back to tree)

# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, n < # x → x[n] = x0[n0 + n], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3], ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 26:
# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x[n] = x0[n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3] ⊦

Rule argument

Additional information

Proof step 26 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x[n] = x0[n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3] ⊦

User applied rule all left

And obtained the following new goals

Proof step 27:
# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x[n] = x0[n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, n0 + n < # x0 → x0[n0 + n] = x1[n1 + n0 + n], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3], ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

Rule argument

pos: left 21 terms: n0 + n abort: F discard: F computed: F

Additional information

Used terms: n0 + n

Proof step 27 from proof trans-list (previous step) (back to tree)

# x1 = n1 + # x0, # x0 = n0 + # x, # x1 = n2 + # x, x[n] = x0[n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < # x1, n < # x1, n < # x0, # x + 1 < # x1, # x < # x1, # x < # x0, # x0 < # x1, n < # x, 2 + n < # x1, n0 + n < # x0 → x0[n0 + n] = x1[n1 + n0 + n], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3], ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 28:
# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x[n] = x0[n0 + n], x[n] = x1[n1 + n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3] ⊦

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 = m0 + n0 ∧ n < n0 → m0 + n < m; (s)

Proof step 28 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, # x1 = n1 + # x0, x[n] = x0[n0 + n], x[n] = x1[n1 + n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < # x1, n < # x, # x0 < # x1, # x < # x0, # x < # x1, # x + 1 < # x1, n < # x0, n < # x1, n + 1 < # x1, n + 1 < # x0, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3] ⊦

User applied rule subst equation

And obtained the following new goals

Proof step 29:
# x0 = n0 + # x, # x1 = n2 + # x, n2 + # x = n1 + # x0, x[n] = x1[n1 + n0 + n], x[n] = x0[n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < n2 + # x, n < n2 + # x, n < # x0, # x + 1 < n2 + # x, # x < n2 + # x, # x < # x0, # x0 < n2 + # x, n < # x, 2 + n < n2 + # x, ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3], ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

Rule argument

pos: left 1, flags:

Additional information

Proof step 29 from proof trans-list (previous step) (back to tree)

# x0 = n0 + # x, # x1 = n2 + # x, n2 + # x = n1 + # x0, x[n] = x1[n1 + n0 + n], x[n] = x0[n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, n + 1 < # x0, n + 1 < n2 + # x, n < n2 + # x, n < # x0, # x + 1 < n2 + # x, # x < n2 + # x, # x < # x0, # x0 < n2 + # x, n < # x, 2 + n < n2 + # x, ∀ n3. n3 < # x0 → x0[n3] = x1[n1 + n3], ∀ n3. n3 < # x → x[n3] = x0[n0 + n3] ⊦

User applied rule subst equation

And obtained the following new goals

Proof step 30:
# x1 = n2 + # x, # x0 = n0 + # x, n2 + # x = n1 + n0 + # x, x[n] = x0[n0 + n], x[n] = x1[n1 + n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < n2 + # x, n < # x, n0 + # x < n2 + # x, # x < n0 + # x, # x < n2 + # x, # x + 1 < n2 + # x, n < n0 + # x, n < n2 + # x, n + 1 < n2 + # x, n + 1 < n0 + # x, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < n0 + # x → x0[n3] = x1[n1 + n3] ⊦

Rule argument

pos: left 1, flags:

Additional information

Proof step 30 from proof trans-list (previous step) (back to tree)

# x1 = n2 + # x, # x0 = n0 + # x, n2 + # x = n1 + n0 + # x, x[n] = x0[n0 + n], x[n] = x1[n1 + n0 + n], x[n] ≠ x1[n2 + n], n0 ≠ 0, n1 ≠ 0, n2 ≠ 0, n2 ≠ 1, 2 + n < n2 + # x, n < # x, n0 + # x < n2 + # x, # x < n0 + # x, # x < n2 + # x, # x + 1 < n2 + # x, n < n0 + # x, n < n2 + # x, n + 1 < n2 + # x, n + 1 < n0 + # x, ∀ n3. n3 < # x → x[n3] = x0[n0 + n3], ∀ n3. n3 < n0 + # x → x0[n3] = x1[n1 + n3] ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 31:
n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n)

Rule argument

spec: nat, name:add-num-01, seq:n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n), subst:[m, n, m0, n0] → [n2, # x, n1, n0 + # x], <all paths>

Additional information

Used simplifier rules: ⊦ m + n - m = n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic Used terms: n2, # x, n1, n0 + # x