| # sgn(bits) = 2 + i→n(i), bits2int(bits) < 2 ^ i * 2, 2 ^ i ≤ bits2int(bits), # bits ≤ 8, 127 < bits2int(bits), 64 < 2 ^ i, 63 < 2 ^ i, 64 < bits2int(bits), 63 < bits2int(bits), 0 < 2 ^ i, 0 ≤ 2 ^ i, 32 < 2 ^ i, 31 < 2 ^ i, 0 < bits2int(bits), 32 < bits2int(bits), 31 < bits2int(bits), 16 < 2 ^ i, 15 < 2 ^ i, 16 < bits2int(bits), 15 < bits2int(bits), 8 < 2 ^ i, 7 < 2 ^ i, 8 < bits2int(bits), 7 < bits2int(bits), 4 < 2 ^ i, 3 < 2 ^ i, 4 < bits2int(bits), 3 < bits2int(bits), 1 < i, 0 < i, 0 ≤ i, 1 < bits2int(bits), 1 < 2 ^ i, 6 < i ⊦ 0 = bits2int(bits), bits = [] |
Used simplifier rules: ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = i + i0 ↔ j = i0;% ⊦ 0 < i → n→i(i→n(i)) = i;% ⊦ n→i(m + n) = n→i(m) + n→i(n);% ⊦ i < j - i0 ↔ i + i0 < j;%0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n;% ⊦ i ≤ j - i0 ↔ i + i0 ≤ j;%0 ≤ i ⊦ (* i) ≤ n→i(n) ↔ i→n(i) ≤ n;% ⊦ m < n → m ≤ n;% ⊦ m < n ∧ n = n0 → m < n0; (forward)% ⊦ m < n → n ≠ 0; (forward)% ⊦ (* i) < j ∧ 0 < i → 0 ≤ j ∧ 0 < j; (forward)% ⊦ i < j ∧ j < i0 → i +1 < i0; (forward)% ⊦ i < j ∧ j < j0 → i < j0; (forward)% ⊦ m ≤ n ∧ n < n0 → m < n0; (forward)% ⊦ i ≤ j ∧ j < j0 → i < j0; (forward)% ⊦ # bits = 0 ↔ bits = [];% ⊦ sgn(bits) = [] ↔ bits = [];%n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0;%0 ≤ i ⊦ (* m) < i→n(i) ↔ n→i(m) < i;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = n + m;% ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0);% ⊦ i * j * j0 = (i * j) * j0;% ⊦ i * j = j * i;% ⊦ m < m + n ↔ n ≠ 0;% ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ i - j = i0 ↔ i = i0 + j;%0 ≤ i ⊦ n→i(n) = (* i) ↔ n = i→n(i);% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ m < n → ¬ n < m;% ⊦ ¬ m ≤ n ↔ n < m;%0 ≤ i ⊦ i→n(i) = (* m) ↔ i = n→i(m);% ⊦ 0 < i → (0 < i * j ↔ 0 < j);% ⊦ ¬ # bits < # sgn(bits); Used formulas: i = n→i(# sgn(bits)) - 2