Impressum scott_continuity.prf
Interaktion und
(scott_continuitynil 3330742497"" (skosimp)"" (typepred "D!1" )"" (typepred "g!1" )"" (expand "lub_set?" )"" (typepred "le2" )"" (expand "directed_complete_partial_order?" )"" (flatten)"" (expand "directed_complete?" )"" (inst - "image(g!1,D!1)" )"" (hide 2)"" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (skosimp)"1" "g!1(x!1)" )"1" expand "member" )"1" expand "image" )"1" (inst + "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "directed?" )"2" (skosimp*)"2" (expand "image" )"2" "2" replace -1)"2" replace -2)"2" expand "directed?" )"2" "x!2" "x!3" )"2" assert )"2" "2" "g!1(z!1)" )"1" expand "increasing?" )"1" "x!2" "z!1" )"1" "x!3" "z!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "z!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" bounded_order_props "orders/" )"bool" directed_orders "orders/" )"(D!1)" scott_continuity nil )"bool" sets nil )"T1" scott_continuity nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(increasing?)" scott_continuity nil )"directed[T1, le1]" scott_continuity nil )"set[R]" function_image nil )"bool" directed_orders "orders/" )"bool" orders nil )"bool" fun_preds_partial nil )"(directed_complete_partial_order?[T2])" nil )nil scott_continuity nil ))nil 3352749145"" (skosimp)"" (typepred "D!1" )"" (expand "nonempty?" )"" (expand "empty?" )"" (skosimp)"" (expand "member" )"" (inst - "g!1(x!1)" )"" (expand "image" ) (("" (inst + "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"set[R]" function_image nil )"T1" scott_continuity nil )"directed[T1, le1]" scott_continuity nil )nil scott_continuity nil )"(directed_complete_partial_order?[T2])" nil )"bool" fun_preds_partial nil ))nil ))nil 3352750482"" (skosimp)"" (typepred "D!1" )"" (typepred "g!1" )"" (expand "directed?" )"" (expand "directed?" )"" (skosimp*)"" (expand "image" )"" (skosimp*)"" (replace -4)"" (replace -5)"" (hide -4 -5 -2)"" (inst - "x!2" "x!3" )"" (assert )"" (skosimp)"" "g!1(z!1)" )"1" expand "increasing?" )"1" "x!2" "z!1" )"1" "x!3" "z!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand "image" )"2" (inst + "z!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(increasing?)" scott_continuity nil )"directed[T1, le1]" scott_continuity nil )"(D!1)" scott_continuity nil )"set[R]" function_image nil )"bool" directed_orders "orders/" )"bool" fun_preds_partial nil )"(directed_complete_partial_order?[T2])" nil )nil scott_continuity nil ))nil 3352749145"" (skosimp)"" (lemma "lub_set_image" ("g" "g!1" "D" "D!1" ))"" (propax) nil nil )) nil ))nil )"bool" fun_preds_partial nil )"(directed_complete_partial_order?[T2])" nil )nil scott_continuity nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil scott_continuity nil )nil scott_continuity nil ))nil ))nil 3352750819"" (skosimp)"" (typepred "D!1" )"" (lemma "directed_image" ("g" "g!1" "D" "D!1" ))"" (typepred "lub(image(g!1, D!1))" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" (inst - "g!1(lub(D!1))" )"1" (split -2)"1" (propax) nil nil )"2" (hide 2)"2" (expand "upper_bound?" 1)"2" (skosimp)"2" (typepred "r!1" )"2" (expand "image" )"2" (skosimp)"2" replace -1)"2" "2" "g!1" )"2" "lub(D!1)" )"1" expand "least_upper_bound?" )"1" "1" "1" expand "upper_bound?" )"1" "x!1" )"1" expand "increasing?" )"1" "x!1" "lub(D!1)" )"1" assert )nil nil )"2" "le1" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le1" )"2" expand "directed_complete_partial_order?" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "le1" )"2" (expand "directed_complete_partial_order?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (typepred "le2" )"2" (expand "directed_complete_partial_order?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set[R]" function_image nil )"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" "orders/" )"bool" bounded_order_props "orders/" )"bool" bounded_orders "orders/" )"bool" bounded_orders "orders/" )nil scott_continuity nil )nil scott_continuity nil )"(directed_complete_partial_order?[T2])" nil )"bool" fun_preds_partial nil ))nil 3353382632"" (skosimp)"" (typepred "D!1" )"" (expand "nonempty?" )"" (expand "empty?" )"" (skosimp)"" (inst - "f!1(x!1)" )"" (expand "member" )"" (expand "image" ) (("" (inst + "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )nil scott_continuity nil )"set[R]" function_image nil )"T1" scott_continuity nil )"directed[T1, le1]" scott_continuity nil )"bool" sets nil ))nil ))nil 3353382632"" (skosimp)"" (typepred "D!1" )"" (expand "lub_set?" )"" (typepred "le2" )"" (expand "directed_complete_partial_order?" )"" (flatten)"" (expand "directed_complete?" )"" (inst - "image[T1,T2](f!1,D!1)" )"" (expand "directed?" -4) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil scott_continuity nil )"(directed_complete_partial_order?[T2])" nil )"bool" orders nil )"bool" directed_orders "orders/" )"set[R]" function_image nil )"directed[T1, le1]" scott_continuity nil )"[T1 -> T2]" scott_continuity nil )"bool" directed_orders "orders/" )"bool" bounded_order_props "orders/" ))nil ))nil 3353382128"" (skolem + ("f" ))"" (expand "increasing?" )"" (flatten)"" (skolem + ("x" "y" ))"" (flatten)"" (name "X" "lambda (z:T1): z=x OR z=y" )"" (case "lub_set?(X)" )"1" (case "lub[T1,le1](X)=y" )"1" (inst - "X" )"1" (replace -1)"1" (case-replace "f(x)=f(y)" )"1" (typepred "le2" )"1" expand "directed_complete_partial_order?" )"1" (expand "partial_order?" )"1" expand "preorder?" )"1" "1" expand "reflexive?" )"1" (inst - "f(y)" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "image(f,X) = LAMBDA (z:T2): z = f(x) OR z = f(y)" )"1" "Y" "LAMBDA (z: T2): z = f(x) OR z = f(y)" )"1" (flatten)"1" case "lub_set?(Y)" )"1" case "lub[T2,le2](Y)=f(x) OR lub[T2,le2](Y)=f(y)" )"1" "1" (assert ) nil nil )"2" "lub[T2, le2](Y)" )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "f(x)" )"1" (assert ) nil nil )"2" expand "Y" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "lub[T2, le2](Y)" )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "f(y)" )"1" "le2" )"1" expand "directed_complete_partial_order?" )"1" expand "partial_order?" )"1" expand "antisymmetric?" )"1" "1" "lub[T2, le2](Y)" "f(y)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Y" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "le2" )"3" expand "directed_complete_partial_order?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" expand "lub_set?" )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" expand "directed_complete?" )"2" "2" "Y" )"2" expand "directed?" )"2" "2" expand "directed?" )"2" "x!1" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "le2" )"3" expand "directed_complete_partial_order?" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality 1 :hide? t)"2" (expand "image" )"2" "2" "EXISTS (x: (X)): x!1 = f(x)" )"1" "1" "x!2" )"1" expand "X" )"1" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "1" "x" )"1" expand "X" )"1" (propax) nil nil ))nil ))nil )"2" "y" )"2" expand "X" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -3)"2" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (inst - "x" )"1" expand "member" )"1" expand "X" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "directed?" )"2" (expand "directed?" )"2" (skosimp)"2" "lub[T1, le1](X)" )"2" replace -4)"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "y" )"1" "x!1" )"1" "y!1" )"1" (assert ) nil nil ))nil ))nil )"2" expand "X" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" (typepred "lub[T1, le1](X)" )"2" (expand "least_upper_bound?" )"2" (flatten)"2" (expand "upper_bound?" )"2" (inst -2 "y" )"2" "y" )"1" "1" "le1" )"1" expand "directed_complete_partial_order?" )"1" expand "partial_order?" )"1" "1" expand "antisymmetric?" )"1" "lub[T1, le1](X)" "y" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "r!1" )"2" expand "X" )"2" "1" (assert ) nil nil )"2" "le1" )"2" expand "directed_complete_partial_order?" )"2" expand "partial_order?" )"2" expand "preorder?" )"2" "2" expand "reflexive?" )"2" "y" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "X" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2 -2 -1)"2" (expand "lub_set?" )"2" (expand "least_bounded_above?" )"2" (inst + "y" )"2" (expand "least_upper_bound?" )"2" (expand "upper_bound?" )"2" (split)"1" "1" "r!1" )"1" expand "X" )"1" "1" (assert ) nil nil )"2" "le1" )"2" expand "directed_complete_partial_order?" )"2" expand "partial_order?" )"2" expand "preorder?" )"2" "2" expand "reflexive?" )"2" "y" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "y" )"2" expand "X" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "le1" )"3" (expand "directed_complete_partial_order?" )"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" fun_preds_partial nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil scott_continuity nil )"bool" bounded_orders "orders/" )"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" "orders/" )"bool" bounded_orders "orders/" )"T1" scott_continuity nil )"T1" scott_continuity nil )"bool" sets nil )"bool" sets nil )"set[R]" function_image nil )"bool" directed_orders "orders/" )"bool" directed_orders "orders/" )"[T2 -> boolean]" scott_continuity nil )"[T1 -> T2]" scott_continuity nil )"T1" scott_continuity nil )"bool" bounded_orders "orders/" )"T1" scott_continuity nil )"bool" relations nil )NOT const-decl "[bool -> bool]" booleans nil )"(directed_complete_partial_order?[T2])" nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )nil scott_continuity nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"[T1 -> boolean]" scott_continuity nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil partial_order_props"orders/" )nil partial_order_props"orders/" )set type-eq-decl nil sets nil )nil defined_types nil )"bool" directed_orders"orders/" )"(directed_complete_partial_order?[T1])" nil )"bool" bounded_order_props "orders/" ))nil 3330155115"" (skosimp)"" (expand "scott_continuous?" )"" (split)"1" (flatten)"1" (case-replace "increasing?(f!1)" )"1" (expand "lub_preserving?" )"1" (skosimp)"1" (typepred "D!1" )"1" (lemma "directed_image" ("g" "f!1" "D" "D!1" ))"1" case "nonempty?[T2](image[T1, T2](f!1,D!1))" )"1" "closure_is_down" "x" "lub[T2, le2](image(f!1, D!1))" ))"1" (name "FD" "image(f!1, D!1)" )"1" (replace -1)"1" (name "JFD" "lub[T2, le2](FD)" )"1" replace -1)"1" "down_is_closed[T2,le2]" "x" "JFD" ))"1" expand "member" )"1" rewrite "continuous_closed_sets" )"1" "down(JFD)" )"1" expand "closed?" )"1" expand "scott_open_sets" )"1" expand "Complement" )"1" expand "member" )"1" "1" "1" "b!1" )"1" rewrite "complement_equal" )"1" case "subset?(D!1,b!1)" )"1" expand "scott_closed_sets" )"1" expand "extend" )"1" "1" "D!1" )"1" assert )"1" "lub[T2,le2](FD)" )"1" replace "1" "lub(D!1)" )"1" "JD" "lub(D!1)" )"1" replace "1" expand "least_upper_bound?" )"1" "1" expand "increasing?" )"1" "f!1(JD)" )"1" "1" expand "inverse_image" )"1" expand "member" )"1" replace "1" assert )"1" expand "down" )"1" "partial_order_antisymmetric" "x" "f!1(JD)" "y" "JFD" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" "r!1" )"2" replace "2" expand "image" )"2" "2" replace "2" "x!1" "JD" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le1" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" "2" expand "member" )"2" replace "2" expand "inverse_image" )"2" expand "member" )"2" expand "down" )"2" expand "JFD" )"2" "lub[T2, le2](FD)" )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "f!1(x!1)" )"2" expand "FD" )"2" expand "image" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "down(JFD)" )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "le2" )"2" expand "directed_complete_partial_order?" )"2" (flatten) nil nil )) nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (skosimp)"2" (expand "member" )"2" "f!1(x!1)" )"2" expand "image" )"2" (inst + "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "increasing?" )"2" (skosimp)"2" case "inverse_image(f!1, Cl(singleton(f!1(y!1))))(y!1)" )"1" "Cl_closed" ("A" "singleton(f!1(y!1))" ))"1" (rewrite "continuous_closed_sets" )"1" (rewrite "order_iff_closure" 1)"1" (inst - "Cl(singleton(f!1(y!1)))" )"1" (assert )"1" expand "closed?" -4)"1" expand "scott_open_sets" )"1" expand "scott_closed_sets" )"1" expand "member" )"1" expand "extend" )"1" expand "Complement" )"1" "1" "b!1" )"1" rewrite "complement_equal" )"1" assert )"1" expand "inverse_image" )"1" expand "member" )"1" expand "lower_set?" )"1" expand "member" )"1" "y!1" "x!1" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "inverse_image" )"2" (expand "member" )"2" "subset_of_Cl" "A" "singleton(f!1(y!1))" ))"2" (expand "subset?" )"2" (inst - "f!1(y!1)" )"2" expand "member" )"2" expand "singleton" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "le2" )"3" (expand "directed_complete_partial_order?" )"3" (flatten) nil nil )) nil ))nil )"4" (typepred "le1" )"4" (expand "directed_complete_partial_order?" )"4" (flatten) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (rewrite "continuous_open_sets" )"2" (skosimp)"2" (case "upper_set?(inverse_image(f!1,Y!1))" )"1" (expand "open?" )"1" (expand "member" )"1" (expand "scott_open_sets" )"1" (expand "Complement" )"1" (skosimp)"1" (typepred "b!1" )"1" (expand "scott_closed_sets" )"1" expand "extend" )"1" "1" "X" "inverse_image(f!1, Y!1)" )"1" replace -1)"1" "complement(X)" )"1" rewrite "complement_complement" )nil nil )"2" expand "scott_closed_sets" )"2" expand "extend" )"2" "complement_upper_set" "U" "X" ))"1" assert )"1" "1" "D!1" )"1" replace -5 * rl)"1" expand "complement" )"1" expand "member" )"1" replace "1" "lub(D!1)" )"1" "image(f!1,D!1)" )"1" expand "inverse_image" )"1" expand "member" )"1" expand "lub_preserving?" )"1" "D!1" )"1" "1" "1" assert )nil nil )"2" expand "subset?" )"2" "2" expand "member" )"2" expand "image" )"2" "2" "x!2" )"2" expand "lower_set?" )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "lub_set?" )"2" "directed_image" "g" "f!1" "D" "D!1" ))"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" "2" expand "directed_complete?" )"2" "image(f!1, D!1)" )"2" expand "directed?" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "directed_image" "g" "f!1" "D" "D!1" ))"2" assert )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "2" "f!1(x!1)" )"2" expand "member" )"2" expand "image" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "open?" )"2" (expand "member" )"2" (expand "scott_open_sets" )"2" (expand "Complement" )"2" (skosimp)"2" (typepred "b!1" )"2" expand "scott_closed_sets" )"2" expand "extend" )"2" "2" expand "upper_set?" )"2" expand "member" )"2" expand "inverse_image" )"2" "2" expand "member" )"2" replace -7)"2" expand "complement" )"2" expand "member" )"2" expand "lower_set?" )"2" expand "member" )"2" "f!1(y!1)" "f!1(x!1)" )"2" expand "increasing?" )"2" "x!1" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "le1" )"3" (expand "directed_complete_partial_order?" )"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" scott_continuity nil )"bool" topology "topology/" )nil partial_order_props"orders/" )nil partial_order_props "orders/" )"T1" scott_continuity nil )"bool" directed_orders "orders/" )"bool" orders nil )"bool" directed_orders "orders/" )"directed[T1, le1]" scott_continuity nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sets_lemmas nil )"set[T1]" scott_continuity nil )"set" sets nil )"bool" partial_order_props "orders/" )nil continuity "topology/" )nil topology "topology/" )nil topology "topology/" )nil scott nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"directed[T, <=]" nil )"topology" nil )"set[T]" topology "topology/" )"bool" sets nil )"(singleton?)" sets nil )"bool" scott_continuity nil )nil directed_order_props "orders/" )"bool" directed_order_props "orders/" )"bool" sets nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )"set[R]" function_image nil )"[T, T -> boolean]" equalities nil )nil scott nil )"setofsets[T]" scott nil )nil sets nil )nil defined_types nil )nil continuity "topology/" )"bool" topology "topology/" )"setofsets[T]" sets_lemmas nil )"setofsets[T]" scott nil )"bool" sets nil )"R" extend nil )"bool" bounded_orders "orders/" )nil partial_order_props"orders/" )"(partial_order?[set[T]])" nil )"closed[T, scott_open_sets]" nil )"compact[T, scott_open_sets]" scott_continuity nil )"non_empty_finite_set[T]" scott_continuity nil )"{x | bounded_orders[T2].least_upper_bound?(x, FD, le2)}" nil )"directed[T1, le1]" scott_continuity nil )"T1" scott_continuity nil )"[T1 -> T2]" scott_continuity nil )"set[T2]" scott_continuity nil )nil sets_lemmas nil )"set[D]" function_image nil )"bool" partial_order_props "orders/" )nil partial_order_props "orders/" )"lower_set" partial_order_props "orders/" )"bool" sets nil )"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" "orders/" )"bool" bounded_orders "orders/" )"bool" bounded_order_props "orders/" )nil scott nil )"bool" sets nil )"T1" scott_continuity nil )nil scott_continuity nil )"bool" fun_preds_partial nil )"(directed_complete_partial_order?[T2])" nil )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )nil booleans nil )nil booleans nil )nil scott_continuity nil )nil scott_continuity nil ))nil 3330316834"" (skosimp)"" (typepred "x!1" )"" (rewrite "scott_continuous_def" ) nil nil )) nil ))nil )"bool" scott_continuity nil )nil scott_continuity nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil scott_continuity nil ))nil 3330316859"" (skosimp)"" (typepred "x!1" )"" (rewrite "scott_continuous_def" ) nil nil )) nil ))nil )"bool" continuity_def "topology/" )"(directed_complete_partial_order?[T2])" nil )"setofsets[T]" scott nil )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )nil sets nil )nil defined_types nil )nil scott_continuity nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil scott_continuity nil ))nil 3330547445"" (skosimp)"" (typepred "x!1" )"" (rewrite "scott_continuous_def" )"" (expand "scott_continuous?" ) (("" (flatten) nil nil ))nil ))nil ))nil ))nil )"bool" continuity_def "topology/" )"(directed_complete_partial_order?[T2])" nil )"setofsets[T]" scott nil )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )nil sets nil )nil defined_types nil )nil scott_continuity nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" scott_continuity nil )nil scott_continuity nil ))nil 3330934809"" (skosimp)"" (typepred "x!1" )"" (rewrite "scott_continuous_def" )"" (expand "scott_continuous?" ) (("" (flatten) nil nil ))nil ))nil ))nil ))nil )"bool" continuity_def "topology/" )"(directed_complete_partial_order?[T2])" nil )"setofsets[T]" scott nil )"(directed_complete_partial_order?[T1])" nil )"bool" directed_orders"orders/" )nil defined_types nil )nil sets nil )nil defined_types nil )nil scott_continuity nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" scott_continuity nil )nil scott_continuity nil ))nil 3352784732"" (expand "restrict" )"" (expand "directed_complete?" )"" (skosimp)"" (typepred "D!1" )"" (expand "pointwise" )"" (expand "least_bounded_above?" )"" case "FORALL (x: T1): lub_set?[T2, le2]({y: T2 | EXISTS (f: (D!1)): y=f(x)})" )"1" "F" "LAMBDA (x:T1): lub[T2,le2]({y: T2 | EXISTS (f: (D!1)): y=f(x)})" )"1" (case "increasing?(F)" )"1" (lemma "directed_is_lub_set[T1,le1]" )"1" (lemma "lub_set_image" ("g" "F" ))"1" "FX" "LAMBDA (D:directed[T1, le1]): {y: T2 | EXISTS (f:(D!1),x:(D)): y = f(x)}" )"1" case "forall (D: directed[T1, le1]): nonempty?[T2](FX(D)) AND directed?[T2](le2)(FX(D))" )"1" case "forall (D: directed[T1, le1]): lub_set?(FX(D))" )"1" case "forall (D:directed[T1, le1]): F(lub(D)) = lub(FX(D))" )"1" case "FORALL (D: directed[T1, le1]): lub(image[T1,T2](F,D)) = lub(FX(D))" )"1" case "lub_preserving?(F)" )"1" case "scott_continuous?(F)" )"1" "F" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "1" "1" "r!1" )"1" "x!1" )"1" "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "r!1(x!1)" )"1" expand "F" )"1" nil nil ))nil )"2" "r!1" )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "r!1" )"2" expand "upper_bound?" )"2" "x!1" )"2" "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})" )"1" expand "least_upper_bound?" )"1" "1" "r!1(x!1)" )"1" "1" expand "F" )"1" nil nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "r!2" )"2" "2" replace "2" "f!1" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "scott_continuous?" )"2" (assert ) nil nil ))nil ))nil )"2" "2" expand "lub_preserving?" )"2" "2" "D!2" )"2" "D!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "lub_set_image" "g" "F" "D" "D!2" ))"2" "D!2" )"2" "lub(image[T1, T2](F, D!2))" )"2" "lub(FX(D!2))" )"2" expand "least_upper_bound?" )"2" "2" "lub(image[T1, T2](F, D!2))" )"1" "1" "lub(FX(D!2))" )"1" "1" "partial_order_antisymmetric" "x" "lub(image[T1, T2](F, D!2))" "y" "lub(FX(D!2))" ))"1" assert )nil nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "r!1" )"2" expand "image" )"2" "2" replace "2" "x!1" )"2" "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})" )"1" expand "least_upper_bound?" )"1" "1" "lub(FX(D!2))" )"1" "1" expand "F" )"1" nil nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "r!2" )"2" "2" replace "2" "f!1(x!1)" )"2" expand "FX" )"2" "f!1" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "r!1" )"2" expand "FX" "2" "2" replace "2" "F(x!1)" )"1" "1" "x!1" )"1" "DRL100" "lub(image[T1, T2](F, D!2))" )"1" expand "F" )"1" "lub({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})" )"1" expand "least_upper_bound?" )"1" "1" "1" expand "upper_bound?" )"1" "f!1(x!1)" )"1" "partial_order_transitive" "x" "f!1(x!1)" "y" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})" "z" "DRL100" ))"1" assert )nil nil ))nil )"2" "f!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "2" "2" expand "F" 1)"2" expand "FX" )"2" "2" "D!2" )"2" "D!2" )"2" "2" "lub({y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)})" )"1" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "lub({y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)})" )"1" "1" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})" )"1" "1" "partial_order_antisymmetric" "x" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})" "y" "lub({y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)})" ))"1" assert )nil nil ))nil )"2" "2" "2" "r!1" )"2" "2" "x!1" )"2" "f!1(lub(D!2))" )"1" "DRL100" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(lub(D!2))})" )"1" replace "1" "1" "f!1" )"1" expand "scott_continuous?" )"1" "1" "lub(D!2)" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "x!1" )"1" expand "increasing?" )"1" "x!1" "lub(D!2)" )"1" assert )"1" "partial_order_transitive" "x" "f!1(x!1)" "y" "f!1(lub(D!2))" "z" "DRL100" ))"1" assert )nil nil ))nil ))nil )"2" "le1" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "f!1" )nil nil )"3" "le1" )"3" expand "directed_complete_partial_order?" )"3" nil nil ))nil ))nil )"4" "le2" )"4" expand "directed_complete_partial_order?" )"4" "4" "directed_is_lub_set[T1,le1]" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "lub(D!2)" )"1" "le1" )"1" expand "directed_complete_partial_order?" )"1" assert )nil nil ))nil ))nil )"2" "directed_is_lub_set[T1,le1]" )"2" nil nil ))nil ))nil )"3" "3" "le1" )"3" expand "directed_complete_partial_order?" )"3" nil nil ))nil ))nil ))nil )"4" "4" "directed_is_lub_set[T1,le1]" )"4" nil nil ))nil ))nil ))nil )"2" "2" "r!1" )"2" "2" replace "2" "2" "2" "f!1" )"2" expand "scott_continuous?" )"2" "2" expand "lub_preserving?" )"2" "D!2" )"2" "lub_set_image" "g" "f!1" "D" "D!2" ))"2" assert )"2" replace "2" expand "image" )"2" "DRL101" "{y: T2 | EXISTS (f: (D!1), x: (D!2)): y = f(x)}" )"2" "DRL102" "{y: T2 | EXISTS (x: (D!2)): y = f!1(x)}" )"2" "above_lub[T2,le2]" )"2" "DRL101" "DRL102" )"2" "1" nil nil )"2" "2" expand "above?" )"2" "2" "x!1" )"2" expand "DRL102" )"2" "2" replace "2" expand "DRL101" )"2" "f!1(x!2)" )"1" rewrite "partial_order_reflexive" )nil nil )"2" expand "DRL101" )"2" "f!1" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "lub(D!2)" )"1" "le1" )"1" expand "directed_complete_partial_order?" )"1" nil nil ))nil ))nil )"2" "directed_is_lub_set[T1,le1]" )"2" nil nil ))nil ))nil )"3" "3" "le1" )"3" expand "directed_complete_partial_order?" )"3" nil nil ))nil ))nil ))nil )"4" "4" "directed_is_lub_set[T1,le1]" )"4" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil )"4" assert )"4" "4" "le1" )"4" expand "directed_complete_partial_order?" )"4" (flatten) nil nil ))nil ))nil ))nil ))nil )"5" (propax) nil nil ))nil )"2" "2" "D!2" )"2" "2" "directed_is_lub_set" "x" "FX(D!2)" ))"1" (propax) nil nil )"2" expand "directed?" 1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "le2" )"3" expand "directed_complete_partial_order?" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2 -1 -5)"2" "2" "D!2" )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "1" "1" expand "FX" )"1" "x!2(x!1)" )"1" "x!2" "x!1" )nil nil ))nil ))nil ))nil )"2" "2" expand "directed?" )"2" "2" expand "FX" )"2" "2" replace -1)"2" replace -2)"2" "f!1" )"2" "f!2" )"2" "f!1" "f!2" )"2" assert )"2" expand "scott_continuous?" )"2" "2" "2" "2" expand "directed?" )"2" "x!2" "x!3" )"2" assert )"2" "2" expand "increasing?" )"2" "x!3" "z!2" )"2" "x!2" "z!2" )"2" assert )"2" "z!2" )"2" "z!2" )"2" "partial_order_transitive" "z" "z!1(z!2)" ))"2" "f!1(x!2)" "f!1(z!2)" )"2" "f!2(x!3)" "f!2(z!2)" )"2" assert )"2" "z!1(z!2)" )"1" assert )nil nil )"2" expand "FX" )"2" "z!1" "z!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" "le2" )"3" expand "directed_complete_partial_order?" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" (expand "increasing?" )"2" (skosimp)"2" (expand "F" )"2" (hide -2)"2" "x!1" )"2" "y!1" )"2" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(x!1)})" )"1" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(y!1)})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(y!1)})" )"1" "1" (propax) nil nil )"2" "2" "2" "r!1" )"2" "2" replace -1)"2" "f!1(y!1)" )"1" "f!1" )"1" expand "scott_continuous?" )"1" "1" expand "increasing?" )"1" "x!1" "y!1" )"1" assert )"1" "partial_order_transitive" "x" "f!1(x!1)" "y" "f!1(y!1)" "z" "lub[T2, le2]({y: T2 | EXISTS (f: (D!1)): y = f(y!1)})" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "f!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "le2" )"2" expand "directed_complete_partial_order?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "le2" )"3" (expand "directed_complete_partial_order?" )"3" (flatten) nil nil )) nil ))nil )"4" (typepred "le1" )"4" (expand "directed_complete_partial_order?" )"4" (flatten) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "lub_set?" )"2" (typepred "le2" )"2" expand "directed_complete_partial_order?" )"2" (flatten)"2" (expand "directed_complete?" )"2" "{y: T2 | EXISTS (f: (D!1)): y = f(x!1)}" )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" "1" expand "member" )"1" "x!2(x!1)" )"1" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "directed?" )"2" "2" replace -1)"2" replace -2)"2" "f!1" )"2" "f!2" )"2" "f!1" "f!2" )"2" assert )"2" "2" "x!1" )"2" "x!1" )"2" "z!1(x!1)" )"1" assert )nil nil )"2" "z!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (typepred "le2" )"3" (expand "directed_complete_partial_order?" )"3" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" directed_orders "orders/" )"(directed_complete_partial_order?[T2])" nil )"bool" directed_orders"orders/" )"bool" pointwise_orders "orders/" )"bool" directed_orders "orders/" )"bool" orders nil )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil )"bool" scott_continuity nil )nil scott_continuity nil )nil scott_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" bounded_orders "orders/" )"(D!1)" scott_continuity nil )"(scott_continuous?)" scott_continuity nil )"T1" scott_continuity nil )"bool" bounded_orders "orders/" )"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" "orders/" )"T1" scott_continuity nil )"(D!1)" scott_continuity nil )nil directed_order_props"orders/" )"bool" directed_order_props "orders/" )nil directed_order_props "orders/" )"bool" sets nil )"directed[T1, le1]" scott_continuity nil )"T1" scott_continuity nil )"(scott_continuous?)" scott_continuity nil )"(D!1)" scott_continuity nil )"(D!2)" scott_continuity nil )"bool" sets nil )"(D!1)" scott_continuity nil )nil bounded_order_props "orders/" )"bool" bounded_order_props "orders/" )"[T2 -> boolean]" scott_continuity nil )nil partial_order_props"orders/" )"(D!2)" scott_continuity nil )"(D!1)" scott_continuity nil )"[T2 -> boolean]" scott_continuity nil )"directed[T1, le1]" scott_continuity nil )"set[R]" function_image nil )"bool" bounded_orders "orders/" )"T1" scott_continuity nil )"(D!1)" scott_continuity nil )"[x: T1 -> " nil )"(directed?(LAMBDA (s: [(scott_continuous?), (scott_continuous?)]): " scott_continuity nil) "bool" scott_continuity nil )nil partial_order_props"orders/" )"[directed[T1, le1] -> [T2 -> boolean]]" nil )"directed[T1, le1]" scott_continuity nil )"(D!1)" scott_continuity nil )"(D!2)" scott_continuity nil )"(D!2)" scott_continuity nil )"(D!1)" scott_continuity nil )nil partial_order_props"orders/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil scott_continuity nil )"bool" fun_preds_partial nil )"(directed_complete_partial_order?[T1])" nil )"[T, T -> boolean]" equalities nil )"bool" bounded_order_props "orders/" )"R" restrict nil ))nil 3352751261"" (lemma "pointwise_complete" )"" (expand "directed_complete_partial_order?" )"" (assert )"" (expand "restrict" )"" (typepred "le2" )"" (expand "directed_complete_partial_order?" )"" (flatten)"" (assert )"" (hide -2 -3)"" (expand "partial_order?" )"" (prop)"1" (expand "pointwise" )"1" (expand "preorder?" )"1" (prop)"1" expand "reflexive?" )"1" "1" (inst?) nil nil ))nil ))nil )"2" expand "transitive?" )"2" "2" "x!2" )"2" "x!2" )"2" assert )"2" "x!1(x!2)" "y!1(x!2)" "z!1(x!2)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "antisymmetric?" )"2" (skosimp*)"2" (expand "pointwise" )"2" "2" "x!2" )"2" "x!2" )"2" "x!1(x!2)" "y!1(x!2)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"bool" directed_orders"orders/" )nil scott_continuity nil ))nil 3352749145"" (lemma "scott_continuous_dcpo" ) (("" (propax) nil nil )) nil )nil scott_continuity nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.154Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-05)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
