:: NORMFORM  semantic presentation begin  







definitionlet "A", "B" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )  ; let "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ); pred "x" :::"c="::: "y" means :: NORMFORM:def 1 (Bool  "("  (Bool (Set "x"  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_tarski :::"c="::: )  (Set "y"  ($#k2_domain_1 :::"`1"::: )  )) & (Bool (Set "x"  ($#k3_domain_1 :::"`2"::: )  )  ($#r1_tarski :::"c="::: )  (Set "y"  ($#k3_domain_1 :::"`2"::: )  ))  ")" ); reflexivity  
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ))  ")" ))
 ; func "x" :::"\/"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) equals :: NORMFORM:def 2 (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" "x"  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" "y"  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" "x"  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" "y"  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))
 ; idempotence  
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))
 ; func "x" :::"/\"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) equals :: NORMFORM:def 3 (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" "x"  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" "y"  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" "x"  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" "y"  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))
 ; idempotence  
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))
 ; func "x" :::"\"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) equals :: NORMFORM:def 4 (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" "x"  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k2_finsub_1 :::"\"::: )  (Set  "(" "y"  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" "x"  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k2_finsub_1 :::"\"::: )  (Set  "(" "y"  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ); func "x" :::"\+\"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) equals :: NORMFORM:def 5 (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" "x"  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" "y"  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" "x"  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" "y"  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))
 ; end; 







































:: deftheorem    defines :::"c="::: NORMFORM:def 1 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_normform :::"c="::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"\/"::: NORMFORM:def 2 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_normform :::"\/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); 
 
:: deftheorem    defines :::"/\"::: NORMFORM:def 3 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_normform :::"/\"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); 
 
:: deftheorem    defines :::"\"::: NORMFORM:def 4 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_normform :::"\"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k2_finsub_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k2_finsub_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); 
 
:: deftheorem    defines :::"\+\"::: NORMFORM:def 5 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_normform :::"\+\"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k4_finsub_1 :::"\+\"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); 
 








theorem :: NORMFORM:1 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) ; 
 
theorem :: NORMFORM:2 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "c"))))) ; 
 
theorem :: NORMFORM:3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")) ")" )  ($#k1_normform :::"\/"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set  "(" (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: NORMFORM:4 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_normform :::"/\"::: )  (Set (Var "b")) ")" )  ($#k2_normform :::"/\"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_normform :::"/\"::: )  (Set  "(" (Set (Var "b"))  ($#k2_normform :::"/\"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: NORMFORM:5 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_normform :::"/\"::: )  (Set  "(" (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_normform :::"/\"::: )  (Set (Var "b")) ")" )  ($#k1_normform :::"\/"::: )  (Set  "(" (Set (Var "a"))  ($#k2_normform :::"/\"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: NORMFORM:6 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set  "(" (Set (Var "b"))  ($#k2_normform :::"/\"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: NORMFORM:7 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_normform :::"/\"::: )  (Set  "(" (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: NORMFORM:8 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set  "(" (Set (Var "b"))  ($#k2_normform :::"/\"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")) ")" )  ($#k2_normform :::"/\"::: )  (Set  "(" (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: NORMFORM:9 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")))  ($#r1_normform :::"c="::: )  (Set (Var "c"))))) ; 
 
theorem :: NORMFORM:10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b"))))  ")" ))) ; 
 
theorem :: NORMFORM:11 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "a"))))) ; 
 
theorem :: NORMFORM:12 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k1_normform :::"\/"::: )  (Set (Var "a")))  ($#r1_normform :::"c="::: )  (Set (Set (Var "c"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")))  ($#r1_normform :::"c="::: )  (Set (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c"))))  ")" ))) ; 
 
theorem :: NORMFORM:13 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_normform :::"\"::: )  (Set (Var "b")) ")" )  ($#k1_normform :::"\/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")))))) ; 
 
theorem :: NORMFORM:14 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_normform :::"\"::: )  (Set (Var "b")))  ($#r1_normform :::"c="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")))))) ; 
 
theorem :: NORMFORM:15 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_finsub_1 :::"preBoolean"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_normform :::"\"::: )  (Set (Var "c")))  ($#r1_normform :::"c="::: )  (Set (Var "b"))))) ; 
 


definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; func  :::"FinPairUnion"::: "A" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "A" ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) means :: NORMFORM:def 6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "A" ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_normform :::"\/"::: )  (Set (Var "y"))))); end; 





:: deftheorem    defines :::"FinPairUnion"::: NORMFORM:def 6 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_normform :::"FinPairUnion"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_normform :::"\/"::: )  (Set (Var "y")))))  ")" ))); 
 


definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "A" be    ($#m1_hidden :::"set"::: )  ; let "B" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Const "X"))); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Const "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); func  :::"FinPairUnion":::  "(" "B" "," "f" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "A" ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: NORMFORM:def 7 (Set (Set  "("  ($#k5_normform :::"FinPairUnion"::: )  "A" ")" )  ($#k7_setwiseo :::"$$"::: )   "(" "B" "," "f" ")" ); end; 








:: deftheorem    defines :::"FinPairUnion"::: NORMFORM:def 7 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set   ($#k6_normform :::"FinPairUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_normform :::"FinPairUnion"::: )  (Set (Var "A")) ")" )  ($#k7_setwiseo :::"$$"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )))))); 
 registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_normform :::"FinPairUnion"::: )  "A") ->   ($#v1_binop_1 :::"commutative"::: )     ($#v2_binop_1 :::"associative"::: )     ($#v3_binop_1 :::"idempotent"::: )   ; 
end; 
theorem :: NORMFORM:16 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_normform :::"c="::: )  (Set   ($#k6_normform :::"FinPairUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))))))) ; 
 
theorem :: NORMFORM:17 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k1_setwiseo :::"{}."::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k1_setwiseo :::"{}."::: )  (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set   ($#k5_normform :::"FinPairUnion"::: )  (Set (Var "A"))))) ; 
 
theorem :: NORMFORM:18 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_normform :::"FinPairUnion"::: )  (Set (Var "A"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) ; 
 
theorem :: NORMFORM:19 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "("  ($#k5_normform :::"FinPairUnion"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k1_setwiseo :::"{}."::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k1_setwiseo :::"{}."::: )  (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) ))) ; 
 
theorem :: NORMFORM:20 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "("  ($#k5_normform :::"FinPairUnion"::: )  (Set (Var "A")) ")" ))  ($#r1_normform :::"c="::: )  (Set (Var "x"))))) ; 
 
theorem :: NORMFORM:21 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_normform :::"c="::: )  (Set (Var "c")))  ")" )) "holds"  (Bool (Set   ($#k6_normform :::"FinPairUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_normform :::"c="::: )  (Set (Var "c")))))))) ; 
 
theorem :: NORMFORM:22 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set   ($#k6_normform :::"FinPairUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_normform :::"FinPairUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"DISJOINT_PAIRS"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "X" ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: NORMFORM:def 8  "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "X" ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Set (Var "a"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "a"))  ($#k3_domain_1 :::"`2"::: )  ))  "}"  ; end; 





