:: HEYTING2 semantic presentation begin theorem :: HEYTING2:1 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::))) ; begin theorem :: HEYTING2:2 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )))) ; theorem :: HEYTING2:3 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) ")" ))))) ; theorem :: HEYTING2:4 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) ")" ))))) ; theorem :: HEYTING2:5 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) ")" )) ")" )) "holds" (Bool (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; definitionlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "V")) "," (Set (Const "C")) ")" ")" )); func :::"Involved"::: "A" -> ($#m1_hidden :::"set"::: ) means :: HEYTING2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )); end; :: deftheorem defines :::"Involved"::: HEYTING2:def 1 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_heyting2 :::"Involved"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) ")" ))))); theorem :: HEYTING2:6 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool (Set ($#k1_heyting2 :::"Involved"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))))) ; theorem :: HEYTING2:7 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_heyting2 :::"Involved"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; registrationlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "V")) "," (Set (Const "C")) ")" ")" )); cluster (Set ($#k1_heyting2 :::"Involved"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: HEYTING2:8 (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "C")) ")" ")" )) "holds" (Bool (Set ($#k1_heyting2 :::"Involved"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "V")) "," (Set (Const "C")) ")" ")" )); func :::"-"::: "A" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" )) equals :: HEYTING2:def 2 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" ($#k1_heyting2 :::"Involved"::: ) "A" ")" ) "," "C" ")" ) : (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "not" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))))) "}" ; end; :: deftheorem defines :::"-"::: HEYTING2:def 2 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool (Set ($#k2_heyting2 :::"-"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" ($#k1_heyting2 :::"Involved"::: ) (Set (Var "A")) ")" ) "," (Set (Var "C")) ")" ) : (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "not" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))))) "}" )))); theorem :: HEYTING2:9 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set "(" ($#k2_heyting2 :::"-"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: HEYTING2:10 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_heyting2 :::"-"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: HEYTING2:11 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k2_heyting2 :::"-"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: HEYTING2:12 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set "(" ($#k2_heyting2 :::"-"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )))))) ; theorem :: HEYTING2:13 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_substlat :::"mi"::: ) (Set "(" ($#k2_heyting2 :::"-"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )))))) ; theorem :: HEYTING2:14 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_heyting2 :::"-"::: ) (Set (Var "A")))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) ")" ))))))) ; definitionlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "V")) "," (Set (Const "C")) ")" ")" )); func "A" :::"=>>"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" )) equals :: HEYTING2:def 3 (Set (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) : (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "A") "}" ")" ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "A" "," "B" ")" ) : (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "A") "}" ); end; :: deftheorem defines :::"=>>"::: HEYTING2:def 3 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k3_heyting2 :::"=>>"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_xboole_0 :::"/\"::: ) "{" (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) : (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ")" ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) : (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) "}" ))))); theorem :: HEYTING2:15 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_heyting2 :::"=>>"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) : (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))))) ; theorem :: HEYTING2:16 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k3_heyting2 :::"=>>"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: HEYTING2:17 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) (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 "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )))))) ; begin definitionlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; func :::"pseudo_compl"::: "(" "V" "," "C" ")" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" )) means :: HEYTING2:def 4 (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" ) (Bool "for" (Set (Var "u9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ) "st" (Bool (Bool (Set (Var "u9")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" ($#k2_heyting2 :::"-"::: ) (Set (Var "u9")) ")" ))))); func :::"StrongImpl"::: "(" "V" "," "C" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" )) means :: HEYTING2:def 5 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" ) (Bool "for" (Set (Var "u9")) "," (Set (Var "v9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ) "st" (Bool (Bool (Set (Var "u9")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "v9")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "u9")) ($#k3_heyting2 :::"=>>"::: ) (Set (Var "v9")) ")" ))))); let "u" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Const "V")) "," (Set (Const "C")) ")" ")" ); func :::"SUB"::: "u" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" ))) equals :: HEYTING2:def 6 (Set ($#k1_zfmisc_1 :::"bool"::: ) "u"); func :::"diff"::: "u" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" )) means :: HEYTING2:def 7 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" ) "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"::: HEYTING2:def 4 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_heyting2 :::"pseudo_compl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )) "iff" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "u9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "u9")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" ($#k2_heyting2 :::"-"::: ) (Set (Var "u9")) ")" ))))) ")" )))); :: deftheorem defines :::"StrongImpl"::: HEYTING2:def 5 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_heyting2 :::"StrongImpl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "u9")) "," (Set (Var "v9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "u9")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "v9")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "u9")) ($#k3_heyting2 :::"=>>"::: ) (Set (Var "v9")) ")" ))))) ")" )))); :: deftheorem defines :::"SUB"::: HEYTING2:def 6 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k6_heyting2 :::"SUB"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "u"))))))); :: deftheorem defines :::"diff"::: HEYTING2:def 7 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_heyting2 :::"diff"::: ) (Set (Var "u")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k6_subset_1 :::"\"::: ) (Set (Var "v"))))) ")" ))))); definitionlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Atom"::: "(" "V" "," "C" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ")" )) means :: HEYTING2:def 8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "a")) ($#k2_setwiseo :::".}"::: ) )))); end; :: deftheorem defines :::"Atom"::: HEYTING2:def 8 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "a")) ($#k2_setwiseo :::".}"::: ) )))) ")" )))); theorem :: HEYTING2:18 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "K")) "," (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "K")) "," (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ")" ) ")" ))))) ; theorem :: HEYTING2:19 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ")" ))))) ; theorem :: HEYTING2:20 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k7_heyting2 :::"diff"::: ) (Set (Var "u")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r3_lattices :::"[="::: ) (Set (Var "u")))))) ; theorem :: HEYTING2:21 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "a")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; theorem :: HEYTING2:22 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Set (Var "L")) ($#k4_substlat :::"^"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Set "(" ($#k4_heyting2 :::"pseudo_compl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))))))))) ; theorem :: HEYTING2:23 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))))) ; theorem :: HEYTING2:24 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "u")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "v"))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "c")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "a")))) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "u")) ($#k3_heyting2 :::"=>>"::: ) (Set (Var "v")))) & (Bool (Set (Var "b")) ($#r1_tarski :::"c="::: ) (Set (Var "a"))) ")" )))))) ; theorem :: HEYTING2:25 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "u")))) "holds" (Bool (Set (Var "b")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "a"))) ")" ) & (Bool (Set (Set (Var "u")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set "(" ($#k8_heyting2 :::"Atom"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Set "(" ($#k5_heyting2 :::"StrongImpl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" )))))) ; theorem :: HEYTING2:26 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set (Set (Var "u")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" ($#k4_heyting2 :::"pseudo_compl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )))))) ; theorem :: HEYTING2:27 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set (Set (Var "u")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" ($#k5_heyting2 :::"StrongImpl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "v")))))) ; registrationlet "V" be ($#m1_hidden :::"set"::: ) ; let "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ) -> ($#v3_filter_0 :::"implicative"::: ) ; end; theorem :: HEYTING2:28 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set (Set (Var "u")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set "(" ($#k6_heyting2 :::"SUB"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" ($#k4_heyting2 :::"pseudo_compl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) "," (Set "(" (Set "(" ($#k5_heyting2 :::"StrongImpl"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k7_heyting2 :::"diff"::: ) (Set (Var "u")) ")" ) "," (Set (Var "v")) ")" ")" ) ")" ")" ) ")" ))))) ;