:: Correctness of a Cyclic Redundancy Check Code Generator
:: by Yuguang Yang , Katsumi Wasaki , Yasushi Fuwa and Yatsuka Nakamura
::
:: Received April 16, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

:: Correctness of Division Circuits with 12-bit Register and 16-bit Register
::
:: Assumptions:
:: g0,g1,g2,...,g12: the coefficients of divident polynomial;
:: a0,a1,a2,...,a11: the present state of register;
:: p: input;
:: b0,b1,b2,...,b11: the state of register with input p;
:: A=(a11, a10, ..., a1, a0), B=(b11, b10, ..., b1,b0);
:: G=(g12,g11,g10,...,g1,g0);
:: A + B = (a11+b11, a10+b10, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or.
::
:: In a division circuit, a shift is expected to complete one step division by
:: divident polynomial. So we can derive the relation of A, B, G and p as following:
:: A*2+p=G*a11+B
:: here, A*2=(a11, a10, ..., a1, a0)*2=(a11, a10, ..., a1, a0,0),
:: G*a11=(g12 & a11, g11 & a11, g10 & a11,...,g1 & a11, g0 & a11).

theorem :: GATE_4:1

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, p being set holds
not ( not g12 is empty & ( not b0 is empty implies not XOR2 (p,(AND2 (g0,a11))) is empty ) & ( not XOR2 (p,(AND2 (g0,a11))) is empty implies not b0 is empty ) & ( not b1 is empty implies not XOR2 (a0,(AND2 (g1,a11))) is empty ) & ( not XOR2 (a0,(AND2 (g1,a11))) is empty implies not b1 is empty ) & ( not b2 is empty implies not XOR2 (a1,(AND2 (g2,a11))) is empty ) & ( not XOR2 (a1,(AND2 (g2,a11))) is empty implies not b2 is empty ) & ( not b3 is empty implies not XOR2 (a2,(AND2 (g3,a11))) is empty ) & ( not XOR2 (a2,(AND2 (g3,a11))) is empty implies not b3 is empty ) & ( not b4 is empty implies not XOR2 (a3,(AND2 (g4,a11))) is empty ) & ( not XOR2 (a3,(AND2 (g4,a11))) is empty implies not b4 is empty ) & ( not b5 is empty implies not XOR2 (a4,(AND2 (g5,a11))) is empty ) & ( not XOR2 (a4,(AND2 (g5,a11))) is empty implies not b5 is empty ) & ( not b6 is empty implies not XOR2 (a5,(AND2 (g6,a11))) is empty ) & ( not XOR2 (a5,(AND2 (g6,a11))) is empty implies not b6 is empty ) & ( not b7 is empty implies not XOR2 (a6,(AND2 (g7,a11))) is empty ) & ( not XOR2 (a6,(AND2 (g7,a11))) is empty implies not b7 is empty ) & ( not b8 is empty implies not XOR2 (a7,(AND2 (g8,a11))) is empty ) & ( not XOR2 (a7,(AND2 (g8,a11))) is empty implies not b8 is empty ) & ( not b9 is empty implies not XOR2 (a8,(AND2 (g9,a11))) is empty ) & ( not XOR2 (a8,(AND2 (g9,a11))) is empty implies not b9 is empty ) & ( not b10 is empty implies not XOR2 (a9,(AND2 (g10,a11))) is empty ) & ( not XOR2 (a9,(AND2 (g10,a11))) is empty implies not b10 is empty ) & ( not b11 is empty implies not XOR2 (a10,(AND2 (g11,a11))) is empty ) & ( not XOR2 (a10,(AND2 (g11,a11))) is empty implies not b11 is empty ) & not ( ( not a11 is empty implies not AND2 (g12,a11) is empty ) & ( not AND2 (g12,a11) is empty implies not a11 is empty ) & ( not a10 is empty implies not XOR2 (b11,(AND2 (g11,a11))) is empty ) & ( not XOR2 (b11,(AND2 (g11,a11))) is empty implies not a10 is empty ) & ( not a9 is empty implies not XOR2 (b10,(AND2 (g10,a11))) is empty ) & ( not XOR2 (b10,(AND2 (g10,a11))) is empty implies not a9 is empty ) & ( not a8 is empty implies not XOR2 (b9,(AND2 (g9,a11))) is empty ) & ( not XOR2 (b9,(AND2 (g9,a11))) is empty implies not a8 is empty ) & ( not a7 is empty implies not XOR2 (b8,(AND2 (g8,a11))) is empty ) & ( not XOR2 (b8,(AND2 (g8,a11))) is empty implies not a7 is empty ) & ( not a6 is empty implies not XOR2 (b7,(AND2 (g7,a11))) is empty ) & ( not XOR2 (b7,(AND2 (g7,a11))) is empty implies not a6 is empty ) & ( not a5 is empty implies not XOR2 (b6,(AND2 (g6,a11))) is empty ) & ( not XOR2 (b6,(AND2 (g6,a11))) is empty implies not a5 is empty ) & ( not a4 is empty implies not XOR2 (b5,(AND2 (g5,a11))) is empty ) & ( not XOR2 (b5,(AND2 (g5,a11))) is empty implies not a4 is empty ) & ( not a3 is empty implies not XOR2 (b4,(AND2 (g4,a11))) is empty ) & ( not XOR2 (b4,(AND2 (g4,a11))) is empty implies not a3 is empty ) & ( not a2 is empty implies not XOR2 (b3,(AND2 (g3,a11))) is empty ) & ( not XOR2 (b3,(AND2 (g3,a11))) is empty implies not a2 is empty ) & ( not a1 is empty implies not XOR2 (b2,(AND2 (g2,a11))) is empty ) & ( not XOR2 (b2,(AND2 (g2,a11))) is empty implies not a1 is empty ) & ( not a0 is empty implies not XOR2 (b1,(AND2 (g1,a11))) is empty ) & ( not XOR2 (b1,(AND2 (g1,a11))) is empty implies not a0 is empty ) & ( not p is empty implies not XOR2 (b0,(AND2 (g0,a11))) is empty ) & ( not XOR2 (b0,(AND2 (g0,a11))) is empty implies not p is empty ) ) )

proof end;

:: Assumptions:
:: g0,g1,g2,...,g16: the coefficients of divident polynomial;
:: a0,a1,a2,...,a15: the present state of register;
:: p: input;
:: b0,b1,b2,...,b15: the state of register with input p;
:: A=(a15, a14, ..., a1, a0), B=(b15, b14, ..., b1,b0);
:: G=(g16,g15,g14,...,g1,g0);
:: A + B = (a15+b15, a14+b14, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or.
::
:: In a division circuit, a shift is expected to complete one step division by
:: divident polynomial. So we can derive the relation of A, B, G and p as following:
:: A*2+p=G*a15+B
:: here, A*2=(a15, a14, ..., a1, a0)*2=(a15, a14, ..., a1, a0,0),
:: G*a15=(g16 & a15, g15 & a15, g14 & a15,...,g1 & a15, g0 is not empty & a15).

theorem :: GATE_4:2

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, p being set holds
not ( not g16 is empty & ( not b0 is empty implies not XOR2 (p,(AND2 (g0,a15))) is empty ) & ( not XOR2 (p,(AND2 (g0,a15))) is empty implies not b0 is empty ) & ( not b1 is empty implies not XOR2 (a0,(AND2 (g1,a15))) is empty ) & ( not XOR2 (a0,(AND2 (g1,a15))) is empty implies not b1 is empty ) & ( not b2 is empty implies not XOR2 (a1,(AND2 (g2,a15))) is empty ) & ( not XOR2 (a1,(AND2 (g2,a15))) is empty implies not b2 is empty ) & ( not b3 is empty implies not XOR2 (a2,(AND2 (g3,a15))) is empty ) & ( not XOR2 (a2,(AND2 (g3,a15))) is empty implies not b3 is empty ) & ( not b4 is empty implies not XOR2 (a3,(AND2 (g4,a15))) is empty ) & ( not XOR2 (a3,(AND2 (g4,a15))) is empty implies not b4 is empty ) & ( not b5 is empty implies not XOR2 (a4,(AND2 (g5,a15))) is empty ) & ( not XOR2 (a4,(AND2 (g5,a15))) is empty implies not b5 is empty ) & ( not b6 is empty implies not XOR2 (a5,(AND2 (g6,a15))) is empty ) & ( not XOR2 (a5,(AND2 (g6,a15))) is empty implies not b6 is empty ) & ( not b7 is empty implies not XOR2 (a6,(AND2 (g7,a15))) is empty ) & ( not XOR2 (a6,(AND2 (g7,a15))) is empty implies not b7 is empty ) & ( not b8 is empty implies not XOR2 (a7,(AND2 (g8,a15))) is empty ) & ( not XOR2 (a7,(AND2 (g8,a15))) is empty implies not b8 is empty ) & ( not b9 is empty implies not XOR2 (a8,(AND2 (g9,a15))) is empty ) & ( not XOR2 (a8,(AND2 (g9,a15))) is empty implies not b9 is empty ) & ( not b10 is empty implies not XOR2 (a9,(AND2 (g10,a15))) is empty ) & ( not XOR2 (a9,(AND2 (g10,a15))) is empty implies not b10 is empty ) & ( not b11 is empty implies not XOR2 (a10,(AND2 (g11,a15))) is empty ) & ( not XOR2 (a10,(AND2 (g11,a15))) is empty implies not b11 is empty ) & ( not b12 is empty implies not XOR2 (a11,(AND2 (g12,a15))) is empty ) & ( not XOR2 (a11,(AND2 (g12,a15))) is empty implies not b12 is empty ) & ( not b13 is empty implies not XOR2 (a12,(AND2 (g13,a15))) is empty ) & ( not XOR2 (a12,(AND2 (g13,a15))) is empty implies not b13 is empty ) & ( not b14 is empty implies not XOR2 (a13,(AND2 (g14,a15))) is empty ) & ( not XOR2 (a13,(AND2 (g14,a15))) is empty implies not b14 is empty ) & ( not b15 is empty implies not XOR2 (a14,(AND2 (g15,a15))) is empty ) & ( not XOR2 (a14,(AND2 (g15,a15))) is empty implies not b15 is empty ) & not ( ( not a15 is empty implies not AND2 (g16,a15) is empty ) & ( not AND2 (g16,a15) is empty implies not a15 is empty ) & ( not a14 is empty implies not XOR2 (b15,(AND2 (g15,a15))) is empty ) & ( not XOR2 (b15,(AND2 (g15,a15))) is empty implies not a14 is empty ) & ( not a13 is empty implies not XOR2 (b14,(AND2 (g14,a15))) is empty ) & ( not XOR2 (b14,(AND2 (g14,a15))) is empty implies not a13 is empty ) & ( not a12 is empty implies not XOR2 (b13,(AND2 (g13,a15))) is empty ) & ( not XOR2 (b13,(AND2 (g13,a15))) is empty implies not a12 is empty ) & ( not a11 is empty implies not XOR2 (b12,(AND2 (g12,a15))) is empty ) & ( not XOR2 (b12,(AND2 (g12,a15))) is empty implies not a11 is empty ) & ( not a10 is empty implies not XOR2 (b11,(AND2 (g11,a15))) is empty ) & ( not XOR2 (b11,(AND2 (g11,a15))) is empty implies not a10 is empty ) & ( not a9 is empty implies not XOR2 (b10,(AND2 (g10,a15))) is empty ) & ( not XOR2 (b10,(AND2 (g10,a15))) is empty implies not a9 is empty ) & ( not a8 is empty implies not XOR2 (b9,(AND2 (g9,a15))) is empty ) & ( not XOR2 (b9,(AND2 (g9,a15))) is empty implies not a8 is empty ) & ( not a7 is empty implies not XOR2 (b8,(AND2 (g8,a15))) is empty ) & ( not XOR2 (b8,(AND2 (g8,a15))) is empty implies not a7 is empty ) & ( not a6 is empty implies not XOR2 (b7,(AND2 (g7,a15))) is empty ) & ( not XOR2 (b7,(AND2 (g7,a15))) is empty implies not a6 is empty ) & ( not a5 is empty implies not XOR2 (b6,(AND2 (g6,a15))) is empty ) & ( not XOR2 (b6,(AND2 (g6,a15))) is empty implies not a5 is empty ) & ( not a4 is empty implies not XOR2 (b5,(AND2 (g5,a15))) is empty ) & ( not XOR2 (b5,(AND2 (g5,a15))) is empty implies not a4 is empty ) & ( not a3 is empty implies not XOR2 (b4,(AND2 (g4,a15))) is empty ) & ( not XOR2 (b4,(AND2 (g4,a15))) is empty implies not a3 is empty ) & ( not a2 is empty implies not XOR2 (b3,(AND2 (g3,a15))) is empty ) & ( not XOR2 (b3,(AND2 (g3,a15))) is empty implies not a2 is empty ) & ( not a1 is empty implies not XOR2 (b2,(AND2 (g2,a15))) is empty ) & ( not XOR2 (b2,(AND2 (g2,a15))) is empty implies not a1 is empty ) & ( not a0 is empty implies not XOR2 (b1,(AND2 (g1,a15))) is empty ) & ( not XOR2 (b1,(AND2 (g1,a15))) is empty implies not a0 is empty ) & ( not p is empty implies not XOR2 (b0,(AND2 (g0,a15))) is empty ) & ( not XOR2 (b0,(AND2 (g0,a15))) is empty implies not p is empty ) ) )

proof end;

:: Degree 12 and 16
:: Assumptions:
:: g0,g1,g2,...,g12: the coefficients of generator polynomial;
:: a0,a1,a2,...,a11: the present state of register;
:: p: input;
:: b0,b1,b2,...,b11: the state of register after a shift with input p;
:: A=(a11, a10, ..., a1, a0), B=(b11, b10, ..., b1,b0);
:: G=(g12,g11,g10,...,g1,g0)
:: A + B=(a11+b11, a10+b10, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or;
:: A*2=(a11, a10, ..., a1, a0)*2=(a11, a10, ..., a1, a0,0);
:: G*a11=(g12 is not empty & a11, g11 & a11, g10 & a11,...,g1 & a11, g0 is not empty & a11);
:: 2^11 means 2 to the 11th power.
::
::
:: In a CRC circuit, with assumption that A is the remainder of message M*2^11
:: divided by G, B which is the contents of register after one shift is expected
:: to be the remainder of (M*2 + p)*2^11 divided by G. That means
:: B= mod((M*2 + p)*2^11,G)
:: = mod(M*2^12+ p*2^11,G)
:: = mod(M*2^12,G) + mod(p*2^11,G)
:: = mod(A*2,G) + mod(p*2^11,G)
:: = (A*2+G*a11)+(p*2^11 + G*p);
::
:: Note: The initial state of register can be regarded as M=0.

theorem :: GATE_4:3

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, z, p being set st not g0 is empty & z is empty & ( not b0 is empty implies not XOR2 (p,a11) is empty ) & ( not XOR2 (p,a11) is empty implies not b0 is empty ) & ( not b1 is empty implies not XOR2 (a0,(AND2 (g1,b0))) is empty ) & ( not XOR2 (a0,(AND2 (g1,b0))) is empty implies not b1 is empty ) & ( not b2 is empty implies not XOR2 (a1,(AND2 (g2,b0))) is empty ) & ( not XOR2 (a1,(AND2 (g2,b0))) is empty implies not b2 is empty ) & ( not b3 is empty implies not XOR2 (a2,(AND2 (g3,b0))) is empty ) & ( not XOR2 (a2,(AND2 (g3,b0))) is empty implies not b3 is empty ) & ( not b4 is empty implies not XOR2 (a3,(AND2 (g4,b0))) is empty ) & ( not XOR2 (a3,(AND2 (g4,b0))) is empty implies not b4 is empty ) & ( not b5 is empty implies not XOR2 (a4,(AND2 (g5,b0))) is empty ) & ( not XOR2 (a4,(AND2 (g5,b0))) is empty implies not b5 is empty ) & ( not b6 is empty implies not XOR2 (a5,(AND2 (g6,b0))) is empty ) & ( not XOR2 (a5,(AND2 (g6,b0))) is empty implies not b6 is empty ) & ( not b7 is empty implies not XOR2 (a6,(AND2 (g7,b0))) is empty ) & ( not XOR2 (a6,(AND2 (g7,b0))) is empty implies not b7 is empty ) & ( not b8 is empty implies not XOR2 (a7,(AND2 (g8,b0))) is empty ) & ( not XOR2 (a7,(AND2 (g8,b0))) is empty implies not b8 is empty ) & ( not b9 is empty implies not XOR2 (a8,(AND2 (g9,b0))) is empty ) & ( not XOR2 (a8,(AND2 (g9,b0))) is empty implies not b9 is empty ) & ( not b10 is empty implies not XOR2 (a9,(AND2 (g10,b0))) is empty ) & ( not XOR2 (a9,(AND2 (g10,b0))) is empty implies not b10 is empty ) & ( not b11 is empty implies not XOR2 (a10,(AND2 (g11,b0))) is empty ) & ( not XOR2 (a10,(AND2 (g11,b0))) is empty implies not b11 is empty ) holds
( ( not b11 is empty implies not XOR2 ((XOR2 (a10,(AND2 (g11,a11)))),(XOR2 (z,(AND2 (g11,p))))) is empty ) & ( not XOR2 ((XOR2 (a10,(AND2 (g11,a11)))),(XOR2 (z,(AND2 (g11,p))))) is empty implies not b11 is empty ) & ( not b10 is empty implies not XOR2 ((XOR2 (a9,(AND2 (g10,a11)))),(XOR2 (z,(AND2 (g10,p))))) is empty ) & ( not XOR2 ((XOR2 (a9,(AND2 (g10,a11)))),(XOR2 (z,(AND2 (g10,p))))) is empty implies not b10 is empty ) & ( not b9 is empty implies not XOR2 ((XOR2 (a8,(AND2 (g9,a11)))),(XOR2 (z,(AND2 (g9,p))))) is empty ) & ( not XOR2 ((XOR2 (a8,(AND2 (g9,a11)))),(XOR2 (z,(AND2 (g9,p))))) is empty implies not b9 is empty ) & ( not b8 is empty implies not XOR2 ((XOR2 (a7,(AND2 (g8,a11)))),(XOR2 (z,(AND2 (g8,p))))) is empty ) & ( not XOR2 ((XOR2 (a7,(AND2 (g8,a11)))),(XOR2 (z,(AND2 (g8,p))))) is empty implies not b8 is empty ) & ( not b7 is empty implies not XOR2 ((XOR2 (a6,(AND2 (g7,a11)))),(XOR2 (z,(AND2 (g7,p))))) is empty ) & ( not XOR2 ((XOR2 (a6,(AND2 (g7,a11)))),(XOR2 (z,(AND2 (g7,p))))) is empty implies not b7 is empty ) & ( not b6 is empty implies not XOR2 ((XOR2 (a5,(AND2 (g6,a11)))),(XOR2 (z,(AND2 (g6,p))))) is empty ) & ( not XOR2 ((XOR2 (a5,(AND2 (g6,a11)))),(XOR2 (z,(AND2 (g6,p))))) is empty implies not b6 is empty ) & ( not b5 is empty implies not XOR2 ((XOR2 (a4,(AND2 (g5,a11)))),(XOR2 (z,(AND2 (g5,p))))) is empty ) & ( not XOR2 ((XOR2 (a4,(AND2 (g5,a11)))),(XOR2 (z,(AND2 (g5,p))))) is empty implies not b5 is empty ) & ( not b4 is empty implies not XOR2 ((XOR2 (a3,(AND2 (g4,a11)))),(XOR2 (z,(AND2 (g4,p))))) is empty ) & ( not XOR2 ((XOR2 (a3,(AND2 (g4,a11)))),(XOR2 (z,(AND2 (g4,p))))) is empty implies not b4 is empty ) & ( not b3 is empty implies not XOR2 ((XOR2 (a2,(AND2 (g3,a11)))),(XOR2 (z,(AND2 (g3,p))))) is empty ) & ( not XOR2 ((XOR2 (a2,(AND2 (g3,a11)))),(XOR2 (z,(AND2 (g3,p))))) is empty implies not b3 is empty ) & ( not b2 is empty implies not XOR2 ((XOR2 (a1,(AND2 (g2,a11)))),(XOR2 (z,(AND2 (g2,p))))) is empty ) & ( not XOR2 ((XOR2 (a1,(AND2 (g2,a11)))),(XOR2 (z,(AND2 (g2,p))))) is empty implies not b2 is empty ) & ( not b1 is empty implies not XOR2 ((XOR2 (a0,(AND2 (g1,a11)))),(XOR2 (z,(AND2 (g1,p))))) is empty ) & ( not XOR2 ((XOR2 (a0,(AND2 (g1,a11)))),(XOR2 (z,(AND2 (g1,p))))) is empty implies not b1 is empty ) & ( not b0 is empty implies not XOR2 ((XOR2 (z,(AND2 (g0,a11)))),(XOR2 (z,(AND2 (g0,p))))) is empty ) & ( not XOR2 ((XOR2 (z,(AND2 (g0,a11)))),(XOR2 (z,(AND2 (g0,p))))) is empty implies not b0 is empty ) )

proof end;

:: Assumptions:
:: g0,g1,g2,...,g16: the coefficients of generator polynomial;
:: a0,a1,a2,...,a15: the present state of register;
:: p: input;
:: b0,b1,b2,...,b15: the state of register with input p;
:: A=(a15, a10, ..., a1, a0), B=(b11, b10, ..., b1,b0);
:: G=(g16,g15,g14,...,g1,g0)
:: A + B=(a15+b15, a14+b14, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or;
:: A*2= (a15, a14, ..., a1, a0)*2=(a15, a14, ..., a1, a0,0);
:: G*a15=(g16 is not empty & a15, g15 & a15, g14 & a15,...,g1 is not empty & a15, g0 is not empty & a15);
:: 2^15 means 2 to the 15th power.
::
:: In a CRC circuit, with assumption that A is the remainder of message M*2^15
:: divided by G, B which is the contents of register after one shift is expected
:: to be the remainder of (M*2 + p)*2^15 divided by G. That means
:: B= mod((M*2 + p)*2^15,G)
:: = mod(M*2^16+ p*2^15,G)
:: = mod(M*2^16,G) + mod(p*2^15,G)
:: = mod(A*2,G) + mod(p*2^15,G)
:: = (A*2+G*a15)+(p*2^15 + G*p);
::
:: Note: The initial state of register can be regarded as M=0.

theorem :: GATE_4:4

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, z, p being set st not g0 is empty & z is empty & ( not b0 is empty implies not XOR2 (p,a15) is empty ) & ( not XOR2 (p,a15) is empty implies not b0 is empty ) & ( not b1 is empty implies not XOR2 (a0,(AND2 (g1,b0))) is empty ) & ( not XOR2 (a0,(AND2 (g1,b0))) is empty implies not b1 is empty ) & ( not b2 is empty implies not XOR2 (a1,(AND2 (g2,b0))) is empty ) & ( not XOR2 (a1,(AND2 (g2,b0))) is empty implies not b2 is empty ) & ( not b3 is empty implies not XOR2 (a2,(AND2 (g3,b0))) is empty ) & ( not XOR2 (a2,(AND2 (g3,b0))) is empty implies not b3 is empty ) & ( not b4 is empty implies not XOR2 (a3,(AND2 (g4,b0))) is empty ) & ( not XOR2 (a3,(AND2 (g4,b0))) is empty implies not b4 is empty ) & ( not b5 is empty implies not XOR2 (a4,(AND2 (g5,b0))) is empty ) & ( not XOR2 (a4,(AND2 (g5,b0))) is empty implies not b5 is empty ) & ( not b6 is empty implies not XOR2 (a5,(AND2 (g6,b0))) is empty ) & ( not XOR2 (a5,(AND2 (g6,b0))) is empty implies not b6 is empty ) & ( not b7 is empty implies not XOR2 (a6,(AND2 (g7,b0))) is empty ) & ( not XOR2 (a6,(AND2 (g7,b0))) is empty implies not b7 is empty ) & ( not b8 is empty implies not XOR2 (a7,(AND2 (g8,b0))) is empty ) & ( not XOR2 (a7,(AND2 (g8,b0))) is empty implies not b8 is empty ) & ( not b9 is empty implies not XOR2 (a8,(AND2 (g9,b0))) is empty ) & ( not XOR2 (a8,(AND2 (g9,b0))) is empty implies not b9 is empty ) & ( not b10 is empty implies not XOR2 (a9,(AND2 (g10,b0))) is empty ) & ( not XOR2 (a9,(AND2 (g10,b0))) is empty implies not b10 is empty ) & ( not b11 is empty implies not XOR2 (a10,(AND2 (g11,b0))) is empty ) & ( not XOR2 (a10,(AND2 (g11,b0))) is empty implies not b11 is empty ) & ( not b12 is empty implies not XOR2 (a11,(AND2 (g12,b0))) is empty ) & ( not XOR2 (a11,(AND2 (g12,b0))) is empty implies not b12 is empty ) & ( not b13 is empty implies not XOR2 (a12,(AND2 (g13,b0))) is empty ) & ( not XOR2 (a12,(AND2 (g13,b0))) is empty implies not b13 is empty ) & ( not b14 is empty implies not XOR2 (a13,(AND2 (g14,b0))) is empty ) & ( not XOR2 (a13,(AND2 (g14,b0))) is empty implies not b14 is empty ) & ( not b15 is empty implies not XOR2 (a14,(AND2 (g15,b0))) is empty ) & ( not XOR2 (a14,(AND2 (g15,b0))) is empty implies not b15 is empty ) holds
( ( not b15 is empty implies not XOR2 ((XOR2 (a14,(AND2 (g15,a15)))),(XOR2 (z,(AND2 (g15,p))))) is empty ) & ( not XOR2 ((XOR2 (a14,(AND2 (g15,a15)))),(XOR2 (z,(AND2 (g15,p))))) is empty implies not b15 is empty ) & ( not b14 is empty implies not XOR2 ((XOR2 (a13,(AND2 (g14,a15)))),(XOR2 (z,(AND2 (g14,p))))) is empty ) & ( not XOR2 ((XOR2 (a13,(AND2 (g14,a15)))),(XOR2 (z,(AND2 (g14,p))))) is empty implies not b14 is empty ) & ( not b13 is empty implies not XOR2 ((XOR2 (a12,(AND2 (g13,a15)))),(XOR2 (z,(AND2 (g13,p))))) is empty ) & ( not XOR2 ((XOR2 (a12,(AND2 (g13,a15)))),(XOR2 (z,(AND2 (g13,p))))) is empty implies not b13 is empty ) & ( not b12 is empty implies not XOR2 ((XOR2 (a11,(AND2 (g12,a15)))),(XOR2 (z,(AND2 (g12,p))))) is empty ) & ( not XOR2 ((XOR2 (a11,(AND2 (g12,a15)))),(XOR2 (z,(AND2 (g12,p))))) is empty implies not b12 is empty ) & ( not b11 is empty implies not XOR2 ((XOR2 (a10,(AND2 (g11,a15)))),(XOR2 (z,(AND2 (g11,p))))) is empty ) & ( not XOR2 ((XOR2 (a10,(AND2 (g11,a15)))),(XOR2 (z,(AND2 (g11,p))))) is empty implies not b11 is empty ) & ( not b10 is empty implies not XOR2 ((XOR2 (a9,(AND2 (g10,a15)))),(XOR2 (z,(AND2 (g10,p))))) is empty ) & ( not XOR2 ((XOR2 (a9,(AND2 (g10,a15)))),(XOR2 (z,(AND2 (g10,p))))) is empty implies not b10 is empty ) & ( not b9 is empty implies not XOR2 ((XOR2 (a8,(AND2 (g9,a15)))),(XOR2 (z,(AND2 (g9,p))))) is empty ) & ( not XOR2 ((XOR2 (a8,(AND2 (g9,a15)))),(XOR2 (z,(AND2 (g9,p))))) is empty implies not b9 is empty ) & ( not b8 is empty implies not XOR2 ((XOR2 (a7,(AND2 (g8,a15)))),(XOR2 (z,(AND2 (g8,p))))) is empty ) & ( not XOR2 ((XOR2 (a7,(AND2 (g8,a15)))),(XOR2 (z,(AND2 (g8,p))))) is empty implies not b8 is empty ) & ( not b7 is empty implies not XOR2 ((XOR2 (a6,(AND2 (g7,a15)))),(XOR2 (z,(AND2 (g7,p))))) is empty ) & ( not XOR2 ((XOR2 (a6,(AND2 (g7,a15)))),(XOR2 (z,(AND2 (g7,p))))) is empty implies not b7 is empty ) & ( not b6 is empty implies not XOR2 ((XOR2 (a5,(AND2 (g6,a15)))),(XOR2 (z,(AND2 (g6,p))))) is empty ) & ( not XOR2 ((XOR2 (a5,(AND2 (g6,a15)))),(XOR2 (z,(AND2 (g6,p))))) is empty implies not b6 is empty ) & ( not b5 is empty implies not XOR2 ((XOR2 (a4,(AND2 (g5,a15)))),(XOR2 (z,(AND2 (g5,p))))) is empty ) & ( not XOR2 ((XOR2 (a4,(AND2 (g5,a15)))),(XOR2 (z,(AND2 (g5,p))))) is empty implies not b5 is empty ) & ( not b4 is empty implies not XOR2 ((XOR2 (a3,(AND2 (g4,a15)))),(XOR2 (z,(AND2 (g4,p))))) is empty ) & ( not XOR2 ((XOR2 (a3,(AND2 (g4,a15)))),(XOR2 (z,(AND2 (g4,p))))) is empty implies not b4 is empty ) & ( not b3 is empty implies not XOR2 ((XOR2 (a2,(AND2 (g3,a15)))),(XOR2 (z,(AND2 (g3,p))))) is empty ) & ( not XOR2 ((XOR2 (a2,(AND2 (g3,a15)))),(XOR2 (z,(AND2 (g3,p))))) is empty implies not b3 is empty ) & ( not b2 is empty implies not XOR2 ((XOR2 (a1,(AND2 (g2,a15)))),(XOR2 (z,(AND2 (g2,p))))) is empty ) & ( not XOR2 ((XOR2 (a1,(AND2 (g2,a15)))),(XOR2 (z,(AND2 (g2,p))))) is empty implies not b2 is empty ) & ( not b1 is empty implies not XOR2 ((XOR2 (a0,(AND2 (g1,a15)))),(XOR2 (z,(AND2 (g1,p))))) is empty ) & ( not XOR2 ((XOR2 (a0,(AND2 (g1,a15)))),(XOR2 (z,(AND2 (g1,p))))) is empty implies not b1 is empty ) & ( not b0 is empty implies not XOR2 ((XOR2 (z,(AND2 (g0,a15)))),(XOR2 (z,(AND2 (g0,p))))) is empty ) & ( not XOR2 ((XOR2 (z,(AND2 (g0,a15)))),(XOR2 (z,(AND2 (g0,p))))) is empty implies not b0 is empty ) )

proof end;