:: deftheorem    defines :::"DISJOINT_PAIRS"::: NORMFORM:def 8 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Set (Var "a"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "a"))  ($#k3_domain_1 :::"`2"::: )  ))  "}"  )); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: NORMFORM:23 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))) "iff" (Bool (Set (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ))  ")" ))) ; 
 








theorem :: NORMFORM:24 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "y"))  ($#k1_normform :::"\/"::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))) "iff" (Bool (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" )  ($#k5_setwiseo :::"\/"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  ")" )  ($#k3_finsub_1 :::"/\"::: )  (Set  "(" (Set (Var "y"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ))) ; 
 
theorem :: NORMFORM:25 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X"))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "a"))  ($#k3_domain_1 :::"`2"::: )  )))) ; 
 
theorem :: NORMFORM:26 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_normform :::"c="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "x")) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X"))))))) ; 
 
theorem :: NORMFORM:27 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "a"))  ($#k2_domain_1 :::"`1"::: )  )) "or"  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "a"))  ($#k3_domain_1 :::"`2"::: )  ))  ")" )))) ; 
 
theorem :: NORMFORM:28 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))  "st" (Bool (Bool (Bool  "not" (Set (Set (Var "a"))  ($#k1_normform :::"\/"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "st"  (Bool  "("  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "a"))  ($#k2_domain_1 :::"`1"::: )  )) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b"))  ($#k3_domain_1 :::"`2"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b"))  ($#k2_domain_1 :::"`1"::: )  )) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "a"))  ($#k3_domain_1 :::"`2"::: )  ))  ")" )  ")" )))) ; 
 
theorem :: NORMFORM:29 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "X")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k2_domain_1 :::"`1"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "x"))  ($#k3_domain_1 :::"`2"::: )  ))) "holds"  (Bool (Set (Var "x")) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))))) ; 
 
theorem :: NORMFORM:30 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "a"))  ($#k2_domain_1 :::"`1"::: )  )) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "a"))  ($#k3_domain_1 :::"`2"::: )  ))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "V")) "," (Set (Var "W")) ($#k4_tarski :::"]"::: ) ) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "X"))))))) ; 
 


















definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; func  :::"Normal_forms_on"::: "A" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A" ")" ) ")" ) equals :: NORMFORM:def 9  "{"  (Set (Var "B")) where B "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A" ")" )) : (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A")  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  "}"  ; end; 





