begin
:: deftheorem Def1 defines Set-Constants CIRCUIT1:def 1 :
theorem
theorem Th2:
:: deftheorem defines -th_InputValues CIRCUIT1:def 2 :
theorem
canceled;
theorem
theorem
:: deftheorem defines depends_on_in CIRCUIT1:def 3 :
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
begin
defpred S1[ set ] means verum;
:: deftheorem Def4 defines size CIRCUIT1:def 4 :
theorem Th11:
theorem
theorem Th13:
theorem
:: deftheorem Def5 defines depth CIRCUIT1:def 5 :
theorem Th15:
theorem Th16:
theorem
begin
:: deftheorem Def6 defines depth CIRCUIT1:def 6 :
:: deftheorem Def7 defines depth CIRCUIT1:def 7 :
theorem
theorem Th19:
theorem