Proof step 32 from proof sis-on-bits (previous step)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: inshort: ⊦ i ∈short ↔ ~32768 ≤ i ∧ i ≤ 32767;%inshort: ⊦ i ∈short ↔ ~32768 ≤ i ∧ i ≤ 32767;% ⊦ i ≠ j → (i ≤ j ↔ i < j);% ⊦ ~1 < i ↔ 0 ≤ i;% ⊦ i ≤ j → (j ≤ i ↔ i = j);% ⊦ int2bits(0) = false ';% ⊦ 0 < n → fillsgn(n, boolvar ') = mklist(boolvar, n);%n ≠ 0 ⊦ mklist(false, (* n)) = false ' + mklist(false, n -1);% ⊦ mklist(boolvar, 0) = [];% ⊦ bits + [] = bits;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;%0 < n ⊦ lastn((* n), bits + boolvar ') = lastn(n -1, bits) + boolvar ';% ⊦ lastn(1, boolvar ') = boolvar ';% ⊦ bits2int(false ' + bits) = bits2uint(bits);% ⊦ bits2uint(bits + false ') = bits2uint(bits) * 2;% ⊦ bits2uint(false ') = 0;% ⊦ # boolvar ' = 0 +1; Used formulas: i = ~1