:: deftheorem    defines :::"Normal_forms_on"::: NORMFORM:def 9 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "B")) where B "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) : (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  "}"  )); 
 registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k8_normform :::"Normal_forms_on"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 





theorem :: NORMFORM:31 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A"))))) ; 
 
theorem :: NORMFORM:32 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A")))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))))) ; 
 
theorem :: NORMFORM:33 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "a"))  ($#r1_normform :::"c="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) "holds"  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A")))))) ; 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; let "B" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Const "A")) ")" )); func  :::"mi"::: "B" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  "A") equals :: NORMFORM:def 10  "{"  (Set (Var "t")) where t "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A") : (Bool  "for" (Set (Var "s")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A") "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  "B") & (Bool (Set (Var "s"))  ($#r1_normform :::"c="::: )  (Set (Var "t")))  ")" ) "iff" (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Var "t")))  ")" ))  "}"  ; let "C" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Const "A")) ")" )); func "B" :::"^"::: "C" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A" ")" )) equals :: NORMFORM:def 11 (Set (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A" ")" )  ($#k8_subset_1 :::"/\"::: )   "{"  (Set  "(" (Set (Var "s"))  ($#k1_normform :::"\/"::: )  (Set (Var "t")) ")" ) where s, t "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  "A") : (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  "B") & (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  "C")  ")" )  "}"  ); end; 













:: deftheorem    defines :::"mi"::: NORMFORM:def 10 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "t")) where t "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A"))) : (Bool  "for" (Set (Var "s")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "s"))  ($#r1_normform :::"c="::: )  (Set (Var "t")))  ")" ) "iff" (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Var "t")))  ")" ))  "}"  ))); 
 
:: deftheorem    defines :::"^"::: NORMFORM:def 11 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )  ($#k8_subset_1 :::"/\"::: )   "{"  (Set  "(" (Set (Var "s"))  ($#k1_normform :::"\/"::: )  (Set (Var "t")) ")" ) where s, t "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A"))) : (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  "}"  )))); 
 
theorem :: NORMFORM:34 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C"))))) "holds"  (Bool  "ex" (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A"))) "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c"))))  ")" ))))) ; 
 
theorem :: NORMFORM:35 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "b"))  ($#k1_normform :::"\/"::: )  (Set (Var "c")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C"))))))) ; 
 
theorem :: NORMFORM:36 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) &  "("  (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "a")))) "implies" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"   ")" )))) ; 
 
theorem :: NORMFORM:37 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))))) ; 
 
theorem :: NORMFORM:38 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B")))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))))) ; 
 
theorem :: NORMFORM:39 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "b"))  ($#r1_normform :::"c="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B"))))))) ; 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "B" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "O" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "B")); let "a", "b" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Const "B")); :: original: :::"."::: redefine func "O" :::".":::  "(" "a" "," "b" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" "B"; end; 
theorem :: NORMFORM:40 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))))) ; 
 
theorem :: NORMFORM:41 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A"))) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r1_normform :::"c="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_normform :::"mi"::: )  (Set (Var "B"))))  ")" ))))) ; 
 
