:: Propositional Calculus for Boolean Valued Functions, VI
:: by Shunichi Kobayashi
::
:: Received July 14, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: BVFUNC10:1
Lm1:
for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))
theorem :: BVFUNC10:2
Lm2:
for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
theorem :: BVFUNC10:3
theorem :: BVFUNC10:4
theorem :: BVFUNC10:5
theorem :: BVFUNC10:6
Lm3:
for Y being non empty set
for a1, a2, b1, b2 being Element of Funcs Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
theorem :: BVFUNC10:7
theorem :: BVFUNC10:8
theorem :: BVFUNC10:9
theorem :: BVFUNC10:10
theorem :: BVFUNC10:11
theorem :: BVFUNC10:12
theorem :: BVFUNC10:13
theorem :: BVFUNC10:14
theorem :: BVFUNC10:15
Lm4:
for Y being non empty set
for a, b, c being Element of Funcs Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))
theorem :: BVFUNC10:16
theorem :: BVFUNC10:17
theorem :: BVFUNC10:18
theorem Th19: :: BVFUNC10:19
theorem Th20: :: BVFUNC10:20
theorem Th21: :: BVFUNC10:21
theorem Th22: :: BVFUNC10:22
theorem :: BVFUNC10:23
theorem :: BVFUNC10:24
theorem :: BVFUNC10:25
theorem :: BVFUNC10:26
theorem :: BVFUNC10:27