| i ^ i0 < i, i ^ i0 ≤ i0, 1 < i, 2 ≤ i, i ^ i0 < 1, i ^ i0 ≤ 0, 0 ≤ i0, i ^ i0 + 1 < i, ∀ j0, i. i→n(j0) < i→n(i0 +1) → true → 1 < i ∧ 0 < j0 → ¬ i ^ j0 ≤ 1 ⊦ |
Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1;%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%rax-04: ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; from specification intnat%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%labs: ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); from specification intnat%absle: ⊦ 0 ≤ i → abs(i) = i; from specification int-abs%irref: ⊦ ¬ i < i; from specification int-basic1%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2 Used terms: i0, i