Proof step 1 from proof restn-size-last (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  restn(# x, a ' + x) ≠ (a ' + x).last ' ⊦

Rule argument

Additional information

Proof step 2 from proof restn-size-last (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 3:

  restn(# x, a ' + x) ≠ (a ' + x).last ', x ≠ [] ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ restn(0, x) = x; ⊦ # [] = 0; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a '.last = a; (s) ⊦ a ' = b ' ↔ a = b; (s) Used formulas: x = []

Proof step 3 from proof restn-size-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  restn(# x, a ' + x) ≠ x.last ', x ≠ [] ⊦

Rule argument

Additional information

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

Proof step 4 from proof restn-size-last (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: restN-rec: ⊦ restn(n + 1, x) = restn(n, x.tail); restN-len: ⊦ restn(# x, x + y) = y; ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) ⊦ (a ' + x).tail = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a ' = b ' ↔ a = b; (s) x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x, a0, y