theorem :: NORMFORM:42 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "K")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A"))) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Var "K"))))) ; 
 
theorem :: NORMFORM:43 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k9_normform :::"mi"::: )  (Set (Var "B")) ")" )  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")))))) ; 
 
theorem :: NORMFORM:44 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set  "("  ($#k9_normform :::"mi"::: )  (Set (Var "B")) ")" )  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: NORMFORM:45 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k5_setwiseo :::"\/"::: )  (Set  "("  ($#k9_normform :::"mi"::: )  (Set (Var "C")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: NORMFORM:46 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))) "holds"  (Bool (Set (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "D")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k10_normform :::"^"::: )  (Set (Var "D")))))) ; 
 
theorem :: NORMFORM:47 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k9_normform :::"mi"::: )  (Set (Var "B")) ")" )  ($#k10_normform :::"^"::: )  (Set (Var "C")))))) ; 
 
theorem :: NORMFORM:48 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k10_normform :::"^"::: )  (Set (Var "B")))))) ; 
 
theorem :: NORMFORM:49 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" ))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))) "holds"  (Bool (Set (Set (Var "D"))  ($#k10_normform :::"^"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "D"))  ($#k10_normform :::"^"::: )  (Set (Var "C")))))) ; 
 
theorem :: NORMFORM:50 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set  "("  ($#k9_normform :::"mi"::: )  (Set (Var "B")) ")" )  ($#k10_normform :::"^"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: NORMFORM:51 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set  "("  ($#k9_normform :::"mi"::: )  (Set (Var "C")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: NORMFORM:52 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "K"))  ($#k10_normform :::"^"::: )  (Set  "(" (Set (Var "L"))  ($#k10_normform :::"^"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "K"))  ($#k10_normform :::"^"::: )  (Set (Var "L")) ")" )  ($#k10_normform :::"^"::: )  (Set (Var "M")))))) ; 
 
theorem :: NORMFORM:53 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "K"))  ($#k10_normform :::"^"::: )  (Set  "(" (Set (Var "L"))  ($#k5_setwiseo :::"\/"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "K"))  ($#k10_normform :::"^"::: )  (Set (Var "L")) ")" )  ($#k5_setwiseo :::"\/"::: )  (Set  "(" (Set (Var "K"))  ($#k10_normform :::"^"::: )  (Set (Var "M")) ")" ))))) ; 
 
theorem :: NORMFORM:54 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "("  ($#k7_normform :::"DISJOINT_PAIRS"::: )  (Set (Var "A")) ")" )) "holds"  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "B")))))) ; 
 
theorem :: NORMFORM:55 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "K")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A"))) "holds"  (Bool (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "K"))  ($#k10_normform :::"^"::: )  (Set (Var "K")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set (Var "K")))))) ; 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; func  :::"NormForm"::: "A" ->   ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   means :: NORMFORM:def 12 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k8_normform :::"Normal_forms_on"::: )  "A")) & (Bool  "("   "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  "A") "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")) ")" ))) & (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")) ")" )))  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"NormForm"::: NORMFORM:def 12 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_normform :::"NormForm"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A")))) & (Bool  "("   "for" (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_normform :::"Normal_forms_on"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k5_setwiseo :::"\/"::: )  (Set (Var "C")) ")" ))) & (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_normform :::"mi"::: )  (Set  "(" (Set (Var "B"))  ($#k10_normform :::"^"::: )  (Set (Var "C")) ")" )))  ")" )  ")" )  ")" )  ")" ))); 
 registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k12_normform :::"NormForm"::: )  "A") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattices :::"strict"::: )   ; 
end; 




registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k12_normform :::"NormForm"::: )  "A") ->   ($#v3_lattices :::"strict"::: )     ($#v10_lattices :::"Lattice-like"::: )   ; 
end; registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k12_normform :::"NormForm"::: )  "A") ->   ($#v3_lattices :::"strict"::: )     ($#v11_lattices :::"distributive"::: )     ($#v13_lattices :::"lower-bounded"::: )   ; 
end; 
theorem :: NORMFORM:56 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k12_normform :::"NormForm"::: )  (Set (Var "A")) ")" ))) ; 
 
theorem :: NORMFORM:57 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "("  ($#k12_normform :::"NormForm"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ;