:: ARMSTRNG semantic presentation begin theorem :: ARMSTRNG:1 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"cap-closed"::: ) )) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "S"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: ARMSTRNG:2 (Bool "for" (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Var "X")) "," (Set (Var "R")))))) ; scheme :: ARMSTRNG:sch 1 SubsetSEq{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) "iff" (Bool P1[(Set (Var "y"))]) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) "iff" (Bool P1[(Set (Var "y"))]) ")" ) ")" )) "holds" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "X2")))) proof end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); func "R" :::"Maximal_in"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: ARMSTRNG:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) "X" "," "R") ")" )); end; :: deftheorem defines :::"Maximal_in"::: ARMSTRNG:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_armstrng :::"Maximal_in"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Var "X")) "," (Set (Var "R"))) ")" )) ")" )))); definitionlet "x", "X" be ($#m1_hidden :::"set"::: ) ; pred "x" :::"is_/\-irreducible_in"::: "X" means :: ARMSTRNG:def 2 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y")))) & (Bool (Bool "not" "x" ($#r1_hidden :::"="::: ) (Set (Var "z"))))) "holds" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ); end; :: deftheorem defines :::"is_/\-irreducible_in"::: ARMSTRNG:def 2 : (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_armstrng :::"is_/\-irreducible_in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ) ")" )); notationlet "x", "X" be ($#m1_hidden :::"set"::: ) ; antonym "x" :::"is_/\-reducible_in"::: "X" for "x" :::"is_/\-irreducible_in"::: "X"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"/\-IRR"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: ARMSTRNG:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r1_armstrng :::"is_/\-irreducible_in"::: ) "X") ")" )); end; :: deftheorem defines :::"/\-IRR"::: ARMSTRNG:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_armstrng :::"/\-IRR"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) ($#r1_armstrng :::"is_/\-irreducible_in"::: ) (Set (Var "X"))) ")" )) ")" ))); scheme :: ARMSTRNG:sch 2 FinIntersect{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "x"))])) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_armstrng :::"is_/\-irreducible_in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "x"))])) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))]) & (Bool P1[(Set (Var "y"))])) "holds" (Bool P1[(Set (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y")))])) proof end; theorem :: ARMSTRNG:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "s")) ($#r1_armstrng :::"is_/\-irreducible_in"::: ) (Set (Var "X"))) ")" ) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "B" is :::"(B1)"::: means :: ARMSTRNG:def 4 (Bool "X" ($#r2_hidden :::"in"::: ) "B"); end; :: deftheorem defines :::"(B1)"::: ARMSTRNG:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_armstrng :::"(B1)"::: ) ) "iff" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ))); notationlet "B" be ($#m1_hidden :::"set"::: ) ; synonym :::"(B2)"::: "B" for :::"cap-closed"::: ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v2_finsub_1 :::"(B2)"::: ) ($#v1_armstrng :::"(B1)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; theorem :: ARMSTRNG:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"cap-closed"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "x")) ($#r1_armstrng :::"is_/\-irreducible_in"::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; registrationlet "X", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2("X" "," (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D")) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "f" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p", "q" be ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func "p" :::"'&'"::: "q" -> ($#m2_finseq_1 :::"Tuple":::) "of" "n" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: ARMSTRNG:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" "q" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Const "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))))) ; end; :: deftheorem defines :::"'&'"::: ARMSTRNG:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_armstrng :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" )))) ")" ))); theorem :: ARMSTRNG:5 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_armstrng :::"'&'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: ARMSTRNG:6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_binarith :::"'not'"::: ) (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_armstrng :::"'&'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: ARMSTRNG:7 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; begin definitionattr "c1" is :::"strict"::: ; struct :::"DB-Rel"::: -> ; aggr :::"DB-Rel":::(# :::"Attributes":::, :::"Domains":::, :::"Relationship"::: #) -> ($#l1_armstrng :::"DB-Rel"::: ) ; sel :::"Attributes"::: "c1" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; sel :::"Domains"::: "c1" -> ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" "c1"); sel :::"Relationship"::: "c1" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "the" ($#u2_armstrng :::"Domains"::: ) "of" "c1") ")" ); end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Subset-Relation of "X" is ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ); mode Dependency-set of "X" is ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Dependencies"::: "X" -> ($#m1_subset_1 :::"Dependency-set":::) "of" "X" equals :: ARMSTRNG:def 6 (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k8_mcart_1 :::":]"::: ) ); end; :: deftheorem defines :::"Dependencies"::: ARMSTRNG:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_armstrng :::"Dependencies"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ($#k8_mcart_1 :::":]"::: ) ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Dependency of "X" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_armstrng :::"Dependencies"::: ) "X"); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_armstrng :::"Dependencies"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "F" -> ($#m1_subset_1 :::"Dependency":::) "of" "X"; end; theorem :: ARMSTRNG:8 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_armstrng :::"Dependencies"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ))) ")" )) ; theorem :: ARMSTRNG:9 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ))))) ; definitionlet "R" be ($#l1_armstrng :::"DB-Rel"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Const "R"))); pred "A" :::">|>"::: "B" "," "R" means :: ARMSTRNG:def 7 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u3_armstrng :::"Relationship"::: ) "of" "R") "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) "A") ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) "A"))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) "B") ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) "B"))); end; :: deftheorem defines :::">|>"::: ARMSTRNG:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_armstrng :::">|>"::: ) (Set (Var "B")) "," (Set (Var "R"))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u3_armstrng :::"Relationship"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))))) ")" ))); notationlet "R" be ($#l1_armstrng :::"DB-Rel"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Const "R"))); synonym "A" "," "B" :::"holds_in"::: "R" for "A" :::">|>"::: "B" "," "R"; end; definitionlet "R" be ($#l1_armstrng :::"DB-Rel"::: ) ; func :::"Dependency-str"::: "R" -> ($#m1_subset_1 :::"Dependency-set":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" "R") equals :: ARMSTRNG:def 8 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" "R") : (Bool (Set (Var "A")) ($#r2_armstrng :::">|>"::: ) (Set (Var "B")) "," "R") "}" ; end; :: deftheorem defines :::"Dependency-str"::: ARMSTRNG:def 8 : (Bool "for" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) "holds" (Bool (Set ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Var "R"))) : (Bool (Set (Var "A")) ($#r2_armstrng :::">|>"::: ) (Set (Var "B")) "," (Set (Var "R"))) "}" )); theorem :: ARMSTRNG:10 (Bool "for" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "A")) ($#r2_armstrng :::">|>"::: ) (Set (Var "B")) "," (Set (Var "R"))) ")" ))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "P", "Q" be ($#m1_subset_1 :::"Dependency":::) "of" (Set (Const "X")); pred "P" :::">="::: "Q" means :: ARMSTRNG:def 9 (Bool "(" (Bool (Set "P" ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set "Q" ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set "Q" ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set "P" ($#k2_xtuple_0 :::"`2"::: ) )) ")" ); reflexivity (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Const "X")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "P")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" )) ; end; :: deftheorem defines :::">="::: ARMSTRNG:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r3_armstrng :::">="::: ) (Set (Var "Q"))) "iff" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Q")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "Q")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ) ")" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "P", "Q" be ($#m1_subset_1 :::"Dependency":::) "of" (Set (Const "X")); synonym "Q" :::"<="::: "P" for "P" :::">="::: "Q"; synonym "P" :::"is_at_least_as_informative_as"::: "Q" for "P" :::">="::: "Q"; end; theorem :: ARMSTRNG:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) ($#r3_armstrng :::"<="::: ) (Set (Var "Q"))) & (Bool (Set (Var "Q")) ($#r3_armstrng :::"<="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))))) ; theorem :: ARMSTRNG:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) ($#r3_armstrng :::"<="::: ) (Set (Var "Q"))) & (Bool (Set (Var "Q")) ($#r3_armstrng :::"<="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "P")) ($#r3_armstrng :::"<="::: ) (Set (Var "S"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); :: original: :::"["::: redefine func :::"[":::"A" "," "B":::"]"::: -> ($#m1_subset_1 :::"Dependency":::) "of" "X"; end; theorem :: ARMSTRNG:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B9")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Dependencies-Order"::: "X" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k4_armstrng :::"Dependencies"::: ) "X" ")" ) equals :: ARMSTRNG:def 10 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k4_tarski :::"]"::: ) ) where P, Q "is" ($#m1_subset_1 :::"Dependency":::) "of" "X" : (Bool (Set (Var "P")) ($#r3_armstrng :::"<="::: ) (Set (Var "Q"))) "}" ; end; :: deftheorem defines :::"Dependencies-Order"::: ARMSTRNG:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_armstrng :::"Dependencies-Order"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k4_tarski :::"]"::: ) ) where P, Q "is" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Var "X")) : (Bool (Set (Var "P")) ($#r3_armstrng :::"<="::: ) (Set (Var "Q"))) "}" )); theorem :: ARMSTRNG:14 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_armstrng :::"Dependencies-Order"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "P")) ($#r3_armstrng :::"<="::: ) (Set (Var "Q"))) ")" )) ")" )) ; theorem :: ARMSTRNG:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_armstrng :::"Dependencies-Order"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ($#k8_mcart_1 :::":]"::: ) ))) ; theorem :: ARMSTRNG:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k7_armstrng :::"Dependencies-Order"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ($#k8_mcart_1 :::":]"::: ) ))) ; theorem :: ARMSTRNG:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" ($#k7_armstrng :::"Dependencies-Order"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ($#k8_mcart_1 :::":]"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_armstrng :::"Dependencies-Order"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k7_armstrng :::"Dependencies-Order"::: ) "X") -> ($#v1_partfun1 :::"total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); synonym :::"(F2)"::: "F" for :::"transitive"::: ; synonym :::"(DC1)"::: "F" for :::"transitive"::: ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); attr "F" is :::"(F1)"::: means :: ARMSTRNG:def 11 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"(F1)"::: ARMSTRNG:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); synonym :::"(DC2)"::: "F" for :::"(F1)"::: ; end; theorem :: ARMSTRNG:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); attr "F" is :::"(F3)"::: means :: ARMSTRNG:def 12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); attr "F" is :::"(F4)"::: means :: ARMSTRNG:def 13 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A9")) ")" ) "," (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B9")) ")" ) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"(F3)"::: ARMSTRNG:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); :: deftheorem defines :::"(F4)"::: ARMSTRNG:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_armstrng :::"(F4)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A9")) ")" ) "," (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B9")) ")" ) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); theorem :: ARMSTRNG:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_armstrng :::"Dependencies"::: ) (Set (Var "X"))) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set ($#k4_armstrng :::"Dependencies"::: ) (Set (Var "X"))) "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool (Set ($#k4_armstrng :::"Dependencies"::: ) (Set (Var "X"))) "is" ($#v4_armstrng :::"(F3)"::: ) ) & (Bool (Set ($#k4_armstrng :::"Dependencies"::: ) (Set (Var "X"))) "is" ($#v5_armstrng :::"(F4)"::: ) ) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v5_relat_1 :::"-valued"::: ) ($#v8_relat_2 :::"(F2)"::: ) ($#v3_armstrng :::"(F1)"::: ) ($#v4_armstrng :::"(F3)"::: ) ($#v5_armstrng :::"(F4)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); attr "F" is :::"full_family"::: means :: ARMSTRNG:def 14 (Bool "(" (Bool "F" "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool "F" "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool "F" "is" ($#v4_armstrng :::"(F3)"::: ) ) & (Bool "F" "is" ($#v5_armstrng :::"(F4)"::: ) ) ")" ); end; :: deftheorem defines :::"full_family"::: ARMSTRNG:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_armstrng :::"full_family"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_armstrng :::"(F4)"::: ) ) ")" ) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v5_relat_1 :::"-valued"::: ) ($#v6_armstrng :::"full_family"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Full-family of "X" is ($#v6_armstrng :::"full_family"::: ) ($#m1_subset_1 :::"Dependency-set":::) "of" "X"; end; theorem :: ARMSTRNG:20 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) ($#v6_armstrng :::"full_family"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v6_armstrng :::"full_family"::: ) -> ($#v8_relat_2 :::"(F2)"::: ) ($#v3_armstrng :::"(F1)"::: ) ($#v4_armstrng :::"(F3)"::: ) ($#v5_armstrng :::"(F4)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v8_relat_2 :::"(F2)"::: ) ($#v3_armstrng :::"(F1)"::: ) ($#v4_armstrng :::"(F3)"::: ) ($#v5_armstrng :::"(F4)"::: ) -> ($#v6_armstrng :::"full_family"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); attr "F" is :::"(DC3)"::: means :: ARMSTRNG:def 15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"(DC3)"::: ARMSTRNG:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v7_armstrng :::"(DC3)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v3_armstrng :::"(F1)"::: ) ($#v4_armstrng :::"(F3)"::: ) -> ($#v7_armstrng :::"(DC3)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v8_relat_2 :::"(F2)"::: ) ($#v7_armstrng :::"(DC3)"::: ) -> ($#v3_armstrng :::"(F1)"::: ) ($#v4_armstrng :::"(F3)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v5_relat_1 :::"-valued"::: ) ($#v8_relat_2 :::"(F2)"::: ) ($#v5_armstrng :::"(F4)"::: ) ($#v7_armstrng :::"(DC3)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: ARMSTRNG:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v7_armstrng :::"(DC3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) ) ")" ))) ; theorem :: ARMSTRNG:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v7_armstrng :::"(DC3)"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v3_armstrng :::"(F1)"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: ARMSTRNG:23 (Bool "for" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) "holds" (Bool (Set ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R"))) "is" ($#v6_armstrng :::"full_family"::: ) )) ; theorem :: ARMSTRNG:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) "}" "is" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X"))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); func :::"Maximal_wrt"::: "F" -> ($#m1_subset_1 :::"Dependency-set":::) "of" "X" equals :: ARMSTRNG:def 16 (Set (Set "(" ($#k7_armstrng :::"Dependencies-Order"::: ) "X" ")" ) ($#k1_armstrng :::"Maximal_in"::: ) "F"); end; :: deftheorem defines :::"Maximal_wrt"::: ARMSTRNG:def 16 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_armstrng :::"Dependencies-Order"::: ) (Set (Var "X")) ")" ) ($#k1_armstrng :::"Maximal_in"::: ) (Set (Var "F")))))); theorem :: ARMSTRNG:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "F"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; pred "x" :::"^|^"::: "y" "," "F" means :: ARMSTRNG:def 17 (Bool (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) "F")); end; :: deftheorem defines :::"^|^"::: ARMSTRNG:def 17 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r4_armstrng :::"^|^"::: ) (Set (Var "y")) "," (Set (Var "F"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F")))) ")" )))); theorem :: ARMSTRNG:26 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Dependency":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F")))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set (Var "P"))) ")" ))))) ; theorem :: ARMSTRNG:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r4_armstrng :::"^|^"::: ) (Set (Var "B")) "," (Set (Var "F"))) "iff" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "or" (Bool "(" (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "A9")))) & (Bool (Bool "not" (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "B9")))) ")" ) "or" "not" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::"<="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) )) ")" ) ")" ) ")" ) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); attr "M" is :::"(M1)"::: means :: ARMSTRNG:def 18 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k6_armstrng :::"]"::: ) )) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "M") ")" ))); attr "M" is :::"(M2)"::: means :: ARMSTRNG:def 19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) ")" )); attr "M" is :::"(M3)"::: means :: ARMSTRNG:def 20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set (Var "A9")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B9")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))); end; :: deftheorem defines :::"(M1)"::: ARMSTRNG:def 18 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v8_armstrng :::"(M1)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k6_armstrng :::"]"::: ) )) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) ")" ))) ")" ))); :: deftheorem defines :::"(M2)"::: ARMSTRNG:def 19 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v9_armstrng :::"(M2)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) ")" )) ")" ))); :: deftheorem defines :::"(M3)"::: ARMSTRNG:def 20 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v10_armstrng :::"(M3)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "A9")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B9")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) ")" ))); theorem :: ARMSTRNG:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F"))) "is" ($#v8_armstrng :::"(M1)"::: ) ) & (Bool (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F"))) "is" ($#v9_armstrng :::"(M2)"::: ) ) & (Bool (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F"))) "is" ($#v10_armstrng :::"(M3)"::: ) ) ")" ))) ; theorem :: ARMSTRNG:29 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v8_armstrng :::"(M1)"::: ) ) & (Bool (Set (Var "M")) "is" ($#v9_armstrng :::"(M2)"::: ) ) & (Bool (Set (Var "M")) "is" ($#v10_armstrng :::"(M3)"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r3_armstrng :::">="::: ) (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) )) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A9")) "," (Set (Var "B9")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) ")" )) "}" )) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_relset_1 :::"="::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) "is" ($#v6_armstrng :::"full_family"::: ) ) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r2_relset_1 :::"="::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "G")) ($#r2_relset_1 :::"="::: ) (Set (Var "F"))) ")" ) ")" ))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Full-family":::) "of" (Set (Const "X")); cluster (Set ($#k8_armstrng :::"Maximal_wrt"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ARMSTRNG:30 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) "}" )) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "K")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k6_armstrng :::"]"::: ) ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Bool "not" (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F"))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); func :::"saturated-subsets"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" equals :: ARMSTRNG:def 21 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Set (Var "A")) ($#r4_armstrng :::"^|^"::: ) (Set (Var "B")) "," "F")) "}" ; end; :: deftheorem defines :::"saturated-subsets"::: ARMSTRNG:def 21 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "A")) ($#r4_armstrng :::"^|^"::: ) (Set (Var "B")) "," (Set (Var "F")))) "}" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); synonym :::"closed_attribute_subset"::: "F" for :::"saturated-subsets"::: "F"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); cluster (Set ($#k9_armstrng :::"saturated-subsets"::: ) "F") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: ARMSTRNG:31 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r4_armstrng :::"^|^"::: ) (Set (Var "B")) "," (Set (Var "F"))) ")" )) ")" ))) ; theorem :: ARMSTRNG:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F"))) "is" ($#v1_armstrng :::"(B1)"::: ) ) & (Bool (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F"))) "is" ($#v2_finsub_1 :::"(B2)"::: ) ) ")" ))) ; definitionlet "X", "B" be ($#m1_hidden :::"set"::: ) ; func "X" :::"deps_encl_by"::: "B" -> ($#m1_subset_1 :::"Dependency-set":::) "of" "X" equals :: ARMSTRNG:def 22 "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k6_armstrng :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "c")))) "}" ; end; :: deftheorem defines :::"deps_encl_by"::: ARMSTRNG:def 22 : (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k6_armstrng :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "c")))) "}" )); theorem :: ARMSTRNG:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "B"))) "is" ($#v6_armstrng :::"full_family"::: ) )))) ; theorem :: ARMSTRNG:34 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set "(" (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "B")) ")" ))))) ; theorem :: ARMSTRNG:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_armstrng :::"(B1)"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"(B2)"::: ) )) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set "(" (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "B")) ")" ))) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "G")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "B")))) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); func :::"enclosure_of"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" equals :: ARMSTRNG:def 23 "{" (Set (Var "b")) where b "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "}" ; end; :: deftheorem defines :::"enclosure_of"::: ARMSTRNG:def 23 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k11_armstrng :::"enclosure_of"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "b")) where b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "}" ))); theorem :: ARMSTRNG:36 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k11_armstrng :::"enclosure_of"::: ) (Set (Var "F"))) "is" ($#v1_armstrng :::"(B1)"::: ) ) & (Bool (Set ($#k11_armstrng :::"enclosure_of"::: ) (Set (Var "F"))) "is" ($#v2_finsub_1 :::"(B2)"::: ) ) ")" ))) ; theorem :: ARMSTRNG:37 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set "(" ($#k11_armstrng :::"enclosure_of"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_relset_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v6_armstrng :::"full_family"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set "(" ($#k11_armstrng :::"enclosure_of"::: ) (Set (Var "F")) ")" )) ($#r1_relset_1 :::"c="::: ) (Set (Var "G"))) ")" ) ")" ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); func :::"Dependency-closure"::: "F" -> ($#m1_subset_1 :::"Full-family":::) "of" "X" means :: ARMSTRNG:def 24 (Bool "(" (Bool "F" ($#r1_relset_1 :::"c="::: ) it) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" "X" "st" (Bool (Bool "F" ($#r1_relset_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v6_armstrng :::"full_family"::: ) )) "holds" (Bool it ($#r1_relset_1 :::"c="::: ) (Set (Var "G"))) ")" ) ")" ); end; :: deftheorem defines :::"Dependency-closure"::: ARMSTRNG:def 24 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_relset_1 :::"c="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_relset_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v6_armstrng :::"full_family"::: ) )) "holds" (Bool (Set (Var "b3")) ($#r1_relset_1 :::"c="::: ) (Set (Var "G"))) ")" ) ")" ) ")" )))); theorem :: ARMSTRNG:38 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set "(" ($#k11_armstrng :::"enclosure_of"::: ) (Set (Var "F")) ")" ))))) ; theorem :: ARMSTRNG:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Bool "not" (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "}" ))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_armstrng :::"(B1)"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"(B2)"::: ) ) ")" )))) ; theorem :: ARMSTRNG:40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) "}" )) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Bool "not" (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F"))))))) ; theorem :: ARMSTRNG:41 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) "}" )) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Bool "not" (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F"))))))) ; definitionlet "X", "G" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); pred "G" :::"is_generator-set_of"::: "B" means :: ARMSTRNG:def 25 (Bool "(" (Bool "G" ($#r1_tarski :::"c="::: ) "B") & (Bool "B" ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "S")) ")" ) where S "is" ($#m1_subset_1 :::"Subset-Family":::) "of" "X" : (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) "G") "}" ) ")" ); end; :: deftheorem defines :::"is_generator-set_of"::: ARMSTRNG:def 25 : (Bool "for" (Set (Var "X")) "," (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r5_armstrng :::"is_generator-set_of"::: ) (Set (Var "B"))) "iff" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "S")) ")" ) where S "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) : (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) "}" ) ")" ) ")" ))); theorem :: ARMSTRNG:42 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "G")) ($#r5_armstrng :::"is_generator-set_of"::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set "(" (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "G")) ")" ))))) ; theorem :: ARMSTRNG:43 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r5_armstrng :::"is_generator-set_of"::: ) (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "G")))) ")" )))) ; theorem :: ARMSTRNG:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_armstrng :::"(B1)"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"(B2)"::: ) )) "holds" (Bool (Set ($#k2_armstrng :::"/\-IRR"::: ) (Set (Var "B"))) ($#r5_armstrng :::"is_generator-set_of"::: ) (Set (Var "B"))))) ; theorem :: ARMSTRNG:45 (Bool "for" (Set (Var "X")) "," (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_armstrng :::"(B1)"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"(B2)"::: ) ) & (Bool (Set (Var "G")) ($#r5_armstrng :::"is_generator-set_of"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_armstrng :::"/\-IRR"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))))) ; begin definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode Tuple of "n" "," "D" is ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; theorem :: ARMSTRNG:46 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) "st" (Bool "(" (Bool (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "the" ($#u2_armstrng :::"Domains"::: ) "of" (Set (Var "R"))) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) )) ")" ) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R")))) ")" )))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); func :::"candidate-keys"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" equals :: ARMSTRNG:def 26 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," "X" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) "F")) "}" ; end; :: deftheorem defines :::"candidate-keys"::: ARMSTRNG:def 26 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_armstrng :::"Maximal_wrt"::: ) (Set (Var "F")))) "}" ))); theorem :: ARMSTRNG:47 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) "}" )) "holds" (Bool (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "K")) ($#k1_tarski :::"}"::: ) ))))) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; antonym :::"(C1)"::: "X" for :::"empty"::: ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"without_proper_subsets"::: means :: ARMSTRNG:def 27 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"without_proper_subsets"::: ARMSTRNG:def 27 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v11_armstrng :::"without_proper_subsets"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"(C2)"::: "X" for :::"without_proper_subsets"::: ; end; theorem :: ARMSTRNG:48 (Bool "for" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) "holds" (Bool "(" (Bool (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set "(" ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R")) ")" )) "is" ($#v1_xboole_0 :::"(C1)"::: ) ) & (Bool (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set "(" ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R")) ")" )) "is" ($#v11_armstrng :::"(C2)"::: ) ) ")" )) ; theorem :: ARMSTRNG:49 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v1_xboole_0 :::"(C1)"::: ) ) & (Bool (Set (Var "C")) "is" ($#v11_armstrng :::"(C2)"::: ) )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Full-family":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set (Var "F"))))))) ; theorem :: ARMSTRNG:50 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) "is" ($#v1_xboole_0 :::"(C1)"::: ) ) & (Bool (Set (Var "C")) "is" ($#v11_armstrng :::"(C2)"::: ) ) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set (Var "b")) where b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "not" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))))) "}" )) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set "(" (Set (Var "X")) ($#k10_armstrng :::"deps_encl_by"::: ) (Set (Var "B")) ")" )))))) ; theorem :: ARMSTRNG:51 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v1_xboole_0 :::"(C1)"::: ) ) & (Bool (Set (Var "C")) "is" ($#v11_armstrng :::"(C2)"::: ) )) "holds" (Bool "ex" (Set (Var "R")) "being" ($#l1_armstrng :::"DB-Rel"::: ) "st" (Bool "(" (Bool (Set "the" ($#u1_armstrng :::"Attributes"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set "(" ($#k5_armstrng :::"Dependency-str"::: ) (Set (Var "R")) ")" ))) ")" )))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); attr "F" is :::"(DC4)"::: means :: ARMSTRNG:def 28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); attr "F" is :::"(DC5)"::: means :: ARMSTRNG:def 29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) "," (Set (Var "D")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) "," (Set (Var "D")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); attr "F" is :::"(DC6)"::: means :: ARMSTRNG:def 30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"(DC4)"::: ARMSTRNG:def 28 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v12_armstrng :::"(DC4)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); :: deftheorem defines :::"(DC5)"::: ARMSTRNG:def 29 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v13_armstrng :::"(DC5)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) "," (Set (Var "D")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) "," (Set (Var "D")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); :: deftheorem defines :::"(DC6)"::: ARMSTRNG:def 30 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v14_armstrng :::"(DC6)"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k6_armstrng :::"["::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); theorem :: ARMSTRNG:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_armstrng :::"(F4)"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_armstrng :::"(DC3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_armstrng :::"(F4)"::: ) ) ")" ) ")" ))) ; theorem :: ARMSTRNG:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_armstrng :::"(F4)"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(DC1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_armstrng :::"(DC3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v12_armstrng :::"(DC4)"::: ) ) ")" ) ")" ))) ; theorem :: ARMSTRNG:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(F1)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v8_relat_2 :::"(F2)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_armstrng :::"(F3)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_armstrng :::"(F4)"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_armstrng :::"(DC2)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v13_armstrng :::"(DC5)"::: ) ) & (Bool (Set (Var "F")) "is" ($#v14_armstrng :::"(DC6)"::: ) ) ")" ) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "X")); func :::"charact_set"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: ARMSTRNG:def 31 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" )) "}" ; end; :: deftheorem defines :::"charact_set"::: ARMSTRNG:def 31 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" )) "}" ))); theorem :: ARMSTRNG:55 (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" )) ")" ))) ; theorem :: ARMSTRNG:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" ))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))))))) ; theorem :: ARMSTRNG:57 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k6_armstrng :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_armstrng :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))))) ")" ) ")" ) & (Bool (Set ($#k9_armstrng :::"saturated-subsets"::: ) (Set "(" ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F")) ")" ))) ")" ))) ; theorem :: ARMSTRNG:58 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F"))) ($#r2_relset_1 :::"="::: ) (Set ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "G")))))) ; theorem :: ARMSTRNG:59 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set "(" ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F")) ")" ))))) ; definitionlet "A", "K" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Const "A")); pred "K" :::"is_p_i_w_ncv_of"::: "F" means :: ARMSTRNG:def 32 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" "A" "st" (Bool (Bool "K" ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) "A")) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) "F")) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r2_xboole_0 :::"c<"::: ) "K")) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" "A" "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) "A") & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) "F"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"is_p_i_w_ncv_of"::: ARMSTRNG:def 32 : (Bool "for" (Set (Var "A")) "," (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "K")) ($#r6_armstrng :::"is_p_i_w_ncv_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F")))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "K")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k14_armstrng :::"charact_set"::: ) (Set (Var "F"))))) ")" )) ")" ) ")" ) ")" ))); theorem :: ARMSTRNG:60 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Dependency-set":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k13_armstrng :::"candidate-keys"::: ) (Set "(" ($#k12_armstrng :::"Dependency-closure"::: ) (Set (Var "F")) ")" ))) "iff" (Bool (Set (Var "K")) ($#r6_armstrng :::"is_p_i_w_ncv_of"::: ) (Set (Var "F"))) ")" )))) ;