:: On the Calculus of Binary Arithmetics
:: by Shunichi Kobayashi
::
:: Received August 23, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem BINARI_5:def 1 :
canceled;
:: deftheorem BINARI_5:def 2 :
canceled;
:: deftheorem defines <=> BINARI_5:def 3 :
theorem :: BINARI_5:1
theorem :: BINARI_5:2
theorem :: BINARI_5:3
theorem :: BINARI_5:4
theorem :: BINARI_5:5
theorem :: BINARI_5:6
theorem :: BINARI_5:7
theorem :: BINARI_5:8
canceled;
theorem :: BINARI_5:9
canceled;
theorem :: BINARI_5:10
theorem :: BINARI_5:11
theorem :: BINARI_5:12
theorem :: BINARI_5:13
theorem :: BINARI_5:14
theorem :: BINARI_5:15
canceled;
theorem :: BINARI_5:16
theorem :: BINARI_5:17
theorem :: BINARI_5:18
theorem :: BINARI_5:19
theorem :: BINARI_5:20
theorem :: BINARI_5:21
theorem :: BINARI_5:22
theorem :: BINARI_5:23
theorem :: BINARI_5:24
canceled;
theorem :: BINARI_5:25
canceled;
theorem :: BINARI_5:26
canceled;
theorem :: BINARI_5:27
canceled;
theorem :: BINARI_5:28
theorem :: BINARI_5:29
theorem :: BINARI_5:30
canceled;
theorem :: BINARI_5:31
canceled;
theorem :: BINARI_5:32
canceled;
theorem :: BINARI_5:33
canceled;
theorem :: BINARI_5:34
theorem :: BINARI_5:35
theorem :: BINARI_5:36
theorem :: BINARI_5:37
canceled;
theorem :: BINARI_5:38
canceled;
theorem :: BINARI_5:39
canceled;
theorem :: BINARI_5:40
canceled;
theorem :: BINARI_5:41
canceled;
theorem :: BINARI_5:42
canceled;
theorem :: BINARI_5:43
canceled;
theorem :: BINARI_5:44
canceled;
theorem :: BINARI_5:45
canceled;
theorem :: BINARI_5:46
canceled;
theorem :: BINARI_5:47
canceled;
theorem :: BINARI_5:48
canceled;
theorem :: BINARI_5:49
canceled;
theorem :: BINARI_5:50
canceled;
theorem :: BINARI_5:51
theorem :: BINARI_5:52
theorem :: BINARI_5:53