:: Algebra of Normal Forms
:: by Andrzej Trybulec
::
:: Received October 5, 1990
:: Copyright (c) 1990 Association of Mizar Users
definition
let A,
B be non
empty preBoolean set ;
let x,
y be
Element of
[:A,B:];
pred x c= y means :: NORMFORM:def 1
(
x `1 c= y `1 &
x `2 c= y `2 );
reflexivity
for x being Element of [:A,B:] holds
( x `1 c= x `1 & x `2 c= x `2 )
;
func x \/ y -> Element of
[:A,B:] equals :: NORMFORM:def 2
[((x `1 ) \/ (y `1 )),((x `2 ) \/ (y `2 ))];
correctness
coherence
[((x `1 ) \/ (y `1 )),((x `2 ) \/ (y `2 ))] is Element of [:A,B:];
;
commutativity
for b1, x, y being Element of [:A,B:] st b1 = [((x `1 ) \/ (y `1 )),((x `2 ) \/ (y `2 ))] holds
b1 = [((y `1 ) \/ (x `1 )),((y `2 ) \/ (x `2 ))]
;
idempotence
for x being Element of [:A,B:] holds x = [((x `1 ) \/ (x `1 )),((x `2 ) \/ (x `2 ))]
by MCART_1:23;
func x /\ y -> Element of
[:A,B:] equals :: NORMFORM:def 3
[((x `1 ) /\ (y `1 )),((x `2 ) /\ (y `2 ))];
correctness
coherence
[((x `1 ) /\ (y `1 )),((x `2 ) /\ (y `2 ))] is Element of [:A,B:];
;
commutativity
for b1, x, y being Element of [:A,B:] st b1 = [((x `1 ) /\ (y `1 )),((x `2 ) /\ (y `2 ))] holds
b1 = [((y `1 ) /\ (x `1 )),((y `2 ) /\ (x `2 ))]
;
idempotence
for x being Element of [:A,B:] holds x = [((x `1 ) /\ (x `1 )),((x `2 ) /\ (x `2 ))]
by MCART_1:23;
func x \ y -> Element of
[:A,B:] equals :: NORMFORM:def 4
[((x `1 ) \ (y `1 )),((x `2 ) \ (y `2 ))];
correctness
coherence
[((x `1 ) \ (y `1 )),((x `2 ) \ (y `2 ))] is Element of [:A,B:];
;
func x \+\ y -> Element of
[:A,B:] equals :: NORMFORM:def 5
[((x `1 ) \+\ (y `1 )),((x `2 ) \+\ (y `2 ))];
correctness
coherence
[((x `1 ) \+\ (y `1 )),((x `2 ) \+\ (y `2 ))] is Element of [:A,B:];
;
commutativity
for b1, x, y being Element of [:A,B:] st b1 = [((x `1 ) \+\ (y `1 )),((x `2 ) \+\ (y `2 ))] holds
b1 = [((y `1 ) \+\ (x `1 )),((y `2 ) \+\ (x `2 ))]
;
end;
:: deftheorem defines c= NORMFORM:def 1 :
:: deftheorem defines \/ NORMFORM:def 2 :
:: deftheorem defines /\ NORMFORM:def 3 :
:: deftheorem defines \ NORMFORM:def 4 :
:: deftheorem defines \+\ NORMFORM:def 5 :
theorem :: NORMFORM:1
canceled;
theorem :: NORMFORM:2
canceled;
theorem :: NORMFORM:3
canceled;
theorem Th4: :: NORMFORM:4
theorem Th5: :: NORMFORM:5
theorem :: NORMFORM:6
canceled;
theorem :: NORMFORM:7
canceled;
theorem :: NORMFORM:8
canceled;
theorem :: NORMFORM:9
canceled;
theorem :: NORMFORM:10
canceled;
theorem :: NORMFORM:11
canceled;
theorem :: NORMFORM:12
canceled;
theorem :: NORMFORM:13
canceled;
theorem :: NORMFORM:14
canceled;
theorem :: NORMFORM:15
canceled;
theorem Th16: :: NORMFORM:16
theorem :: NORMFORM:17
canceled;
theorem :: NORMFORM:18
canceled;
theorem :: NORMFORM:19
theorem Th20: :: NORMFORM:20
theorem Th21: :: NORMFORM:21
theorem Th22: :: NORMFORM:22
theorem :: NORMFORM:23
canceled;
theorem :: NORMFORM:24
theorem Th25: :: NORMFORM:25
theorem Th26: :: NORMFORM:26
theorem :: NORMFORM:27
theorem Th28: :: NORMFORM:28
theorem :: NORMFORM:29
theorem :: NORMFORM:30
theorem :: NORMFORM:31
definition
let A be
set ;
func FinPairUnion A -> BinOp of
[:(Fin A),(Fin A):] means :
Def6:
:: NORMFORM:def 6
for
x,
y being
Element of
[:(Fin A),(Fin A):] holds
it . x,
y = x \/ y;
existence
ex b1 being BinOp of [:(Fin A),(Fin A):] st
for x, y being Element of [:(Fin A),(Fin A):] holds b1 . x,y = x \/ y
uniqueness
for b1, b2 being BinOp of [:(Fin A),(Fin A):] st ( for x, y being Element of [:(Fin A),(Fin A):] holds b1 . x,y = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds b2 . x,y = x \/ y ) holds
b1 = b2
end;
:: deftheorem Def6 defines FinPairUnion NORMFORM:def 6 :
:: deftheorem defines FinPairUnion NORMFORM:def 7 :
Lm1:
for A being set holds FinPairUnion A is idempotent
Lm2:
for A being set holds FinPairUnion A is commutative
Lm3:
for A being set holds FinPairUnion A is associative
theorem :: NORMFORM:32
canceled;
theorem :: NORMFORM:33
canceled;
theorem :: NORMFORM:34
canceled;
theorem :: NORMFORM:35
theorem Th36: :: NORMFORM:36
theorem Th37: :: NORMFORM:37
theorem Th38: :: NORMFORM:38
theorem Th39: :: NORMFORM:39
theorem :: NORMFORM:40
theorem :: NORMFORM:41
:: deftheorem defines DISJOINT_PAIRS NORMFORM:def 8 :
theorem Th42: :: NORMFORM:42
theorem :: NORMFORM:43
theorem :: NORMFORM:44
theorem Th45: :: NORMFORM:45
theorem Th46: :: NORMFORM:46
theorem :: NORMFORM:47
theorem :: NORMFORM:48
canceled;
theorem :: NORMFORM:49
theorem :: NORMFORM:50
Lm4:
for A being set holds {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b }
:: deftheorem defines Normal_forms_on NORMFORM:def 9 :
theorem :: NORMFORM:51
theorem Th52: :: NORMFORM:52
theorem Th53: :: NORMFORM:53
:: deftheorem defines mi NORMFORM:def 10 :
:: deftheorem defines ^ NORMFORM:def 11 :
theorem :: NORMFORM:54
canceled;
theorem Th55: :: NORMFORM:55
theorem Th56: :: NORMFORM:56
theorem :: NORMFORM:57
canceled;
theorem Th58: :: NORMFORM:58
theorem :: NORMFORM:59
theorem :: NORMFORM:60
theorem Th61: :: NORMFORM:61
Lm5:
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds
a in C ) holds
B c= C
theorem :: NORMFORM:62
canceled;
theorem :: NORMFORM:63
canceled;
theorem Th64: :: NORMFORM:64
theorem Th65: :: NORMFORM:65
theorem Th66: :: NORMFORM:66
theorem Th67: :: NORMFORM:67
theorem Th68: :: NORMFORM:68
theorem :: NORMFORM:69
theorem Th70: :: NORMFORM:70
Lm6:
for A being set
for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C )
theorem Th71: :: NORMFORM:71
theorem Th72: :: NORMFORM:72
theorem Th73: :: NORMFORM:73
theorem Th74: :: NORMFORM:74
theorem Th75: :: NORMFORM:75
theorem Th76: :: NORMFORM:76
theorem Th77: :: NORMFORM:77
Lm7:
for A being set
for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a )
Lm8:
for A being set
for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L
theorem Th78: :: NORMFORM:78
theorem Th79: :: NORMFORM:79
definition
let A be
set ;
canceled;canceled;func NormForm A -> strict LattStr means :
Def14:
:: NORMFORM:def 14
( the
carrier of
it = Normal_forms_on A & ( for
B,
C being
Element of
Normal_forms_on A holds
( the
L_join of
it . B,
C = mi (B \/ C) & the
L_meet of
it . B,
C = mi (B ^ C) ) ) );
existence
ex b1 being strict LattStr st
( the carrier of b1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b1 . B,C = mi (B \/ C) & the L_meet of b1 . B,C = mi (B ^ C) ) ) )
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b1 . B,C = mi (B \/ C) & the L_meet of b1 . B,C = mi (B ^ C) ) ) & the carrier of b2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b2 . B,C = mi (B \/ C) & the L_meet of b2 . B,C = mi (B ^ C) ) ) holds
b1 = b2
end;
:: deftheorem NORMFORM:def 12 :
canceled;
:: deftheorem NORMFORM:def 13 :
canceled;
:: deftheorem Def14 defines NormForm NORMFORM:def 14 :
Lm9:
for A being set
for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a
Lm10:
for A being set
for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
Lm11:
for A being set
for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),L = L
Lm12:
for A being set
for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b
Lm13:
for A being set
for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a
Lm14:
for A being set
for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
Lm15:
for A being set
for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . K,(the L_join of (NormForm A) . L,M) = the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),(the L_meet of (NormForm A) . K,M)
Lm16:
for A being set
for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a
theorem :: NORMFORM:80
canceled;
theorem :: NORMFORM:81
canceled;
theorem :: NORMFORM:82
canceled;
theorem :: NORMFORM:83
canceled;
theorem :: NORMFORM:84
canceled;
theorem :: NORMFORM:85
theorem :: NORMFORM:86