:: KNASTER semantic presentation begin theorem :: KNASTER:1 (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")))) ")" ) ")" )) ; begin theorem :: KNASTER:2 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k1_abian :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k1_abian :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ))))) ; theorem :: KNASTER:3 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k1_abian :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k1_abian :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ))) "holds" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"c=-monotone"::: redefine attr "f" is :::"c=-monotone"::: means :: KNASTER:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"c=-monotone"::: KNASTER:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_cohsp_1 :::"c=-monotone"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "A" ($#v4_relat_1 :::"-defined"::: ) "B" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v6_cohsp_1 :::"c=-monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X")) ")" ); func :::"lfp"::: "(" "X" "," "f" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: KNASTER:def 2 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) "}" ); func :::"gfp"::: "(" "X" "," "f" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: KNASTER:def 3 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set (Var "h")) ($#r1_tarski :::"c="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "h")))) "}" ); end; :: deftheorem defines :::"lfp"::: KNASTER:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k1_knaster :::"lfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) "}" )))); :: deftheorem defines :::"gfp"::: KNASTER:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k2_knaster :::"gfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "h")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "h")))) "}" )))); theorem :: KNASTER:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k1_knaster :::"lfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))))) ; theorem :: KNASTER:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k2_knaster :::"gfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))))) ; theorem :: KNASTER:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_knaster :::"lfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "S")))))) ; theorem :: KNASTER:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k2_knaster :::"gfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ))))) ; theorem :: KNASTER:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "(" (Bool (Set ($#k1_knaster :::"lfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k2_knaster :::"gfp"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" )) ")" )))) ; scheme :: KNASTER:sch 1 Knaster{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set F2 "(" (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) ")" )) provided (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set F2 "(" (Set (Var "X")) ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" (Set (Var "Y")) ")" ))) and (Bool (Set F2 "(" (Set F1 "(" ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) proof end; theorem :: KNASTER:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "ex" (Set (Var "Xa")) "," (Set (Var "Xb")) "," (Set (Var "Ya")) "," (Set (Var "Yb")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Xa")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Xb"))) & (Bool (Set (Var "Ya")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Yb"))) & (Bool (Set (Set (Var "Xa")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Xb"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "Ya")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Yb"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Xa"))) ($#r1_hidden :::"="::: ) (Set (Var "Ya"))) & (Bool (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Yb"))) ($#r1_hidden :::"="::: ) (Set (Var "Xb"))) ")" ))))) ; theorem :: KNASTER:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Set (Var "h")) "is" ($#v3_funct_2 :::"bijective"::: ) ))))) ; theorem :: KNASTER:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r2_tarski :::"are_equipotent"::: ) ))) ; theorem :: KNASTER:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r2_tarski :::"are_equipotent"::: ) )))) ; begin definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "O" be ($#m1_hidden :::"Ordinal":::); func "(" "f" "," "O" ")" :::"+."::: "x" -> ($#m1_hidden :::"set"::: ) means :: KNASTER:def 4 (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "x") & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O"))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ) "," "L" ")" )) ")" ) ")" )); func "(" "f" "," "O" ")" :::"-."::: "x" -> ($#m1_hidden :::"set"::: ) means :: KNASTER:def 5 (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "x") & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O"))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ) "," "L" ")" )) ")" ) ")" )); end; :: deftheorem defines :::"+."::: KNASTER:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O"))))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ) "," (Set (Var "L")) ")" )) ")" ) ")" )) ")" )))))); :: deftheorem defines :::"-."::: KNASTER:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O"))))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ) "," (Set (Var "L")) ")" )) ")" ) ")" )) ")" )))))); theorem :: KNASTER:13 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: KNASTER:14 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: KNASTER:15 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")) ")" ) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: KNASTER:16 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")) ")" ) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: KNASTER:17 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "O")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "O"))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "A")) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T")) ")" ) "," (Set (Var "L")) ")" ))))))) ; theorem :: KNASTER:18 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "O")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "O"))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "A")) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T")) ")" ) "," (Set (Var "L")) ")" ))))))) ; theorem :: KNASTER:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k1_abian :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "n")) ")" ($#k3_knaster :::"+."::: ) (Set (Var "x")))))))) ; theorem :: KNASTER:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k1_abian :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "n")) ")" ($#k4_knaster :::"-."::: ) (Set (Var "x")))))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "O" be ($#m1_hidden :::"Ordinal":::); :: original: :::"+."::: redefine func "(" "f" "," "O" ")" :::"+."::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "L"; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "O" be ($#m1_hidden :::"Ordinal":::); :: original: :::"-."::: redefine func "(" "f" "," "O" ")" :::"-."::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "P" is :::"with_suprema"::: means :: KNASTER:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_lattices :::"[="::: ) (Set (Var "z"))) & (Bool "(" "for" (Set (Var "z9")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "z9")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "z9"))) & (Bool (Set (Var "y")) ($#r1_lattices :::"[="::: ) (Set (Var "z9")))) "holds" (Bool (Set (Var "z")) ($#r1_lattices :::"[="::: ) (Set (Var "z9"))) ")" ) ")" ))); attr "P" is :::"with_infima"::: means :: KNASTER:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "z")) ($#r1_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_lattices :::"[="::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "z9")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "z9")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "z9")) ($#r1_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "z9")) ($#r1_lattices :::"[="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "z9")) ($#r1_lattices :::"[="::: ) (Set (Var "z"))) ")" ) ")" ))); end; :: deftheorem defines :::"with_suprema"::: KNASTER:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_knaster :::"with_suprema"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_lattices :::"[="::: ) (Set (Var "z"))) & (Bool "(" "for" (Set (Var "z9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "z9"))) & (Bool (Set (Var "y")) ($#r1_lattices :::"[="::: ) (Set (Var "z9")))) "holds" (Bool (Set (Var "z")) ($#r1_lattices :::"[="::: ) (Set (Var "z9"))) ")" ) ")" ))) ")" ))); :: deftheorem defines :::"with_infima"::: KNASTER:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_knaster :::"with_infima"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "z")) ($#r1_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_lattices :::"[="::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "z9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "z9")) ($#r1_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "z9")) ($#r1_lattices :::"[="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "z9")) ($#r1_lattices :::"[="::: ) (Set (Var "z"))) ")" ) ")" ))) ")" ))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_knaster :::"with_suprema"::: ) ($#v3_knaster :::"with_infima"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_knaster :::"with_suprema"::: ) ($#v3_knaster :::"with_infima"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func :::"latt"::: "P" -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) means :: KNASTER:def 8 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "P") & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & "(" (Bool (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "y")))) "implies" (Bool (Set (Var "x9")) ($#r3_lattices :::"[="::: ) (Set (Var "y9"))) ")" & "(" (Bool (Bool (Set (Var "x9")) ($#r3_lattices :::"[="::: ) (Set (Var "y9")))) "implies" (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "y"))) ")" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"latt"::: KNASTER:def 8 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_knaster :::"with_suprema"::: ) ($#v3_knaster :::"with_infima"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_knaster :::"latt"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3")) (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & "(" (Bool (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "y")))) "implies" (Bool (Set (Var "x9")) ($#r3_lattices :::"[="::: ) (Set (Var "y9"))) ")" & "(" (Bool (Bool (Set (Var "x9")) ($#r3_lattices :::"[="::: ) (Set (Var "y9")))) "implies" (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "y"))) ")" ")" )) ")" ) ")" ) ")" )))); begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) -> ($#v15_lattices :::"bounded"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: KNASTER:21 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "a")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))))) ; theorem :: KNASTER:22 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a")))))))) ; theorem :: KNASTER:23 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a"))))))) ; theorem :: KNASTER:24 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a")))))))) ; theorem :: KNASTER:25 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a")))))))) ; theorem :: KNASTER:26 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "O2"))) & (Bool (Bool "not" (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))))) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a")))))))) ; theorem :: KNASTER:27 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "O2"))) & (Bool (Bool "not" (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))))) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a")))))))) ; theorem :: KNASTER:28 (Bool "for" (Set (Var "O1")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "for" (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))))))))) ; theorem :: KNASTER:29 (Bool "for" (Set (Var "O1")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "for" (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O1")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))))))))) ; theorem :: KNASTER:30 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "O"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) ")" ))))) ; theorem :: KNASTER:31 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "O"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) ")" ))))) ; theorem :: KNASTER:32 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) & (Bool (Set (Var "b")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "O"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k5_knaster :::"+."::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) & (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k5_knaster :::"+."::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k5_knaster :::"+."::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ))) ")" ))))) ; theorem :: KNASTER:33 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) & (Bool (Set (Var "b")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "O"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k6_knaster :::"-."::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k6_knaster :::"-."::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k6_knaster :::"-."::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) ")" ))))) ; theorem :: KNASTER:34 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "for" (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k5_knaster :::"+."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "b"))))))) ; theorem :: KNASTER:35 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set (Var "b")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "for" (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "O2")) ")" ($#k6_knaster :::"-."::: ) (Set (Var "a")))))))) ; definitionlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "L")); assume (Bool (Set (Const "f")) "is" ($#v14_quantal1 :::"monotone"::: ) ) ; func :::"FixPoints"::: "f" -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) means :: KNASTER:def 9 (Bool "ex" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_knaster :::"with_suprema"::: ) ($#v3_knaster :::"with_infima"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "x")) ($#r2_abian :::"is_a_fixpoint_of"::: ) "f") "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k7_knaster :::"latt"::: ) (Set (Var "P")))) ")" )); end; :: deftheorem defines :::"FixPoints"::: KNASTER:def 9 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v14_quantal1 :::"monotone"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_knaster :::"FixPoints"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_knaster :::"with_suprema"::: ) ($#v3_knaster :::"with_infima"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) "}" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_knaster :::"latt"::: ) (Set (Var "P")))) ")" )) ")" )))); theorem :: KNASTER:36 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_knaster :::"FixPoints"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) "}" ))) ; theorem :: KNASTER:37 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_knaster :::"FixPoints"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: KNASTER:38 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_knaster :::"FixPoints"::: ) (Set (Var "f")) ")" ))) "iff" (Bool (Set (Var "a")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) ")" )))) ; theorem :: KNASTER:39 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k8_knaster :::"FixPoints"::: ) (Set (Var "f")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) ")" ))))) ; theorem :: KNASTER:40 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k8_knaster :::"FixPoints"::: ) (Set (Var "f"))) "is" ($#v4_lattice3 :::"complete"::: ) ))) ; definitionlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); let "f" be ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "L")); func :::"lfp"::: "f" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: KNASTER:def 10 (Set "(" "f" "," (Set "(" ($#k2_card_1 :::"nextcard"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ")" ) ")" ($#k5_knaster :::"+."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) "L" ")" )); func :::"gfp"::: "f" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: KNASTER:def 11 (Set "(" "f" "," (Set "(" ($#k2_card_1 :::"nextcard"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ")" ) ")" ($#k6_knaster :::"-."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) "L" ")" )); end; :: deftheorem defines :::"lfp"::: KNASTER:def 10 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k9_knaster :::"lfp"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set "(" ($#k2_card_1 :::"nextcard"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" ) ")" ($#k5_knaster :::"+."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ))))); :: deftheorem defines :::"gfp"::: KNASTER:def 11 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k10_knaster :::"gfp"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set "(" ($#k2_card_1 :::"nextcard"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" ) ")" ($#k6_knaster :::"-."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ))))); theorem :: KNASTER:41 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k9_knaster :::"lfp"::: ) (Set (Var "f"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) & (Bool "ex" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "O"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k5_knaster :::"+."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_knaster :::"lfp"::: ) (Set (Var "f")))) ")" )) ")" ))) ; theorem :: KNASTER:42 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k10_knaster :::"gfp"::: ) (Set (Var "f"))) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f"))) & (Bool "ex" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "O"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) & (Bool (Set "(" (Set (Var "f")) "," (Set (Var "O")) ")" ($#k6_knaster :::"-."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_knaster :::"gfp"::: ) (Set (Var "f")))) ")" )) ")" ))) ; theorem :: KNASTER:43 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))) "holds" (Bool "(" (Bool (Set ($#k9_knaster :::"lfp"::: ) (Set (Var "f"))) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set ($#k10_knaster :::"gfp"::: ) (Set (Var "f")))) ")" )))) ; theorem :: KNASTER:44 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k9_knaster :::"lfp"::: ) (Set (Var "f"))) ($#r3_lattices :::"[="::: ) (Set (Var "a")))))) ; theorem :: KNASTER:45 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set ($#k10_knaster :::"gfp"::: ) (Set (Var "f"))))))) ; begin theorem :: KNASTER:46 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k1_lattice3 :::"BooleLatt"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v14_quantal1 :::"monotone"::: ) ) "iff" (Bool (Set (Var "f")) "is" bbbadV6_COHSP_1()) ")" ))) ; theorem :: KNASTER:47 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k1_lattice3 :::"BooleLatt"::: ) (Set (Var "A")) ")" ) (Bool "ex" (Set (Var "g")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) "st" (Bool (Set ($#k1_knaster :::"lfp"::: ) "(" (Set (Var "A")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_knaster :::"lfp"::: ) (Set (Var "f"))))))) ; theorem :: KNASTER:48 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v14_quantal1 :::"monotone"::: ) ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k1_lattice3 :::"BooleLatt"::: ) (Set (Var "A")) ")" ) (Bool "ex" (Set (Var "g")) "being" bbbadV6_COHSP_1() ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A")) ")" ) "st" (Bool (Set ($#k2_knaster :::"gfp"::: ) "(" (Set (Var "A")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_knaster :::"gfp"::: ) (Set (Var "f"))))))) ;