| #oc(a0, (y + y0) -1l a) < #oc(a0, y) + #oc(a0, y0 -1l a), #oc(a0, x) ≤ #oc(a0, y) + #oc(a0, y0 -1l a), a0 ∈ x, a ∈ y0, #oc(a0, (y + y0) -1l a) < #oc(a0, x), ∀ a1. #oc(a1, x) ≤ #oc(a1, y) + #oc(a1, y0 -1l a) ⊦ #oc(a0, y) + #oc(a0, y0 -1l a) = 0 |
Used simplifier rules: del1: ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1;%in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0;%oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x;%oc-del-01: ⊦ a ∈ y → #oc(a, (x + y) -1l a) = #oc(a, x + y) -1;%ocappend: ⊦ #oc(a, x + y) = #oc(a, x) + #oc(a, y);%del1-01: ⊦ a ≠ b → #oc(a, x -1l b) = #oc(a, x);%ocappend: ⊦ #oc(a, x + y) = #oc(a, x) + #oc(a, y);%a: ⊦ (x + y) + z = x + y + z; from specification list%l: ⊦ m + n < m + n0 ↔ n < n0; 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%pred-03: ⊦ n -1 = n - 1; from specification nat%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%one-01: ⊦ m < 1 ↔ m = 0; from specification nat-basic1%eq-02: n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; from specification nat%one: ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; from specification nat-basic2%z-01: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; from specification nat-basic2%ls-01: n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; from specification nat%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2 Used formulas: a = a0