| x.last = z.last, x.butlast ⊒ y + z.butlast, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z → x0 ⊒ z ∨ (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ y + z = [], z = [], x = [], x.butlast ⊒ z.butlast, ∃ x0. x0 + z = x ∧ x0 ⊒ y |
Used simplifier rules: lb: ⊦ x ≠ [] → # x.butlast = # x - 1;%blapp-01: ⊦ x ≠ [] → (x.butlast = y ↔ x = y + x.last ');%butlast-last: x ≠ [] ⊦ x.butlast + x.last ' = x;%lapp: ⊦ y ≠ [] → (x + y).last = y.last;%lin-01: ⊦ x.last ∈ x ↔ x ≠ [];%bapp: ⊦ y ≠ [] → (x + y).butlast = x + y.butlast;%postfix-app-02: ⊦ y + x ⊒ z + x ↔ y ⊒ z;%in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list%a: ⊦ (x + y) + z = x + y + z; from specification list%in-append: ⊦ a ∈ x + y ↔ ¬ ¬(a ∈ x ∨ a ∈ y); from specification list%app-03: ⊦ x + y = z + y ↔ x = z; from specification list%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%one-01: ⊦ m < 1 ↔ m = 0; from specification nat-basic1%l: ⊦ # x = 0 ↔ x = []; from specification list-data%ls-01: n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; from specification nat%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%ref-1: ⊦ ¬ n < n; from specification nat-basic1%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2 Used terms: x.butlast, y, z.butlast