:: Preliminaries to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received November 17, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem :: PRE_CIRC:1
canceled;
theorem :: PRE_CIRC:2
theorem Th3: :: PRE_CIRC:3
theorem :: PRE_CIRC:4
theorem :: PRE_CIRC:5
:: deftheorem PRE_CIRC:def 1 :
canceled;
:: deftheorem PRE_CIRC:def 2 :
canceled;
:: deftheorem defines locally-finite PRE_CIRC:def 3 :
theorem Th6: :: PRE_CIRC:6
theorem Th7: :: PRE_CIRC:7
theorem :: PRE_CIRC:8
theorem :: PRE_CIRC:9
theorem :: PRE_CIRC:10
theorem :: PRE_CIRC:11
canceled;
theorem :: PRE_CIRC:12
theorem Th13: :: PRE_CIRC:13
theorem Th14: :: PRE_CIRC:14
theorem Th15: :: PRE_CIRC:15
theorem Th16: :: PRE_CIRC:16
theorem :: PRE_CIRC:17
theorem Th18: :: PRE_CIRC:18
theorem :: PRE_CIRC:19
theorem :: PRE_CIRC:20
theorem Th21: :: PRE_CIRC:21
theorem Th22: :: PRE_CIRC:22
theorem :: PRE_CIRC:23
theorem :: PRE_CIRC:24
theorem :: PRE_CIRC:25
theorem :: PRE_CIRC:26
theorem :: PRE_CIRC:27
theorem :: PRE_CIRC:28
canceled;
theorem :: PRE_CIRC:29