:: Correctness of Binary Counter Circuits
:: by Yuguang Yang , Wasaki Katsumi , Yasushi Fuwa and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users

begin

theorem :: GATE_2:1

for s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3 being set holds
not ( ( not s0 is empty implies not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND3 (NOT1 q3),(NOT1 q2),q1 is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND3 (NOT1 q3),q2,(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND3 (NOT1 q3),q2,q1 is empty ) & ( not AND3 (NOT1 q3),q2,q1 is empty implies not s3 is empty ) & ( not s4 is empty implies not AND3 q3,(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 q3,(NOT1 q2),(NOT1 q1) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND3 q3,(NOT1 q2),q1 is empty ) & ( not AND3 q3,(NOT1 q2),q1 is empty implies not s5 is empty ) & ( not s6 is empty implies not AND3 q3,q2,(NOT1 q1) is empty ) & ( not AND3 q3,q2,(NOT1 q1) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND3 q3,q2,q1 is empty ) & ( not AND3 q3,q2,q1 is empty implies not s7 is empty ) & ( not ns0 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND3 (NOT1 nq3),nq2,nq1 is empty ) & ( not AND3 (NOT1 nq3),nq2,nq1 is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND3 nq3,(NOT1 nq2),nq1 is empty ) & ( not AND3 nq3,(NOT1 nq2),nq1 is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND3 nq3,nq2,(NOT1 nq1) is empty ) & ( not AND3 nq3,nq2,(NOT1 nq1) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND3 nq3,nq2,nq1 is empty ) & ( not AND3 nq3,nq2,nq1 is empty implies not ns7 is empty ) & ( not nq1 is empty implies not NOT1 q1 is empty ) & ( not NOT1 q1 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not XOR2 q1,q2 is empty ) & ( not XOR2 q1,q2 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty ) & ( not OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) is empty implies not nq3 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns2 is empty ) & ( not ns3 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns3 is empty ) & ( not ns4 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns4 is empty ) & ( not ns5 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns5 is empty ) & ( not ns6 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns6 is empty ) & ( not ns7 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns7 is empty ) & ( not ns0 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns0 is empty ) ) )

proof end;

theorem :: GATE_2:2

for a, d, b, c being set holds
( not AND3 (AND2 a,d),(AND2 b,d),(AND2 c,d) is empty iff not AND2 (AND3 a,b,c),d is empty )

proof end;

theorem :: GATE_2:3

for a, b, c, d being set holds
( ( AND2 a,b is empty implies not OR2 (NOT1 a),(NOT1 b) is empty ) & ( not OR2 (NOT1 a),(NOT1 b) is empty implies AND2 a,b is empty ) & ( not OR2 a,b is empty & not OR2 c,b is empty implies not OR2 (AND2 a,c),b is empty ) & ( not OR2 (AND2 a,c),b is empty implies ( not OR2 a,b is empty & not OR2 c,b is empty ) ) & ( not OR2 a,b is empty & not OR2 c,b is empty & not OR2 d,b is empty implies not OR2 (AND3 a,c,d),b is empty ) & ( not OR2 (AND3 a,c,d),b is empty implies ( not OR2 a,b is empty & not OR2 c,b is empty & not OR2 d,b is empty ) ) & not ( not OR2 a,b is empty & ( not a is empty implies not c is empty ) & ( not c is empty implies not a is empty ) & OR2 c,b is empty ) )

proof end;

theorem :: GATE_2:4

for s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3, R being set holds
not ( ( not s0 is empty implies not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND3 (NOT1 q3),(NOT1 q2),q1 is empty ) & ( not AND3 (NOT1 q3),(NOT1 q2),q1 is empty implies not s1 is empty ) & ( not s2 is empty implies not AND3 (NOT1 q3),q2,(NOT1 q1) is empty ) & ( not AND3 (NOT1 q3),q2,(NOT1 q1) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND3 (NOT1 q3),q2,q1 is empty ) & ( not AND3 (NOT1 q3),q2,q1 is empty implies not s3 is empty ) & ( not s4 is empty implies not AND3 q3,(NOT1 q2),(NOT1 q1) is empty ) & ( not AND3 q3,(NOT1 q2),(NOT1 q1) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND3 q3,(NOT1 q2),q1 is empty ) & ( not AND3 q3,(NOT1 q2),q1 is empty implies not s5 is empty ) & ( not s6 is empty implies not AND3 q3,q2,(NOT1 q1) is empty ) & ( not AND3 q3,q2,(NOT1 q1) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND3 q3,q2,q1 is empty ) & ( not AND3 q3,q2,q1 is empty implies not s7 is empty ) & ( not ns0 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty ) & ( not AND3 (NOT1 nq3),(NOT1 nq2),nq1 is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty ) & ( not AND3 (NOT1 nq3),nq2,(NOT1 nq1) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND3 (NOT1 nq3),nq2,nq1 is empty ) & ( not AND3 (NOT1 nq3),nq2,nq1 is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty ) & ( not AND3 nq3,(NOT1 nq2),(NOT1 nq1) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND3 nq3,(NOT1 nq2),nq1 is empty ) & ( not AND3 nq3,(NOT1 nq2),nq1 is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND3 nq3,nq2,(NOT1 nq1) is empty ) & ( not AND3 nq3,nq2,(NOT1 nq1) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND3 nq3,nq2,nq1 is empty ) & ( not AND3 nq3,nq2,nq1 is empty implies not ns7 is empty ) & ( not nq1 is empty implies not AND2 (NOT1 q1),R is empty ) & ( not AND2 (NOT1 q1),R is empty implies not nq1 is empty ) & ( not nq2 is empty implies not AND2 (XOR2 q1,q2),R is empty ) & ( not AND2 (XOR2 q1,q2),R is empty implies not nq2 is empty ) & ( not nq3 is empty implies not AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),R is empty ) & ( not AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),R is empty implies not nq3 is empty ) & not ( ( not ns1 is empty implies not AND2 s0,R is empty ) & ( not AND2 s0,R is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND2 s1,R is empty ) & ( not AND2 s1,R is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND2 s2,R is empty ) & ( not AND2 s2,R is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND2 s3,R is empty ) & ( not AND2 s3,R is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND2 s4,R is empty ) & ( not AND2 s4,R is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND2 s5,R is empty ) & ( not AND2 s5,R is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND2 s6,R is empty ) & ( not AND2 s6,R is empty implies not ns7 is empty ) & ( not ns0 is empty implies not OR2 s7,(NOT1 R) is empty ) & ( not OR2 s7,(NOT1 R) is empty implies not ns0 is empty ) ) )

proof end;