:: Introduction to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 15, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: deftheorem Def1 defines Set-Constants CIRCUIT1:def 1 :
theorem :: CIRCUIT1:1
theorem Th2: :: CIRCUIT1:2
:: deftheorem defines -th_InputValues CIRCUIT1:def 2 :
theorem :: CIRCUIT1:3
canceled;
theorem :: CIRCUIT1:4
theorem :: CIRCUIT1:5
:: deftheorem defines depends_on_in CIRCUIT1:def 3 :
theorem Th6: :: CIRCUIT1:6
theorem Th7: :: CIRCUIT1:7
theorem Th8: :: CIRCUIT1:8
theorem :: CIRCUIT1:9
theorem Th10: :: CIRCUIT1:10
defpred S1[ set ] means verum;
:: deftheorem Def4 defines size CIRCUIT1:def 4 :
theorem Th11: :: CIRCUIT1:11
theorem :: CIRCUIT1:12
theorem Th13: :: CIRCUIT1:13
theorem :: CIRCUIT1:14
:: deftheorem Def5 defines depth CIRCUIT1:def 5 :
theorem Th15: :: CIRCUIT1:15
theorem Th16: :: CIRCUIT1:16
theorem :: CIRCUIT1:17
:: deftheorem Def6 defines depth CIRCUIT1:def 6 :
:: deftheorem Def7 defines depth CIRCUIT1:def 7 :
theorem :: CIRCUIT1:18
theorem Th19: :: CIRCUIT1:19
theorem :: CIRCUIT1:20