| 0 ≤ j, 0 ≤ i0, 0 ≤ i0 * j, 0 ≤ 1 * j, ∀ j1, j, i. i→n(j1) < i→n(i0 + 1) → 0 ≤ j1 ∧ 0 ≤ j → i ^ (j * j1) = (i ^ j) ^ j1 ⊦ i ^ (i0 * j) * i ^ (1 * j) = (i ^ j) ^ i0 * i ^ j |
Used simplifier rules: ⊦ 1 * i = i; (s)%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult% ⊦ 0 ≤ i → (0 ≤ i * j ↔ i = 0 ∨ 0 ≤ j); (s)% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)%neq-not-zero: ⊦ i * j ≠ i * j0 → i ≠ 0; (forward) from specification int-mult% ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; (s)%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s)% ⊦ 0 ≤ i → abs(i) = i; (s)% ⊦ ¬ i < i; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic Used terms: i0, j, i