| 0 ≤ i0 * j ∧ 0 ≤ 1 * j, 0 ≤ j, 0 ≤ i0, ∀ j1, j, i. i→n(j1) < i→n(i0 + 1) → 0 ≤ j ∧ 0 ≤ j1 → i ^ (j * j1) = (i ^ j) ^ j1 ⊦ i ^ (i0 * j) * i ^ (1 * j) = (i ^ j) ^ i0 * i ^ j |
Used simplifier rules: one: ⊦ 1 * i = i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%zero-ge-02: ⊦ 0 ≤ i → (0 ≤ i * j ↔ ¬ ¬(i = 0 ∨ 0 ≤ j)); from specification int-mult%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%neq-not-zero: ⊦ i * j ≠ i * j0 → i ≠ 0; (forward) from specification int-mult%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, j, i