:: NORMFORM semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th4: :: NORMFORM:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th5: :: NORMFORM:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th10: :: NORMFORM:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th11: :: NORMFORM:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th12: :: NORMFORM:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th16: :: NORMFORM:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th20: :: NORMFORM:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th21: :: NORMFORM:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th22: :: NORMFORM:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th25: :: NORMFORM:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th26: :: NORMFORM:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th28: :: NORMFORM:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th36: :: NORMFORM:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th37: :: NORMFORM:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th38: :: NORMFORM:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th39: :: NORMFORM:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:40 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:41 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines DISJOINT_PAIRS NORMFORM:def 8 :
theorem Th42: :: NORMFORM:42 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:43 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:44 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th45: :: NORMFORM:45 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th46: :: NORMFORM:46 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:47 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:48 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:49 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:50 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 Th51: :: NORMFORM:51 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th52: :: NORMFORM:52 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th53: :: NORMFORM:53 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines mi NORMFORM:def 10 :
:: deftheorem defines ^ NORMFORM:def 11 :
theorem :: NORMFORM:54 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th55: :: NORMFORM:55 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th56: :: NORMFORM:56 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:57 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th58: :: NORMFORM:58 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:59 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:60 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th61: :: NORMFORM:61 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:63 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th64: :: NORMFORM:64 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th65: :: NORMFORM:65 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th66: :: NORMFORM:66 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th67: :: NORMFORM:67 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th68: :: NORMFORM:68 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:69 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th70: :: NORMFORM:70 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th72: :: NORMFORM:72 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th73: :: NORMFORM:73 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th74: :: NORMFORM:74 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th75: :: NORMFORM:75 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th76: :: NORMFORM:76 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th77: :: NORMFORM:77 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th79: :: NORMFORM:79 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:81 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:82 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:83 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:84 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: NORMFORM:85 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NORMFORM:86 :: Showing IDV graph ... (Click the Palm Tree again to close it)