:: HEYTING1 semantic presentation begin theorem :: HEYTING1:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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 "A")) "," (Set (Var "B")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B", "C" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "A"))); :: original: :::"c="::: redefine pred "B" :::"c="::: "C" means :: HEYTING1:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "C")); end; :: deftheorem defines :::"c="::: HEYTING1:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_heyting1 :::"c="::: ) (Set (Var "C"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ")" ))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Bool "not" (Set (Const "A")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; func :::"[":::"A":::"]"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: HEYTING1:def 2 "A"; end; :: deftheorem defines :::"["::: HEYTING1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k1_heyting1 :::"["::: ) (Set (Var "A")) ($#k1_heyting1 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "A")))); theorem :: HEYTING1:2 (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 (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k9_normform :::"mi"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_normform :::"Normal_forms_on"::: ) "A"); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Const "A"))); :: original: :::"{"::: redefine func :::"{":::"a":::"}"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_normform :::"Normal_forms_on"::: ) "A"); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Const "A")) ")" ); func :::"@"::: "u" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_normform :::"Normal_forms_on"::: ) "A") equals :: HEYTING1:def 3 "u"; end; :: deftheorem defines :::"@"::: HEYTING1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k3_heyting1 :::"@"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "u"))))); theorem :: HEYTING1:3 (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 (Var "K"))))) ; theorem :: HEYTING1:4 (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"))) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k8_normform :::"Normal_forms_on"::: ) (Set (Var "A"))))))) ; theorem :: HEYTING1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "u")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"Atom"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" )) means :: HEYTING1:def 4 (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_heyting1 :::"{"::: ) (Set (Var "a")) ($#k2_heyting1 :::"}"::: ) ))); end; :: deftheorem defines :::"Atom"::: HEYTING1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_heyting1 :::"{"::: ) (Set (Var "a")) ($#k2_heyting1 :::"}"::: ) ))) ")" ))); theorem :: HEYTING1:6 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: HEYTING1:7 (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"))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))))) ; theorem :: HEYTING1:8 (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"))) "holds" (Bool (Set (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))))) ; theorem :: HEYTING1:9 (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 ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "K")) "," (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "K")) "," (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) ")" ) ")" )))) ; theorem :: HEYTING1:10 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) "," (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ")" )))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"pair_diff"::: "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 :: HEYTING1:def 5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "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 "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_normform :::"\"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"pair_diff"::: HEYTING1:def 5 : (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_heyting1 :::"pair_diff"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "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 "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_normform :::"\"::: ) (Set (Var "b"))))) ")" ))); 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 :::"-"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" )) equals :: HEYTING1:def 6 (Set (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" ) ($#k8_subset_1 :::"/\"::: ) "{" (Set ($#k4_tarski :::"["::: ) "{" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")) ")" ) where t1 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A") : (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "t1")) ($#k3_domain_1 :::"`2"::: ) )) & (Bool (Set (Var "t1")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" "," "{" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")) ")" ) where t2 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A") : (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "t2")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Var "t2")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ($#k4_tarski :::"]"::: ) ) where g "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" ) "," (Set ($#k1_heyting1 :::"["::: ) "A" ($#k1_heyting1 :::"]"::: ) ) ")" ) : (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A") "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "s")) ($#k3_domain_1 :::"`2"::: ) ")" )))) "}" ); 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 :: HEYTING1:def 7 (Set (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" ) ($#k8_subset_1 :::"/\"::: ) "{" (Set "(" ($#k6_normform :::"FinPairUnion"::: ) "(" "B" "," (Set "(" (Set "(" ($#k5_heyting1 :::"pair_diff"::: ) "A" ")" ) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" ) ")" ) ")" ")" ) ")" ")" ) where f "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) "A" ")" ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "A" ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) : (Bool (Set (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) "B") ($#r1_tarski :::"c="::: ) "C") "}" ); end; :: deftheorem defines :::"-"::: HEYTING1:def 6 : (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 ($#k6_heyting1 :::"-"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) ($#k8_subset_1 :::"/\"::: ) "{" (Set ($#k4_tarski :::"["::: ) "{" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")) ")" ) where t1 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) : (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "t1")) ($#k3_domain_1 :::"`2"::: ) )) & (Bool (Set (Var "t1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" "," "{" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")) ")" ) where t2 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) : (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "t2")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Var "t2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" ($#k4_tarski :::"]"::: ) ) where g "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) "," (Set ($#k1_heyting1 :::"["::: ) (Set (Var "A")) ($#k1_heyting1 :::"]"::: ) ) ")" ) : (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "s")) ($#k3_domain_1 :::"`2"::: ) ")" )))) "}" )))); :: deftheorem defines :::"=>>"::: HEYTING1:def 7 : (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")) ($#k7_heyting1 :::"=>>"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) ($#k8_subset_1 :::"/\"::: ) "{" (Set "(" ($#k6_normform :::"FinPairUnion"::: ) "(" (Set (Var "B")) "," (Set "(" (Set "(" ($#k5_heyting1 :::"pair_diff"::: ) (Set (Var "A")) ")" ) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) ")" ) ")" ")" ) ")" ")" ) where f "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) : (Bool (Set (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) "}" )))); theorem :: HEYTING1:11 (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")) ")" )) (Bool "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k6_heyting1 :::"-"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) "," (Set ($#k1_heyting1 :::"["::: ) (Set (Var "A")) ($#k1_heyting1 :::"]"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "s")) ($#k3_domain_1 :::"`2"::: ) ")" ))) ")" ) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) "{" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")) ")" ) where t1 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) : (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "t1")) ($#k3_domain_1 :::"`2"::: ) )) & (Bool (Set (Var "t1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" "," "{" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")) ")" ) where t2 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) : (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "t2")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Var "t2")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" ($#k4_tarski :::"]"::: ) )) ")" ))))) ; theorem :: HEYTING1:12 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))))) ; theorem :: HEYTING1:13 (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"))) "st" (Bool (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_heyting1 :::"-"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: HEYTING1:14 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_normform :::"Normal_forms_on"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "K")) ($#k7_heyting1 :::"=>>"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: HEYTING1:15 (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ))) ; theorem :: HEYTING1:16 (Bool (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: HEYTING1:17 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_normform :::"Normal_forms_on"::: ) (Set (Var "A"))))) ; theorem :: HEYTING1:18 (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")) ")" )) (Bool "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k7_heyting1 :::"=>>"::: ) (Set (Var "C"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) "," (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")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_normform :::"FinPairUnion"::: ) "(" (Set (Var "B")) "," (Set "(" (Set "(" ($#k5_heyting1 :::"pair_diff"::: ) (Set (Var "A")) ")" ) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set "(" ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")) ")" ) ")" ) ")" ")" ) ")" )) ")" ))))) ; theorem :: HEYTING1:19 (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 "K")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_normform :::"Normal_forms_on"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "K")) ($#k10_normform :::"^"::: ) (Set ($#k2_heyting1 :::"{"::: ) (Set (Var "a")) ($#k2_heyting1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (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 ($#k6_heyting1 :::"-"::: ) (Set (Var "K")))) & (Bool (Set (Var "b")) ($#r1_normform :::"c="::: ) (Set (Var "a"))) ")" ))))) ; theorem :: HEYTING1:20 (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 "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "u")))) "holds" (Bool "ex" (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 "v"))) & (Bool (Set (Var "b")) ($#r1_normform :::"c="::: ) (Set (Set (Var "c")) ($#k1_normform :::"\/"::: ) (Set (Var "a")))) ")" )) ")" )) "holds" (Bool "ex" (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 (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) ($#k7_heyting1 :::"=>>"::: ) (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "v")) ")" ))) & (Bool (Set (Var "b")) ($#r1_normform :::"c="::: ) (Set (Var "a"))) ")" ))))) ; theorem :: HEYTING1:21 (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 (Set (Var "K")) ($#k10_normform :::"^"::: ) (Set "(" ($#k6_heyting1 :::"-"::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"pseudo_compl"::: "A" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" )) means :: HEYTING1:def 8 (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k9_normform :::"mi"::: ) (Set "(" ($#k6_heyting1 :::"-"::: ) (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) ")" )))); func :::"StrongImpl"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" )) means :: HEYTING1:def 9 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_normform :::"mi"::: ) (Set "(" (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) ($#k7_heyting1 :::"=>>"::: ) (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "v")) ")" ) ")" )))); let "u" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Const "A")) ")" ); func :::"SUB"::: "u" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" ))) equals :: HEYTING1:def 10 (Set ($#k1_zfmisc_1 :::"bool"::: ) "u"); func :::"diff"::: "u" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" )) means :: HEYTING1:def 11 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) "A" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "u" ($#k6_subset_1 :::"\"::: ) (Set (Var "v"))))); end; :: deftheorem defines :::"pseudo_compl"::: HEYTING1:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_heyting1 :::"pseudo_compl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k9_normform :::"mi"::: ) (Set "(" ($#k6_heyting1 :::"-"::: ) (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) ")" )))) ")" ))); :: deftheorem defines :::"StrongImpl"::: HEYTING1:def 9 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_heyting1 :::"StrongImpl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_normform :::"mi"::: ) (Set "(" (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) ($#k7_heyting1 :::"=>>"::: ) (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "v")) ")" ) ")" )))) ")" ))); :: deftheorem defines :::"SUB"::: HEYTING1:def 10 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k10_heyting1 :::"SUB"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "u")))))); :: deftheorem defines :::"diff"::: HEYTING1:def 11 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_heyting1 :::"diff"::: ) (Set (Var "u")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k6_subset_1 :::"\"::: ) (Set (Var "v"))))) ")" )))); theorem :: HEYTING1:22 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set "(" ($#k11_heyting1 :::"diff"::: ) (Set (Var "u")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r3_lattices :::"[="::: ) (Set (Var "u"))))) ; theorem :: HEYTING1:23 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "u")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" ($#k8_heyting1 :::"pseudo_compl"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ))))) ; theorem :: HEYTING1:24 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "u")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" ($#k9_heyting1 :::"StrongImpl"::: ) (Set (Var "A")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "v"))))) ; theorem :: HEYTING1:25 (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 "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set "(" ($#k3_heyting1 :::"@"::: ) (Set (Var "u")) ")" ) ($#k10_normform :::"^"::: ) (Set ($#k2_heyting1 :::"{"::: ) (Set (Var "a")) ($#k2_heyting1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Set "(" ($#k8_heyting1 :::"pseudo_compl"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))))))) ; theorem :: HEYTING1:26 (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 "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "st" (Bool (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 "u")))) "holds" (Bool (Set (Set (Var "b")) ($#k1_normform :::"\/"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_normform :::"DISJOINT_PAIRS"::: ) (Set (Var "A")))) ")" ) & (Bool (Set (Set (Var "u")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set "(" ($#k4_heyting1 :::"Atom"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Set "(" ($#k9_heyting1 :::"StrongImpl"::: ) (Set (Var "A")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ))))) ; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_normform :::"NormForm"::: ) "A") -> ($#v3_filter_0 :::"implicative"::: ) ; end; theorem :: HEYTING1:27 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "u")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set "(" ($#k10_heyting1 :::"SUB"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" )) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" ($#k8_heyting1 :::"pseudo_compl"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set "(" ($#k9_heyting1 :::"StrongImpl"::: ) (Set (Var "A")) ")" ) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k11_heyting1 :::"diff"::: ) (Set (Var "u")) ")" ) "," (Set (Var "v")) ")" ")" ) ")" ")" ) ")" )))) ; theorem :: HEYTING1:28 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k12_normform :::"NormForm"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ;