:: POSET_1 semantic presentation begin registrationlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_orders_2 :::"strongly_connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P"))); end; definitionlet "IT" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "IT" is :::"chain-complete"::: means :: POSET_1:def 1 (Bool "(" (Bool "IT" "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) & (Bool "(" "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"Chain":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "L")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "L")) "," "IT") ")" ) ")" ); end; :: deftheorem defines :::"chain-complete"::: POSET_1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_poset_1 :::"chain-complete"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) & (Bool "(" "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "L")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "L")) "," (Set (Var "IT"))) ")" ) ")" ) ")" )); theorem :: POSET_1:1 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P1")) (Bool "for" (Set (Var "h")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P1")) "," (Set (Var "P2")) "holds" (Bool (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "K"))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P2")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_poset_1 :::"chain-complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#v1_poset_1 :::"chain-complete"::: ) -> ($#v1_yellow_0 :::"lower-bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: POSET_1:2 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "L")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "L")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "L")) ")" )))))) ; begin definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "g" be ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "P")) "," (Set (Const "P")); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); func :::"iterSet"::: "(" "g" "," "p" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: POSET_1:def 2 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "P" : (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" "g" "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) "p"))) "}" ; end; :: deftheorem defines :::"iterSet"::: POSET_1:def 2 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool (Set ($#k1_poset_1 :::"iterSet"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) : (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))) "}" )))); theorem :: POSET_1:3 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "holds" (Bool (Set ($#k1_poset_1 :::"iterSet"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "P")) ")" ) ")" ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P"))))) ; definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "g" be ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "P")) "," (Set (Const "P")); func :::"iter_min"::: "g" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" "P" equals :: POSET_1:def 3 (Set ($#k1_poset_1 :::"iterSet"::: ) "(" "g" "," (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) "P" ")" ) ")" ); end; :: deftheorem defines :::"iter_min"::: POSET_1:def 3 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "holds" (Bool (Set ($#k2_poset_1 :::"iter_min"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_poset_1 :::"iterSet"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "P")) ")" ) ")" )))); theorem :: POSET_1:4 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k2_poset_1 :::"iter_min"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_poset_1 :::"iter_min"::: ) (Set (Var "g")) ")" ) ")" ))))) ; theorem :: POSET_1:5 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_yellow_2 :::"<="::: ) (Set (Var "g2")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k2_poset_1 :::"iter_min"::: ) (Set (Var "g1")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k2_poset_1 :::"iter_min"::: ) (Set (Var "g2")) ")" ))))) ; definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "P")) "," (Set (Const "Q")); attr "f" is :::"continuous"::: means :: POSET_1:def 4 (Bool "(" (Bool "f" "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "L")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" "P" "holds" (Bool "f" ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "L"))) ")" ) ")" ); end; :: deftheorem defines :::"continuous"::: POSET_1:def 4 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_poset_1 :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "L")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "L"))) ")" ) ")" ) ")" ))); theorem :: POSET_1:6 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_poset_1 :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "L")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "L")) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: POSET_1:7 (Bool "for" (Set (Var "Q")) "," (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set (Var "P")) ($#k6_struct_0 :::"-->"::: ) (Set (Var "z"))) "is" ($#v2_poset_1 :::"continuous"::: ) ))) ; registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_poset_1 :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q"))))); end; registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_poset_1 :::"continuous"::: ) -> ($#v5_orders_3 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q"))))); end; theorem :: POSET_1:8 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "st" (Bool (Bool "(" "for" (Set (Var "L")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "L")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "L")) ")" ))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_poset_1 :::"continuous"::: ) ))) ; definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "g" be ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "P")) "," (Set (Const "P")); assume (Bool (Set (Const "g")) "is" ($#v2_poset_1 :::"continuous"::: ) ) ; func :::"least_fix_point"::: "g" -> ($#m1_subset_1 :::"Element":::) "of" "P" means :: POSET_1:def 5 (Bool "(" (Bool it ($#r2_abian :::"is_a_fixpoint_of"::: ) "g") & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "p")) ($#r2_abian :::"is_a_fixpoint_of"::: ) "g")) "holds" (Bool it ($#r3_orders_2 :::"<="::: ) (Set (Var "p"))) ")" ) ")" ); end; :: deftheorem defines :::"least_fix_point"::: POSET_1:def 5 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_poset_1 :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_poset_1 :::"least_fix_point"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "g"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "p")) ($#r2_abian :::"is_a_fixpoint_of"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "b3")) ($#r3_orders_2 :::"<="::: ) (Set (Var "p"))) ")" ) ")" ) ")" )))); theorem :: POSET_1:9 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "holds" (Bool (Set ($#k3_poset_1 :::"least_fix_point"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k2_poset_1 :::"iter_min"::: ) (Set (Var "g")) ")" ))))) ; theorem :: POSET_1:10 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_yellow_2 :::"<="::: ) (Set (Var "g2")))) "holds" (Bool (Set ($#k3_poset_1 :::"least_fix_point"::: ) (Set (Var "g1"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k3_poset_1 :::"least_fix_point"::: ) (Set (Var "g2")))))) ; begin definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); func :::"ConFuncs"::: "(" "P" "," "Q" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: POSET_1:def 6 "{" (Set (Var "x")) where x "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Q") ")" ) : (Bool "ex" (Set (Var "f")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "P" "," "Q" "st" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "x")))) "}" ; end; :: deftheorem defines :::"ConFuncs"::: POSET_1:def 6 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k4_poset_1 :::"ConFuncs"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) ")" ) : (Bool "ex" (Set (Var "f")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "st" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "x")))) "}" )); definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); func :::"ConRelat"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k4_poset_1 :::"ConFuncs"::: ) "(" "P" "," "Q" ")" ")" ) means :: POSET_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_poset_1 :::"ConFuncs"::: ) "(" "P" "," "Q" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_poset_1 :::"ConFuncs"::: ) "(" "P" "," "Q" ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "P" "," "Q" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "f")) ($#r1_yellow_2 :::"<="::: ) (Set (Var "g"))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"ConRelat"::: POSET_1:def 7 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k4_poset_1 :::"ConFuncs"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_poset_1 :::"ConRelat"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_poset_1 :::"ConFuncs"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_poset_1 :::"ConFuncs"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) & (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "f")) ($#r1_yellow_2 :::"<="::: ) (Set (Var "g"))) ")" )) ")" ) ")" )) ")" ))); registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k5_poset_1 :::"ConRelat"::: ) "(" "P" "," "Q" ")" ) -> ($#v1_relat_2 :::"reflexive"::: ) ; cluster (Set ($#k5_poset_1 :::"ConRelat"::: ) "(" "P" "," "Q" ")" ) -> ($#v8_relat_2 :::"transitive"::: ) ; cluster (Set ($#k5_poset_1 :::"ConRelat"::: ) "(" "P" "," "Q" ")" ) -> ($#v4_relat_2 :::"antisymmetric"::: ) ; end; definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); func :::"ConPoset"::: "(" "P" "," "Q" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"Poset":::) equals :: POSET_1:def 8 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k4_poset_1 :::"ConFuncs"::: ) "(" "P" "," "Q" ")" ")" ) "," (Set "(" ($#k5_poset_1 :::"ConRelat"::: ) "(" "P" "," "Q" ")" ")" ) "#)" ); end; :: deftheorem defines :::"ConPoset"::: POSET_1:def 8 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k4_poset_1 :::"ConFuncs"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "," (Set "(" ($#k5_poset_1 :::"ConRelat"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "#)" ))); definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Const "P")) "," (Set (Const "Q")) ")" ")" ); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); func "F" :::"-image"::: "p" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" "Q" equals :: POSET_1:def 9 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "Q" : (Bool "ex" (Set (Var "f")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "P" "," "Q" "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) "p")) ")" )) "}" ; end; :: deftheorem defines :::"-image"::: POSET_1:def 9 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "F")) ($#k7_poset_1 :::"-image"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool "ex" (Set (Var "f")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) ")" )) "}" )))); definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Const "P")) "," (Set (Const "Q")) ")" ")" ); func :::"sup_func"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" "P" "," "Q" means :: POSET_1:def 10 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" "Q" "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "F" ($#k7_poset_1 :::"-image"::: ) (Set (Var "p"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "M")))))); end; :: deftheorem defines :::"sup_func"::: POSET_1:def 10 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_poset_1 :::"sup_func"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_poset_1 :::"-image"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "M")))))) ")" )))); registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Const "P")) "," (Set (Const "Q")) ")" ")" ); cluster (Set ($#k8_poset_1 :::"sup_func"::: ) "F") -> ($#v2_poset_1 :::"continuous"::: ) ; end; theorem :: POSET_1:11 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Chain":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "F")) "," (Set ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) & (Bool (Set ($#k8_poset_1 :::"sup_func"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "F")) "," (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) ")" )) ")" ))) ; definitionlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); func :::"min_func"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Function":::) "of" "P" "," "Q" equals :: POSET_1:def 11 (Set "P" ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) "Q" ")" )); end; :: deftheorem defines :::"min_func"::: POSET_1:def 11 : (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k9_poset_1 :::"min_func"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "Q")) ")" )))); registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k9_poset_1 :::"min_func"::: ) "(" "P" "," "Q" ")" ) -> ($#v2_poset_1 :::"continuous"::: ) ; end; theorem :: POSET_1:12 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k9_poset_1 :::"min_func"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ))))) ; registrationlet "P", "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k6_poset_1 :::"ConPoset"::: ) "(" "P" "," "Q" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ; end; begin definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); func :::"fix_func"::: "P" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" "P" "," "P" ")" ")" ) "," "P" means :: POSET_1:def 12 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" "P" "," "P" ")" ")" ) (Bool "for" (Set (Var "h")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "P" "," "P" "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_poset_1 :::"least_fix_point"::: ) (Set (Var "h")))))); end; :: deftheorem defines :::"fix_func"::: POSET_1:def 12 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "P")) ")" ")" ) "," (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_poset_1 :::"fix_func"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_poset_1 :::"ConPoset"::: ) "(" (Set (Var "P")) "," (Set (Var "P")) ")" ")" ) (Bool "for" (Set (Var "h")) "being" ($#v2_poset_1 :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "P")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_poset_1 :::"least_fix_point"::: ) (Set (Var "h")))))) ")" ))); registrationlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_poset_1 :::"chain-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k10_poset_1 :::"fix_func"::: ) "P") -> ($#v2_poset_1 :::"continuous"::: ) ; end;