Comparison of the length of the code and the transparency of the solution via "Calculus basic predicates" and via Bitwise2 in solving a complex problem on bitwise conjunction

Down here we sequentially apply

¬A + A*B = (¬A + A)*(¬A + B) = ¬A + B
 A + ¬A*B = (A + ¬A)*(A + B) = A + B

Solution via "Calculus of basic predicates"
********************************************************************
(x&248 ¬= 152)v(x&252 = 156)v(x&250 = 154)v(x&A = 0) = 1
********************************************************************
252 = 11111100
156 = 10011100
248 = 11111000
152 = 10011000
250 = 11111010
154 = 10011010

(x&248 ¬= 152) = E(96) + ¬E(128) + ¬E(16) + ¬E(8)
(x&252 =  156)  =  ¬E(96)*E(128)*E(16)*E(8)*E(4)
(x&250 =  154)  =  ¬E(96)*E(128)*E(16)*E(8)*E(2)

E(96) + ¬E(128) + ¬E(16) + ¬E(8) + ¬E(96)*E(128)*E(16)*E(8)*E(4)
       + ¬E(96)*E(128)*E(16)*E(8)*E(2) + ¬E(A) ≡ 1

Converting ¬E(96)*E(128)*E(16)*E(8)*E(4) and get
E(96) + ¬E(128) + ¬E(16) + ¬E(8) entries like before run (1)
E(96) + ¬E(128) + ¬E(16) + ¬E(8)  + E(4) +
      + ¬E(96)*E(128)*E(16)*E(8)*E(2) + ¬E(A) = 1


Converting ¬E(96)*E(128)*E(16)*E(8)*E(2) and get
E(96) + ¬E(128) + ¬E(16) + ¬E(8) entries like before run (2)
E(96) + ¬E(128) + ¬E(16) + ¬E(8) + E(4) +
      + ¬E(96)*E(128)*E(16)*E(8)*E(2) + ¬E(A) ≡ 1

E(96)+ ¬E(128) + ¬E(16) + ¬E(8) + E(4) + E(2) ¬E(A) ≡ 1
E(102) + ¬E(128) + ¬E(16) + ¬E(8) +  ¬E(A) ≡ 1
(E(A)=> E(102)) + (E(A)=> ¬E(128)) + (E(A)=> ¬E(16)) + (E(A)=> ¬E(8)) ≡ 1

We get A(min) = 102

Solution via Bitwise2
********************************************************************
(x&248 ¬= 152)v(x&252 = 156)v(x&250 = 154)v(x&A = 0) = 1
********************************************************************
252 = 11111100
156 = 10011100
248 = 11111000
152 = 10011000
250 = 11111010
154 = 10011010

(x&248 ¬= 152) = ¬Z(96) + Z(128) + Z(16) + Z(8)
(x&252 =  156)  =  Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(4)
(x&250 =  154)  =  Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(2)


¬Z(96) + Z(128) + Z(16) + Z(8) + Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(4)
       + Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(2) + A = 1


Converting Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(4) and get
¬Z(96) + Z(128) + Z(16) + Z(8) entries like before run (1)
¬Z(96) + Z(128) + Z(16) + Z(8) + ¬Z(4)
       + Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(2)  + A =  1


Converting Z(96)*¬Z(128)*¬Z(16)*¬Z(8)*¬Z(2) and get
¬Z(96) + Z(128) + Z(16) + Z(8) entries like before run (2)
¬Z(96) + Z(128) + Z(16) + Z(8) + ¬Z(4) + ¬Z(2)  + A =  1


Now we are ready to apply De Morgan rules :-
     ¬(Z(96)*Z(4)*Z(2)) + Z(128) + Z(16) + Z(8) + A = 1

Finally getting done

Z(102) => Z(128) + Z(16) + Z(8) + A = 1
(Z(102)=>Z(128)) + (Z(102)=>Z(16)) + (Z(102)=>Z(8)) + (Z(102)=>A) = 1
Z(102) => A = 1

Which appears to be dual to

E(96)+ ¬E(128) + ¬E(16) + ¬E(8) + E(4) + E(2) ¬E(A) ≡ 1
E(102) + ¬E(128) + ¬E(16) + ¬E(8) +  ¬E(A) ≡ 1
(E(A)=> E(102)) + (E(A)=> ¬E(128)) + (E(A)=> ¬E(16)) + (E(A)=> ¬E(8)) ≡ 1

Due to Theorem 1
  For truth ∀ x: E(k)(x) => E(m)(x), e.g. E(k) => E(m) ≡ 1
  it is necessary  and sufficient that the set of unit bits "k"
  is fully included in the set of unit bits "m"


Final conclusion - the both approaches work almost the same way 
due to Polyakov's formulas for extended Bitwise2 functionality.
Both approaches one more time demonstrate completely dual nature
of working code in both versions and provide the same level transparency .
In other words, if "c" (see snapshot above) requires a decomposition 
into a relatively long sum of basic predicates, Polyakov's formulas work absolutely as well as basic predicates, what generally can be seen directly 
from their definition

Окончательный вывод - оба подхода работают практически одинаково
в силу формул Полякова для расширенной функциональности Bitwise2.
Оба подхода еще раз демонстрируют полностью двойственную природу
рабочего кода в обоих версиях и обеспечивают тот же уровень прозрачности. Другими словами, если «c» (см. снапшот выше) требует декомпозиции в сравнительно длинную сумму базисных предикатов формулы Полякова работают абсолютно так же, как и базисные предикаты,что легко можно увидеть непосредственно из их определения.