:: SUBSTLAT semantic presentation begin definitionlet "V", "C" be ($#m1_hidden :::"set"::: ) ; func :::"SubstitutionSet"::: "(" "V" "," "C" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" ) ")" ) equals :: SUBSTLAT:def 1 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" )) : (Bool "(" (Bool "(" "for" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "u")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r1_tarski :::"c="::: ) (Set (Var "t")))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ) ")" ) "}" ; end; :: deftheorem defines :::"SubstitutionSet"::: SUBSTLAT:def 1 : (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) : (Bool "(" (Bool "(" "for" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "u")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r1_tarski :::"c="::: ) (Set (Var "t")))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ) ")" ) "}" )); theorem :: SUBSTLAT:1 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ))) ; theorem :: SUBSTLAT:2 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ))) ; registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "V", "C" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Const "V")) "," (Set (Const "C")) ")" ); :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ")" )); end; registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ); end; registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ); end; definitionlet "V", "C" be ($#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 :::"mi"::: "A" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ) equals :: SUBSTLAT:def 2 "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) : (Bool "(" (Bool (Set (Var "t")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "s")) ($#r1_tarski :::"c="::: ) (Set (Var "t"))) ")" ) "iff" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ) ")" ) ")" ) "}" ; end; :: deftheorem defines :::"mi"::: SUBSTLAT:def 2 : (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) : (Bool "(" (Bool (Set (Var "t")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r1_tarski :::"c="::: ) (Set (Var "t"))) ")" ) "iff" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ) ")" ) ")" ) "}" ))); registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ); end; definitionlet "V", "C" be ($#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 :: SUBSTLAT:def 3 "{" (Set "(" (Set (Var "s")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "t")) ")" ) where s, t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ) : (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "s")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "t"))) ")" ) "}" ; end; :: deftheorem defines :::"^"::: SUBSTLAT:def 3 : (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "s")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "t")) ")" ) where s, t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) : (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "s")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "t"))) ")" ) "}" ))); theorem :: SUBSTLAT:3 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_substlat :::"^"::: ) (Set (Var "A")))))) ; theorem :: SUBSTLAT:4 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (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 "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: SUBSTLAT:5 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (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 "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"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; theorem :: SUBSTLAT:6 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (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 "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_substlat :::"mi"::: ) (Set (Var "B"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool "(" "for" (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 (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )))) ; registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster bbbadV1_RELAT_1() ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "V" "," "C" ")" ); end; theorem :: SUBSTLAT:7 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (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 "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#v1_finset_1 :::"finite"::: ) ($#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 (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_substlat :::"mi"::: ) (Set (Var "B"))))))) ; theorem :: SUBSTLAT:8 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; theorem :: SUBSTLAT:9 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: SUBSTLAT:10 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (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 "b")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k3_substlat :::"mi"::: ) (Set (Var "B")))) ")" ))))) ; theorem :: SUBSTLAT:11 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Var "K"))))) ; theorem :: SUBSTLAT:12 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_substlat :::"mi"::: ) (Set (Var "A")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")))))) ; theorem :: SUBSTLAT:13 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set "(" ($#k3_substlat :::"mi"::: ) (Set (Var "A")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SUBSTLAT:14 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "D")) "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_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "D"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k4_substlat :::"^"::: ) (Set (Var "D")))))) ; theorem :: SUBSTLAT:15 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "c")))) ")" ))))) ; theorem :: SUBSTLAT:16 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 "b")) "," (Set (Var "c")) "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 "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "b")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B"))))))) ; theorem :: SUBSTLAT:17 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_substlat :::"mi"::: ) (Set (Var "A")) ")" ) ($#k4_substlat :::"^"::: ) (Set (Var "B")))))) ; theorem :: SUBSTLAT:18 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "D")) "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_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "D")) ($#k4_substlat :::"^"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "D")) ($#k4_substlat :::"^"::: ) (Set (Var "B")))))) ; theorem :: SUBSTLAT:19 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set "(" ($#k3_substlat :::"mi"::: ) (Set (Var "A")) ")" ) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SUBSTLAT:20 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set "(" ($#k3_substlat :::"mi"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SUBSTLAT:21 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "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 "K")) ($#k4_substlat :::"^"::: ) (Set "(" (Set (Var "L")) ($#k4_substlat :::"^"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "K")) ($#k4_substlat :::"^"::: ) (Set (Var "L")) ")" ) ($#k4_substlat :::"^"::: ) (Set (Var "M")))))) ; theorem :: SUBSTLAT:22 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "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 "K")) ($#k4_substlat :::"^"::: ) (Set "(" (Set (Var "L")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "K")) ($#k4_substlat :::"^"::: ) (Set (Var "L")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set "(" (Set (Var "K")) ($#k4_substlat :::"^"::: ) (Set (Var "M")) ")" ))))) ; theorem :: SUBSTLAT:23 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (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 (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k4_substlat :::"^"::: ) (Set (Var "B")))))) ; theorem :: SUBSTLAT:24 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set (Var "A")))))) ; theorem :: SUBSTLAT:25 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#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 ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "K")) ($#k4_substlat :::"^"::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "K"))))) ; begin definitionlet "V", "C" be ($#m1_hidden :::"set"::: ) ; func :::"SubstLatt"::: "(" "V" "," "C" ")" -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) means :: SUBSTLAT:def 4 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" )) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" "V" "," "C" ")" ) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k2_substlat :::"\/"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" ))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SubstLatt"::: SUBSTLAT:def 4 : (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" )) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_substlat :::"SubstitutionSet"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b3"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k2_substlat :::"\/"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b3"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substlat :::"mi"::: ) (Set "(" (Set (Var "A")) ($#k4_substlat :::"^"::: ) (Set (Var "B")) ")" ))) ")" ) ")" ) ")" ) ")" ))); registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ; end; registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ) -> ($#v3_lattices :::"strict"::: ) ($#v10_lattices :::"Lattice-like"::: ) ; end; registrationlet "V", "C" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_substlat :::"SubstLatt"::: ) "(" "V" "," "C" ")" ) -> ($#v3_lattices :::"strict"::: ) ($#v11_lattices :::"distributive"::: ) ($#v15_lattices :::"bounded"::: ) ; end; theorem :: SUBSTLAT:26 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SUBSTLAT:27 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k5_substlat :::"SubstLatt"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ;